bump cbmc dependency

Author: kroening

.github/workflows/pull-request-checks.yaml

@@ -104,7 +104,7 @@ jobs:
   # This job takes approximately 15 minutes
   check-centos8-make-gcc:
     name: CentOS 8
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-22.04
     container:
       image: centos:8
     steps:
@@ -134,7 +134,7 @@ jobs:
       - name: Get minisat
         run: make -C lib/cbmc/src minisat2-download
       - name: Build with make
-        run: make CXX="ccache g++" -C src -j2
+        run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j2
       - name: Run the ebmc tests with SAT
         run: |
           rm regression/ebmc/neural-liveness/counter1.desc

lib/cbmc

@@ -8,15 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "aiger_language.h"
 
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, [email protected]
-
-\*******************************************************************/
-
-#include "aiger_language.h"
+#include <util/message.h>
 
 /*******************************************************************\
 
@@ -31,8 +23,9 @@ Function: aiger_languaget::parse
 \*******************************************************************/
 
 bool aiger_languaget::parse(
-  std::istream &instream,
-  const std::string &path)
+  std::istream &,
+  const std::string &,
+  message_handlert &)
 {
   return true;
 }
@@ -50,11 +43,13 @@ Function: aiger_languaget::preprocess
 \*******************************************************************/
 
 bool aiger_languaget::preprocess(
-  std::istream &instream,
-  const std::string &path,
-  std::ostream &outstream)
+  std::istream &,
+  const std::string &,
+  std::ostream &,
+  message_handlert &message_handler)
 {
-  error() << "there is no AIGER preprocessing" << eom;
+  messaget message(message_handler);
+  message.error() << "there is no AIGER preprocessing" << messaget::eom;
   return true;
 }
 
@@ -106,8 +101,9 @@ Function: aiger_languaget::typecheck
 \*******************************************************************/
 
 bool aiger_languaget::typecheck(
-  symbol_table_baset &symbol_table,
-  const std::string &module)
+  symbol_table_baset &,
+  const std::string &,
+  message_handlert &)
 {
   return true;
 }
@@ -124,7 +120,7 @@ Function: aiger_languaget::interfaces
 
 \*******************************************************************/
 
-bool aiger_languaget::interfaces(symbol_table_baset &symbol_table)
+bool aiger_languaget::interfaces(symbol_table_baset &, message_handlert &)
 {
   return false;
 }
@@ -140,8 +136,8 @@ Function: aiger_languaget::show_parse
  Purpose:
 
 \*******************************************************************/
-  
-void aiger_languaget::show_parse(std::ostream &out)
+
+void aiger_languaget::show_parse(std::ostream &, message_handlert &)
 {
 }
 
@@ -200,8 +196,9 @@ Function: aiger_languaget::to_expr
 bool aiger_languaget::to_expr(
   const std::string &code,
   const std::string &module,
-  exprt &expr,
-  const namespacet &ns)
+  exprt &,
+  const namespacet &,
+  message_handlert &)
 {
   return true;
 }

src/aiger/aiger_language.cpp

@@ -17,27 +17,30 @@ class aiger_languaget:public languaget
 {
 public:
   bool preprocess(
-    std::istream &instream,
+    std::istream &,
     const std::string &path,
-    std::ostream &outstream) override;
+    std::ostream &,
+    message_handlert &) override;
+
+  bool
+  parse(std::istream &, const std::string &path, message_handlert &) override;
 
-  bool parse(
-    std::istream &instream,
-    const std::string &path) override;
-             
   void dependencies(
     const std::string &module,
     std::set<std::string> &module_set) override;
 
   void modules_provided(
     std::set<std::string> &module_set) override;
 
-  bool interfaces(symbol_table_baset &) override;
+  bool interfaces(symbol_table_baset &, message_handlert &) override;
 
-  bool typecheck(symbol_table_baset &, const std::string &module) override;
+  bool typecheck(
+    symbol_table_baset &,
+    const std::string &module,
+    message_handlert &) override;
+
+  void show_parse(std::ostream &, message_handlert &) override;
 
-  void show_parse(std::ostream &out) override;
-  
   ~aiger_languaget() override { }
 
   bool from_expr(
@@ -51,10 +54,12 @@ class aiger_languaget:public languaget
   bool to_expr(
     const std::string &code,
     const std::string &module,
-    exprt &expr,
-    const namespacet &ns) override;
+    exprt &,
+    const namespacet &,
+    message_handlert &) override;
 
-  bool generate_support_functions(symbol_table_baset &) override
+  bool
+  generate_support_functions(symbol_table_baset &, message_handlert &) override
   {
     return false;
   }

src/aiger/aiger_language.h

@@ -71,8 +71,6 @@ endif
 include ../config.inc
 include ../common
 
-LIBS = ../ic3/minisat/build/release/lib/libminisat.a
-
 CLEANFILES = ebmc$(EXEEXT)
 
 all: ebmc$(EXEEXT)
@@ -87,5 +85,5 @@ endif
 
 ###############################################################################
 
