Reimplement remove-static-init-loops to avoid need to inspect GOTO program

src/cbmc/bmc.h

@@ -71,6 +71,17 @@ class bmct:public safety_checkert
     return run(goto_functions);
   }
 
+  void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
+  {
+    symex.add_loop_unwind_handler(handler);
+  }
+
+  void add_unwind_recursion_handler(
+    symex_bmct::recursion_unwind_handlert handler)
+  {
+    symex.add_recursion_unwind_handler(handler);
+  }
+
 protected:
   const optionst &options;
   symbol_tablet new_symbol_table;

src/cbmc/cbmc_parse_options.cpp

@@ -45,7 +45,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_static_init_loops.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_symbol_table.h>

src/cbmc/symex_bmc.cpp

@@ -110,27 +110,49 @@ bool symex_bmct::get_unwind(
 {
   const irep_idt id=goto_programt::loop_id(*source.pc);
 
-  // We use the most specific limit we have,
-  // and 'infinity' when we have none.
-
+  tvt abort_unwind_decision;
   unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
 
-  loop_limitst &this_thread_limits=
-    thread_loop_limits[source.thread_nr];
+  for(auto handler : loop_unwind_handlers)
+  {
+    abort_unwind_decision =
+      handler(
+        source.pc->function,
+        source.pc->loop_number,
+        unwind,
+        this_loop_limit);
+    if(abort_unwind_decision.is_known())
+      break;
+  }
 
-  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-  if(l_it!=this_thread_limits.end())
-    this_loop_limit=l_it->second;
-  else
+  // If no handler gave an opinion, use standard command-line --unwindset
+  // / --unwind options to decide:
+  if(abort_unwind_decision.is_unknown())
   {
-    l_it=loop_limits.find(id);
-    if(l_it!=loop_limits.end())
+    // We use the most specific limit we have,
+    // and 'infinity' when we have none.
+
+    loop_limitst &this_thread_limits=
+      thread_loop_limits[source.thread_nr];
+
+    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
+    if(l_it!=this_thread_limits.end())
       this_loop_limit=l_it->second;
-    else if(max_unwind_is_set)
-      this_loop_limit=max_unwind;
+    else
+    {
+      l_it=loop_limits.find(id);
+      if(l_it!=loop_limits.end())
+        this_loop_limit=l_it->second;
+      else if(max_unwind_is_set)
+        this_loop_limit=max_unwind;
+    }
+
+    abort_unwind_decision = tvt(unwind >= this_loop_limit);
   }
 
-  bool abort=unwind>=this_loop_limit;
+  INVARIANT(
+    abort_unwind_decision.is_known(), "unwind decision should be taken by now");
+  bool abort = abort_unwind_decision.is_true();
 
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
@@ -149,27 +171,44 @@ bool symex_bmct::get_unwind_recursion(
   const unsigned thread_nr,
   unsigned unwind)
 {
-  // We use the most specific limit we have,
-  // and 'infinity' when we have none.
-
+  tvt abort_unwind_decision;
   unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
 
-  loop_limitst &this_thread_limits=
-    thread_loop_limits[thread_nr];
+  for(auto handler : recursion_unwind_handlers)
+  {
+    abort_unwind_decision = handler(id, unwind, this_loop_limit);
+    if(abort_unwind_decision.is_known())
+      break;
+  }
 
-  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-  if(l_it!=this_thread_limits.end())
-    this_loop_limit=l_it->second;
-  else
+  // If no handler gave an opinion, use standard command-line --unwindset
+  // / --unwind options to decide:
+  if(abort_unwind_decision.is_unknown())
   {
-    l_it=loop_limits.find(id);
-    if(l_it!=loop_limits.end())
+    // We use the most specific limit we have,
+    // and 'infinity' when we have none.
+
+    loop_limitst &this_thread_limits=
+      thread_loop_limits[thread_nr];
+
+    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
+    if(l_it!=this_thread_limits.end())
       this_loop_limit=l_it->second;
-    else if(max_unwind_is_set)
-      this_loop_limit=max_unwind;
+    else
+    {
+      l_it=loop_limits.find(id);
+      if(l_it!=loop_limits.end())
+        this_loop_limit=l_it->second;
+      else if(max_unwind_is_set)
+        this_loop_limit=max_unwind;
+    }
+
+    abort_unwind_decision = tvt(unwind>this_loop_limit);
   }
 
-  bool abort=unwind>this_loop_limit;
+  INVARIANT(
+    abort_unwind_decision.is_known(), "unwind decision should be taken by now");
+  bool abort = abort_unwind_decision.is_true();
 
   if(unwind>0 || abort)
   {

src/cbmc/symex_bmc.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_CBMC_SYMEX_BMC_H
 
 #include <util/message.h>
+#include <util/threeval.h>
 
 #include <goto-symex/goto_symex.h>
 
@@ -53,6 +54,43 @@ class symex_bmct: public goto_symext
     loop_limits[id]=limit;
   }
 
+  /// Loop unwind handlers take the function ID and loop number, the unwind
+  /// count so far, and an out-parameter specifying an advisory maximum, which
+  /// they may set. If set the advisory maximum is set it is *only* used to
+  /// print useful 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 irep_idt &, unsigned, unsigned, unsigned &)>
+    loop_unwind_handlert;
+
+  /// Recursion unwind handlers take the function ID, the unwind count so far,
+  /// and an out-parameter specifying an advisory maximum, which they may set.
+  /// If set the advisory maximum is set it is *only* used to print useful
+  /// 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 irep_idt &, unsigned, unsigned &)>
+    recursion_unwind_handlert;
+
+  /// Add a callback function that will be called to determine whether to unwind
+  /// loops. The first function added will get the first chance to answer, and
+  /// the first authoratitive (true or false) answer is final.
+  /// \param handler: new callback
+  void add_loop_unwind_handler(loop_unwind_handlert handler)
+  {
+    loop_unwind_handlers.push_back(handler);
+  }
+
+  /// Add a callback function that will be called to determine whether to unwind
+  /// recursion. The first function added will get the first chance to answer,
+  /// and the first authoratitive (true or false) answer is final.
+  /// \param handler: new callback
+  void add_recursion_unwind_handler(recursion_unwind_handlert handler)
+  {
+    recursion_unwind_handlers.push_back(handler);
+  }
+
   bool output_coverage_report(
     const goto_functionst &goto_functions,
     const std::string &path) const
@@ -67,6 +105,8 @@ class symex_bmct: public goto_symext
   // 1) a global limit (max_unwind)
   // 2) a limit per loop, all threads
   // 3) a limit for a particular thread.
+  // 4) zero or more handler functions that can special-case particular
+  //    functions or loops
   // We use the most specific of the above.
 
   unsigned max_unwind;
@@ -78,6 +118,12 @@ class symex_bmct: public goto_symext
   typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
   thread_loop_limitst thread_loop_limits;
 
+  /// Callbacks that may provide an unwind/do-not-unwind decision for a loop
+  std::vector<loop_unwind_handlert> loop_unwind_handlers;
+  /// Callbacks that may provide an unwind/do-not-unwind decision for a
+  /// recursive call
+  std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
+
   //
   // overloaded from goto_symext
   //

src/goto-programs/Makefile

@@ -47,7 +47,6 @@ SRC = basic_blocks.cpp \
       remove_instanceof.cpp \
       remove_returns.cpp \
       remove_skip.cpp \
-      remove_static_init_loops.cpp \
       remove_unreachable.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \