Merge pull request #6835 from thomasspriggs/tas/smt_object_size

Add support for object_size expressions to incremental SMT solving

Author: thomasspriggs

regression/cbmc-incr-smt2/pointers/object_size.c

@@ -0,0 +1,17 @@
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x;
+  uint32_t y;
+  bool nondet_bool1;
+  void *ptr = nondet_bool1 ? (&x) : (&y);
+  size_t size = __CPROVER_OBJECT_SIZE(ptr);
+  __CPROVER_assert(size == 2 || size == 4, "Expected int sizes.");
+  __CPROVER_assert(size == 2, "Size is always 2. (Can be disproved.)");
+  __CPROVER_assert(size == 4, "Size is always 4. (Can be disproved.)");
+  size_t null_size = __CPROVER_OBJECT_SIZE(NULL);
+  __CPROVER_assert(null_size == 254, "Size of NULL.");
+}

regression/cbmc-incr-smt2/pointers/object_size.desc

@@ -0,0 +1,17 @@
+CORE
+object_size.c
+--trace
+line 12 Expected int sizes\.: SUCCESS
+line 13 Size is always 2\. \(Can be disproved\.\): FAILURE
+line 14 Size is always 4\. \(Can be disproved\.\): FAILURE
+line 16 Size of NULL\.: FAILURE
+size=2ul
+size=4ul
+null_size=0ul
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the model of object_size can take only the expected values in the case
+where the pointer it is given may point to one of two objects. Test that the
+size of the null object is zero.

src/solvers/Makefile

@@ -201,6 +201,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_index.cpp \
       smt2_incremental/smt_logics.cpp \
+      smt2_incremental/smt_object_size.cpp \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_response_validation.cpp \
       smt2_incremental/smt_responses.cpp \

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1238,11 +1238,18 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const object_size_exprt &object_size,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const smt_object_sizet::make_applicationt &call_object_size)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for object_size expression: " +
-    object_size.pretty());
+  const smt_termt &pointer = converted.at(object_size.pointer());
+  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 call_object_size(
+    std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
+      pointer_width - 1,
+      pointer_width - config.bv_encoding.object_bits)(pointer)});
 }
 
 static smt_termt
@@ -1291,7 +1298,8 @@ static smt_termt convert_expr_to_smt(
 static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted,
-  const smt_object_mapt &object_map)
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &call_object_size)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
@@ -1589,7 +1597,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
   }
   if(const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    return convert_expr_to_smt(*object_size, converted);
+    return convert_expr_to_smt(*object_size, converted, call_object_size);
   }
   if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
   {
@@ -1647,8 +1655,10 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
 }
 #endif
 
-smt_termt
-convert_expr_to_smt(const exprt &expr, const smt_object_mapt &object_map)
+smt_termt convert_expr_to_smt(
+  const exprt &expr,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
   static bool in_conversion = false;
@@ -1665,8 +1675,8 @@ convert_expr_to_smt(const exprt &expr, const smt_object_mapt &object_map)
     const auto find_result = sub_expression_map.find(expr);
     if(find_result != sub_expression_map.cend())
       return;
-    smt_termt term =
-      dispatch_expr_to_smt_conversion(expr, sub_expression_map, object_map);
+    smt_termt term = dispatch_expr_to_smt_conversion(
+      expr, sub_expression_map, object_map, object_size);
     sub_expression_map.emplace_hint(find_result, expr, std::move(term));
   });
   return std::move(sub_expression_map.at(expr));

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -4,6 +4,7 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
 
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 
@@ -16,7 +17,9 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
 
 /// \brief Converts the \p expression to an smt encoding of the same expression
 ///   stored as term ast (abstract syntax tree).
-smt_termt
-convert_expr_to_smt(const exprt &expression, const smt_object_mapt &object_map);
+smt_termt convert_expr_to_smt(
+  const exprt &expression,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/object_tracking.cpp

@@ -2,6 +2,7 @@
 
 #include "object_tracking.h"
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_code.h>
@@ -42,6 +43,7 @@ static decision_procedure_objectt make_null_object()
   decision_procedure_objectt 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());
   return null_object;
 }
 
@@ -64,10 +66,12 @@ void track_expression_objects(
       const auto find_result = object_map.find(object_base);
       if(find_result != object_map.cend())
         return;
+      const auto size = size_of_expr(object_base.type(), ns);
+      INVARIANT(size, "Objects are expected to have well defined size");
       decision_procedure_objectt object;
       object.base_expression = object_base;
       object.unique_id = object_map.size();
-      object.size = size_of_expr(object_base.type(), ns);
+      object.size = *size;
       object_map.emplace_hint(find_result, object_base, std::move(object));
     });
 }

src/solvers/smt2_incremental/object_tracking.h

@@ -1,5 +1,33 @@
 // Author: Diffblue Ltd.
 
