Implement sending commands to solver in incremental SMT2 backend

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -1,4 +1,10 @@
 
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+    set(exclude_win_broken_tests -X winbug)
+else()
+    set(exclude_win_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
 )

regression/cbmc-incr-smt2/Makefile

@@ -3,8 +3,14 @@ default: test
 include ../../src/config.inc
 include ../../src/common
 
+ifeq ($(BUILD_ENV_),MSVC)
+	exclude_broken_windows_tests=-X winbug
+else
+	exclude_broken_windows_tests=
+endif
+
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
 
 tests.log: ../test.pl test
 

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

@@ -0,0 +1,16 @@
+
+int main()
+{
+  int x, y;
+  if(x != 0)
+  {
+    y = 9;
+  }
+  else
+  {
+    y = 4;
+  }
+  int z = y;
+  __CPROVER_assert(x != z, "Assert of integer equality.");
+  return 0;
+}

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

@@ -0,0 +1,32 @@
+CORE winbug
+control_flow.c
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(set-option :produce-models true\)
+Sending command to SMT2 solver - \(set-logic QF_UFBV\)
+Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |goto_symex::&92;guard#1| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::y!0@1#4| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#3| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::z!0@1#2| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
+Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)
+Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
+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)$
+^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.

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

@@ -1,17 +1,26 @@
-CORE
+CORE winbug
 test.c
---incremental-smt2-solver z3
-Passing problem to incremental SMT2 solving via "z3"
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(set-option :produce-models true\)
+Sending command to SMT2 solver - \(set-logic QF_UFBV\)
+Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+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)$
 ^SIGNAL=0$
-identifier: main::1::x
 --
 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 solving.
-Regexes matching the printing in the expected failed invariant are included in
-order to test that `--slice-formula` is causing the first unimplemented
-expression passed to `smt2_incremental_decision_proceduret` to relate to the
-variable `x` in function `main` and not to `cprover_initialise`.
+an invariant violation is expected due to the unimplemented response parsing.
+
+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
+receive a "sat" response.

src/goto-checker/solver_factory.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
@@ -330,10 +331,12 @@ std::unique_ptr<solver_factoryt::solvert>
 solver_factoryt::get_incremental_smt2(std::string solver_command)
 {
   no_beautification();
+  auto solver_process = util_make_unique<smt_piped_solver_processt>(
+    std::move(solver_command), message_handler);
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      std::move(solver_command)));
+      ns, std::move(solver_process), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>

src/solvers/Makefile

@@ -199,6 +199,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
+      smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -46,8 +46,8 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
 
 static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for symbol expression: " + symbol_expr.pretty());
+  return smt_identifier_termt{symbol_expr.get_identifier(),
+                              convert_type_to_smt_sort(symbol_expr.type())};
 }
 
 static smt_termt convert_expr_to_smt(const nondet_symbol_exprt &nondet_symbol)

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,16 +2,130 @@
 
 #include "smt2_incremental_decision_procedure.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_solver_process.h>
+#include <solvers/smt2_incremental/smt_terms.h>
 #include <util/expr.h>
