From dc998f6cca899ebcdc1d13ca91f71d62d622b1fa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 28 Mar 2025 11:48:53 -0700 Subject: [PATCH 1/2] SMV: expression typechecker now post-traversal This hoists the recursive call to typecheck the expression operands out of the case split, i.e., operands are always typechecked first. --- src/smvlang/parser.y | 12 ++++++-- src/smvlang/smv_typecheck.cpp | 54 ++++------------------------------- 2 files changed, 16 insertions(+), 50 deletions(-) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index a5e2bd76b..2d78425c7 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -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; } @@ -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); } ; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 0bec5d149..03a4d04b7 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -631,6 +631,12 @@ Function: smv_typecheckt::typecheck_expr_rec void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) { + // Do the operands + for(auto &op : expr.operands()) + typecheck_expr_rec(op, mode); + + // now post-traversal + if(expr.id()==ID_symbol || expr.id()==ID_next_symbol) { @@ -668,9 +674,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? @@ -708,9 +711,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) @@ -731,9 +731,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(); @@ -757,9 +754,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); @@ -784,10 +778,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()); @@ -800,9 +791,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 @@ -873,9 +861,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(); @@ -911,7 +896,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( @@ -923,7 +907,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) @@ -934,7 +917,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()); } @@ -949,7 +931,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( @@ -961,8 +942,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()); } @@ -975,8 +954,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()); } @@ -996,7 +973,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) @@ -1024,8 +1000,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(to_constant_expr(binary_expr.rhs())); @@ -1038,8 +1012,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(to_constant_expr(binary_expr.rhs())); @@ -1056,8 +1028,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) @@ -1077,8 +1047,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) @@ -1112,9 +1080,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) @@ -1139,7 +1104,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(); @@ -1154,8 +1118,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 = @@ -1174,8 +1136,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(); @@ -1196,7 +1156,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 @@ -1209,7 +1168,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 From 17ede1a9f67938fab04c83979a75a4dfd7ba244e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Mar 2025 19:33:46 -0700 Subject: [PATCH 2/2] SMV: stack-based expression type checking To address #17, this replaces the recusion in the SMV expression type checker by exprt::visit_post. Closes #17 --- src/smvlang/smv_typecheck.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 03a4d04b7..78051cec4 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -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; @@ -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); }); } /*******************************************************************\ @@ -629,12 +632,8 @@ 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) { - // Do the operands - for(auto &op : expr.operands()) - typecheck_expr_rec(op, mode); - // now post-traversal if(expr.id()==ID_symbol ||