fix refinement queries to ignore corner case when Pre(I, N) is
false for a fixed I and any N
no change in perf mostly
test cases by Juneyoung Lee
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -62,7 +62,7 @@ struct LoopLikeFunctionApproximator {
prefix.add(ub_i);
if (is_last) {
- s.addPre(prefix().implies(!continue_i), true);
+ s.addPre(prefix().implies(!continue_i));
return { move(res_i), move(np_i), move(ub) };
}

MODIFY
ir/state.h
ir/state.h
@@ -52,7 +52,7 @@ private:
bool source;
bool disable_undef_rewrite = false;
bool is_initialization_phase = true;
- smt::AndExpr precondition, preconditionForApprox;
+ smt::AndExpr precondition;
smt::AndExpr axioms;
smt::AndExpr ooms;
@@ -132,8 +132,7 @@ public:
void addAxiom(smt::AndExpr &&ands) { axioms.add(std::move(ands)); }
void addAxiom(smt::expr &&axiom) { axioms.add(std::move(axiom)); }
- void addPre(smt::expr &&cond, bool forApprox = false)
- { (forApprox ? preconditionForApprox : precondition).add(std::move(cond)); }
+ void addPre(smt::expr &&cond) { precondition.add(std::move(cond)); }
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
void addUB(smt::AndExpr &&ubs);
@@ -159,9 +158,7 @@ public:
auto& getFn() const { return f; }
auto& getMemory() { return memory; }
auto& getAxioms() const { return axioms; }
- auto& getPre(bool forApprox = false) const
- { return forApprox ? preconditionForApprox : precondition; }
- auto& getPreForApprox() const { return preconditionForApprox; }
+ auto& getPre() const { return precondition; }
auto& getOOM() const { return ooms; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1650,6 +1650,9 @@ expr expr::simplify() const {
expr expr::subst(const vector<pair<expr, expr>> &repls) const {
C();
+ if (repls.empty())
+ return *this;
+
unique_ptr<Z3_ast[]> from(new Z3_ast[repls.size()]);
unique_ptr<Z3_ast[]> to(new Z3_ast[repls.size()]);

ADD
tests/alive-tv/memory/alloca-array.srctgt.ll
+declare void @free(i8*)
+
+define void @src(i32 %x) {
+ %conv = sext i32 %x to i64
+ %mul = mul nsw i64 %conv, 4
+ %xx = alloca i8, i64 %mul, align 16
+ %y= bitcast i8* %xx to float*
+ store float 0.0, float* %y
+ ret void
+}
+
+define void @tgt(i32 %x) {
+ %conv = sext i32 %x to i64
+ %y = alloca float, i64 %conv, align 16
+ store float 0.0, float* %y
+ ret void
+}

ADD
tests/alive-tv/memory/calloc-overflow-3.srctgt.ll
+define i8 @src(i8*) {
+ %ptr = call i8* @calloc(i64 555555555555555, i64 40000000)
+ call void @free(i8* null)
+ ret i8 1
+}
+
+define i8 @tgt(i8*) {
+ ret i8 1
+}
+
+declare void @free(i8*)
+declare i8* @calloc(i64, i64)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -208,7 +208,6 @@ static expr preprocess(Transform &t, const set<expr> &qvars0,
qvars.erase(var);
}
- // TODO: maybe try to instantiate undet_xx vars?
if (undef_qvars.empty() || hit_half_memory_limit())
return expr::mkForAll(qvars, move(e));
@@ -256,9 +255,6 @@ static expr preprocess(Transform &t, const set<expr> &qvars0,
for (auto &[e, v] : instances) {
insts |= expr::mkForAll(qvars, move(const_cast<expr&>(e))) && v;
}
-
- // TODO: try out instantiating the undefs in forall quantifier
-
return insts;
}
@@ -308,8 +304,22 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
pre_tgt &= src_state.getOOM()();
pre_tgt &= !tgt_state.sinkDomain();
- pre_tgt &= src_state.getPre(true)();
- pre_tgt &= tgt_state.getPre(true)();
+
+ expr pre_src_exists = pre_src, pre_src_forall = true;
+ {
+ vector<pair<expr,expr>> repls;
+ auto vars_pre = pre_src.vars();
+ for (auto &v : qvars) {
+ if (vars_pre.count(v))
+ repls.emplace_back(v, expr::mkFreshVar("#exists", v));
+ }
+ auto new_pre = pre_src.subst(repls);
+ if (!new_pre.eq(pre_src)) {
+ pre_src_exists = move(new_pre);
+ pre_src_forall = pre_src;
+ }
+ }
+ expr pre = pre_src_exists && pre_tgt;
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
@@ -337,8 +347,8 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
if (refines.isFalse())
return move(refines);
- auto fml = pre_tgt && pre_src.implies(refines);
- return axioms_expr && preprocess(t, qvars, uvars, move(fml));
+ return axioms_expr &&
+ preprocess(t, qvars, uvars, pre && pre_src_forall.implies(refines));
};
auto print_ptr_load = [&](ostream &s, const Model &m) {

fix refinement queries to ignore corner case when Pre(I, N) is
false for a fixed I and any N
no change in perf mostly
test cases by Juneyoung Lee