Revert "add preliminary support for the 'initialized' param attr"

This reverts commit 77e9d25.

Author: jmciver

ir/attrs.cpp

@@ -10,7 +10,6 @@
 #include "ir/state_value.h"
 #include "ir/type.h"
 #include "util/compiler.h"
-#include <algorithm>
 #include <cassert>
 
 using namespace std;
@@ -57,17 +56,6 @@ 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;
 }
 
@@ -354,9 +342,6 @@ 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);
 }
 
@@ -366,10 +351,6 @@ 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
@@ -427,19 +408,12 @@ 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, false);
 
-    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,8 +82,6 @@ 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

@@ -1321,64 +1321,6 @@ 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, offset);
-      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.zextOrTrunc(offset.bits())
-                          .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) {
-  auto is_local = p.isLocal();
-  if (is_local.isTrue())
-    return;
-
-  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, offset);
-      has_stored_arg
-        = expr::mkIf(is_local,
-                     has_stored_arg,
-                     has_stored_arg.store(bid.concat(offset + off_expr), true));
-    }
-  } else {
-    expr var     = expr::mkQVar(0, bid.concat(offset));
-    expr var_bid = var.extract(var.bits()-1, offset.bits());
-    expr var_off = var.trunc(offset.bits());
-
-    expr bytes_div = bytes.zextOrTrunc(offset.bits())
-                          .udiv(expr::mkUInt(bytes_per_byte, bytes));
-    has_stored_arg
-      = expr::mkIf(is_local,
-                   has_stored_arg,
-                   expr::mkLambda(var, "#bid_off",
-                     (bid == var_bid &&
-                      var_off.uge(offset) &&
-                      var_off.ult(offset + bytes_div)) ||
-                     has_stored_arg.load(var)));
-  }
-}
-
 static bool memory_unused() {
   return num_locals_src == 0 && num_locals_tgt == 0 && num_nonlocals == 0;
 }
@@ -1532,10 +1474,6 @@ 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);
@@ -2806,8 +2744,6 @@ 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);
@@ -2957,7 +2893,6 @@ 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,9 +154,6 @@ 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;
@@ -227,10 +224,6 @@ 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(const_cast<Memory&>(m)),
+                 const expr &attr) : m(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(const_cast<Memory&>(m)) {
+                 const ParamAttrs &attr) : m(m) {
   unsigned bits = bitsShortBid() + bits_for_offset;
   p = expr::mkVar(var_name, bits, false)
         .zext(hasLocalBit() + (1 + padding_logical()) * hasLogicalBit());
@@ -87,13 +87,12 @@ Pointer::Pointer(const Memory &m, const char *var_name,
   assert(p.bits() == totalBits());
 }
 
-Pointer::Pointer(const Memory &m, expr repr)
-  : m(const_cast<Memory&>(m)), p(std::move(repr)) {
+Pointer::Pointer(const Memory &m, expr repr) : m(m), p(std::move(repr)) {
   assert(!p.isValid() || p.bits() == totalBits());
 }
 
 Pointer::Pointer(const Memory &m, unsigned bid, bool local, expr attr)
-  : m(const_cast<Memory&>(m)), p(
+  : m(m), p(
     prepend_if(expr::mkUInt(0, 1 + padding_logical()),
       prepend_if(expr::mkUInt(local, 1),
                  expr::mkUInt(bid, bitsShortBid())
@@ -531,35 +530,12 @@ 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;
   };
 
@@ -592,7 +568,6 @@ 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 start, unsigned limit, bool local) {
       for (unsigned i = start; i < limit; ++i) {
@@ -602,24 +577,20 @@ 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, addr) : addr - this_addr;
-
         expr cond = p.isInboundsOf(this_ptr, bytes, is_phy) &&
-                    block_constraints(this_ptr + offset);
+                    block_constraints(this_ptr);
         if (cond.isFalse())
           continue;
 
         ub |= cond;
 
         cond = p.isOfBlock(this_ptr, bytes, is_phy);
 
-        all_same_size &= same_size;
+        all_same_size &= bytes.eq(this_ptr.blockSizeAligned());
 
         bids.add(
           observes_local ? this_ptr.getBid() : this_ptr.getShortBid(), cond);
-        addrs.add(std::move(this_addr), std::move(cond));
+        addrs.add(this_ptr.getLogAddress(), std::move(cond));
       }
     };
     add(0, m.numLocals(), true);
@@ -631,6 +602,8 @@ 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
@@ -711,9 +684,6 @@ 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 {
-  Memory &m;
+  const Memory &m;
 
   // [0, padding, bid, offset, attributes (1 bit for each)] -- logical pointer
   // [1, padding, address, attributes] -- physical pointer

llvm_util/llvm2alive.cpp

@@ -19,7 +19,6 @@
 #include "llvm/IR/IntrinsicsX86.h"
 #include "llvm/IR/Operator.h"
 #include "llvm/Support/ModRef.h"
-#include <algorithm>
 #include <sstream>
 #include <unordered_map>
 #include <unordered_set>
@@ -1510,7 +1509,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();
@@ -1634,19 +1633,6 @@ 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

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