Merge pull request #6699 from tautschnig/cleanup/partial-loops

SSA steps: don't guess the property id, set it during construction

Author: tautschnig

Diff for: src/goto-checker/bmc_util.cpp

@@ -57,7 +57,7 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
   return [property_id](
            symex_target_equationt::SSA_stepst::const_iterator step,
            const decision_proceduret &decision_procedure) {
-    return step->is_assert() && step->get_property_id() == property_id &&
+    return step->is_assert() && step->property_id == property_id &&
            decision_procedure.get(step->cond_handle).is_false();
   };
 }
@@ -246,7 +246,7 @@ void update_properties_status_from_symex_target_equation(
     if(!step.is_assert())
       continue;
 
-    irep_idt property_id = step.get_property_id();
+    const irep_idt &property_id = step.property_id;
     CHECK_RETURN(!property_id.empty());
 
     // Don't update status of properties that are constant 'false';

Diff for: src/goto-checker/goto_symex_fault_localizer.cpp

@@ -69,10 +69,10 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
         localization_points.emplace(l, emplace_result.first);
       }
     }
-
-    // reached failed assertion?
-    if(step.is_assert() && step.get_property_id() == failed_property_id)
+    else if(step.is_assert() && step.property_id == failed_property_id)
+    {
       return step;
+    }
   }
   UNREACHABLE;
 }

Diff for: src/goto-checker/goto_symex_property_decider.cpp

@@ -51,7 +51,7 @@ void goto_symex_property_decidert::
   {
     if(it->is_assert())
     {
-      irep_idt property_id = it->get_property_id();
+      const irep_idt &property_id = it->property_id;
       CHECK_RETURN(!property_id.empty());
 
       // consider goal instance if it is in the given properties

Diff for: src/goto-symex/build_goto_trace.cpp

@@ -346,7 +346,7 @@ void build_goto_trace(
       if(SSA_step.is_assert())
       {
         goto_trace_step.comment = SSA_step.comment;
-        goto_trace_step.property_id = SSA_step.get_property_id();
+        goto_trace_step.property_id = SSA_step.property_id;
       }
       goto_trace_step.type = SSA_step.type;
       goto_trace_step.hidden = SSA_step.hidden;

Diff for: src/goto-symex/goto_symex.h

@@ -376,10 +376,16 @@ class goto_symext
     value_sett *jump_not_taken_value_set,
     const namespacet &ns);
 
+  /// Symbolically execute a verification condition (assertion).
+  /// \param cond: The guard of the assumption
+  /// \param property_id: Unique property identifier of this assertion
+  /// \param msg: The message associated with this assertion
+  /// \param state: Symbolic execution state for current instruction
   virtual void vcc(
-    const exprt &,
+    const exprt &cond,
+    const irep_idt &property_id,
     const std::string &msg,
-    statet &);
+    statet &state);
 
   /// Symbolically execute an ASSUME instruction or simulate such an execution
   /// for a synthetic assumption

Diff for: src/goto-symex/ssa_step.cpp

@@ -133,6 +133,7 @@ void SSA_stept::validate(const namespacet &ns, const validation_modet vm) const
   switch(type)
   {
   case goto_trace_stept::typet::ASSERT:
+    DATA_CHECK(vm, !property_id.empty(), "missing property id in assert step");
   case goto_trace_stept::typet::ASSUME:
   case goto_trace_stept::typet::GOTO:
   case goto_trace_stept::typet::CONSTRAINT:
@@ -185,36 +186,6 @@ void SSA_stept::validate(const namespacet &ns, const validation_modet vm) const
   }
 }
 
-irep_idt SSA_stept::get_property_id() const
-{
-  PRECONDITION(is_assert());
-
-  irep_idt property_id;
-
-  if(source.pc->is_assert())
-  {
-    property_id = source.pc->source_location().get_property_id();
-  }
-  else if(source.pc->is_goto())
-  {
-    // this is likely an unwinding assertion
-    property_id = id2string(source.pc->source_location().get_function()) +
-                  ".unwind." + std::to_string(source.pc->loop_number);
-  }
-  else if(source.pc->is_function_call())
-  {
-    // this is likely a recursion unwinding assertion
-    property_id =
-      id2string(source.pc->source_location().get_function()) + ".recursion";
-  }
-  else
-  {
-    UNREACHABLE;
-  }
-
-  return property_id;
-}
-
 SSA_assignment_stept::SSA_assignment_stept(
   symex_targett::sourcet source,
   exprt _guard,

Diff for: src/goto-symex/ssa_step.h

@@ -129,10 +129,6 @@ class SSA_stept
     return type == goto_trace_stept::typet::ATOMIC_END;
   }
 
-  /// Returns the property ID if this is a step resulting from an ASSERT, or
-  /// builds a unique name for an unwinding assertion.
-  irep_idt get_property_id() const;
-
   // we may choose to hide
   bool hidden = false;
 
@@ -149,6 +145,8 @@ class SSA_stept
   exprt cond_expr;
   exprt cond_handle;
   std::string comment;
+  // for ASSERT (which includes loop unwinding assertions)
+  irep_idt property_id;
 
   exprt get_ssa_expr() const
   {

Diff for: src/goto-symex/symex_function_call.cpp

@@ -245,7 +245,13 @@ void goto_symext::symex_function_call_post_clean(
   if(stop_recursing)
   {
     if(symex_config.unwinding_assertions)
-      vcc(false_exprt(), "recursion unwinding assertion", state);
+    {
+      vcc(
+        false_exprt(),
+        id2string(identifier) + ".recursion",
+        "recursion unwinding assertion",
+        state);
+    }
     if(!symex_config.partial_loops)
     {
       // Rule out this path:

Diff for: src/goto-symex/symex_goto.cpp

@@ -927,7 +927,7 @@ void goto_symext::loop_bound_exceeded(
   statet &state,
   const exprt &guard)
 {
-  const unsigned loop_number=state.source.pc->loop_number;
+  const std::string loop_number = std::to_string(state.source.pc->loop_number);
 
   exprt negated_cond;
 
@@ -939,9 +939,13 @@ void goto_symext::loop_bound_exceeded(
   if(symex_config.unwinding_assertions)
   {
     // Generate VCC for unwinding assertion.
+    const std::string property_id =
+      id2string(state.source.pc->source_location().get_function()) +
+      ".unwind." + loop_number;
     vcc(
       negated_cond,
-      "unwinding assertion loop " + std::to_string(loop_number),
+      property_id,
+      "unwinding assertion loop " + loop_number,
       state);
   }
 

Diff for: src/goto-symex/symex_main.cpp

@@ -176,11 +176,13 @@ void goto_symext::symex_assert(
   if(msg.empty())
     msg = "assertion";
 
-  vcc(l2_condition, msg, state);
+  vcc(
+    l2_condition, instruction.source_location().get_property_id(), msg, state);
 }
 
 void goto_symext::vcc(
   const exprt &condition,
+  const irep_idt &property_id,
   const std::string &msg,
   statet &state)
 {
@@ -193,7 +195,8 @@ void goto_symext::vcc(
   const exprt guarded_condition = state.guard.guard_expr(condition);
 
   state.remaining_vccs++;
-  target.assertion(state.guard.as_expr(), guarded_condition, msg, state.source);
+  target.assertion(
+    state.guard.as_expr(), guarded_condition, property_id, msg, state.source);
 }
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)

Diff for: src/goto-symex/symex_target.h

@@ -233,14 +233,16 @@ class symex_targett
   /// Record an assertion.
   /// \param guard: Precondition for reaching this assertion
   /// \param cond: Condition this assertion represents
+  /// \param property_id: Unique property identifier of this assertion
   /// \param msg: The message associated with this assertion
   /// \param source: Pointer to location in the input GOTO program of this
   ///  assertion
   virtual void assertion(
     const exprt &guard,
     const exprt &cond,
+    const irep_idt &property_id,
     const std::string &msg,
-    const sourcet &source)=0;
+    const sourcet &source) = 0;
 
   /// Record a goto instruction.
   /// \param guard: Precondition for reaching this goto instruction

Diff for: src/goto-symex/symex_target_equation.cpp

@@ -282,6 +282,7 @@ void symex_target_equationt::assumption(
 void symex_target_equationt::assertion(
   const exprt &guard,
   const exprt &cond,
+  const irep_idt &property_id,
   const std::string &msg,
   const sourcet &source)
 {
@@ -291,6 +292,7 @@ void symex_target_equationt::assertion(
   SSA_step.guard=guard;
   SSA_step.cond_expr=cond;
   SSA_step.comment=msg;
+  SSA_step.property_id = property_id;
 
   merge_ireps(SSA_step);
 }

Diff for: src/goto-symex/symex_target_equation.h

@@ -130,6 +130,7 @@ class symex_target_equationt:public symex_targett
   virtual void assertion(
     const exprt &guard,
     const exprt &cond,
+    const irep_idt &property_id,
     const std::string &msg,
     const sourcet &source);