From 7a897a583c56901d14b9471b1b5fe02af7eb8399 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 23 Oct 2018 12:31:07 +0100 Subject: [PATCH] Bugfix: store VCC counters per-path Prior to this commit, total_vccs and remaining_vccs had been members of goto_symext, meaning that they would be reset to zero every time a path was resumed. This would make CBMC incorrectly report safety for the included test program when running in path exploration mode, even though the program is reported as unsafe when CBMC runs in model-checking mode. This commit moves those members to goto_symex_statet, with goto_symext retaining cached versions so that its clients can read their values after the state has been torn down. --- regression/cbmc/path-per-path-vccs/main.c | 7 ++++ regression/cbmc/path-per-path-vccs/test.desc | 8 ++++ src/cbmc/bmc.cpp | 10 ++--- src/goto-symex/goto_symex.h | 39 +++++++++++++++++--- src/goto-symex/goto_symex_state.cpp | 2 + src/goto-symex/goto_symex_state.h | 29 +++++++++------ src/goto-symex/symex_main.cpp | 8 +++- 7 files changed, 79 insertions(+), 24 deletions(-) create mode 100644 regression/cbmc/path-per-path-vccs/main.c create mode 100644 regression/cbmc/path-per-path-vccs/test.desc diff --git a/regression/cbmc/path-per-path-vccs/main.c b/regression/cbmc/path-per-path-vccs/main.c new file mode 100644 index 00000000000..ea8cbe20745 --- /dev/null +++ b/regression/cbmc/path-per-path-vccs/main.c @@ -0,0 +1,7 @@ +int main() +{ + __CPROVER_assert(0, ""); + int x; + while(x) + --x; +} diff --git a/regression/cbmc/path-per-path-vccs/test.desc b/regression/cbmc/path-per-path-vccs/test.desc new file mode 100644 index 00000000000..d399e5b2ddb --- /dev/null +++ b/regression/cbmc/path-per-path-vccs/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--paths lifo --unwind 1 --pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 4290736f490..e2f8584b9e4 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -314,8 +314,9 @@ safety_checkert::resultt bmct::execute( } // any properties to check at all? - if(!options.get_bool_option("program-only") && - symex.remaining_vccs==0) + if( + !options.get_bool_option("program-only") && + symex.get_remaining_vccs() == 0) { report_success(); output_graphml(resultt::SAFE); @@ -392,9 +393,8 @@ void bmct::slice() } } } - statistics() << "Generated " - << symex.total_vccs<<" VCC(s), " - << symex.remaining_vccs + statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), " + << symex.get_remaining_vccs() << " remaining after simplification" << eom; } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index e13bf576cab..667f85039ef 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -60,8 +60,6 @@ class goto_symext doing_path_exploration(options.is_set("paths")), allow_pointer_unsoundness( options.get_bool_option("allow-pointer-unsoundness")), - total_vccs(0), - remaining_vccs(0), constant_propagation(true), self_loops_to_assumptions(true), language_mode(), @@ -71,7 +69,9 @@ class goto_symext atomic_section_counter(0), log(mh), guard_identifier("goto_symex::\\guard"), - path_storage(path_storage) + path_storage(path_storage), + _total_vccs(std::numeric_limits::max()), + _remaining_vccs(std::numeric_limits::max()) { } @@ -209,9 +209,6 @@ class goto_symext // these bypass the target maps virtual void symex_step_goto(statet &, bool taken); - // statistics - unsigned total_vccs, remaining_vccs; - bool constant_propagation; bool self_loops_to_assumptions; @@ -466,6 +463,36 @@ class goto_symext void rewrite_quantifiers(exprt &, statet &); path_storaget &path_storage; + +protected: + /// @{\name Statistics + /// + /// The actual number of total and remaining VCCs should be assigned to + /// the relevant members of goto_symex_statet. The members below are used to + /// cache the values from goto_symex_statet after symex has ended, so that + /// \ref bmct can read those values even after the state has been deallocated. + + unsigned _total_vccs, _remaining_vccs; + ///@} + +public: + unsigned get_total_vccs() + { + INVARIANT( + _total_vccs != std::numeric_limits::max(), + "symex_threaded_step should have been executed at least once before " + "attempting to read total_vccs"); + return _total_vccs; + } + + unsigned get_remaining_vccs() + { + INVARIANT( + _remaining_vccs != std::numeric_limits::max(), + "symex_threaded_step should have been executed at least once before " + "attempting to read remaining_vccs"); + return _remaining_vccs; + } }; #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index d312860169e..b6ea8d6274a 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -27,6 +27,8 @@ goto_symex_statet::goto_symex_statet() : depth(0), symex_target(nullptr), atomic_section_id(0), + total_vccs(0), + remaining_vccs(0), record_events(true), dirty() { diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 201389c5f4b..fd5be134a04 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -211,16 +211,19 @@ class goto_symex_statet final propagationt propagation; unsigned atomic_section_id; std::unordered_map safe_pointers; - - explicit goto_statet(const goto_symex_statet &s): - depth(s.depth), - level2_current_names(s.level2.current_names), - value_set(s.value_set), - guard(s.guard), - source(s.source), - propagation(s.propagation), - atomic_section_id(s.atomic_section_id), - safe_pointers(s.safe_pointers) + unsigned total_vccs, remaining_vccs; + + explicit goto_statet(const goto_symex_statet &s) + : depth(s.depth), + level2_current_names(s.level2.current_names), + value_set(s.value_set), + guard(s.guard), + source(s.source), + propagation(s.propagation), + atomic_section_id(s.atomic_section_id), + safe_pointers(s.safe_pointers), + total_vccs(s.total_vccs), + remaining_vccs(s.remaining_vccs) { } @@ -250,7 +253,9 @@ class goto_symex_statet final propagation(s.propagation), safe_pointers(s.safe_pointers), value_set(s.value_set), - atomic_section_id(s.atomic_section_id) + atomic_section_id(s.atomic_section_id), + total_vccs(s.total_vccs), + remaining_vccs(s.remaining_vccs) { level2.current_names = s.level2_current_names; } @@ -346,6 +351,8 @@ class goto_symex_statet final read_in_atomic_sectiont read_in_atomic_section; written_in_atomic_sectiont written_in_atomic_section; + unsigned total_vccs, remaining_vccs; + class threadt { public: diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 2127bbd2d5e..fb213414477 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -51,7 +51,7 @@ void goto_symext::vcc( const std::string &msg, statet &state) { - total_vccs++; + state.total_vccs++; exprt expr=vcc_expr; @@ -69,7 +69,7 @@ void goto_symext::vcc( state.guard.guard_expr(expr); - remaining_vccs++; + state.remaining_vccs++; target.assertion(state.guard.as_expr(), expr, msg, state.source); } @@ -149,6 +149,10 @@ void goto_symext::symex_threaded_step( statet &state, const get_goto_functiont &get_goto_function) { symex_step(get_goto_function, state); + + _total_vccs = state.total_vccs; + _remaining_vccs = state.remaining_vccs; + if(should_pause_symex) return;