diff --git a/regression/cbmc/unwind_counters1/main.c b/regression/cbmc/unwind_counters1/main.c new file mode 100644 index 0000000000..6668d3a391 --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/unwind_counters1/test.desc b/regression/cbmc/unwind_counters1/test.desc new file mode 100644 index 0000000000..46efb30683 --- /dev/null +++ b/regression/cbmc/unwind_counters1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 11 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/unwind_counters2/main.c b/regression/cbmc/unwind_counters2/main.c new file mode 100644 index 0000000000..447015074c --- /dev/null +++ b/regression/cbmc/unwind_counters2/main.c @@ -0,0 +1,8 @@ +int main() +{ + l2: goto l1; + l1: int x=5; + goto l2; + + return 0; +} diff --git a/regression/cbmc/unwind_counters2/test.desc b/regression/cbmc/unwind_counters2/test.desc new file mode 100644 index 0000000000..70b64ab793 --- /dev/null +++ b/regression/cbmc/unwind_counters2/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 3 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/cbmc/unwind_counters3/main.c b/regression/cbmc/unwind_counters3/main.c new file mode 100644 index 0000000000..caa1d60759 --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/unwind_counters3/test.desc b/regression/cbmc/unwind_counters3/test.desc new file mode 100644 index 0000000000..70b64ab793 --- /dev/null +++ b/regression/cbmc/unwind_counters3/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 3 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index f45d722ebf..a9d428ae07 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -155,6 +155,16 @@ protected: 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); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index e50d1c8ea7..d50c66f85f 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/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); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 03186a129b..410a7e94eb 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/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()) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 501fdabea7..e64ee0b93b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -20,6 +20,30 @@ Author: Daniel Kroening, kroening@kroening.com #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: