Merge pull request #7061 from diffblue/esteffin/nondet-symbol-to-new-SMT2

Add nondet_symbol_exprt translation to new SMT2 backend

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/nondeterministic-int-assert/nondet_symbol.c

@@ -0,0 +1,11 @@
+extern int undefined_function();
+
+int main()
+{
+  int nondet1 = undefined_function();
+  __CPROVER_assume(nondet1 == 10);
+  __CPROVER_assert(nondet1 < 11, "");
+  __CPROVER_assert(undefined_function() == 0, "");
+
+  __CPROVER_assert(undefined_function() == undefined_function(), "");
+}

regression/cbmc-incr-smt2/nondeterministic-int-assert/nondet_symbol.desc

@@ -0,0 +1,12 @@
+CORE
+nondet_symbol.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line 7 assertion: SUCCESS
+\[main\.assertion\.2\] line 8 assertion: FAILURE
+\[main\.assertion\.3\] line 10 assertion: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that running cbmc with the `--incremental-smt2-solver` supports nondet_symbol expressions.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -124,9 +124,11 @@ static smt_termt convert_expr_to_smt(
   const nondet_symbol_exprt &nondet_symbol,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for nondet symbol expression: " +
-    nondet_symbol.pretty());
+  // A nondet_symbol is a reference to an unconstrained function. This function
+  // will already have been added as a dependency.
+  return smt_identifier_termt{
+    nondet_symbol.get_identifier(),
+    convert_type_to_smt_sort(nondet_symbol.type())};
 }
 
 /// \brief Makes a term which is true if \p input is not 0 / false.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -62,13 +62,16 @@ get_problem_messages(const smt_responset &response)
 ///   `convert_expr_to_smt`. This is because any sub expressions which
 ///   `convert_expr_to_smt` translates into function applications, must also be
 ///   returned by this`gather_dependent_expressions` function.
+/// \details `symbol_exprt`, `array_exprt` and `nondet_symbol_exprt` add
+///   dependant expressions.
 static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
 {
   std::vector<exprt> dependent_expressions;
   expr.visit_pre([&](const exprt &expr_node) {
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
-      can_cast_expr<array_exprt>(expr_node))
+      can_cast_expr<array_exprt>(expr_node) ||
+      can_cast_expr<nondet_symbol_exprt>(expr_node))
     {
       dependent_expressions.push_back(expr_node);
     }
@@ -100,6 +103,21 @@ void smt2_incremental_decision_proceduret::define_array_function(
   expression_identifiers.emplace(array, array_identifier);
 }
 
+void send_function_definition(
+  const exprt &expr,
+  const irep_idt &symbol_identifier,
+  const std::unique_ptr<smt_base_solver_processt> &solver_process,
+  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_identifiers)
+{
+  const smt_declare_function_commandt function{
+    smt_identifier_termt(
+      symbol_identifier, convert_type_to_smt_sort(expr.type())),
+    {}};
+  expression_identifiers.emplace(expr, function.identifier());
+  solver_process->send(function);
+}
+
 /// \brief Defines any functions which \p expr depends on, which have not yet
 ///   been defined, along with their dependencies in turn.
 void smt2_incremental_decision_proceduret::define_dependent_functions(
@@ -134,12 +152,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
       const symbolt *symbol = nullptr;
       if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
       {
-        const smt_declare_function_commandt function{
-          smt_identifier_termt(
-            identifier, convert_type_to_smt_sort(symbol_expr->type())),
-          {}};
-        expression_identifiers.emplace(*symbol_expr, function.identifier());
-        solver_process->send(function);
+        send_function_definition(
+          *symbol_expr,
+          symbol_expr->get_identifier(),
+          solver_process,
+          expression_identifiers);
       }
       else
       {
@@ -153,6 +170,16 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     }
     if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
       define_array_function(*array_expr);
+    if(
+      const auto nondet_symbol =
+        expr_try_dynamic_cast<nondet_symbol_exprt>(current))
+    {
+      send_function_definition(
+        *nondet_symbol,
+        nondet_symbol->get_identifier(),
+        solver_process,
+        expression_identifiers);
+    }
     to_be_defined.pop();
   }
 }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -119,6 +119,20 @@ TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
     smt_identifier_termt("foo", smt_bool_sortt{}));
 }
 
