add preliminary support for the 'initialized' param attr

cf #1125

ir/attrs.cpp

@@ -10,6 +10,7 @@
 #include "ir/state_value.h"
 #include "ir/type.h"
 #include "util/compiler.h"
+#include <algorithm>
 #include <cassert>
 
 using namespace std;
@@ -56,6 +57,17 @@ ostream& operator<<(ostream &os, const ParamAttrs &attr) {
     os << "dead_on_unwind ";
   if (attr.has(ParamAttrs::Writable))
     os << "writable ";
+  if (!attr.initializes.empty()) {
+    os << "initializes(";
+    bool first = true;
+    for (auto [low, high] : attr.initializes) {
+      if (!first)
+        os << ", ";
+      first = false;
+      os << '(' << low << ", " << high << ')';
+    }
+    os << ") ";
+  }
   return os;
 }
 
@@ -342,6 +354,9 @@ uint64_t ParamAttrs::maxAccessSize() const {
   uint64_t bytes = getDerefBytes();
   if (has(ParamAttrs::DereferenceableOrNull))
     bytes = max(bytes, derefOrNullBytes);
+  for (auto [low, high] : initializes) {
+    bytes = max(bytes, high);
+  }
   return round_up(bytes, align);
 }
 
@@ -351,6 +366,10 @@ void ParamAttrs::merge(const ParamAttrs &other) {
   derefOrNullBytes = max(derefOrNullBytes, other.derefOrNullBytes);
   blockSize        = max(blockSize, other.blockSize);
   align            = max(align, other.align);
+
+  decltype(initializes) tmp;
+  ranges::set_union(initializes, other.initializes, std::back_inserter(tmp));
+  initializes = std::move(tmp);
 }
 
 static expr
@@ -406,12 +425,19 @@ StateValue ParamAttrs::encode(State &s, StateValue &&val, const Type &ty,
     val.non_poison &= !isfpclass(val.value, ty, nofpclass);
   }
 
