Merge pull request #988 from tautschnig/fix-unwind-count
Reset unwinding counters when leaving a loop at the loop head
This commit is contained in:
commit
32b68ced26
|
@ -0,0 +1,6 @@
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
for(int i=0; i<2; ++i)
|
||||||
|
for(int j=0; j<10; ++j);
|
||||||
|
return 0;
|
||||||
|
}
|
|
@ -0,0 +1,7 @@
|
||||||
|
CORE
|
||||||
|
main.c
|
||||||
|
--unwind 11 --unwinding-assertions
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
^VERIFICATION SUCCESSFUL$
|
||||||
|
--
|
|
@ -0,0 +1,8 @@
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
l2: goto l1;
|
||||||
|
l1: int x=5;
|
||||||
|
goto l2;
|
||||||
|
|
||||||
|
return 0;
|
||||||
|
}
|
|
@ -0,0 +1,7 @@
|
||||||
|
CORE
|
||||||
|
main.c
|
||||||
|
--unwind 3 --unwinding-assertions
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
--
|
|
@ -0,0 +1,9 @@
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
int i=0;
|
||||||
|
l2: if(i==1) int y=0;
|
||||||
|
l1: int x=5;
|
||||||
|
goto l2;
|
||||||
|
|
||||||
|
return 0;
|
||||||
|
}
|
|
@ -0,0 +1,7 @@
|
||||||
|
CORE
|
||||||
|
main.c
|
||||||
|
--unwind 3 --unwinding-assertions
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
--
|
|
@ -155,6 +155,16 @@ protected:
|
||||||
irep_idt guard_identifier;
|
irep_idt guard_identifier;
|
||||||
|
|
||||||
// symex
|
// 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_goto(statet &state);
|
||||||
virtual void symex_start_thread(statet &state);
|
virtual void symex_start_thread(statet &state);
|
||||||
|
|
|
@ -254,7 +254,7 @@ void goto_symext::symex_function_call_code(
|
||||||
state.guard.add(false_exprt());
|
state.guard.add(false_exprt());
|
||||||
}
|
}
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -276,7 +276,7 @@ void goto_symext::symex_function_call_code(
|
||||||
symex_assign_rec(state, code);
|
symex_assign_rec(state, code);
|
||||||
}
|
}
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -314,7 +314,7 @@ void goto_symext::symex_function_call_code(
|
||||||
frame.loop_iterations[identifier].count++;
|
frame.loop_iterations[identifier].count++;
|
||||||
|
|
||||||
state.source.is_set=true;
|
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
|
/// pop one call frame
|
||||||
|
@ -326,7 +326,7 @@ void goto_symext::pop_frame(statet &state)
|
||||||
statet::framet &frame=state.top();
|
statet::framet &frame=state.top();
|
||||||
|
|
||||||
// restore program counter
|
// restore program counter
|
||||||
state.source.pc=frame.calling_location.pc;
|
symex_transition(state, frame.calling_location.pc);
|
||||||
|
|
||||||
// restore L1 renaming
|
// restore L1 renaming
|
||||||
state.level1.restore_from(frame.old_level1);
|
state.level1.restore_from(frame.old_level1);
|
||||||
|
|
|
@ -36,12 +36,8 @@ void goto_symext::symex_goto(statet &state)
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
target.location(state.guard.as_expr(), state.source);
|
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
|
// next instruction
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
return; // nothing to do
|
return; // nothing to do
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -77,7 +73,7 @@ void goto_symext::symex_goto(statet &state)
|
||||||
symex_assume(state, negated_cond);
|
symex_assume(state, negated_cond);
|
||||||
|
|
||||||
// next instruction
|
// next instruction
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -91,17 +87,14 @@ void goto_symext::symex_goto(statet &state)
|
||||||
// no!
|
// no!
|
||||||
loop_bound_exceeded(state, new_guard);
|
loop_bound_exceeded(state, new_guard);
|
||||||
|
|
||||||
// reset unwinding
|
|
||||||
unwind=0;
|
|
||||||
|
|
||||||
// next instruction
|
// next instruction
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
if(new_guard.is_true())
|
if(new_guard.is_true())
|
||||||
{
|
{
|
||||||
state.source.pc=goto_target;
|
symex_transition(state, goto_target, true);
|
||||||
return; // nothing else to do
|
return; // nothing else to do
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -122,7 +115,7 @@ void goto_symext::symex_goto(statet &state)
|
||||||
|
|
||||||
if(state_pc==goto_target)
|
if(state_pc==goto_target)
|
||||||
{
|
{
|
||||||
state.source.pc=goto_target;
|
symex_transition(state, goto_target);
|
||||||
return; // nothing else to do
|
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));
|
goto_state_list.push_back(statet::goto_statet(state));
|
||||||
statet::goto_statet &new_state=goto_state_list.back();
|
statet::goto_statet &new_state=goto_state_list.back();
|
||||||
|
|
||||||
state.source.pc=state_pc;
|
symex_transition(state, state_pc, !forward);
|
||||||
|
|
||||||
// adjust guards
|
// adjust guards
|
||||||
if(new_guard.is_true())
|
if(new_guard.is_true())
|
||||||
|
|
|
@ -20,6 +20,30 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
|
|
||||||
#include "goto_symex.h"
|
#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)
|
void goto_symext::new_name(symbolt &symbol)
|
||||||
{
|
{
|
||||||
get_new_name(symbol, ns);
|
get_new_name(symbol, ns);
|
||||||
|
@ -114,6 +138,8 @@ void goto_symext::operator()(
|
||||||
state.symex_target=⌖
|
state.symex_target=⌖
|
||||||
state.dirty=new dirtyt(goto_functions);
|
state.dirty=new dirtyt(goto_functions);
|
||||||
|
|
||||||
|
symex_transition(state, state.source.pc);
|
||||||
|
|
||||||
assert(state.top().end_of_function->is_end_function());
|
assert(state.top().end_of_function->is_end_function());
|
||||||
|
|
||||||
while(!state.call_stack().empty())
|
while(!state.call_stack().empty())
|
||||||
|
@ -127,6 +153,7 @@ void goto_symext::operator()(
|
||||||
unsigned t=state.source.thread_nr+1;
|
unsigned t=state.source.thread_nr+1;
|
||||||
// std::cout << "********* Now executing thread " << t << '\n';
|
// std::cout << "********* Now executing thread " << t << '\n';
|
||||||
state.switch_to_thread(t);
|
state.switch_to_thread(t);
|
||||||
|
symex_transition(state, state.source.pc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -190,20 +217,20 @@ void goto_symext::symex_step(
|
||||||
case SKIP:
|
case SKIP:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
target.location(state.guard.as_expr(), state.source);
|
target.location(state.guard.as_expr(), state.source);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case END_FUNCTION:
|
case END_FUNCTION:
|
||||||
// do even if state.guard.is_false() to clear out frame created
|
// do even if state.guard.is_false() to clear out frame created
|
||||||
// in symex_start_thread
|
// in symex_start_thread
|
||||||
symex_end_of_function(state);
|
symex_end_of_function(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case LOCATION:
|
case LOCATION:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
target.location(state.guard.as_expr(), state.source);
|
target.location(state.guard.as_expr(), state.source);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case GOTO:
|
case GOTO:
|
||||||
|
@ -219,7 +246,7 @@ void goto_symext::symex_step(
|
||||||
symex_assume(state, tmp);
|
symex_assume(state, tmp);
|
||||||
}
|
}
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case ASSERT:
|
case ASSERT:
|
||||||
|
@ -233,21 +260,21 @@ void goto_symext::symex_step(
|
||||||
vcc(tmp, msg, state);
|
vcc(tmp, msg, state);
|
||||||
}
|
}
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case RETURN:
|
case RETURN:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
return_assignment(state);
|
return_assignment(state);
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case ASSIGN:
|
case ASSIGN:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
symex_assign_rec(state, to_code_assign(instruction.code));
|
symex_assign_rec(state, to_code_assign(instruction.code));
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case FUNCTION_CALL:
|
case FUNCTION_CALL:
|
||||||
|
@ -267,58 +294,58 @@ void goto_symext::symex_step(
|
||||||
symex_function_call(goto_functions, state, deref_code);
|
symex_function_call(goto_functions, state, deref_code);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case OTHER:
|
case OTHER:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
symex_other(goto_functions, state);
|
symex_other(goto_functions, state);
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case DECL:
|
case DECL:
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
symex_decl(state);
|
symex_decl(state);
|
||||||
|
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case DEAD:
|
case DEAD:
|
||||||
symex_dead(state);
|
symex_dead(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case START_THREAD:
|
case START_THREAD:
|
||||||
symex_start_thread(state);
|
symex_start_thread(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case END_THREAD:
|
case END_THREAD:
|
||||||
// behaves like assume(0);
|
// behaves like assume(0);
|
||||||
if(!state.guard.is_false())
|
if(!state.guard.is_false())
|
||||||
state.guard.add(false_exprt());
|
state.guard.add(false_exprt());
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case ATOMIC_BEGIN:
|
case ATOMIC_BEGIN:
|
||||||
symex_atomic_begin(state);
|
symex_atomic_begin(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case ATOMIC_END:
|
case ATOMIC_END:
|
||||||
symex_atomic_end(state);
|
symex_atomic_end(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case CATCH:
|
case CATCH:
|
||||||
symex_catch(state);
|
symex_catch(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case THROW:
|
case THROW:
|
||||||
symex_throw(state);
|
symex_throw(state);
|
||||||
state.source.pc++;
|
symex_transition(state);
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case NO_INSTRUCTION_TYPE:
|
case NO_INSTRUCTION_TYPE:
|
||||||
|
|
Loading…
Reference in New Issue