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

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;
+    }
 
-    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);
+    time_map[current_time].push_back(it);
+  }
 
-    if(SSA_step.ssa_lhs.is_not_nil())
-      goto_trace_step.lhs_object_value=prop_conv.get(SSA_step.ssa_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_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);
-    }
+  // Now build the GOTO trace, ordered by time, then by SSA trace order.
+
+  // 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.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.is_assert() ||
-       SSA_step.is_assume() ||
-       SSA_step.is_goto())
-    {
-      goto_trace_step.cond_expr=SSA_step.cond_expr;
+      if(SSA_step.ssa_lhs.is_not_nil())
+        goto_trace_step.lhs_object_value = prop_conv.get(SSA_step.ssa_lhs);
+
+      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);
+        }
+      }
 
-      goto_trace_step.cond_value=
-        prop_conv.l_get(SSA_step.cond_literal).is_true();
+      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);