Skip to content

Commit

Permalink
Verilog: add checks for operators that require integral types
Browse files Browse the repository at this point in the history
This adds checks to the typechecker to enforce that the operands have an
integral type.
  • Loading branch information
kroening committed Nov 17, 2024
1 parent 51fa81e commit 374151c
Show file tree
Hide file tree
Showing 8 changed files with 87 additions and 20 deletions.
5 changes: 2 additions & 3 deletions regression/verilog/expressions/equality3.desc
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
KNOWNBUG
CORE
equality3.v
--bound 0
^EXIT=0$
^EXIT=2$
^SIGNAL=0$
--
^warning: ignoring
--
This should be errored.
6 changes: 3 additions & 3 deletions regression/verilog/expressions/mod2.desc
Original file line number Diff line number Diff line change
@@ -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.
10 changes: 10 additions & 0 deletions regression/verilog/expressions/replication3.desc
Original file line number Diff line number Diff line change
@@ -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.
5 changes: 5 additions & 0 deletions regression/verilog/expressions/replication3.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module main;

wire [31:0] x = {4{1.1}};

endmodule
6 changes: 3 additions & 3 deletions regression/verilog/expressions/shr2.desc
Original file line number Diff line number Diff line change
@@ -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.
6 changes: 3 additions & 3 deletions regression/verilog/expressions/wildcard_equality2.desc
Original file line number Diff line number Diff line change
@@ -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.
68 changes: 60 additions & 8 deletions src/verilog/verilog_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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 ||
Expand All @@ -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();
Expand All @@ -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);
Expand All @@ -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(
Expand Down
1 change: 1 addition & 0 deletions src/verilog/verilog_typecheck_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 374151c

Please sign in to comment.