From ef6005dd6fca551b2afbb3875ebaa529e713d915 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 9 Aug 2019 16:52:53 +0100 Subject: [PATCH] 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) --- regression/cbmc/residual-guards-1/test.c | 19 ++++++++++++ regression/cbmc/residual-guards-1/test.desc | 14 +++++++++ .../residual-guards-1/test_execution.desc | 11 +++++++ regression/cbmc/residual-guards-2/test.c | 16 ++++++++++ regression/cbmc/residual-guards-2/test.desc | 12 ++++++++ .../residual-guards-2/test_execution.desc | 11 +++++++ .../residual-guards-2/unreachable-code.desc | 9 ++++++ regression/cbmc/residual-guards-3/test.c | 19 ++++++++++++ regression/cbmc/residual-guards-3/test.desc | 14 +++++++++ .../residual-guards-3/test_execution.desc | 11 +++++++ regression/cbmc/residual-guards-4/test.c | 14 +++++++++ regression/cbmc/residual-guards-4/test.desc | 12 ++++++++ .../residual-guards-4/test_execution.desc | 11 +++++++ .../residual-guards-4/unreachable-code.desc | 9 ++++++ src/goto-symex/call_stack.h | 5 ++-- src/goto-symex/frame.h | 7 +++-- src/goto-symex/goto_symex_state.cpp | 2 +- src/goto-symex/symex_function_call.cpp | 30 ++++++++++++++++--- 18 files changed, 216 insertions(+), 10 deletions(-) create mode 100644 regression/cbmc/residual-guards-1/test.c create mode 100644 regression/cbmc/residual-guards-1/test.desc create mode 100644 regression/cbmc/residual-guards-1/test_execution.desc create mode 100644 regression/cbmc/residual-guards-2/test.c create mode 100644 regression/cbmc/residual-guards-2/test.desc create mode 100644 regression/cbmc/residual-guards-2/test_execution.desc create mode 100644 regression/cbmc/residual-guards-2/unreachable-code.desc create mode 100644 regression/cbmc/residual-guards-3/test.c create mode 100644 regression/cbmc/residual-guards-3/test.desc create mode 100644 regression/cbmc/residual-guards-3/test_execution.desc create mode 100644 regression/cbmc/residual-guards-4/test.c create mode 100644 regression/cbmc/residual-guards-4/test.desc create mode 100644 regression/cbmc/residual-guards-4/test_execution.desc create mode 100644 regression/cbmc/residual-guards-4/unreachable-code.desc diff --git a/regression/cbmc/residual-guards-1/test.c b/regression/cbmc/residual-guards-1/test.c new file mode 100644 index 0000000000..f27e395641 --- /dev/null +++ b/regression/cbmc/residual-guards-1/test.c @@ -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); +} diff --git a/regression/cbmc/residual-guards-1/test.desc b/regression/cbmc/residual-guards-1/test.desc new file mode 100644 index 0000000000..2edbd29163 --- /dev/null +++ b/regression/cbmc/residual-guards-1/test.desc @@ -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 diff --git a/regression/cbmc/residual-guards-1/test_execution.desc b/regression/cbmc/residual-guards-1/test_execution.desc new file mode 100644 index 0000000000..e73e7239f2 --- /dev/null +++ b/regression/cbmc/residual-guards-1/test_execution.desc @@ -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. diff --git a/regression/cbmc/residual-guards-2/test.c b/regression/cbmc/residual-guards-2/test.c new file mode 100644 index 0000000000..f34a7c4225 --- /dev/null +++ b/regression/cbmc/residual-guards-2/test.c @@ -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); +} diff --git a/regression/cbmc/residual-guards-2/test.desc b/regression/cbmc/residual-guards-2/test.desc new file mode 100644 index 0000000000..0c2247e36d --- /dev/null +++ b/regression/cbmc/residual-guards-2/test.desc @@ -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 diff --git a/regression/cbmc/residual-guards-2/test_execution.desc b/regression/cbmc/residual-guards-2/test_execution.desc new file mode 100644 index 0000000000..e73e7239f2 --- /dev/null +++ b/regression/cbmc/residual-guards-2/test_execution.desc @@ -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. diff --git a/regression/cbmc/residual-guards-2/unreachable-code.desc b/regression/cbmc/residual-guards-2/unreachable-code.desc new file mode 100644 index 0000000000..889393fe66 --- /dev/null +++ b/regression/cbmc/residual-guards-2/unreachable-code.desc @@ -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;' diff --git a/regression/cbmc/residual-guards-3/test.c b/regression/cbmc/residual-guards-3/test.c new file mode 100644 index 0000000000..423dfdd0ea --- /dev/null +++ b/regression/cbmc/residual-guards-3/test.c @@ -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); +} diff --git a/regression/cbmc/residual-guards-3/test.desc b/regression/cbmc/residual-guards-3/test.desc new file mode 100644 index 0000000000..21c34f474b --- /dev/null +++ b/regression/cbmc/residual-guards-3/test.desc @@ -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 diff --git a/regression/cbmc/residual-guards-3/test_execution.desc b/regression/cbmc/residual-guards-3/test_execution.desc new file mode 100644 index 0000000000..d196319c90 --- /dev/null +++ b/regression/cbmc/residual-guards-3/test_execution.desc @@ -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. diff --git a/regression/cbmc/residual-guards-4/test.c b/regression/cbmc/residual-guards-4/test.c new file mode 100644 index 0000000000..ac72adb3c3 --- /dev/null +++ b/regression/cbmc/residual-guards-4/test.c @@ -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); +} diff --git a/regression/cbmc/residual-guards-4/test.desc b/regression/cbmc/residual-guards-4/test.desc new file mode 100644 index 0000000000..7a51b34f87 --- /dev/null +++ b/regression/cbmc/residual-guards-4/test.desc @@ -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 diff --git a/regression/cbmc/residual-guards-4/test_execution.desc b/regression/cbmc/residual-guards-4/test_execution.desc new file mode 100644 index 0000000000..1ab6c2e23d --- /dev/null +++ b/regression/cbmc/residual-guards-4/test_execution.desc @@ -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. diff --git a/regression/cbmc/residual-guards-4/unreachable-code.desc b/regression/cbmc/residual-guards-4/unreachable-code.desc new file mode 100644 index 0000000000..bc8e1deb07 --- /dev/null +++ b/regression/cbmc/residual-guards-4/unreachable-code.desc @@ -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;' diff --git a/src/goto-symex/call_stack.h b/src/goto-symex/call_stack.h index 9aeaf46458..bb97d654a1 100644 --- a/src/goto-symex/call_stack.h +++ b/src/goto-symex/call_stack.h @@ -26,9 +26,10 @@ public: 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(); } diff --git a/src/goto-symex/frame.h b/src/goto-symex/frame.h index 325829f69a..8df0db9655 100644 --- a/src/goto-symex/frame.h +++ b/src/goto-symex/frame.h @@ -27,7 +27,7 @@ struct framet std::map goto_state_map; symex_targett::sourcet calling_location; std::vector parameter_names; - + guardt guard_at_function_start; goto_programt::const_targett end_of_function; exprt return_value = nil_exprt(); bool hidden_function = false; @@ -48,8 +48,9 @@ struct framet std::unordered_map loop_iterations; - explicit framet(symex_targett::sourcet _calling_location) - : calling_location(std::move(_calling_location)) + framet(symex_targett::sourcet _calling_location, const guardt &state_guard) + : calling_location(std::move(_calling_location)), + guard_at_function_start(state_guard) { } }; diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b68ee8187b..ffc43d3f40 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -44,7 +44,7 @@ goto_symex_statet::goto_symex_statet( fresh_l2_name_provider(fresh_l2_name_provider) { 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; diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 7907699bf4..f18912b250 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -303,7 +303,7 @@ void goto_symext::symex_function_call_code( // produce a new frame 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 locality(identifier, state, path_storage, goto_function, ns); @@ -332,8 +332,10 @@ void goto_symext::symex_function_call_code( } /// pop one call frame -static void -pop_frame(goto_symext::statet &state, const path_storaget &path_storage) +static void pop_frame( + goto_symext::statet &state, + const path_storaget &path_storage, + bool doing_path_exploration) { PRECONDITION(!state.call_stack().empty()); @@ -347,6 +349,26 @@ pop_frame(goto_symext::statet &state, const path_storaget &path_storage) // restore L1 renaming 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; 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); // 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