Symex: expose call stack to unwinding decision making

This enables unwind handlers to use the calling context to decide when to unwind a particular loop,
the first use case being generic array clone methods called from enumeration type methods with known
bounds.

Author: smowton

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -480,12 +480,12 @@ int jbmc_parse_optionst::doit()
     configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
       bmc.add_loop_unwind_handler(
         [&symbol_table](
-          const irep_idt &function_id,
+          const goto_symex_statet::call_stackt &context,
           unsigned loop_number,
           unsigned unwind,
           unsigned &max_unwind) {
           return java_enum_static_init_unwind_handler(
-            function_id,
+            context,
             loop_number,
             unwind,
             max_unwind,

src/cbmc/symex_bmc.cpp

@@ -106,6 +106,7 @@ void symex_bmct::merge_goto(
 
 bool symex_bmct::get_unwind(
   const symex_targett::sourcet &source,
+  const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
   const irep_idt id=goto_programt::loop_id(*source.pc);
@@ -117,7 +118,7 @@ bool symex_bmct::get_unwind(
   {
     abort_unwind_decision =
       handler(
-        source.pc->function,
+        context,
         source.pc->loop_number,
         unwind,
         this_loop_limit);

src/cbmc/symex_bmc.h

@@ -35,14 +35,15 @@ class symex_bmct: public goto_symext
   // To show progress
   source_locationt last_source_location;
 
-  /// 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.
+  /// Loop unwind handlers take the call stack, 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 &)>
+    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,
@@ -105,6 +106,7 @@ class symex_bmct: public goto_symext
   // for loop unwinding
   virtual bool get_unwind(
     const symex_targett::sourcet &source,
+    const goto_symex_statet::call_stackt &context,
     unsigned unwind);
 
   virtual bool get_unwind_recursion(

src/goto-symex/goto_symex.h

@@ -328,6 +328,7 @@ class goto_symext
   // with false we continue.
   virtual bool get_unwind(
     const symex_targett::sourcet &source,
+    const goto_symex_statet::call_stackt &context,
     unsigned unwind);
 
   virtual void loop_bound_exceeded(statet &, const exprt &guard);

src/goto-symex/symex_goto.cpp

@@ -86,7 +86,7 @@ void goto_symext::symex_goto(statet &state)
     unwind++;
 
     // continue unwinding?
-    if(get_unwind(state.source, unwind))
+    if(get_unwind(state.source, state.call_stack(), unwind))
     {
       // no!
       loop_bound_exceeded(state, new_guard);
@@ -540,6 +540,7 @@ void goto_symext::loop_bound_exceeded(
 
 bool goto_symext::get_unwind(
   const symex_targett::sourcet &source,
+  const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
   // by default, we keep going