Merge pull request #6131 from thomasspriggs/tas/incremental_smt2

Add start of foundational work for incremental SMT2 solving support

Author: thomasspriggs

CODEOWNERS

@@ -54,6 +54,7 @@
 /jbmc/src/jdiff/ @smowton @peterschrammel
 /src/cpp/ @kroening @tautschnig @peterschrammel
 /src/solvers/smt2 @kroening @martin-cs @tautschnig @peterschrammel @allredj @romainbrenguier
+/src/solvers/smt2_incremental @peterschrammel @thomasspriggs @NlightNFotis @TGWDB @chrisr-diffblue
 /src/statement-list/ @kroening @tautschnig @peterschrammel @pkesseli
 
 /cmake/        @diffblue/diffblue-opensource

regression/CMakeLists.txt

@@ -32,6 +32,7 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
+add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)

regression/Makefile

@@ -10,6 +10,7 @@ DIRS = cbmc \
        cbmc-concurrency \
        cbmc-cover \
        cbmc-incr-oneloop \
+       cbmc-incr-smt2 \
        cbmc-incr \
        cbmc-with-incr \
        array-refinement-with-incr \

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -0,0 +1,4 @@
+
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
+)

regression/cbmc-incr-smt2/Makefile

@@ -0,0 +1,14 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
+
+tests.log: ../test.pl test
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests*.log

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

@@ -0,0 +1,17 @@
+CORE
+test.c
+--incremental-smt2-solver z3
+Passing problem to incremental SMT2 solving via "z3"
+^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`.

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

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int x;
+  __CPROVER_assert(x, "Nondeterministic int assert.");
+  return 0;
+}

src/cbmc/cbmc_parse_options.cpp

@@ -409,6 +409,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("incremental-smt2-solver"))
+  {
+    options.set_option(
+      "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
+      solver_set = true;
+  }
+
   if(cmdline.isset("external-sat-solver"))
   {
     options.set_option(
@@ -1042,6 +1049,9 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --incremental-smt2-solver cmd\n"
+    "                              command to invoke external SMT solver for\n"
+    "                              incremental solving (experimental)\n"
     " --external-sat-solver cmd    command to invoke SAT solver process\n"
     HELP_STRING_REFINEMENT_CBMC
     " --outfile filename           output formula to given file\n"

src/cbmc/cbmc_parse_options.h

@@ -57,6 +57,7 @@ class optionst;
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
+  "(incremental-smt2-solver):" \
   "(external-sat-solver):" \
   "(no-sat-preprocessor)" \
   "(beautify)" \

src/goto-checker/solver_factory.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
+#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
@@ -140,6 +141,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
   }
   else if(options.get_bool_option("refine-strings"))
     return get_string_refinement();
+  const auto incremental_smt2_solver =
+    options.get_option("incremental-smt2-solver");
+  if(!incremental_smt2_solver.empty())
+    return get_incremental_smt2(incremental_smt2_solver);
   if(options.get_bool_option("smt2"))
     return get_smt2(get_smt2_solver_type());
   return get_default();
@@ -321,6 +326,16 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
+std::unique_ptr<solver_factoryt::solvert>
+solver_factoryt::get_incremental_smt2(std::string solver_command)
+{
+  no_beautification();
+
+  return util_make_unique<solvert>(
+    util_make_unique<smt2_incremental_decision_proceduret>(
+      std::move(solver_command)));
+}
+
 std::unique_ptr<solver_factoryt::solvert>
 solver_factoryt::get_smt2(smt2_dect::solvert solver)
 {