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;