add heap free

SpencerL-Y · Jul 28, 2024 · e56a982 · e56a982
1 parent f5b3ed7
commit e56a982
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 12 deletions.
diff --git 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
@@ -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
@@ -1002,6 +1002,19 @@ class pointer_with_region_data : public expr2t
   typedef esbmct::expr2t_traits<pointer_with_region_loc_ptr_field, pointer_with_region_region_field> 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<expr2tc, heap_free_data, &heap_free_data::pwr> heap_free_data_pwr_field;
+  typedef esbmct::expr2t_traits<heap_free_data_pwr_field> 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
@@ -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
@@ -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
@@ -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);