Log SMT formula to file for new incremental backend.

regression/CMakeLists.txt

@@ -34,6 +34,7 @@ add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
 add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-output-file)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)
 add_subdirectory(goto-instrument-chc)

regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc

@@ -0,0 +1,18 @@
+CORE
+test.c
+--outfile -
+Starting Bounded Model Checking
+^\(set-option :produce-models true\)$
+^\(set-logic ALL\)$
+^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec 64\)\)$
+^Passing problem to incremental SMT2 solving via SMT2 incremental dry-run$
+^\(define-fun B0 \(\) Bool true\)$
+^\(define-fun B2 \(\) Bool \(not false\)\)$
+^\(assert B2\)$
+^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 64\)\)\)$
+^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 64\)\)\)$
+^\(check-sat\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the `--outfile -` argument is used correctly.

regression/cbmc-output-file/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.py $<TARGET_FILE:cbmc>" "-f"
+)

regression/cbmc-output-file/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc'
+
+tests.log:
+	@../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc'
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/cbmc-output-file/chain.py

@@ -0,0 +1,71 @@
+#!/usr/bin/env python3
+
+import subprocess
+import sys
+import re
+
+
+class Options:
+    def __init__(self):
+        self.cmd_binary = sys.argv[1]
+        self.test_name = sys.argv[2]
+        self.cmd_options = sys.argv[3:]
+        self.outfile = self.test_name + "-out-file.out"
+        self.outfile_rules = self.test_name + "-out-file-rules.txt"
+
+    def __str__(self):
+        return """
+  cmd_binary: {},
+  test_name: {},
+  cmd_options: {},
+  outfile: {},
+  outfile_rules: {},
+        """.format(self.cmd_binary,
+                   self.test_name,
+                   self.cmd_options,
+                   self.outfile,
+                   self.outfile_rules)
+
+
+def try_compile_regex(regex_content):
+    try:
+        return re.compile(regex_content)
+    except re.error:
+        print("Bad regex: {}".format(regex_content))
+        raise
+
+
+def check_outfile(options):
+    with open(options.outfile) as outfile_f:
+        with open(options.outfile_rules) as outfile_rules_f:
+            unprocessed_outfile = outfile_f.readlines()
+            outfile_rules = [try_compile_regex(c) for c in outfile_rules_f.readlines()]
+            for rule in outfile_rules:
+                found = False
+                while not found:
+                    if len(unprocessed_outfile) == 0:
+                        return False
+                    match = rule.match(unprocessed_outfile[0])
+                    found = match is not None
+                    unprocessed_outfile = unprocessed_outfile[1:]
+    return True
+
+
+def main():
+    options = Options()
+    cmd_options = [options.outfile if item == '%out-file-name%' else item for item in
+                   options.cmd_options]
+    cmd_line = [options.cmd_binary] + cmd_options
+    print("Running: ", cmd_line)
+    subprocess.run(cmd_line)
+    print("\n--- Checking outfiles ---")
+    if check_outfile(options):
+        print("Output file matches.")
+        sys.exit(0)
+    else:
+        print("Output file does not match.")
+        sys.exit(1)
+
+
+if __name__ == "__main__":
+    main()

regression/cbmc-output-file/outfile/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\)

regression/cbmc-output-file/outfile/cvc5-match.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
+Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --outfile argument is used correctly and that the output file matches the
+rules defined in test-outfile-rules.txt

regression/cbmc-output-file/outfile/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\)

regression/cbmc-output-file/outfile/cvc5-no-match.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
+Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --outfile argument is used correctly and that the output file matches the
+rules defined in test-outfile-rules.txt

regression/cbmc-output-file/outfile/test.c

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

regression/cbmc-output-file/outfile/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\)

regression/cbmc-output-file/outfile/z3-match.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
+Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --outfile argument is used correctly and that the output file matches the
+rules defined in test-outfile-rules.txt

regression/cbmc-output-file/outfile/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\)

regression/cbmc-output-file/outfile/z3-no-match.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
+Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --outfile argument is used correctly and that the output file matches the
+rules defined in test-outfile-rules.txt

src/goto-checker/solver_factory.cpp

