Merge pull request #1128 from diffblue/sva-from-to

SVA: use `from`/`to` instead of `lower`/`upper`

Author: kroening

src/ebmc/completeness_threshold.cpp

@@ -39,13 +39,12 @@ bool has_low_completeness_threshold(const exprt &expr)
     auto &always_expr = to_sva_ranged_always_expr(expr);
     if(has_temporal_operator(always_expr.op()))
       return false;
-    else if(always_expr.upper().is_constant())
+    else if(always_expr.to().is_constant())
     {
-      auto lower_int = numeric_cast_v<mp_integer>(always_expr.lower());
-      auto upper_int =
-        numeric_cast_v<mp_integer>(to_constant_expr(always_expr.upper()));
-      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
-             upper_int <= 1;
+      auto from_int = numeric_cast_v<mp_integer>(always_expr.from());
+      auto to_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(always_expr.to()));
+      return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
     }
     else
       return false;
@@ -57,10 +56,9 @@ bool has_low_completeness_threshold(const exprt &expr)
       return false;
     else
     {
-      auto lower_int = numeric_cast_v<mp_integer>(s_always_expr.lower());
-      auto upper_int = numeric_cast_v<mp_integer>(s_always_expr.upper());
-      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
-             upper_int <= 1;
+      auto from_int = numeric_cast_v<mp_integer>(s_always_expr.from());
+      auto to_int = numeric_cast_v<mp_integer>(s_always_expr.to());
+      return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
     }
   }
   else if(

src/temporal-logic/ltl_sva_to_string.cpp

@@ -161,16 +161,16 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     auto &always = to_sva_ranged_always_expr(expr);
     auto new_expr = unary_exprt{ID_sva_ranged_always, always.op()};
-    auto lower = numeric_cast_v<mp_integer>(always.lower());
+    auto from = numeric_cast_v<mp_integer>(always.from());
     if(!always.is_range())
-      return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + "]", new_expr, mode);
     else if(always.is_unbounded())
-      return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
     else
     {
-      auto upper = numeric_cast_v<mp_integer>(to_constant_expr(always.upper()));
+      auto to = numeric_cast_v<mp_integer>(to_constant_expr(always.to()));
       return prefix(
-        "F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
+        "F[" + integer2string(from) + ":" + integer2string(to) + "]",
         new_expr,
         mode);
     }
@@ -188,19 +188,19 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     expr.id() == ID_sva_ranged_s_eventually || expr.id() == ID_sva_eventually)
   {
     PRECONDITION(mode == PROPERTY);
+
     auto &eventually = to_sva_ranged_predicate_exprt(expr);
     auto new_expr = unary_exprt{expr.id(), eventually.op()};
-    auto lower = numeric_cast_v<mp_integer>(eventually.lower());
+    auto from = numeric_cast_v<mp_integer>(eventually.from());
     if(!eventually.is_range())
-      return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + "]", new_expr, mode);
     else if(eventually.is_unbounded())
-      return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
     else
     {
-      auto upper =
-        numeric_cast_v<mp_integer>(to_constant_expr(eventually.upper()));
+      auto to = numeric_cast_v<mp_integer>(to_constant_expr(eventually.to()));
       return prefix(
-        "F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
+        "F[" + integer2string(from) + ":" + integer2string(to) + "]",
         new_expr,
         mode);
     }

src/temporal-logic/nnf.cpp

@@ -79,14 +79,14 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // not always [x:y] p --> s_eventually [x:y] not p
     auto &always = to_sva_ranged_always_expr(expr);
     return sva_ranged_s_eventually_exprt{
-      always.lower(), always.upper(), not_exprt{always.op()}};
+      always.from(), always.to(), not_exprt{always.op()}};
   }
   else if(expr.id() == ID_sva_s_always)
   {
     // not s_always [x:y] p --> eventually [x:y] not p
     auto &s_always = to_sva_s_always_expr(expr);
     return sva_eventually_exprt{
-      s_always.lower(), s_always.upper(), not_exprt{s_always.op()}};
+      s_always.from(), s_always.to(), not_exprt{s_always.op()}};
   }
   else if(expr.id() == ID_sva_s_eventually)
   {
@@ -98,7 +98,7 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // not eventually[i:j] p --> s_always[i:j] not p
     auto &eventually = to_sva_eventually_expr(expr);
     return sva_s_always_exprt{
-      eventually.lower(), eventually.upper(), not_exprt{eventually.op()}};
+      eventually.from(), eventually.to(), not_exprt{eventually.op()}};
   }
   else if(expr.id() == ID_sva_until)
   {

src/temporal-logic/sva_to_ltl.cpp

@@ -57,28 +57,28 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     if(rec.has_value())
     {
       // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
 
       // Is there an upper end of the range?
-      if(ranged_always.upper().is_constant())
+      if(ranged_always.to().is_constant())
       {
         // upper end set
-        auto upper_int =
-          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.upper()));
-        PRECONDITION(upper_int >= lower_int);
-        auto diff = upper_int - lower_int;
+        auto to_int =
+          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.to()));
+        PRECONDITION(to_int >= from_int);
+        auto diff = to_int - from_int;
 
         exprt::operandst conjuncts;
 
         for(auto i = 0; i <= diff; i++)
           conjuncts.push_back(n_Xes(i, rec.value()));
 
