Merge pull request #1137 from diffblue/verilog-unsized

Verilog: mark unsized literals

Author: kroening

regression/verilog/case/case4.v

@@ -4,7 +4,7 @@ module m(input [7:0] i, output reg [31:0] x);
     casex(i)
       8'b1x: x=1;
       8'bxx: x=2;
-      { 'b11, 'bx, 'bx }: x=3;
+      { 2'b11, 1'bx, 1'bx }: x=3;
       default: x=4;
     endcase
 

regression/verilog/expressions/concatenation4.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 concatenation4.v
 
-^EXIT=0$
+^file .* line 5: unsized literals are not allowed in concatenations$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should yield an error.

regression/verilog/expressions/replication2.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 replication2.v
 
-^EXIT=0$
+^file .* line 6: unsized literals are not allowed in concatenations$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should yield an error.

src/hw_cbmc_irep_ids.h

@@ -243,6 +243,7 @@ IREP_ID_ONE(wire)
 IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
+IREP_ID_TWO(C_verilog_unsized, #verilog_unsized)
 IREP_ID_TWO(C_verilog_type, #verilog_type)
 IREP_ID_TWO(C_verilog_aval_bval, #verilog_aval_bval)
 IREP_ID_ONE(verilog_enum)

src/verilog/convert_literals.cpp

@@ -118,6 +118,20 @@ constant_exprt convert_real_literal(const irep_idt &value)
   return result;
 }
 
+static constant_exprt unsized(constant_exprt expr)
+{
+  expr.set(ID_C_verilog_unsized, true);
+  return expr;
+}
+
+static constant_exprt cond_unsized(constant_exprt expr, bool is_unsized)
+{
+  if(is_unsized)
+    return unsized(std::move(expr));
+  else
+    return expr;
+}
+
 constant_exprt convert_integral_literal(const irep_idt &value)
 {
   // first, get rid of whitespace and underscores
@@ -135,19 +149,19 @@ constant_exprt convert_integral_literal(const irep_idt &value)
   // special case the "unbased unsized literals"
   if(rest == "'0")
   {
-    return from_integer(0, unsignedbv_typet{1});
+    return unsized(from_integer(0, unsignedbv_typet{1}));
   }
   else if(rest == "'1")
   {
-    return from_integer(1, unsignedbv_typet{1});
+    return unsized(from_integer(1, unsignedbv_typet{1}));
   }
   else if(rest == "'x" || rest == "'X")
   {
-    return constant_exprt{"x", verilog_unsignedbv_typet{1}};
+    return unsized(constant_exprt{"x", verilog_unsignedbv_typet{1}});
   }
   else if(rest == "'z" || rest == "'Z")
   {
-    return constant_exprt{"z", verilog_unsignedbv_typet{1}};
+    return unsized(constant_exprt{"z", verilog_unsignedbv_typet{1}});
   }
 
   std::string::size_type pos = rest.find('\'');
@@ -183,15 +197,17 @@ constant_exprt convert_integral_literal(const irep_idt &value)
     auto type = s_flag_given
                   ? static_cast<typet>(verilog_signedbv_typet{final_bits})
                   : verilog_unsignedbv_typet{final_bits};
-    return constant_exprt{std::string(final_bits, 'x'), type};
+    return cond_unsized(
+      constant_exprt{std::string(final_bits, 'x'), type}, !bits_given);
   }
   else if(rest == "dz" || rest == "dZ")
   {
     std::size_t final_bits = bits_given ? bits : 32;
     auto type = s_flag_given
                   ? static_cast<typet>(verilog_signedbv_typet{final_bits})
                   : verilog_unsignedbv_typet{final_bits};
-    return constant_exprt{std::string(final_bits, 'z'), type};
+    return cond_unsized(
+      constant_exprt{std::string(final_bits, 'z'), type}, !bits_given);
   }
 
   unsigned base = 10;
@@ -353,7 +369,7 @@ constant_exprt convert_integral_literal(const irep_idt &value)
         type = verilog_unsignedbv_typet(bits);
 
       // stored as individual bits
-      return constant_exprt{fvalue, type};
+      return cond_unsized(constant_exprt{fvalue, type}, !bits_given);
     }
     else // two valued
     {
@@ -372,7 +388,8 @@ constant_exprt convert_integral_literal(const irep_idt &value)
         type = unsignedbv_typet(bits);
 
       // stored as bvrep
-      return constant_exprt{integer2bvrep(int_value, bits), type};
+      return cond_unsized(
+        constant_exprt{integer2bvrep(int_value, bits), type}, !bits_given);
     }
   }
   else
@@ -395,7 +412,8 @@ constant_exprt convert_integral_literal(const irep_idt &value)
     else
       type = unsignedbv_typet(bits);
 
-    return constant_exprt{integer2bvrep(int_value, bits), type};
+    return cond_unsized(
+      constant_exprt{integer2bvrep(int_value, bits), type}, !bits_given);
   }
 
   UNREACHABLE;

src/verilog/verilog_typecheck_expr.cpp

@@ -286,6 +286,14 @@ exprt verilog_typecheck_exprt::convert_expr_concatenation(
   Forall_operands(it, expr)
   {
     convert_expr(*it);
+
+    // check if there's an unsized literal (1800-2017 11.4.12)
+    if(it->get_bool(ID_C_verilog_unsized))
+    {
+      throw errort().with_location(it->source_location())
+        << "unsized literals are not allowed in concatenations";
+    }
+
     must_be_integral(*it);
 
     const typet &type = it->type();