Implement handling of unexpected responses from SMT solver

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -32,6 +32,21 @@ static smt_responset get_response_to_command(
     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
@@ -236,5 +251,7 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
       log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
     return lookup_decision_procedure_result(check_sat_response->kind());
   }
-  UNIMPLEMENTED_FEATURE("handling solver response.");
+  if(const auto problem = get_problem_messages(result))
+    throw analysis_exceptiont{*problem};
+  throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
 }

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -11,6 +11,7 @@
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/exception_utils.h>
 #include <util/make_unique.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -23,6 +24,36 @@
 
 #include <deque>
 
+class analysis_execption_with_messaget
+  : public Catch::MatcherBase<analysis_exceptiont>
+{
+public:
+  explicit analysis_execption_with_messaget(std::string message);
+  bool match(const analysis_exceptiont &exception) const override;
+  std::string describe() const override;
+
+private:
+  std::string expected;
+};
+
+analysis_execption_with_messaget::analysis_execption_with_messaget(
+  std::string message)
+  : expected{std::move(message)}
+{
+}
+
+bool analysis_execption_with_messaget::match(
+  const analysis_exceptiont &exception) const
+{
+  return expected == exception.what();
+}
+
+std::string analysis_execption_with_messaget::describe() const
+{
+  return std::string{"analysis_exceptiont with `.what' containing - \""} +
+         expected + "\"";
+}
+
 class smt_mock_solver_processt : public smt_base_solver_processt
 {
   std::function<void(const smt_commandt &)> _send;
@@ -293,7 +324,57 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   decision_procedure_test_environmentt test{};
-  test.mock_responses = {smt_success_responset{},
-                         smt_check_sat_responset{smt_sat_responset{}}};
-  REQUIRE_NOTHROW(test.procedure());
+  SECTION("Expected success response.")
+  {
+    test.mock_responses = {smt_success_responset{},
+                           smt_check_sat_responset{smt_sat_responset{}}};
+    REQUIRE_NOTHROW(test.procedure());
+  }
+  SECTION("Duplicated success messages.")
+  {
+    test.mock_responses = {smt_success_responset{},
+                           smt_success_responset{},
+                           smt_check_sat_responset{smt_sat_responset{}}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "Unexpected kind of response from SMT solver."});
+  }
+}
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret receives unexpected responses to "
+  "check-sat.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  SECTION("get-value response")
+  {
+    test.mock_responses = {
+      smt_get_value_responset{{{"x", smt_bool_literal_termt{false}}}}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "Unexpected kind of response from SMT solver."});
+  }
+  SECTION("error message response")
+  {
+    test.mock_responses = {smt_error_responset{"foobar"}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "SMT solver returned an error message - foobar"});
+  }
+  SECTION("unsupported response")
+  {
+    test.mock_responses = {smt_unsupported_responset{}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "SMT solver does not support given command."});
+  }
 }