Merge pull request #7313 from thomasspriggs/tas/dynamic_object

Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.desc

@@ -0,0 +1,11 @@
+CORE
+assert_dynamic.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion __CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE
+make_dynamic\=FALSE
+^EXIT=10$
+^SIGNAL=0$
+--
+make_dynamic\=TRUE
+--

regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(!__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.desc

@@ -0,0 +1,11 @@
+CORE
+assert_not_dynamic.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE
+make_dynamic\=TRUE
+^EXIT=10$
+^SIGNAL=0$
+--
+make_dynamic\=FALSE
+--

regression/cbmc-incr-smt2/dynamic-memory/valid.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(make_dynamic || !__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/valid.desc

@@ -0,0 +1,10 @@
+CORE
+valid.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion make_dynamic \|\| \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: SUCCESS
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+--

src/solvers/Makefile

@@ -203,6 +203,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
       smt2_incremental/type_size_mapping.cpp \
+      smt2_incremental/smt_is_dynamic_object.cpp \
       smt2_incremental/smt_object_size.cpp \
       smt2_incremental/smt_response_validation.cpp \
       smt2_incremental/smt_solver_process.cpp \

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1042,11 +1042,18 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const is_dynamic_object_exprt &is_dynamic_object,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is dynamic object expression: " +
-    is_dynamic_object.pretty());
+  const smt_termt &pointer = converted.at(is_dynamic_object.address());
+  const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
+  const std::size_t pointer_width = pointer_sort->bit_width();
+  return apply_is_dynamic_object(
+    std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
+      pointer_width - 1,
+      pointer_width - config.bv_encoding.object_bits)(pointer)});
 }
 
 static smt_termt convert_expr_to_smt(
@@ -1458,7 +1465,8 @@ static smt_termt dispatch_expr_to_smt_conversion(
   const sub_expression_mapt &converted,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &call_object_size)
+  const smt_object_sizet::make_applicationt &call_object_size,
+  const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
@@ -1660,7 +1668,8 @@ static smt_termt dispatch_expr_to_smt_conversion(
     const auto is_dynamic_object =
       expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
   {
-    return convert_expr_to_smt(*is_dynamic_object, converted);
+    return convert_expr_to_smt(
+      *is_dynamic_object, converted, apply_is_dynamic_object);
   }
   if(
     const auto is_invalid_pointer =
@@ -1837,7 +1846,8 @@ smt_termt convert_expr_to_smt(
   const exprt &expr,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &object_size)
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
   static bool in_conversion = false;
@@ -1856,7 +1866,12 @@ smt_termt convert_expr_to_smt(
     if(find_result != sub_expression_map.cend())
       return;
     smt_termt term = dispatch_expr_to_smt_conversion(
-      expr, sub_expression_map, object_map, pointer_sizes, object_size);
+      expr,
+      sub_expression_map,
+      object_map,
+      pointer_sizes,
+      object_size,
+      is_dynamic_object);
     sub_expression_map.emplace_hint(find_result, expr, std::move(term));
   });
   return std::move(sub_expression_map.at(lowered_expr));

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -6,6 +6,7 @@
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 
@@ -27,6 +28,7 @@ smt_termt convert_expr_to_smt(
   const exprt &expression,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &object_size);
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

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>
@@ -49,6 +51,7 @@ static decision_procedure_objectt make_null_object()
   null_object.unique_id = 0;
   null_object.base_expression = null_pointer_exprt{pointer_type(void_type())};
   null_object.size = from_integer(0, size_type());
+  null_object.is_dynamic = false;
   return null_object;
 }
 
@@ -60,6 +63,7 @@ static decision_procedure_objectt make_invalid_pointer_object()
   invalid_pointer_object.unique_id = 1;
   invalid_pointer_object.base_expression = make_invalid_pointer_expr();
   invalid_pointer_object.size = from_integer(0, size_type());
+  invalid_pointer_object.is_dynamic = false;
   return invalid_pointer_object;
 }
 
@@ -77,6 +81,23 @@ 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.
+  const bool dynamic_type = object.type().get_bool(ID_C_dynamic);
+  if(dynamic_type)
+    return true;
+  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 symbol_is_dynamic;
+}
+
 void track_expression_objects(
   const exprt &expression,
   const namespacet &ns,
@@ -93,6 +114,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

@@ -43,9 +43,11 @@ struct decision_procedure_objectt
   /// to deferencing a pointer to this object with a zero offset.
   exprt base_expression;
   /// Number which uniquely identifies this particular object.
-  std::size_t unique_id;
+  std::size_t unique_id = 0;
   /// 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 = false;
 };
 
 /// The model of addresses we use consists of a unique object identifier and an

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -255,6 +255,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
   solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
   solver_process->send(object_size_function.declaration);
