fix bug when producing axioms for non-local blocks after fn call

also works as optimization as formulas get a bit smaller

ir/memory.cpp

@@ -1423,20 +1423,6 @@ static expr mk_liveness_array() {
   return expr::mkInt(-1, num_nonlocals);
 }
 
-void Memory::mkNonPoisonAxioms(bool local) const {
-  expr offset = expr::mkQVar(0, Pointer::bitsShortOffset());
-  const char *name = "#axoff";
-
-  unsigned bid = 0;
-  for (auto &block : local ? local_block_val : non_local_block_val) {
-    if (isInitialMemBlock(block.val, config::disallow_ub_exploitation))
-      state->addAxiom(
-        expr::mkForAll(1, &offset, &name,
-                       !raw_load(local, bid, offset).isPoison()));
-    ++bid;
-  }
-}
-
 expr Memory::mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const {
   bool mk_axiom = &val == &val2;
 
@@ -1462,62 +1448,56 @@ expr Memory::mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const {
          val2.nonptrValue().lshr(leftover_bits) == 0;
 }
 
-void Memory::mkNonlocalValAxioms(bool skip_consts) const {
+void Memory::mkNonlocalValAxioms(const expr &block) const {
+  expr offset = expr::mkQVar(0, Pointer::bitsShortOffset());
+  const char *name = "#axoff";
+  Byte byte(*this, ::raw_load(block, offset));
+
   // Users may request the initial memory to be non-poisonous
   if ((config::disable_poison_input && state->isSource()) &&
       (does_int_mem_access || does_ptr_mem_access)) {
-    mkNonPoisonAxioms(false);
+    state->addAxiom(expr::mkForAll(1, &offset, &name, !byte.isPoison()));
   }
 
-  if (!does_ptr_mem_access && !(num_sub_byte_bits && isAsmMode()))
+  if (!does_ptr_mem_access && !(num_sub_byte_bits && config::tgt_is_asm))
     return;
 
-  expr offset = expr::mkQVar(0, Pointer::bitsShortOffset());
-  const char *name = "#axoff";
-
-  for (unsigned i = 0, e = numNonlocals(); i != e; ++i) {
-    if (always_noread(i, true))
-      continue;
-
-    Byte byte = raw_load(false, i, offset);
+  // in ASM mode, non-byte-aligned values are expected to be zero-extended
+  // per the ABI.
+  if (num_sub_byte_bits && config::tgt_is_asm) {
+    state->addAxiom(
+      expr::mkForAll(1, &offset, &name, mkSubByteZExtStoreCond(byte, byte)));
+  }
 
-    // in ASM mode, non-byte-aligned values are expected to be zero-extended
-    // per the ABI.
-    if (num_sub_byte_bits && isAsmMode()) {
-      state->addAxiom(
-        expr::mkForAll(1, &offset, &name, mkSubByteZExtStoreCond(byte, byte)));
-    }
+  if (!does_ptr_mem_access)
+    return;
 
-    if (!does_ptr_mem_access)
-      continue;
+  Pointer loadedptr = byte.ptr();
+  expr bid = loadedptr.getShortBid();
 
-    Pointer loadedptr = byte.ptr();
-    expr bid = loadedptr.getShortBid();
-
-    unsigned upperbid = numNonlocals() - 1;
-    expr bid_cond(true);
-    if (has_fncall) {
-      // initial memory cannot contain a pointer to fncall mem block.
-      if (is_fncall_mem(upperbid)) {
-        upperbid--;
-      } else if (has_write_fncall && !num_inaccessiblememonly_fns) {
-        assert(!state->isSource()); // target-only glb vars exist
-        bid_cond = bid != get_fncallmem_bid();
-      } else if (num_inaccessiblememonly_fns) {
-        bid_cond = bid.ult(num_nonlocals_src - num_inaccessiblememonly_fns
-                                             - has_write_fncall);
-        if (upperbid > num_nonlocals_src)
-          bid_cond |= bid.ugt(num_nonlocals_src - 1);
-      }
+  unsigned upperbid = numNonlocals() - 1;
+  expr bid_cond(true);
+  if (has_fncall) {
+    // initial memory cannot contain a pointer to fncall mem block.
+    if (is_fncall_mem(upperbid)) {
+      upperbid--;
+    } else if (has_write_fncall && !num_inaccessiblememonly_fns) {
+      assert(!state->isSource()); // target-only glb vars exist
+      bid_cond = bid != get_fncallmem_bid();
+    } else if (num_inaccessiblememonly_fns) {
+      bid_cond = bid.ult(num_nonlocals_src - num_inaccessiblememonly_fns
+                                            - has_write_fncall);
+      if (upperbid > num_nonlocals_src)
+        bid_cond |= bid.ugt(num_nonlocals_src - 1);
     }
-    bid_cond &= bid.ule(upperbid);
-
-    state->addAxiom(
-      expr::mkForAll(1, &offset, &name,
-        byte.isPtr().implies(!loadedptr.isLocal(false) &&
-                             !loadedptr.isNocapture(false) &&
-                             std::move(bid_cond))));
   }
+  bid_cond &= bid.ule(upperbid);
+
+  state->addAxiom(
+    expr::mkForAll(1, &offset, &name,
+      byte.isPtr().implies(!loadedptr.isLocal(false) &&
+                           !loadedptr.isNocapture(false) &&
+                           bid_cond)));
 }
 
 bool Memory::isAsmMode() const {
@@ -1586,14 +1566,8 @@ void Memory::mkAxioms(const Memory &tgt) const {
 
   // Non-local blocks cannot initially contain pointers to local blocks
   // and no-capture pointers.
-  for (auto m_ptr : { this, &tgt }) {
-    auto &m = const_cast<Memory&>(*m_ptr);
-    auto old_vals = m.non_local_block_val;
-    for (unsigned i = skip_null(), e = old_vals.size(); i != e; ++i) {
-      m.non_local_block_val.at(i).val = m.mk_block_val_array(i);
-    }
-    m.mkNonlocalValAxioms(false);
-    m.non_local_block_val = std::move(old_vals);
+  for (unsigned i = skip_null(), e = numNonlocals(); i != e; ++i) {
+    mkNonlocalValAxioms(mk_block_val_array(i));
   }
 
   auto skip_bid = [&](unsigned bid) {
@@ -1975,6 +1949,10 @@ Memory::mkCallState(const string &fnname, bool nofree, unsigned num_ptr_args,
                   st.non_local_liveness);
   }
 
+  for (auto &block : st.non_local_block_val) {
+    mkNonlocalValAxioms(block);
+  }
+
   return st;
 }
 
@@ -2074,8 +2052,6 @@ void Memory::setState(const Memory::CallState &st,
 
   // TODO: function calls can also free local objects passed by argument
 
-  mkNonlocalValAxioms(true);
-
   // TODO: havoc local blocks
   // for now, zero out if in non UB-exploitation mode to avoid false positives
   if (config::disallow_ub_exploitation) {

ir/memory.h

@@ -198,9 +198,8 @@ class Memory {
 
   smt::expr isBlockAlive(const smt::expr &bid, bool local) const;
 
-  void mkNonPoisonAxioms(bool local) const;
   smt::expr mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const;
-  void mkNonlocalValAxioms(bool skip_consts) const;
+  void mkNonlocalValAxioms(const smt::expr &block) const;
 
   bool mayalias(bool local, unsigned bid, const smt::expr &offset,
                 const smt::expr &bytes, uint64_t align, bool write) const;