Log SMT formula to file for new incremental backend. #7126

esteffin · 2022-09-12T16:57:53Z

Add the possibility to log the SMT formula generated by the new SMT2 incremental backend to a file.

To use the feature add --outfile <filename> to command-line arguments.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-09-13T12:14:35Z

Codecov Report

Base: 77.88% // Head: 77.89% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (1dc2e03) compared to base (c764c1d).
Patch coverage: 91.66% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7126   +/-   ##
========================================
  Coverage    77.88%   77.89%           
========================================
  Files         1576     1576           
  Lines       181856   181886   +30     
========================================
+ Hits        141645   141675   +30     
  Misses       40211    40211

Impacted Files	Coverage Δ
src/util/expr.h	`97.02% <ø> (ø)`
src/goto-checker/solver_factory.cpp	`78.17% <86.95%> (+0.93%)`	⬆️
...rc/solvers/smt2_incremental/smt_solver_process.cpp	`79.16% <100.00%> (+9.72%)`	⬆️
src/solvers/smt2_incremental/smt_solver_process.h	`100.00% <100.00%> (ø)`

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

tautschnig · 2022-09-17T09:39:51Z

regression/cbmc-outfile/chain.py

@@ -0,0 +1,71 @@
+#!/usr/bin/env python3


Do we really need that script? Couldn't it also be done by using --outfile /dev/stdout?

Yes, unfortunately we need it as:

We test on windows where /dev/stdout may not work

By adding --outfile /dev/stdout we will know that the SMT formula is printed on the screen, not that it is added to the out file, so we cannot distinguish file from normal output.

The way the test output is checked is not in a certain order while the python script enforce a certain ordering, so if we want to have 2 (check-sat) calls the old system will be satisfied with one (check-sat) in the output, the new one instead will require 2 in the specified order

I believe you can use - instead of /dev/stdout, which will then work across platforms.

Granted, but I'm not sure this one aspect is a sufficient reason to warrant yet another piece of code that needs to be maintained.

You can use activate-multi-line-match to handle this case.

I don't intend to block on that, but every line of code that is written has a (future) cost. So I ask for careful consideration whether this really is needed.

Unfortunately in the new SMT backend we do not support the old --outfile - behaviour as, because of the interactive behaviour, the output will be interleaved with other messages (defying the sense of --outfile).
It is still possible to get the SMT formula on the stdout by using --verbosity 10 and then filtering the lines sent to the solver.

Hmm, good point. So I guess you have to keep the Python script, and I'm just hoping it won't break...

I believe you can use - instead of /dev/stdout, which will then work across platforms.

The - option is special cased in the solver factory. So tests which rely on this aren't fully testing the code path for writing to file.

I think this python script has value beyond the new incremental smt backend, because it could also be used to test the dimacs output for example.

tautschnig · 2022-09-21T15:32:01Z

src/solvers/smt2_incremental/smt_solver_process.cpp

+    // Using std::endl to flush the stream as it is a debugging functionality,
+    // and we can guarantee a consistent output in case of hanging after
+    // (check-sat)
+    *out_stream << command_string << std::endl;


Do you perhaps just want to use std::flush instead? Most of the comment would remain useful to keep, though.

As we want a new line and a flush I prefer std::endl instead of adding a new line + adding an explicit std::flush.

Ok, but then you might want the comment to say "Using std::endl instead of \n"

tautschnig · 2022-09-21T15:32:11Z

src/solvers/smt2_incremental/smt_solver_process.h

@@ -35,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.


tautschnig · 2022-09-21T15:33:16Z

src/solvers/smt2_incremental/smt_solver_process.h

  smt_piped_solver_processt(
    std::string command_line,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    std::unique_ptr<std::ostream> out_stream);


Is passing the std::unique_ptr by value rather than as a reference the right thing to do?

Yes as we want to extend the lifetime of the passed stream to the one of the smt_solver_proces object that is longer than the one of the solver_factory where the pointer is created.

tautschnig · 2022-09-21T15:36:06Z

src/cbmc/cbmc_parse_options.cpp

+  if(
+    cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") ||
+    (cmdline.isset("outfile") && !cmdline.isset("incremental-smt2-solver")))
+  {
    options.set_option("stop-on-fail", true);
+  }


I'm either failing to parse the commit message or don't understand why the incremental SMT2 solver now interacts with "outfile" in this way. Is it the case that "outfile" has a very different semantics with the incremental SMT2 solver?! Does not seem like a good idea.

If we stop on fail, then we stop processing after the first round of solving. If we want to dump the SMT2 formula to file for all rounds of solving for ease of debugging (human reading) of the written file then we need to not stop on failure. Otherwise only the first round of solving is written to file, because we stopped on failure.

My somewhat related question would be why do we automatically stop on failure when --outfile is used with any of the decision procedures?

To your "somewhat related question:" no actual solving takes place with other back-ends with --outfile, and also: what would be the semantics of having only a single output file but multiple formulae having to be written?

So if the incremental SMT2 back-end has substantially different behaviour (solving actually takes place, multiple formulae are written) then we really shouldn't be using the same command-line option name. This confusing user-experience is a blocker.

Otherwise only the first round of solving is written to file, because we stopped on failure.

But if you specified --stop-on-fail then this is exactly what you asked for. So, I don't see the point of having special behaviour here, @thomasspriggs. If you want all rounds to be written to the file then remove the --stop-on-fail flag.

But this is for when we aren't explicitly specifying --stop-on-fail. The argument parsing is currently adding "stop-on-fail" implicitly when --outfile is specified. Do we need to add an explicit --continue-on-fail to override the implicit option?

