Reset unwinding counters when leaving a loop at the loop head

Constant propagation and simplification may determine that a loop cannot be
unrolled further. This is determined at the loop head, which is a forward goto
in case of for or while (but not do-while) loops. Before this patch, forward
gotos would never cause loop counters to be reset. In nested loops, the inner
loop(s) would thus have their unwinding counts added to previous (complete) loop
executions.

Author: tautschnig

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/symex_goto.cpp

@@ -105,6 +105,18 @@ void goto_symext::symex_goto(statet &state)
       return; // nothing else to do
     }
   }
+  else if(new_guard.is_true() && !old_guard.is_true())
+  {
+    // we may have left a loop (i.e., the forward goto is beyond
+    // the end of the loop) as the loop condition has become false
+    // via constant propagation and simplification (the original
+    // condition "old_guard" was not trivially true, but "new_guard"
+    // is) -- reset all candidate loop counters
+    for(const auto &i_e : instruction.incoming_edges)
+      if(i_e->is_goto() && i_e->is_backwards_goto() &&
+         goto_target->location_number>i_e->location_number)
+        frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
+  }
 
   goto_programt::const_targett new_state_pc, state_pc;
   symex_targett::sourcet original_source=state.source;