Merge pull request #7161 from esteffin/esteffin/add-dump-smt-formula-arg

thomasspriggs · web-flow · commit 5d603e419bde · 2022-12-12T19:31:25.000Z
Log to file the SMT formula run by the solver
diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
@@ -467,6 +467,9 @@ The flag \fB\-\-slice\-formula\fR should be added to remove some not-yet support
 \fB\-\-outfile\fR filename
 output formula to given file
 .TP
+\fB\-\-dump\-smt\-formula\fR filename
+output smt incremental formula to the given file
+.TP
 \fB\-\-write\-solver\-stats\-to\fR json\-file
 collect the solver query complexity
 .TP
diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1
@@ -445,6 +445,9 @@ incremental solving (experimental)
 \fB\-\-outfile\fR filename
 output formula to given file
 .TP
+\fB\-\-dump\-smt\-formula\fR filename
+output smt incremental formula to the given file
+.TP
 \fB\-\-write\-solver\-stats\-to\fR \fIjson\-file\fR
 collect the solver query complexity
 .TP
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-match-out-file-rules.txt b/regression/cbmc-output-file/dump-smt-formula/cvc5-match-out-file-rules.txt
@@ -0,0 +1,9 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(assert B2\)
+\(check-sat\)
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-match.desc b/regression/cbmc-output-file/dump-smt-formula/cvc5-match.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file
+matches the rules defined in test-outfile-rules.txt
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match-out-file-rules.txt b/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match-out-file-rules.txt
@@ -0,0 +1,6 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(check-sat\)
+\(assert B2\)
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match.desc b/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file does
+not match the rules defined in test-outfile-rules.txt
diff --git a/regression/cbmc-output-file/dump-smt-formula/test.c b/regression/cbmc-output-file/dump-smt-formula/test.c
@@ -0,0 +1,7 @@
+
+int main()
+{
+  int x;
+  __CPROVER_assert(x, "Nondeterministic int assert.");
+  return 0;
+}
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-match-out-file-rules.txt b/regression/cbmc-output-file/dump-smt-formula/z3-match-out-file-rules.txt
@@ -0,0 +1,9 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(assert B2\)
+\(check-sat\)
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-match.desc b/regression/cbmc-output-file/dump-smt-formula/z3-match.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file
+matches the rules defined in test-outfile-rules.txt
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-no-match-out-file-rules.txt b/regression/cbmc-output-file/dump-smt-formula/z3-no-match-out-file-rules.txt
@@ -0,0 +1,6 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(check-sat\)
+\(assert B2\)
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-no-match.desc b/regression/cbmc-output-file/dump-smt-formula/z3-no-match.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file does
+not match the rules defined in test-outfile-rules.txt
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -331,7 +331,8 @@ solver_factoryt::get_string_refinement()
 
 std::unique_ptr<std::ofstream> open_outfile_and_check(
   const std::string &filename,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const std::string &arg_name)
 {
   if(filename.empty())
     return nullptr;
@@ -345,7 +346,7 @@ std::unique_ptr<std::ofstream> open_outfile_and_check(
   if(!*out)
   {
     throw invalid_command_line_argument_exceptiont(
-      "failed to open file: " + filename, "--outfile");
+      "failed to open file: " + filename, arg_name);
   }
 
   messaget log(message_handler);
@@ -360,22 +361,38 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
   no_beautification();
 
   const std::string outfile_arg = options.get_option("outfile");
+  const std::string dump_smt_formula = options.get_option("dump-smt-formula");
+
+  if(!outfile_arg.empty() && !dump_smt_formula.empty())
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "Argument --outfile is incompatible with --dump-smt-formula. ",
+      "--outfile");
+  }
 
   std::unique_ptr<smt_base_solver_processt> solver_process = nullptr;
 
   if(!outfile_arg.empty())
   {
     bool on_std_out = outfile_arg == "-";
     std::unique_ptr<std::ostream> outfile =
-      on_std_out ? nullptr
-                 : open_outfile_and_check(outfile_arg, message_handler);
+      on_std_out
+        ? nullptr
+        : open_outfile_and_check(outfile_arg, message_handler, "--outfile");
     solver_process = util_make_unique<smt_incremental_dry_run_solvert>(
       message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
   }
   else
   {
+    const auto out_filename = options.get_option("dump-smt-formula");
+
+    // If no out_filename is provided `open_outfile_and_check` will return
+    // `nullptr`, and the solver will work normally without any logging.
     solver_process = util_make_unique<smt_piped_solver_processt>(
-      std::move(solver_command), message_handler);
+      std::move(solver_command),
+      message_handler,
+      open_outfile_and_check(
+        out_filename, message_handler, "--dump-smt-formula"));
   }
 
   return util_make_unique<solvert>(
@@ -432,7 +449,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
   }
   else
   {
-    auto out = open_outfile_and_check(filename, message_handler);
+    auto out = open_outfile_and_check(filename, message_handler, "--outfile");
 
     auto smt2_conv = util_make_unique<smt2_convt>(
       ns,
@@ -574,6 +591,10 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options)
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
 
+  if(cmdline.isset("dump-smt-formula"))
+    options.set_option(
+      "dump-smt-formula", cmdline.get_value("dump-smt-formula"));
+
   if(cmdline.isset("write-solver-stats-to"))
   {
     options.set_option(
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
@@ -113,6 +113,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(refine-arrays)"                                                            \
   "(refine-arithmetic)"                                                        \
   "(outfile):"                                                                 \
+  "(dump-smt-formula):"                                                        \
   "(write-solver-stats-to):"
 
 #define HELP_SOLVER                                                            \
@@ -140,6 +141,8 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "                              command to invoke external SMT solver for\n"  \
   "                              incremental solving (experimental)\n"         \
   " --outfile filename           output formula to given file\n"               \
+  " --dump-smt-formula filename  output smt incremental formula to the\n"      \
+  "                              given file\n"                                 \
   " --write-solver-stats-to json-file\n"                                       \
   "                              collect the solver query complexity\n"
 
diff --git a/src/solvers/smt2_incremental/smt_solver_process.cpp b/src/solvers/smt2_incremental/smt_solver_process.cpp
@@ -11,8 +11,10 @@
 
 smt_piped_solver_processt::smt_piped_solver_processt(
   std::string command_line,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  std::unique_ptr<std::ostream> out_stream)
   : command_line_description{"\"" + command_line + "\""},
+    out_stream(std::move(out_stream)),
     process{split_string(command_line, ' ', false, true), message_handler},
     log{message_handler}
 {
@@ -28,6 +30,15 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   const std::string command_string = smt_to_smt2_string(smt_command);
   log.debug() << "Sending command to SMT2 solver - " << command_string
               << messaget::eom;
+
+  if(out_stream != nullptr)
+  {
+    // Using `std::endl` instead of '\n' to also flush the stream as it is a
+    // debugging functionality, to guarantee a consistent output in case of
+    // hanging after `(check-sat)`
+    *out_stream << command_string << std::endl;
+  }
+
   const auto response = process.send(command_string + "\n");
   switch(response)
   {
diff --git a/src/solvers/smt2_incremental/smt_solver_process.h b/src/solvers/smt2_incremental/smt_solver_process.h
@@ -37,9 +37,12 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   ///   The command and arguments for invoking the smt2 solver.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
+  /// \param out_stream:
+  ///   Pointer to the stream to print the SMT formula. `nullptr` if no output.
   smt_piped_solver_processt(
     std::string command_line,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    std::unique_ptr<std::ostream> out_stream);
 
   const std::string &description() override;
 
@@ -54,6 +57,8 @@ class smt_piped_solver_processt : public smt_base_solver_processt
 protected:
   /// The command line used to start the process.
   std::string command_line_description;
+  /// Pointer to the stream to print the SMT formula. `nullptr` if no output.
+  std::unique_ptr<std::ostream> out_stream;
   /// The raw solver sub process.
   piped_processt process;
   /// For buffering / combining communications from the solver to cbmc.
