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.

Author: karkhaz

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;