Skip to content

SMV: expression typechecker now post-traversal #1040

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 2 commits into
base: main
Choose a base branch
from
Open

SMV: expression typechecker now post-traversal #1040

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dc998f6
SMV: expression typechecker now post-traversal
kroening Mar 28, 2025
17ede1a
SMV: stack-based expression type checking
kroening Mar 30, 2025
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
12 changes: 10 additions & 2 deletions src/smvlang/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -678,7 +678,7 @@ term : variable_name
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
| NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
| number_expr
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
| FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
| case_Token cases esac_Token { $$=$2; }
Expand Down Expand Up @@ -770,11 +770,19 @@ term : variable_name
}
;

number_expr: NUMBER_Token
{
init($$, ID_constant);
stack_expr($$).set(ID_value, stack_expr($1).id());
stack_expr($$).type()=integer_typet();
}
;

bound : '[' NUMBER_Token ',' NUMBER_Token ']'
{ init($$); mto($$, $2); mto($$, $4); }
;

range : NUMBER_Token DOTDOT_Token NUMBER_Token
range : number_expr DOTDOT_Token number_expr
{ init($$); mto($$, $1); mto($$, $3); }
;

Expand Down
59 changes: 8 additions & 51 deletions src/smvlang/smv_typecheck.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ class smv_typecheckt:public typecheckt

void convert(smv_parse_treet::modulet::itemt &);
void typecheck(smv_parse_treet::modulet::itemt &);
void typecheck_expr_rec(exprt &, modet);
void typecheck_expr_node(exprt &, modet);
void convert_expr_to(exprt &, const typet &dest);

smv_parse_treet::modulet *modulep;
Expand Down Expand Up @@ -614,7 +614,10 @@ Function: smv_typecheckt::typecheck

void smv_typecheckt::typecheck(exprt &expr, modet mode)
{
typecheck_expr_rec(expr, mode);
// We use visit_post instead of recursion to avoid
// stack overflows on very deep nestings of DEFINE definitions.
expr.visit_post([this, mode](exprt &expr)
{ typecheck_expr_node(expr, mode); });
}

