Add documentation and refactor incremental one loop changes

`check_break` is now documented in `goto_symex.h` as well (I removed the
parameters that were not used anywhere).

Author: petr-bauch

regression/cbmc-incr-oneloop/Makefile

@@ -1,5 +1,6 @@
 default: tests.log
 
+# Note the `perl -e` serves the purpose of providing timeout
 test:
 	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
 

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -100,17 +100,14 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind(
 /// \return True if the back edge encountered during symbolic execution
 ///   corresponds to the given loop (incr_loop_id)
 bool symex_bmc_incremental_one_loopt::check_break(
-  const irep_idt &id,
-  bool is_function,
-  statet &state,
-  const exprt &cond,
+  const irep_idt &loop_id,
   unsigned unwind)
 {
   if(unwind < incr_min_unwind)
     return false;
 
   // loop specified by incremental-loop
-  return (id == incr_loop_id);
+  return (loop_id == incr_loop_id);
 }
 
 bool symex_bmc_incremental_one_loopt::from_entry_point_of(

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -38,12 +38,7 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
   std::unique_ptr<goto_symext::statet> state;
 
   // returns true if the symbolic execution is to be interrupted for checking
-  bool check_break(
-    const irep_idt &id,
-    bool is_function,
-    goto_symext::statet &state,
-    const exprt &cond,
-    unsigned unwind) override;
+  bool check_break(const irep_idt &loop_id, unsigned unwind) override;
 
   bool should_stop_unwind(
     const symex_targett::sourcet &source,

src/goto-symex/goto_symex.h

@@ -168,12 +168,15 @@ class goto_symext
   /// by the symbolic executions.
   bool ignore_assertions = false;
 
-  virtual bool check_break(
-    const irep_idt &id,
-    bool is_function,
-    statet &state,
-    const exprt &cond,
-    unsigned unwind);
+  /// \brief Defines condition for interrupting symbolic execution for a
+  ///   specific loop
+  ///
+  /// False constant by default, over-ridden by incremental BMC implementation
+  ///   to allow breaking if the unwinding the user specified loop
+  /// \param id: the loop identifier
+  /// \param unwind: current unwinding counter
+  /// \return true if the symbolic execution is to be interrupted for checking
+  virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
 
 protected:
   /// The configuration to use for this symbolic execution

src/goto-symex/symex_goto.cpp

@@ -287,7 +287,7 @@ void goto_symext::symex_goto(statet &state)
     if(new_guard.is_true())
     {
       // we continue executing the loop
-      if(check_break(loop_id, false, state, new_guard, unwind))
+      if(check_break(loop_id, unwind))
       {
         should_pause_symex = true;
       }
@@ -584,12 +584,7 @@ void goto_symext::symex_unreachable_goto(statet &state)
   symex_transition(state);
 }
 
-bool goto_symext::check_break(
-  const irep_idt &id,
-  bool is_function,
-  statet &state,
-  const exprt &cond,
-  unsigned unwind)
+bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
 {
   // dummy implementation
   return false;

src/goto-symex/symex_target_equation.cpp

@@ -333,15 +333,8 @@ void symex_target_equationt::convert_without_assertions(
 
 void symex_target_equationt::convert(decision_proceduret &decision_procedure)
 {
-  convert_guards(decision_procedure);
-  convert_assignments(decision_procedure);
-  convert_decls(decision_procedure);
-  convert_assumptions(decision_procedure);
+  convert_without_assertions(decision_procedure);
   convert_assertions(decision_procedure);
-  convert_goto_instructions(decision_procedure);
-  convert_function_calls(decision_procedure);
-  convert_io(decision_procedure);
-  convert_constraints(decision_procedure);
 }
 
 void symex_target_equationt::convert_assignments(
@@ -476,7 +469,7 @@ void symex_target_equationt::convert_assertions(
   {
     for(auto &step : SSA_steps)
     {
-      // ignore already converted assertions in the error trace
+      // hide already converted assertions in the error trace
       if(step.is_assert() && step.converted)
         step.hidden = true;
 
@@ -503,7 +496,7 @@ void symex_target_equationt::convert_assertions(
 
   for(auto &step : SSA_steps)
   {
-    // ignore already converted assertions in the error trace
+    // hide already converted assertions in the error trace
     if(step.is_assert() && step.converted)
       step.hidden = true;