add memcpy to alive2

ir/instr.cpp

@@ -1501,4 +1501,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);
+}
+
 }

ir/instr.h

@@ -429,4 +429,39 @@ class Store final : public Instr {
   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;
+};
+
 }

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=";
@@ -307,7 +324,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) {

ir/memory.h

@@ -68,6 +68,8 @@ class Pointer {
   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);
 };

llvm_util/utils.cpp

@@ -347,6 +347,28 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
     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;

tests/memcpy/1-src.ll

@@ -0,0 +1,12 @@
+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
+}

tests/memcpy/1-tgt.ll

@@ -0,0 +1,3 @@
+define i8 @f() {
+  ret i8 1
+}

tests/memcpy/2-src.ll

@@ -0,0 +1,10 @@
+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
+}

tests/memcpy/2-tgt.ll

@@ -0,0 +1,3 @@
+define i8 @f() {
+  ret i8 3
+}

tests/memcpy/3-src.ll

@@ -0,0 +1,12 @@
+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
+}

tests/memcpy/3-tgt.ll

@@ -0,0 +1,3 @@
+define i8 @f() {
+  ret i8 1
+}

tests/memcpy/4-src.ll

@@ -0,0 +1,14 @@
+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
+}

tests/memcpy/4-tgt.ll

@@ -0,0 +1,3 @@
+define i8 @f() {
+  ret i8 3
+}