memory: fix bug with encoding of nonnull parameters that may be undef
MODIFY
ir/memory.cpp
ir/memory.cpp
#include "ir/memory.h"
#include "ir/globals.h"
#include "ir/state.h"
+#include "ir/value.h"
#include "util/compiler.h"
using namespace IR;
@@ -660,7 +661,8 @@ expr Pointer::block_refined(const Pointer &other) const {
blk_size == other.block_size() &&
get_alloc_type() == other.get_alloc_type() &&
is_writable() == other.is_writable() &&
- block_alignment().ule(other.block_alignment()) &&
+ m.state->simplifyWithAxioms(
+ block_alignment().ule(other.block_alignment())) &&
(is_block_alive() && get_offset().ult(blk_size)).implies(val_refines);
}
@@ -900,19 +902,36 @@ void Memory::resetLocalBids() {
ptr_next_idx = 0;
}
-expr Memory::mkInput(const char *name) const {
+expr Memory::mkInput(const char *name, unsigned attributes) const {
Pointer p(*this,
prepend_if(expr::mkUInt(0, 1),
expr::mkVar(name, bits_shortbid() + bits_for_offset),
ptr_has_local_bit()));
state->addAxiom(p.get_short_bid().ule(num_nonlocals - 1));
+
+ if (attributes & Input::NonNull)
+ state->addAxiom(p.isNonZero());
+
return p.release();
}
-pair<expr, expr> Memory::mkUndefInput() const {
- expr offset = expr::mkFreshVar("undef", expr::mkUInt(0, bits_for_offset));
+pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
+ bool nonnull = attributes & Input::NonNull;
+ unsigned log_offset = ilog2_ceil(bits_for_offset);
+ unsigned bits_undef = bits_for_offset + nonnull * log_offset;
+ expr undef = expr::mkFreshVar("undef", expr::mkUInt(0, bits_undef));
+ expr offset = undef;
+
+ if (nonnull) {
+ expr var = undef.extract(log_offset - 1, 0);
+ expr one = expr::mkUInt(1, bits_for_offset);
+ expr shl = expr::mkIf(var.ugt(bits_for_offset-1),
+ one,
+ one << var.zextOrTrunc(bits_for_offset));
+ offset = undef.extract(bits_undef - 1, log_offset) | shl;
+ }
Pointer p(*this, expr::mkUInt(0, bits_for_bid), offset);
- return { p.release(), move(offset) };
+ return { p.release(), move(undef) };
}
expr Memory::mkFnRet(const char *name) const {
@@ -1232,8 +1251,7 @@ pair<expr,Pointer> Memory::refined(const Memory &other) const {
Pointer q(other, p());
ret &= (ptr_bid == bid_expr).implies(p.block_refined(q));
}
- return { (ptr_bid != 0 && ptr_bid.ule(num_nonlocals - 1)).implies(ret),
- move(ptr) };
+ return { move(ret), move(ptr) };
}
Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {

MODIFY
ir/memory.h
ir/memory.h
@@ -197,8 +197,8 @@ public:
static void resetGlobalData();
static void resetLocalBids();
- smt::expr mkInput(const char *name) const;
- std::pair<smt::expr, smt::expr> mkUndefInput() const;
+ smt::expr mkInput(const char *name, unsigned attributes) const;
+ std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
smt::expr mkFnRet(const char *name) const;
// Allocates a new memory block and returns (pointer expr, allocated).

MODIFY
ir/state.cpp
ir/state.cpp
@@ -355,4 +355,8 @@ void State::mkAxioms(State &tgt) {
}
}
+expr State::simplifyWithAxioms(smt::expr &&e) const {
+ return axioms.contains(e) ? expr(true) : move(e);
+}
+
}

MODIFY
ir/state.h
ir/state.h
@@ -144,6 +144,7 @@ public:
void syncSEdataWithSrc(const State &src);
void mkAxioms(State &tgt);
+ smt::expr simplifyWithAxioms(smt::expr &&e) const;
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);

