Fix (and cleanup) bounded thread spawn from loops or recursive calls with --unwind

- Also fixes bounded loop unwinding when loops contain recursive calls

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3161 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: tautschnig

regression/cbmc-concurrency/recursion1/main.c

@@ -0,0 +1,25 @@
+void rec_spawn()
+{
+__CPROVER_ASYNC_1: rec_spawn();
+}
+
+int main()
+{
+start:
+  (void)0;
+__CPROVER_ASYNC_1:
+  ({(void)0;
+  goto start;});
+
+start2:
+  (void)0;
+__CPROVER_ASYNC_1:
+  goto start2;
+
+  rec_spawn();
+
+  __CPROVER_assert(0, "should be reachable when using --partial-loops");
+
+  return 0;
+}
+

regression/cbmc-concurrency/recursion1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 1 --partial-loops --depth 100
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^Unwinding loop c::main.0 iteration 1 file main.c line 12 function main thread 1
+^Unwinding loop c::main.1 iteration 1 file main.c line 17 function main thread 2
+^Unwinding recursion rec_spawn iteration 1
+--
+^warning: ignoring
+^Unwinding recursion rec_spawn iteration [0-9][0-9]

regression/cbmc/Recursion5/main.c

@@ -0,0 +1,22 @@
+void loop();
+
+void rec()
+{
+  loop();
+}
+
+void loop()
+{
+  while(nondet_bool())
+    rec();
+}
+
+int main()
+{
+  rec();
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}
+

regression/cbmc/Recursion5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 2 --no-unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/cbmc/bmc.cpp

@@ -549,11 +549,22 @@ void bmct::setup_unwind()
     std::string::size_type next=set.find(",", idx);
     std::string val=set.substr(idx, next-idx);
 
+    long thread_nr=-1;
+    if(!val.empty() &&
+       isdigit(val[0]) &&
+       val.find(":")!=std::string::npos)
+    {
+      std::string nr=val.substr(0, val.find(":"));
+      thread_nr=atol(nr.c_str());
+      val.erase(0, nr.size()+1);
+    }
+
     if(val.rfind(":")!=std::string::npos)
     {
       std::string id=val.substr(0, val.rfind(":"));
-      unsigned long uw=atol(val.substr(val.rfind(":")+1).c_str());
-      symex.unwind_set[id]=uw;
+      long uw=atol(val.substr(val.rfind(":")+1).c_str());
+
+      symex.set_unwind_limit(id, thread_nr, uw);
     }
 
     if(next==std::string::npos) break;

src/cbmc/symex_bmc.cpp

