optimize encoding of memory loads to take into account max idx withou…

…t overflowing

Also optimize encoding when load size == block size (thus, offsets are known)

ir/memory.cpp

@@ -972,16 +972,26 @@ vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
   loaded.resize(loaded_bytes, poison);
 
   expr offset = ptr.getShortOffset();
-  unsigned off_bits = Pointer::bitsShortOffset();
 
   auto fn = [&](MemBlock &blk, unsigned bid, bool local, expr &&cond) {
     bool is_poison = (type & blk.type) == DATA_NONE;
-    for (unsigned i = 0; i < loaded_bytes; ++i) {
-      unsigned idx = left2right ? i : (loaded_bytes - i - 1);
-      expr off = offset + expr::mkUInt(idx, off_bits);
-      loaded[i].add(is_poison ? poison : blk.val.load(off), cond);
-      if (!is_poison)
-        undef.insert(blk.undef.begin(), blk.undef.end());
+    if (is_poison) {
+      for (unsigned i = 0; i < loaded_bytes; ++i) {
+        loaded[i].add(poison, cond);
+      }
+    } else {
+      uint64_t blk_size = UINT64_MAX;
+      Pointer(*this, bid, local).blockSize().isUInt(blk_size);
+      expr blk_offset = blk_size == bytes ? expr::mkUInt(0, offset) : offset;
+
+      for (unsigned i = 0; i < loaded_bytes; ++i) {
+        unsigned idx = left2right ? i : (loaded_bytes - i - 1);
+        assert(idx < blk_size);
+        uint64_t max_idx = blk_size - bytes + idx;
+        expr off = blk_offset + expr::mkUInt(idx, offset);
+        loaded[i].add(blk.val.load(off, max_idx), cond);
+      }
+      undef.insert(blk.undef.begin(), blk.undef.end());
     }
   };
 

smt/expr.cpp

@@ -2001,17 +2001,22 @@ expr expr::store(const expr &idx, const expr &val) const {
   return Z3_mk_store(ctx(), ast(), idx(), val());
 }
 
-expr expr::load(const expr &idx) const {
+expr expr::load(const expr &idx, uint64_t max_idx) const {
   C(idx);
 
   // TODO: add support for alias analysis plugin
   expr array, str_idx, val;
   if (isStore(array, str_idx, val)) { // store(array, idx, val)
+    uint64_t str_idx_val;
+    // loaded idx can't possibly match the stored idx; there's UB otherwise
+    if (str_idx.isUInt(str_idx_val) && str_idx_val > max_idx)
+      return array.load(idx, max_idx);
+
     expr cmp = idx == str_idx;
     if (cmp.isTrue())
       return val;
 
-    auto loaded = array.load(idx);
+    auto loaded = array.load(idx, max_idx);
     if (cmp.isFalse() || val.eq(loaded))
       return loaded;
 

smt/expr.h

@@ -339,7 +339,7 @@ class expr {
   static expr mkConstArray(const expr &domain, const expr &value);
 
   expr store(const expr &idx, const expr &val) const;
-  expr load(const expr &idx) const;
+  expr load(const expr &idx, uint64_t max_idx = UINT64_MAX) const;
 
   static expr mkIf(const expr &cond, const expr &then, const expr &els);
   static expr mkForAll(const std::set<expr> &vars, expr &&val);