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

This was supplying synthetic --unwind parameters for each loop found in the GOTO program,
but that required early access to the GOTO code, which will not be available under symex-
driven lazy loading. Therefore we replace that pass with a handler mechanism that allows
the driver program to provide its own callback to make unwinding decisions, and use it in
JBMC to ensure that enumeration type static initialisers are unwound sufficiently.

Author: smowton

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, [email protected]
 #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, [email protected]
 #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 \