MODIFY
ir/type.cpp
ir/type.cpp
@@ -245,8 +245,8 @@ expr Type::combine_poison(const expr &boolean, const expr &orig) const {
return expr::mkIf(boolean, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) | orig;
}
-pair<expr, vector<expr>> Type::mkUndefInput(State &s) const {
- auto var = expr::mkFreshVar("undef", mkInput(s, ""));
+pair<expr, vector<expr>> Type::mkUndefInput(State &s, unsigned attrs) const {
+ auto var = expr::mkFreshVar("undef", mkInput(s, "", attrs));
return { var, { var } };
}
@@ -286,7 +286,7 @@ VoidType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { true, true };
}
-expr VoidType::mkInput(State &s, const char *name) const {
+expr VoidType::mkInput(State &s, const char *name, unsigned attributes) const {
UNREACHABLE();
}
@@ -344,7 +344,7 @@ IntType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
-expr IntType::mkInput(State &s, const char *name) const {
+expr IntType::mkInput(State &s, const char *name, unsigned attributes) const {
return expr::mkVar(name, bits());
}
@@ -485,7 +485,7 @@ FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
-expr FloatType::mkInput(State &s, const char *name) const {
+expr FloatType::mkInput(State &s, const char *name, unsigned attrs) const {
switch (fpType) {
case Half: return expr::mkHalfVar(name);
case Float: return expr::mkFloatVar(name);
@@ -597,12 +597,12 @@ PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(p.refined(q)) };
}
-expr PtrType::mkInput(State &s, const char *name) const {
- return s.getMemory().mkInput(name);
+expr PtrType::mkInput(State &s, const char *name, unsigned attrs) const {
+ return s.getMemory().mkInput(name, attrs);
}
-pair<expr, vector<expr>> PtrType::mkUndefInput(State &s) const {
- auto [val, var] = s.getMemory().mkUndefInput();
+pair<expr, vector<expr>> PtrType::mkUndefInput(State &s, unsigned attrs) const {
+ auto [val, var] = s.getMemory().mkUndefInput(attrs);
return { move(val), { move(var) } };
}
@@ -811,23 +811,24 @@ AggregateType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { expr::mk_and(poison), expr::mk_and(value) };
}
-expr AggregateType::mkInput(State &s, const char *name) const {
+expr AggregateType::mkInput(State &s, const char *name, unsigned attrs) const {
expr val;
for (unsigned i = 0; i < elements; ++i) {
string c_name = string(name) + "#" + to_string(i);
- auto v = children[i]->mkInput(s, c_name.c_str());
+ auto v = children[i]->mkInput(s, c_name.c_str(), attrs);
v = children[i]->toBV(move(v));
val = i == 0 ? move(v) : val.concat(v);
}
return val;
}
-pair<expr, vector<expr>> AggregateType::mkUndefInput(State &s) const {
+pair<expr, vector<expr>>
+AggregateType::mkUndefInput(State &s, unsigned attrs) const {
expr val;
vector<expr> vars;
for (unsigned i = 0; i < elements; ++i) {
- auto [v, vs] = children[i]->mkUndefInput(s);
+ auto [v, vs] = children[i]->mkUndefInput(s, attrs);
v = children[i]->toBV(move(v));
val = i == 0 ? move(v) : val.concat(v);
vars.insert(vars.end(), vs.begin(), vs.end());
@@ -1244,12 +1245,13 @@ SymbolicType::refines(State &src_s, State &tgt_s, const StateValue &src,
DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
-expr SymbolicType::mkInput(State &st, const char *name) const {
- DISPATCH(mkInput(st, name), UNREACHABLE());
+expr SymbolicType::mkInput(State &st, const char *name, unsigned attrs) const {
+ DISPATCH(mkInput(st, name, attrs), UNREACHABLE());
}
-pair<expr, vector<expr>> SymbolicType::mkUndefInput(State &st) const {
- DISPATCH(mkUndefInput(st), UNREACHABLE());
+pair<expr, vector<expr>>
+SymbolicType::mkUndefInput(State &st, unsigned attrs) const {
+ DISPATCH(mkUndefInput(st, attrs), UNREACHABLE());
}
void SymbolicType::printVal(ostream &os, State &st, const expr &e) const {

MODIFY
ir/type.h
ir/type.h
@@ -107,9 +107,10 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const = 0;
- virtual smt::expr mkInput(State &s, const char *name) const = 0;
+ virtual smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const = 0;
virtual std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s) const;
+ mkUndefInput(State &s, unsigned attributes) const;
virtual void printVal(std::ostream &os, State &s,
const smt::expr &e) const = 0;
@@ -134,7 +135,8 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -160,7 +162,8 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -200,7 +203,8 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -230,9 +234,10 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s) const override;
+ mkUndefInput(State &s, unsigned attributes) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -279,9 +284,10 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s) const override;
+ mkUndefInput(State &s, unsigned attributes) const override;
unsigned numPointerElements() const;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
const AggregateType* getAsAggregateType() const override;
@@ -384,9 +390,10 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- smt::expr mkInput(State &s, const char *name) const override;
+ smt::expr
+ mkInput(State &s, const char *name, unsigned attributes) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s) const override;
+ mkUndefInput(State &s, unsigned attributes) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -174,19 +174,16 @@ StateValue Input::toSMT(State &s) const {
// 00: normal, 01: undef, else: poison
expr type = getTyVar();
- auto val = getType().mkInput(s, smt_name.c_str());
+ auto val = getType().mkInput(s, smt_name.c_str(), attributes);
if (!config::disable_undef_input) {
- auto [undef, vars] = getType().mkUndefInput(s);
+ auto [undef, vars] = getType().mkUndefInput(s, attributes);
for (auto &v : vars) {
s.addUndefVar(move(v));
}
val = expr::mkIf(type.extract(0, 0) == 0, val, undef);
}
- if (attributes & NonNull)
- s.addPre(Pointer(s.getMemory(), val).isNonZero());
-
expr poison = getType().getDummyValue(false).non_poison;
expr non_poison = getType().getDummyValue(true).non_poison;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1081,15 +1081,11 @@ expr expr::notImplies(const expr &rhs) const {
}
expr expr::ule(const expr &rhs) const {
- if (eq(rhs) || isZero())
+ if (eq(rhs) || isZero() || rhs.isAllOnes())
return true;
-
- if (rhs.isZero())
+ if (rhs.isZero() || isAllOnes())
return *this == rhs;
- if (rhs.isAllOnes())
- return true;
-
return binop_fold(rhs, Z3_mk_bvule);
}

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -23,6 +23,10 @@ void AndExpr::del(const AndExpr &other) {
exprs.erase(e);
}
+bool AndExpr::contains(const expr &e) const {
+ return exprs.count(e);
+}
+
expr AndExpr::operator()() const {
return expr::mk_and(exprs);
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -18,6 +18,7 @@ public:
void add(expr &&e);
void add(const AndExpr &other);
void del(const AndExpr &other);
+ bool contains(const expr &e) const;
expr operator()() const;
friend std::ostream &operator<<(std::ostream &os, const AndExpr &e);
};

ADD
tests/alive-tv/attrs/nonnull.src.ll
+define i1 @f1(i8* nonnull %p) {
+ %a = ptrtoint i8* %p to i64
+ %b = ptrtoint i8* %p to i64
+ %c = icmp eq i64 %b, 0
+ ret i1 %c
+}
+
+define i1 @f2(i8* nonnull %p) {
+ ret i1 0
+}

ADD
tests/alive-tv/attrs/nonnull.tgt.ll
+define i1 @f1(i8* nonnull %p) {
+ ret i1 0
+}
+
+define i1 @f2(i8* nonnull %p) {
+ ret i1 0
+}

MODIFY
tests/alive-tv/memory/memset-fn.tgt.ll
tests/alive-tv/memory/memset-fn.tgt.ll
@@ -7,6 +7,4 @@ define i32* @f(i32* %ptr, i32 %val, i64 %len) {
ret i32* %ptr
}
-declare void @llvm.memset.p0i8.i64(i8* nocapture writeonly, i8, i64, i1 immarg) #0
-
-attributes #0 = { argmemonly nounwind willreturn }
+declare void @llvm.memset.p0i8.i64(i8*, i8, i64, i1)

MODIFY
tests/alive-tv/memory/memset-large.src.ll
tests/alive-tv/memory/memset-large.src.ll
-; TEST-ARGS: -smt-to=10000
+; TEST-ARGS: -smt-to=10000 -disable-undef-input
+
declare void @llvm.memset.p0i8.i128(i8*, i8, i128, i1)
define void @f(i8* %p, i128 %n) {

MODIFY
tests/alive-tv/memory/zeroinit-memset.tgt.ll
tests/alive-tv/memory/zeroinit-memset.tgt.ll
@@ -9,4 +9,4 @@ define void @destroysrc(%S* %src, %S* %dst) {
ret void
}
-declare void @llvm.memset.p0i8.i64(i8* nocapture writeonly, i8, i64, i1 immarg)
+declare void @llvm.memset.p0i8.i64(i8*, i8, i64, i1)

memory: fix bug with encoding of nonnull parameters that may be undef