Skip to content

Verilog: cleanup downwards type propagation #1292

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Verilog: cleanup downwards type propagation #1292

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
203 changes: 92 additions & 111 deletions src/verilog/verilog_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,39 @@ void verilog_typecheck_exprt::propagate_type(

/*******************************************************************\

Function: zero_extend

Inputs:

Outputs:

Purpose:

\*******************************************************************/

static exprt zero_extend(const exprt &expr, const typet &type)
{
auto old_width = expr.type().id() == ID_bool ? 1
: expr.type().id() == ID_integer
? 32
: to_bitvector_type(expr.type()).get_width();

// first make unsigned
typet tmp_type;

if(type.id() == ID_unsignedbv)
tmp_type = unsignedbv_typet{old_width};
else if(type.id() == ID_verilog_unsignedbv)
tmp_type = verilog_unsignedbv_typet{old_width};
else
PRECONDITION(false);

return typecast_exprt::conditional_cast(
typecast_exprt::conditional_cast(expr, tmp_type), type);
}
Comment on lines +235 to +254
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't use of zero_extend_exprt make this unnecessary?


/*******************************************************************\

Function: verilog_typecheck_exprt::downwards_type_progatation

Inputs:
Expand All @@ -241,95 +274,76 @@ void verilog_typecheck_exprt::downwards_type_propagation(

// Any context-determined operand of an operator shall be the
// same type and size as the result of the operator.
// Exceptions:
// * result type real -- just cast
// * relational operators are always 1 bit unsigned
// As an exception, if the result type is real, the operands
// are just casted.

if(expr.type() == type)
return;

vtypet vt_from = vtypet(expr.type());
vtypet vt_to = vtypet(type);

if(!vt_from.is_other() && !vt_to.is_other() && expr.has_operands())
if(type.id() == ID_verilog_real || type.id() == ID_verilog_shortreal)
{
// arithmetic

if(
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
expr.id() == ID_div || expr.id() == ID_unary_minus ||
expr.id() == ID_unary_plus)
{
if(type.id() != ID_bool)
{
Forall_operands(it, expr)
propagate_type(*it, type);

expr.type() = type;

return;
}
}
else if(
expr.id() == ID_bitand || expr.id() == ID_bitor ||
expr.id() == ID_bitnand || expr.id() == ID_bitnor ||
expr.id() == ID_bitxor || expr.id() == ID_bitxnor ||
expr.id() == ID_bitnot)
{
Forall_operands(it, expr)
propagate_type(*it, type);

expr.type() = type;
expr = typecast_exprt{expr, type};
return;
}

if(type.id() == ID_bool)
{
if(expr.id() == ID_bitand)
expr.id(ID_and);
else if(expr.id() == ID_bitor)
expr.id(ID_or);
else if(expr.id() == ID_bitnand)
expr.id(ID_nand);
else if(expr.id() == ID_bitnor)
expr.id(ID_nor);
else if(expr.id() == ID_bitxor)
expr.id(ID_xor);
else if(expr.id() == ID_bitxnor)
expr.id(ID_xnor);
else if(expr.id() == ID_bitnot)
expr.id(ID_not);
}
// expressions with context-determined width, following
// 1800-2017 Table 11-21
if(
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand ||
expr.id() == ID_bitor || expr.id() == ID_bitxor ||
expr.id() == ID_bitxnor || expr.id() == ID_unary_plus ||
expr.id() == ID_unary_minus || expr.id() == ID_bitnot)
{
// All operands are context-determined.
for(auto &op : expr.operands())
downwards_type_propagation(op, type);
expr.type() = type;
return;
}
else if(
expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr ||
expr.id() == ID_power)
{
// The LHS is context-determined, the RHS is self-determined
auto &binary_expr = to_binary_expr(expr);
downwards_type_propagation(binary_expr.lhs(), type);
expr.type() = type;
return;
}
else if(expr.id() == ID_if)
{
// The first operand is self-determined, the others are context-determined
auto &if_expr = to_if_expr(expr);
downwards_type_propagation(if_expr.op1(), type);
downwards_type_propagation(if_expr.op2(), type);
expr.type() = type;
return;
}

return;
}
else if(expr.id() == ID_if)
{
if(expr.operands().size() == 3)
{
propagate_type(to_if_expr(expr).true_case(), type);
propagate_type(to_if_expr(expr).false_case(), type);
// Just cast the expression, leave any operands as they are.

expr.type() = type;
return;
}
}
else if(expr.id() == ID_shl) // does not work with shr
{
// does not work with boolean
if(type.id() != ID_bool)
{
if(expr.operands().size() == 2)
{
propagate_type(to_binary_expr(expr).op0(), type);
// not applicable to second operand
bool is_constant = expr.is_constant();

expr.type() = type;
return;
}
}
}
if(
(expr.type().id() == ID_signedbv ||
expr.type().id() == ID_verilog_signedbv) &&
(type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv) &&
get_width(expr.type()) < get_width(type))
{
// "If the operand shall be extended, then it shall be sign-extended only
// if the propagated type is signed."
// A typecast from signed to a larger unsigned would sign extend.
expr = zero_extend(expr, type);
}
else
{
expr = typecast_exprt{expr, type};
}

implicit_typecast(expr, type);
// fold constants
if(is_constant)
expr = verilog_simplifier(expr, ns);
}

/*******************************************************************\
Expand Down Expand Up @@ -2535,39 +2549,6 @@ void verilog_typecheck_exprt::tc_binary_expr(

/*******************************************************************\

Function: zero_extend

Inputs:

Outputs:

Purpose:

\*******************************************************************/

static exprt zero_extend(const exprt &expr, const typet &type)
{
auto old_width = expr.type().id() == ID_bool ? 1
: expr.type().id() == ID_integer
? 32
: to_bitvector_type(expr.type()).get_width();

// first make unsigned
typet tmp_type;

if(type.id() == ID_unsignedbv)
tmp_type = unsignedbv_typet{old_width};
else if(type.id() == ID_verilog_unsignedbv)
tmp_type = verilog_unsignedbv_typet{old_width};
else
PRECONDITION(false);

return typecast_exprt::conditional_cast(
typecast_exprt::conditional_cast(expr, tmp_type), type);
}

/*******************************************************************\

Function: verilog_typecheck_exprt::convert_relation

Inputs:
Expand Down
Loading