+TEST_CASE(
+  "\"nondet_symbol_exprt\" to smt term conversion",
+  "[core][smt2_incremental]")
+{
+  auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
+  CHECK(
+    test.convert(nondet_symbol_exprt{"nondet_symbol1", bool_typet{}}) ==
+    smt_identifier_termt("nondet_symbol1", smt_bool_sortt{}));
+  CHECK(
+    test.convert(
+      nondet_symbol_exprt{"nondet_symbol2", bitvector_typet{ID_bv, 42}}) ==
+    smt_identifier_termt{"nondet_symbol2", smt_bit_vector_sortt{42}});
+}
+
 TEST_CASE(
   "\"exprt\" to smt term conversion for constants/literals",
   "[core][smt2_incremental]")
@@ -1350,7 +1364,7 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
         exprt{false_exprt{}});
       const smt_termt from_term = test.convert(from_expr);
       const std::size_t width = GENERATE(1, 8, 16, 32, 64);
-      const typecast_exprt cast{from_expr, bitvector_typet{ID_bv, width}};
+      const typecast_exprt cast{from_expr, bv_typet(width)};
       CHECK(
         test.convert(cast) == smt_core_theoryt::if_then_else(
                                 from_term,

unit/solvers/smt2_incremental/module_dependencies.txt

@@ -1,3 +1,4 @@
+goto-symex
 solvers/smt2_incremental
 testing-utils
 util

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -23,6 +23,7 @@
 // means that we get error messages showing the smt formula expressed as SMT2
 // strings instead of `{?}` being printed. It works because catch uses the
 // appropriate overload of `operator<<` where it exists.
+#include <goto-symex/path_storage.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 
 #include <deque>
@@ -306,6 +307,49 @@ TEST_CASE(
             "B0", {}, smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}}});
     }
   }
+  SECTION("Handle single nondet_symbol")
+  {
+    // Using the standard way to create nondet_symbol_exprt.
+    ::symex_nondet_generatort generator;
+    const nondet_symbol_exprt nondet_symbol0 =
+      generator(bool_typet{}, source_locationt{});
+    const smt_identifier_termt nondet_symbol_term0{
+      nondet_symbol0.get_identifier(), smt_bool_sortt{}};
+    test.sent_commands.clear();
+    test.procedure.handle(nondet_symbol0);
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{nondet_symbol_term0, {}},
+        smt_define_function_commandt{"B0", {}, nondet_symbol_term0}});
+  }
+  SECTION("Handle multiple nested nondet_symbol")
+  {
+    ::symex_nondet_generatort generator;
+    const nondet_symbol_exprt nondet_symbol1 =
+      generator(bv_typet(42), source_locationt{});
+    const smt_identifier_termt nondet_symbol_term1{
+      nondet_symbol1.get_identifier(), smt_bit_vector_sortt{42}};
+    const nondet_symbol_exprt nondet_symbol2 =
+      generator(bv_typet(42), source_locationt{});
+    const smt_identifier_termt nondet_symbol_term2{
+      nondet_symbol2.get_identifier(), smt_bit_vector_sortt{42}};
+    // Check that the 2 calls to the generator returns unique nondet_symbols.
+    REQUIRE(
+      nondet_symbol1.get_identifier() != nondet_symbol_term2.identifier());
+    test.sent_commands.clear();
+    test.procedure.handle(equal_exprt{nondet_symbol1, nondet_symbol2});
+    // Checking that we defined 2 symbols and that they are correctly compared.
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{nondet_symbol_term1, {}},
+        smt_declare_function_commandt{nondet_symbol_term2, {}},
+        smt_define_function_commandt{
+          "B0",
+          {},
+          smt_core_theoryt::equal(nondet_symbol_term1, nondet_symbol_term2)}});
+  }
 }
 
 TEST_CASE(