Skip to content

Conversation

kroening
Copy link
Collaborator

@kroening kroening commented Oct 1, 2025

This cleans up verilog_typecheck_exprt::downwards_type_progatation to handle all the cases in 1800-2017 11.8.2.

@tautschnig
Copy link
Collaborator

Should the failing regression test cause the test to be changed or is this a bug being introduced?

@kroening
Copy link
Collaborator Author

kroening commented Oct 2, 2025

Should the failing regression test cause the test to be changed or is this a bug being introduced?

I'll change the test. I think it's better not to try to optimise during type checking, even if it's just folding a constant.

@kroening
Copy link
Collaborator Author

kroening commented Oct 2, 2025

I'll do the semantic change as a separate PR.

This cleans up verilog_typecheck_exprt::downwards_type_progatation to handle
all the cases in 1800-2017 11.8.2.
@kroening kroening force-pushed the verilog-downwards-prop branch from ef2522f to 9b7f39d Compare October 2, 2025 17:09
@kroening
Copy link
Collaborator Author

kroening commented Oct 2, 2025

Restored previous semantics, which prevents the test failure

Comment on lines +235 to +254
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);
}
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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants