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

Author: nunoplopes

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(

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,

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);

ir/pointer.h

@@ -113,8 +113,6 @@ class Pointer {
   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;

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) {

ir/state.h

@@ -94,8 +94,7 @@ class State {
   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 @@ class State {
   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 @@ class State {
 
   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);

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,20 +134,39 @@ 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()) {
-    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 &src_approx = src_state.getApproximations();
+    auto &tgt_approx = tgt_state.getApproximations();
     auto approx = src_approx;
     approx.insert(tgt_approx.begin(), tgt_approx.end());
-    for (auto &a : approx) {
-      s << " - " << a << '\n';
+
+    // 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";
+      for (auto &[msg, var] : approx) {
+        s << " - " << msg << '\n';
+      }
+      errs.add(s.str(), false);
+      return;
     }
-    errs.add(s.str(), false);
-    return;
   }
 
   s << msg;
@@ -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;