Merge pull request #3580 from peterschrammel/move-symex-bmc

Move symex-bmc and symex-coverage to goto-checker [blocks: 3583]

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -43,8 +43,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src

jbmc/unit/Makefile

@@ -89,8 +89,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \

src/cbmc/Makefile

@@ -6,8 +6,6 @@ SRC = all_properties.cpp \
       cbmc_parse_options.cpp \
       counterexample_beautification.cpp \
       fault_localization.cpp \
-      symex_bmc.cpp \
-      symex_coverage.cpp \
       xml_interface.cpp \
       # Empty last line
 

src/cbmc/bmc.h

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/decision_procedure.h>
 
+#include <goto-checker/symex_bmc.h>
+
 #include <goto-programs/goto_trace.h>
 
 #include <goto-symex/symex_target_equation.h>
@@ -29,7 +31,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
-#include "symex_bmc.h"
 
 class cbmc_solverst;
 

src/goto-checker/Makefile

@@ -1,5 +1,7 @@
 SRC = bmc_util.cpp \
       solver_factory.cpp \
+      symex_coverage.cpp \
+      symex_bmc.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/goto-checker/bmc_util.cpp

@@ -14,8 +14,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <fstream>
 #include <iostream>
 
-#include <cbmc/symex_bmc.h>
-
 #include <goto-programs/graphml_witness.h>
 #include <goto-programs/json_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
@@ -33,6 +31,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/make_unique.h>
 #include <util/ui_message.h>
 
