From 820b050d8a721c6408e3b8cdad73c00b3c5799f2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 17 Nov 2024 09:35:54 +0000 Subject: [PATCH] Verilog: add checks for operators that require integral types This adds checks to the typechecker to enforce that the operands have an integral type. --- .../verilog/expressions/concatenation5.desc | 6 +- regression/verilog/expressions/equality3.desc | 5 +- regression/verilog/expressions/mod2.desc | 6 +- .../verilog/expressions/reduction2.desc | 9 ++ regression/verilog/expressions/reduction2.v | 6 ++ .../verilog/expressions/replication3.desc | 9 ++ regression/verilog/expressions/replication3.v | 5 + regression/verilog/expressions/shr2.desc | 6 +- .../expressions/streaming_concatenation2.desc | 9 ++ .../expressions/streaming_concatenation2.sv | 6 ++ .../expressions/wildcard_equality2.desc | 6 +- src/verilog/verilog_typecheck_expr.cpp | 95 ++++++++++++++----- src/verilog/verilog_typecheck_expr.h | 1 + 13 files changed, 128 insertions(+), 41 deletions(-) create mode 100644 regression/verilog/expressions/reduction2.desc create mode 100644 regression/verilog/expressions/reduction2.v create mode 100644 regression/verilog/expressions/replication3.desc create mode 100644 regression/verilog/expressions/replication3.v create mode 100644 regression/verilog/expressions/streaming_concatenation2.desc create mode 100644 regression/verilog/expressions/streaming_concatenation2.sv diff --git a/regression/verilog/expressions/concatenation5.desc b/regression/verilog/expressions/concatenation5.desc index 615d8ef7c..ec1e4ef33 100644 --- a/regression/verilog/expressions/concatenation5.desc +++ b/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. diff --git a/regression/verilog/expressions/equality3.desc b/regression/verilog/expressions/equality3.desc index f294b3095..e73073616 100644 --- a/regression/verilog/expressions/equality3.desc +++ b/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. diff --git a/regression/verilog/expressions/mod2.desc b/regression/verilog/expressions/mod2.desc index 8652378a8..87d22d748 100644 --- a/regression/verilog/expressions/mod2.desc +++ b/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. diff --git a/regression/verilog/expressions/reduction2.desc b/regression/verilog/expressions/reduction2.desc new file mode 100644 index 000000000..46a884dd3 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/expressions/reduction2.v b/regression/verilog/expressions/reduction2.v new file mode 100644 index 000000000..d605abde9 --- /dev/null +++ b/regression/verilog/expressions/reduction2.v @@ -0,0 +1,6 @@ +module main; + + // reduction operators only take integral types + wire x = &1.1; + +endmodule diff --git a/regression/verilog/expressions/replication3.desc b/regression/verilog/expressions/replication3.desc new file mode 100644 index 000000000..73c59cd20 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/expressions/replication3.v b/regression/verilog/expressions/replication3.v new file mode 100644 index 000000000..fa4b21883 --- /dev/null +++ b/regression/verilog/expressions/replication3.v @@ -0,0 +1,5 @@ +module main; + + wire [31:0] x = {4{1.1}}; + +endmodule diff --git a/regression/verilog/expressions/shr2.desc b/regression/verilog/expressions/shr2.desc index 300ce7612..a83a5c432 100644 --- a/regression/verilog/expressions/shr2.desc +++ b/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. diff --git a/regression/verilog/expressions/streaming_concatenation2.desc b/regression/verilog/expressions/streaming_concatenation2.desc new file mode 100644 index 000000000..7cb342eb8 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/expressions/streaming_concatenation2.sv b/regression/verilog/expressions/streaming_concatenation2.sv new file mode 100644 index 000000000..90ebefa2a --- /dev/null +++ b/regression/verilog/expressions/streaming_concatenation2.sv @@ -0,0 +1,6 @@ +module main; + + // operand must be integral + wire x = {<<{1.1}}; + +endmodule diff --git a/regression/verilog/expressions/wildcard_equality2.desc b/regression/verilog/expressions/wildcard_equality2.desc index 82ed5243a..c2ad5e192 100644 --- a/regression/verilog/expressions/wildcard_equality2.desc +++ b/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. diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index d0cc7ac1b..42c3be9eb 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/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( diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index d9c6ba15b..9d8087f32 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/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)