From 1d6d39b5a488e35218bc8f054dbbd02931f3b264 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 25 Jun 2021 18:26:02 +0100 Subject: [PATCH 1/2] Deduplicate output streams in `smt2_convt::write_footer()` 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. --- regression/cbmc/Malloc6/test.desc | 2 +- regression/cbmc/Pointer1/test.desc | 2 +- regression/cbmc/Pointer28/test.desc | 2 +- regression/cbmc/Pointer4/test.desc | 2 +- regression/cbmc/String8/test.desc | 2 +- regression/cbmc/String_Abstraction7/test.desc | 2 +- .../cbmc/address_space_size_limit3/test.desc | 2 +- regression/cbmc/null7/test.desc | 2 +- regression/cbmc/struct7/test.desc | 2 +- regression/cbmc/void_pointer2/test.desc | 2 +- src/solvers/smt2/smt2_conv.cpp | 34 +++++++++---------- src/solvers/smt2/smt2_conv.h | 2 +- src/solvers/smt2/smt2_dec.cpp | 16 +++++---- src/solvers/smt2/smt2_dec.h | 4 +++ 14 files changed, 41 insertions(+), 35 deletions(-) diff --git a/regression/cbmc/Malloc6/test.desc b/regression/cbmc/Malloc6/test.desc index 5e4496882a0..7561cd38b9b 100644 --- a/regression/cbmc/Malloc6/test.desc +++ b/regression/cbmc/Malloc6/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer1/test.desc b/regression/cbmc/Pointer1/test.desc index 5136794fb58..39c491ba8bb 100644 --- a/regression/cbmc/Pointer1/test.desc +++ b/regression/cbmc/Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer28/test.desc b/regression/cbmc/Pointer28/test.desc index b0acb9b5913..f5e039ba3ed 100644 --- a/regression/cbmc/Pointer28/test.desc +++ b/regression/cbmc/Pointer28/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer4/test.desc b/regression/cbmc/Pointer4/test.desc index 5136794fb58..39c491ba8bb 100644 --- a/regression/cbmc/Pointer4/test.desc +++ b/regression/cbmc/Pointer4/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/String8/test.desc b/regression/cbmc/String8/test.desc index 35db6e71ddb..96c9b4bcd7b 100644 --- a/regression/cbmc/String8/test.desc +++ b/regression/cbmc/String8/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction7/test.desc b/regression/cbmc/String_Abstraction7/test.desc index fb3f890f27f..e6fb3bba609 100644 --- a/regression/cbmc/String_Abstraction7/test.desc +++ b/regression/cbmc/String_Abstraction7/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc index ac8f72553aa..a157f11a7f4 100644 --- a/regression/cbmc/address_space_size_limit3/test.desc +++ b/regression/cbmc/address_space_size_limit3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend main.i --32 --little-endian --object-bits 25 --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/null7/test.desc b/regression/cbmc/null7/test.desc index 7937640a49b..45989540170 100644 --- a/regression/cbmc/null7/test.desc +++ b/regression/cbmc/null7/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc index 35db6e71ddb..96c9b4bcd7b 100644 --- a/regression/cbmc/struct7/test.desc +++ b/regression/cbmc/struct7/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc index a59cfa54721..3556481d977 100644 --- a/regression/cbmc/void_pointer2/test.desc +++ b/regression/cbmc/void_pointer2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --no-simplify --unwind 3 ^EXIT=0$ diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 9c05dcbcba8..289beb85509 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -176,9 +176,9 @@ void smt2_convt::write_header() out << "(set-logic " << logic << ")" << "\n"; } -void smt2_convt::write_footer(std::ostream &os) +void smt2_convt::write_footer() { - os << "\n"; + out << "\n"; // fix up the object sizes for(const auto &object : object_sizes) @@ -186,45 +186,45 @@ void smt2_convt::write_footer(std::ostream &os) if(use_check_sat_assuming && !assumptions.empty()) { - os << "(check-sat-assuming ("; + out << "(check-sat-assuming ("; for(const auto &assumption : assumptions) convert_literal(to_literal_expr(assumption).get_literal()); - os << "))\n"; + out << "))\n"; } else { // add the assumptions, if any if(!assumptions.empty()) { - os << "; assumptions\n"; + out << "; assumptions\n"; for(const auto &assumption : assumptions) { - os << "(assert "; + out << "(assert "; convert_literal(to_literal_expr(assumption).get_literal()); - os << ")" - << "\n"; + out << ")" + << "\n"; } } - os << "(check-sat)\n"; + out << "(check-sat)\n"; } - os << "\n"; + out << "\n"; if(solver!=solvert::BOOLECTOR) { for(const auto &id : smt2_identifiers) - os << "(get-value (|" << id << "|))" - << "\n"; + out << "(get-value (|" << id << "|))" + << "\n"; } - os << "\n"; + out << "\n"; - os << "(exit)\n"; + out << "(exit)\n"; - os << "; end of SMT2 file" - << "\n"; + out << "; end of SMT2 file" + << "\n"; } void smt2_convt::define_object_size( @@ -267,7 +267,7 @@ void smt2_convt::define_object_size( decision_proceduret::resultt smt2_convt::dec_solve() { - write_footer(out); + write_footer(); out.flush(); return decision_proceduret::resultt::D_ERROR; } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 3c812d5c341..e3eee89279b 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -96,7 +96,7 @@ class smt2_convt : public stack_decision_proceduret resultt dec_solve() override; void write_header(); - void write_footer(std::ostream &); + void write_footer(); // tweaks for arrays bool use_array_theory(const exprt &); diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index cf420233477..5a2979707fb 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -39,13 +39,15 @@ decision_proceduret::resultt smt2_dect::dec_solve() temp_file_stdout("smt2_dec_stdout_", ""), temp_file_stderr("smt2_dec_stderr_", ""); - { - // we write the problem into a file - std::ofstream problem_out( - temp_file_problem(), std::ios_base::out | std::ios_base::trunc); - problem_out << stringstream.str(); - write_footer(problem_out); - } + const auto write_problem_to_file = [&](std::ofstream problem_out) { + cached_output << stringstream.str(); + stringstream.str(std::string{}); + write_footer(); + problem_out << cached_output.str() << stringstream.str(); + stringstream.str(std::string{}); + }; + write_problem_to_file(std::ofstream( + temp_file_problem(), std::ios_base::out | std::ios_base::trunc)); std::vector argv; std::string stdin_filename; diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index 1ee4f814a96..dd9872ffc0a 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -45,6 +45,10 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt protected: message_handlert &message_handler; + /// Everything except the footer is cached, so that output files can be + /// rewritten with varying footers. + std::stringstream cached_output; + resultt read_result(std::istream &in); }; From b68902f60cd2779541d9361112adecfb227e9895 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 29 Jun 2021 11:18:52 +0100 Subject: [PATCH 2/2] Add doxygen of `smt_convt::write_footer` This is worth explaining because it is no longer clear where the output is written to based on the arguments/usage. --- src/solvers/smt2/smt2_conv.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index e3eee89279b..e1a65ff2fb5 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -96,6 +96,15 @@ class smt2_convt : public stack_decision_proceduret resultt dec_solve() override; void write_header(); + /// Writes the end of the SMT file to the `smt_convt::out` stream. These parts + /// of the output may be changed when using multiple rounds of solving. They + /// include the following parts of the output file - + /// * The object size definitions. + /// * The assertions based on the `assumptions` member variable. + /// * The `(check-sat)` or `check-sat-assuming` command. + /// * A `(get-value |identifier|)` command for each of the identifiers in + /// `smt2_convt::smt2_identifiers`. + /// * An `(exit)` command. void write_footer(); // tweaks for arrays