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/pointer_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 pointer_size_mapt &pointer_sizes)
 {
   if(std::all_of(
        plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
@@ -1299,6 +1300,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted,
   const smt_object_mapt &object_map,
+  const pointer_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 +1417,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 +1660,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 pointer_size_mapt &pointer_sizes,
   const smt_object_sizet::make_applicationt &object_size)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
@@ -1676,7 +1679,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

@@ -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/pointer_size_mapping.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
@@ -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 pointer_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/pointer_size_mapping.cpp

@@ -0,0 +1,60 @@
+// Author: Diffblue Ltd.
+
+#include "pointer_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,
+  pointer_size_mapt &pointer_size_map,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size)
+{
+  if(std::any_of(
+       expression.operands().cbegin(),
+       expression.operands().cend(),
+       [](exprt operand)
+       { return can_cast_type<pointer_typet>(operand.type()); }))
+  {
+    exprt pointer;
+    for(auto &operand : expression.operands())
+    {
+      if(can_cast_type<pointer_typet>(operand.type()))
+      {
+        pointer = operand;
+      }
+    }
+
+    auto pointer_type = to_pointer_type(pointer.type());
+    auto pointer_base_type = pointer_type.base_type();
+    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_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, pointer_size_map, object_size);
+
+    const auto find_result = pointer_size_map.find(pointer_base_type);
+    if(find_result != pointer_size_map.cend())
+      return;
+    pointer_size_map.emplace_hint(
+      find_result, pointer_base_type, pointer_size_term);
+  }
+}

src/solvers/smt2_incremental/pointer_size_mapping.h

@@ -0,0 +1,33 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Utilities for making a map of types to associated sizes.
+
+#ifndef CPROVER_SOLVERS_SMT2_POINTER_SIZE_TRACKING_H
+#define CPROVER_SOLVERS_SMT2_POINTER_SIZE_TRACKING_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 pointer_size_mapt = std::unordered_map<typet, smt_termt, irep_full_hash>;
+
+/// Establish pointer-sizes map for all pointers present in the
+/// expression argument.
+/// \param expression: the expression we're building the map for.
+/// \param ns: a namespace - passed to size_of_expr to find expression sizes.
+/// \param pointer_size_map: the map containing the pointer.base_type() -> size (in bytes) mappings.
+/// \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,
+  pointer_size_mapt &pointer_size_map,
+  const smt_object_mapt &object_map,
+  const smt_object_sizet::make_applicationt &object_size);
+
+#endif

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/pointer_size_mapping.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 <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

@@ -10,6 +10,7 @@
 #include <util/std_expr.h>
 
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/pointer_size_mapping.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
@@ -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;
+  pointer_size_mapt pointer_sizes_map;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

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]")