add support for memcpy
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1485,4 +1485,74 @@ unique_ptr<Instr> Store::dup(const string &suffix) const {
return make_unique<Store>(*ptr, *val, align);
}
+
+vector<Value*> Memset::operands() const {
+ return { ptr, val, bytes };
+}
+
+void Memset::rauw(const Value &what, Value &with) {
+ RAUW(ptr);
+ RAUW(val);
+ RAUW(bytes);
+}
+
+void Memset::print(ostream &os) const {
+ os << "memset " << *ptr << " align " << align << ", " << *val
+ << ", " << *bytes;
+}
+
+StateValue Memset::toSMT(State &s) const {
+ auto &[vptr, np_ptr] = s[*ptr];
+ auto &[vbytes, np_bytes] = s[*bytes];
+ s.addUB(vbytes.ugt(0).implies(np_ptr));
+ s.addUB(np_bytes);
+ s.getMemory().memset(vptr, s[*val], vbytes, align);
+ return {};
+}
+
+expr Memset::getTypeConstraints(const Function &f) const {
+ return ptr->getType().enforcePtrType() &&
+ bytes->getType().enforceIntType();
+}
+
+unique_ptr<Instr> Memset::dup(const string &suffix) const {
+ return make_unique<Memset>(*ptr, *val, *bytes, align);
+}
+
+
+vector<Value*> Memcpy::operands() const {
+ return { dst, src, bytes };
+}
+
+void Memcpy::rauw(const Value &what, Value &with) {
+ RAUW(dst);
+ RAUW(src);
+ RAUW(bytes);
+}
+
+void Memcpy::print(ostream &os) const {
+ os << "memcpy " << *dst << " align " << align_dst << ", " << *src
+ << " align " << align_src << ", " << *bytes;
+}
+
+StateValue Memcpy::toSMT(State &s) const {
+ auto &[vdst, np_dst] = s[*dst];
+ auto &[vsrc, np_src] = s[*src];
+ 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);
+ return {};
+}
+
+expr Memcpy::getTypeConstraints(const Function &f) const {
+ return dst->getType().enforcePtrType() &&
+ dst->getType().enforcePtrType() &&
+ bytes->getType().enforceIntType();
+}
+
+unique_ptr<Instr> Memcpy::dup(const string &suffix) const {
+ return make_unique<Memcpy>(*dst, *src, *bytes, align_dst, align_src);
+}
+
}

