over-approximate more features instead of returning invalid exprs
this also introduces a mode that checks which approaximations (if any) contribute to the bug report
if none, it's a real bug
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -320,20 +320,16 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b,
non_poison &= !val.isInf();
}
if (fmath.flags & FastMathFlags::ARCP) {
- s.useUnsupported("arcp");
- non_poison &= expr(); // TODO
+ s.doesApproximation("arcp", val);
}
if (fmath.flags & FastMathFlags::Contract) {
- s.useUnsupported("contract");
- non_poison &= expr(); // TODO
+ s.doesApproximation("contract", val);
}
if (fmath.flags & FastMathFlags::Reassoc) {
- s.useUnsupported("reassoc");
- non_poison &= expr(); // TODO
+ s.doesApproximation("reassoc", val);
}
if (fmath.flags & FastMathFlags::AFN) {
- s.useUnsupported("afn");
- non_poison &= expr(); // TODO
+ s.doesApproximation("afn", val);
}
if (fmath.flags & FastMathFlags::NSZ && !only_input)
val = any_fp_zero(s, move(val));
@@ -606,8 +602,12 @@ StateValue BinOp::toSMT(State &s) const {
case FRem:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
- s.useUnsupported("frem");
- return fm_poison(s, a, ap, b, bp, [](expr &a, expr &b) { return expr(); },
+ return fm_poison(s, a, ap, b, bp,
+ [&](expr &a, expr &b) {
+ auto val = expr::mkUF("fmod", {a, b}, a);
+ s.doesApproximation("frem", val);
+ return val;
+ },
fmath, false);
};
break;
@@ -1285,8 +1285,9 @@ StateValue ConversionOp::toSMT(State &s) const {
break;
case Int2Ptr:
fn = [&](auto &&val, auto &to_type) -> StateValue {
- s.useUnsupported("inttoptr");
- return { s.getMemory().int2ptr(val), true };
+ auto ret = s.getMemory().int2ptr(val);
+ s.doesApproximation("inttoptr", ret);
+ return { move(ret), true };
};
break;
}
@@ -1689,7 +1690,6 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
if (ty.isPtrType()) {
expr np(true);
Pointer p(s.getMemory(), move(value.value));
- p.stripAttrs();
if (argflag.has(ParamAttrs::Dereferenceable) ||
argflag.has(ParamAttrs::ByVal))
s.addUB(

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1619,7 +1619,8 @@ expr Memory::ptr2int(const expr &ptr) const {
expr Memory::int2ptr(const expr &val) const {
assert(!memory_unused());
// TODO
- return {};
+ expr null = Pointer::mkNullPointer(*this).release();
+ return expr::mkIf(val == 0, null, expr::mkUF("int2ptr", { val }, null));
}
expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -517,11 +517,6 @@ expr Pointer::isReadnone() const {
return p.extract(idx, idx) == 1;
}
-void Pointer::stripAttrs() {
- p = p.extract(totalBits()-1, bits_for_ptrattrs)
- .concat_zeros(bits_for_ptrattrs);
-}
-
Pointer Pointer::mkNullPointer(const Memory &m) {
// Null pointer exists if either source or target uses it.
assert(has_null_block);

MODIFY
ir/pointer.h
ir/pointer.h
@@ -113,8 +113,6 @@ public:
smt::expr isReadonly() const;
smt::expr isReadnone() const;
- void stripAttrs();
-
smt::expr refined(const Pointer &other) const;
smt::expr fninputRefined(const Pointer &other, std::set<smt::expr> &undef,
bool is_byval_arg) const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -334,8 +334,7 @@ expr State::strip_undef_and_add_ub(const Value &val, const expr &e) {
StateValue* State::no_more_tmp_slots() {
if (i_tmp_values < tmp_values.size())
return nullptr;
- useUnsupported("Too many temporaries");
- return &null_sv;
+ throw AliveException("Too many temporaries", false);
}
const StateValue& State::operator[](const Value &val) {
@@ -838,12 +837,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return retval;
}
-void State::useUnsupported(const char *name) {
- used_unsupported.emplace(name);
-}
-
-void State::doesApproximation(string &&name) {
- used_approximations.emplace(move(name));
+void State::doesApproximation(string &&name, optional<expr> e) {
+ used_approximations.emplace(move(name), move(e));
}
void State::addQuantVar(const expr &var) {

MODIFY
ir/state.h
ir/state.h
@@ -94,8 +94,7 @@ private:
smt::AndExpr precondition;
smt::AndExpr axioms;
- std::set<const char*> used_unsupported;
- std::set<std::string> used_approximations;
+ std::set<std::pair<std::string,std::optional<smt::expr>>> used_approximations;
std::set<smt::expr> quantified_vars;
@@ -119,7 +118,6 @@ private:
std::set<smt::expr> undef_vars;
ValueAnalysis analysis;
std::array<StateValue, 64> tmp_values;
- StateValue null_sv;
unsigned i_tmp_values = 0; // next available position in tmp_values
StateValue* no_more_tmp_slots();
@@ -206,10 +204,7 @@ public:
auto& getVarArgsData() { return var_args_data.data; }
- void useUnsupported(const char *name);
- auto& getUnsupported() const { return used_unsupported; }
-
- void doesApproximation(std::string &&name);
+ void doesApproximation(std::string &&name, std::optional<smt::expr> e = {});
auto& getApproximations() const { return used_approximations; }
void addQuantVar(const smt::expr &var);

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -111,20 +111,6 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
if (r.isInvalid()) {
errs.add("Invalid expr", false);
- auto unsupported = src_state.getUnsupported();
- auto &u_tgt = tgt_state.getUnsupported();
- unsupported.insert(u_tgt.begin(), u_tgt.end());
- if (!unsupported.empty()) {
- string str = "The program uses the following unsupported features: ";
- bool first = true;
- for (auto name : unsupported) {
- if (!first)
- str += ", ";
- str += name;
- first = false;
- }
- errs.add(move(str), false);
- }
return;
}
@@ -148,21 +134,40 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
auto &var_name = var ? var->getName() : empty;
auto &m = r.getModel();
+ {
auto &src_approx = src_state.getApproximations();
auto &tgt_approx = tgt_state.getApproximations();
- if (!src_approx.empty() || !tgt_approx.empty()) {
+ auto approx = src_approx;
+ approx.insert(tgt_approx.begin(), tgt_approx.end());
+
+ // filter out approximations that don't contribute to the bug
+ // i.e., they don't show up in the SMT model
+ for (auto I = approx.begin(); I != approx.end(); ) {
+ if (!I->second) {
+ ++I;
+ continue;
+ }
+
+ auto &var = *I->second;
+ if (m.eval(var).isConst()) {
+ ++I;
+ } else {
+ I = approx.erase(I);
+ }
+ }
+
+ if (!approx.empty()) {
s << "Couldn't prove the correctness of the transformation\n"
"Alive2 approximated the semantics of the programs and therefore we\n"
"cannot conclude whether the bug found is valid or not.\n\n"
"Approximations done:\n";
- auto approx = src_approx;
- approx.insert(tgt_approx.begin(), tgt_approx.end());
- for (auto &a : approx) {
- s << " - " << a << '\n';
+ for (auto &[msg, var] : approx) {
+ s << " - " << msg << '\n';
}
errs.add(s.str(), false);
return;
}
+ }
s << msg;
if (!var_name.empty())
@@ -841,7 +846,7 @@ static void calculateAndInitConstants(Transform &t) {
// check if null block is needed
// Global variables cannot be null pointers
has_null_block = num_ptrinputs > 0 || nullptr_is_used || has_malloc ||
- has_ptr_load || has_fncall;
+ has_ptr_load || has_fncall || has_int2ptr;
num_nonlocals_src = num_globals_src + num_ptrinputs + num_nonlocals_inst_src +
has_null_block;

over-approximate more features instead of returning invalid exprs
this also introduces a mode that checks which approaximations (if any) contribute to the bug report
if none, it's a real bug