Merge pull request #716 from diffblue/extract-sequence

BMC: extract instantiate_sequence into separate file

Author: tautschnig

src/trans-word-level/Makefile

@@ -4,6 +4,7 @@ SRC = counterexample_word_level.cpp \
       property.cpp \
       trans_trace_word_level.cpp \
       instantiate_word_level.cpp \
+      sequence.cpp \
       show_modules.cpp \
       show_module_hierarchy.cpp \
       unwind.cpp \

src/trans-word-level/instantiate_word_level.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <verilog/sva_expr.h>
 #include <verilog/verilog_expr.h>
 
-#include "property.h"
+#include "sequence.h"
 
 /*******************************************************************\
 
@@ -91,11 +91,6 @@ class wl_instantiatet
   [[nodiscard]] std::pair<mp_integer, exprt>
   instantiate_rec(exprt, const mp_integer &t) const;
   [[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
-
-  // Returns a list of match points and matching conditions
-  // for the given sequence expression starting at time t
-  [[nodiscard]] std::vector<std::pair<mp_integer, exprt>>
-  instantiate_sequence(exprt, const mp_integer &t) const;
 };
 
 /*******************************************************************\
@@ -121,180 +116,6 @@ static exprt default_value(const typet &type)
 
 /*******************************************************************\
 
-Function: wl_instantiatet::instantiate_sequence
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-std::vector<std::pair<mp_integer, exprt>>
-wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
-{
-  if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
-  {
-    auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);
-
-    if(sva_cycle_delay_expr.to().is_nil()) // ##1 something
-    {
-      mp_integer offset;
-      if(to_integer_non_constant(sva_cycle_delay_expr.from(), offset))
-        throw "failed to convert sva_cycle_delay offset";
-
-      const auto u = t + offset;
-
-      // Do we exceed the bound? Make it 'true'
-      if(u >= no_timeframes)
-      {
-        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
-      }
-      else
-        return instantiate_sequence(sva_cycle_delay_expr.op(), u);
-    }
-    else
-    {
-      mp_integer from, to;
-      if(to_integer_non_constant(sva_cycle_delay_expr.from(), from))
-        throw "failed to convert sva_cycle_delay offsets";
-
-      if(sva_cycle_delay_expr.to().id() == ID_infinity)
-      {
-        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        to = no_timeframes - 1;
-      }
-      else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
-        throw "failed to convert sva_cycle_delay offsets";
-
-      auto lower = t + from;
-      auto upper = t + to;
-
-      // Do we exceed the bound? Make it 'true'
-      if(upper >= no_timeframes)
-      {
-        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
-      }
-
-      std::vector<std::pair<mp_integer, exprt>> match_points;
-
-      for(mp_integer u = lower; u <= upper; ++u)
-      {
-        auto sub_result = instantiate_sequence(sva_cycle_delay_expr.op(), u);
-        for(auto &match_point : sub_result)
-          match_points.push_back(match_point);
-      }
-
-      return match_points;
-    }
-  }
-  else if(
-    expr.id() == ID_sva_sequence_concatenation ||
-    expr.id() == ID_sva_overlapped_implication ||
-    expr.id() == ID_sva_non_overlapped_implication)
-  {
-    auto &implication = to_binary_expr(expr);
-    std::vector<std::pair<mp_integer, exprt>> result;
-
-    // This is the product of the match points on the LHS and RHS
-    const auto lhs_match_points = instantiate_sequence(implication.lhs(), t);
-    for(auto &lhs_match_point : lhs_match_points)
-    {
-      // The RHS of the non-overlapped implication starts one timeframe later
-      auto t_rhs = expr.id() == ID_sva_non_overlapped_implication
-                     ? lhs_match_point.first + 1
-                     : lhs_match_point.first;
-
-      // Do we exceed the bound? Make it 'true'
-      if(t_rhs >= no_timeframes)
-      {
-        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
-      }
-
-      const auto rhs_match_points =
-        instantiate_sequence(implication.rhs(), t_rhs);
-
-      for(auto &rhs_match_point : rhs_match_points)
-      {
-        exprt cond;
-        if(expr.id() == ID_sva_sequence_concatenation)
-        {
-          cond = and_exprt{lhs_match_point.second, rhs_match_point.second};
-        }
-        else if(
-          expr.id() == ID_sva_overlapped_implication ||
-          expr.id() == ID_sva_non_overlapped_implication)
-        {
-          cond = implies_exprt{lhs_match_point.second, rhs_match_point.second};
-        }
-        else
-          PRECONDITION(false);
-
-        result.push_back({rhs_match_point.first, cond});
-      }
-    }
-
-    return result;
-  }
-  else if(expr.id() == ID_sva_sequence_intersect)
-  {
-    // IEEE 1800-2017 16.9.6
-    PRECONDITION(false);
-  }
-  else if(expr.id() == ID_sva_sequence_first_match)
-  {
-    PRECONDITION(false);
-  }
-  else if(expr.id() == ID_sva_sequence_throughout)
-  {
-    PRECONDITION(false);
-  }
-  else if(expr.id() == ID_sva_sequence_within)
-  {
-    PRECONDITION(false);
-  }
-  else if(expr.id() == ID_sva_and)
-  {
-    // IEEE 1800-2017 16.9.5
-    // 1. Both operands must match.
-    // 2. Both sequences start at the same time.
-    // 3. The end time of the composite sequence is
-    //    the end time of the operand sequence that completes last.
-    // Condition (3) is TBD.
-    exprt::operandst conjuncts;
-
-    for(auto &op : expr.operands())
-      conjuncts.push_back(instantiate_rec(op, t).second);
-
-    exprt condition = conjunction(conjuncts);
-    return {{t, condition}};
-  }
-  else if(expr.id() == ID_sva_or)
-  {
-    // IEEE 1800-2017 16.9.7
-    // The set of matches of a or b is the set union of the matches of a
-    // and the matches of b.
-    std::vector<std::pair<mp_integer, exprt>> result;
-
-    for(auto &op : expr.operands())
-      for(auto &match_point : instantiate_sequence(op, t))
-        result.push_back(match_point);
-
-    return result;
-  }
-  else
-  {
-    // not a sequence, evaluate as state predicate
-    return {instantiate_rec(expr, t)};
-  }
-}
-
-/*******************************************************************\
-
 Function: wl_instantiatet::instantiate_rec
 
   Inputs:
@@ -324,7 +145,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   {
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches
-    const auto match_points = instantiate_sequence(expr, t);
+    const auto match_points = instantiate_sequence(expr, t, no_timeframes, ns);
     exprt::operandst disjuncts;
     disjuncts.reserve(match_points.size());
     mp_integer max = t;