simplifications to memcmp smt encoding (e.g. reduce 1 quantified var per iteration)
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -37,7 +37,10 @@ struct print_type {
struct LoopLikeFunctionApproximator {
// input: (i, is the last iter?)
// output: (value, UB, continue?)
- function<tuple<expr, AndExpr, expr>(unsigned, bool)> ith_exec;
+ using fn_t = function<tuple<expr, AndExpr, expr>(unsigned, bool)>;
+ fn_t ith_exec;
+
+ LoopLikeFunctionApproximator(fn_t ith_exec) : ith_exec(move(ith_exec)) {}
pair<expr, expr> encode(IR::State &s, unsigned unroll_cnt) {
AndExpr prefix;
@@ -48,21 +51,21 @@ struct LoopLikeFunctionApproximator {
unsigned unroll_cnt) {
bool is_last = i == unroll_cnt - 1;
auto [res_i, ub_i, continue_i] = ith_exec(i, is_last);
+ auto ub = ub_i();
+ prefix.add(ub_i);
if (is_last) {
- prefix.add(ub_i);
s.addPre(prefix().implies(!continue_i), true);
- return { move(res_i), ub_i() };
+ return { move(res_i), move(ub) };
}
- if (continue_i.isFalse() || ub_i().isFalse())
- return { move(res_i), ub_i() };
+ if (continue_i.isFalse() || ub.isFalse())
+ return { move(res_i), move(ub) };
- prefix.add(ub_i);
prefix.add(continue_i);
auto [val_next, ub_next] = _loop(s, prefix, i + 1, unroll_cnt);
return { expr::mkIf(continue_i, move(val_next), move(res_i)),
- ub_i() && continue_i.implies(ub_next) };
+ ub && continue_i.implies(ub_next) };
}
};
}
@@ -2435,6 +2438,22 @@ unique_ptr<Instr> Memcpy::dup(const string &suffix) const {
}
+
+vector<Value*> Memcmp::operands() const {
+ return { ptr1, ptr2, num };
+}
+
+void Memcmp::rauw(const Value &what, Value &with) {
+ RAUW(ptr1);
+ RAUW(ptr2);
+ RAUW(num);
+}
+
+void Memcmp::print(ostream &os) const {
+ os << getName() << " = " << (is_bcmp ? "bcmp " : "memcmp ") << *ptr1
+ << ", " << *ptr2 << ", " << *num;
+}
+
StateValue Memcmp::toSMT(State &s) const {
auto &[vptr1, np1] = s[*ptr1];
auto &[vptr2, np2] = s[*ptr2];
@@ -2442,54 +2461,47 @@ StateValue Memcmp::toSMT(State &s) const {
s.addUB(vnum.ugt(0).implies(np1 && np2));
s.addUB(npn);
- AndExpr prefix;
Pointer p1(s.getMemory(), vptr1), p2(s.getMemory(), vptr2);
// memcmp can be optimized to load & icmps, and it requires this
// dereferenceability check of vnum.
s.addUB(p1.isDereferenceable(vnum, 1, false));
s.addUB(p2.isDereferenceable(vnum, 1, false));
- expr vn = vnum;
+ expr zero = expr::mkUInt(0, 32);
+ auto &vn = vnum;
+
auto ith_exec =
[&, this](unsigned i, bool is_last) -> tuple<expr, AndExpr, expr> {
- AndExpr ub_and;
auto [val1, ub1] = s.getMemory().load((p1 + i)(), IntType("i8", 8), 1);
auto [val2, ub2] = s.getMemory().load((p2 + i)(), IntType("i8", 8), 1);
- ub_and.add(val1.non_poison);
- ub_and.add(val2.non_poison);
+ AndExpr ub_and;
+ ub_and.add(move(val1.non_poison));
+ ub_and.add(move(val2.non_poison));
ub_and.add(move(ub1));
ub_and.add(move(ub2));
- expr ei = expr::mkUInt(i, vn.bits());
- auto val_eq = val1.value == val2.value;
- expr continue_cond = val_eq && ei.ult(vn);
- if (is_last)
- continue_cond &= (p1 != p2);
-
- expr zero = expr::mkUInt(0, 32);
expr result_neq;
if (is_bcmp) {
result_neq = expr::mkFreshVar("bcmp_nonzero", zero);
s.addQuantVar(result_neq);
s.addPre(result_neq != zero);
} else {
- expr pos = expr::mkFreshVar("memcmp_pos", expr::mkUInt(0, 31));
- expr neg = expr::mkFreshVar("memcmp_neg", expr::mkUInt(0, 31));
- s.addQuantVar(pos);
- s.addQuantVar(neg);
- s.addPre(pos != expr::mkUInt(0u, 31));
- pos = expr::mkUInt(0, 1).concat(pos);
- neg = expr::mkUInt(1, 1).concat(neg);
- result_neq = expr::mkIf(val1.value.ugt(val2.value), move(pos), move(neg));
- }
- auto result = expr::mkIf(val_eq, zero, result_neq);
-
- return { move(result), move(ub_and), move(continue_cond) };
+ expr var = expr::mkFreshVar("memcmp", expr::mkUInt(0, 31));
+ s.addQuantVar(var);
+ auto pos = val1.value.uge(val2.value);
+ s.addPre(pos.implies(var != 0));
+ result_neq = expr::mkIf(pos, expr::mkUInt(0, 1), expr::mkUInt(1, 1))
+ .concat(var);
+ }
+
+ auto val_eq = val1.value == val2.value;
+ return { expr::mkIf(val_eq, zero, result_neq),
+ move(ub_and),
+ val_eq && expr::mkUInt(i, vn.bits()).ult(vn) };
};
- LoopLikeFunctionApproximator apprx;
- apprx.ith_exec = ith_exec;
- auto [val, ub] = apprx.encode(s, memcmp_unroll_cnt);
+ auto [val, ub]
+ = LoopLikeFunctionApproximator(ith_exec).encode(s, memcmp_unroll_cnt);
s.addUB(move(ub));
return { move(val), true };
}
@@ -2505,21 +2517,6 @@ unique_ptr<Instr> Memcmp::dup(const string &suffix) const {
is_bcmp);
}
-vector<Value*> Memcmp::operands() const {
- return { ptr1, ptr2, num };
-}
-
-void Memcmp::rauw(const Value &what, Value &with) {
- RAUW(ptr1);
- RAUW(ptr2);
- RAUW(num);
-}
-
-void Memcmp::print(ostream &os) const {
- os << getName() << " = " << (is_bcmp ? "bcmp " : "memcmp ") << *ptr1
- << ", " << *ptr2 << ", " << *num;
-}
-
vector<Value*> Strlen::operands() const {
return { ptr };
@@ -2537,7 +2534,6 @@ StateValue Strlen::toSMT(State &s) const {
auto &[eptr, np_ptr] = s[*ptr];
s.addUB(np_ptr);
- LoopLikeFunctionApproximator apprx;
Pointer p(s.getMemory(), eptr);
Type &ty = getType();
@@ -2545,14 +2541,12 @@ StateValue Strlen::toSMT(State &s) const {
[&s, &p, &ty](unsigned i, bool _) -> tuple<expr, AndExpr, expr> {
AndExpr ub;
auto [val, ub_load] = s.getMemory().load((p + i)(), IntType("i8", 8), 1);
- ub.add(ub_load);
- ub.add(val.non_poison);
- auto nonnull = val.value != 0;
- auto result = expr::mkUInt(i, ty.bits());
- return { move(result), move(ub), move(nonnull) };
+ ub.add(move(ub_load));
+ ub.add(move(val.non_poison));
+ return { expr::mkUInt(i, ty.bits()), move(ub), val.value != 0 };
};
- apprx.ith_exec = ith_exec;
- auto [val, ub] = apprx.encode(s, strlen_unroll_cnt);
+ auto [val, ub]
+ = LoopLikeFunctionApproximator(ith_exec).encode(s, strlen_unroll_cnt);
s.addUB(move(ub));
return { move(val), true };
}

MODIFY
ir/instr.h
ir/instr.h
@@ -590,13 +590,15 @@ public:
};
-class Strlen final : public Instr {
- Value *ptr;
+class Memcmp final : public Instr {
+ Value *ptr1, *ptr2, *num;
+ bool is_bcmp;
public:
- Strlen(Type &type, std::string &&name, Value &ptr)
- : Instr(type, std::move(name)), ptr(&ptr) {}
+ Memcmp(Type &type, std::string &&name, Value &ptr1, Value &ptr2, Value &num,
+ bool is_bcmp): Instr(type, std::move(name)), ptr1(&ptr1), ptr2(&ptr2),
+ num(&num), is_bcmp(is_bcmp) {}
- Value *getPointer() const { return ptr; }
+ Value &getBytes() const { return *num; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;
@@ -606,15 +608,13 @@ public:
};
-class Memcmp final : public Instr {
- Value *ptr1, *ptr2, *num;
- bool is_bcmp;
+class Strlen final : public Instr {
+ Value *ptr;
public:
- Memcmp(Type &type, std::string &&name, Value &ptr1, Value &ptr2, Value &num,
- bool is_bcmp): Instr(type, std::move(name)), ptr1(&ptr1), ptr2(&ptr2),
- num(&num), is_bcmp(is_bcmp) {}
+ Strlen(Type &type, std::string &&name, Value &ptr)
+ : Instr(type, std::move(name)), ptr(&ptr) {}
- Value &getBytes() const { return *num; }
+ Value *getPointer() const { return ptr; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;

MODIFY
tests/alive-tv/memory/punning-ptrint.src.ll
tests/alive-tv/memory/punning-ptrint.src.ll
-; TEST-ARGS: -disable-poison-input
+; TEST-ARGS: -smt-to=10000
define i8 @ptr_int_punning(i8** %pptr, i64 %n) {
%ptr = alloca i8

simplifications to memcmp smt encoding (e.g. reduce 1 quantified var per iteration)