Verilog: fix for signed constants

Verilog allows constants to be marked as signed (e.g., 'sb1).  When using
base 2, 8 and 16, these need to be sign extended to 32 bits unless the
number of bits is given.

Author: kroening

regression/verilog/expressions/equality1.desc

@@ -5,10 +5,10 @@ equality1.v
 ^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
 ^\[.*\] always 10 != 20 === 1: PROVED up to bound 0$
 ^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
-^\[.*\] always 1'bx == 10 === 1'bx: PROVED up to bound 0$
-^\[.*\] always 1'bz == 20 === 1'bx: PROVED up to bound 0$
-^\[.*\] always 1'bx != 10 === 1'bx: PROVED up to bound 0$
-^\[.*\] always 1'bz != 20 === 1'bx: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
 ^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$
 ^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED up to bound 0$
 ^EXIT=10$

regression/verilog/expressions/equality2.desc

@@ -5,11 +5,11 @@ equality2.v
 ^\[.*\] always 10 === 20 == 0: PROVED up to bound 0$
 ^\[.*\] always 10 !== 10 == 0: PROVED up to bound 0$
 ^\[.*\] always 10 !== 20 == 1: PROVED up to bound 0$
-^\[.*\] always 1'bx === 1'bx == 1: PROVED up to bound 0$
-^\[.*\] always 1'bz === 1'bz == 1: PROVED up to bound 0$
-^\[.*\] always 1'bx === 1'bz == 0: PROVED up to bound 0$
-^\[.*\] always 1'bx === 1 == 0: PROVED up to bound 0$
-^\[.*\] always 1'bz === 1 == 0: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED up to bound 0$
+^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED up to bound 0$
 ^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$
 ^\[.*\] always 3'b011 === 3'b111 == 1: REFUTED$
 ^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED up to bound 0$

regression/verilog/expressions/signed2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 signed2.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The signed base 2 literal should be sign-extended.

regression/verilog/expressions/signed2.sv

@@ -1,7 +1,30 @@
 module main;
 
-  p0: assert final ('sb1 == -1);
-  p1: assert final ('sb11 == -1);
-  p2: assert final (4'sb111 == 7);
+  // base 2
+  pA0: assert final ('sb1 == -1);
+  pA1: assert final ('sb01 == 1);
+  pA2: assert final ('sb1x === 'sb1111111111111111111111111111111x);
+  pA3: assert final ($bits('sb1) == 32);
+  pA4: assert final ('sb11 == -1);
+  pA5: assert final (4'sb111 == 7);
+  pA6: assert final ($bits(4'sb111) == 4);
+
+  // base 8
+  pB0: assert final ('so7 == -1);
+  pB1: assert final ('so1 == 1);
+  pB2: assert final ('so7x === 'so3777777777x);
+  pB3: assert final ($bits('so1) == 32);
+  pB4: assert final ('so77 == -1);
+  pB5: assert final (4'so7 == 7);
+  pB6: assert final ($bits(4'so7) == 4);
+
+  // base 16
+  pC0: assert final ('shf == -1);
+  pC1: assert final ('sh1 == 1);
+  pC2: assert final ('shfx === 'shfffffffx);
+  pC3: assert final ($bits('sh1) == 32);
+  pC4: assert final ('shff == -1);
+  pC5: assert final (8'shf == 15);
+  pC6: assert final ($bits(8'shf) == 8);
 
 endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
+#include <util/string2int.h>
 
 #include "expr2verilog.h"
 #include "sva_expr.h"
@@ -1223,14 +1224,14 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
   // check representation
 
   std::string::size_type pos=rest.find('\'');
-  unsigned bits=0;
+  std::size_t bits = 0;
   bool bits_given=false;
 
   if(pos!=std::string::npos) // size given?
   {
     if(rest[0]!='\'')
     {
-      bits=atoi(rest.c_str());
+      bits = safe_string2size_t(rest);
       bits_given=true;
 
       if(bits==0)
@@ -1273,14 +1274,13 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
   bool is_signed=!based || s_flag_given;
 
   // check for z/x
-
-  bool other=false;
+  bool four_valued = false;
 
   for(unsigned i=0; i<rest.size(); i++)
     if(rest[i]=='?' || rest[i]=='z' || rest[i]=='x')
-      other=true;
+      four_valued = true;
 
-  if(other) // z/x/? found
+  if(base != 10)
   {
     // expand bits
 
@@ -1370,17 +1370,51 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
       bits=fvalue.size();
     }
 
-    if(is_signed)
-      expr.type()=verilog_signedbv_typet(bits);
-    else
-      expr.type()=verilog_unsignedbv_typet(bits);
+    if(four_valued)
+    {
+      // we do a 32-bit minimum if the number of bits isn't given
+      if(!bits_given)
+      {
+        if(bits < 32)
+        {
+          // do sign extension
+          char extension = is_signed ? fvalue.front() : '0';
+          fvalue = std::string(32 - bits, extension) + fvalue;
+          bits = 32;
+        }
+      }
+
+      if(is_signed)
+        expr.type() = verilog_signedbv_typet(bits);
+      else
+        expr.type() = verilog_unsignedbv_typet(bits);
 
-    expr.set(ID_value, fvalue);
+      // stored as individual bits
+      expr.set_value(fvalue);
+    }
+    else // two valued
+    {
+      mp_integer int_value = binary2integer(fvalue, is_signed);
+
+      // we do a 32-bit minimum if the number of bits isn't given
+      if(!bits_given)
+        if(bits < 32)
+          bits = 32;
+
+      if(is_signed)
+        expr.type() = signedbv_typet(bits);
+      else
+        expr.type() = unsignedbv_typet(bits);
+
+      // stored as bvrep
+      expr.set_value(integer2bvrep(int_value, bits));
+    }
   }
   else
   {
+    // base 10, never negative
     mp_integer int_value=string2integer(rest, base);
-    
+
     if(!bits_given)
     {
       bits = address_bits(int_value + 1);
@@ -1393,7 +1427,7 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
     else
       expr.type()=unsignedbv_typet(bits);
 
-    expr.set(ID_value, integer2bvrep(int_value, bits));
+    expr.set_value(integer2bvrep(int_value, bits));
   }
 
   return std::move(expr);