Merge pull request #6207 from thomasspriggs/tas/smt2_stream_consistency_for_develop

Fix bugs stemming from duplicate output streams in smt2_convt::write_footer()

Author: TGWDB

regression/cbmc/Malloc6/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/Pointer1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/Pointer28/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --little-endian
 ^EXIT=0$

regression/cbmc/Pointer4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/String8/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

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$

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$

regression/cbmc/null7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/struct7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

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$

src/solvers/smt2/smt2_conv.cpp

@@ -176,55 +176,55 @@ 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)
     define_object_size(object.second, object.first);
 
   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;
 }

src/solvers/smt2/smt2_conv.h

@@ -96,7 +96,16 @@ class smt2_convt : public stack_decision_proceduret
   resultt dec_solve() override;
 
   void write_header();
-  void write_footer(std::ostream &);
+  /// 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
   bool use_array_theory(const exprt &);

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<std::string> argv;
   std::string stdin_filename;

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);
 };