Verilog: add checks for operators that require integral types

This adds checks to the typechecker to enforce that the operands have an
integral type.

Author: kroening

regression/verilog/expressions/concatenation5.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 concatenation5.v
 --bound 0
-^EXIT=0$
+^file .* line 4: operand 1.1 must be integral$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be errored.

regression/verilog/expressions/equality3.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 equality3.v
 --bound 0
-^EXIT=0$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be errored.

regression/verilog/expressions/mod2.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 mod2.v
 --bound 0
-^EXIT=0$
+^file .* line 4: operand 1\.1 must be integral$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be errored.

regression/verilog/expressions/reduction2.desc

@@ -0,0 +1,9 @@
+CORE
+reduction2.v
+--bound 0
+^file .* line 4: operand 1\.1 must be integral$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/reduction2.v

@@ -0,0 +1,6 @@
+module main;
+
+  // reduction operators only take integral types
+  wire x = &1.1;
+
+endmodule

regression/verilog/expressions/replication3.desc

@@ -0,0 +1,9 @@
+CORE
+replication3.v
+--bound 0
+^file .* line 3: operand 1\.1 must be integral$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/replication3.v

@@ -0,0 +1,5 @@
+module main;
+
+  wire [31:0] x = {4{1.1}};
+
+endmodule

regression/verilog/expressions/shr2.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 shr2.v
 --bound 0
-^EXIT=0$
+^file .* line 4: operand 1\.1 must be integral$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be errored.

regression/verilog/expressions/streaming_concatenation2.desc

@@ -0,0 +1,9 @@
+CORE
+streaming_concatenation2.sv
+--bound 0
+^file .* line 4: operand 1\.1 must be integral$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/streaming_concatenation2.sv

@@ -0,0 +1,6 @@
+module main;
+
+  // operand must be integral
+  wire x = {<<{1.1}};
+
+endmodule

regression/verilog/expressions/wildcard_equality2.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 wildcard_equality2.v
 --bound 0
-^EXIT=0$
+^file .* line 4: operand 1\.1 must be integral$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be errored.

src/verilog/verilog_typecheck_expr.cpp

@@ -226,6 +226,37 @@ void verilog_typecheck_exprt::no_bool_ops(exprt &expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::must_be_integral
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheck_exprt::must_be_integral(const exprt &expr)
+{
+  // Throw an error if the given expression doesn't have an integral type.
+  const auto &type = expr.type();
+  if(type.id() == ID_bool)
+  {
+    // ok as is
+  }
+  else if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv)
+  {
+    // ok as is
+  }
+  else
+    throw errort().with_location(expr.source_location())
+      << "operand " << to_string(expr) << " must be integral";
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::convert_expr_rec
 
   Inputs:
@@ -263,22 +294,14 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
     Forall_operands(it, expr)
     {
       convert_expr(*it);
-      
+      must_be_integral(*it);
+
       const typet &type=it->type();
 
-      if(type.id()==ID_array)
-      {
-        throw errort().with_location(it->source_location())
-          << "array type not allowed in concatenation";
-      }
-      else if(type.id() == ID_integer)
+      if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
       {
-        throw errort().with_location(it->source_location())
-          << "integer type not allowed in concatenation";
-      }
-      else if(type.id()==ID_verilog_signedbv ||
-              type.id()==ID_verilog_unsignedbv)
         has_verilogbv=true;
+      }
 
       width+=get_width(*it);
     }
@@ -2640,10 +2663,13 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   {
     // these may produce an 'x' if the operand is a verilog_bv
     convert_expr(expr.op());
+    must_be_integral(expr.op());
 
     if (expr.op().type().id() == ID_verilog_signedbv ||
         expr.op().type().id() == ID_verilog_unsignedbv)
+    {
       expr.type()=verilog_unsignedbv_typet(1);
+    }
     else
       expr.type()=bool_typet();
   }
@@ -2676,6 +2702,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     // slice_size is defaulted to 1
     PRECONDITION(expr.op().operands().size() == 1);
     convert_expr(expr.op().operands()[0]);
+    must_be_integral(expr.op().operands()[0]);
     expr.type() = expr.op().operands()[0].type();
     return std::move(expr);
   }
@@ -2817,12 +2844,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
   exprt &op1=expr.op1();
 
   convert_expr(op1);
-
-  if(op1.type().id()==ID_array)
-  {
-    throw errort().with_location(op1.source_location())
-      << "array type not allowed in replication";
-  }
+  must_be_integral(op1);
 
   if(op1.type().id()==ID_bool)
     op1 = typecast_exprt{op1, unsignedbv_typet{1}};
@@ -3020,11 +3042,14 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     // a proper equality is performed.
     expr.type()=bool_typet();
 
-    Forall_operands(it, expr)
-      convert_expr(*it);
-
+    convert_expr(expr.lhs());
+    convert_expr(expr.rhs());
     typecheck_relation(expr);
 
+    // integral operands only
+    must_be_integral(expr.lhs());
+    must_be_integral(expr.rhs());
+
     return std::move(expr);
   }
   else if(expr.id()==ID_lt || expr.id()==ID_gt ||
@@ -3049,8 +3074,10 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     // This is the >>> expression, which turns into ID_lshr or ID_ashr
     // depending on type of first operand.
 
-    convert_expr(expr.op0());
-    convert_expr(expr.op1());
+    convert_expr(expr.lhs());
+    convert_expr(expr.rhs());
+    must_be_integral(expr.lhs());
+    must_be_integral(expr.rhs());
     no_bool_ops(expr);
 
     const typet &op0_type = expr.op0().type();
@@ -3074,14 +3101,16 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(expr.id()==ID_lshr)
   {
     // logical right shift >>
-    convert_expr(expr.op0());
-    convert_expr(expr.op1());
+    convert_expr(expr.lhs());
+    convert_expr(expr.rhs());
+    must_be_integral(expr.lhs());
+    must_be_integral(expr.rhs());
     no_bool_ops(expr);
     expr.type()=expr.op0().type();
 
     return std::move(expr);
   }
-  else if(expr.id()==ID_div || expr.id()==ID_mod)
+  else if(expr.id() == ID_div)
   {
     Forall_operands(it, expr)
       convert_expr(*it);
@@ -3093,6 +3122,20 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_mod)
+  {
+    convert_expr(expr.lhs());
+    convert_expr(expr.rhs());
+    must_be_integral(expr.lhs());
+    must_be_integral(expr.rhs());
+
+    tc_binary_expr(expr);
+    no_bool_ops(expr);
+
+    expr.type() = expr.lhs().type();
+
+    return std::move(expr);
+  }
   else if(expr.id()==ID_hierarchical_identifier)
   {
     return convert_hierarchical_identifier(

src/verilog/verilog_typecheck_expr.h

@@ -187,6 +187,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
   void typecheck_relation(binary_exprt &);
   void no_bool_ops(exprt &);
+  void must_be_integral(const exprt &);
 
   // SVA
   void convert_sva(exprt &expr)