Skip to content

Commit 3ea0b0d

Browse files
authored
Merge pull request #825 from diffblue/must_be_integral
Verilog: add checks for operators that require integral types
2 parents 423de3f + 820b050 commit 3ea0b0d

13 files changed

+128
-41
lines changed
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
KNOWNBUG
1+
CORE
22
concatenation5.v
33
--bound 0
4-
^EXIT=0$
4+
^file .* line 4: operand 1.1 must be integral$
5+
^EXIT=2$
56
^SIGNAL=0$
67
--
78
^warning: ignoring
89
--
9-
This should be errored.
Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
equality3.v
33
--bound 0
4-
^EXIT=0$
4+
^EXIT=2$
55
^SIGNAL=0$
66
--
77
^warning: ignoring
88
--
9-
This should be errored.
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
KNOWNBUG
1+
CORE
22
mod2.v
33
--bound 0
4-
^EXIT=0$
4+
^file .* line 4: operand 1\.1 must be integral$
5+
^EXIT=2$
56
^SIGNAL=0$
67
--
78
^warning: ignoring
89
--
9-
This should be errored.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
reduction2.v
3+
--bound 0
4+
^file .* line 4: operand 1\.1 must be integral$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module main;
2+
3+
// reduction operators only take integral types
4+
wire x = &1.1;
5+
6+
endmodule
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
replication3.v
3+
--bound 0
4+
^file .* line 3: operand 1\.1 must be integral$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module main;
2+
3+
wire [31:0] x = {4{1.1}};
4+
5+
endmodule
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
KNOWNBUG
1+
CORE
22
shr2.v
33
--bound 0
4-
^EXIT=0$
4+
^file .* line 4: operand 1\.1 must be integral$
5+
^EXIT=2$
56
^SIGNAL=0$
67
--
78
^warning: ignoring
89
--
9-
This should be errored.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
streaming_concatenation2.sv
3+
--bound 0
4+
^file .* line 4: operand 1\.1 must be integral$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module main;
2+
3+
// operand must be integral
4+
wire x = {<<{1.1}};
5+
6+
endmodule
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
KNOWNBUG
1+
CORE
22
wildcard_equality2.v
33
--bound 0
4-
^EXIT=0$
4+
^file .* line 4: operand 1\.1 must be integral$
5+
^EXIT=2$
56
^SIGNAL=0$
67
--
78
^warning: ignoring
89
--
9-
This should be errored.

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 69 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,37 @@ void verilog_typecheck_exprt::no_bool_ops(exprt &expr)
227227