-  if (ty.isPtrType())
+  if (ty.isPtrType()) {
     val.non_poison &=
       encodePtrAttrs(s, val.value, getDerefBytes(), derefOrNullBytes, align,
                      has(NonNull), has(NoCapture), has(Writable), {}, nullptr,
                      isdecl);
 
+    if (!initializes.empty()) {
+      Pointer p(s.getMemory(), val.value);
+      uint64_t high = initializes.back().second;
+      s.addUB(p.addNoUSOverflow(expr::mkUInt(high, bits_for_offset), false));
+    }
+  }
+
   if (poisonImpliesUB()) {
     s.addUB(std::move(val.non_poison));
     val.non_poison = true;

ir/attrs.h

@@ -82,6 +82,8 @@ class ParamAttrs final {
   uint64_t align = 1;
   uint16_t nofpclass = 0;
 
+  std::vector<std::pair<uint64_t, uint64_t>> initializes;
+
   bool has(Attribute a) const { return (bits & a) != 0; }
   void set(Attribute a) { bits |= (unsigned)a; }
   bool refinedBy(const ParamAttrs &other) const;

ir/memory.cpp

@@ -1296,6 +1296,48 @@ void Memory::storeLambda(const Pointer &ptr, const expr &offset,
   access(ptr, bytes.zextOrTrunc(bits_size_t), align, true, fn);
 }
 
+
+expr Memory::hasStored(const Pointer &p, const expr &bytes) const {
+  unsigned bytes_per_byte = bits_byte / 8;
+  expr bid = p.getShortBid();
+  expr offset = p.getShortOffset();
+  uint64_t bytes_i;
+  if (bytes.isUInt(bytes_i) && (bytes_i / bytes_per_byte) <= 8) {
+    expr ret = true;
+    for (uint64_t off = 0; off < (bytes_i / bytes_per_byte); ++off) {
+      expr off_expr = expr::mkUInt(off, Pointer::bitsShortOffset());
+      ret &= has_stored_arg.load(bid.concat(offset + off_expr));
+    }
+    return ret;
+  } else {
+    expr var = expr::mkFreshVar("#off", offset);
+    state->addQuantVar(var);
+    expr bytes_div = bytes.udiv(expr::mkUInt(bytes_per_byte, bytes));
+    return (var.uge(offset) && var.ult(offset + bytes_div))
+             .implies(has_stored_arg.load(bid.concat(var)));
+  }
+}
+
+void Memory::record_store(const Pointer &p, const smt::expr &bytes) {
+  unsigned bytes_per_byte = bits_byte / 8;
+  expr bid = p.getShortBid();
+  expr offset = p.getShortOffset();
+  uint64_t bytes_i;
+  if (bytes.isUInt(bytes_i) && (bytes_i / bytes_per_byte) <= 8) {
+    for (uint64_t off = 0; off < (bytes_i / bytes_per_byte); ++off) {
+      expr off_expr = expr::mkUInt(off, Pointer::bitsShortOffset());
+      has_stored_arg
+        = has_stored_arg.store(bid.concat(offset + off_expr), true);
+    }
+  } else {
+    expr var = expr::mkFreshVar("#off", offset);
+    expr bytes_div = bytes.udiv(expr::mkUInt(bytes_per_byte, bytes));
+    has_stored_arg = expr::mkLambda(var,
+      (var.uge(offset) && var.ult(offset + bytes_div)) ||
+      has_stored_arg.load(bid.concat(var)));
+  }
+}
+
 static bool memory_unused() {
   return num_locals_src == 0 && num_locals_tgt == 0 && num_nonlocals == 0;
 }
@@ -1448,6 +1490,10 @@ Memory::Memory(State &state)
     local_block_liveness = expr::mkUInt(0, numLocals());
   }
 
+  // no argument has been written to at entry
+  unsigned bits = Pointer::bitsShortBid() + Pointer::bitsShortOffset();
+  has_stored_arg = expr::mkConstArray(expr::mkUInt(0, bits), false);
+
   // Initialize a memory block for null pointer.
   if (skip_null) {
     auto zero = expr::mkUInt(0, bits_size_t);
@@ -2706,6 +2752,8 @@ Memory Memory::mkIf(const expr &cond, Memory &&then, Memory &&els) {
                                             els.non_local_block_liveness);
   ret.local_block_liveness     = expr::mkIf(cond, then.local_block_liveness,
                                             els.local_block_liveness);
+  ret.has_stored_arg           = expr::mkIf(cond, then.has_stored_arg,
+                                            els.has_stored_arg);
   ret.local_blk_addr.add(els.local_blk_addr);
   ret.local_blk_size.add(els.local_blk_size);
   ret.local_blk_align.add(els.local_blk_align);
@@ -2855,6 +2903,7 @@ ostream& operator<<(ostream &os, const Memory &m) {
   if (!m.local_blk_addr.empty()) {
     os << "\nLOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
   }
+  os << "\nSTORED ADDRS: " << m.has_stored_arg << '\n';
   if (!m.ptr_alias.empty()) {
     os << "\nALIAS SETS:\n";
     for (auto &[bid, alias] : m.ptr_alias) {

ir/memory.h

@@ -154,6 +154,9 @@ class Memory {
   smt::expr non_local_block_liveness; // BV w/ 1 bit per bid (1 if live)
   smt::expr local_block_liveness;
 
+  // TODO: change from short idx to arg number
+  smt::expr has_stored_arg; // (short idx, short offset) -> bool
+
   smt::FunctionExpr local_blk_addr; // bid -> (bits_size_t - 1)
   smt::FunctionExpr local_blk_size;
   smt::FunctionExpr local_blk_align;
@@ -223,6 +226,10 @@ class Memory {
                    const std::vector<std::pair<unsigned, smt::expr>> &data,
                    const std::set<smt::expr> &undef, uint64_t align);
 
+  // to implement the 'initializes' parameter attribute
+  smt::expr hasStored(const Pointer &p, const smt::expr &bytes) const;
+  void record_store(const Pointer &p, const smt::expr &bytes);
+
   smt::expr blockValRefined(const Memory &other, unsigned bid, bool local,
                             const smt::expr &offset,
                             std::set<smt::expr> &undef) const;

ir/pointer.cpp

@@ -69,7 +69,7 @@ static expr attr_to_bitvec(const ParamAttrs &attrs) {
 namespace IR {
 
 Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset,
-                 const expr &attr) : m(m),
+                 const expr &attr) : m(const_cast<Memory&>(m)),
   p(prepend_if(expr::mkUInt(0, 1 + padding_logical()),
                bid.concat(offset), hasLogicalBit())) {
   if (bits_for_ptrattrs)
@@ -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) : m(m) {
+                 const ParamAttrs &attr) : m(const_cast<Memory&>(m)) {
   unsigned bits = bitsShortBid() + bits_for_offset;
   p = expr::mkVar(var_name, bits, false)
         .zext(hasLocalBit() + (1 + padding_logical()) * hasLogicalBit());
@@ -87,12 +87,13 @@ Pointer::Pointer(const Memory &m, const char *var_name,
   assert(p.bits() == totalBits());
 }
 
-Pointer::Pointer(const Memory &m, expr repr) : m(m), p(std::move(repr)) {
+Pointer::Pointer(const Memory &m, expr repr)
+  : m(const_cast<Memory&>(m)), p(std::move(repr)) {
   assert(!p.isValid() || p.bits() == totalBits());
 }
 
 Pointer::Pointer(const Memory &m, unsigned bid, bool local, expr attr)
-  : m(m), p(
+  : m(const_cast<Memory&>(m)), p(
     prepend_if(expr::mkUInt(0, 1 + padding_logical()),
       prepend_if(expr::mkUInt(local, 1),
                  expr::mkUInt(bid, bitsShortBid())
@@ -522,12 +523,35 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
     bytes = bytes.round_up(expr::mkUInt(align, bytes));
   expr bytes_off = bytes.zextOrTrunc(bits_for_offset);
 
-  auto block_constraints = [=](const Pointer &p) {
+  auto block_constraints = [&](const Pointer &p) {
     expr ret = p.isBlockAlive();
     if (iswrite)
       ret &= p.isWritable() && !p.isNoWrite();
     else if (!ignore_accessability)
       ret &= !p.isNoRead();
+
+    // If we are loading from an argument and it has the 'initializes'
+    // attribute, make sure we have already stored to it before.
+    if (!ignore_accessability && !iswrite) {
+      auto &s = m.getState();
+      for (auto &input0 : s.getFn().getInputs()) {
+        auto &input = static_cast<const Input&>(input0);
+        auto &inits = input.getAttributes().initializes;
+        if (inits.empty())
+          continue;
+
+        Pointer arg(m, s[input].value);
+        expr offsets = true;
+        for (auto [l, h] : inits) {
+          offsets &= (p.getOffset().uge((arg + l).getOffset()) &&
+                      p.getOffset().ult((arg + h).getOffset())
+                     ).implies(m.hasStored(p, bytes));
+        }
+        // TODO: isBasedOnArg is not sufficient; we have to store the arg number
+        // in the pointer as we can have 2 args with same initializes attr
+        ret&= (p.isBasedOnArg() && p.getBid() == arg.getBid()).implies(offsets);
+      }
+    }
     return ret;
   };
 
@@ -560,6 +584,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
     DisjointExpr<expr> addrs(expr::mkUInt(0, bits_ptr_address));
     expr ub = false;
     bool all_same_size = true;
+    expr addr = is_phy ? p.getPhysicalAddress() : p.getAddress();
 
     auto add = [&](unsigned limit, bool local) {
       for (unsigned i = 0; i != limit; ++i) {
@@ -569,20 +594,25 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
 
         Pointer this_ptr(m, i, local, p.getAttrs());
 
+        bool same_size = bytes.eq(this_ptr.blockSizeAligned());
+        expr this_addr = this_ptr.getLogAddress();
+        expr offset
+          = same_size ? expr::mkUInt(0, bits_for_offset) : addr - this_addr;
+
         expr cond = p.isInboundsOf(this_ptr, bytes, is_phy) &&
-                    block_constraints(this_ptr);
+                    block_constraints(this_ptr + offset);
         if (cond.isFalse())
           continue;
 
         ub |= cond;
 
         cond = p.isOfBlock(this_ptr, bytes, is_phy);
 
-        all_same_size &= bytes.eq(this_ptr.blockSizeAligned());
+        all_same_size &= same_size;
 
         bids.add(
           observes_local ? this_ptr.getBid() : this_ptr.getShortBid(), cond);
-        addrs.add(this_ptr.getLogAddress(), std::move(cond));
+        addrs.add(std::move(this_addr), std::move(cond));
       }
     };
     add(m.numLocals(), true);
@@ -592,8 +622,6 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
     if (!observes_local)
       bid = mkLongBid(bid, false);
 
-    expr addr = is_phy ? p.getPhysicalAddress() : p.getAddress();
-
     return { std::move(ub),
              Pointer(m, std::move(bid),
                      all_same_size
@@ -671,6 +699,9 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
   auto ptrs = std::move(all_ptrs)();
   p = ptrs ? *std::move(ptrs) : expr::mkUInt(0, totalBits());
 
+  if (!ignore_accessability && iswrite)
+    m.record_store(*this, bytes);
+
   return { std::move(exprs), *std::move(is_aligned)() };
 }
 

ir/pointer.h

@@ -15,7 +15,7 @@ namespace IR {
 class Memory;
 
 class Pointer {
-  const Memory &m;
+  Memory &m;
 
   // [0, padding, bid, offset, attributes (1 bit for each)] -- logical pointer
   // [1, padding, address, attributes] -- physical pointer

llvm_util/llvm2alive.cpp

@@ -17,6 +17,7 @@
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Operator.h"
 #include "llvm/Support/ModRef.h"
+#include <algorithm>
 #include <sstream>
 #include <unordered_map>
 #include <unordered_set>
@@ -1466,7 +1467,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
   unique_ptr<Instr>
   handleRangeAttrNoInsert(const llvm::Attribute &attr, Value &val,
                           bool is_welldefined = false) {
-    auto CR = attr.getValueAsConstantRange();
+    auto &CR = attr.getValueAsConstantRange();
     vector<Value*> bounds{ make_intconst(CR.getLower()),
                            make_intconst(CR.getUpper()) };
     string name = "%#range_" + to_string(range_idx++) + "_" + val.getName();
@@ -1590,6 +1591,19 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
         attrs.set(ParamAttrs::DeadOnUnwind);
         break;
 
+      case llvm::Attribute::Initializes:
+        for (auto &CR : llvmattr.getInitializes()) {
+          auto l = CR.getLower().tryZExtValue();
+          auto h = CR.getUpper().tryZExtValue();
+          if (!l || !h) {
+            errorAttr(llvmattr);
+            return false;
+          }
+          attrs.initializes.emplace_back(*l, *h);
+        }
+        ranges::sort(attrs.initializes);
+        break;
+
       default:
         // If it is call site, it should be added at approximation list
         if (!is_callsite)

smt/expr.cpp

@@ -732,7 +732,7 @@ expr expr::sdiv(const expr &rhs) const {
   if (rhs.isZero())
     return rhs;
 
-  if (isZero())
+  if (isZero() || rhs.isOne())
     return *this;
 
   if (isSMin() && rhs.isAllOnes())
@@ -748,7 +748,7 @@ expr expr::udiv(const expr &rhs) const {
   if (rhs.isZero())
     return rhs;
 
-  if (isZero())
+  if (isZero() || rhs.isOne())
     return *this;
 
   return binop_fold(rhs, Z3_mk_bvudiv);