Add support for mapping the sizes of expression subtypes in the new SMT backend.

This will be needed later to support pointer arithmetic.

Author: NlightNFotis

src/solvers/Makefile

@@ -196,6 +196,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
+      smt2_incremental/type_size_mapping.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -587,7 +587,8 @@ static optionalt<smt_termt> try_relational_conversion(
 
 static smt_termt convert_expr_to_smt(
   const plus_exprt &plus,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const type_size_mapt &pointer_sizes)
 {
   if(std::all_of(
        plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
@@ -606,7 +607,8 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const minus_exprt &minus,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const type_size_mapt &pointer_sizes)
 {
   const bool both_operands_bitvector =
     can_cast_type<integer_bitvector_typet>(minus.lhs().type()) &&
@@ -1299,6 +1301,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   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)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
@@ -1415,7 +1418,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
   }
   if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
   {
-    return convert_expr_to_smt(*plus, converted);
+    return convert_expr_to_smt(*plus, converted, pointer_sizes);
   }
   if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
   {
@@ -1658,6 +1661,7 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
 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)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
@@ -1676,7 +1680,7 @@ 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, object_size);
+      expr, sub_expression_map, object_map, pointer_sizes, 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

@@ -7,6 +7,7 @@
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
 
 class exprt;
 class typet;
@@ -20,6 +21,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
 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);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,13 +2,6 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
-#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
-#include <solvers/smt2_incremental/convert_expr_to_smt.h>
-#include <solvers/smt2_incremental/smt_commands.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
-#include <solvers/smt2_incremental/smt_responses.h>
-#include <solvers/smt2_incremental/smt_solver_process.h>
-#include <solvers/smt2_incremental/smt_terms.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
@@ -17,6 +10,15 @@
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_responses.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
+
 #include <stack>
 
 /// Issues a command to the solving process which is expected to optionally
@@ -163,8 +165,14 @@ smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   track_expression_objects(expr, ns, object_map);
+  associate_pointer_sizes(
+    expr,
+    ns,
+    pointer_sizes_map,
+    object_map,
+    object_size_function.make_application);
   return ::convert_expr_to_smt(
-    expr, object_map, object_size_function.make_application);
+    expr, object_map, pointer_sizes_map, object_size_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -208,7 +216,10 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
       descriptor = ::convert_expr_to_smt(
-        expr, object_map, object_size_function.make_application);
+        expr,
+        object_map,
+        pointer_sizes_map,
+        object_size_function.make_application);
     }
     else
     {

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -12,6 +12,7 @@
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
 
 #include <memory>
@@ -89,6 +90,7 @@ class smt2_incremental_decision_proceduret final
   smt_object_mapt object_map;
   std::vector<bool> object_size_defined;
   smt_object_sizet object_size_function;
+  type_size_mapt pointer_sizes_map;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

src/solvers/smt2_incremental/type_size_mapping.cpp

@@ -0,0 +1,51 @@
+// Author: Diffblue Ltd.
+
+#include "type_size_mapping.h"
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/invariant.h>
+#include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
+
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
+
+void associate_pointer_sizes(
+  const exprt &expression,
+  const namespacet &ns,
+  type_size_mapt &type_size_map,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size)
+{
+  expression.visit_pre(
+    [&](const exprt &sub_expression)
+    {
+      if(
+        const auto &pointer_type =
+          type_try_dynamic_cast<pointer_typet>(sub_expression.type()))
+      {
+        const auto find_result = type_size_map.find(pointer_type->base_type());
+        if(find_result != type_size_map.cend())
+          return;
+        exprt pointer_size_expr;
+        // There's a special case for a pointer subtype here: the case where the pointer is
+        // `void *`. This means that we don't know the underlying base type, so we're just
+        // assigning a size expression value of 1 (given that this is going to be used in a
+        // multiplication and 1 is the identity value for multiplcation)
+        if(is_void_pointer(*pointer_type))
+        {
+          pointer_size_expr = from_integer(1, size_type());
+        }
+        else
+        {
+          auto pointer_size_opt = size_of_expr(pointer_type->base_type(), ns);
+          PRECONDITION(pointer_size_opt.has_value());
+          pointer_size_expr = pointer_size_opt.value();
+        }
+        auto pointer_size_term = convert_expr_to_smt(
+          pointer_size_expr, object_map, type_size_map, object_size);
+        type_size_map.emplace_hint(
+          find_result, pointer_type->base_type(), pointer_size_term);
+      }
+    });
+}

src/solvers/smt2_incremental/type_size_mapping.h

@@ -0,0 +1,37 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Utilities for making a map of types to associated sizes.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_SIZE_MAPPING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_SIZE_MAPPING_H
+
+#include <util/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 <unordered_map>
+
+using type_size_mapt = std::unordered_map<typet, smt_termt, irep_full_hash>;
+
+/// This function populates the (pointer) type -> size map.
+/// \param expression: the expression we're building the map for.
+/// \param ns:
+///   A namespace - passed to size_of_expr to lookup type symbols in case the
+///   pointers have type `tag_typet`, rather than a more completely defined type.
+/// \param type_size_map:
+///   A map of types to terms expressing the size of the type (in bytes). This
+///   function adds new entries to the map for instances of pointer.base_type()
+///   from \p expression which are not already keys in the map.
+/// \param object_map: passed through to convert_expr_to_smt
+/// \param object_size: passed through to convert_expr_to_smt
+void associate_pointer_sizes(
+  const exprt &expression,
+  const namespacet &ns,
+  type_size_mapt &type_size_map,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size);
+
+#endif

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -14,6 +14,7 @@
 
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/pointer_size_mapping.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
@@ -57,6 +58,7 @@ struct expr_to_smt_conversion_test_environmentt
 
   smt_object_mapt object_map;
   smt_object_sizet object_size_function;
+  pointer_size_mapt pointer_sizes;
 
 private:
   // This is private to ensure the above make() function is used to make
@@ -88,7 +90,10 @@ smt_termt
 expr_to_smt_conversion_test_environmentt::convert(const exprt &expression) const
 {
   return convert_expr_to_smt(
-    expression, object_map, object_size_function.make_application);
+    expression,
+    object_map,
+    pointer_sizes,
+    object_size_function.make_application);
 }
 
 TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")