From 374151c229ca0bce3011c9c39f2564390d258fa2 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. --- regression/verilog/expressions/equality3.desc | 5 +- regression/verilog/expressions/mod2.desc | 6 +- .../verilog/expressions/replication3.desc | 10 +++ regression/verilog/expressions/replication3.v | 5 ++ regression/verilog/expressions/shr2.desc | 6 +- .../expressions/wildcard_equality2.desc | 6 +- src/verilog/verilog_typecheck_expr.cpp | 68 ++++++++++++++++--- src/verilog/verilog_typecheck_expr.h | 1 + 8 files changed, 87 insertions(+), 20 deletions(-) create mode 100644 regression/verilog/expressions/replication3.desc create mode 100644 regression/verilog/expressions/replication3.v diff --git a/regression/verilog/expressions/equality3.desc b/regression/verilog/expressions/equality3.desc index f294b309..e7307361 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 8652378a..87d22d74 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/replication3.desc b/regression/verilog/expressions/replication3.desc new file mode 100644 index 00000000..8802259e --- /dev/null +++ b/regression/verilog/expressions/replication3.desc @@ -0,0 +1,10 @@ +KNOWNBUG +replication3.v +--bound 0 +^file .* line 4: operand 1\.1 must be integral$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Should be errored. diff --git a/regression/verilog/expressions/replication3.v b/regression/verilog/expressions/replication3.v new file mode 100644 index 00000000..fa4b2188 --- /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 300ce761..a83a5c43 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/wildcard_equality2.desc b/regression/verilog/expressions/wildcard_equality2.desc index 82ed5243..c2ad5e19 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 d0cc7ac1..81ca4605 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(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) + { + expr = typecast_exprt{expr, unsignedbv_typet{1}}; + } + 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: @@ -3020,11 +3051,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 +3083,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 +3110,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 +3131,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 d9c6ba15..ccc2f759 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(exprt &); // SVA void convert_sva(exprt &expr)