From cc9210b87e58db12fb56220c023baf50ac98466f Mon Sep 17 00:00:00 2001 From: zhuyt Date: Thu, 5 Sep 2024 14:30:02 +0800 Subject: [PATCH] fix build deref for a whole region and fix project for field_of --- benchmark/case_3.c | 8 +-- src/goto-symex/symex_target_equation.cpp | 7 ++- src/pointer-analysis/dereference.cpp | 18 +++--- src/solvers/smt/smt_conv.cpp | 19 +++--- src/solvers/z3-slhv/z3_slhv_conv.cpp | 74 ++++++++++-------------- src/solvers/z3-slhv/z3_slhv_conv.h | 4 -- 6 files changed, 58 insertions(+), 72 deletions(-) diff --git a/benchmark/case_3.c b/benchmark/case_3.c index b80f5896..8a3aa9ed 100644 --- a/benchmark/case_3.c +++ b/benchmark/case_3.c @@ -2,8 +2,8 @@ int main(){ - int num = 5; - int *j = (int*)malloc(num*sizeof(int)); - *(j+6) = num + (-1); - free(j); + int **p = malloc(sizeof(int*)); + *p = malloc(sizeof(int)); + free(*p); + free(p); } \ No newline at end of file diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 6929b399..62be9118 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -169,9 +169,10 @@ void symex_target_equationt::convert_internal_step( step.dump(); log_status(" ============================== step ======================== "); - log_status("convert step guard ast: "); - step.guard_ast = smt_conv.convert_ast(step.guard); - step.guard_ast->dump(); + // log_status("convert step guard ast: "); + // guard_ast is used for generating witness + // not used now + // step.guard_ast = smt_conv.convert_ast(step.guard); if (step.is_assume() || step.is_assert()) { diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index 57b6d36a..ea797cf5 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -532,12 +532,12 @@ expr2tc dereferencet::dereference( if (is_nil_expr(new_value)) continue; - - log_status("after building reference to : not nill"); - new_value->dump(); assert(!is_nil_expr(pointer_guard)); + new_value->dump(); + type->dump(); + if (!dereference_type_compare(new_value, type)) { guardt new_guard(guard); @@ -915,6 +915,7 @@ expr2tc dereferencet::build_reference_to( // to have a reference built at all. if (is_internal(mode)) { + log_status("collect objects for doing free"); dereference_callbackt::internal_item internal; internal.object = value; internal.offset = final_offset; // offset for SLHV @@ -1274,10 +1275,8 @@ void dereferencet::build_deref_slhv( log_error("heap region must be aligned"); abort(); } - - // heap region as a value - if (field == 0 && access_sz == _type.total_bytes) return; + bool is_field = true; if (field >= _type.field_types.size() || access_sz != _type.total_bytes / _type.field_types.size()) { @@ -1286,15 +1285,18 @@ void dereferencet::build_deref_slhv( type, dereference_callback.get_nondet_id("undefined_behavior_var")); value = sym; - return; + is_field = false; } else value = field_of2tc(type, value, gen_ulong(field)); // update field type - if (_type.set_field_type(field, type)) + if (is_field && _type.set_field_type(field, type)) dereference_callback.update_heap_type(_type); + log_status("return dereference --->"); + value->dump(); + log_status(" ----------------- build deref slhv ----------------- "); } diff --git a/src/solvers/smt/smt_conv.cpp b/src/solvers/smt/smt_conv.cpp index 8e1b4f05..c50cd3ef 100644 --- a/src/solvers/smt/smt_conv.cpp +++ b/src/solvers/smt/smt_conv.cpp @@ -252,6 +252,8 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) return (cache_result->ast); } + bool use_old_encoding = !options.get_bool_option("z3-slhv"); + /* Vectors! * * Here we need special attention for Vectors, because of the way @@ -262,7 +264,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) * for some reason we would like to run ESBMC without simplifications * then we need to apply it here. */ - if (!options.get_bool_option("z3-slhv") && is_vector_type(expr)) + if (use_old_encoding && is_vector_type(expr)) { if (is_neg2t(expr)) { @@ -317,12 +319,15 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) case expr2t::pointer_capability_id: case expr2t::field_of_id: + case expr2t::heap_region_id: case expr2t::heap_update_id: case expr2t::heap_delete_id: break; // Don't convert their operands default: { + if (is_same_object2t(expr) && !use_old_encoding) break; + // Convert all the arguments and store them in 'args'. unsigned int i = 0; expr->foreach_operand( @@ -365,8 +370,6 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) case expr2t::symbol_id: { a = convert_terminal(expr); - log_status("convert_terminal result: "); - a->dump(); break; } case expr2t::constant_string_id: @@ -455,7 +458,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) is_pointer_type(expr->type) || is_pointer_type(add.side_1) || is_pointer_type(add.side_2)) { - a = this->solver_text() == "Z3-slhv" ? + a = !use_old_encoding ? convert_slhv_opts(expr, args) : convert_pointer_arith(expr, expr->type); } @@ -476,7 +479,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) is_pointer_type(expr->type) || is_pointer_type(sub.side_1) || is_pointer_type(sub.side_2)) { - a = this->solver_text() == "Z3-slhv" ? + a = !use_old_encoding ? convert_slhv_opts(expr, args) : convert_pointer_arith(expr, expr->type); } @@ -742,7 +745,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) { const same_object2t& so = to_same_object2t(expr); // Two projects, then comparison. - if (this->solver_text() != "Z3-slhv") { + if (use_old_encoding) { args[0] = args[0]->project(this, 0); args[1] = args[1]->project(this, 0); a = mk_eq(args[0], args[1]); @@ -760,7 +763,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) ptr = &to_typecast2t(*ptr).from; args[0] = convert_ast(*ptr); - a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0); + a = !use_old_encoding ? args[0] : args[0]->project(this, 0); break; } case expr2t::pointer_object_id: @@ -772,7 +775,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr) ptr = &to_typecast2t(*ptr).from; args[0] = convert_ast(*ptr); - a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0); + a = !use_old_encoding ? 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 9c96e8bf..452b6393 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.cpp +++ b/src/solvers/z3-slhv/z3_slhv_conv.cpp @@ -206,13 +206,15 @@ z3_slhv_convt::convert_slhv_opts( case expr2t::heap_region_id: { const intheap_type2t &_type = to_intheap_type(expr->type); + + smt_astt base_loc = convert_ast(_type.location); std::vector pt_vec; if (_type.is_aligned) { for (unsigned i = 0; i < _type.field_types.size(); i++) { - smt_astt loc = i == 0 ? args[1] : mk_locadd(args[1], mk_smt_int(BigInt(i))); + smt_astt loc = i == 0 ? base_loc : mk_locadd(base_loc, mk_smt_int(BigInt(i))); smt_sortt sort = is_intloc_type(_type.field_types[i]) ? mk_intloc_sort() : mk_int_sort(); @@ -229,7 +231,7 @@ z3_slhv_convt::convert_slhv_opts( // Default sort is intloc pt_vec.push_back( mk_pt( - args[1], + base_loc, mk_fresh(mk_intloc_sort(), mk_fresh_name("tmp_loc::") ) ) @@ -289,43 +291,12 @@ z3_slhv_convt::convert_slhv_opts( } return mk_subh(args[1], args[0]); } - case expr2t::field_of_id: - case expr2t::heap_update_id: - case expr2t::heap_delete_id: - { - z3_slhv_convt::smt_ast_pair sap = convert_opt_without_assert(expr); - assert_ast(sap.first); - return sap.second; - } - case expr2t::same_object_id: - { - // Do project for SLHV - const same_object2t& same = to_same_object2t(expr); - smt_astt p1 = this->project(same.side_1); - smt_astt p2 = this->project(same.side_2); - smt_astt eq = mk_eq(p1, p2); - return eq; - } - default: { - log_status("Invalid SLHV operations!!!"); - abort(); - } - } -} - -z3_slhv_convt::smt_ast_pair -z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr) -{ - switch (expr->expr_id) - { case expr2t::field_of_id: { const field_of2t &field_of = to_field_of2t(expr); if (is_constant_intheap2t(field_of.source_heap)) - return std::make_pair( - mk_smt_bool(true), - mk_fresh(convert_sort(field_of.type), mk_fresh_name("invalid_loc_"))); + return mk_fresh(convert_sort(field_of.type), mk_fresh_name("invalid_fieldof_")); if (!is_constant_int2t(field_of.operand)) { @@ -357,8 +328,8 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr) } smt_astt v1 = mk_fresh(s1, name); - smt_astt assert_expr = mk_subh(mk_pt(loc, v1), convert_ast(heap_region)); - return std::make_pair(assert_expr, v1); + assert_ast(mk_subh(mk_pt(loc, v1), convert_ast(heap_region))); + return v1; } case expr2t::heap_update_id: { @@ -387,13 +358,11 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr) // current heap state smt_astt old_state = mk_uplus(h1, mk_pt(loc, v1)); - smt_astt assert_expr = mk_eq(h, old_state); + assert_ast(mk_eq(h, old_state)); // new heap state smt_astt new_state = mk_uplus(h1, mk_pt(loc, val)); - - // new heap state - return std::make_pair(assert_expr, new_state); + return new_state; } case expr2t::heap_delete_id: { @@ -404,12 +373,22 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr) smt_astt h1 = mk_fresh(mk_intheap_sort(), mk_fresh_name("tmp_heap::")); smt_astt v1 = mk_fresh(mk_int_sort(), mk_fresh_name("tmp_val::")); - smt_astt assert_expr = mk_eq(h, mk_uplus(h1, mk_pt(l, v1))); - return std::make_pair(assert_expr, h1); + assert_ast(mk_eq(h, mk_uplus(h1, mk_pt(l, v1)))); + return h1; + } + case expr2t::same_object_id: + { + // Do project for SLHV + const same_object2t& same = to_same_object2t(expr); + smt_astt p1 = this->project(same.side_1); + smt_astt p2 = this->project(same.side_2); + smt_astt eq = mk_eq(p1, p2); + return eq; } default: { - return std::make_pair(mk_smt_bool(true), convert_ast(expr)); + log_status("Invalid SLHV operations!!!"); + abort(); } } } @@ -423,12 +402,17 @@ smt_astt z3_slhv_convt::project(const expr2tc &expr) const intheap_type2t &_type = to_intheap_type(expr->type); return this->project(_type.location); } - return convert_opt_without_assert(expr).second; + + if (is_intloc_type(expr) || is_pointer_type(expr)) + return convert_ast(expr); + + log_error("Wrong symbol for projection"); + expr->dump(); } else if (is_location_of2t(expr)) return this->project(to_location_of2t(expr).source_heap); else if (is_field_of2t(expr)) - return convert_opt_without_assert(expr).second; + return convert_ast(expr); else if (is_typecast2t(expr)) return this->project(to_typecast2t(expr).from); else if (is_locadd2t(expr)) diff --git a/src/solvers/z3-slhv/z3_slhv_conv.h b/src/solvers/z3-slhv/z3_slhv_conv.h index 5ab9d3d7..611096fa 100644 --- a/src/solvers/z3-slhv/z3_slhv_conv.h +++ b/src/solvers/z3-slhv/z3_slhv_conv.h @@ -42,10 +42,6 @@ class z3_slhv_convt : public z3_convt { smt_astt convert_slhv_opts(const expr2tc &expr, const std::vector& args) override; - typedef std::pair smt_ast_pair; - - smt_ast_pair convert_opt_without_assert(const expr2tc &expr); - smt_astt project(const expr2tc &expr); void dump_smt() override;