add support for memmove
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1531,8 +1531,8 @@ void Memcpy::rauw(const Value &what, Value &with) {
}
void Memcpy::print(ostream &os) const {
- os << "memcpy " << *dst << " align " << align_dst << ", " << *src
- << " align " << align_src << ", " << *bytes;
+ os << (move ? "memmove " : "memcpy ") << *dst << " align " << align_dst
+ << ", " << *src << " align " << align_src << ", " << *bytes;
}
StateValue Memcpy::toSMT(State &s) const {
@@ -1541,7 +1541,7 @@ StateValue Memcpy::toSMT(State &s) const {
auto &[vbytes, np_bytes] = s[*bytes];
s.addUB(vbytes.ugt(0).implies(np_dst && np_src));
s.addUB(np_bytes);
- s.getMemory().memcpy(vdst, vsrc, vbytes, align_dst, align_src);
+ s.getMemory().memcpy(vdst, vsrc, vbytes, align_dst, align_src, move);
return {};
}
@@ -1552,7 +1552,7 @@ expr Memcpy::getTypeConstraints(const Function &f) const {
}
unique_ptr<Instr> Memcpy::dup(const string &suffix) const {
- return make_unique<Memcpy>(*dst, *src, *bytes, align_dst, align_src);
+ return make_unique<Memcpy>(*dst, *src, *bytes, align_dst, align_src, move);
}
}

MODIFY
ir/instr.h
ir/instr.h
@@ -450,11 +450,12 @@ public:
class Memcpy final : public Instr {
Value *dst, *src, *bytes;
unsigned align_dst, align_src;
+ bool move;
public:
Memcpy(Value &dst, Value &src, Value &bytes,
- unsigned align_dst, unsigned align_src)
+ unsigned align_dst, unsigned align_src, bool move)
: Instr(Type::voidTy, "memcpy"), dst(&dst), src(&src), bytes(&bytes),
- align_dst(align_dst), align_src(align_src) {}
+ align_dst(align_dst), align_src(align_src), move(move) {}
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -302,18 +302,20 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
}
void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
- unsigned align_dst, unsigned align_src) {
+ unsigned align_dst, unsigned align_src, bool move) {
Pointer dst(*this, d), src(*this, s);
dst.is_dereferenceable(bytes, align_dst);
src.is_dereferenceable(bytes, align_src);
+ if (!move)
src.is_disjoint(bytes, dst, bytes);
uint64_t n;
if (bytes.isUInt(n) && n <= 4) {
+ auto old_val = blocks_val;
for (unsigned i = 0; i < n; ++i) {
auto src_i = (src + i).release();
auto dst_i = (dst + i).release();
- blocks_val = blocks_val.store(dst_i, blocks_val.load(src_i));
+ blocks_val = blocks_val.store(dst_i, old_val.load(src_i));
}
} else {
string name = "#idx_" + to_string(last_idx_ptr++);
@@ -323,7 +325,7 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
expr cond = dst_idx.uge(dst).both() && dst_idx.ult(dst + bytes).both();
expr val = expr::mkIf(cond, blocks_val.load(src_idx()),
blocks_val.load(dst_idx()));
- blocks_val = expr::mkLambda({ dst_idx() }, move(val));
+ blocks_val = expr::mkLambda({ dst_idx() }, std::move(val));
}
}

MODIFY
ir/memory.h
ir/memory.h
@@ -108,7 +108,8 @@ public:
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytes, unsigned align);
void memcpy(const smt::expr &dst, const smt::expr &src,
- const smt::expr &bytes, unsigned align_dst, unsigned align_src);
+ const smt::expr &bytes, unsigned align_dst, unsigned align_src,
+ bool move);
smt::expr ptr2int(const smt::expr &ptr);
smt::expr int2ptr(const smt::expr &val);

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -358,7 +358,7 @@ public:
RETURN_IDENTIFIER(make_unique<Memset>(*ptr, *val, *bytes, 1));
}
- RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
+ RetTy visitMemTransferInst(llvm::MemTransferInst &i) {
auto dst = get_operand(i.getOperand(0));
auto src = get_operand(i.getOperand(1));
auto bytes = get_operand(i.getOperand(2));
@@ -366,7 +366,8 @@ public:
if (!dst || !src || !bytes)
return error(i);
- RETURN_IDENTIFIER(make_unique<Memcpy>(*dst, *src, *bytes, 1, 1));
+ RETURN_IDENTIFIER(make_unique<Memcpy>(*dst, *src, *bytes, 1, 1,
+ isa<llvm::MemMoveInst>(&i)));
}
RetTy visitICmpInst(llvm::ICmpInst &i) {

add support for memmove