replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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.
This commit is contained in:
Michael Tautschnig 2017-07-03 18:47:41 +01:00
parent 5fc1ca689e
commit 21afd2f173
4 changed files with 64 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/goto-symex/goto_symex.h
View File

@ -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);

8
src/goto-symex/symex_function_call.cpp
View File

@ -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);

19
src/goto-symex/symex_goto.cpp
View File

@ -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())

61
src/goto-symex/symex_main.cpp
View File

@ -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: