Update to CBMC 5.12

regression/memsafety/built_from_end_false/test.desc

@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.17\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE
+\[main.pointer_dereference.17\] dereference failure: deallocated dynamic object in p->n: FAILURE

regression/memsafety/simple_false/test.desc

@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.38\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE
+\[main.pointer_dereference.38\] dereference failure: deallocated dynamic object in p->n: FAILURE

regression/termination/precond_term1/test.desc

@@ -1,6 +1,17 @@
-CORE
+KNOWNBUG
 main.c
 --preconditions
 ^EXIT=5$
 ^SIGNAL=0$
 \[__CPROVER__start\]: !\(argc' <= 1 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -1\)
+--
+--
+CBMC 5.12 introduced significant changes to solvers and this test failure
+seems to be one of its consequences. The formulae pushed into the solver
+seem to be identical to the previous 2LS version, however the solver in
+SSA analyzer then throws UNSAT on the first iteration when doing
+backward analysis (the invariants up until that point are correct)
+resulting in no improvements done to the template.
+
+This problem will require further investigation once the CBMC rebase
+is complete

src/2ls/2ls_parse_options.cpp

@@ -69,7 +69,7 @@ Author: Daniel Kroening, Peter Schrammel
 #define FILTER_ASSERTIONS 1
 
 twols_parse_optionst::twols_parse_optionst(int argc, const char **argv):
-  parse_options_baset(TWOLS_OPTIONS, argc, argv),
+  parse_options_baset(TWOLS_OPTIONS, argc, argv, "2LS " TWOLS_VERSION),
   messaget(ui_message_handler),
   ui_message_handler(cmdline, "2LS " TWOLS_VERSION),
   recursion_detected(false),
@@ -630,34 +630,43 @@ int twols_parse_optionst::doit()
     // do actual analysis
     switch((*checker)(goto_model))
     {
-    case property_checkert::resultt::PASS:
+    case resultt::PASS:
       if(report_assertions)
-        report_properties(options, goto_model, checker->property_map);
+        report_properties(
+          options,
+          goto_model,
+          checker->property_map,
+          checker->traces);
       report_success();
       if(cmdline.isset("graphml-witness"))
         output_graphml_proof(options, goto_model, *checker);
       retval=0;
       break;
 
-    case property_checkert::resultt::FAIL:
+    case resultt::FAIL:
     {
       if(report_assertions)
-        report_properties(options, goto_model, checker->property_map);
+        report_properties(
+          options,
+          goto_model,
+          checker->property_map,
+          checker->traces);
 
       // validate trace
       bool trace_valid=false;
       for(const auto &p : checker->property_map)
       {
-        if(p.second.result!=property_checkert::resultt::FAIL)
+        if(p.second.status!=property_statust::FAIL)
           continue;
 
+        goto_tracet trace=checker->traces[p.first];
         if(options.get_bool_option("trace"))
-          show_counterexample(goto_model, p.second.error_trace);
+          show_counterexample(goto_model, trace);
 
         trace_valid=
-          !p.second.error_trace.steps.empty() &&
+          !trace.steps.empty() &&
           (options.get_bool_option("nontermination") ||
-           p.second.error_trace.steps.back().is_assert());
+           trace.steps.back().is_assert());
         break;
       }
 
@@ -678,9 +687,13 @@ int twols_parse_optionst::doit()
       retval=10;
       break;
     }
-    case property_checkert::resultt::UNKNOWN:
+    case resultt::UNKNOWN:
       if(report_assertions)
-        report_properties(options, goto_model, checker->property_map);
+        report_properties(
+          options,
+          goto_model,
+          checker->property_map,
+          checker->traces);
       retval=5;
       report_unknown();
       break;
@@ -693,6 +706,7 @@ int twols_parse_optionst::doit()
     {
       checker->instrument_and_output(
         goto_model,
+        ui_message_handler,
         ui_message_handler.get_verbosity());
     }
 
@@ -1128,10 +1142,7 @@ bool twols_parse_optionst::process_goto_program(
 
     if(cmdline.isset("show-properties"))
     {
-      show_properties(
-        goto_model,
-        get_message_handler(),
-        ui_message_handler.get_ui());
+      show_properties(goto_model, ui_message_handler);
       return true;
     }
 
@@ -1143,8 +1154,7 @@ bool twols_parse_optionst::process_goto_program(
     {
       show_goto_functions(
         goto_model,
-        get_message_handler(),
-        ui_message_handler.get_ui(),
+        ui_message_handler,
         false);
       return true;
     }
@@ -1179,9 +1189,10 @@ bool twols_parse_optionst::process_goto_program(
 void twols_parse_optionst::report_properties(
   const optionst &options,
   const goto_modelt &goto_model,
-  const property_checkert::property_mapt &property_map)
+  const propertiest &property_map,
+  const tracest &traces)
 {
-  for(property_checkert::property_mapt::const_iterator
+  for(propertiest::const_iterator
         it=property_map.begin();
       it!=property_map.end();
       it++)
@@ -1193,7 +1204,7 @@ void twols_parse_optionst::report_properties(
 #endif
 
     if(!options.get_bool_option("all-properties") &&
-       it->second.result!=property_checkert::resultt::FAIL)
+       it->second.status!=property_statust::FAIL)
       continue;
 
     if(ui_message_handler.get_ui()==ui_message_handlert::uit::XML_UI)
@@ -1202,27 +1213,27 @@ void twols_parse_optionst::report_properties(
       xml_result.set_attribute("property", id2string(it->first));
       xml_result.set_attribute(
         "status",
-        property_checkert::as_string(it->second.result));
+        as_string(it->second.status));
       std::cout << xml_result << "\n";
     }
     else
     {
       status() << "[" << it->first << "] "
-               << it->second.location->source_location.get_comment()
+               << it->second.pc->source_location.get_comment()
                << ": "
-               << property_checkert::as_string(it->second.result)
+               << as_string(it->second.status)
                << eom;
     }
 
     if(options.get_bool_option("trace") &&
-       it->second.result==property_checkert::resultt::FAIL)
-      show_counterexample(goto_model, it->second.error_trace);
+       it->second.status==property_statust::FAIL)
+      show_counterexample(goto_model, traces.at(it->first));
     if(cmdline.isset("json-cex") &&
-       it->second.result==property_checkert::resultt::FAIL)
+       it->second.status==property_statust::FAIL)
       output_json_cex(
         options,
         goto_model,
-        it->second.error_trace,
+        traces.at(it->first),
         id2string(it->first));
   }
 
@@ -1233,14 +1244,15 @@ void twols_parse_optionst::report_properties(
     unsigned failed=0;
     unsigned unknown=0;
 
-    for(property_checkert::property_mapt::const_iterator
+    for(propertiest::const_iterator
           it=property_map.begin();
         it!=property_map.end();
         it++)
     {
-      if(it->second.result==property_checkert::resultt::UNKNOWN)
+      if(it->second.status==property_statust::UNKNOWN ||
+         it->second.status==property_statust::NOT_CHECKED)
         unknown++;
-      if(it->second.result==property_checkert::resultt::FAIL)
+      if(it->second.status==property_statust::FAIL)
         failed++;
     }
 
@@ -1309,15 +1321,15 @@ void twols_parse_optionst::output_graphml_cex(
 {
   for(const auto &p : summary_checker.property_map)
   {
-    if(p.second.result!=property_checkert::resultt::FAIL)
+    if(p.second.status!=property_statust::FAIL)
       continue;
 
     const namespacet ns(goto_model.symbol_table);
     const std::string graphml=options.get_option("graphml-witness");
     if(!graphml.empty())
     {
       graphml_witnesst graphml_witness(ns);
-      graphml_witness(p.second.error_trace);
+      graphml_witness(summary_checker.traces.at(p.first));
 
       if(graphml=="-")
         write_graphml(graphml_witness.graph(), std::cout);

src/2ls/2ls_parse_options.h

@@ -16,8 +16,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/parse_options.h>
 #include <util/replace_symbol.h>
 
-#include <langapi/language_ui.h>
-
 #include <analyses/goto_check.h>
 #include <ssa/dynobj_instance_analysis.h>
 
@@ -104,7 +102,8 @@ class twols_parse_optionst:
   void report_properties(
     const optionst &options,
     const goto_modelt &,
-    const summary_checker_baset::property_mapt &);
+    const propertiest &,
+    const tracest &traces);
 
   void show_counterexample(
     const goto_modelt &,

src/2ls/Makefile

@@ -27,6 +27,7 @@ OBJ+= $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       $(CPROVER_DIR)/src/util/util$(LIBEXT) \
       $(CPROVER_DIR)/src/goto-instrument/unwind$(OBJEXT) \
       $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
+      $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
       ../domains/domains$(LIBEXT) \
       ../ssa/ssa$(LIBEXT) \
       ../solver/solver$(LIBEXT) \

src/2ls/cover_goals_ext.cpp

@@ -130,14 +130,15 @@ void cover_goals_extt::assignment()
     for(goal_mapt::const_iterator it=goal_map.begin();
         it!=goal_map.end(); it++, g_it++)
     {
-      if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
+      if((property_map.at(it->first).status==property_statust::UNKNOWN ||
+          property_map.at(it->first).status==property_statust::NOT_CHECKED) &&
          solver.l_get(g_it->condition).is_true())
       {
-        property_map[it->first].result=property_checkert::resultt::FAIL;
+        property_map.at(it->first).status=property_statust::FAIL;
         if(build_error_trace)
         {
           ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
-          build_goto_trace(property_map[it->first].error_trace);
+          build_goto_trace(traces[it->first]);
           if(!all_properties)
             break;
         }
@@ -159,14 +160,15 @@ void cover_goals_extt::assignment()
     for(goal_mapt::const_iterator it=goal_map.begin();
         it!=goal_map.end(); it++, g_it++)
     {
-      if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
+      if((property_map.at(it->first).status==property_statust::UNKNOWN ||
+          property_map.at(it->first).status==property_statust::NOT_CHECKED) &&
          solver.l_get(g_it->condition).is_true())
       {
-        property_map[it->first].result=property_checkert::resultt::FAIL;
+        property_map.at(it->first).status=property_statust::FAIL;
         if(build_error_trace)
         {
           ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
-          build_goto_trace(property_map[it->first].error_trace);
+          build_goto_trace(traces[it->first]);
 
 #if 0
           show_raw_countermodel(

src/2ls/cover_goals_ext.h

@@ -13,11 +13,12 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_2LS_2LS_COVER_GOALS_EXT_H
 
 #include <util/message.h>
-#include <goto-programs/property_checker.h>
+#include <goto-checker/properties.h>
 
 #include "../ssa/local_ssa.h"
 #include "../ssa/unwindable_local_ssa.h"
 #include "../domains/incremental_solver.h"
+#include "traces.h"
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.
@@ -46,13 +47,15 @@ class cover_goals_extt:public messaget
     unwindable_local_SSAt &_SSA,
     incremental_solvert &_solver,
     const exprt::operandst& _loophead_selects,
-    property_checkert::property_mapt &_property_map,
+    propertiest &_property_map,
+    tracest &_traces,
     bool _spurious_check,
     bool _all_properties,
     bool _build_error_trace):
     SSA(_SSA),
     solver(_solver),
     property_map(_property_map),
+    traces(_traces),
     spurious_check(_spurious_check),
     all_properties(_all_properties),
     build_error_trace(_build_error_trace),
@@ -111,7 +114,8 @@ class cover_goals_extt:public messaget
   unwindable_local_SSAt &SSA;
   unsigned _number_covered, _iterations;
   incremental_solvert &solver;
-  property_checkert::property_mapt &property_map;
+  propertiest &property_map;
+  tracest &traces;
   bool spurious_check, all_properties, build_error_trace;
   exprt::operandst loophead_selects;
 

src/2ls/graphml_witness_ext.cpp

@@ -57,7 +57,7 @@ void graphml_witness_extt::operator()(
       continue;
     }
 
-    const graphmlt::node_indext node=add_node(cfg[i]);
+    const graphmlt::node_indext node=add_node(cfg[i], function_name);
     index_map[i]=node;
   }
   for(std::size_t i=0; i<cfg.size(); ++i)
@@ -71,7 +71,8 @@ void graphml_witness_extt::operator()(
 }
 
 graphmlt::node_indext graphml_witness_extt::add_node(
-  const dynamic_cfg_nodet &cfg_node)
+  const dynamic_cfg_nodet &cfg_node,
+  const irep_idt &function_identifier)
 {
   const graphmlt::node_indext node=graphml.add_node();
   graphml[node].node_name=cfg_node.id.to_string();
@@ -81,7 +82,7 @@ graphmlt::node_indext graphml_witness_extt::add_node(
     std::ostringstream invs;
     invs << from_expr(ns, "", cfg_node.assumption);
     graphml[node].invariant=invs.str();
-    graphml[node].invariant_scope=id2string(cfg_node.id.pc->function);
+    graphml[node].invariant_scope=id2string(function_identifier);
   }
   return node;
 }

src/2ls/graphml_witness_ext.h

@@ -30,19 +30,15 @@ class graphml_witness_extt:public graphml_witnesst
   void operator()(const summary_checker_baset &summary_checker);
 
 protected:
-  graphmlt::node_indext add_node(
-    std::map<unsigned,
-    unsigned> &loc_to_node,
-    goto_programt::const_targett it);
-
   void add_edge(
     const graphmlt::node_indext &from,
     const dynamic_cfg_nodet &from_cfg_node,
     const graphmlt::node_indext &to,
     const dynamic_cfg_nodet &to_cfg_node);
 
   graphmlt::node_indext add_node(
-    const dynamic_cfg_nodet &cfg_node);
+    const dynamic_cfg_nodet &cfg_node,
+    const irep_idt &function_identifier);
 };
 
 #endif // CPROVER_2LS_SUMMARIZER_GRAPHML_WITNESS_EXT_H