diff --git a/ir/attrs.cpp b/ir/attrs.cpp index 857394522..307cc680e 100644 --- a/ir/attrs.cpp +++ b/ir/attrs.cpp @@ -10,6 +10,7 @@ #include "ir/state_value.h" #include "ir/type.h" #include "util/compiler.h" +#include #include 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; diff --git a/ir/attrs.h b/ir/attrs.h index 2544f90df..dbb56826b 100644 --- a/ir/attrs.h +++ b/ir/attrs.h @@ -82,6 +82,8 @@ class ParamAttrs final { uint64_t align = 1; uint16_t nofpclass = 0; + std::vector> initializes; + bool has(Attribute a) const { return (bits & a) != 0; } void set(Attribute a) { bits |= (unsigned)a; } bool refinedBy(const ParamAttrs &other) const; diff --git a/ir/memory.cpp b/ir/memory.cpp index 4b880ca1b..ecae886f9 100644 --- a/ir/memory.cpp +++ b/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) { diff --git a/ir/memory.h b/ir/memory.h index 5f27ed31c..d48c26bae 100644 --- a/ir/memory.h +++ b/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> &data, const std::set &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 &undef) const; diff --git a/ir/pointer.cpp b/ir/pointer.cpp index c95850823..0290c5696 100644 --- a/ir/pointer.cpp +++ b/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(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(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(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(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(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 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,8 +594,13 @@ 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; @@ -578,11 +608,11 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align, 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)() }; } diff --git a/ir/pointer.h b/ir/pointer.h index 97105c0e5..e32d3e6a4 100644 --- a/ir/pointer.h +++ b/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 diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 7d619a456..ec9ebe6f0 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -17,6 +17,7 @@ #include "llvm/IR/Instructions.h" #include "llvm/IR/Operator.h" #include "llvm/Support/ModRef.h" +#include #include #include #include @@ -1466,7 +1467,7 @@ class llvm2alive_ : public llvm::InstVisitor> { unique_ptr handleRangeAttrNoInsert(const llvm::Attribute &attr, Value &val, bool is_welldefined = false) { - auto CR = attr.getValueAsConstantRange(); + auto &CR = attr.getValueAsConstantRange(); vector 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> { 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) diff --git a/smt/expr.cpp b/smt/expr.cpp index e4a3aa4c3..755dc64a9 100644 --- a/smt/expr.cpp +++ b/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);