reflect comments to code

AliveToolkit · Sep 3, 2019 · e93bb6c · e93bb6c
1 parent 2027577
commit e93bb6c
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 14 deletions.
diff --git a/ir/instr.h b/ir/instr.h
@@ -387,7 +387,8 @@ class Memset final : public Instr {
   unsigned align;
 public:
   Memset(Value &ptr, Value &val, Value &bytes, unsigned align)
-    : Instr(Type::voidTy, "memset"), ptr(ptr), val(val), bytes(bytes), align(align) {}
+    : Instr(Type::voidTy, "memset"), ptr(ptr), val(val), bytes(bytes),
+            align(align) {}
 
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
@@ -400,8 +401,10 @@ 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) {}
+  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) {}
 
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;

diff --git a/ir/memory.cpp b/ir/memory.cpp
@@ -149,12 +149,16 @@ 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));
+// general disjoint check for unsigned integer
+static expr disjoint(expr begin1, const expr &len1, 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.
 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));
+  m.state->addUB(get_bid() != ptr2.get_bid() ||
+                  disjoint(get_offset(), len1, ptr2.get_offset(), len2));
 }
 
 ostream& operator<<(ostream &os, const Pointer &p) {

diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp
@@ -336,10 +336,6 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
   }
 
   RetTy visitMemSetInst(llvm::MemSetInst &i) {
-    auto fn = i.getCalledFunction();
-    if (!fn) // TODO: check real memset
-      return error(i);
-
     auto ty = llvm_type2alive(i.getType());
     if (ty != &Type::voidTy)
       return error(i);
@@ -355,10 +351,6 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
   }
 
   RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
-    auto fn = i.getCalledFunction();
-    if (!fn) // TODO: check real memcpy
-      return error(i);
-
     auto ty = llvm_type2alive(i.getType());
     if (ty != &Type::voidTy)
       return error(i);