further work on growable objects (#1227)

Author: nunoplopes

ir/instr.cpp

@@ -4056,13 +4056,13 @@ StateValue GEP::toSMT(State &s) const {
       // FIXME: not implemented for physical pointers
       s.addUB(ptr.isLogical());
       s.doesApproximation("gep inbounds of phy ptr", !ptr.isLogical(), true);
-      inbounds_np.add(ptr.inbounds(false));
+      inbounds_np.add(ptr.inbounds(false, true));
     }
 
     expr offset_sum = expr::mkUInt(0, bits_for_offset);
     for (auto &[sz, idx] : offsets) {
       auto &[v, np] = idx;
-      auto multiplier = expr::mkUInt(sz, bits_for_offset);
+      auto multiplier = expr::mkUInt(sz, offset_sum);
       auto val = v.sextOrTrunc(bits_for_offset);
       auto inc = multiplier * val;
 
@@ -4100,7 +4100,7 @@ StateValue GEP::toSMT(State &s) const {
       non_poison.add(np);
 
       if (inbounds)
-        inbounds_np.add(ptr.inbounds(false));
+        inbounds_np.add(ptr.inbounds(false, true));
     }
 
     if (inbounds) {
@@ -4114,7 +4114,7 @@ StateValue GEP::toSMT(State &s) const {
 
       // try to simplify the pointer
       if (all_zeros.isFalse())
-        ptr.inbounds(true);
+        ptr.inbounds(true, true);
     }
 
     return { std::move(ptr).release(), non_poison() };

ir/memory.cpp

@@ -1374,7 +1374,7 @@ expr Memory::hasStored(const Pointer &p, const expr &bytes) const {
   }
 }
 
-void Memory::record_store(const Pointer &p, const smt::expr &bytes) {
+void Memory::record_store(const Pointer &p, const expr &bytes) {
   assert(has_initializes_attr);
 
   auto is_local = p.isLocal();
@@ -1618,7 +1618,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
     state->addAxiom(q.isHeapAllocated().implies(q.blockAlignment() == align));
   }
 
-  for (unsigned bid = has_null_block; bid < num_nonlocals_src; ++bid) {
+  for (unsigned bid = skip_null(); bid < num_nonlocals_src; ++bid) {
     Pointer p(*this, bid, false);
     state->addAxiom(p.getAllocType().ult(Pointer::NUM_ALLOC_TYPES));
     state->addAxiom(p.blockSize().ule(p.blockMaxSize()));
@@ -1666,15 +1666,15 @@ void Memory::mkAxioms(const Memory &tgt) const {
              expr::mkUInt(0, 1).concat(last.extract(bits_ptr_address-2, 0)))
          : addr != last);
     } else {
-      sz = p1.blockSizeAligned().zextOrTrunc(bits_ptr_address);
+      sz = p1.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address);
       state->addAxiom(
         Pointer::hasLocalBit()
           // don't spill to local addr section
           ? (addr + sz).sign() == 0
           : addr.add_no_uoverflow(sz));
     }
 
-    state->addAxiom(p1.blockSize()
+    state->addAxiom(p1.blockMaxSize()
                       .round_up_bits_no_overflow(p1.blockAlignment()));
 
     if (num_nonlocals > max_quadratic_disjoint)
@@ -1686,7 +1686,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
         continue;
       Pointer p2(tgt, bid2, false);
       state->addAxiom(disjoint(addr, sz, align, p2.getAddress(),
-                               p2.blockSizeAligned()
+                               p2.blockMaxSizeAligned()
                                  .zextOrTrunc(bits_ptr_address),
                                p2.blockAlignment()));
     }
@@ -1958,7 +1958,7 @@ Memory::mkCallState(const string &fnname, bool nofree, unsigned num_ptr_args,
   }
 
   st.non_local_sizes.resize(num_nonlocals_src);
-  for (unsigned bid = has_null_block; bid < num_nonlocals_src; ++bid) {
+  for (unsigned bid = skip_null(); bid < num_nonlocals_src; ++bid) {
     Pointer p(*this, bid, false);
     if (!p.isGrowableAlloc().isFalse()) {
       expr max_size = p.blockMaxSize();
@@ -2117,9 +2117,9 @@ void Memory::setState(const Memory::CallState &st,
 
   // TODO: function calls can also free local objects passed by argument
 
-  for (unsigned bid = has_null_block; bid < num_nonlocals_src; ++bid) {
+  for (unsigned bid = skip_null(); bid < num_nonlocals_src; ++bid) {
     Pointer p(*this, bid, false);
-    expr growable = p.isGrowableAlloc();
+    expr growable = p.isGrowableAlloc() && access.canWrite(MemoryAccess::Other);
     if (!growable.isFalse())
       non_local_blk_size.replace(
         p.getShortBid(),

ir/pointer.cpp

@@ -78,7 +78,7 @@ Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset,
 }
 
 Pointer::Pointer(const Memory &m, const char *var_name,
-                 const ParamAttrs &attr, const std::set<smt::expr> &fn_vars)
+                 const ParamAttrs &attr, const set<expr> &fn_vars)
   : m(const_cast<Memory&>(m)) {
   auto ty = expr::mkUInt(0, bitsShortBid() + bits_for_offset);
   vector<expr> vars(fn_vars.begin(), fn_vars.end());
@@ -332,7 +332,7 @@ expr Pointer::blockSize() const {
 expr Pointer::blockMaxSize() const {
   return
     mkIf_fold(getAllocType() == GROWABLE,
-              getValue("blk_max_size", m.local_blk_size, m.non_local_blk_size,
+              getValue("blk_max_size", m.local_blk_size, {},
                        expr::mkUInt(0, bits_size_t)),
               blockSize());
 }
@@ -351,6 +351,16 @@ expr Pointer::blockSizeAlignedOffsetT() const {
   return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
 }
 
+expr Pointer::blockMaxSizeAligned() const {
+  return
+    blockMaxSize().round_up_bits(blockAlignment().zextOrTrunc(bits_size_t));
+}
+
+expr Pointer::blockMaxSizeAlignedOffsetT() const {
+  expr sz = blockMaxSizeAligned();
+  return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
+}
+
 expr Pointer::leftoverSize() const {
   auto off = getOffsetSizet();
   auto sz  = blockSizeOffsetT();
@@ -447,22 +457,23 @@ expr Pointer::isInboundsOf(const Pointer &block, const expr &bytes0,
          (addr + bytes).ule(block_addr + block_size);
 }
 
-expr Pointer::isInbounds(bool strict) const {
+expr Pointer::isInbounds(bool strict, bool max_size) const {
   auto offset = getOffsetSizet();
-  auto size   = blockSizeAlignedOffsetT();
+  auto size   = max_size ? blockMaxSizeAlignedOffsetT()
+                         : blockSizeAlignedOffsetT();
   expr ret = strict ? offset.ult(size) : offset.ule(size);
   if (bits_for_offset <= bits_size_t) // implied
     ret &= !offset.isNegative();
   return ret;
 }
 
-expr Pointer::inbounds(bool simplify_ptr) {
+expr Pointer::inbounds(bool simplify_ptr, bool max_size) {
   if (!simplify_ptr)
-    return isInbounds(false);
+    return isInbounds(false, max_size);
 
   DisjointExpr<expr> ret(expr(false)), all_ptrs;
   for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
-    expr inb = Pointer(m, ptr_expr).isInbounds(false);
+    expr inb = Pointer(m, ptr_expr).isInbounds(false, max_size);
     if (!inb.isFalse())
       all_ptrs.add(ptr_expr, domain);
     ret.add(std::move(inb), domain);

ir/pointer.h

@@ -92,6 +92,8 @@ class Pointer {
   smt::expr blockSizeOffsetT() const; // to compare with offsets
   smt::expr blockSizeAligned() const;
   smt::expr blockSizeAlignedOffsetT() const; // to compare with offsets
+  smt::expr blockMaxSizeAligned() const;
+  smt::expr blockMaxSizeAlignedOffsetT() const;
 
   smt::expr leftoverSize() const;
 
@@ -118,8 +120,8 @@ class Pointer {
                       bool is_phy) const;
   smt::expr isInboundsOf(const Pointer &block, const smt::expr &bytes,
                          bool is_phy) const;
-  smt::expr isInbounds(bool strict) const;
-  smt::expr inbounds(bool simplify_ptr = false);
+  smt::expr isInbounds(bool strict, bool max_size = false) const;
+  smt::expr inbounds(bool simplify_ptr = false, bool max_size = false);
 
   smt::expr blockAlignment() const; // log(bits)
   smt::expr isBlockAligned(uint64_t align, bool exact = false) const;