-ebmc$(EXEEXT): $(OBJ)
+ebmc$(EXEEXT): $(OBJ) ../ic3/minisat/build/release/lib/libminisat.a
 	$(LINKBIN)

src/ebmc/Makefile

@@ -33,7 +33,7 @@ void bmc(
   const namespacet ns(transition_system.symbol_table);
 
   auto solver_wrapper = solver_factory(ns, message_handler);
-  auto &solver = solver_wrapper.stack_decision_procedure();
+  auto &solver = solver_wrapper.decision_procedure();
 
   ::unwind(
     transition_system.trans_expr, message_handler, solver, bound + 1, ns, true);
@@ -87,18 +87,9 @@ void bmc(
 
       message.status() << "Checking " << property.name << messaget::eom;
 
-      auto constraint = not_exprt(conjunction(property.timeframe_handles));
-      auto handle = solver.handle(constraint);
-      if(handle.is_true())
-        solver.push({literal_exprt(const_literal(true))});
-      else if(handle.is_false())
-        solver.push({literal_exprt(const_literal(false))});
-      else
-        solver.push({solver.handle(constraint)});
+      auto assumption = not_exprt(conjunction(property.timeframe_handles));
 
-      decision_proceduret::resultt dec_result = solver();
-
-      solver.pop();
+      decision_proceduret::resultt dec_result = solver(assumption);
 
       switch(dec_result)
       {

src/ebmc/bmc.cpp

@@ -25,7 +25,7 @@ class ebmc_errort
     return message;
   }
 
-  optionalt<int> exit_code() const
+  std::optional<int> exit_code() const
   {
     return __exit_code;
   }
@@ -49,7 +49,7 @@ class ebmc_errort
 
 protected:
   std::ostringstream message;
-  optionalt<int> __exit_code = {};
+  std::optional<int> __exit_code = {};
   source_locationt __location = source_locationt::nil();
 };
 

src/ebmc/ebmc_error.h

@@ -128,14 +128,13 @@ ebmc_propertiest ebmc_propertiest::from_command_line(
 
     auto property_string = cmdline.get_value('p');
 
-    language->set_message_handler(message_handler);
-
     exprt expr;
     if(language->to_expr(
          property_string,
          id2string(transition_system.main_symbol->module),
          expr,
-         ns))
+         ns,
+         message_handler))
     {
       throw ebmc_errort() << "failed to parse the given property expression";
     }

src/ebmc/ebmc_properties.cpp

@@ -56,7 +56,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
     }
   }
 
-  optionalt<smt2_convt::solvert> smt2_solver =
+  std::optional<smt2_convt::solvert> smt2_solver =
     cmdline.isset("bitwuzla")    ? smt2_convt::solvert::BITWUZLA
     : cmdline.isset("boolector") ? smt2_convt::solvert::BOOLECTOR
     : cmdline.isset("cvc3")      ? smt2_convt::solvert::CVC3
@@ -66,7 +66,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
     : cmdline.isset("yices")     ? smt2_convt::solvert::YICES
     : cmdline.isset("z3")        ? smt2_convt::solvert::Z3
     : cmdline.isset("smt2")      ? smt2_convt::solvert::GENERIC
-                                 : optionalt<smt2_convt::solvert>{};
+                                 : std::optional<smt2_convt::solvert>{};
 
   if(cmdline.isset("outfile"))
   {

src/ebmc/ebmc_solver_factory.cpp

@@ -13,30 +13,30 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/namespace.h>
 
+#include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
-#include <solvers/stack_decision_procedure.h>
 
 #include <iosfwd>
 #include <memory>
 
 class ebmc_solvert final
 {
 public:
-  explicit ebmc_solvert(std::unique_ptr<stack_decision_proceduret> p)
+  explicit ebmc_solvert(std::unique_ptr<decision_proceduret> p)
     : decision_procedure_ptr(std::move(p))
   {
   }
 
   ebmc_solvert(
     std::unique_ptr<propt> p1,
-    std::unique_ptr<stack_decision_proceduret> p2)
+    std::unique_ptr<decision_proceduret> p2)
     : prop_ptr(std::move(p1)), decision_procedure_ptr(std::move(p2))
   {
   }
 
   ebmc_solvert(
     std::unique_ptr<std::ofstream> p1,
-    std::unique_ptr<stack_decision_proceduret> p2)
+    std::unique_ptr<decision_proceduret> p2)
     : ofstream_ptr(std::move(p1)), decision_procedure_ptr(std::move(p2))
   {
   }
@@ -47,16 +47,10 @@ class ebmc_solvert final
     return *decision_procedure_ptr;
   }
 
-  stack_decision_proceduret &stack_decision_procedure() const
-  {
-    PRECONDITION(decision_procedure_ptr);
-    return *decision_procedure_ptr;
-  }
-
   // the objects are deleted in the opposite order they appear below
   std::unique_ptr<std::ofstream> ofstream_ptr;
   std::unique_ptr<propt> prop_ptr;
-  std::unique_ptr<stack_decision_proceduret> decision_procedure_ptr;
+  std::unique_ptr<decision_proceduret> decision_procedure_ptr;
 };
 
 using ebmc_solver_factoryt =