introduce verilog_non_indexed_part_select_exprt

This introduces the class verilog_non_indexed_part_select_exprt, which
documents an expression generated by the Verilog parser.

Author: kroening

src/verilog/verilog_expr.h

@@ -1989,4 +1989,68 @@ 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);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -2350,70 +2350,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);