Merge pull request #1357 from diffblue/verilog3

netlist: fix further `extractbits` off-by-one errors

Author: tautschnig

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 5.8
 
+* AIG/netlist engine: fix for conversion of extract bits operator
 * Verilog: semantic fix for output register ports
 * SystemVerilog: cover sequence
 * SystemVerilog: labeled immediate assert/assume/cover statements

regression/ebmc/smv-netlist/verilog3.desc

@@ -0,0 +1,5 @@
+CORE
+verilog3.sv
+--smv-netlist
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/smv-netlist/verilog3.sv

@@ -0,0 +1,5 @@
+module main;
+  wire [7:0] some_wire;
+  wire [31:0] something_else;
+  assign something_else = some_wire[7:1];
+endmodule

src/trans-netlist/trans_to_netlist.cpp

@@ -594,7 +594,10 @@ void convert_trans_to_netlistt::convert_lhs_rec(
     if(!to_integer_non_constant(to_extractbits_expr(expr).index(), new_from))
     {
       boolbv_widtht boolbv_width(ns);
-      mp_integer new_to = new_from + boolbv_width(expr.type());
+      const auto width = boolbv_width(expr.type());
+      DATA_INVARIANT(
+        width != 0, "trans_to_netlist got extractbits with zero-width operand");
+      mp_integer new_to = new_from + width - 1;
 
       from = new_from.to_ulong();
       to = new_to.to_ulong();