Merge pull request #6474 from thomasspriggs/tas/smt_sat_unsat

Add interpretation of SMT check-sat responses for incremental SMT solving support

Author: NlightNFotis

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

@@ -0,0 +1,12 @@
+
+int main()
+{
+  int x;
+  int y;
+  if(y)
+    y = x;
+  else
+    y = x;
+  __CPROVER_assert(y == x, "Nondeterministic int assert.");
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE winbug
+valid_unsat.c
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(check-sat\)
+Solver response - unsat
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+type: pointer
+--
+Test that given a `.c` program where all assertions hold, the solver responds
+with unsat and CBMC reports that verification is successful.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -5,17 +5,48 @@
 #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_responses.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/nodiscard.h>
 #include <util/range.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
 #include <stack>
 
+/// Issues a command to the solving process which is expected to optionally
+/// return a success status followed by the actual response of interest.
+static smt_responset get_response_to_command(
+  smt_base_solver_processt &solver_process,
+  const smt_commandt &command)
+{
+  solver_process.send(command);
+  auto response = solver_process.receive_response();
+  if(response.cast<smt_success_responset>())
+    return solver_process.receive_response();
+  else
+    return response;
+}
+
+static optionalt<std::string>
+get_problem_messages(const smt_responset &response)
+{
+  if(const auto error = response.cast<smt_error_responset>())
+  {
+    return "SMT solver returned an error message - " +
+           id2string(error->message());
+  }
+  if(response.cast<smt_unsupported_responset>())
+  {
+    return {"SMT solver does not support given command."};
+  }
+  return {};
+}
+
 /// \brief Find all sub expressions of the given \p expr which need to be
 ///   expressed as separate smt commands.
 /// \return A collection of sub expressions, which need to be expressed as
@@ -196,10 +227,31 @@ void smt2_incremental_decision_proceduret::pop()
   UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
+NODISCARD
+static decision_proceduret::resultt lookup_decision_procedure_result(
+  const smt_check_sat_response_kindt &response_kind)
+{
+  if(response_kind.cast<smt_sat_responset>())
+    return decision_proceduret::resultt::D_SATISFIABLE;
+  if(response_kind.cast<smt_unsat_responset>())
+    return decision_proceduret::resultt::D_UNSATISFIABLE;
+  if(response_kind.cast<smt_unknown_responset>())
+    return decision_proceduret::resultt::D_ERROR;
+  UNREACHABLE;
+}
+
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  solver_process->send(smt_check_sat_commandt{});
-  const smt_responset result = solver_process->receive_response();
-  UNIMPLEMENTED_FEATURE("handling solver response.");
+  const smt_responset result =
+    get_response_to_command(*solver_process, smt_check_sat_commandt{});
+  if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
+  {
+    if(check_sat_response->kind().cast<smt_unknown_responset>())
+      log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
+    return lookup_decision_procedure_result(check_sat_response->kind());
+  }
+  if(const auto problem = get_problem_messages(result))
+    throw analysis_exceptiont{*problem};
+  throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
 }

src/solvers/smt2_incremental/smt_response_validation.h

@@ -5,6 +5,7 @@
 
 #include <solvers/smt2_incremental/smt_responses.h>
 #include <util/invariant.h>
+#include <util/nodiscard.h>
 #include <util/optional.h>
 
 #include <string>
@@ -37,7 +38,7 @@ class response_or_errort final
   std::vector<std::string> messages;
 };
 
-response_or_errort<smt_responset>
+NODISCARD response_or_errort<smt_responset>
 validate_smt_response(const irept &parse_tree);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -2,7 +2,10 @@
 
 #include <solvers/smt2_incremental/smt_solver_process.h>
 
+#include <solvers/smt2/smt2irep.h>
+#include <solvers/smt2_incremental/smt_response_validation.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/string_utils.h>
 
@@ -28,9 +31,28 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   process.send(command_string + "\n");
 }
 
+/// Log messages and throw exception.
+static void handle_invalid_smt(
+  const std::vector<std::string> &validation_errors,
+  messaget &log)
+{
+  for(const std::string &message : validation_errors)
+  {
+    log.error() << message << messaget::eom;
+  }
+  throw analysis_exceptiont{"Invalid SMT response received from solver."};
+}
+
 smt_responset smt_piped_solver_processt::receive_response()
 {
   const auto response_text = process.wait_receive();
   log.debug() << "Solver response - " << response_text << messaget::eom;
-  UNIMPLEMENTED_FEATURE("parsing of solver response.");
+  response_stream << response_text;
+  const auto parse_tree = smt2irep(response_stream, log.get_message_handler());
+  if(!parse_tree)
+    throw deserialization_exceptiont{"Incomplete SMT response."};
+  const auto validation_result = validate_smt_response(*parse_tree);
+  if(const auto validation_errors = validation_result.get_if_error())
+    handle_invalid_smt(*validation_errors, log);
+  return *validation_result.get_if_valid();
 }

src/solvers/smt2_incremental/smt_solver_process.h

@@ -9,6 +9,7 @@ class smt_commandt;
 #include <util/message.h>
 #include <util/piped_process.h>
 
+#include <sstream>
 #include <string>
 
 class smt_base_solver_processt
@@ -49,6 +50,8 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   std::string command_line_description;
   /// The raw solver sub process.
   piped_processt process;
+  /// For buffering / combining communications from the solver to cbmc.
+  std::stringstream response_stream;
   /// For debug printing.
   messaget log;
 };