From e56a98222dae88ed43217f5697c597dd57aa179f Mon Sep 17 00:00:00 2001 From: clexmaAtFlankerB Date: Sun, 28 Jul 2024 18:36:04 +0800 Subject: [PATCH] add heap free --- src/irep2/irep2.h | 3 ++- src/irep2/irep2_expr.cpp | 1 + src/irep2/irep2_expr.h | 22 +++++++++++++++++++ src/irep2/templates/irep2_templates.cpp | 2 ++ .../templates/irep2_templates_expr_data.cpp | 1 + src/util/migrate.cpp | 19 +++++++--------- 6 files changed, 36 insertions(+), 12 deletions(-) diff --git a/src/irep2/irep2.h b/src/irep2/irep2.h index 74dd5539..fd04902f 100644 --- a/src/irep2/irep2.h +++ b/src/irep2/irep2.h @@ -107,6 +107,7 @@ BOOST_PP_LIST_CONS(uplus, \ BOOST_PP_LIST_CONS(locadd, \ BOOST_PP_LIST_CONS(pointer_with_region, \ + BOOST_PP_LIST_CONS(heap_free, \ BOOST_PP_LIST_CONS(heap_load, \ BOOST_PP_LIST_CONS(heap_update, \ BOOST_PP_LIST_CONS(heap_append, \ @@ -151,7 +152,7 @@ BOOST_PP_LIST_CONS(signbit, \ BOOST_PP_LIST_CONS(concat, \ BOOST_PP_LIST_CONS(extract, \ - BOOST_PP_LIST_NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + BOOST_PP_LIST_NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) #define ESBMC_LIST_OF_TYPES \ BOOST_PP_LIST_CONS(bool, \ diff --git a/src/irep2/irep2_expr.cpp b/src/irep2/irep2_expr.cpp index 2148f8e5..96ca0181 100644 --- a/src/irep2/irep2_expr.cpp +++ b/src/irep2/irep2_expr.cpp @@ -78,6 +78,7 @@ static const char *expr_names[] = { "uplus", "locadd", "pointer_with_region", + "heap_free", "heap_load", "heap_update", "heap_append", diff --git a/src/irep2/irep2_expr.h b/src/irep2/irep2_expr.h index ac849c76..14aa07b6 100644 --- a/src/irep2/irep2_expr.h +++ b/src/irep2/irep2_expr.h @@ -1002,6 +1002,19 @@ class pointer_with_region_data : public expr2t typedef esbmct::expr2t_traits traits; }; +class heap_free_data : public expr2t { +public: + heap_free_data( + const type2tc &t, + datatype_ops::expr_ids id, + expr2tc pwr + ) : expr2t(t, id), pwr(pwr){} + + expr2tc pwr; + typedef esbmct::field_traits heap_free_data_pwr_field; + typedef esbmct::expr2t_traits traits; +}; + class heap_load_data : public expr2t { public: heap_load_data( @@ -1752,6 +1765,7 @@ irep_typedefs(points_to, points_to_data); irep_typedefs(uplus, uplus_data); irep_typedefs(locadd, locadd_data); irep_typedefs(pointer_with_region, pointer_with_region_data); +irep_typedefs(heap_free, heap_free_data); irep_typedefs(heap_load, heap_load_data); irep_typedefs(heap_update, heap_update_data); irep_typedefs(heap_append, heap_append_data); @@ -3259,6 +3273,14 @@ class pointer_with_region2t : public pointer_with_region_expr_methods static std::string field_names[esbmct::num_type_fields]; }; +class heap_free2t : public heap_free_expr_methods +{ +public: + heap_free2t(const type2tc &type, expr2tc pwr) : heap_free_expr_methods(type, heap_free_id, pwr) {} + + static std::string field_names[esbmct::num_type_fields]; +}; + class heap_load2t : public heap_load_expr_methods { public: diff --git a/src/irep2/templates/irep2_templates.cpp b/src/irep2/templates/irep2_templates.cpp index 9957fc08..51ec1b00 100644 --- a/src/irep2/templates/irep2_templates.cpp +++ b/src/irep2/templates/irep2_templates.cpp @@ -168,6 +168,8 @@ std::string locadd2t::field_names[esbmct::num_type_fields] = {"baseaddr", "added_num", "", "", ""}; std::string pointer_with_region2t::field_names[esbmct::num_type_fields] = {"loc_ptr", "region", "", "", ""}; +std::string heap_free2t::field_names[esbmct::num_type_fields] = +{"pointer_with_region", "", "", "", ""}; std::string heap_load2t::field_names[esbmct::num_type_fields] = {"src_heap", "start_addr", "byte_len", "", ""}; std::string heap_update2t::field_names[esbmct::num_type_fields] = diff --git a/src/irep2/templates/irep2_templates_expr_data.cpp b/src/irep2/templates/irep2_templates_expr_data.cpp index 43905b33..7c3f5667 100644 --- a/src/irep2/templates/irep2_templates_expr_data.cpp +++ b/src/irep2/templates/irep2_templates_expr_data.cpp @@ -33,6 +33,7 @@ expr_typedefs3(points_to, points_to_data); expr_typedefs2(uplus, uplus_data); expr_typedefs2(locadd, locadd_data); expr_typedefs2(pointer_with_region, pointer_with_region_data); +expr_typedefs1(heap_free, heap_free_data); expr_typedefs3(heap_load, heap_load_data); expr_typedefs4(heap_update, heap_update_data); expr_typedefs4(heap_append, heap_append_data); diff --git a/src/util/migrate.cpp b/src/util/migrate.cpp index 40d9e173..52651c87 100644 --- a/src/util/migrate.cpp +++ b/src/util/migrate.cpp @@ -2636,6 +2636,14 @@ exprt migrate_expr_back(const expr2tc &ref) pointer_with_region.copy_to_operands(migrate_expr_back(ref2.region)); return pointer_with_region; } + case expr2t::heap_free_id: + { + const heap_free2t &ref2 = to_heap_free2t(ref); + typet thetype = migrate_type_back(ref->type); + exprt heap_free("heap_free", thetype); + heap_free.copy_to_operands(migrate_expr_back(ref2.pwr)); + return heap_free; + } case expr2t::heap_load_id: { const heap_load2t& ref2 = to_heap_load2t(ref); @@ -2668,17 +2676,6 @@ exprt migrate_expr_back(const expr2tc &ref) heap_update.set("byte_len", irep_idt(std::to_string(ref2.byte_len))); return heap_update; } - case expr2t::heap_append_id: - { - const heap_append2t &ref2 = to_heap_append2t(ref); - typet thetype = migrate_type_back(ref->type); - exprt heap_append("heap_append", thetype); - heap_append.copy_to_operands(migrate_expr_back(ref2.src_heap)); - heap_append.copy_to_operands(migrate_expr_back(ref2.start_addr)); - heap_append.copy_to_operands(migrate_expr_back(ref2.create_val)); - heap_append.set("byte_len", irep_idt(std::to_string(ref2.byte_len))); - return heap_append; - } case expr2t::heap_contains_id: { const heap_contains2t &ref2 = to_heap_contains2t(ref);