I see. Then I'd call the current behaviour somewhat confusing... not sure how to fix that without having different behaviour for incremental vs non-incremental, or having multiple options. (Definitely not a --continue-on-fail option)

thomasspriggs

Partial review only.

thomasspriggs · 2022-09-16T13:22:05Z

src/goto-checker/solver_factory.cpp

+    {
+      throw invalid_command_line_argument_exceptiont(
+        "failed to open file: " + outfile, "--outfile");
+    }


⛏️ This section of code appears to have been duplicated from the get_smt2, can you separate it into a function. I guess the function should take the (potentially empty) outfile string and either throw or return an std::unique_ptr<std::ofstream>.

thomasspriggs · 2022-09-21T15:50:19Z

src/cbmc/cbmc_parse_options.cpp

+  if(
+    cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") ||
+    (cmdline.isset("outfile") && !cmdline.isset("incremental-smt2-solver")))
+  {
    options.set_option("stop-on-fail", true);
+  }


If we stop on fail, then we stop processing after the first round of solving. If we want to dump the SMT2 formula to file for all rounds of solving for ease of debugging (human reading) of the written file then we need to not stop on failure. Otherwise only the first round of solving is written to file, because we stopped on failure.

My somewhat related question would be why do we automatically stop on failure when --outfile is used with any of the decision procedures?

NlightNFotis · 2022-09-21T15:59:03Z

src/solvers/smt2_incremental/smt_solver_process.cpp

+    // Using std::endl to flush the stream as it is a debugging functionality,
+    // and we can guarantee a consistent output in case of hanging after
+    // (check-sat)
+    *out_stream << command_string << std::endl;


Does it make sense to print a message that this action has been performed? E.g.

std::cout << "Outputting SMTLib to $file"

Probably somewhere else (constructor maybe?) so that the user can see what's going on (now I can use that, but there's no indication that this worked at all, which I found a bit surprising).

thomasspriggs · 2022-09-27T10:18:50Z

Re-opened as it was closed in error.

esteffin · 2022-09-27T10:29:49Z

Due to review comments, some extra work has been done so that now the --outfile works as with other backends (including --outfile - that will log on stdout.
Also when --outfile is added no SMT solver will be run.

There will be a subsequent PR that will add a new argument --dump-smt-formula that will log the SMT formula to a file while the SMT solver is also run (no stop-on-fail behaviour).

thomasspriggs

👍

src/goto-checker/solver_factory.cpp

src/solvers/smt2_incremental/smt_solver_process.cpp

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

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

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

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

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

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

esteffin · 2022-09-28T12:58:22Z

@tautschnig I think the new reworked commits should address your comments and concerns, especially as now the old --outfile behaviour has been restored.
Can you please double check this and if all good approve this PR?

esteffin requested a review from thomasspriggs September 12, 2022 16:58

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from 0bf0711 to a506981 Compare September 13, 2022 11:00

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from a506981 to 43439bc Compare September 16, 2022 13:13

esteffin marked this pull request as ready for review September 16, 2022 13:13

esteffin requested review from peterschrammel, NlightNFotis, TGWDB, chris-ryder, kroening and tautschnig as code owners September 16, 2022 13:13

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from 43439bc to b2b7199 Compare September 16, 2022 17:06

tautschnig self-assigned this Sep 17, 2022

tautschnig reviewed Sep 17, 2022

View reviewed changes

tautschnig removed their assignment Sep 17, 2022

tautschnig reviewed Sep 21, 2022

View reviewed changes

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from b2b7199 to ca83774 Compare September 21, 2022 15:48

thomasspriggs reviewed Sep 21, 2022

View reviewed changes

NlightNFotis reviewed Sep 21, 2022

View reviewed changes

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from ca83774 to 95a411c Compare September 22, 2022 17:20

esteffin closed this Sep 26, 2022

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from 95a411c to 06b377d Compare September 26, 2022 23:58

thomasspriggs reopened this Sep 27, 2022

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from ecfd902 to 7fd76e6 Compare September 27, 2022 10:24

esteffin requested review from thomasspriggs September 27, 2022 10:25

esteffin requested review from NlightNFotis and tautschnig September 27, 2022 10:30

esteffin force-pushed the esteffin/log-smt-formula-to-file branch 5 times, most recently from 5f22a32 to 821b9ad Compare September 27, 2022 16:09

thomasspriggs approved these changes Sep 27, 2022

View reviewed changes

Enrico Steffinlongo added 2 commits September 27, 2022 20:09

Log SMT formula to file for new incremental solver

21d4907

Add regression tests for --outfile argument

1dc2e03

esteffin force-pushed the esteffin/log-smt-formula-to-file branch from 821b9ad to 1dc2e03 Compare September 27, 2022 19:09

thomasspriggs approved these changes Sep 28, 2022

View reviewed changes

esteffin mentioned this pull request Sep 28, 2022

Log to file the SMT formula run by the solver #7161

Merged

7 tasks

peterschrammel approved these changes Sep 29, 2022

View reviewed changes

kroening merged commit 66f913e into diffblue:develop Sep 29, 2022

Log SMT formula to file for new incremental backend. #7126

Log SMT formula to file for new incremental backend. #7126

Uh oh!

Conversation

esteffin commented Sep 12, 2022

Uh oh!

codecov bot commented Sep 13, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

esteffin Sep 20, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel Sep 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel Sep 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Sep 27, 2022

Uh oh!

esteffin commented Sep 27, 2022

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

esteffin commented Sep 28, 2022

codecov bot commented Sep 13, 2022 •

edited

Loading

esteffin Sep 20, 2022 •

edited

Loading

peterschrammel Sep 21, 2022 •

edited

Loading

peterschrammel Sep 21, 2022 •

edited

Loading