228228
/*******************************************************************\
229229
230+
Function: verilog_typecheck_exprt::must_be_integral
231+
232+
Inputs:
233+
234+
Outputs:
235+
236+
Purpose:
237+
238+
\*******************************************************************/
239+
240+
void verilog_typecheck_exprt::must_be_integral(const exprt &expr)
241+
{
242+
// Throw an error if the given expression doesn't have an integral type.
243+
const auto &type = expr.type();
244+
if(type.id() == ID_bool)
245+
{
246+
// ok as is
247+
}
248+
else if(
249+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
250+
type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv)
251+
{
252+
// ok as is
253+
}
254+
else
255+
throw errort().with_location(expr.source_location())
256+
<< "operand " << to_string(expr) << " must be integral";
257+
}
258+
259+
/*******************************************************************\
260+
230261
Function: verilog_typecheck_exprt::convert_expr_rec
231262
232263
Inputs:
@@ -264,22 +295,14 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
264295
Forall_operands(it, expr)
265296
{
266297
convert_expr(*it);
267-
298+
must_be_integral(*it);
299+
268300
const typet &type=it->type();
269301

270-
if(type.id()==ID_array)
271-
{
272-
throw errort().with_location(it->source_location())
273-
<< "array type not allowed in concatenation";
274-
}
275-
else if(type.id() == ID_integer)
302+
if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
276303
{
277-
throw errort().with_location(it->source_location())
278-
<< "integer type not allowed in concatenation";
279-
}
280-
else if(type.id()==ID_verilog_signedbv ||
281-
type.id()==ID_verilog_unsignedbv)
282304
has_verilogbv=true;
305+
}
283306

284307
width+=get_width(*it);
285308
}
@@ -2642,10 +2665,13 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
26422665
{
26432666
// these may produce an 'x' if the operand is a verilog_bv
26442667
convert_expr(expr.op());
2668+
must_be_integral(expr.op());
26452669

26462670
if (expr.op().type().id() == ID_verilog_signedbv ||
26472671
expr.op().type().id() == ID_verilog_unsignedbv)
2672+
{
26482673
expr.type()=verilog_unsignedbv_typet(1);
2674+
}
26492675
else
26502676
expr.type()=bool_typet();
26512677
}
@@ -2678,6 +2704,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
26782704
// slice_size is defaulted to 1
26792705
PRECONDITION(expr.op().operands().size() == 1);
26802706
convert_expr(expr.op().operands()[0]);
2707+
must_be_integral(expr.op().operands()[0]);
26812708
expr.type() = expr.op().operands()[0].type();
26822709
return std::move(expr);
26832710
}
@@ -2819,12 +2846,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
28192846
exprt &op1=expr.op1();
28202847

28212848
convert_expr(op1);
2822-
2823-
if(op1.type().id()==ID_array)
2824-
{
2825-
throw errort().with_location(op1.source_location())
2826-
<< "array type not allowed in replication";
2827-
}
2849+
must_be_integral(op1);
28282850

28292851
if(op1.type().id()==ID_bool)
28302852
op1 = typecast_exprt{op1, unsignedbv_typet{1}};
@@ -3022,11 +3044,14 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
30223044
// a proper equality is performed.
30233045
expr.type()=bool_typet();
30243046

3025-
Forall_operands(it, expr)
3026-
convert_expr(*it);
3027-
3047+
convert_expr(expr.lhs());
3048+
convert_expr(expr.rhs());
30283049
typecheck_relation(expr);
30293050

3051+
// integral operands only
3052+
must_be_integral(expr.lhs());
3053+
must_be_integral(expr.rhs());
3054+
30303055
return std::move(expr);
30313056
}
30323057
else if(expr.id()==ID_lt || expr.id()==ID_gt ||
@@ -3051,8 +3076,10 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
30513076
// This is the >>> expression, which turns into ID_lshr or ID_ashr
30523077
// depending on type of first operand.
30533078

3054-
convert_expr(expr.op0());
3055-
convert_expr(expr.op1());
3079+
convert_expr(expr.lhs());
3080+
convert_expr(expr.rhs());
3081+
must_be_integral(expr.lhs());
3082+
must_be_integral(expr.rhs());
30563083
no_bool_ops(expr);
30573084

30583085
const typet &op0_type = expr.op0().type();
@@ -3076,14 +3103,16 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
30763103
else if(expr.id()==ID_lshr)
30773104
{
30783105
// logical right shift >>
3079-
convert_expr(expr.op0());
3080-
convert_expr(expr.op1());
3106+
convert_expr(expr.lhs());
3107+
convert_expr(expr.rhs());
3108+
must_be_integral(expr.lhs());
3109+
must_be_integral(expr.rhs());
30813110
no_bool_ops(expr);
30823111
expr.type()=expr.op0().type();
30833112

30843113
return std::move(expr);
30853114
}
3086-
else if(expr.id()==ID_div || expr.id()==ID_mod)
3115+
else if(expr.id() == ID_div)
30873116
{
30883117
Forall_operands(it, expr)
30893118
convert_expr(*it);
@@ -3095,6 +3124,20 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
30953124

30963125
return std::move(expr);
30973126
}
3127+
else if(expr.id() == ID_mod)
3128+
{
3129+
convert_expr(expr.lhs());
3130+
convert_expr(expr.rhs());
3131+
must_be_integral(expr.lhs());
3132+
must_be_integral(expr.rhs());
3133+
3134+
tc_binary_expr(expr);
3135+
no_bool_ops(expr);
3136+
3137+
expr.type() = expr.lhs().type();
3138+
3139+
return std::move(expr);
3140+
}
30983141
else if(expr.id()==ID_hierarchical_identifier)
30993142
{
31003143
return convert_hierarchical_identifier(

src/verilog/verilog_typecheck_expr.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -187,6 +187,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
187187
void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
188188
void typecheck_relation(binary_exprt &);
189189
void no_bool_ops(exprt &);
190+
void must_be_integral(const exprt &);
190191

191192
// SVA
192193
void convert_sva(exprt &expr)

0 commit comments

Comments
 (0)