From 617aec227bad99109938c570c717db4fdd10155d Mon Sep 17 00:00:00 2001 From: zhuyt Date: Thu, 11 Jul 2024 17:27:32 +0800 Subject: [PATCH] heap update encoding --- src/esbmc/bmc.cpp | 2 +- src/solvers/smt/smt_casts.cpp | 2 +- src/solvers/smt/smt_conv.cpp | 43 ++++++++++++++++++++++++++-- src/solvers/z3-slhv/z3_slhv_conv.cpp | 43 ++++++++++++++-------------- src/solvers/z3-slhv/z3_slhv_conv.h | 32 ++++++++++----------- 5 files changed, 79 insertions(+), 43 deletions(-) diff --git a/src/esbmc/bmc.cpp b/src/esbmc/bmc.cpp index c5278d4f..29455ac8 100644 --- a/src/esbmc/bmc.cpp +++ b/src/esbmc/bmc.cpp @@ -657,7 +657,7 @@ smt_convt::resultt bmct::run_thread(std::shared_ptr &eq) std::unique_ptr(create_solver("", ns, options)); log_status("smt_convt created"); if (options.get_bool_option("z3-slhv")) { - // show_vcc(*eq); + show_vcc(*eq); generate_smt_from_equation(*runtime_solver, *eq); return smt_convt::P_SMTLIB; } diff --git a/src/solvers/smt/smt_casts.cpp b/src/solvers/smt/smt_casts.cpp index 05c54985..6e82338d 100644 --- a/src/solvers/smt/smt_casts.cpp +++ b/src/solvers/smt/smt_casts.cpp @@ -403,7 +403,7 @@ smt_astt smt_convt::convert_typecast_to_ptr(const typecast2t &cast) { // First, sanity check -- typecast from one kind of a pointer to another kind // is a simple operation. Check for that first. - if (is_pointer_type(cast.from)) + if (is_pointer_type(cast.from) || is_intloc_type(cast.from)) return convert_ast(cast.from); // Unpleasentness; we don't know what pointer this integer is going to diff --git a/src/solvers/smt/smt_conv.cpp b/src/solvers/smt/smt_conv.cpp index e5dc3aab..5149eb5a 100644 --- a/src/solvers/smt/smt_conv.cpp +++ b/src/solvers/smt/smt_conv.cpp @@ -232,6 +232,11 @@ smt_astt smt_convt::convert_assign(const expr2tc &expr) smt_cache_entryt e = {eq.side_1, side2, ctx_level}; smt_cache.insert(e); + log_status(" ----------------- assignment result ----------------- "); + side1->dump(); + side2->dump(); + log_status(" ----------------- assignment result ----------------- "); + return side2; } @@ -315,6 +320,12 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) unsigned int i = 0; expr->foreach_operand( [this, &args, &i](const expr2tc &e) { args[i++] = convert_ast(e); }); + log_status(" -------------- convert args finished ------------ "); + for (int i = 0; i < expr->get_num_sub_exprs(); i++) { + args[i]->dump(); + } + log_status(" -------------- convert args finished ------------ "); + } } @@ -339,6 +350,29 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) a = mk_locadd(args[0], args[1]); break; } + case expr2t::heap_update_id: { + log_status("heap update"); + const heap_update2t& heap_upd = to_heap_update2t(expr); + smt_astt h = args[0]; + smt_astt h1 = mk_fresh(mk_intheap_sort(), mk_fresh_name("tmp_heap")); + smt_astt adr = args[1]; + smt_astt val = args[2]; + smt_astt v1 = mk_fresh(val->sort, mk_fresh_name("tmp_val")); + // old heap state + smt_astt o_state = mk_eq(h, mk_uplus(mk_pt(adr, v1), h1)); + assert_ast(o_state); + // new heap state + a = mk_uplus(mk_pt(adr, val), h1); + break; + } + case expr2t::heap_load_id: { + log_status("TODO: heap load"); + abort(); + } + case expr2t::heap_contains_id: { + log_status("TODO: heap contains"); + abort(); + } case expr2t::constant_intheap_id: case expr2t::constant_intloc_id: @@ -721,9 +755,12 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) } case expr2t::same_object_id: { + const same_object2t& so = to_same_object2t(expr); // Two projects, then comparison. - args[0] = args[0]->project(this, 0); - args[1] = args[1]->project(this, 0); + if (this->solver_text() != "Z3-slhv") { + args[0] = args[0]->project(this, 0); + args[1] = args[1]->project(this, 0); + } a = mk_eq(args[0], args[1]); break; } @@ -748,7 +785,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) ptr = &to_typecast2t(*ptr).from; args[0] = convert_ast(*ptr); - a = args[0]->project(this, 0); + a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0); break; } case expr2t::pointer_capability_id: diff --git a/src/solvers/z3-slhv/z3_slhv_conv.cpp b/src/solvers/z3-slhv/z3_slhv_conv.cpp index 9c670a49..39b5cf45 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.cpp +++ b/src/solvers/z3-slhv/z3_slhv_conv.cpp @@ -3,8 +3,7 @@ #include #include - -#define new_ast new_solver_ast +#define new_ast new_solver_ast smt_convt *create_new_z3_slhv_solver( const optionst &options, @@ -43,22 +42,22 @@ smt_convt *create_new_z3_slhv_solver( return conv; } -smt_astt z3_slhv_smt_ast::update(smt_convt *ctx, - smt_astt value, - unsigned int idx, - expr2tc idx_expr) - const { - log_status("slhv_smt does not support update"); - return nullptr; - } -smt_astt z3_slhv_smt_ast::project(smt_convt *ctx, unsigned int elem)const { - log_status("slhv_smt does not support project"); - return nullptr; -} -void z3_slhv_smt_ast::dump() const { - std::string print_str = a.to_string(); - log_status("{}\n sort is {}", print_str, a.get_sort().to_string()); -} +// smt_astt z3_slhv_smt_ast::update(smt_convt *ctx, +// smt_astt value, +// unsigned int idx, +// expr2tc idx_expr) +// const { +// log_status("slhv_smt does not support update"); +// return nullptr; +// } +// smt_astt z3_slhv_smt_ast::project(smt_convt *ctx, unsigned int elem) const { +// log_status("slhv_smt does not support project"); +// return nullptr; +// } +// void z3_slhv_smt_ast::dump() const { +// std::string print_str = a.to_string(); +// log_status("{}\n sort is {}", print_str, a.get_sort().to_string()); +// } z3_slhv_convt::z3_slhv_convt(const namespacet &_ns, const optionst& _options) : z3_convt(_ns, _options) { // initialize the z3 based slhv converter here @@ -192,15 +191,15 @@ const std::string z3_slhv_convt::solver_text() { // heap terms smt_astt z3_slhv_convt::mk_pt(smt_astt a, smt_astt b) { z3::expr pt = z3::points_to( - to_solver_smt_ast(a)->a, - to_solver_smt_ast(b)->a + to_solver_smt_ast(a)->a, + to_solver_smt_ast(b)->a ); return new_ast(pt, this->mk_intheap_sort()); } smt_astt z3_slhv_convt::mk_uplus(smt_astt a, smt_astt b){ z3::expr h = z3::uplus( - to_solver_smt_ast(a)->a, - to_solver_smt_ast(b)->a + to_solver_smt_ast(a)->a, + to_solver_smt_ast(b)->a ); return new_ast(h, this->mk_intheap_sort()); } diff --git a/src/solvers/z3-slhv/z3_slhv_conv.h b/src/solvers/z3-slhv/z3_slhv_conv.h index 9f237ffa..a64bad17 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.h +++ b/src/solvers/z3-slhv/z3_slhv_conv.h @@ -7,22 +7,22 @@ #include #include -class z3_slhv_smt_ast : public solver_smt_ast -{ -public: - using solver_smt_ast::solver_smt_ast; - ~z3_slhv_smt_ast() override = default; - - smt_astt 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; - - void dump() const override; -}; +// class z3_slhv_smt_ast : public solver_smt_ast +// { +// public: +// using solver_smt_ast::solver_smt_ast; +// ~z3_slhv_smt_ast() override = default; + +// smt_astt 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; + +// void dump() const override; +// }; class z3_slhv_convt : public z3_convt { public: