SSA trace: don't concretise steps that will subsequently be dropped

Previously the SSA trace did all concretisation (taking the solver's output
and turning it into concrete expressions to be output in the result trace) before
sorting the steps by time and determining what belongs in the final trace. This
was generally harmless, but could result in much wasted time and potentially
memory exhaustion when concretising very large arrays and strings.

Therefore, we now perform the time-order sort and figure out which steps are
to be kept first, *then* concretise them.

Author: smowton

src/cbmc/all_properties.cpp

@@ -41,10 +41,7 @@ void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
       if(solver.l_get(cond).is_false())
       {
         g.second.status=goalt::statust::FAILURE;
-        symex_target_equationt::SSA_stepst::iterator next=c;
-        next++; // include the assertion
-        build_goto_trace(bmc.equation, next, solver, bmc.ns,
-                         g.second.goto_trace);
+        build_goto_trace(bmc.equation, c, solver, bmc.ns, g.second.goto_trace);
         break;
       }
     }

src/cbmc/bmc_cover.cpp

@@ -144,6 +144,13 @@ class bmc_covert:
   bmct &bmc;
 };
 
+static bool is_failed_assumption_step(
+  symex_target_equationt::SSA_stepst::const_iterator step,
+  const prop_convt &prop_conv)
+{
+  return step->is_assume() && prop_conv.l_get(step->cond_literal).is_false();
+}
+
 void bmc_covert::satisfying_assignment()
 {
   tests.push_back(testt());
@@ -173,21 +180,8 @@ void bmc_covert::satisfying_assignment()
     }
   }
 
-  build_goto_trace(bmc.equation, bmc.equation.SSA_steps.end(),
-                   solver, bmc.ns, test.goto_trace);
-
-  goto_tracet &goto_trace=test.goto_trace;
-
-  // Now delete anything after first failed assumption
-  for(goto_tracet::stepst::iterator
-      s_it1=goto_trace.steps.begin();
-      s_it1!=goto_trace.steps.end();
-      s_it1++)
-    if(s_it1->is_assume() && !s_it1->cond_value)
-    {
-      goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
-      break;
-    }
+  build_goto_trace(
+    bmc.equation, is_failed_assumption_step, solver, bmc.ns, test.goto_trace);
 }
 
 bool bmc_covert::operator()()

src/cbmc/fault_localization.cpp

@@ -336,10 +336,8 @@ void fault_localizationt::goal_covered(
       if(solver.l_get(cond).is_false())
       {
         goal_pair.second.status=goalt::statust::FAILURE;
-        symex_target_equationt::SSA_stepst::iterator next=inst;
-        next++; // include the assertion
         build_goto_trace(
-          bmc.equation, next, solver, bmc.ns, goal_pair.second.goto_trace);
+          bmc.equation, inst, solver, bmc.ns, goal_pair.second.goto_trace);
 
         // localize faults
         run(goal_pair.first);

src/goto-symex/build_goto_trace.cpp

@@ -164,7 +164,7 @@ void update_internal_field(
 
 void build_goto_trace(
   const symex_target_equationt &target,
-  symex_target_equationt::SSA_stepst::const_iterator end_step,
+  ssa_step_predicatet is_last_step_to_keep,
   const prop_convt &prop_conv,
   const namespacet &ns,
   goto_tracet &goto_trace)
@@ -173,21 +173,28 @@ void build_goto_trace(
   // Furthermore, read-events need to occur before write
   // events with the same clock.
 
-  typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
+  typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
+  typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
   time_mapt time_map;
 
   mp_integer current_time=0;
 
-  const goto_trace_stept *end_ptr=nullptr;
-  bool end_step_seen=false;
+  ssa_step_iteratort last_step_to_keep = target.SSA_steps.end();
+  bool last_step_was_kept = false;
 
-  for(symex_target_equationt::SSA_stepst::const_iterator
-      it=target.SSA_steps.begin();
-      it!=target.SSA_steps.end();
+  // First sort the SSA steps by time, in the process dropping steps
+  // we definitely don't want to retain in the final trace:
+
+  for(ssa_step_iteratort it = target.SSA_steps.begin();
+      it != target.SSA_steps.end();
       it++)
   {
-    if(it==end_step)
-      end_step_seen=true;
+    if(
+      last_step_to_keep == target.SSA_steps.end() &&
+      is_last_step_to_keep(it, prop_conv))
+    {
+      last_step_to_keep = it;
+    }
 
     const symex_target_equationt::SSA_stept &SSA_step=*it;
 
@@ -227,12 +234,21 @@ void build_goto_trace(
 
       if(time_before<0)
       {
-        time_mapt::iterator entry=
-          time_map.insert(std::make_pair(
-              current_time,
-              goto_tracet::stepst())).first;
-        entry->second.splice(entry->second.end(), time_map[time_before]);
-        time_map.erase(time_before);
+        time_mapt::const_iterator time_before_steps_it =
+          time_map.find(time_before);
+
+        if(time_before_steps_it != time_map.end())
+        {
+          std::vector<ssa_step_iteratort> &current_time_steps =
+            time_map[current_time];
+
+          current_time_steps.insert(
+            current_time_steps.end(),
+            time_before_steps_it->second.begin(),
+            time_before_steps_it->second.end());
+
+          time_map.erase(time_before_steps_it);
+        }
       }
 
       continue;
@@ -248,97 +264,128 @@ void build_goto_trace(
       continue;
     }
 
-    goto_tracet::stepst &steps=time_map[current_time];
-    steps.push_back(goto_trace_stept());
-    goto_trace_stept &goto_trace_step=steps.back();
-    if(!end_step_seen)
-      end_ptr=&goto_trace_step;
-
-    goto_trace_step.thread_nr=SSA_step.source.thread_nr;
-    goto_trace_step.pc=SSA_step.source.pc;
-    goto_trace_step.comment=SSA_step.comment;
-    if(SSA_step.ssa_lhs.is_not_nil())
-      goto_trace_step.lhs_object=
-        ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
-    else
-      goto_trace_step.lhs_object.make_nil();
-    goto_trace_step.type=SSA_step.type;
-    goto_trace_step.hidden=SSA_step.hidden;
-    goto_trace_step.format_string=SSA_step.format_string;
-    goto_trace_step.io_id=SSA_step.io_id;
-    goto_trace_step.formatted=SSA_step.formatted;
-    goto_trace_step.identifier=SSA_step.identifier;
-
-    // update internal field for specific variables in the counterexample
-    update_internal_field(SSA_step, goto_trace_step, ns);
-
-    goto_trace_step.assignment_type=
-      (it->is_assignment()&&
-       (SSA_step.assignment_type==
-          symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER ||
-        SSA_step.assignment_type==
-          symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER))?
-      goto_trace_stept::assignment_typet::ACTUAL_PARAMETER:
-      goto_trace_stept::assignment_typet::STATE;
+    if(it == last_step_to_keep)
+    {
+      last_step_was_kept = true;
+    }
+
+    time_map[current_time].push_back(it);
+  }
 
-    if(SSA_step.original_full_lhs.is_not_nil())
-      goto_trace_step.full_lhs=
-        build_full_lhs_rec(
-          prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
+  INVARIANT(
+    last_step_to_keep == target.SSA_steps.end() || last_step_was_kept,
+    "last step in SSA trace to keep must not be filtered out as a sync "
+    "instruction, not-taken branch, PHI node, or similar");
 
-    if(SSA_step.ssa_lhs.is_not_nil())
-      goto_trace_step.lhs_object_value=prop_conv.get(SSA_step.ssa_lhs);
+  // Now build the GOTO trace, ordered by time, then by SSA trace order.
 
-    if(SSA_step.ssa_full_lhs.is_not_nil())
-    {
-      goto_trace_step.full_lhs_value=prop_conv.get(SSA_step.ssa_full_lhs);
-      simplify(goto_trace_step.full_lhs_value, ns);
-    }
+  // produce the step numbers
+  unsigned step_nr = 0;
 
-    for(const auto &j : SSA_step.converted_io_args)
+  for(const auto &time_and_ssa_steps : time_map)
+  {
+    for(const auto ssa_step_it : time_and_ssa_steps.second)
     {
-      if(j.is_constant() ||
-         j.id()==ID_string_constant)
-        goto_trace_step.io_args.push_back(j);
+      const auto &SSA_step = *ssa_step_it;
+      goto_trace.steps.push_back(goto_trace_stept());
+      goto_trace_stept &goto_trace_step = goto_trace.steps.back();
+
+      goto_trace_step.step_nr = ++step_nr;
+
+      goto_trace_step.thread_nr = SSA_step.source.thread_nr;
+      goto_trace_step.pc = SSA_step.source.pc;
+      goto_trace_step.comment = SSA_step.comment;
+      if(SSA_step.ssa_lhs.is_not_nil())
+      {
+        goto_trace_step.lhs_object =
+          ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
+      }
       else
       {
-        exprt tmp=prop_conv.get(j);
-        goto_trace_step.io_args.push_back(tmp);
+        goto_trace_step.lhs_object.make_nil();
       }
-    }
+      goto_trace_step.type = SSA_step.type;
+      goto_trace_step.hidden = SSA_step.hidden;
+      goto_trace_step.format_string = SSA_step.format_string;
+      goto_trace_step.io_id = SSA_step.io_id;
+      goto_trace_step.formatted = SSA_step.formatted;
+      goto_trace_step.identifier = SSA_step.identifier;
+
+      // update internal field for specific variables in the counterexample
+      update_internal_field(SSA_step, goto_trace_step, ns);
+
+      goto_trace_step.assignment_type =
+        (SSA_step.is_assignment() &&
+         (SSA_step.assignment_type ==
+          symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER ||
+          SSA_step.assignment_type ==
+          symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER))
+        ? goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
+        : goto_trace_stept::assignment_typet::STATE;
 
-    if(SSA_step.is_assert() ||
-       SSA_step.is_assume() ||
-       SSA_step.is_goto())
-    {
-      goto_trace_step.cond_expr=SSA_step.cond_expr;
+      if(SSA_step.original_full_lhs.is_not_nil())
+      {
+        goto_trace_step.full_lhs = build_full_lhs_rec(
+            prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
+      }
+
+      if(SSA_step.ssa_lhs.is_not_nil())
+        goto_trace_step.lhs_object_value = prop_conv.get(SSA_step.ssa_lhs);
 
-      goto_trace_step.cond_value=
-        prop_conv.l_get(SSA_step.cond_literal).is_true();
+      if(SSA_step.ssa_full_lhs.is_not_nil())
+      {
+        goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
+        simplify(goto_trace_step.full_lhs_value, ns);
+      }
+
+      for(const auto &j : SSA_step.converted_io_args)
+      {
+        if(j.is_constant() || j.id() == ID_string_constant)
+        {
+          goto_trace_step.io_args.push_back(j);
+        }
+        else
+        {
+          exprt tmp = prop_conv.get(j);
+          goto_trace_step.io_args.push_back(tmp);
+        }
+      }
+
+      if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
+      {
+        goto_trace_step.cond_expr = SSA_step.cond_expr;
+
+        goto_trace_step.cond_value =
+          prop_conv.l_get(SSA_step.cond_literal).is_true();
+      }
+
+      if(ssa_step_it == last_step_to_keep)
+        return;
     }
   }
+}
 
-  // Now assemble into a single goto_trace.
-  // This exploits sorted-ness of the map.
-  for(auto &t_it : time_map)
-    goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
-
-  // cut off the trace at the desired end
-  for(goto_tracet::stepst::iterator
-      s_it1=goto_trace.steps.begin();
-      s_it1!=goto_trace.steps.end();
-      ++s_it1)
-    if(end_step_seen && end_ptr==&(*s_it1))
-    {
-      goto_trace.trim_after(s_it1);
-      break;
-    }
+void build_goto_trace(
+  const symex_target_equationt &target,
+  symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
+  const prop_convt &prop_conv,
+  const namespacet &ns,
+  goto_tracet &goto_trace)
+{
+  const auto is_last_step_to_keep = [last_step_to_keep](
+    symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
+    return last_step_to_keep == it;
+  };
 
-  // produce the step numbers
-  unsigned step_nr=0;
+  return build_goto_trace(
+    target, is_last_step_to_keep, prop_conv, ns, goto_trace);
+}
 
-  for(auto &s_it : goto_trace.steps)
-    s_it.step_nr=++step_nr;
+static bool is_failed_assertion_step(
+  symex_target_equationt::SSA_stepst::const_iterator step,
+  const prop_convt &prop_conv)
+{
+  return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
 }
 
 void build_goto_trace(
@@ -347,17 +394,5 @@ void build_goto_trace(
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  build_goto_trace(
-    target, target.SSA_steps.end(), prop_conv, ns, goto_trace);
-
-  // Now delete anything after first failed assertion
-  for(goto_tracet::stepst::iterator
-      s_it1=goto_trace.steps.begin();
-      s_it1!=goto_trace.steps.end();
-      s_it1++)
-    if(s_it1->is_assert() && !s_it1->cond_value)
-    {
-      goto_trace.trim_after(s_it1);
-      break;
-    }
+  build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
 }

src/goto-symex/build_goto_trace.h

@@ -24,10 +24,22 @@ void build_goto_trace(
   const namespacet &ns,
   goto_tracet &goto_trace);
 
-// builds a trace that stops after given step
+// builds a trace that stops after the given step
 void build_goto_trace(
   const symex_target_equationt &target,
-  symex_target_equationt::SSA_stepst::const_iterator stop,
+  symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
+  const prop_convt &prop_conv,
+  const namespacet &ns,
+  goto_tracet &goto_trace);
+
+typedef std::function<
+  bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)>
+  ssa_step_predicatet;
+
+// builds a trace that stops after the step matching a given condition
+void build_goto_trace(
+  const symex_target_equationt &target,
+  ssa_step_predicatet stop_after_predicate,
   const prop_convt &prop_conv,
   const namespacet &ns,
   goto_tracet &goto_trace);