+/// \file
+/// Data structures and algorithms used by smt2_incremental_decision_proceduret
+/// to track data about the objects which pointers point to. An object here
+/// is the whole of an allocated block of memory. Objects in this sense have
+/// no sub objects; only offsets. Valid examples of objects include -
+///  * Primitives stored on the stack such as `int foo;`.
+///  * Pointer primitives stored on the stack such as `int *sam;`.
+///  * The entirety of a struct stored on the stack such as -
+///    `struct bart{int eggs, int ham} bar;`
+///  * The entirety of an array stored on the stack such as `int green[20];`
+///  * The memory allocated by a malloc call - `malloc(20)`.
+/// Examples of things / expressions which are not objects -
+///  * A pointer to a primitive stored on the stack, such as `&foo` or `&sam`.
+///    The value of these pointers encodes the combination of the unique object
+///    identifier of `foo` / `sam` objects and a (zero) offset, but these
+///    pointer values / memory addresses are not in themselves objects, although
+///    the values may be stored in another object. This is a distinction between
+///    values and the objects which contain them.
+///  * A field within a struct, such as `bar.ham` from the previous example. A
+///    pointer to this field is an offset into the base `bar` object.
+///  * A pointer to element within an array, such as `&(green[5])`. A pointer to
+///    an element in this example is an offset into the base `int green[20]`
+///    object.
+/// \note
+/// The functionality in this file is intended to cover tracking objects and
+/// their sizes only. It does not track anything to do with the offsets into
+/// objects or the SMT encodings of objects / offsets / pointers.
+
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
 
@@ -17,7 +45,7 @@ struct decision_procedure_objectt
   /// Number which uniquely identifies this particular object.
   std::size_t unique_id;
   /// Expression which evaluates to the size of the object in bytes.
-  optionalt<exprt> size;
+  exprt size;
 };
 
 /// The model of addresses we use consists of a unique object identifier and an

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -139,6 +139,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_quantifier_free_uninterpreted_functions_bit_vectorst{}});
+  solver_process->send(object_size_function.declaration);
 }
 
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
@@ -162,7 +163,8 @@ smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   track_expression_objects(expr, ns, object_map);
-  return ::convert_expr_to_smt(expr, object_map);
+  return ::convert_expr_to_smt(
+    expr, object_map, object_size_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -205,7 +207,8 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         objects_are_already_tracked(expr, object_map),
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
-      descriptor = ::convert_expr_to_smt(expr, object_map);
+      descriptor = ::convert_expr_to_smt(
+        expr, object_map, object_size_function.make_application);
     }
     else
     {
@@ -320,9 +323,26 @@ static decision_proceduret::resultt lookup_decision_procedure_result(
   UNREACHABLE;
 }
 
+void smt2_incremental_decision_proceduret::define_object_sizes()
+{
+  object_size_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])
+      continue;
+    else
+      object_size_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)));
+  }
+}
+
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
+  define_object_sizes();
   const smt_responset result =
     get_response_to_command(*solver_process, smt_check_sat_commandt{});
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -10,6 +10,7 @@
 #include <util/std_expr.h>
 
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
 
@@ -60,6 +61,8 @@ class smt2_incremental_decision_proceduret final
   /// \brief Add objects in \p expr to object_map if needed and convert to smt.
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
+  /// Sends the solver the definitions of the object sizes.
+  void define_object_sizes();
 
   const namespacet &ns;
 
@@ -84,6 +87,8 @@ class smt2_incremental_decision_proceduret final
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_identifiers;
   smt_object_mapt object_map;
+  std::vector<bool> object_size_defined;
+  smt_object_sizet object_size_function;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

src/solvers/smt2_incremental/smt_object_size.cpp

@@ -0,0 +1,38 @@
+// Author: Diffblue Ltd.
+
+#include "smt_object_size.h"
+
+#include <util/c_types.h>
+#include <util/config.h>
+
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_sorts.h>
+
+static smt_declare_function_commandt make_object_size_function_declaration()
+{
+  return smt_declare_function_commandt{
+    smt_identifier_termt{
+      "size_of_object", convert_type_to_smt_sort(size_type())},
+    {smt_bit_vector_sortt{config.bv_encoding.object_bits}}};
+}
+
+smt_object_sizet::smt_object_sizet()
+  : declaration{make_object_size_function_declaration()},
+    make_application{smt_command_functiont{declaration}}
+{
+}
+
+smt_commandt smt_object_sizet::make_definition(
+  const std::size_t unique_id,
+  smt_termt size) const
+{
+  const auto id_sort =
+    declaration.parameter_sorts().at(0).get().cast<smt_bit_vector_sortt>();
+  INVARIANT(id_sort, "Object identifiers are expected to have bit vector sort");
+  const auto bit_vector_of_id =
+    smt_bit_vector_constant_termt{unique_id, *id_sort};
+  return smt_assert_commandt{smt_core_theoryt::equal(
+    make_application(std::vector<smt_termt>{bit_vector_of_id}),
+    std::move(size))};
+}