@@ -329,12 +329,54 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
+std::unique_ptr<std::ofstream> open_outfile_and_check(
+  const std::string &filename,
+  message_handlert &message_handler)
+{
+  if(filename.empty())
+    return nullptr;
+
+#ifdef _MSC_VER
+  auto out = util_make_unique<std::ofstream>(widen(filename));
+#else
+  auto out = util_make_unique<std::ofstream>(filename);
+#endif
+
+  if(!*out)
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "failed to open file: " + filename, "--outfile");
+  }
+
+  messaget log(message_handler);
+  log.status() << "Outputting SMTLib formula to file: " << filename
+               << messaget::eom;
+  return out;
+}
+
 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);
+
+  const std::string outfile_arg = options.get_option("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);
+    solver_process = util_make_unique<smt_incremental_dry_run_solvert>(
+      message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
+  }
+  else
+  {
+    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>(
@@ -390,17 +432,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
   }
   else
   {
-#ifdef _MSC_VER
-    auto out = util_make_unique<std::ofstream>(widen(filename));
-#else
-    auto out = util_make_unique<std::ofstream>(filename);
-#endif
-
-    if(!*out)
-    {
-      throw invalid_command_line_argument_exceptiont(
-        "failed to open file: " + filename, "--outfile");
-    }
+    auto out = open_outfile_and_check(filename, message_handler);
 
     auto smt2_conv = util_make_unique<smt2_convt>(
       ns,

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -68,3 +68,33 @@ smt_responset smt_piped_solver_processt::receive_response(
     handle_invalid_smt(*validation_errors, log);
   return *validation_result.get_if_valid();
 }
+
+smt_incremental_dry_run_solvert::smt_incremental_dry_run_solvert(
+  message_handlert &message_handler,
+  std::ostream &out_stream,
+  std::unique_ptr<std::ostream> file_stream)
+  : file_stream(std::move(file_stream)),
+    out_stream(out_stream),
+    log(message_handler)
+{
+}
+
+const std::string &smt_incremental_dry_run_solvert::description()
+{
+  return desc;
+}
+
+void smt_incremental_dry_run_solvert::send(const smt_commandt &smt_command)
+{
+  out_stream << smt_to_smt2_string(smt_command) << '\n';
+}
+
+smt_responset smt_incremental_dry_run_solvert::receive_response(
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+{
+  // Using `smt_unsat_responset` as response because the decision-procedure will
+  // terminate anyway (stop-on-fail), it is not reported to the user as for
+  // `unknown`, and does not trigger a subsequent invocation to get the model
+  // (as a `smt_sat_responset` answer will trigger).
+  return smt_check_sat_responset{smt_unsat_responset{}};
+}

src/solvers/smt2_incremental/smt_solver_process.h

@@ -5,10 +5,12 @@
 
 class smt_commandt;
 
-#include <solvers/smt2_incremental/smt_responses.h>
 #include <util/message.h>
 #include <util/piped_process.h>
 
+#include <solvers/smt2_incremental/smt_responses.h>
+
+#include <memory>
 #include <sstream>
 #include <string>
 
@@ -60,4 +62,45 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   messaget log;
 };
 
+/// Class for an incremental SMT solver used in combination with `--outfile`
+///    argument where the solver is never run.
+class smt_incremental_dry_run_solvert : public smt_base_solver_processt
+{
+public:
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  /// \param out_stream:
+  ///   Reference to the stream to print the SMT formula.
+  /// \param file_stream:
+  ///   Pointer to the file stream to print the SMT formula into. `nullptr` if
+  ///     output is to `std::cout`.
+  smt_incremental_dry_run_solvert(
+    message_handlert &message_handler,
+    std::ostream &out_stream,
+    std::unique_ptr<std::ostream> file_stream);
+
+  const std::string &description() override;
+
+  void send(const smt_commandt &smt_command) override;
+
+  /// \note This function returns always a valid unsat response.
+  smt_responset receive_response(
+    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+    override;
+
+  ~smt_incremental_dry_run_solvert() override = default;
+
+protected:
+  /// Pointer to the file stream to print the SMT formula. `nullptr` if output
+  ///    is to `std::cout`.
+  std::unique_ptr<std::ostream> file_stream;
+  /// The output stream reference to print the SMT formula to.
+  std::ostream &out_stream;
+  /// For debug printing.
+  messaget log;
+
+  /// Description of the current solver
+  const std::string desc = "SMT2 incremental dry-run";
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H