+  solver_process->send(is_dynamic_object_function.declaration);
 }
 
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
@@ -321,12 +322,14 @@ smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
     ns,
     pointer_sizes_map,
     object_map,
-    object_size_function.make_application);
+    object_size_function.make_application,
+    is_dynamic_object_function.make_application);
   return ::convert_expr_to_smt(
     substituted,
     object_map,
     pointer_sizes_map,
-    object_size_function.make_application);
+    object_size_function.make_application,
+    is_dynamic_object_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -376,7 +379,8 @@ array_exprt smt2_incremental_decision_proceduret::get_expr(
           from_integer(index, index_type),
           object_map,
           pointer_sizes_map,
-          object_size_function.make_application)),
+          object_size_function.make_application,
+          is_dynamic_object_function.make_application)),
       type.element_type()));
   }
   return array_exprt{elements, type};
@@ -442,7 +446,8 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         expr,
         object_map,
         pointer_sizes_map,
-        object_size_function.make_application);
+        object_size_function.make_application,
+        is_dynamic_object_function.make_application);
     }
     else
     {
@@ -548,26 +553,28 @@ static decision_proceduret::resultt lookup_decision_procedure_result(
   UNREACHABLE;
 }
 
-void smt2_incremental_decision_proceduret::define_object_sizes()
+void smt2_incremental_decision_proceduret::define_object_properties()
 {
-  object_size_defined.resize(object_map.size());
+  object_properties_defined.resize(object_map.size());
   for(const auto &key_value : object_map)
   {
     const decision_procedure_objectt &object = key_value.second;
-    if(object_size_defined[object.unique_id])
+    if(object_properties_defined[object.unique_id])
       continue;
     else
-      object_size_defined[object.unique_id] = true;
+      object_properties_defined[object.unique_id] = true;
     define_dependent_functions(object.size);
     solver_process->send(object_size_function.make_definition(
       object.unique_id, convert_expr_to_smt(object.size)));
+    solver_process->send(is_dynamic_object_function.make_definition(
+      object.unique_id, object.is_dynamic));
   }
 }
 
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  define_object_sizes();
+  define_object_properties();
   const smt_responset result = get_response_to_command(
     *solver_process, smt_check_sat_commandt{}, identifier_table);
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -11,6 +11,7 @@
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
@@ -92,8 +93,9 @@ class smt2_incremental_decision_proceduret final
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
   void define_index_identifiers(const exprt &expr);
-  /// Sends the solver the definitions of the object sizes.
-  void define_object_sizes();
+  /// Sends the solver the definitions of the object sizes and dynamic memory
+  /// statuses.
+  void define_object_properties();
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but
@@ -149,16 +151,21 @@ class smt2_incremental_decision_proceduret final
   /// This map is used to track object related state. See documentation in
   /// object_tracking.h for details.
   smt_object_mapt object_map;
-  /// The size of each object is separately defined as a pre-solving step.
-  /// `object_size_defined[object ID]` is set to true for objects where the size
-  /// has been defined. This is used to avoid defining the size of the same
-  /// object multiple times in the case where multiple rounds of solving are
-  /// carried out.
-  std::vector<bool> object_size_defined;
+  /// The size of each object and the dynamic object stus is separately defined
+  /// as a pre-solving step. `object_properties_defined[object ID]` is set to
+  /// true for objects where the size has been defined. This is used to avoid
+  /// defining the size of the same object multiple times in the case where
+  /// multiple rounds of solving are carried out.
+  std::vector<bool> object_properties_defined;
   /// Implementation of the SMT formula for the object size function. This is
   /// stateful because it depends on the configuration of the number of object
   /// bits and how many bits wide the size type is configured to be.
   smt_object_sizet object_size_function;
+  /// Implementation of the SMT formula for the dynamic object status lookup
+  /// function. This is stateful because it depends on the configuration of the
+  /// number of object bits and how many bits wide the size type is configured
+  /// to be.
+  smt_is_dynamic_objectt is_dynamic_object_function;
   /// Precalculated type sizes used for pointer arithmetic.
   type_size_mapt pointer_sizes_map;
 };