+#include "symex_bmc.h"
+
 void build_error_trace(
   goto_tracet &goto_trace,
   const namespacet &ns,

src/cbmc/symex_bmc.cpp renamed to src/goto-checker/symex_bmc.cpp

@@ -15,8 +15,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <limits>
 
-#include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/source_location.h>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
@@ -35,28 +35,28 @@ void symex_bmct::symex_step(
   const get_goto_functiont &get_goto_function,
   statet &state)
 {
-  const source_locationt &source_location=state.source.pc->source_location;
+  const source_locationt &source_location = state.source.pc->source_location;
 
-  if(!source_location.is_nil() && last_source_location!=source_location)
+  if(!source_location.is_nil() && last_source_location != source_location)
   {
-    log.debug() << "BMC at " << source_location.as_string()
-                << " (depth " << state.depth << ')' << log.eom;
+    log.debug() << "BMC at " << source_location.as_string() << " (depth "
+                << state.depth << ')' << log.eom;
 
-    last_source_location=source_location;
+    last_source_location = source_location;
   }
 
-  const goto_programt::const_targett cur_pc=state.source.pc;
-  const guardt cur_guard=state.guard;
+  const goto_programt::const_targett cur_pc = state.source.pc;
+  const guardt cur_guard = state.guard;
 
-  if(!state.guard.is_false() &&
-     state.source.pc->is_assume() &&
-     simplify_expr(state.source.pc->guard, ns).is_false())
+  if(
+    !state.guard.is_false() && state.source.pc->is_assume() &&
+    simplify_expr(state.source.pc->guard, ns).is_false())
   {
     log.statistics() << "aborting path on assume(false) at "
                      << state.source.pc->source_location << " thread "
                      << state.source.thread_nr;
 
-    const irep_idt &c=state.source.pc->source_location.get_comment();
+    const irep_idt &c = state.source.pc->source_location.get_comment();
     if(!c.empty())
       log.statistics() << ": " << c;
 
@@ -77,9 +77,9 @@ void symex_bmct::symex_step(
     // taken an impossible transition); thus we synthesize a
     // transition from the goto instruction to its target to make
     // sure the goto is considered covered
-    if(cur_pc->is_goto() &&
-       cur_pc->get_target()!=state.source.pc &&
-       cur_pc->guard.is_true())
+    if(
+      cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
+      cur_pc->guard.is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
@@ -90,18 +90,18 @@ void symex_bmct::merge_goto(
   const statet::goto_statet &goto_state,
   statet &state)
 {
-  const goto_programt::const_targett prev_pc=goto_state.source.pc;
-  const guardt prev_guard=goto_state.guard;
+  const goto_programt::const_targett prev_pc = goto_state.source.pc;
+  const guardt prev_guard = goto_state.guard;
 
   goto_symext::merge_goto(goto_state, state);
 
   PRECONDITION(prev_pc->is_goto());
-  if(record_coverage &&
-     // could the branch possibly be taken?
-     !prev_guard.is_false() &&
-     !state.guard.is_false() &&
-     // branches only, no single-successor goto
-     !prev_pc->guard.is_true())
+  if(
+    record_coverage &&
+    // could the branch possibly be taken?
+    !prev_guard.is_false() && !state.guard.is_false() &&
+    // branches only, no single-successor goto
+    !prev_pc->guard.is_true())
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 
@@ -110,10 +110,10 @@ bool symex_bmct::should_stop_unwind(
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id=goto_programt::loop_id(*source.pc);
+  const irep_idt id = goto_programt::loop_id(*source.pc);
 
   tvt abort_unwind_decision;
-  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
   for(auto handler : loop_unwind_handlers)
   {
@@ -127,7 +127,7 @@ bool symex_bmct::should_stop_unwind(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    auto limit=unwindset.get_limit(id, source.thread_nr);
+    auto limit = unwindset.get_limit(id, source.thread_nr);
 
     if(!limit.has_value())
       abort_unwind_decision = tvt(false);
@@ -142,7 +142,7 @@ bool symex_bmct::should_stop_unwind(
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
 
-  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+  if(this_loop_limit != std::numeric_limits<unsigned>::max())
     log.statistics() << " (" << this_loop_limit << " max)";
 
   log.statistics() << " " << source.pc->source_location << " thread "
@@ -157,7 +157,7 @@ bool symex_bmct::get_unwind_recursion(
   unsigned unwind)
 {
   tvt abort_unwind_decision;
-  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
   for(auto handler : recursion_unwind_handlers)
   {
@@ -170,7 +170,7 @@ bool symex_bmct::get_unwind_recursion(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    auto limit=unwindset.get_limit(id, thread_nr);
+    auto limit = unwindset.get_limit(id, thread_nr);
 
     if(!limit.has_value())
       abort_unwind_decision = tvt(false);
@@ -182,14 +182,14 @@ bool symex_bmct::get_unwind_recursion(
     abort_unwind_decision.is_known(), "unwind decision should be taken by now");
   bool abort = abort_unwind_decision.is_true();
 
-  if(unwind>0 || abort)
+  if(unwind > 0 || abort)
   {
-    const symbolt &symbol=ns.lookup(id);
+    const symbolt &symbol = ns.lookup(id);
 
     log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
                      << symbol.display_name() << " iteration " << unwind;
 
-    if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+    if(this_loop_limit != std::numeric_limits<unsigned>::max())
       log.statistics() << " (" << this_loop_limit << " max)";
 
     log.statistics() << log.eom;

src/cbmc/symex_bmc.h renamed to src/goto-checker/symex_bmc.h

@@ -9,20 +9,20 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Bounded Model Checking for ANSI-C
 
-#ifndef CPROVER_CBMC_SYMEX_BMC_H
-#define CPROVER_CBMC_SYMEX_BMC_H
+#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
+#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
 
 #include <util/message.h>
 #include <util/threeval.h>
 
-#include <goto-symex/path_storage.h>
 #include <goto-symex/goto_symex.h>
+#include <goto-symex/path_storage.h>
 
 #include <goto-instrument/unwindset.h>
 
 #include "symex_coverage.h"
 
-class symex_bmct: public goto_symext
+class symex_bmct : public goto_symext
 {
 public:
   symex_bmct(
@@ -41,9 +41,8 @@ class symex_bmct: public goto_symext
   /// information for the user (e.g. "unwinding iteration N, max M"), and is not
   /// enforced. They return true to halt unwinding, false to authorise
   /// unwinding, or Unknown to indicate they have no opinion.
-  typedef
-    std::function<tvt(
-      const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
+  typedef std::function<
+    tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
     loop_unwind_handlert;
 
   /// Recursion unwind handlers take the function ID, the unwind count so far,
@@ -115,4 +114,4 @@ class symex_bmct: public goto_symext
   symex_coveraget symex_coverage;
 };
 
-#endif // CPROVER_CBMC_SYMEX_BMC_H
+#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H