Merge pull request #506 from diffblue/verilog_non_indexed_part_select_exprt

introduce verilog_non_indexed_part_select_exprt

Author: kroening

src/verilog/verilog_expr.h

@@ -1989,4 +1989,138 @@ inline verilog_past_exprt &to_verilog_past_expr(exprt &expr)
   return static_cast<verilog_past_exprt &>(expr);
 }
 
+class verilog_non_indexed_part_select_exprt : public ternary_exprt
+{
+public:
+  verilog_non_indexed_part_select_exprt(
+    exprt src,
+    exprt msb,
+    exprt lsb,
+    typet type)
+    : ternary_exprt(
+        ID_verilog_non_indexed_part_select,
+        std::move(src),
+        std::move(msb),
+        std::move(lsb),
+        std::move(type))
+  {
+  }
+
+  const exprt &src() const
+  {
+    return op0();
+  }
+
+  exprt &src()
+  {
+    return op0();
+  }
+
+  const exprt &msb() const
+  {
+    return op1();
+  }
+
+  exprt &msb()
+  {
+    return op1();
+  }
+
+  const exprt &lsb() const
+  {
+    return op2();
+  }
+
+  exprt &lsb()
+  {
+    return op2();
+  }
+};
+
+inline const verilog_non_indexed_part_select_exprt &
+to_verilog_non_indexed_part_select_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_non_indexed_part_select);
+  verilog_non_indexed_part_select_exprt::check(expr);
+  return static_cast<const verilog_non_indexed_part_select_exprt &>(expr);
+}
+
+inline verilog_non_indexed_part_select_exprt &
+to_verilog_non_indexed_part_select_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_non_indexed_part_select);
+  verilog_non_indexed_part_select_exprt::check(expr);
+  return static_cast<verilog_non_indexed_part_select_exprt &>(expr);
+}
+
+class verilog_indexed_part_select_plus_or_minus_exprt : public ternary_exprt
+{
+public:
+  verilog_indexed_part_select_plus_or_minus_exprt(
+    irep_idt id,
+    exprt src,
+    exprt index,
+    exprt width,
+    typet type)
+    : ternary_exprt(
+        id,
+        std::move(src),
+        std::move(index),
+        std::move(width),
+        std::move(type))
+  {
+  }
+
+  const exprt &src() const
+  {
+    return op0();
+  }
+
+  exprt &src()
+  {
+    return op0();
+  }
+
+  const exprt &index() const
+  {
+    return op1();
+  }
+
+  exprt &index()
+  {
+    return op1();
+  }
+
+  const exprt &width() const
+  {
+    return op2();
+  }
+
+  exprt &width()
+  {
+    return op2();
+  }
+};
+
+inline const verilog_indexed_part_select_plus_or_minus_exprt &
+to_verilog_indexed_part_select_plus_or_minus_expr(const exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_verilog_indexed_part_select_plus ||
+    expr.id() == ID_verilog_indexed_part_select_minus);
+  verilog_indexed_part_select_plus_or_minus_exprt::check(expr);
+  return static_cast<const verilog_indexed_part_select_plus_or_minus_exprt &>(
+    expr);
+}
+
+inline verilog_indexed_part_select_plus_or_minus_exprt &
+to_verilog_indexed_part_select_plus_or_minus_expr(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_verilog_indexed_part_select_plus ||
+    expr.id() == ID_verilog_indexed_part_select_minus);
+  verilog_indexed_part_select_plus_or_minus_exprt::check(expr);
+  return static_cast<verilog_indexed_part_select_plus_or_minus_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -2317,70 +2317,71 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
 {
   if(expr.id() == ID_verilog_non_indexed_part_select)
   {
-    exprt &op0 = expr.op0();
-    convert_expr(op0);
+    auto &part_select = to_verilog_non_indexed_part_select_expr(expr);
+    exprt &src = part_select.src();
+    convert_expr(src);
 
-    if(op0.type().id()==ID_array)
+    if(src.type().id() == ID_array)
     {
-      throw errort().with_location(op0.source_location())
+      throw errort().with_location(src.source_location())
         << "array type not allowed in part select";
     }
 
-    if(op0.type().id() == ID_verilog_real)
+    if(src.type().id() == ID_verilog_real)
     {
-      throw errort().with_location(op0.source_location())
+      throw errort().with_location(src.source_location())
         << "real not allowed in part select";
     }
 
-    mp_integer op0_width = get_width(op0.type());
-    mp_integer op0_offset = string2integer(op0.type().get_string(ID_C_offset));
+    mp_integer src_width = get_width(src.type());
+    mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));
 
     // In non-indexed part-select expressions, both
     // indices must be constants (1800-2017 11.5.1).
-    mp_integer op1 = convert_integer_constant_expression(expr.op1());
-    mp_integer op2 = convert_integer_constant_expression(expr.op2());
+    mp_integer msb = convert_integer_constant_expression(part_select.msb());
+    mp_integer lsb = convert_integer_constant_expression(part_select.lsb());
 
-    if(op1<op2)
-      std::swap(op1, op2); // now op1>=op2
+    if(msb < lsb)
+      std::swap(msb, lsb); // now msb>=lsb
 
     // 1800-2017 sec 11.5.1: out-of-bounds bit-select is
     // x for 4-state and 0 for 2-state values. We
     // achieve that by padding the operand from either end,
     // or both.
-    if(op2 < op0_offset)
+    if(lsb < src_offset)
     {
-      auto padding_width = op0_offset - op2;
+      auto padding_width = src_offset - lsb;
       auto padding = from_integer(
         0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
       auto new_type = unsignedbv_typet{
-        numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
-      expr.op0() = concatenation_exprt(expr.op0(), padding, new_type);
-      op2 += padding_width;
-      op1 += padding_width;
+        numeric_cast_v<std::size_t>(get_width(src.type()) + padding_width)};
+      src = concatenation_exprt(src, padding, new_type);
+      lsb += padding_width;
+      msb += padding_width;
     }
 
-    if(op1 >= op0_width + op0_offset)
+    if(msb >= src_width + src_offset)
     {
-      auto padding_width = op1 - (op0_width + op0_offset) + 1;
+      auto padding_width = msb - (src_width + src_offset) + 1;
       auto padding = from_integer(
         0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
       auto new_type = unsignedbv_typet{
-        numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
-      expr.op0() = concatenation_exprt(padding, expr.op0(), new_type);
+        numeric_cast_v<std::size_t>(get_width(src.type()) + padding_width)};
+      src = concatenation_exprt(padding, src, new_type);
     }
 
     // Part-select expressions are unsigned, even if the
     // entire expression is selected!
     auto expr_type =
-      unsignedbv_typet{numeric_cast_v<std::size_t>(op1 - op2 + 1)};
+      unsignedbv_typet{numeric_cast_v<std::size_t>(msb - lsb + 1)};
 
-    op2 -= op0_offset;
-    op1 -= op0_offset;
+    lsb -= src_offset;
+    msb -= src_offset;
 
     // Construct the extractbits expression
     expr.id(ID_extractbits);
-    expr.op1() = from_integer(op1, integer_typet());
-    expr.op2() = from_integer(op2, integer_typet());
+    expr.op1() = from_integer(msb, integer_typet());
+    expr.op2() = from_integer(lsb, integer_typet());
     expr.type() = expr_type;
 
     return std::move(expr);
@@ -2389,62 +2390,63 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     expr.id() == ID_verilog_indexed_part_select_plus ||
     expr.id() == ID_verilog_indexed_part_select_minus)
   {
-    exprt &op0 = expr.op0();
-    convert_expr(op0);
+    auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(expr);
+    exprt &src = part_select.src();
+    convert_expr(src);
 
-    if(op0.type().id() == ID_array)
+    if(src.type().id() == ID_array)
     {
-      throw errort().with_location(op0.source_location())
+      throw errort().with_location(src.source_location())
         << "array type not allowed in part select";
     }
 
-    if(op0.type().id() == ID_verilog_real)
+    if(src.type().id() == ID_verilog_real)
     {
-      throw errort().with_location(op0.source_location())
+      throw errort().with_location(src.source_location())
         << "real not allowed in part select";
     }
 
-    mp_integer op0_width = get_width(op0.type());
-    mp_integer op0_offset = string2integer(op0.type().get_string(ID_C_offset));
+    mp_integer src_width = get_width(src.type());
+    mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));
 
     // The index need not be a constant.
-    exprt &op1 = expr.op1();
-    convert_expr(op1);
+    exprt &index = part_select.index();
+    convert_expr(index);
 
     // The width of the indexed part select must be an
     // elaboration-time constant.
-    mp_integer op2 = convert_integer_constant_expression(expr.op2());
+    mp_integer width = convert_integer_constant_expression(part_select.width());
 
     // The width must be positive. 1800-2017 11.5.1
-    if(op2 < 0)
+    if(width < 0)
     {
-      throw errort().with_location(expr.op2().source_location())
+      throw errort().with_location(part_select.width().source_location())
         << "width of indexed part select must be positive";
     }
 
     // Part-select expressions are unsigned, even if the
     // entire expression is selected!
-    auto expr_type = unsignedbv_typet{numeric_cast_v<std::size_t>(op2)};
+    auto expr_type = unsignedbv_typet{numeric_cast_v<std::size_t>(width)};
 
-    mp_integer op1_int;
-    if(is_constant_expression(op1, op1_int))
+    mp_integer index_int;
+    if(is_constant_expression(index, index_int))
     {
       // Construct the extractbits expression
       mp_integer bottom, top;
 
-      if(expr.id() == ID_verilog_indexed_part_select_plus)
+      if(part_select.id() == ID_verilog_indexed_part_select_plus)
       {
-        bottom = op1_int - op0_offset;
-        top = bottom + op2;
+        bottom = index_int - src_offset;
+        top = bottom + width;
       }
       else // ID_verilog_indexed_part_select_minus
       {
-        top = op1_int - op0_offset;
-        bottom = bottom - op2;
+        top = index_int - src_offset;
+        bottom = bottom - width;
       }
 
       return extractbits_exprt{
-        std::move(op0),
+        std::move(src),
         from_integer(top, integer_typet{}),
         from_integer(bottom, integer_typet{}),
         std::move(expr_type)}
@@ -2454,14 +2456,14 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     {
       // Index not constant.
       // Use logical right-shift followed by (constant) extractbits.
-      auto op1_adjusted =
-        minus_exprt{op1, from_integer(op0_offset, op1.type())};
+      auto index_adjusted =
+        minus_exprt{index, from_integer(src_offset, index.type())};
 
-      auto op0_shifted = lshr_exprt(op0, op1_adjusted);
+      auto src_shifted = lshr_exprt(src, index_adjusted);
 
       return extractbits_exprt{
-        std::move(op0_shifted),
-        from_integer(op2 - 1, integer_typet{}),
+        std::move(src_shifted),
+        from_integer(width - 1, integer_typet{}),
         from_integer(0, integer_typet{}),
         std::move(expr_type)}
         .with_source_location(expr);