Fix bugs stemming from duplicate output streams in smt2_convt::write_footer() #6207
Conversation
This fixes bugs arising from some of the member functions of `smt2::convt` writing to an `os` argument and some of the them writing to `smt2_convt::out`. This was causing some of the generated text to be written out when using `--outfile` argument with cbmc, but not without it. It might be easier to understand `smt2_convt` if the output stream was passed as an argument to the member functions, instead of kept as a member variable. This commit replaces the arguments with references to the member variable because it is a less wide sweeping change and it still solves the bugs. The address_space_size_limit3 test is disabled with smt2, because the output of this test was already different between the sat and smt2 backends and therefore it was already not producing the correct output. Presumably this test was returning the expected `VERIFICATION FAILED` result for the wrong reasons. The `VERIFICATION FAILED` result is only returned in the case where the object size limits are missing. Further work will be needed to properly debug the support for `--pointer-check` with smt2.
This is worth explaining because it is no longer clear where the output is written to based on the arguments/usage.
thomasspriggs
requested review from
allredj,
kroening,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6207 +/- ##
===========================================
+ Coverage 67.40% 75.39% +7.98%
===========================================
Files 1157 1456 +299
Lines 95236 161216 +65980
===========================================
+ Hits 64197 121544 +57347
- Misses 31039 39672 +8633
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
| @@ -1,4 +1,4 @@ | |||
| CORE | |||
| CORE broken-smt-backend | |||
There was a problem hiding this comment.
Why has this now broken?
| problem_out << stringstream.str(); | ||
| write_footer(problem_out); | ||
| } | ||
| const auto write_problem_to_file = [&](std::ofstream problem_out) { |
There was a problem hiding this comment.
This seems longer, more complex and harder to debug than the code it replaces. What am I missing?
There was a problem hiding this comment.
The old code would do the following:
- Write the internal stored string stream to file
- Call the footer to explicitly write to the file
The problem was that the write_footer call would call another function (define_object_size) that would write to the internal string stream.
The desirable behaviour is to do the following:
- Have stored string of the SMT that can be used for multiple calls to the solver
- Write this stored string to the file
- Add a footer to the file with the specific details of the current call/check (e.g. assumptions and
check-sat-assuming).
The modified code stores the common SMT to the cached_output and then writes this at the beginning of each call. The write_footer function (and called functions such as define_object_size) now write to the same internal string stream as all the other SMT conversion code (reducing future misunderstandings like this fixes). The internal string stream is cleared before writing the footer and after, to ensure no accidental duplication of SMT instructions/data.
I hope this has helped clarify.
|
I believe this also fixes #5952 |
This fixes bugs arising from some of the member functions of
smt2::convtwriting to anosargument and some of the them writingto
smt2_convt::out. This was causing some of the generated text to bewritten out when using
--outfileargument with cbmc, but not withoutit.
My commit message includes data points confirming performance improvements (if claimed).