-        return n_Xes(lower_int, conjunction(conjuncts));
+        return n_Xes(from_int, conjunction(conjuncts));
       }
-      else if(ranged_always.upper().id() == ID_infinity)
+      else if(ranged_always.to().id() == ID_infinity)
       {
         // always [l:$] op ---> X ... X G op
-        return n_Xes(lower_int, G_exprt{rec.value()});
+        return n_Xes(from_int, G_exprt{rec.value()});
       }
       else
         PRECONDITION(false);
@@ -93,17 +93,17 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     if(rec.has_value())
     {
       // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
-      auto upper_int = numeric_cast_v<mp_integer>(ranged_always.upper());
-      PRECONDITION(upper_int >= lower_int);
-      auto diff = upper_int - lower_int;
+      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
+      auto to_int = numeric_cast_v<mp_integer>(ranged_always.to());
+      PRECONDITION(to_int >= from_int);
+      auto diff = to_int - from_int;
 
       exprt::operandst conjuncts;
 
       for(auto i = 0; i <= diff; i++)
         conjuncts.push_back(n_Xes(i, rec.value()));
 
-      return n_Xes(lower_int, conjunction(conjuncts));
+      return n_Xes(from_int, conjunction(conjuncts));
     }
     else
       return {};

src/temporal-logic/trivial_sva.cpp

@@ -113,7 +113,7 @@ exprt trivial_sva(exprt expr)
   }
   else if(expr.id() == ID_sva_case)
   {
-    expr = to_sva_case_expr(expr).lowering();
+    expr = to_sva_case_expr(expr).lower();
   }
 
   // rewrite the operands, recursively

src/trans-word-level/property.cpp

@@ -213,24 +213,22 @@ static obligationst property_obligations_rec(
     const auto &eventually_expr = to_sva_eventually_expr(property_expr);
     const auto &op = eventually_expr.op();
 
-    mp_integer lower;
-    if(to_integer_non_constant(eventually_expr.lower(), lower))
-      throw "failed to convert sva_eventually index";
+    mp_integer from = numeric_cast_v<mp_integer>(eventually_expr.from());
 
-    mp_integer upper;
-    if(to_integer_non_constant(eventually_expr.upper(), upper))
+    mp_integer to;
+    if(to_integer_non_constant(eventually_expr.to(), to))
       throw "failed to convert sva_eventually index";
 
     // We rely on NNF.
-    if(current + lower >= no_timeframes || current + upper >= no_timeframes)
+    if(current + from >= no_timeframes || current + to >= no_timeframes)
     {
       DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
       return obligationst{no_timeframes - 1, true_exprt()};
     }
 
     exprt::operandst disjuncts = {};
 
-    for(mp_integer u = current + lower; u <= current + upper; ++u)
+    for(mp_integer u = current + from; u <= current + to; ++u)
     {
       auto obligations_rec = property_obligations_rec(op, u, no_timeframes);
       disjuncts.push_back(obligations_rec.conjunction().second);
@@ -283,29 +281,24 @@ static obligationst property_obligations_rec(
   }
   else if(property_expr.id() == ID_sva_ranged_s_eventually)
   {
-    auto &phi = to_sva_ranged_s_eventually_expr(property_expr).op();
-    auto &lower = to_sva_ranged_s_eventually_expr(property_expr).lower();
-    auto &upper = to_sva_ranged_s_eventually_expr(property_expr).upper();
+    const auto &s_eventually = to_sva_ranged_s_eventually_expr(property_expr);
+    auto from = numeric_cast_v<mp_integer>(s_eventually.from());
 
-    auto from_opt = numeric_cast<mp_integer>(lower);
-    if(!from_opt.has_value())
-      throw ebmc_errort() << "failed to convert SVA s_eventually from index";
-
-    if(*from_opt < 0)
+    if(from < 0)
       throw ebmc_errort() << "SVA s_eventually from index must not be negative";
 
-    auto from = std::min(no_timeframes - 1, current + *from_opt);
+    from = std::min(no_timeframes - 1, current + from);
 
     mp_integer to;
 
-    if(upper.id() == ID_infinity)
+    if(s_eventually.is_unbounded())
     {
       throw ebmc_errort()
         << "failed to convert SVA s_eventually to index (infinity)";
     }
     else
     {
-      auto to_opt = numeric_cast<mp_integer>(upper);
+      auto to_opt = numeric_cast<mp_integer>(s_eventually.to());
       if(!to_opt.has_value())
         throw ebmc_errort() << "failed to convert SVA s_eventually to index";
       to = std::min(current + *to_opt, no_timeframes - 1);
@@ -316,7 +309,8 @@ static obligationst property_obligations_rec(
 
     for(mp_integer c = from; c <= to; ++c)
     {
-      auto tmp = property_obligations_rec(phi, c, no_timeframes).conjunction();
+      auto tmp = property_obligations_rec(s_eventually.op(), c, no_timeframes)
+                   .conjunction();
       time = std::max(time, tmp.first);
       disjuncts.push_back(tmp.second);
     }
@@ -330,14 +324,14 @@ static obligationst property_obligations_rec(
     auto &phi = property_expr.id() == ID_sva_ranged_always
                   ? to_sva_ranged_always_expr(property_expr).op()
                   : to_sva_s_always_expr(property_expr).op();
-    auto &lower = property_expr.id() == ID_sva_ranged_always
-                    ? to_sva_ranged_always_expr(property_expr).lower()
-                    : to_sva_s_always_expr(property_expr).lower();
-    auto &upper = property_expr.id() == ID_sva_ranged_always
-                    ? to_sva_ranged_always_expr(property_expr).upper()
-                    : to_sva_s_always_expr(property_expr).upper();
-
-    auto from_opt = numeric_cast<mp_integer>(lower);
+    auto &from_expr = property_expr.id() == ID_sva_ranged_always
+                        ? to_sva_ranged_always_expr(property_expr).from()
+                        : to_sva_s_always_expr(property_expr).from();
+    auto &to_expr = property_expr.id() == ID_sva_ranged_always
+                      ? to_sva_ranged_always_expr(property_expr).to()
+                      : to_sva_s_always_expr(property_expr).to();
+
+    auto from_opt = numeric_cast<mp_integer>(from_expr);
     if(!from_opt.has_value())
       throw ebmc_errort() << "failed to convert SVA always from index";
 
@@ -348,13 +342,13 @@ static obligationst property_obligations_rec(
 
     mp_integer to;
 
-    if(upper.id() == ID_infinity)
+    if(to_expr.id() == ID_infinity)
     {
       to = no_timeframes - 1;
     }
     else
     {
-      auto to_opt = numeric_cast<mp_integer>(upper);
+      auto to_opt = numeric_cast<mp_integer>(to_expr);
       if(!to_opt.has_value())
         throw ebmc_errort() << "failed to convert SVA always to index";
       to = std::min(current + *to_opt, no_timeframes - 1);

src/verilog/expr2verilog.cpp

@@ -460,11 +460,11 @@ expr2verilogt::resultt expr2verilogt::convert_sva_ranged_predicate(
 {
   std::string range_str;
 
-  range_str = "[" + convert(src.lower()) + ':';
-  if(src.upper().id() == ID_infinity)
+  range_str = "[" + convert(src.from()) + ':';
+  if(src.is_unbounded())
     range_str += "$";
   else
-    range_str += convert(src.upper());
+    range_str += convert(src.to());
   range_str += "] ";
 
   auto &src_op = src.op();

src/verilog/sva_expr.cpp

@@ -29,7 +29,7 @@ exprt sva_cycle_delay_star_exprt::lower() const
     op()};
 }
 
-exprt sva_case_exprt::lowering() const
+exprt sva_case_exprt::lower() const
 {
   auto &case_items = this->case_items();
 
@@ -51,7 +51,7 @@ exprt sva_case_exprt::lowering() const
   reduced.case_items().erase(reduced.case_items().begin());
 
   // rec. call
-  auto reduced_rec = reduced.lowering();
+  auto reduced_rec = reduced.lower();
 
   return if_exprt{
     disjunction(disjuncts), case_items.front().result(), reduced_rec};