Symex: restore guards on function exit
Executing a function may have a cumulative effect on the state guard. For example, if the callee contained ASSUME statements that rendered one or more control-flow options unviable then the guard might still embody that restriction (i.e. for if(x) ASSUME(false) the guard might still be `!x`). However, on function return we know that all control-flow paths have converged or been shown to be unviable, so we can restore the simpler guard as it was when we entered the callee function. Exceptions: (a) if the guard is false it would be correct but inefficient to restore it; keep it false until we find a convergeance with another viable path (b) if we're doing path-sensitive symex then we do tail duplication, and there are no control-flow convergeances. Keep the guard as-was. (c) if we're executing a multi-threaded program then symex_assume_l2 uses the guard to accumulate assumptions, which we must not discard. In truth this optimisation is applicable whenever a block postdominates another, but function structure gives us a cheap way to establish postdominance without analysis (in the absence of setjmp/longjmp at least)
This commit is contained in:
parent
719e9a985d
commit
ef6005dd6f
|
@ -0,0 +1,19 @@
|
||||||
|
void g()
|
||||||
|
{
|
||||||
|
g();
|
||||||
|
}
|
||||||
|
|
||||||
|
void f(int y)
|
||||||
|
{
|
||||||
|
if(y == 5)
|
||||||
|
{
|
||||||
|
g();
|
||||||
|
y = 10;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(int argc, char **argv)
|
||||||
|
{
|
||||||
|
f(argc);
|
||||||
|
assert(argc == 1);
|
||||||
|
}
|
|
@ -0,0 +1,14 @@
|
||||||
|
CORE paths-lifo-expected-failure
|
||||||
|
test.c
|
||||||
|
--show-vcc --unwind 10
|
||||||
|
^\{1\} main::argc!0@1#1 = 1$
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
|
||||||
|
--
|
||||||
|
This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form
|
||||||
|
'guard => condition'). Such a guard is redundant, but could be added before goto-symex
|
||||||
|
made sure to restore guards to their state at function entry.
|
||||||
|
We also check that no VCC is created for the unreachable code 'y = 10;'
|
||||||
|
--paths mode is excluded as it currently always accrues large guards as it proceeds through execution
|
|
@ -0,0 +1,11 @@
|
||||||
|
CORE
|
||||||
|
test.c
|
||||||
|
--unwind 10
|
||||||
|
^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
The main test is in test.desc; this just checks that the test is executable and
|
||||||
|
the assertion fails as expected.
|
|
@ -0,0 +1,16 @@
|
||||||
|
void f(int y)
|
||||||
|
{
|
||||||
|
if(y == 5)
|
||||||
|
{
|
||||||
|
for(int i = 0; i < 20; ++i)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
y = 10;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(int argc, char **argv)
|
||||||
|
{
|
||||||
|
f(argc);
|
||||||
|
assert(argc == 1);
|
||||||
|
}
|
|
@ -0,0 +1,12 @@
|
||||||
|
CORE paths-lifo-expected-failure
|
||||||
|
test.c
|
||||||
|
--show-vcc --unwind 10
|
||||||
|
^\{1\} main::argc!0@1#1 = 1$
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form
|
||||||
|
'guard => condition'). Such a guard is redundant, but could be added before goto-symex
|
||||||
|
made sure to restore guards to their state at function entry.
|
||||||
|
--paths mode is excluded as it currently always accrues large guards as it proceeds through execution
|
|
@ -0,0 +1,11 @@
|
||||||
|
CORE
|
||||||
|
test.c
|
||||||
|
--unwind 10
|
||||||
|
^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
The main test is in test.desc; this just checks that the test is executable and
|
||||||
|
the assertion fails as expected.
|
|
@ -0,0 +1,9 @@
|
||||||
|
FUTURE
|
||||||
|
test.c
|
||||||
|
--show-vcc --unwind 10
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
|
||||||
|
--
|
||||||
|
We also check that no VCC is created for the unreachable code 'y = 10;'
|
|
@ -0,0 +1,19 @@
|
||||||
|
void g(int x)
|
||||||
|
{
|
||||||
|
return g(x + 1);
|
||||||
|
}
|
||||||
|
|
||||||
|
void f(int y)
|
||||||
|
{
|
||||||
|
if(y == 5)
|
||||||
|
{
|
||||||
|
g(1);
|
||||||
|
y = 10;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(int argc, char **argv)
|
||||||
|
{
|
||||||
|
f(argc);
|
||||||
|
assert(argc == 1);
|
||||||
|
}
|
|
@ -0,0 +1,14 @@
|
||||||
|
CORE paths-lifo-expected-failure
|
||||||
|
test.c
|
||||||
|
--show-vcc --depth 1000
|
||||||
|
^\{1\} main::argc!0@1#1 = 1$
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
|
||||||
|
--
|
||||||
|
This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form
|
||||||
|
'guard => condition'). Such a guard is redundant, but could be added before goto-symex
|
||||||
|
made sure to restore guards to their state at function entry.
|
||||||
|
We also check that no VCC is created for the unreachable code 'y = 10;'
|
||||||
|
--paths mode is excluded as it currently always accrues large guards as it proceeds through execution
|
|
@ -0,0 +1,11 @@
|
||||||
|
CORE
|
||||||
|
test.c
|
||||||
|
--depth 1000
|
||||||
|
^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
The main test is in test.desc; this just checks that the test is executable and
|
||||||
|
the assertion fails as expected.
|
|
@ -0,0 +1,14 @@
|
||||||
|
void f(int y)
|
||||||
|
{
|
||||||
|
if(y == 5)
|
||||||
|
{
|
||||||
|
__CPROVER_assume(0);
|
||||||
|
y = 10;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(int argc, char **argv)
|
||||||
|
{
|
||||||
|
f(argc);
|
||||||
|
assert(argc == 1);
|
||||||
|
}
|
|
@ -0,0 +1,12 @@
|
||||||
|
CORE paths-lifo-expected-failure
|
||||||
|
test.c
|
||||||
|
--show-vcc
|
||||||
|
^\{1\} main::argc!0@1#1 = 1$
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form
|
||||||
|
'guard => condition'). Such a guard is redundant, but could be added before goto-symex
|
||||||
|
made sure to restore guards to their state at function entry.
|
||||||
|
--paths mode is excluded as it currently always accrues large guards as it proceeds through execution
|
|
@ -0,0 +1,11 @@
|
||||||
|
CORE
|
||||||
|
test.c
|
||||||
|
|
||||||
|
^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
|
||||||
|
^VERIFICATION FAILED$
|
||||||
|
^EXIT=10$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
--
|
||||||
|
The main test is in test.desc; this just checks that the test is executable and
|
||||||
|
the assertion fails as expected.
|
|
@ -0,0 +1,9 @@
|
||||||
|
FUTURE
|
||||||
|
test.c
|
||||||
|
--show-vcc
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
--
|
||||||
|
^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
|
||||||
|
--
|
||||||
|
We also check that no VCC is created for the unreachable code 'y = 10;'
|
|
@ -26,9 +26,10 @@ public:
|
||||||
return back();
|
return back();
|
||||||
}
|
}
|
||||||
|
|
||||||
framet &new_frame(symex_targett::sourcet calling_location)
|
framet &
|
||||||
|
new_frame(symex_targett::sourcet calling_location, const guardt &guard)
|
||||||
{
|
{
|
||||||
emplace_back(calling_location);
|
emplace_back(calling_location, guard);
|
||||||
return back();
|
return back();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -27,7 +27,7 @@ struct framet
|
||||||
std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
|
std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
|
||||||
symex_targett::sourcet calling_location;
|
symex_targett::sourcet calling_location;
|
||||||
std::vector<irep_idt> parameter_names;
|
std::vector<irep_idt> parameter_names;
|
||||||
|
guardt guard_at_function_start;
|
||||||
goto_programt::const_targett end_of_function;
|
goto_programt::const_targett end_of_function;
|
||||||
exprt return_value = nil_exprt();
|
exprt return_value = nil_exprt();
|
||||||
bool hidden_function = false;
|
bool hidden_function = false;
|
||||||
|
@ -48,8 +48,9 @@ struct framet
|
||||||
|
|
||||||
std::unordered_map<irep_idt, loop_infot> loop_iterations;
|
std::unordered_map<irep_idt, loop_infot> loop_iterations;
|
||||||
|
|
||||||
explicit framet(symex_targett::sourcet _calling_location)
|
framet(symex_targett::sourcet _calling_location, const guardt &state_guard)
|
||||||
: calling_location(std::move(_calling_location))
|
: calling_location(std::move(_calling_location)),
|
||||||
|
guard_at_function_start(state_guard)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
@ -44,7 +44,7 @@ goto_symex_statet::goto_symex_statet(
|
||||||
fresh_l2_name_provider(fresh_l2_name_provider)
|
fresh_l2_name_provider(fresh_l2_name_provider)
|
||||||
{
|
{
|
||||||
threads.emplace_back(guard_manager);
|
threads.emplace_back(guard_manager);
|
||||||
call_stack().new_frame(source);
|
call_stack().new_frame(source, guardt(true_exprt(), manager));
|
||||||
}
|
}
|
||||||
|
|
||||||
goto_symex_statet::~goto_symex_statet()=default;
|
goto_symex_statet::~goto_symex_statet()=default;
|
||||||
|
|
|
@ -303,7 +303,7 @@ void goto_symext::symex_function_call_code(
|
||||||
|
|
||||||
// produce a new frame
|
// produce a new frame
|
||||||
PRECONDITION(!state.call_stack().empty());
|
PRECONDITION(!state.call_stack().empty());
|
||||||
framet &frame = state.call_stack().new_frame(state.source);
|
framet &frame = state.call_stack().new_frame(state.source, state.guard);
|
||||||
|
|
||||||
// preserve locality of local variables
|
// preserve locality of local variables
|
||||||
locality(identifier, state, path_storage, goto_function, ns);
|
locality(identifier, state, path_storage, goto_function, ns);
|
||||||
|
@ -332,8 +332,10 @@ void goto_symext::symex_function_call_code(
|
||||||
}
|
}
|
||||||
|
|
||||||
/// pop one call frame
|
/// pop one call frame
|
||||||
static void
|
static void pop_frame(
|
||||||
pop_frame(goto_symext::statet &state, const path_storaget &path_storage)
|
goto_symext::statet &state,
|
||||||
|
const path_storaget &path_storage,
|
||||||
|
bool doing_path_exploration)
|
||||||
{
|
{
|
||||||
PRECONDITION(!state.call_stack().empty());
|
PRECONDITION(!state.call_stack().empty());
|
||||||
|
|
||||||
|
@ -347,6 +349,26 @@ pop_frame(goto_symext::statet &state, const path_storaget &path_storage)
|
||||||
// restore L1 renaming
|
// restore L1 renaming
|
||||||
state.level1.restore_from(frame.old_level1);
|
state.level1.restore_from(frame.old_level1);
|
||||||
|
|
||||||
|
// If the program is multi-threaded then the state guard is used to
|
||||||
|
// accumulate assumptions (in symex_assume_l2) and must be left alone.
|
||||||
|
// If however it is single-threaded then we should restore the guard, as the
|
||||||
|
// guard coming out of the function may be more complex (e.g. if the callee
|
||||||
|
// was { if(x) __CPROVER_assume(false); } then the guard may still be `!x`),
|
||||||
|
// but at this point all control-flow paths have either converged or been
|
||||||
|
// proven unviable, so we can stop specifying the callee's constraints when
|
||||||
|
// we generate an assumption or VCC.
|
||||||
|
|
||||||
|
// If the guard is false, *this* path is unviable and we shouldn't discard
|
||||||
|
// that knowledge. If we're doing path exploration then we do
|
||||||
|
// tail-duplication, and we actually *are* in a more-restricted context
|
||||||
|
// than we were when the function began.
|
||||||
|
if(
|
||||||
|
state.threads.size() == 1 && !state.guard.is_false() &&
|
||||||
|
!doing_path_exploration)
|
||||||
|
{
|
||||||
|
state.guard = frame.guard_at_function_start;
|
||||||
|
}
|
||||||
|
|
||||||
symex_renaming_levelt::viewt view;
|
symex_renaming_levelt::viewt view;
|
||||||
state.get_level2().current_names.get_view(view);
|
state.get_level2().current_names.get_view(view);
|
||||||
|
|
||||||
|
@ -387,7 +409,7 @@ void goto_symext::symex_end_of_function(statet &state)
|
||||||
state.guard.as_expr(), state.source.function_id, state.source, hidden);
|
state.guard.as_expr(), state.source.function_id, state.source, hidden);
|
||||||
|
|
||||||
// then get rid of the frame
|
// then get rid of the frame
|
||||||
pop_frame(state, path_storage);
|
pop_frame(state, path_storage, symex_config.doing_path_exploration);
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Preserves locality of parameters of a given function by applying L1
|
/// Preserves locality of parameters of a given function by applying L1
|
||||||
|
|
Loading…
Reference in New Issue