@@ -78,13 +78,11 @@ bool symex_bmct::get_unwind(
   const symex_targett::sourcet &source,
   unsigned unwind)
 {
-  irep_idt id=(source.thread_nr!=0?(i2string(source.thread_nr)+":"):"")+
-              id2string(source.pc->function)+"."+
-              i2string(source.pc->loop_number);
-  unsigned long this_loop_max_unwind=max_unwind;
-
-  if(unwind_set.count(id)!=0)
-    this_loop_max_unwind=unwind_set[id];
+  const irep_idt id=goto_programt::loop_id(source.pc);
+  const long this_loop_max_unwind=
+    std::max(max_unwind,
+             std::max(thread_loop_limits[(unsigned)-1][id],
+                      thread_loop_limits[source.thread_nr][id]));
 
   #if 1
   statistics() << "Unwinding loop " << id << " iteration "
@@ -109,15 +107,19 @@ Function: symex_bmct::get_unwind_recursion
 \*******************************************************************/
 
 bool symex_bmct::get_unwind_recursion(
-  const irep_idt &identifier,
+  const irep_idt &id,
+  const unsigned thread_nr,
   unsigned unwind)
 {
-  unsigned long this_loop_max_unwind=max_unwind;
+  const long this_loop_max_unwind=
+    std::max(max_unwind,
+             std::max(thread_loop_limits[(unsigned)-1][id],
+                      thread_loop_limits[thread_nr][id]));
 
   #if 1
   if(unwind!=0)
   {
-    const symbolt &symbol=ns.lookup(identifier);
+    const symbolt &symbol=ns.lookup(id);
 
     statistics() << "Unwinding recursion "
                  << symbol.display_name()

src/cbmc/symex_bmc.h

@@ -28,10 +28,23 @@ class symex_bmct:
   irept last_location;
 
   // control unwinding  
-  unsigned long max_unwind;
-  std::map<irep_idt, long> unwind_set;
+  long max_unwind;
+
+  void set_unwind_limit(
+    const irep_idt &id,
+    long thread_nr,
+    long limit)
+  {
+    unsigned t=thread_nr>=0 ? thread_nr : (unsigned)-1;
+
+    thread_loop_limits[t][id]=limit;
+  }
 
 protected:  
+  typedef hash_map_cont<irep_idt, long, irep_id_hash> loop_limitst;
+  typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
+  thread_loop_limitst thread_loop_limits;
+
   //
   // overloaded from goto_symext
   //
@@ -46,6 +59,7 @@ class symex_bmct:
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
+    const unsigned thread_nr,
     unsigned unwind);
 
   virtual void no_body(const irep_idt &identifier);

src/goto-programs/goto_convert.cpp

@@ -1721,17 +1721,6 @@ void goto_convertt::convert_start_thread(
 
   start_thread->location=code.location();
 
-  // see if op0 is an unconditional goto
-  
-  if(code.op0().get(ID_statement)==ID_goto)
-  {
-    start_thread->code.set(ID_destination,
-      code.op0().get(ID_destination));
-      
-    // remember it to do target later
-    targets.gotos.push_back(start_thread);
-  }
-  else
   {
     // start_thread label;
     // goto tmp;

src/goto-programs/goto_program_template.h

@@ -381,6 +381,13 @@ class goto_program_templatet
 
   //! Update all indices  
   void update();
+
+  //! Human-readable loop name
+  inline static irep_idt loop_id(const_targett target)
+  {
+    return id2string(target->function)+"."+
+           i2string(target->loop_number);
+  }
 
   //! Is the program empty?
   inline bool empty() const

src/goto-symex/goto_symex.h

@@ -209,6 +209,7 @@ class goto_symext
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
+    const unsigned thread_nr,
     unsigned unwind);
 
   void argument_assignments(
@@ -225,9 +226,6 @@ class goto_symext
   void add_end_of_function(
     exprt &code,
     const irep_idt &identifier);
-                           
-  std::map<irep_idt, unsigned> function_unwind;
-  std::map<symex_targett::sourcet, unsigned> unwind_map;
 
   // exceptions
 

src/goto-symex/goto_symex_state.h

@@ -291,6 +291,22 @@ class goto_symex_statet
     // exceptions
     typedef std::map<irep_idt, goto_programt::targett> catch_mapt;
     catch_mapt catch_map;
+
+    // loop and recursion unwinding
+    struct loop_infot
+    {
+      loop_infot():
+        count(0),
+        is_recursion(false)
+      {
+      }
+
+      unsigned count;
+      bool is_recursion;
+    };
+    typedef hash_map_cont<irep_idt, loop_infot, irep_id_hash>
+      loop_iterationst;
+    loop_iterationst loop_iterations;
   };
 
   typedef std::vector<framet> call_stackt;

src/goto-symex/symex_function_call.cpp

@@ -35,6 +35,7 @@ Function: goto_symext::get_unwind_recursion
 
 bool goto_symext::get_unwind_recursion(
   const irep_idt &identifier,
+  const unsigned thread_nr,
   unsigned unwind)
 {
   return false;
@@ -263,10 +264,13 @@ void goto_symext::symex_function_call_code(
 
   const goto_functionst::goto_functiont &goto_function=it->second;
 
-  unsigned &unwinding_counter=function_unwind[identifier];
+  const bool stop_recursing=get_unwind_recursion(
+    identifier,
+    state.source.thread_nr,
+    state.top().loop_iterations[identifier].count);
 
   // see if it's too much
-  if(get_unwind_recursion(identifier, unwinding_counter))
+  if(stop_recursing)
   {
     if(options.get_bool_option("partial-loops"))
     {
@@ -314,9 +318,6 @@ void goto_symext::symex_function_call_code(
   for(unsigned i=0; i<arguments.size(); i++)
     state.rename(arguments[i], ns);
 
-  // increase unwinding counter
-  unwinding_counter++;
-  
   // produce a new frame
   assert(!state.call_stack().empty());
   goto_symex_statet::framet &frame=state.new_frame();
@@ -332,6 +333,17 @@ void goto_symext::symex_function_call_code(
   frame.calling_location=state.source;
   frame.function_identifier=identifier;
 
+  const goto_symex_statet::framet &p_frame=state.previous_frame();
+  for(goto_symex_statet::framet::loop_iterationst::const_iterator
+      it=p_frame.loop_iterations.begin();
+      it!=p_frame.loop_iterations.end();
+      ++it)
+    if(it->second.is_recursion)
+      frame.loop_iterations.insert(*it);
+  // increase unwinding counter
+  frame.loop_iterations[identifier].is_recursion=true;
+  frame.loop_iterations[identifier].count++;
+
   state.source.is_set=true;
   state.source.pc=goto_function.body.instructions.begin();
 }
@@ -367,10 +379,6 @@ void goto_symext::pop_frame(statet &state)
         it!=frame.local_variables.end();
         it++)
       state.level2.remove(*it);
-
-    // decrease recursion unwinding counter
-    if(frame.function_identifier!="")
-      function_unwind[frame.function_identifier]--;
   }
 
   state.pop_frame();

src/goto-symex/symex_goto.cpp

@@ -29,6 +29,7 @@ Function: goto_symext::symex_goto
 void goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
+  statet::framet &frame=state.top();
 
   exprt old_guard=instruction.guard;
   clean_expr(old_guard, state, false);
@@ -43,7 +44,8 @@ void goto_symext::symex_goto(statet &state)
      state.guard.is_false())
   {
     // reset unwinding counter
-    unwind_map[state.source]=0;
+    if(instruction.is_backwards_goto())
+      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count=0;
 
     // next instruction
     state.source.pc++;
@@ -59,21 +61,20 @@ void goto_symext::symex_goto(statet &state)
   goto_programt::const_targett goto_target=
     instruction.get_target();
 
-  bool forward=
-    state.source.pc->location_number<
-    goto_target->location_number;
+  bool forward=!instruction.is_backwards_goto();
 
   if(!forward) // backwards?
   {
-    unsigned &unwind=unwind_map[state.source];
+    unsigned &unwind=
+      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
     unwind++;
 
     if(get_unwind(state.source, unwind))
     {
       loop_bound_exceeded(state, new_guard);
 
       // reset unwinding
-      unwind_map[state.source]=0;
+      unwind=0;
 
       // next instruction
       state.source.pc++;