/*******************************************************************\
Expand All @@ -629,8 +632,10 @@ Function: smv_typecheckt::typecheck_expr_rec

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

void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
void smv_typecheckt::typecheck_expr_node(exprt &expr, modet mode)
{
// now post-traversal

if(expr.id()==ID_symbol ||
expr.id()==ID_next_symbol)
{
Expand Down Expand Up @@ -668,9 +673,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
{
PRECONDITION(!expr.operands().empty());

for(auto &op : expr.operands())
typecheck_expr_rec(op, mode);

auto &op0_type = to_multi_ary_expr(expr).op0().type();

// boolean or bit-wise?
Expand Down Expand Up @@ -708,9 +710,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_iff)
{
auto &binary_expr = to_binary_expr(expr);
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);

auto &op0_type = binary_expr.op0().type();

if(op0_type.id() == ID_signedbv || op0_type.id() == ID_unsignedbv)
Expand All @@ -731,9 +730,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
}
else if(expr.id()==ID_constraint_select_one)
{
for(auto &op : expr.operands())
typecheck_expr_rec(op, mode);

typet op_type;
op_type.make_nil();

Expand All @@ -757,9 +753,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
exprt &op0 = to_binary_expr(expr).op0();
exprt &op1 = to_binary_expr(expr).op1();

typecheck_expr_rec(op0, mode);
typecheck_expr_rec(op1, mode);

typet op_type = type_union(op0.type(), op1.type(), expr.source_location());

convert_expr_to(op0, op_type);
Expand All @@ -784,10 +777,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
auto &if_expr = to_if_expr(expr);
auto &true_case = if_expr.true_case();
auto &false_case = if_expr.false_case();
typecheck_expr_rec(if_expr.cond(), mode);
convert_expr_to(if_expr.cond(), bool_typet{});
typecheck_expr_rec(true_case, mode);
typecheck_expr_rec(false_case, mode);
expr.type() =
type_union(true_case.type(), false_case.type(), expr.source_location());
convert_expr_to(true_case, expr.type());
Expand All @@ -800,9 +790,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
auto &op0 = to_binary_expr(expr).op0();
auto &op1 = to_binary_expr(expr).op1();

typecheck_expr_rec(op0, mode);
typecheck_expr_rec(op1, mode);

if(op0.type().id() == ID_range || op0.type().id() == ID_bool)
{
// find proper type for precise arithmetic
Expand Down Expand Up @@ -873,9 +860,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id()==ID_cond)
{
// case ... esac
for(auto &op : expr.operands())
typecheck_expr_rec(op, mode);

bool condition = true;

expr.type().make_nil();
Expand Down Expand Up @@ -911,7 +895,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "CTL operator not permitted here";
expr.type() = bool_typet();
auto &op = to_unary_expr(expr).op();
typecheck_expr_rec(op, mode);
convert_expr_to(op, expr.type());
}
else if(
Expand All @@ -923,7 +906,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "CTL operator not permitted here";
expr.type() = bool_typet();
auto &op2 = to_ternary_expr(expr).op2();
typecheck_expr_rec(op2, mode);
convert_expr_to(op2, expr.type());
}
else if(expr.id() == ID_smv_ABU || expr.id() == ID_smv_EBU)
Expand All @@ -934,7 +916,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
expr.type() = bool_typet();
for(std::size_t i = 0; i < expr.operands().size(); i++)
{
typecheck_expr_rec(expr.operands()[i], mode);
if(i == 0 || i == 3)
convert_expr_to(expr.operands()[i], expr.type());
}
Expand All @@ -949,7 +930,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "LTL operator not permitted here";
expr.type() = bool_typet{};
auto &op = to_unary_expr(expr).op();
typecheck_expr_rec(op, mode);
convert_expr_to(op, expr.type());
}
else if(
Expand All @@ -961,8 +941,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "CTL operator not permitted here";
auto &binary_expr = to_binary_expr(expr);
expr.type() = bool_typet{};
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
convert_expr_to(binary_expr.lhs(), expr.type());
convert_expr_to(binary_expr.rhs(), expr.type());
}
Expand All @@ -975,8 +953,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
<< "LTL operator not permitted here";
auto &binary_expr = to_binary_expr(expr);
expr.type() = bool_typet{};
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
convert_expr_to(binary_expr.lhs(), expr.type());
convert_expr_to(binary_expr.rhs(), expr.type());
}
Expand All @@ -996,7 +972,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_unary_minus)
{
auto &uminus_expr = to_unary_minus_expr(expr);
typecheck_expr_rec(uminus_expr.op(), mode);
auto &op_type = uminus_expr.op().type();

if(op_type.id() == ID_range)
Expand Down Expand Up @@ -1024,8 +999,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_swconst)
{
auto &binary_expr = to_binary_expr(expr);
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
PRECONDITION(binary_expr.lhs().is_constant());
PRECONDITION(binary_expr.rhs().is_constant());
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
Expand All @@ -1038,8 +1011,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_uwconst)
{
auto &binary_expr = to_binary_expr(expr);
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
PRECONDITION(binary_expr.lhs().is_constant());
PRECONDITION(binary_expr.rhs().is_constant());
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
Expand All @@ -1056,8 +1027,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
auto &binary_expr = to_binary_expr(expr);

// The LHS must be a word type.
typecheck_expr_rec(binary_expr.lhs(), mode);

binary_expr.type() = binary_expr.lhs().type();

if(binary_expr.type().id() == ID_signedbv)
Expand All @@ -1077,8 +1046,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
}

// The RHS must be an integer constant
typecheck_expr_rec(binary_expr.rhs(), mode);

if(
binary_expr.rhs().type().id() != ID_range &&
binary_expr.rhs().type().id() != ID_natural)
Expand Down Expand Up @@ -1112,9 +1079,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
{
auto &binary_expr = to_binary_expr(expr);

typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);

if(
binary_expr.lhs().type().id() != ID_signedbv &&
binary_expr.lhs().type().id() != ID_unsignedbv)
Expand All @@ -1139,7 +1103,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_sizeof)
{
auto &op = to_unary_expr(expr).op();
typecheck_expr_rec(op, mode);
if(op.type().id() == ID_signedbv || op.type().id() == ID_unsignedbv)
{
auto bits = to_bitvector_type(op.type()).get_width();
Expand All @@ -1154,8 +1117,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_resize)
{
auto &binary_expr = to_binary_expr(expr);
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
PRECONDITION(binary_expr.rhs().is_constant());
auto &lhs_type = binary_expr.lhs().type();
auto new_bits =
Expand All @@ -1174,8 +1135,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
else if(expr.id() == ID_smv_extend)
{
auto &binary_expr = to_binary_expr(expr);
typecheck_expr_rec(binary_expr.lhs(), mode);
typecheck_expr_rec(binary_expr.rhs(), mode);
PRECONDITION(binary_expr.rhs().is_constant());
auto &lhs_type = binary_expr.lhs().type();
auto old_bits = to_bitvector_type(lhs_type).get_width();
Expand All @@ -1196,7 +1155,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
{
// a reinterpret cast
auto &op = to_unary_expr(expr).op();
typecheck_expr_rec(op, mode);
if(op.type().id() == ID_signedbv)
expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
else
Expand All @@ -1209,7 +1167,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
{
// a reinterpret cast
auto &op = to_unary_expr(expr).op();
typecheck_expr_rec(op, mode);
if(op.type().id() == ID_unsignedbv)
expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
else
Expand Down
Loading