Reset unwinding counters when leaving a loop at the loop head

regression/cbmc/unwind_counters1/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  for(int i=0; i<2; ++i)
+    for(int j=0; j<10; ++j);
+  return 0;
+}

regression/cbmc/unwind_counters1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 11 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/unwind_counters2/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  l2: goto l1;
+  l1: int x=5;
+  goto l2;
+
+  return 0;
+}

regression/cbmc/unwind_counters2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 3 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

regression/cbmc/unwind_counters3/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int i=0;
+  l2: if(i==1) int y=0;
+  l1: int x=5;
+  goto l2;
+
+  return 0;
+}

regression/cbmc/unwind_counters3/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 3 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/goto-symex/goto_symex.h

@@ -155,6 +155,16 @@ class goto_symext
   irep_idt guard_identifier;
 
   // symex
+  virtual void symex_transition(
+    statet &state,
+    goto_programt::const_targett to,
+    bool is_backwards_goto=false);
+  virtual void symex_transition(statet &state)
+  {
+    goto_programt::const_targett next=state.source.pc;
+    ++next;
+    symex_transition(state, next);
+  }
 
   virtual void symex_goto(statet &state);
   virtual void symex_start_thread(statet &state);

src/goto-symex/symex_function_call.cpp

@@ -254,7 +254,7 @@ void goto_symext::symex_function_call_code(
       state.guard.add(false_exprt());
     }
 
-    state.source.pc++;
+    symex_transition(state);
     return;
   }
 
@@ -276,7 +276,7 @@ void goto_symext::symex_function_call_code(
       symex_assign_rec(state, code);
     }
 
-    state.source.pc++;
+    symex_transition(state);
     return;
   }
 
@@ -314,7 +314,7 @@ void goto_symext::symex_function_call_code(
   frame.loop_iterations[identifier].count++;
 
   state.source.is_set=true;
-  state.source.pc=goto_function.body.instructions.begin();
+  symex_transition(state, goto_function.body.instructions.begin());
 }
 
 /// pop one call frame
@@ -326,7 +326,7 @@ void goto_symext::pop_frame(statet &state)
     statet::framet &frame=state.top();
 
     // restore program counter
-    state.source.pc=frame.calling_location.pc;
+    symex_transition(state, frame.calling_location.pc);
 
     // restore L1 renaming
     state.level1.restore_from(frame.old_level1);

src/goto-symex/symex_goto.cpp

@@ -36,12 +36,8 @@ void goto_symext::symex_goto(statet &state)
     if(!state.guard.is_false())
       target.location(state.guard.as_expr(), state.source);
 
-    // reset unwinding counter
-    if(instruction.is_backwards_goto())
-      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count=0;
-
     // next instruction
-    state.source.pc++;
+    symex_transition(state);
     return; // nothing to do
   }
 
@@ -77,7 +73,7 @@ void goto_symext::symex_goto(statet &state)
       symex_assume(state, negated_cond);
 
       // next instruction
-      state.source.pc++;
+      symex_transition(state);
       return;
     }
 
@@ -91,17 +87,14 @@ void goto_symext::symex_goto(statet &state)
       // no!
       loop_bound_exceeded(state, new_guard);
 
-      // reset unwinding
-      unwind=0;
-
       // next instruction
-      state.source.pc++;
+      symex_transition(state);
       return;
     }
 
     if(new_guard.is_true())
     {
-      state.source.pc=goto_target;
+      symex_transition(state, goto_target, true);
       return; // nothing else to do
     }
   }
@@ -122,7 +115,7 @@ void goto_symext::symex_goto(statet &state)
 
     if(state_pc==goto_target)
     {
-      state.source.pc=goto_target;
+      symex_transition(state, goto_target);
       return; // nothing else to do
     }
   }
@@ -140,7 +133,7 @@ void goto_symext::symex_goto(statet &state)
   goto_state_list.push_back(statet::goto_statet(state));
   statet::goto_statet &new_state=goto_state_list.back();
 
-  state.source.pc=state_pc;
+  symex_transition(state, state_pc, !forward);
 
   // adjust guards
   if(new_guard.is_true())

src/goto-symex/symex_main.cpp

@@ -20,6 +20,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
+void goto_symext::symex_transition(
+  statet &state,
+  goto_programt::const_targett to,
+  bool is_backwards_goto)
+{
+  if(!state.call_stack().empty())
+  {
+    // initialize the loop counter of any loop we are newly entering
+    // upon this transition; we are entering a loop if
+    // 1. the transition from state.source.pc to "to" is not a backwards goto
+    // or
+    // 2. we are arriving from an outer loop
+    statet::framet &frame=state.top();
+    const goto_programt::instructiont &instruction=*to;
+    for(const auto &i_e : instruction.incoming_edges)
+      if(i_e->is_goto() && i_e->is_backwards_goto() &&
+         (!is_backwards_goto ||
+          state.source.pc->location_number>i_e->location_number))
+        frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
+  }
+
+  state.source.pc=to;
+}
+
 void goto_symext::new_name(symbolt &symbol)
 {
   get_new_name(symbol, ns);
@@ -114,6 +138,8 @@ void goto_symext::operator()(
   state.symex_target=⌖
   state.dirty=new dirtyt(goto_functions);
 
+  symex_transition(state, state.source.pc);
+
   assert(state.top().end_of_function->is_end_function());
 
   while(!state.call_stack().empty())
@@ -127,6 +153,7 @@ void goto_symext::operator()(
       unsigned t=state.source.thread_nr+1;
       // std::cout << "********* Now executing thread " << t << '\n';
       state.switch_to_thread(t);
+      symex_transition(state, state.source.pc);
     }
   }
 
@@ -190,20 +217,20 @@ void goto_symext::symex_step(
   case SKIP:
     if(!state.guard.is_false())
       target.location(state.guard.as_expr(), state.source);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case END_FUNCTION:
     // do even if state.guard.is_false() to clear out frame created
     // in symex_start_thread
     symex_end_of_function(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case LOCATION:
     if(!state.guard.is_false())
       target.location(state.guard.as_expr(), state.source);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case GOTO:
@@ -219,7 +246,7 @@ void goto_symext::symex_step(
       symex_assume(state, tmp);
     }
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case ASSERT:
@@ -233,21 +260,21 @@ void goto_symext::symex_step(
       vcc(tmp, msg, state);
     }
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case RETURN:
     if(!state.guard.is_false())
       return_assignment(state);
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case ASSIGN:
     if(!state.guard.is_false())
       symex_assign_rec(state, to_code_assign(instruction.code));
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case FUNCTION_CALL:
@@ -267,58 +294,58 @@ void goto_symext::symex_step(
       symex_function_call(goto_functions, state, deref_code);
     }
     else
-      state.source.pc++;
+      symex_transition(state);
     break;
 
   case OTHER:
     if(!state.guard.is_false())
       symex_other(goto_functions, state);
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case DECL:
     if(!state.guard.is_false())
       symex_decl(state);
 
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case DEAD:
     symex_dead(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case START_THREAD:
     symex_start_thread(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case END_THREAD:
     // behaves like assume(0);
     if(!state.guard.is_false())
       state.guard.add(false_exprt());
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case ATOMIC_BEGIN:
     symex_atomic_begin(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case ATOMIC_END:
     symex_atomic_end(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case CATCH:
     symex_catch(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case THROW:
     symex_throw(state);
-    state.source.pc++;
+    symex_transition(state);
     break;
 
   case NO_INSTRUCTION_TYPE: