Verilog: extract .lower() method for part select expressions

This moves the lowering for Verilog's part select expressions into an
explicit .lower() method.

src/verilog/verilog_expr.cpp

@@ -8,6 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "verilog_expr.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
 #include <util/prefix.h>
 
 #include "verilog_typecheck_base.h"
@@ -95,3 +99,53 @@ std::vector<irep_idt> verilog_module_sourcet::submodules() const
 
   return result;
 }
+
+exprt verilog_non_indexed_part_select_exprt::lower() const
+{
+  PRECONDITION(msb().is_constant());
+  PRECONDITION(lsb().is_constant());
+
+  auto op1 = numeric_cast_v<mp_integer>(to_constant_expr(msb()));
+  auto op2 = numeric_cast_v<mp_integer>(to_constant_expr(lsb()));
+
+  mp_integer this_width = to_bitvector_type(type()).get_width();
+  mp_integer this_offset = string2integer(type().get_string(ID_C_offset));
+
+  // 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.
+  exprt this_padded = *this;
+
+  if(op2 < this_offset)
+  {
+    // lsb too small, pad below
+    auto padding_width = this_offset - op2;
+    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>(
+      to_bitvector_type(this_padded.type()).get_width() + padding_width)};
+    this_padded = concatenation_exprt(this_padded, padding, new_type);
+    op2 += padding_width;
+    op1 += padding_width;
+  }
+
+  if(op1 >= this_width + this_offset)
+  {
+    // msb too large, pad above
+    auto padding_width = op1 - (this_width + this_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>(
+      to_bitvector_type(this_padded.type()).get_width() + padding_width)};
+    this_padded = concatenation_exprt(padding, this_padded, new_type);
+  }
+
+  op2 -= this_offset;
+  op1 -= this_offset;
+
+  // Construct the extractbits expression
+  return extractbits_exprt{
+    this_padded, from_integer(op2, integer_typet()), type()}
+    .with_source_location(source_location());
+}

src/verilog/verilog_expr.h

@@ -2203,6 +2203,9 @@ class verilog_non_indexed_part_select_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  /// lower to combination of concatenation and extractbits
+  exprt lower() const;
 };
 
 inline const verilog_non_indexed_part_select_exprt &

src/verilog/verilog_synthesis.cpp

@@ -345,53 +345,9 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
   else if(expr.id() == ID_verilog_non_indexed_part_select)
   {
     auto &part_select = to_verilog_non_indexed_part_select_expr(expr);
-    auto &src = part_select.src();
-
-    src = synth_expr(src, symbol_state);
-
-    auto op1 = numeric_cast_v<mp_integer>(to_constant_expr(part_select.msb()));
-    auto op2 = numeric_cast_v<mp_integer>(to_constant_expr(part_select.lsb()));
-
-    mp_integer src_width = get_width(src.type());
-    mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));
-
-    // 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.
-    exprt src_padded = src;
-
-    if(op2 < src_offset)
-    {
-      // lsb too small, pad below
-      auto padding_width = src_offset - op2;
-      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(src_padded.type()) + padding_width)};
-      src_padded = concatenation_exprt(src_padded, padding, new_type);
-      op2 += padding_width;
-      op1 += padding_width;
-    }
-
-    if(op1 >= src_width + src_offset)
-    {
-      // msb too large, pad above
-      auto padding_width = op1 - (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(src_padded.type()) + padding_width)};
-      src_padded = concatenation_exprt(padding, src_padded, new_type);
-    }
-
-    op2 -= src_offset;
-    op1 -= src_offset;
 
     // Construct the extractbits expression
-    return extractbits_exprt{
-      src_padded, from_integer(op2, integer_typet()), expr.type()}
-      .with_source_location(expr.source_location());
+    return part_select.lower();
   }
   else if(
     expr.id() == ID_verilog_indexed_part_select_plus ||