Supply smt object size function to expr to smt conversion

Ready for converting object size expressions

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1291,7 +1291,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 &object_size)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
@@ -1647,8 +1648,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 +1668,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/smt2_incremental_decision_procedure.cpp

@@ -163,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)
@@ -206,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
     {

src/solvers/smt2_incremental/smt_object_size.h

@@ -17,9 +17,10 @@ struct smt_object_sizet final
   /// The command for declaring the object size function. The defined function
   /// takes a bit vector encoded unique object identifier and returns
   smt_declare_function_commandt declaration;
-  /// Function which makes applications of the function.
-  smt_function_application_termt::factoryt<smt_command_functiont>
-    make_application;
+  /// Function which makes applications of the smt function.
+  using make_applicationt =
+    smt_function_application_termt::factoryt<smt_command_functiont>;
+  make_applicationt make_application;
   /// Makes the command to define the resulting \p size of calling the object
   /// size function with \p unique_id.
   smt_commandt make_definition(std::size_t unique_id, smt_termt size) const;

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -45,7 +45,8 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
 
 smt_termt convert_expr_to_smt(const exprt &expression)
 {
-  return convert_expr_to_smt(expression, initial_smt_object_map());
+  return convert_expr_to_smt(
+    expression, initial_smt_object_map(), smt_object_sizet{}.make_application);
 }
 
 TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
@@ -1092,6 +1093,7 @@ TEST_CASE(
   config.ansi_c.set_arch_spec_x86_64();
   const symbol_tablet symbol_table;
   const namespacet ns{symbol_table};
+  const smt_object_sizet object_size;
   smt_object_mapt object_map = initial_smt_object_map();
   const symbol_exprt foo{"foo", unsignedbv_typet{32}};
   const symbol_exprt bar{"bar", unsignedbv_typet{32}};
@@ -1103,7 +1105,8 @@ TEST_CASE(
     SECTION("8 object bits")
     {
       config.bv_encoding.object_bits = 8;
-      const auto converted = convert_expr_to_smt(address_of_foo, object_map);
+      const auto converted = convert_expr_to_smt(
+        address_of_foo, object_map, object_size.make_application);
       CHECK(object_map.at(foo).unique_id == 1);
       CHECK(
         converted == smt_bit_vector_theoryt::concat(
@@ -1113,7 +1116,8 @@ TEST_CASE(
     SECTION("16 object bits")
     {
       config.bv_encoding.object_bits = 16;
-      const auto converted = convert_expr_to_smt(address_of_foo, object_map);
+      const auto converted = convert_expr_to_smt(
+        address_of_foo, object_map, object_size.make_application);
       CHECK(object_map.at(foo).unique_id == 1);
       CHECK(
         converted == smt_bit_vector_theoryt::concat(
@@ -1129,15 +1133,17 @@ TEST_CASE(
       exprt address_of = address_of_exprt{foo};
       address_of.type() = bool_typet{};
       REQUIRE_THROWS_MATCHES(
-        convert_expr_to_smt(address_of, object_map),
+        convert_expr_to_smt(
+          address_of, object_map, object_size.make_application),
         invariant_failedt,
         invariant_failure_containing(
           "Result of the address_of operator should have pointer type."));
     }
     SECTION("Objects should already be tracked")
     {
       REQUIRE_THROWS_MATCHES(
-        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        convert_expr_to_smt(
+          address_of_exprt{foo}, object_map, object_size.make_application),
         invariant_failedt,
         invariant_failure_containing("Objects should be tracked before "
                                      "converting their address to SMT terms"));
@@ -1149,7 +1155,8 @@ TEST_CASE(
       track_expression_objects(address_of_foo, ns, object_map);
       object_map.at(foo).unique_id = 256;
       REQUIRE_THROWS_MATCHES(
-        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        convert_expr_to_smt(
+          address_of_exprt{foo}, object_map, object_size.make_application),
         invariant_failedt,
         invariant_failure_containing("There should be sufficient bits to "
                                      "encode unique object identifier."));
@@ -1161,7 +1168,8 @@ TEST_CASE(
       track_expression_objects(address_of_foo, ns, object_map);
       object_map.at(foo).unique_id = 256;
       REQUIRE_THROWS_MATCHES(
-        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        convert_expr_to_smt(
+          address_of_exprt{foo}, object_map, object_size.make_application),
         invariant_failedt,
         invariant_failure_containing("Pointer should be wider than object_bits "
                                      "in order to allow for offset encoding."));
@@ -1174,7 +1182,8 @@ TEST_CASE(
       notequal_exprt{address_of_exprt{foo}, address_of_exprt{bar}};
     track_expression_objects(comparison, ns, object_map);
     INFO("Expression " + comparison.pretty(1, 0));
-    const auto converted = convert_expr_to_smt(comparison, object_map);
+    const auto converted =
+      convert_expr_to_smt(comparison, object_map, object_size.make_application);
     CHECK(object_map.at(foo).unique_id == 2);
     CHECK(object_map.at(bar).unique_id == 1);
     CHECK(