Merge pull request #582 from diffblue/bit-extract5

Verilog: fix for index on packed arrays that are lsb first

Author: tautschnig

regression/verilog/expressions/bit-extract5.desc

@@ -0,0 +1,11 @@
+CORE
+bit-extract5.sv
+--module main --bound 0
+^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED up to bound 0$
+^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED up to bound 0$
+^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED up to bound 0$
+^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bit-extract5.sv

@@ -0,0 +1,13 @@
+module main;
+
+  wire [31:0] w1 = 'b1;
+  wire [32:1] w2 = 'b1;
+  wire [0:31] w3 = 'b1;
+  wire [1:32] w4 = 'b1;
+
+  p0: assert property (w1[0] and !w1[31]);
+  p1: assert property (w2[1] and !w2[32]);
+  p2: assert property (w3[31] and !w3[0]);
+  p3: assert property (w4[32] and !w4[1]);
+
+endmodule

regression/verilog/expressions/bit-extract6.desc

@@ -0,0 +1,9 @@
+CORE
+bit-extract6.sv
+--module main --bound 0
+^\[main\.p0\] always \(main\.index == 8 |-> main\.vector\[7 - main\.index - 1\] == 1\): PROVED up to bound 0$
+^\[main\.p1\] always \(main\.index >= 1 \&\& main\.index <= 7 |-> main\.vector\[7 - main\.index - 1\] == 0\): PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bit-extract6.sv

@@ -0,0 +1,13 @@
+module main;
+
+  wire [1:8] vector = 1;
+  wire [7:0] index;
+
+  // Non-constant index.
+  // Note that index 8 is the least significant bit.
+  p0: assert property (index == 8 |-> vector[index] == 1);
+
+  // Verilog guarantees that any out-of-bounds access is zero.
+  p1: assert property (index >= 1 && index <= 7 |-> vector[index] == 0);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -1635,26 +1635,46 @@ bool verilog_typecheck_exprt::is_constant_expression(
   exprt tmp(expr);
 
   convert_expr(tmp);
-  ns.follow_macros(tmp);
-
-  simplify(tmp, ns);
 
-  if(tmp.is_true())
-  {
-    value=1;
-    return true;
-  }
-  else if(tmp.is_false())
-  {
-    value=0;
-    return true;
-  }
-  else if(!to_integer_non_constant(tmp, value))
+  auto integer_opt = is_constant_integer_post_convert(tmp);
+  if(integer_opt.has_value())
   {
+    value = integer_opt.value();
     return true;
   }
+  else
+    return false;
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::is_constant_integer_post_convert
+
+  Inputs:
 
-  return false;
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::optional<mp_integer>
+verilog_typecheck_exprt::is_constant_integer_post_convert(const exprt &expr)
+{
+  exprt tmp = expr;
+
+  ns.follow_macros(tmp);
+  tmp = simplify_expr(tmp, ns);
+
+  if(!tmp.is_constant())
+    return {};
+
+  if(tmp.is_true())
+    return 1;
+  else if(tmp.is_false())
+    return 0;
+  else
+    return numeric_cast<mp_integer>(to_constant_expr(tmp));
 }
 
 /*******************************************************************\
@@ -2189,65 +2209,65 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
   // Verilog's bit select expression may map onto an extractbit
   // or an array index expression, depending on the type of the first
   // operand.
-  exprt &op0 = expr.op0();
+  exprt &op0 = expr.op0(), &op1 = expr.op1();
   convert_expr(op0);
+  convert_expr(op1);
 
   if(op0.type().id() == ID_verilog_real)
   {
     throw errort().with_location(op0.source_location())
       << "bit-select of real is not allowed";
   }
 
-  if(op0.type().id()==ID_array)
+  if(op1.type().id() == ID_verilog_real)
   {
-    exprt &op1 = expr.op1();
-    convert_expr(op1);
-    if(op1.type().id() == ID_verilog_real)
-    {
-      throw errort().with_location(op1.source_location())
-        << "real number index is not allowed";
-    }
+    throw errort().with_location(op1.source_location())
+      << "real number index is not allowed";
+  }
 
+  if(op0.type().id() == ID_array)
+  {
     typet _index_type = index_type(to_array_type(op0.type()));
-
-    if(_index_type!=op1.type())
-    {
-      mp_integer i;
-      if(!to_integer_non_constant(op1, i))
-        op1=from_integer(i, _index_type);
-      else if(op1.is_true() || op1.is_false())
-        op1=from_integer(op1.is_true()?1:0, _index_type);
-      else
-        op1 = typecast_exprt{op1, _index_type};
-    }
+    op1 = typecast_exprt{op1, _index_type};
 
     expr.type() = to_array_type(op0.type()).element_type();
     expr.id(ID_index);
   }
   else
   {
     auto width = get_width(op0.type());
-    auto offset = atoi(op0.type().get(ID_C_offset).c_str());
+    auto offset = op0.type().get_int(ID_C_offset);
 
-    mp_integer op1;
+    auto op1_opt = is_constant_integer_post_convert(op1);
 
-    if(is_constant_expression(expr.op1(), op1))
+    if(op1_opt.has_value()) // constant index
     {
       // 1800-2017 sec 11.5.1: out-of-bounds bit-select is
       // x for 4-state and 0 for 2-state values.
-      if(op1 < offset || op1 >= width + offset)
+      auto op1_int = op1_opt.value();
+
+      if(op1_int < offset || op1_int >= width + offset)
         return false_exprt().with_source_location(expr);
 
-      op1 -= offset;
-      expr.op1() = from_integer(op1, natural_typet());
+      op1_int -= offset;
+
+      if(op0.type().get_bool(ID_C_big_endian))
+        op1_int = width - op1_int - 1;
+
+      expr.op1() = from_integer(op1_int, natural_typet());
     }
-    else
+    else // non-constant index
     {
-      convert_expr(expr.op1());
-      if(expr.op1().type().id() == ID_verilog_real)
+      if(offset != 0)
+      {
+        expr.op1() =
+          minus_exprt{expr.op1(), from_integer(offset, expr.op1().type())};
+      }
+
+      if(op0.type().get_bool(ID_C_big_endian))
       {
-        throw errort().with_location(expr.op1().source_location())
-          << "real number index is not allowed";
+        expr.op1() =
+          minus_exprt{from_integer(width - 1, expr.op1().type()), expr.op1()};
       }
     }
 

src/verilog/verilog_typecheck_expr.h

@@ -104,6 +104,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   // elaboration (expansion and folding) of constant expressions and functions
   bool is_constant_expression(const exprt &, mp_integer &value);
+  std::optional<mp_integer> is_constant_integer_post_convert(const exprt &);
   exprt elaborate_constant_expression(exprt);
 
   // To be overridden, requires a Verilog interpreter.