Add padding instantiation to decision procedure

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -18,6 +18,7 @@
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/encoding/enum_encoding.h>
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
@@ -364,12 +365,28 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
   });
 }
 
+exprt smt2_incremental_decision_proceduret::substitute_defined_padding(
+  exprt root_expr)
+{
+  root_expr.visit_pre([&](exprt &node) {
+    if(const auto pad = expr_try_dynamic_cast<nondet_padding_exprt>(node))
+    {
+      const auto instance = "padding_" + std::to_string(padding_sequence());
+      const auto term =
+        smt_identifier_termt{instance, convert_type_to_smt_sort(pad->type())};
+      solver_process->send(smt_declare_function_commandt{term, {}});
+      node = symbol_exprt{instance, node.type()};
+    }
+  });
+  return root_expr;
+}
+
 smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   define_index_identifiers(expr);
-  const exprt substituted =
-    substitute_identifiers(expr, expression_identifiers);
+  const exprt substituted = substitute_defined_padding(
+    substitute_identifiers(expr, expression_identifiers));
   track_expression_objects(substituted, ns, object_map);
   associate_pointer_sizes(
     substituted,

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -102,6 +102,11 @@ 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);
+  /// In the case where lowering passes insert instances of the anonymous
+  /// `nondet_padding_exprt`, these need functions declaring for each instance.
+  /// These instances are then substituted for the function identifier in order
+  /// to free the solver to choose a non-det value.
+  exprt substitute_defined_padding(exprt expr);
   /// Sends the solver the definitions of the object sizes and dynamic memory
   /// statuses.
   void define_object_properties();
@@ -135,7 +140,7 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence, array_sequence, index_sequence;
+  } handle_sequence, array_sequence, index_sequence, padding_sequence;
   /// When the `handle(exprt)` member function is called, the decision procedure
   /// commands the SMT solver to define a new function corresponding to the
   /// given expression. The mapping of the expressions to the function

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1,6 +1,7 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
@@ -13,6 +14,7 @@
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
@@ -268,6 +270,28 @@ TEST_CASE(
               smt_identifier_termt{"third_comparison", smt_bool_sortt{}})},
           smt_assert_commandt{comparison_conjunction_term}});
     }
+    SECTION("Set with nondet_padding")
+    {
+      const exprt to_set = equal_exprt{
+        concatenation_exprt{
+          {nondet_padding_exprt{bv_typet{8}}, from_integer(42, bv_typet{8})},
+          bv_typet{16}},
+        from_integer(42, bv_typet{16})};
+      test.sent_commands.clear();
+      test.procedure.set_to(to_set, true);
+      // (declare-fun padding_0 () (_ BitVec 8))
+      // (assert (= (concat padding_0 (_ bv42 8)) (_ bv42 16)))
+      const auto expected_padding_term =
+        smt_identifier_termt{"padding_0", smt_bit_vector_sortt{8}};
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{
+          smt_declare_function_commandt{expected_padding_term, {}},
+          smt_assert_commandt{smt_core_theoryt::equal(
+            smt_bit_vector_theoryt::concat(
+              expected_padding_term, smt_bit_vector_constant_termt{42, 8}),
+            smt_bit_vector_constant_termt{42, 16})}});
+    }
     SECTION("Handle of value-less symbol.")
     {
       const symbolt foo = make_test_symbol("foo", bool_typet{});