From 959b250e4a70a4db0d79fa0d667a3c5cc9b2cdcb Mon Sep 17 00:00:00 2001 From: RuiqiGao Date: Fri, 4 Nov 2022 15:08:24 -0400 Subject: [PATCH] equality_sustitution --- benchmarks/llvm/equality.c | 16 +++++ headers/gensym/cli.hpp | 8 ++- headers/gensym/defs.hpp | 7 +++ headers/gensym/monitor.hpp | 5 ++ headers/gensym/smt_checker.hpp | 90 +++++++++++++++++++++++++++- src/main/scala/llvm/Benchmarks.scala | 4 +- 6 files changed, 125 insertions(+), 5 deletions(-) create mode 100644 benchmarks/llvm/equality.c diff --git a/benchmarks/llvm/equality.c b/benchmarks/llvm/equality.c new file mode 100644 index 00000000..a19044e7 --- /dev/null +++ b/benchmarks/llvm/equality.c @@ -0,0 +1,16 @@ +#include "../../headers/gensym_client.h" +#include + +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; +} \ No newline at end of file diff --git a/headers/gensym/cli.hpp b/headers/gensym/cli.hpp index 9a7bb339..42e97b35 100644 --- a/headers/gensym/cli.hpp +++ b/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(); diff --git a/headers/gensym/defs.hpp b/headers/gensym/defs.hpp index 8a361873..5c00ab77 100644 --- a/headers/gensym/defs.hpp +++ b/headers/gensym/defs.hpp @@ -36,6 +36,9 @@ inline std::atomic cached_query_num = 0; // Number of concretization queries inline std::atomic conc_query_num = 0; +// Number of concretized queries after equality substitution +inline std::atomic 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 ext_solver_time = 0; // Internal solver time (the whole process of constraint translation/caching/solving) inline std::atomic int_solver_time = 0; +inline std::atomic simp_expr_time = 0; +inline std::atomic equality_time = 0; +inline std::atomic rewriting_time = 0; // FS time: time taken to perform FS operations inline std::atomic fs_time = 0; // Time spent in solver expression construction diff --git a/headers/gensym/monitor.hpp b/headers/gensym/monitor.hpp index 9e0620ed..8e8180ca 100644 --- a/headers/gensym/monitor.hpp +++ b/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/" diff --git a/headers/gensym/smt_checker.hpp b/headers/gensym/smt_checker.hpp index c4fffcc0..660a2e1f 100644 --- a/headers/gensym/smt_checker.hpp +++ b/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(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(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(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); diff --git a/src/main/scala/llvm/Benchmarks.scala b/src/main/scala/llvm/Benchmarks.scala index 93e00308..b00a2240 100644 --- a/src/main/scala/llvm/Benchmarks.scala +++ b/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")