Merge pull request #581 from diffblue/array_functions1

Verilog: `$low`, `$high`, `$increment`, `$left`, `$right`

regression/verilog/system-functions/array_functions1.desc

@@ -0,0 +1,22 @@
+CORE
+array_functions1.sv
+--module main --bound 0
+^\[main\.pP0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
+^\[main\.pP1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
+^\[main\.pP2\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
+^\[main\.pP3\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
+^\[main\.pP4\] always 1 == 1: PROVED up to bound 0$
+^\[main\.pP5\] always -1 == -1: PROVED up to bound 0$
+^\[main\.pU0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
+^\[main\.pU1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
+^\[main\.pU2\] always 31 == 31 && 0 == 0: PROVED up to bound 0$
+^\[main\.pU3\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
+^\[main\.pU4\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
+^\[main\.pU5\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
+^\[main\.pU6\] always 1 == 1: PROVED up to bound 0$
+^\[main\.pU7\] always -1 == -1: PROVED up to bound 0$
+^\[main\.pU8\] always 1 == 1: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/array_functions1.sv

@@ -0,0 +1,27 @@
+module main;
+
+  wire [32:1] packed1;
+  wire [0:31] packed2;
+
+  wire unpacked1 [32:1];
+  wire unpacked2 [0:31];
+  wire unpacked3 [32];
+
+  pP0: assert property ($left(packed1) == 32 and $right(packed1) == 1);
+  pP1: assert property ($left(packed2) == 0 and $right(packed2) == 31);
+  pP2: assert property ($low(packed1) == 1 and $high(packed1) == 32);
+  pP3: assert property ($low(packed2) == 0 and $high(packed2) == 31);
+  pP4: assert property ($increment(packed1) == 1);
+  pP5: assert property ($increment(packed2) == -1);
+
+  pU0: assert property ($left(unpacked1) == 32 and $right(unpacked1) == 1);
+  pU1: assert property ($left(unpacked2) == 0 and $right(unpacked2) == 31);
+  pU2: assert property ($left(unpacked3) == 31 and $right(unpacked3) == 0);
+  pU3: assert property ($low(unpacked1) == 1 and $high(unpacked1) == 32);
+  pU4: assert property ($low(unpacked2) == 0 and $high(unpacked2) == 31);
+  pU5: assert property ($low(unpacked3) == 0 and $high(unpacked3) == 31);
+  pU6: assert property ($increment(unpacked1) == 1);
+  pU7: assert property ($increment(unpacked2) == -1);
+  pU8: assert property ($increment(unpacked3) == 1);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -447,6 +447,179 @@ exprt verilog_typecheck_exprt::bits(const exprt &expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::left
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::left(const exprt &expr)
+{
+  // unpacked array: left bound
+  // packed array: index of most significant element
+  // 0 otherwise
+  auto left = [](const typet &type) -> mp_integer {
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
+      type.id() == ID_bool)
+    {
+      auto offset = type.get_int(ID_C_offset);
+      if(type.get_bool(ID_C_little_endian))
+        return offset + get_width(type) - 1;
+      else
+        return offset;
+    }
+    else if(type.id() == ID_array)
+    {
+      auto offset = numeric_cast_v<mp_integer>(
+        to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
+      if(type.get_bool(ID_C_little_endian))
+        return offset +
+               numeric_cast_v<mp_integer>(
+                 to_constant_expr(to_array_type(type).size())) -
+               1;
+      else
+        return offset;
+    }
+    else
+      return 0;
+  };
+
+  return from_integer(left(expr.type()), integer_typet{});
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::right
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
+{
+  // unpacked array: right bound
+  // packed array: index of least significant element
+  // 0 otherwise
+  auto right = [](const typet &type) -> mp_integer {
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
+      type.id() == ID_bool)
+    {
+      auto offset = type.get_int(ID_C_offset);
+      if(type.get_bool(ID_C_little_endian))
+        return offset;
+      else
+        return offset + get_width(type) - 1;
+    }
+    else if(type.id() == ID_array)
+    {
+      auto offset = numeric_cast_v<mp_integer>(
+        to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
+      if(type.get_bool(ID_C_little_endian))
+        return offset;
+      else
+        return offset +
+               numeric_cast_v<mp_integer>(
+                 to_constant_expr(to_array_type(type).size())) -
+               1;
+    }
+    else
+      return 0;
+  };
+
+  return from_integer(right(expr.type()), integer_typet{});
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::increment
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::increment(const exprt &expr)
+{
+  // fixed-size dimension: 1 if $left >= $right, -1 otherwise
+  auto increment = [](const typet &type) -> mp_integer {
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
+      type.id() == ID_array)
+    {
+      if(type.get_bool(ID_C_little_endian))
+        return 1;
+      else
+        return -1;
+    }
+    else
+      return -1;
+  };
+
+  return from_integer(increment(expr.type()), integer_typet{});
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::low
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::low(const exprt &expr)
+{
+  // $left if $increment returns –1
+  // $right otherwise
+  if(numeric_cast_v<mp_integer>(increment(expr)) == -1)
+    return left(expr);
+  else
+    return right(expr);
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::high
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::high(const exprt &expr)
+{
+  // $right if $increment returns –1
+  // $left otherwise
+  if(numeric_cast_v<mp_integer>(increment(expr)) == -1)
+    return right(expr);
+  else
+    return left(expr);
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::convert_system_function
 
   Inputs:
@@ -549,12 +722,14 @@ exprt verilog_typecheck_exprt::convert_system_function(
     expr.type() = arguments.front().type();
     return std::move(expr);
   }
-  else if(identifier == "$bits")
+  else if(
+    identifier == "$bits" || identifier == "$left" || identifier == "$right" ||
+    identifier == "$increment" || identifier == "$low" || identifier == "$high")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << "$bits takes one argument";
+        << identifier << " takes one argument";
     }
 
     // The return type is integer.
@@ -1370,6 +1545,31 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call(
     DATA_INVARIANT(arguments.size() == 1, "$bits has one argument");
     return bits(arguments[0]);
   }
+  else if(identifier == "$low")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$low has one argument");
+    return low(arguments[0]);
+  }
+  else if(identifier == "$high")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$high has one argument");
+    return high(arguments[0]);
+  }
+  else if(identifier == "$left")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$left has one argument");
+    return left(arguments[0]);
+  }
+  else if(identifier == "$right")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$right has one argument");
+    return right(arguments[0]);
+  }
+  else if(identifier == "$increment")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$increment has one argument");
+    return increment(arguments[0]);
+  }
   else if(identifier == "$clog2")
   {
     // the ceiling of the log with base 2 of the argument

src/verilog/verilog_typecheck_expr.h

@@ -133,8 +133,14 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
   void no_bool_ops(exprt &);
 
+  // system functions
   exprt bits(const exprt &);
   std::optional<mp_integer> bits_rec(const typet &) const;
+  constant_exprt left(const exprt &);
+  constant_exprt right(const exprt &);
+  constant_exprt low(const exprt &);
+  constant_exprt high(const exprt &);
+  constant_exprt increment(const exprt &);
 };
 
 bool verilog_typecheck(