+#include <util/namespace.h>
+#include <util/range.h>
+#include <util/std_expr.h>
+#include <util/string_utils.h>
+#include <util/symbol.h>
+
+#include <stack>
+
+/// \brief Find all sub expressions of the given \p expr which need to be
+///   expressed as separate smt commands.
+/// \note This pass over \p expr is tightly coupled to the implementation of
+///   `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.
+static std::unordered_set<exprt, irep_hash>
+gather_dependent_expressions(const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> dependent_expressions;
+  expr.visit_pre([&](const exprt &expr_node) {
+    if(can_cast_expr<symbol_exprt>(expr_node))
+    {
+      dependent_expressions.insert(expr_node);
+    }
+  });
+  return dependent_expressions;
+}
+
+/// \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(
+  const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> seen_expressions =
+    make_range(expression_identifiers)
+      .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
+        return expr_identifier.first;
+      });
+  std::stack<exprt> to_be_defined;
+  const auto dependencies_needed = [&](const exprt &expr) {
+    bool result = false;
+    for(const auto &dependency : gather_dependent_expressions(expr))
+    {
+      if(!seen_expressions.insert(dependency).second)
+        continue;
+      result = true;
+      to_be_defined.push(dependency);
+    }
+    return result;
+  };
+  dependencies_needed(expr);
+  while(!to_be_defined.empty())
+  {
+    const exprt current = to_be_defined.top();
+    if(dependencies_needed(current))
+      continue;
+    if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
+    {
+      const irep_idt &identifier = symbol_expr->get_identifier();
+      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);
+      }
+      else
+      {
+        if(dependencies_needed(symbol->value))
+          continue;
+        const smt_define_function_commandt function{
+          symbol->name, {}, convert_expr_to_smt(symbol->value)};
+        expression_identifiers.emplace(*symbol_expr, function.identifier());
+        solver_process->send(function);
+      }
+    }
+    to_be_defined.pop();
+  }
+}
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
-  std::string solver_command)
-  : solver_command{std::move(solver_command)}, number_of_solver_calls{0}
+  const namespacet &_ns,
+  std::unique_ptr<smt_base_solver_processt> _solver_process,
+  message_handlert &message_handler)
+  : ns{_ns},
+    number_of_solver_calls{0},
+    solver_process(std::move(_solver_process)),
+    log{message_handler}
+{
+  solver_process->send(
+    smt_set_option_commandt{smt_option_produce_modelst{true}});
+  solver_process->send(smt_set_logic_commandt{
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
+}
+
+void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
+  const exprt &expr)
 {
+  if(
+    expression_handle_identifiers.find(expr) !=
+    expression_handle_identifiers.cend())
+  {
+    return;
+  }
+
+  define_dependent_functions(expr);
+  smt_define_function_commandt function{
+    "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
+  expression_handle_identifiers.emplace(expr, function.identifier());
+  solver_process->send(function);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
 {
+  log.debug() << "`handle`  -\n  " << expr.pretty(2, 0) << messaget::eom;
+  ensure_handle_for_expr_defined(expr);
   return expr;
 }
 
@@ -29,7 +143,7 @@ void smt2_incremental_decision_proceduret::print_assignment(
 std::string
 smt2_incremental_decision_proceduret::decision_procedure_text() const
 {
-  return "incremental SMT2 solving via \"" + solver_command + "\"";
+  return "incremental SMT2 solving via " + solver_process->description();
 }
 
 std::size_t
@@ -40,9 +154,22 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
 
 void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
 {
-  UNIMPLEMENTED_FEATURE(
-    "`set_to` (" + std::string{value ? "true" : "false"} + "):\n  " +
-    expr.pretty(2, 0));
+  PRECONDITION(can_cast_type<bool_typet>(expr.type()));
+  log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
+              << ") -\n  " << expr.pretty(2, 0) << messaget::eom;
+
+  define_dependent_functions(expr);
+  auto converted_term = [&]() -> smt_termt {
+    const auto expression_handle_identifier =
+      expression_handle_identifiers.find(expr);
+    if(expression_handle_identifier != expression_handle_identifiers.cend())
+      return expression_handle_identifier->second;
+    else
+      return convert_expr_to_smt(expr);
+  }();
+  if(!value)
+    converted_term = smt_core_theoryt::make_not(converted_term);
+  solver_process->send(smt_assert_commandt{converted_term});
 }
 
 void smt2_incremental_decision_proceduret::push(
@@ -69,5 +196,7 @@ void smt2_incremental_decision_proceduret::pop()
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  UNIMPLEMENTED_FEATURE("solving.");
+  solver_process->send(smt_check_sat_commandt{});
+  const smt_responset result = solver_process->receive_response();
+  UNIMPLEMENTED_FEATURE("handling solver response.");
 }