MODIFY
ir/instr.h
ir/instr.h
@@ -429,4 +429,39 @@ public:
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
};
+
+class Memset final : public Instr {
+ Value *ptr, *val, *bytes;
+ unsigned align;
+public:
+ Memset(Value &ptr, Value &val, Value &bytes, unsigned align)
+ : Instr(Type::voidTy, "memset"), ptr(&ptr), val(&val), bytes(&bytes),
+ align(align) {}
+
+ std::vector<Value*> operands() const override;
+ void rauw(const Value &what, Value &with) override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
+class Memcpy final : public Instr {
+ Value *dst, *src, *bytes;
+ unsigned align_dst, align_src;
+public:
+ Memcpy(Value &dst, Value &src, Value &bytes,
+ unsigned align_dst, unsigned align_src)
+ : Instr(Type::voidTy, "memcpy"), dst(&dst), src(&src), bytes(&bytes),
+ align_dst(align_dst), align_src(align_src) {}
+
+ std::vector<Value*> operands() const override;
+ void rauw(const Value &what, Value &with) override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -130,16 +130,18 @@ expr Pointer::is_aligned(unsigned align) const {
return true;
}
+// When bytes is 0, pointer is always derefenceable
void Pointer::is_dereferenceable(const expr &bytes, unsigned align) {
expr block_sz = block_size();
expr offset = get_offset();
// 1) check that offset is within bounds and that arith doesn't overflow
- m.state->addUB((offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz));
- m.state->addUB(offset.add_no_uoverflow(bytes));
+ m.state->addUB(bytes.ugt(0).implies(
+ (offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz)));
+ m.state->addUB(bytes.ugt(0).implies(offset.add_no_uoverflow(bytes)));
// 2) check block's address is aligned
- m.state->addUB(is_aligned(align));
+ m.state->addUB(bytes.ugt(0).implies(is_aligned(align)));
// 3) check block is alive
// TODO
@@ -149,6 +151,21 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
}
+// general disjoint check for unsigned integer
+// This function assumes that both begin + len don't overflow
+static expr disjoint(const expr begin1, const expr &len1, const expr begin2,
+ const expr &len2) {
+ return begin1.uge(begin2 + len2) || begin2.uge(begin1 + len1);
+}
+
+// offset + len's overflow is checked by 'is_dereferenceable' at line 139.
+// When bytes is zero, this is already no ub.
+void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2,
+ const expr &len2) const {
+ m.state->addUB(get_bid() != ptr2.get_bid() ||
+ disjoint(get_offset(), len1, ptr2.get_offset(), len2));
+}
+
ostream& operator<<(ostream &os, const Pointer &p) {
os << "pointer(" << (p.is_local().simplify().isTrue() ? "local" : "non-local")
<< ", block_id=";
@@ -283,7 +300,25 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
Pointer dst(*this, d), src(*this, s);
dst.is_dereferenceable(bytes, align_dst);
src.is_dereferenceable(bytes, align_src);
- // TODO
+ src.is_disjoint(bytes, dst, bytes);
+
+ uint64_t n;
+ if (bytes.isUInt(n) && n <= 4) {
+ 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));
+ }
+ } else {
+ string name = "#idx_" + to_string(last_idx_ptr++);
+ Pointer dst_idx(*this, expr::mkVar(name.c_str(), dst.bits()));
+ Pointer src_idx = src + (dst_idx.get_offset() - dst.get_offset());
+
+ 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));
+ }
}
expr Memory::ptr2int(const expr &ptr) {

MODIFY
ir/memory.h
ir/memory.h
@@ -68,6 +68,8 @@ public:
smt::expr is_aligned(unsigned align) const;
void is_dereferenceable(unsigned bytes, unsigned align);
void is_dereferenceable(const smt::expr &bytes, unsigned align);
+ void is_disjoint(const smt::expr &len1, const Pointer &ptr2,
+ const smt::expr &len2) const;
friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -347,6 +347,28 @@ public:
RETURN_IDENTIFIER(move(call));
}
+ RetTy visitMemSetInst(llvm::MemSetInst &i) {
+ auto ptr = get_operand(i.getOperand(0));
+ auto val = get_operand(i.getOperand(1));
+ auto bytes = get_operand(i.getOperand(2));
+ // TODO: add isvolatile, alignment
+ if (!ptr || !val || !bytes)
+ return error(i);
+
+ RETURN_IDENTIFIER(make_unique<Memset>(*ptr, *val, *bytes, 1));
+ }
+
+ RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
+ auto dst = get_operand(i.getOperand(0));
+ auto src = get_operand(i.getOperand(1));
+ auto bytes = get_operand(i.getOperand(2));
+ // TODO: add isvolatile, alignment
+ if (!dst || !src || !bytes)
+ return error(i);
+
+ RETURN_IDENTIFIER(make_unique<Memcpy>(*dst, *src, *bytes, 1, 1));
+ }
+
RetTy visitICmpInst(llvm::ICmpInst &i) {
PARSE_BINOP();
ICmp::Cond cond;

ADD
tests/memcpy/1-src.ll
+declare void @llvm.memcpy.p0i8.p0i8.i32(i8*, i8*, i32, i1)
+
+define i8 @f() {
+ %p1 = alloca [16 x i8]
+ %p2 = bitcast [16 x i8]* %p1 to i8*
+ %p3 = alloca [16 x i8]
+ %p4 = bitcast [16 x i8]* %p3 to i8*
+ store i8 3, i8* %p2
+ call void @llvm.memcpy.p0i8.p0i8.i32(i8* %p4, i8* %p2, i32 1, i1 0)
+ %v = load i8, i8* %p4
+ ret i8 %v
+}

ADD
tests/memcpy/1-tgt.ll
+define i8 @f() {
+ ret i8 1
+}

ADD
tests/memcpy/2-src.ll
+declare void @llvm.memset.p0i8.i8(i8*, i8, i32, i1)
+
+define i8 @f() {
+ %p1 = alloca [16 x i8]
+ %p2 = bitcast [16 x i8]* %p1 to i8*
+ %p3 = getelementptr i8, i8* %p2 , i32 6
+ call void @llvm.memset.p0i8.i8(i8* %p2, i8 3, i32 16, i1 0)
+ %v = load i8, i8* %p3
+ ret i8 %v
+}

ADD
tests/memcpy/2-tgt.ll
+define i8 @f() {
+ ret i8 3
+}

ADD
tests/memcpy/3-src.ll
+declare void @llvm.memcpy.p0i8.p0i8.i32(i8*, i8*, i32, i1)
+declare void @llvm.memset.p0i8.i8(i8*, i8, i32, i1)
+
+define i8 @f() {
+ %p1 = alloca [16 x i8]
+ %p2 = bitcast [16 x i8]* %p1 to i8*
+ call void @llvm.memset.p0i8.i8(i8* %p2, i8 3, i32 2, i1 0)
+ %p3 = getelementptr i8, i8* %p2 , i32 2
+ call void @llvm.memcpy.p0i8.p0i8.i32(i8* %p3, i8* %p2, i32 3, i1 0)
+ %v = load i8, i8* %p3
+ ret i8 %v
+}

ADD
tests/memcpy/3-tgt.ll
+define i8 @f() {
+ ret i8 1
+}

ADD
tests/memcpy/4-src.ll
+declare void @llvm.memcpy.p0i8.p0i8.i32(i8*, i8*, i32, i1)
+declare void @llvm.memset.p0i8.i8(i8*, i8, i32, i1)
+
+define i8 @f() {
+ %p1 = alloca [16 x i8]
+ %p2 = bitcast [16 x i8]* %p1 to i8*
+ %p3 = alloca [16 x i8]
+ %p4 = bitcast [16 x i8]* %p3 to i8*
+ call void @llvm.memset.p0i8.i8(i8* %p2, i8 3, i32 16, i1 0)
+ call void @llvm.memcpy.p0i8.p0i8.i32(i8* %p4, i8* %p2, i32 16, i1 0)
+ %p5 = getelementptr i8, i8* %p4 , i32 6
+ %v = load i8, i8* %p5
+ ret i8 %v
+}

ADD
tests/memcpy/4-tgt.ll
+define i8 @f() {
+ ret i8 3
+}

add support for memcpy (#88)