add memcpy to alive2 #88

Dongjoo-Kim · 2019-08-23T14:24:51Z

Add memcpy's SMT encoding(in memory.cpp).
Make Alive2 interpret memset and memcpy correctly(in instr.cpp, instr.h, utils.cpp).

Previous Alive2 doesn't interpret memset and memcpy, because there is no visit function for them.
So basic tests in 'test/memcpy/' made 'LLVM error: Unsupported instruction'.
I fixed it, as a result basic tests which I made are successfully verified by Alive2.

nunoplopes · 2019-08-25T22:14:40Z

llvm_util/utils.cpp

+
+  RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
+    auto fn = i.getCalledFunction();
+    if (!fn) // TODO: check real memcpy


this error checking isn't needed. The intrinsic should be valid

tests/memcpy/1-src.ll

nunoplopes · 2019-08-25T22:18:22Z

ir/instr.h

+  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) {}


these lines are too long. Please wrap at 80 columns

nunoplopes · 2019-08-25T22:20:19Z

ir/memory.cpp

@@ -304,10 +312,27 @@ 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) {
+  // TODO: Add ub condition - bytes == 0


this requites some API changes. Either address it in this PR or in a subsequent patch.

I'm not sure that when 'bytes' is zero and 'src (or tgt) pointer' is poison, the code has ub or not.

I am going to address similar cases in a subsequent patch.

That's a good point. From my understanding, LLVM folks didn't want to be too evil here, so it should be UB only if bytes > 0

nunoplopes · 2019-08-25T22:22:41Z

ir/memory.cpp

@@ -149,6 +149,14 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
  is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
 }

+expr disjoint(expr offset1, const expr &len1, expr offset2, const expr &len2) {


should be static

nunoplopes · 2019-08-25T22:23:21Z

ir/memory.cpp

@@ -149,6 +149,14 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
  is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
 }

+expr disjoint(expr offset1, const expr &len1, expr offset2, const expr &len2) {
+  return ((offset1+len1).ule(offset2) || (offset2+len2).ule(offset1));


this has too many parenthesis

nunoplopes · 2019-08-25T22:24:33Z

ir/memory.cpp

@@ -149,6 +149,14 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
  is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
 }

+expr disjoint(expr offset1, const expr &len1, expr offset2, const expr &len2) {
+  return ((offset1+len1).ule(offset2) || (offset2+len2).ule(offset1));


Is this condition correct if offset + len overflows? Or can't that happen (because of the half of the address space limitation)? If that's the case, we need a comment there explaining the assumption/reasoning.

When I use is_disjoint in memcpy, overflow checking is run in is_dereferenceable.

If we need this condition at other code, overflow condition is considered.

I add a comment in the code also.

nunoplopes

A few more comments.
Also, there are still many lines over 80 characters. The build is broken; please have a look.

nunoplopes · 2019-09-04T21:52:55Z

llvm_util/utils.cpp

+  }
+
+  RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
+    auto ty = llvm_type2alive(i.getType());


this isn't needed. same for memset

nunoplopes · 2019-09-04T21:55:17Z

ir/instr.cpp

+}
+
+StateValue Memset::toSMT(State &s) const {
+  // TODO: check following lines are correct


given the discussion below, it seems that we should have someting like s.addUB(vbytes.ugt(0).implies(np_ptr))

I modified memset, memcpy and is_dereferenceable using your conditions.
is_disjoint doesn't need modifying because when bytes is 0, is_disjoint is already no ub.

nunoplopes · 2019-09-04T21:55:51Z

ir/instr.cpp

+}
+
+
+void Memcpy::print(std::ostream &os) const {


no std:: here

nunoplopes · 2019-09-04T21:59:54Z

ir/memory.cpp

@@ -304,10 +312,27 @@ 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) {
+  // TODO: Add ub condition - bytes == 0


That's a good point. From my understanding, LLVM folks didn't want to be too evil here, so it should be UB only if bytes > 0

tests/memcpy/1-src.ll

nunoplopes

looking good. almost there :)

nunoplopes · 2019-09-08T22:16:07Z

ir/instr.cpp

+  auto &[vdst, np] = s[*dst];
+  auto &[vsrc, np2] = s[*src];
+  auto &[vbytes, np3] = s[*bytes];
+  s.addUB(vbytes.ugt(0).implies(np));


please combine the two checks into one: ".implies(np && np2)"

nunoplopes · 2019-09-08T22:18:29Z

ir/instr.cpp

+  auto &[vptr, np] = s[*ptr];
+  auto &[vbytes, np2] = s[*bytes];
+  s.addUB(vbytes.ugt(0).implies(np));
+  s.addUB(vbytes.ugt(0).implies(np2));


this second line should be simply "s.addUB(np2)". If vbytes is poison, the copy is UB since the value to copy is unbounded.

nunoplopes · 2019-09-08T22:19:48Z

ir/instr.cpp

