Merge pull request #6573 from thomasspriggs/tas/smt2_incremental_solving

Add implementation of `smt2_incremental_decision_proceduret::get`

Author: thomasspriggs

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

@@ -20,13 +20,11 @@ Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(|not| false\)\)
 Sending command to SMT2 solver - \(assert |B4|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat
-^EXIT=(0|127|134|137)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 type: pointer
 --
 Test that running cbmc with the `--incremental-smt2-solver` argument can be used
 to send a valid SMT2 formula to a sub-process solver for an example input file
-which include control flow constructs. Note that at the time of adding this
-test, an invariant violation is expected due to the unimplemented response
-parsing.
+which include control flow constructs.

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

@@ -12,14 +12,13 @@ Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
 Sending command to SMT2 solver - \(assert |B2|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat
-^EXIT=(0|127|134|137)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 type: pointer
 --
 Test that running cbmc with the `--incremental-smt2-solver` argument causes the
-incremental smt2 solving to be used. Note that at the time of adding this test,
-an invariant violation is expected due to the unimplemented response parsing.
+incremental smt2 solving to be used.
 
 The sliced formula is expected to use only the implemented subset of exprts.
 This is implementation is sufficient to send this example to the solver and

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

@@ -0,0 +1,11 @@
+
+int main()
+{
+  int x, y;
+  if(x != 0)
+    __CPROVER_assert(y != 4, "Assert of inequality to 4.");
+  else
+    __CPROVER_assert(y != 2, "Assert of inequality to 2.");
+  int z = y;
+  return 0;
+}

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

@@ -0,0 +1,17 @@
+CORE winbug
+trace.c
+--incremental-smt2-solver "z3 --smt2 -in" --trace
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Assert of inequality to 4\.: FAILURE
+Assert of inequality to 2\.: FAILURE
+y=4
+y=2
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+type: pointer
+--
+Test that running cbmc with the `--incremental-smt2-solver` argument can be used
+to send a valid SMT2 formula to a sub-process solver for an example input file
+which include control flow constructs.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,6 +2,7 @@
 
 #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>
@@ -163,9 +164,70 @@ exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
   return expr;
 }
 
+static optionalt<smt_termt> get_identifier(
+  const exprt &expr,
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_handle_identifiers,
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_identifiers)
+{
+  const auto handle_find_result = expression_handle_identifiers.find(expr);
+  if(handle_find_result != expression_handle_identifiers.cend())
+    return handle_find_result->second;
+  const auto expr_find_result = expression_identifiers.find(expr);
+  if(expr_find_result != expression_identifiers.cend())
+    return expr_find_result->second;
+  return {};
+}
+
 exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
 {
-  UNIMPLEMENTED_FEATURE("`get` of:\n  " + expr.pretty(2, 0));
+  log.debug() << "`get` - \n  " + expr.pretty(2, 0) << messaget::eom;
+  optionalt<smt_termt> descriptor =
+    get_identifier(expr, expression_handle_identifiers, expression_identifiers);
+  if(!descriptor)
+  {
+    if(gather_dependent_expressions(expr).empty())
+    {
+      descriptor = convert_expr_to_smt(expr);
+    }
+    else
+    {
+      const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
+      INVARIANT(
+        symbol_expr, "Unhandled expressions are expected to be symbols");
+      // Note this case is currently expected to be encountered during trace
+      // generation for -
+      //  * Steps which were removed via --slice-formula.
+      //  * Getting concurrency clock values.
+      // The below implementation which returns the given expression was chosen
+      // based on the implementation of `smt2_convt::get` in the non-incremental
+      // smt2 decision procedure.
+      log.warning()
+        << "`get` attempted for unknown symbol, with identifier - \n"
+        << symbol_expr->get_identifier() << messaget::eom;
+      return expr;
+    }
+  }
+  const smt_get_value_commandt get_value_command{*descriptor};
+  const smt_responset response =
+    get_response_to_command(*solver_process, get_value_command);
+  const auto get_value_response = response.cast<smt_get_value_responset>();
+  if(!get_value_response)
+  {
+    throw analysis_exceptiont{
+      "Expected get-value response from solver, but received - " +
+      response.pretty()};
+  }
+  if(get_value_response->pairs().size() > 1)
+  {
+    throw analysis_exceptiont{
+      "Expected single valuation pair in get-value response from solver, but "
+      "received multiple pairs - " +
+      response.pretty()};
+  }
+  return construct_value_expr_from_smt(
+    get_value_response->pairs()[0].get().value(), expr.type());
 }
 
 void smt2_incremental_decision_proceduret::print_assignment(

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -9,6 +9,7 @@
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <testing-utils/invariant.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
 #include <util/exception_utils.h>
@@ -85,6 +86,14 @@ class smt_mock_solver_processt : public smt_base_solver_processt
   ~smt_mock_solver_processt() override = default;
 };
 
+/// \brief Data structures and their initialisation shared between tests.
+/// \details
+///   Instantiates a `smt2_incremental_decision_proceduret` using a mock of the
+///   solver process to direct communication with the solver to collections of
+///   `sent_commands` and `mock_responses`. The `mock_respones` must be
+///   populated by the test, before the decision procedure expects them. The
+///   `sent_commands` should be checked by the test after the decision procedure
+///   has sent them.
 struct decision_procedure_test_environmentt final
 {
   void send(const smt_commandt &smt_command);
@@ -378,3 +387,112 @@ TEST_CASE(
         "SMT solver does not support given command."});
   }
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret getting values back from solver.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  const symbolt foo = make_test_symbol("foo", signedbv_typet{16});
+  const smt_identifier_termt foo_term{"foo", smt_bit_vector_sortt{16}};
+  const exprt expr_42 = from_integer({42}, signedbv_typet{16});
+  const smt_bit_vector_constant_termt term_42{42, 16};
+  SECTION("Set \"foo\" identifier and solve.")
+  {
+    test.sent_commands.clear();
+    const exprt equal_42 = equal_exprt{foo.symbol_expr(), expr_42};
+    test.procedure.set_to(equal_42, true);
+    test.mock_responses.push_back(smt_check_sat_responset{smt_sat_responset{}});
+    test.procedure();
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{foo_term, {}},
+        smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
+        smt_check_sat_commandt{}});
+    SECTION("Get \"foo\" value back")
+    {
+      test.sent_commands.clear();
+      test.mock_responses.push_back(
+        smt_get_value_responset{{{foo_term, term_42}}});
+      REQUIRE(test.procedure.get(foo.symbol_expr()) == expr_42);
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
+    }
+    SECTION("Get value of non-set symbol")
+    {
+      // smt2_incremental_decision_proceduret is used this way when cbmc is
+      // invoked with the combination of `--trace` and `--slice-formula`.
+      test.sent_commands.clear();
+      const exprt bar =
+        make_test_symbol("bar", signedbv_typet{16}).symbol_expr();
+      REQUIRE(test.procedure.get(bar) == bar);
+      REQUIRE(test.sent_commands.empty());
+    }
+    SECTION("Get value of type less symbol back")
+    {
+      // smt2_incremental_decision_proceduret is used this way as part of
+      // building the goto trace, to get the partial order concurrency clock
+      // values.
+      test.sent_commands.clear();
+      const symbol_exprt baz = symbol_exprt::typeless("baz");
+      REQUIRE(test.procedure.get(baz) == baz);
+      REQUIRE(test.sent_commands.empty());
+    }
+    SECTION("Get value of trivially solved expression")
+    {
+      test.sent_commands.clear();
+      const smt_termt not_true_term =
+        smt_core_theoryt::make_not(smt_bool_literal_termt{true});
+      test.mock_responses.push_back(smt_get_value_responset{
+        {{not_true_term, smt_bool_literal_termt{false}}}});
+      REQUIRE(test.procedure.get(not_exprt{true_exprt{}}) == false_exprt{});
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{not_true_term}});
+    }
+    SECTION("Invariant violated due to expression in unexpected form.")
+    {
+      const mult_exprt unexpected{foo.symbol_expr(), from_integer(2, foo.type)};
+      const cbmc_invariants_should_throwt invariants_throw;
+      REQUIRE_THROWS_MATCHES(
+        test.procedure.get(unexpected),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Unhandled expressions are expected to be symbols"));
+    }
+    SECTION("Error handling of mismatched response.")
+    {
+      test.sent_commands.clear();
+      const smt_check_sat_responset unexpected{smt_sat_responset{}};
+      test.mock_responses.push_back(unexpected);
+      REQUIRE_THROWS_MATCHES(
+        test.procedure.get(foo.symbol_expr()),
+        analysis_exceptiont,
+        analysis_execption_with_messaget{
+          "Expected get-value response from solver, but received - " +
+          unexpected.pretty()});
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
+    }
+    SECTION("Error handling of multiple responses.")
+    {
+      test.sent_commands.clear();
+      const smt_get_value_responset unexpected{
+        {{foo_term, term_42}, {foo_term, term_42}}};
+      test.mock_responses.push_back(unexpected);
+      REQUIRE_THROWS_MATCHES(
+        test.procedure.get(foo.symbol_expr()),
+        analysis_exceptiont,
+        analysis_execption_with_messaget{
+          "Expected single valuation pair in get-value response from solver, "
+          "but received multiple pairs - " +
+          unexpected.pretty()});
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
+    }
+  }
+}