Add is_dynamic to object map

So that the information is available in subsequent conversions.

Author: thomasspriggs

src/solvers/smt2_incremental/object_tracking.cpp

@@ -5,6 +5,8 @@
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
+#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
@@ -77,6 +79,21 @@ smt_object_mapt initial_smt_object_map()
   return object_map;
 }
 
+/// This function returns true for heap allocated objects or false for stack
+/// allocated objects.
+static bool is_dynamic(const exprt &object)
+{
+  // This check corresponds to the symbols created in
+  // `goto_symext::symex_allocate`, which implements the `__CPROVER_allocate`
+  // intrinsic function used by the standard library models.
+  bool dynamic_type = object.type().get_bool(ID_C_dynamic);
+  const auto symbol = expr_try_dynamic_cast<symbol_exprt>(object);
+  bool symbol_is_dynamic =
+    symbol &&
+    has_prefix(id2string(symbol->get_identifier()), SYMEX_DYNAMIC_PREFIX);
+  return dynamic_type || symbol_is_dynamic;
+}
+
 void track_expression_objects(
   const exprt &expression,
   const namespacet &ns,
@@ -93,6 +110,7 @@ void track_expression_objects(
       object.base_expression = object_base;
       object.unique_id = object_map.size();
       object.size = *size;
+      object.is_dynamic = is_dynamic(object_base);
       object_map.emplace_hint(find_result, object_base, std::move(object));
     });
 }

src/solvers/smt2_incremental/object_tracking.h

@@ -46,6 +46,8 @@ struct decision_procedure_objectt
   std::size_t unique_id;
   /// Expression which evaluates to the size of the object in bytes.
   exprt size;
+  /// This is true for heap allocated objects and false for stack allocated.
+  bool is_dynamic;
 };
 
 /// The model of addresses we use consists of a unique object identifier and an

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -4,6 +4,7 @@
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/namespace.h>
+#include <util/pointer_predicates.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -199,3 +200,32 @@ TEST_CASE("Tracking object sizes.", "[core][smt2_incremental]")
   REQUIRE(object != object_map.end());
   REQUIRE(object->second.size == expected_size);
 }
+
+static typet make_type_dynamic(typet base_type)
+{
+  base_type.set(ID_C_dynamic, true);
+  return base_type;
+}
+
+TEST_CASE("Tracking dynamic object status.", "[core][smt2_incremental]")
+{
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64();
+  smt_object_mapt object_map = initial_smt_object_map();
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  exprt base_object;
+  bool expected_dynamic_status;
+  using rowt =
+    std::pair<decltype(base_object), decltype(expected_dynamic_status)>;
+  std::tie(base_object, expected_dynamic_status) = GENERATE_REF(
+    rowt{from_integer(0, unsignedbv_typet{(8)}), false},
+    rowt{symbol_exprt{"foo", bool_typet{}}, false},
+    rowt{symbol_exprt{SYMEX_DYNAMIC_PREFIX "bar", bool_typet{}}, true},
+    rowt{from_integer(42, make_type_dynamic(signedbv_typet{16})), true});
+  INFO("base_object is - " + base_object.pretty(1, 0));
+  track_expression_objects(address_of_exprt{base_object}, ns, object_map);
+  const auto object = object_map.find(base_object);
+  REQUIRE(object != object_map.end());
+  REQUIRE(object->second.is_dynamic == expected_dynamic_status);
+}