+  auto &[vbytes, np3] = s[*bytes];
+  s.addUB(vbytes.ugt(0).implies(np));
+  s.addUB(vbytes.ugt(0).implies(np2));
+  s.addUB(vbytes.ugt(0).implies(np3));


same comment as for memset: should be addUB(np3) only.
Also, please rename vars to np_dst, np_src, or something like that. np2/np3 are error prone :)

nunoplopes · 2019-09-08T22:20:37Z

ir/instr.cpp

+}
+
+expr Memcpy::getTypeConstraints(const Function &f) const {
+  return dst->getType().enforcePtrType() && dst->getType().enforcePtrType()


please do this like:

return enforcefoo() && enforceBar && etc;

Dongjoo-Kim · 2019-09-09T10:37:10Z

I reflected your comments and pushed it.

nunoplopes

Looking good, thanks! I left a few more comments, including a question about correctness of the encoding.

nunoplopes · 2019-09-09T18:22:09Z

ir/memory.h

@@ -68,6 +68,7 @@ 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;


this is over 80 characters

nunoplopes · 2019-09-09T18:25:24Z

ir/memory.cpp

@@ -149,6 +151,20 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
  is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
 }

+// general disjoint check for unsigned integer
+static expr disjoint(expr begin1, const expr &len1, expr begin2,


typo: begin1 & begin2 should be const references as well.

ir/memory.cpp

nunoplopes · 2019-09-09T18:28:51Z

ir/memory.cpp

+    Pointer idx(*this, expr::mkVar(name.c_str(), dst.bits()));
+
+    expr cond = idx.uge(dst).both() && idx.ult(dst + bytes).both();
+    expr val = expr::mkIf(cond, blocks_val.load((src + idx.get_offset()).release()),


this lines seems over 80 characters

not sure the condition for the src load is correct. It assumes that offset of src = 0.
Remember that memcpy both src and dst may start in the middle of an object.
So we need src + "delta between start of copy and idx". Which may not be idx.get_offset() if the memcpy wasn't done the start of the object.
What do you think?

Thank you for your comment. I fixed this bug.

Dongjoo-Kim · 2019-09-14T08:13:56Z

Sorry for late response. I reflect your comments.

nunoplopes requested changes Aug 25, 2019

View reviewed changes

nunoplopes reviewed Sep 4, 2019

View reviewed changes

Dongjoo-Kim force-pushed the memcpy-share2 branch from e93bb6c to 7652232 Compare September 6, 2019 06:28

nunoplopes mentioned this pull request Sep 8, 2019

Add lit test support for opt plugin & alive-tv #95

Closed

nunoplopes reviewed Sep 8, 2019

View reviewed changes

Dongjoo-Kim force-pushed the memcpy-share2 branch from 7652232 to c6bad7c Compare September 9, 2019 07:42

nunoplopes reviewed Sep 9, 2019

View reviewed changes

Dongjoo-Kim added 5 commits September 14, 2019 17:08

add memcpy to alive2

8ce274e

reflect comments to code

fcae398

make compilalbe & consider when bytes is 0 in memset and memcpy

b540392

reflect comments to code

c241071

fix memcpy's bug

05c0d1d

Dongjoo-Kim force-pushed the memcpy-share2 branch from c6bad7c to 05c0d1d Compare September 14, 2019 08:11

nunoplopes merged commit 5356f55 into AliveToolkit:master Sep 14, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

add memcpy to alive2 #88

add memcpy to alive2 #88

Dongjoo-Kim commented Aug 23, 2019

nunoplopes Aug 25, 2019

nunoplopes Aug 25, 2019

nunoplopes Aug 25, 2019

Dongjoo-Kim Sep 3, 2019

nunoplopes Sep 4, 2019

nunoplopes Aug 25, 2019

nunoplopes Aug 25, 2019

nunoplopes Aug 25, 2019

Dongjoo-Kim Sep 3, 2019

nunoplopes left a comment

nunoplopes Sep 4, 2019

nunoplopes Sep 4, 2019

Dongjoo-Kim Sep 6, 2019

nunoplopes Sep 4, 2019

nunoplopes Sep 4, 2019

nunoplopes left a comment

nunoplopes Sep 8, 2019

nunoplopes Sep 8, 2019

nunoplopes Sep 8, 2019

nunoplopes Sep 8, 2019

Dongjoo-Kim commented Sep 9, 2019

nunoplopes left a comment

nunoplopes Sep 9, 2019

nunoplopes Sep 9, 2019

nunoplopes Sep 9, 2019

nunoplopes Sep 9, 2019

Dongjoo-Kim Sep 14, 2019

Dongjoo-Kim commented Sep 14, 2019

add memcpy to alive2 #88

add memcpy to alive2 #88

Conversation

Dongjoo-Kim commented Aug 23, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nunoplopes left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nunoplopes left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dongjoo-Kim commented Sep 9, 2019

nunoplopes left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dongjoo-Kim commented Sep 14, 2019