move region info to intheap type

src/goto-symex/builtin_functions.cpp

@@ -281,10 +281,7 @@ expr2tc goto_symext::symex_mem(
     symbol.mode = "C";
     new_context.add(symbol);
 
-    expr2tc rhs_heap = symbol2tc(heap_type, symbol.id);
-    guardt rhs_guard = cur_state->guard;
-
-    // set a location for new heap region
+    // create a new location for new heap region
     symbolt heap_region_loc;
     heap_region_loc.name = "heap_region_loc_"+ i2string(dynamic_counter);
 
@@ -301,6 +298,12 @@ expr2tc goto_symext::symex_mem(
     // use l2 symbol, do not need to be renamed
     cur_state->rename(rhs_base_loc);
 
+    // store base location in intheap type
+    _heap_type.location = rhs_base_loc;
+
+    expr2tc rhs_heap = symbol2tc(heap_type, symbol.id);
+    guardt rhs_guard = cur_state->guard;
+
     expr2tc rhs_region = heap_region2tc(heap_type, rhs_heap, rhs_base_loc);
 
     log_status("symex assign in symex_mem: allocated_heap = heaplet");
@@ -320,7 +323,7 @@ expr2tc goto_symext::symex_mem(
     );
 
     log_status("create valueset base loc symbol and assign");
-    symex_assign(code_assign2tc(lhs, locationof2tc(rhs_region)));
+    symex_assign(code_assign2tc(lhs, locationof2tc(rhs_heap)));
 
     return expr2tc();
   }
@@ -459,14 +462,12 @@ void goto_symext::symex_free(const expr2tc &expr)
     // set each heap region to empty, guarded by item.gurad
     for(auto const& item : internal_deref_items)
     {
-      assert(is_heap_region2t(item.object));
+      assert(is_intheap_type(item.object));
       log_status("free object guard");
       item.guard->dump();
-
-      const heap_region2t& heap_region = to_heap_region2t(item.object);
-      expr2tc free_heap = heap_region.flag;
+
       guardt g; g.add(item.guard);
-      symex_assign(code_assign2tc(free_heap, gen_emp()), false, g);
+      symex_assign(code_assign2tc(item.object, gen_emp()), false, g);
 
       // collect guards for deleting heap alloc size
       when = or2tc(when, item.guard);

src/goto-symex/dynamic_allocation.cpp

@@ -33,9 +33,15 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
       // Checking that the object is valid by heap_alloc_size
       log_status(" --- generate cond for checking heap region --- ");
       const valid_object2t &obj = to_valid_object2t(expr);
-      obj.dump();
-      const heap_region2t &valid_inner = to_heap_region2t(obj.value);
-      const intheap_type2t &_type = to_intheap_type(valid_inner.type);
+      const expr2tc &heap_region = obj.value;
+      if (!is_intheap_type(heap_region->type) ||
+          !to_intheap_type(heap_region->type).is_region)
+      {
+        log_error("Wrong object");
+        abort();
+      }
+
+      const intheap_type2t &_type = to_intheap_type(heap_region->type);
       // get alloc size heap
       expr2tc alloc_size_heap;
       migrate_expr(symbol_expr(*ns.lookup(alloc_size_heap_name)), alloc_size_heap);
@@ -44,7 +50,7 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
       expr2tc heap_contain =
         heap_contain2tc(
           alloc_size_heap,
-          points_to2tc(valid_inner.source_location, size)
+          points_to2tc(_type.location, size)
         );
       expr = heap_contain;
       log_status(" --- generate cond for checking heap region --- ");

src/goto-symex/goto_symex.h

@@ -969,8 +969,8 @@ class symex_dereference_statet : public dereference_callbackt
   dump_internal_state(const std::list<struct internal_item> &data) override;
   bool is_live_variable(const expr2tc &sym) override;
 
-  void update_heap_type(const expr2tc &flag) override;
-  void update_heap_type_rec(expr2tc &expr, const symbol2t &flag) override;
+  void update_heap_type(const intheap_type2t &type) override;
+  void update_heap_type_rec(expr2tc &expr, const intheap_type2t &type) override;
   std::string get_nondet_id(std::string prefix = "") override;
   irep_idt get_alloc_size_heap_name() override;
 };

src/goto-symex/goto_symex_state.cpp

@@ -67,9 +67,7 @@ void goto_symex_statet::initialize(
 bool goto_symex_statet::constant_propagation(const expr2tc &expr) const
 {
   // SLHV propagation
-  if (is_constant_intheap2t(expr) ||
-      is_constant_intloc2t(expr) ||
-      is_heap_region2t(expr))
+  if (is_constant_intheap2t(expr) || is_constant_intloc2t(expr))
     return true;
 
   if (is_locadd2t(expr))
@@ -210,13 +208,6 @@ void goto_symex_statet::assignment(expr2tc &lhs, const expr2tc &rhs)
   expr2tc l1_lhs = lhs;
 
   expr2tc const_value = constant_propagation(rhs) ? rhs : expr2tc();
-
-  // Each heap region has only one unique flag that does not change
-  // during its lifetime. The l1 version of flag is the representation.
-  // For constant_propagation, all heap regions should hold their flag. 
-  if (!is_nil_expr(const_value) && is_heap_region2t(const_value))
-    level2.get_original_name(to_heap_region2t(const_value).flag);
-
   level2.make_assignment(lhs, const_value, rhs);
 
   if (use_value_set)
@@ -230,6 +221,7 @@ void goto_symex_statet::assignment(expr2tc &lhs, const expr2tc &rhs)
     l1_lhs->dump();
     log_status("#####");
     value_set.assign(l1_lhs, l1_rhs);
+    log_status("update value set done!!!!");
   }
 }
 
@@ -263,7 +255,8 @@ void goto_symex_statet::rename_type(expr2tc &expr)
 void goto_symex_statet::rename(expr2tc &expr)
 {
   // rename all the symbols with their last known value
-  if (is_nil_expr(expr))
+  if (is_nil_expr(expr) ||
+      is_heap_region2t(expr))
     return;
 
   rename_type(expr);
@@ -280,15 +273,6 @@ void goto_symex_statet::rename(expr2tc &expr)
     address_of2t &addrof = to_address_of2t(expr);
     rename_address(addrof.ptr_obj);
   }
-  else  if (is_heap_region2t(expr))
-  {
-    heap_region2t &heap_region = to_heap_region2t(expr);
-    rename(heap_region.source_location);
-    // Return to l1 name first
-    level2.get_original_name(heap_region.flag);
-    // Get the newest l2 name
-    level2.get_ident_name(heap_region.flag);
-  }
   else
   {
     // do this recursively

src/goto-symex/slice.cpp

@@ -15,19 +15,14 @@ bool symex_slicet::get_symbols(const expr2tc &expr)
   // locationof only has heap_region as oprend
   // the location of heap_region is completely fresh
   // and is not being used in symbolic execution
-  if (is_locationof2t(expr)) return false;
+  if (is_locationof2t(expr) || is_heap_region2t(expr)) return false;
 
-  if (is_heap_region2t(expr))
-    return get_symbols<Add>(to_heap_region2t(expr).flag);
-  else
-  {
-    // Recursively look if any of the operands has a inner symbol
-    expr->foreach_operand([this, &res](const expr2tc &e) {
-      if (!is_nil_expr(e))
-        res |= get_symbols<Add>(e);
-      return res;
-    });
-  }
+  // Recursively look if any of the operands has a inner symbol
+  expr->foreach_operand([this, &res](const expr2tc &e) {
+    if (!is_nil_expr(e))
+      res |= get_symbols<Add>(e);
+    return res;
+  });
 
   if (!is_symbol2t(expr))
     return res;

src/goto-symex/symex_assign.cpp

@@ -294,6 +294,7 @@ void goto_symext::symex_assign_rec(
   {
     log_status("symex_assign_symbol");
     symex_assign_symbol(lhs, full_lhs, rhs, full_rhs, guard, hidden);
+    log_status("symex_assign_symbol done!!!");
   } 
   else if (is_index2t(lhs))
   {
@@ -349,10 +350,7 @@ void goto_symext::symex_assign_rec(
   {
     log_status("symex_assign_fieldof");
     symex_assign_fieldof(lhs, full_lhs, rhs, full_rhs, guard, hidden);
-  }
-  else if (is_heap_region2t(lhs))
-  {
-    log_status("symex_assign_heap_region");
+    log_status("symex_assign_fieldof done!!!");
   }
   else
   {
@@ -397,6 +395,8 @@ void goto_symext::symex_assign_symbol(
 
   cur_state->assignment(renamed_lhs, rhs);
 
+  log_status("cur state assignment done!!!");
+
   // Special case when the lhs is an array access, we need to get the
   // right symbol for the index
   expr2tc new_lhs = full_lhs;
@@ -906,18 +906,13 @@ void goto_symext::symex_assign_fieldof(
   assert(is_scalar_type(rhs));
 
   const fieldof2t& fieldof = to_fieldof2t(lhs);
-  const heap_region2t &heap_region = to_heap_region2t(fieldof.source_heap);
+  const expr2tc &heap_region = fieldof.source_heap;
   const expr2tc &field = fieldof.operand;
 
   expr2tc update_heap =
-    heap_update2tc(heap_region.type, fieldof.source_heap, field, rhs);
+    heap_update2tc(heap_region->type, heap_region, field, rhs);
 
-  symex_assign_rec(
-    heap_region.flag,
-    fieldof.source_heap,
-    update_heap,
-    update_heap,
-    guard, hidden);
+  symex_assign_rec(heap_region, full_lhs, update_heap, full_rhs, guard, hidden);
 }
 
 void goto_symext::replace_nondet(expr2tc &expr)

src/goto-symex/symex_dereference.cpp

@@ -166,82 +166,56 @@ bool symex_dereference_statet::is_live_variable(const expr2tc &symbol)
   return false;
 }
 
-void symex_dereference_statet::update_heap_type(const expr2tc &flag)
+void symex_dereference_statet::update_heap_type(const intheap_type2t &type)
 {
-  if (!is_symbol2t(flag))
+  if (is_nil_expr(to_intheap_type(type).location))
   {
-    log_error("Wrong flag!!!!");
+    log_error("Wrong type!!!!");
     abort();
   }
 
-  log_status("begin update heap type");
-  flag->dump();
-
-  // Each heap region has a unique L0 name
-  expr2tc l0_flag = flag;
-  goto_symex.cur_state->get_original_name(l0_flag);
-  const symbol2t l0_sym = to_symbol2t(l0_flag);
-
-  l0_flag->dump();
-
   // update value set
   value_sett& value_set = goto_symex.cur_state->value_set;
   unsigned int n = value_set.object_numbering.size();
   for(unsigned int i = 0; i < n; i++)
-    update_heap_type_rec(value_set.object_numbering[i], l0_sym);
-
-
-  log_status("finishing update value set");
+    update_heap_type_rec(value_set.object_numbering[i], type);
 
   // update eq system
   std::shared_ptr<symex_target_equationt> eq =
     std::dynamic_pointer_cast<symex_target_equationt>(goto_symex.target);
   for(auto& ssa_step : eq->SSA_steps)
   {
-    update_heap_type_rec(ssa_step.guard, l0_sym);
-    update_heap_type_rec(ssa_step.rhs, l0_sym);
-    update_heap_type_rec(ssa_step.cond, l0_sym);
+    update_heap_type_rec(ssa_step.guard, type);
+    update_heap_type_rec(ssa_step.rhs, type);
+    update_heap_type_rec(ssa_step.cond, type);
   }
-
-  log_status("finishing replace");
 }
 
 void symex_dereference_statet::update_heap_type_rec(
-  expr2tc &expr, const symbol2t &flag)
+  expr2tc &expr, const intheap_type2t &type)
 {
   if (is_nil_expr(expr)) return;
-  log_status("update type of :");
-  expr->dump();
-  if (is_symbol2t(expr))
+  if (is_intheap_type(expr))
   {
-    // update heap variable
-    expr2tc l0_sym = expr;
-    goto_symex.cur_state->get_original_name(l0_sym);
+    intheap_type2t &_type = to_intheap_type(expr->type);
 
-    if (flag.get_symbol_name() == to_symbol2t(l0_sym).get_symbol_name())
-      expr->type = flag.type;
-  }
-  else if (is_heap_region2t(expr))
-  {
-    heap_region2t &heap_region = to_heap_region2t(expr);
-
-    expr2tc l0_flag = heap_region.flag;
-    goto_symex.cur_state->get_original_name(l0_flag);
+    if (is_nil_expr(_type.location)) return;
 
-    l0_flag->dump();
-
-    if (flag.get_symbol_name() ==
-        to_symbol2t(l0_flag).get_symbol_name()) 
+    if (to_symbol2t(_type.location).get_symbol_name() ==
+        to_symbol2t(type.location).get_symbol_name())
+      expr->type = intheap_type2tc(type);
+
+    if (is_heap_region2t(expr))
     {
-      heap_region.type = flag.type;
-      update_heap_type_rec(heap_region.flag, flag);
+      heap_region2t &heap_region = to_heap_region2t(expr);
+      update_heap_type_rec(heap_region.flag, type);
     }
   }
   else
   {
-    expr->Foreach_operand([this, &flag](expr2tc& e){
+    expr->Foreach_operand([this, &type](expr2tc& e){
       if (!is_nil_expr(e))
-        update_heap_type_rec(e, flag);
+        update_heap_type_rec(e, type);
     });
   }
 }

src/goto-symex/symex_main.cpp

@@ -1226,8 +1226,7 @@ void goto_symext::add_memory_leak_checks()
     log_status(" ----------- [memleak encoding]----------- ");
     for (auto const &it : dynamic_memory){
       log_status("allocated object {}: ", it.name);
-      expr2tc obj_flag = flagof2tc(it.obj);
-      expr2tc deallocated = equality2tc(obj_flag, gen_emp());
+      expr2tc deallocated = equality2tc(it.obj, gen_emp());
       expr2tc when = it.alloc_guard.as_expr();
       expr2tc cond = implies2tc(when, deallocated);
       cur_state->rename(cond);

src/irep2/irep2.h

@@ -107,7 +107,6 @@
   BOOST_PP_LIST_CONS(uplus,                                                    \
   BOOST_PP_LIST_CONS(locadd,                                                   \
   BOOST_PP_LIST_CONS(heap_region,                                              \
-  BOOST_PP_LIST_CONS(flagof,                                                   \
   BOOST_PP_LIST_CONS(locationof,                                               \
   BOOST_PP_LIST_CONS(fieldof,                                                  \
   BOOST_PP_LIST_CONS(heap_update,                                              \
@@ -154,7 +153,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,                                                     \

src/irep2/irep2_expr.cpp

@@ -78,7 +78,6 @@ static const char *expr_names[] = {
   "uplus",
   "locadd",
   "heap_region",
-  "flagof",
   "locationof",
   "fieldof",
   "heap_update",

src/irep2/irep2_expr.h

@@ -1704,7 +1704,6 @@ irep_typedefs(points_to, points_to_data);
 irep_typedefs(uplus, uplus_data);
 irep_typedefs(locadd, locadd_data);
 irep_typedefs(heap_region, heap_region_data);
-irep_typedefs(flagof, heap_ops);
 irep_typedefs(locationof, heap_ops);
 irep_typedefs(fieldof, heap_1op);
 irep_typedefs(heap_update, heap_2ops);
@@ -3231,18 +3230,6 @@ class heap_region2t : public heap_region_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
-class flagof2t : public flagof_expr_methods
-{
-public:
-  flagof2t(const expr2tc &source_region)
-    : flagof_expr_methods(get_intheap_type(), flagof_id, source_region)
-  {
-  }
-  flagof2t(const flagof2t &ref) = default;
-
-  static std::string field_names[esbmct::num_type_fields];
-};
-
 class locationof2t : public locationof_expr_methods
 {
 public: