From e10d054038475b9b8659773f9736332ee3e7d179 Mon Sep 17 00:00:00 2001 From: clexmaAtFlankerB Date: Thu, 23 May 2024 18:32:45 +0800 Subject: [PATCH] slhv_convt_framework established --- scripts/README | 0 scripts/README.md | 0 scripts/benchexec.sh | 0 scripts/build.ps1 | 0 scripts/build.sh | 0 scripts/buildidobj.py | 0 scripts/flail.py | 0 scripts/release-notes.txt | 0 scripts/run_csmith.py | 0 scripts/winflexbison_install.ps1 | 0 scripts/witness.sh | 0 src/esbmc/bmc.cpp | 19 ++++++- src/esbmc/bmc.h | 3 + src/goto-symex/symex_target_equation.h | 3 + src/solvers/solve.cpp | 18 ++---- src/solvers/solve.h | 5 ++ src/solvers/z3-slhv/z3_slhv_conv.cpp | 78 +++++++++++++++++++++++--- src/solvers/z3-slhv/z3_slhv_conv.h | 18 ++++-- 18 files changed, 117 insertions(+), 27 deletions(-) mode change 100644 => 100755 scripts/README mode change 100644 => 100755 scripts/README.md mode change 100644 => 100755 scripts/benchexec.sh mode change 100644 => 100755 scripts/build.ps1 mode change 100644 => 100755 scripts/build.sh mode change 100644 => 100755 scripts/buildidobj.py mode change 100644 => 100755 scripts/flail.py mode change 100644 => 100755 scripts/release-notes.txt mode change 100644 => 100755 scripts/run_csmith.py mode change 100644 => 100755 scripts/winflexbison_install.ps1 mode change 100644 => 100755 scripts/witness.sh diff --git a/scripts/README b/scripts/README old mode 100644 new mode 100755 diff --git a/scripts/README.md b/scripts/README.md old mode 100644 new mode 100755 diff --git a/scripts/benchexec.sh b/scripts/benchexec.sh old mode 100644 new mode 100755 diff --git a/scripts/build.ps1 b/scripts/build.ps1 old mode 100644 new mode 100755 diff --git a/scripts/build.sh b/scripts/build.sh old mode 100644 new mode 100755 diff --git a/scripts/buildidobj.py b/scripts/buildidobj.py old mode 100644 new mode 100755 diff --git a/scripts/flail.py b/scripts/flail.py old mode 100644 new mode 100755 diff --git a/scripts/release-notes.txt b/scripts/release-notes.txt old mode 100644 new mode 100755 diff --git a/scripts/run_csmith.py b/scripts/run_csmith.py old mode 100644 new mode 100755 diff --git a/scripts/winflexbison_install.ps1 b/scripts/winflexbison_install.ps1 old mode 100644 new mode 100755 diff --git a/scripts/witness.sh b/scripts/witness.sh old mode 100644 new mode 100755 diff --git a/src/esbmc/bmc.cpp b/src/esbmc/bmc.cpp index a69482af..314d01a4 100644 --- a/src/esbmc/bmc.cpp +++ b/src/esbmc/bmc.cpp @@ -162,6 +162,13 @@ void bmct::generate_smt_from_equation( "Encoding to solver time: {}s", time2string(encode_stop - encode_start)); } +std::string bmct::generate_slhv_smt_from_equation(z3_slhv_convt& slhv_solver, symex_target_equationt &eq) { + log_status("generate slhv formula from equation"); + std::string result; + + return result; +} + smt_convt::resultt bmct::run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq) { @@ -190,6 +197,8 @@ bmct::run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq) return dec_result; } + + void bmct::report_success() { log_success("\nVERIFICATION SUCCESSFUL"); @@ -638,13 +647,21 @@ smt_convt::resultt bmct::run_thread(std::shared_ptr &eq) return smt_convt::P_UNSATISFIABLE; } - if (!options.get_bool_option("smt-during-symex")) + if (!options.get_bool_option("smt-during-symex") && !options.get_bool_option("z3-slhv")) { runtime_solver = std::unique_ptr(create_solver("", ns, options)); log_status("smt_convt created"); } + if (!options.get_bool_option("smt-during-symex") && options.get_bool_option("z3-slhv")) { + + z3_slhv_convt* slhv_conv = new z3_slhv_convt(ns, options); + slhv_converter = std::unique_ptr(slhv_conv); + ; + std::string smt_str = generate_slhv_smt_from_equation(*slhv_converter, *eq); + } + if ( options.get_bool_option("multi-property") && options.get_bool_option("base-case")) diff --git a/src/esbmc/bmc.h b/src/esbmc/bmc.h index 8ceaf620..0046aaf8 100644 --- a/src/esbmc/bmc.h +++ b/src/esbmc/bmc.h @@ -32,6 +32,7 @@ class bmct namespacet ns; std::unique_ptr runtime_solver; + std::unique_ptr slhv_converter; std::unique_ptr symex; virtual smt_convt::resultt @@ -71,6 +72,8 @@ class bmct void generate_smt_from_equation(smt_convt &smt_conv, symex_target_equationt &eq); + + std::string generate_slhv_smt_from_equation(z3_slhv_convt& slhv_solver, symex_target_equationt &eq); }; #endif diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 7b902663..c85ad5fa 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -10,6 +10,7 @@ #include #include #include +#include #include #include #include @@ -72,6 +73,8 @@ class symex_target_equationt : public symex_targett const sourcet &source) override; virtual void convert(smt_convt &smt_conv); + std::string convert2slhv(z3_slhv_convt& slhv_convt); + void convert_internal_step( smt_convt &smt_conv, smt_astt &assumpt_ast, diff --git a/src/solvers/solve.cpp b/src/solvers/solve.cpp index 2c420275..50a2be28 100644 --- a/src/solvers/solve.cpp +++ b/src/solvers/solve.cpp @@ -5,6 +5,7 @@ #include #include #include +#include #include @@ -16,7 +17,6 @@ solver_creator create_new_cvc_solver; solver_creator create_new_mathsat_solver; solver_creator create_new_yices_solver; solver_creator create_new_bitwuzla_solver; -solver_creator create_new_z3_slhv_solver; static const std::unordered_map esbmc_solvers = { #ifdef SMTLIB @@ -43,11 +43,10 @@ static const std::unordered_map esbmc_solvers = { #ifdef BITWUZLA {"bitwuzla", create_new_bitwuzla_solver} #endif -#ifdef Z3_SLHV - {"z3-slhv", create_new_z3_slhv_solver} -#endif }; + + static const std::string all_solvers[] = { "smtlib", "z3", @@ -56,8 +55,7 @@ static const std::string all_solvers[] = { "cvc", "mathsat", "yices", - "bitwuzla", - "z3-slhv"}; + "bitwuzla"}; static std::string pick_default_solver() { @@ -124,14 +122,13 @@ smt_convt *create_solver( array_iface *array_api = nullptr; fp_convt *fp_api = nullptr; + solver_creator &factory = pick_solver(solver_name, options); smt_convt *ctx = factory(options, ns, &tuple_api, &array_api, &fp_api); - bool node_flat = options.get_bool_option("tuple-node-flattener"); bool sym_flat = options.get_bool_option("tuple-sym-flattener"); bool array_flat = options.get_bool_option("array-flattener"); bool fp_to_bv = options.get_bool_option("fp2bv"); - // Pick a tuple flattener to use. If the solver has native support, and no // options were given, use that by default if (tuple_api != nullptr && !node_flat && !sym_flat) @@ -145,7 +142,6 @@ smt_convt *create_solver( // Default: node flattener else ctx->set_tuple_iface(new smt_tuple_node_flattener(ctx, ns)); - // Pick an array flattener to use. Again, pick the solver native one by // default, or the one specified, or if none of the above then use the built // in arrays -> to BV flattener. @@ -155,13 +151,11 @@ smt_convt *create_solver( ctx->set_array_iface(new array_convt(ctx)); else ctx->set_array_iface(new array_convt(ctx)); - if (fp_api == nullptr || fp_to_bv) ctx->set_fp_conv(new fp_convt(ctx)); else ctx->set_fp_conv(fp_api); - - // TODO: SLHV ctx->smt_post_init(); return ctx; + } diff --git a/src/solvers/solve.h b/src/solvers/solve.h index 04e3e1de..1dde9273 100644 --- a/src/solvers/solve.h +++ b/src/solvers/solve.h @@ -14,6 +14,11 @@ typedef smt_convt *(solver_creator)( array_iface **array_api, fp_convt **fp_api); +// slhv added +typedef smt_convt *(slhv_solver_creator)( + const optionst &options, + const namespacet &ns); + smt_convt *create_solver( std::string solver_name, const namespacet &ns, diff --git a/src/solvers/z3-slhv/z3_slhv_conv.cpp b/src/solvers/z3-slhv/z3_slhv_conv.cpp index cac47ced..632b1cbe 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.cpp +++ b/src/solvers/z3-slhv/z3_slhv_conv.cpp @@ -1,16 +1,78 @@ #include #include +#include #include -smt_convt *create_new_z3_slhv_solver( - const optionst &options, - const namespacet &ns -) { - z3_slhv_convt* conv = new z3_slhv_convt(ns, options); - return conv; -} - z3_slhv_convt::z3_slhv_convt(const namespacet &_ns, const optionst& _options) : smt_convt(_ns, _options) { // initialize the z3 based slhv converter here +} + +z3_slhv_convt::~z3_slhv_convt() { + delete_all_asts(); +} +void z3_slhv_convt::push_ctx() { + +} + +void z3_slhv_convt::pop_ctx() { + +} + +void z3_slhv_convt::assert_ast(smt_astt a) { + +} + +smt_convt::resultt z3_slhv_convt::dec_solve() { + return P_SMTLIB; +} + +const std::string z3_slhv_convt::solver_text() { + return "Z3-slhv"; +} + +smt_astt z3_slhv_convt::mk_smt_int(const BigInt &theint) { + +} + +smt_astt z3_slhv_convt::mk_smt_real(const std::string &str) { + +} + +smt_astt z3_slhv_convt::mk_smt_bv(const BigInt &theint, smt_sortt s) { + +} +smt_astt z3_slhv_convt::mk_smt_bool(bool val){ + +} +smt_astt z3_slhv_convt::mk_smt_symbol(const std::string &name, smt_sortt s){ + +} +smt_astt z3_slhv_convt::mk_extract(smt_astt a, unsigned int high, unsigned int low){ + +} +smt_astt z3_slhv_convt::mk_sign_ext(smt_astt a, unsigned int topwidth){ + +} +smt_astt z3_slhv_convt::mk_zero_ext(smt_astt a, unsigned int topwidth){ + +} +smt_astt z3_slhv_convt::mk_concat(smt_astt a, smt_astt b){ + +} +smt_astt z3_slhv_convt::mk_ite(smt_astt cond, smt_astt t, smt_astt f){ + +} +bool z3_slhv_convt::get_bool(smt_astt a){ + +} +BigInt z3_slhv_convt::get_bv(smt_astt a, bool is_signed){ + +} +smt_astt z3_slhv_convt::overflow_arith(const expr2tc &expr){ + +} + +void z3_slhv_convt::dump_smt(){ + } \ No newline at end of file diff --git a/src/solvers/z3-slhv/z3_slhv_conv.h b/src/solvers/z3-slhv/z3_slhv_conv.h index 2e4b171a..1d468204 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.h +++ b/src/solvers/z3-slhv/z3_slhv_conv.h @@ -11,10 +11,13 @@ class z3_slhv_smt_ast : public solver_smt_ast { public: using solver_smt_ast::solver_smt_ast; - ~z3_smt_ast() override = default; + ~z3_slhv_smt_ast() override = default; smt_astt - update(smt_convt *ctx, smt_astt value, unsigned int idx, expr2tc idx_expr) + update(smt_convt *ctx, + smt_astt value, + unsigned int idx, + expr2tc idx_expr) const override; smt_astt project(smt_convt *ctx, unsigned int elem) const override; @@ -30,12 +33,15 @@ class z3_slhv_convt : public smt_convt { z3_slhv_convt(const namespacet &ns, const optionst &options); ~z3_slhv_convt() override; public: + // interface for translation + // TODO slhv: move to the api later, currently we use the smt-lib2 string translation + // interfaces of smt_convt need implementation void push_ctx() override; void pop_ctx() override; void assert_ast(smt_astt a) override; - resultt dec_solver() override; - std::string solver_text() override; + resultt dec_solve() override; + const std::string solver_text() override; smt_astt mk_smt_int(const BigInt &theint) override; smt_astt mk_smt_real(const std::string &str) override; @@ -49,10 +55,10 @@ class z3_slhv_convt : public smt_convt { smt_astt mk_ite(smt_astt cond, smt_astt t, smt_astt f) override; bool get_bool(smt_astt a) override; BigInt get_bv(smt_astt a, bool is_signed) override; - smt_astt overflow_arith(const expr2tc *&expr) override; + smt_astt overflow_arith(const expr2tc &expr) override; void dump_smt() override; -} +}; #endif \ No newline at end of file