equality_sustitution

benchmarks/llvm/equality.c

@@ -0,0 +1,16 @@
+#include "../../headers/gensym_client.h"
+#include <stdio.h>
+
+int main() {
+  char x[10];
+  make_symbolic(x, 10);
+
+  gs_assume(0 == x[0]);
+  if (x[0] == 2) {
+    print_string("should be here!\n");
+  } else {
+    print_string("oops!\n");
+  }
+
+  return 0;
+}

headers/gensym/cli.hpp

@@ -20,6 +20,7 @@ static struct option long_options[] =
   {"no-br-cache",                no_argument,       0, 27},
   {"no-cons-indep",              no_argument,       0, 5},
   {"simplify",                   no_argument,       0, 26},
+  {"equality-substitution",      no_argument,       0, 28},
   // Test case generation
   {"output-tests-cov-new",       no_argument,       0, 6},
   {"output-ktest",               no_argument,       0, 7},
@@ -226,6 +227,9 @@ inline void handle_cli_args(int argc, char** argv) {
       case 27:
         use_brcache = false;
         break;
+      case 28:
+        use_equality_substitution = true;
+        break;
       case '?':
       default:
         print_help(argv[0]);
@@ -278,11 +282,11 @@ inline void handle_cli_args(int argc, char** argv) {
     initial_fs.sym_objs = initial_fs.sym_objs.push_back(SymObj("stdout-stat", stat_size, false));
   }
   if (output_ktest && (cli_argv.size() > 0)) {
-    const int extra_args = 3 + 3; 
+    const int extra_args = 3 + 3;
     // + 3 for -sym-files n m, + 3 for -sym-stdout, -sym-stdin n
     // each symarg also requires an additional slot
 
-    g_conc_argc = cli_argv.size() + extra_args + n_sym_arg; 
+    g_conc_argc = cli_argv.size() + extra_args + n_sym_arg;
     g_conc_argv = new char* [g_conc_argc + extra_args + n_sym_arg];
     INFO("g_conc_argc: " << g_conc_argc);
     auto cli_iter = cli_argv.begin();

headers/gensym/defs.hpp

@@ -36,6 +36,9 @@ inline std::atomic<unsigned int> cached_query_num = 0;
 // Number of concretization queries
 inline std::atomic<unsigned int> conc_query_num = 0;
 
+// Number of concretized queries after equality substitution
+inline std::atomic<unsigned int> rewrited_query_num = 0;
+
 /* Global options */
 
 inline bool use_thread_pool = false;
@@ -55,6 +58,7 @@ inline bool use_objcache = true;
 inline bool use_cexcache = true;
 // Use branch query caching or not
 inline bool use_brcache = true;
+inline bool use_equality_substitution = false;
 // Use constraint independence resolving or not
 inline bool use_cons_indep = true;
 // Only generate testcases for states that cover new blocks or not
@@ -95,6 +99,9 @@ inline SolverKind solver_kind = SolverKind::stp;
 inline std::atomic<long int> ext_solver_time = 0;
 // Internal solver time (the whole process of constraint translation/caching/solving)
 inline std::atomic<long int> int_solver_time = 0;
+inline std::atomic<long int> simp_expr_time = 0;
+inline std::atomic<long int> equality_time = 0;
+inline std::atomic<long int> rewriting_time = 0;
 // FS time: time taken to perform FS operations
 inline std::atomic<long int> fs_time = 0;
 // Time spent in solver expression construction

headers/gensym/monitor.hpp

@@ -140,6 +140,11 @@ struct Monitor {
         std::cout << "else-br: " << (else_miss_time / 1.0e6) << "s; "
                   << "then-br: " << (then_miss_time / 1.0e6) << "s; "
                   << "both-br: " << (both_miss_time / 1.0e6) << "s\n";
+
+        std::cout << "Simplify expr: " << (simp_expr_time / 1.0e6) << "s; "
+                  << "Collecting equalities: " << (equality_time / 1.0e6) << "s; "
+                  << "Rewrite expr: " << (rewriting_time / 1.0e6) << "s; "
+                  << "#Rewrited concrete query: " << rewrited_query_num <<"/" << br_query_num << "\n";
       }
       std::cout << "[" << (ext_solver_time / 1.0e6) << "s/"
                 << (int_solver_time / 1.0e6) << "s/"

headers/gensym/smt_checker.hpp

@@ -150,7 +150,7 @@ class CachedChecker : public Checker {
       ABORT("Cannot create the test case file, abort.\n");
     }
     for (auto& v : pc.vars) {
-      output << v->to_SymV()->name << "=" 
+      output << v->to_SymV()->name << "="
              << self()->eval_model(model, v) << std::endl;
     }
     int n = write(out_fd, output.str().c_str(), output.str().size());
@@ -250,13 +250,99 @@ class CachedChecker : public Checker {
     auto res = check_model(indep_pc);
     update_model_cache(res, indep_pc);
     pop();
-    
+
     return res;
   }
 
+  // Rewrite the expression val according to given equalities
+  PtrVal rewriteExpr(std::map< PtrVal, PtrVal >& equalities, PtrVal val) {
+    if (val->to_IntV()) return val;
+
+    auto sym_val = val->to_SymV();
+    ASSERT(sym_val, "Rewriting a non-symbolic term");
+    auto eq_it = equalities.find(sym_val);
+    if (eq_it != equalities.end()) {
+      return eq_it->second;
+    }
+    if (sym_val->is_var()) {
+      return sym_val;
+    }
+    if (sym_val->rator == iOP::op_extract) {
+      auto hi = (*sym_val)[1]->to_IntV()->as_signed();
+      auto lo = (*sym_val)[2]->to_IntV()->as_signed();
+      return bv_extract(rewriteExpr(equalities, (*sym_val)[0]), hi, lo);
+    }
+    if (sym_val->rands.size() == 1) {
+      if (sym_val->rator == iOP::op_trunc) {
+        auto from = (*sym_val)[0]->get_bw();
+        auto to = sym_val->get_bw();
+        return int_op_1(sym_val->rator, rewriteExpr(equalities, (*sym_val)[0]), { from, to });
+      }
+      return int_op_1(sym_val->rator, rewriteExpr(equalities, (*sym_val)[0]), { sym_val->get_bw() });
+    }
+    if (sym_val->rands.size() == 2) {
+      return int_op_2(sym_val->rator, rewriteExpr(equalities, (*sym_val)[0]), rewriteExpr(equalities, (*sym_val)[1]));
+    }
+    if (sym_val->rands.size() == 3) {
+      return int_op_3(sym_val->rator, rewriteExpr(equalities, (*sym_val)[0]), rewriteExpr(equalities, (*sym_val)[1]), rewriteExpr(equalities, (*sym_val)[2]));
+    }
+    ABORT("Unknown operation");
+  }
+
+  PtrVal simplifyExpr(PC& pc, PtrVal cond) {
+    if (cond->to_IntV())
+      return cond;
+
+    std::map< PtrVal, PtrVal > equalities;
+
+    auto eq_start = steady_clock::now();
+
+    for (auto &constraint : pc.get_path_conds()) {
+      auto sym_cons = constraint->to_SymV();
+      if (sym_cons) {
+        if (sym_cons->rands.size() == 2 && iOP::op_eq == sym_cons->rator) {
+          auto left = (*sym_cons)[0];
+          auto right = (*sym_cons)[1];
+          if (left->to_IntV()) {
+            equalities.insert(std::make_pair(right, left));
+          } else if (right->to_IntV()) {
+            equalities.insert(std::make_pair(left, right));
+          } else {
+            equalities.insert(std::make_pair(constraint, make_IntV(1, 1)));
+          }
+        } else {
+          equalities.insert(std::make_pair(constraint, make_IntV(1, 1)));
+        }
+      }
+    }
+
+    auto eq_end = steady_clock::now();
+    equality_time += duration_cast<microseconds>(eq_end - eq_start).count();
+
+    if (!equalities.empty()) {
+      auto rw_start = steady_clock::now();
+      cond = rewriteExpr(equalities, cond);
+      auto rw_end = steady_clock::now();
+      rewriting_time += duration_cast<microseconds>(rw_end - rw_start).count();
+    }
+
+    return cond;
+  }
+
   virtual BrResult check_branch(PC& pc, PtrVal cond) override {
     if (!use_solver) return std::make_pair(sat, sat);
     br_query_num++;
+    auto simp_start = steady_clock::now();
+    if (use_equality_substitution) {
+      cond = simplifyExpr(pc, cond);
+    }
+    auto simp_end = steady_clock::now();
+    simp_expr_time += duration_cast<microseconds>(simp_end - simp_start).count();
+    if (cond->to_IntV()) {
+      rewrited_query_num++;
+      IntData condv = proj_IntV(cond);
+      return std::make_pair(0 == condv ? solver_result::unsat : solver_result::sat, 0 == condv ? solver_result::sat : solver_result::unsat);
+    }
 
     auto start = steady_clock::now();
     auto neg_cond = SymV::neg(cond);

src/main/scala/llvm/Benchmarks.scala

@@ -114,7 +114,9 @@ object Benchmarks {
   lazy val argv2Test = parseFile("benchmarks/llvm/argv2.ll")
 
   lazy val unprintableCharTest = parseFile("benchmarks/llvm/unprintable_char.ll")
-
+
+  lazy val equalityTest = parseFile("benchmarks/llvm/equality.ll")
+
   lazy val echo_linked = parseFile("benchmarks/coreutils/echo.ll")
   lazy val cat_linked = parseFile("benchmarks/coreutils/cat.ll")
   lazy val true_linked = parseFile("benchmarks/coreutils/true.ll")