Merge pull request #3220 from karkhaz/kk-bugfix-per-path-vcc-counters

Bugfix: store VCC counters per-path

Author: tautschnig

regression/cbmc/path-per-path-vccs/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  __CPROVER_assert(0, "");
+  int x;
+  while(x)
+    --x;
+}

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

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;
 }
 

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<unsigned>::max()),
+      _remaining_vccs(std::numeric_limits<unsigned>::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<unsigned>::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<unsigned>::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

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

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<irep_idt, local_safe_pointerst> 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:

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;