From a4945f35a62de89aa70359a9f282fbc09d4de56e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 5 Jun 2017 21:38:21 +0100 Subject: [PATCH 1/3] 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. --- regression/cbmc/unwind_counters1/main.c | 6 ++++++ regression/cbmc/unwind_counters1/test.desc | 7 +++++++ regression/cbmc/unwind_counters2/main.c | 8 ++++++++ regression/cbmc/unwind_counters2/test.desc | 7 +++++++ regression/cbmc/unwind_counters3/main.c | 9 +++++++++ regression/cbmc/unwind_counters3/test.desc | 7 +++++++ src/goto-symex/symex_goto.cpp | 12 ++++++++++++ 7 files changed, 56 insertions(+) create mode 100644 regression/cbmc/unwind_counters1/main.c create mode 100644 regression/cbmc/unwind_counters1/test.desc create mode 100644 regression/cbmc/unwind_counters2/main.c create mode 100644 regression/cbmc/unwind_counters2/test.desc create mode 100644 regression/cbmc/unwind_counters3/main.c create mode 100644 regression/cbmc/unwind_counters3/test.desc 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/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 03186a129b..8919f32b65 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/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; From 5fc1ca689e9c6a674e53a076708597912ecc0291 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Jul 2017 17:16:38 +0100 Subject: [PATCH 2/3] Partly revert to try out more beautiful approach --- src/goto-symex/symex_goto.cpp | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 8919f32b65..03186a129b 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -105,18 +105,6 @@ 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; From 21afd2f173ca4198a3131d0040b47ba82bf6b55f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Jul 2017 18:47:41 +0100 Subject: [PATCH 3/3] Initialise loop counters at loop entry The previous approach would reset loop counters when reaching an unwinding bound, which was broken as shown by newly added regression tests. --- src/goto-symex/goto_symex.h | 10 +++++ src/goto-symex/symex_function_call.cpp | 8 ++-- src/goto-symex/symex_goto.cpp | 19 +++----- src/goto-symex/symex_main.cpp | 61 +++++++++++++++++++------- 4 files changed, 64 insertions(+), 34 deletions(-) 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: