Skip to content

Commit dc998f6

Browse files
kroeningkroening
committed
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.
1 parent 0ec55ad commit dc998f6

File tree

2 files changed

+16
-50
lines changed

2 files changed

+16
-50
lines changed

‎src/smvlang/parser.y

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -678,7 +678,7 @@ term : variable_name
678678
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
679679
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
680680
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
681-
| NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
681+
| number_expr
682682
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
683683
| FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
684684
| case_Token cases esac_Token { $$=$2; }
@@ -770,11 +770,19 @@ term : variable_name
770770
}
771771
;
772772

773+
number_expr: NUMBER_Token
774+
{
775+
init($$, ID_constant);
776+
stack_expr($$).set(ID_value, stack_expr($1).id());
777+
stack_expr($$).type()=integer_typet();
778+
}
779+
;
780+
773781
bound : '[' NUMBER_Token ',' NUMBER_Token ']'
774782
{ init($$); mto($$, $2); mto($$, $4); }
775783
;
776784

777-
range : NUMBER_Token DOTDOT_Token NUMBER_Token
785+
range : number_expr DOTDOT_Token number_expr
778786
{ init($$); mto($$, $1); mto($$, $3); }
779787
;
780788

‎src/smvlang/smv_typecheck.cpp

Lines changed: 6 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -631,6 +631,12 @@ Function: smv_typecheckt::typecheck_expr_rec
631631

632632
void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
633633
{
634+
// Do the operands
635+
for(auto &op : expr.operands())
636+
typecheck_expr_rec(op, mode);
637+
638+
// now post-traversal
639+
634640
if(expr.id()==ID_symbol ||
635641
expr.id()==ID_next_symbol)
636642
{
@@ -668,9 +674,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
668674
{
669675
PRECONDITION(!expr.operands().empty());
670676

671-
for(auto &op : expr.operands())
672-
typecheck_expr_rec(op, mode);
673-
674677
auto &op0_type = to_multi_ary_expr(expr).op0().type();
675678

676679
// boolean or bit-wise?
@@ -708,9 +711,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
708711
else if(expr.id() == ID_smv_iff)
709712
{
710713
auto &binary_expr = to_binary_expr(expr);
711-
typecheck_expr_rec(binary_expr.lhs(), mode);
712-
typecheck_expr_rec(binary_expr.rhs(), mode);
713-
714714
auto &op0_type = binary_expr.op0().type();
715715

716716
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)
731731
}
732732
else if(expr.id()==ID_constraint_select_one)
733733
{
734-
for(auto &op : expr.operands())
735-
typecheck_expr_rec(op, mode);
736-
737734
typet op_type;
738735
op_type.make_nil();
739736

@@ -757,9 +754,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
757754
exprt &op0 = to_binary_expr(expr).op0();
758755
exprt &op1 = to_binary_expr(expr).op1();
759756

760-
typecheck_expr_rec(op0, mode);
761-
typecheck_expr_rec(op1, mode);
762-
763757
typet op_type = type_union(op0.type(), op1.type(), expr.source_location());
764758

765759
convert_expr_to(op0, op_type);
@@ -784,10 +778,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
784778
auto &if_expr = to_if_expr(expr);
785779
auto &true_case = if_expr.true_case();
786780
auto &false_case = if_expr.false_case();
787-
typecheck_expr_rec(if_expr.cond(), mode);
788781
convert_expr_to(if_expr.cond(), bool_typet{});
789-
typecheck_expr_rec(true_case, mode);
790-
typecheck_expr_rec(false_case, mode);
791782
expr.type() =
792783
type_union(true_case.type(), false_case.type(), expr.source_location());
793784
convert_expr_to(true_case, expr.type());
@@ -800,9 +791,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
800791
auto &op0 = to_binary_expr(expr).op0();
801792
auto &op1 = to_binary_expr(expr).op1();
802793

803-
typecheck_expr_rec(op0, mode);
804-
typecheck_expr_rec(op1, mode);
805-
806794
if(op0.type().id() == ID_range || op0.type().id() == ID_bool)
807795
{
808796
// find proper type for precise arithmetic
@@ -873,9 +861,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
873861
else if(expr.id()==ID_cond)
874862
{
875863
// case ... esac
876-
for(auto &op : expr.operands())
877-
typecheck_expr_rec(op, mode);
878-
879864
bool condition = true;
880865

881866
expr.type().make_nil();
@@ -911,7 +896,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
911896
<< "CTL operator not permitted here";
912897
expr.type() = bool_typet();
913898
auto &op = to_unary_expr(expr).op();
914-
typecheck_expr_rec(op, mode);
915899
convert_expr_to(op, expr.type());
916900
}
917901
else if(
@@ -923,7 +907,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
923907
<< "CTL operator not permitted here";
924908
expr.type() = bool_typet();
925909
auto &op2 = to_ternary_expr(expr).op2();
926-
typecheck_expr_rec(op2, mode);
927910
convert_expr_to(op2, expr.type());
928911
}
929912
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)
934917
expr.type() = bool_typet();
935918
for(std::size_t i = 0; i < expr.operands().size(); i++)
936919
{
937-
typecheck_expr_rec(expr.operands()[i], mode);
938920
if(i == 0 || i == 3)
939921
convert_expr_to(expr.operands()[i], expr.type());
940922
}
@@ -949,7 +931,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
949931
<< "LTL operator not permitted here";
950932
expr.type() = bool_typet{};
951933
auto &op = to_unary_expr(expr).op();
952-
typecheck_expr_rec(op, mode);
953934
convert_expr_to(op, expr.type());
954935
}
955936
else if(
@@ -961,8 +942,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
961942
<< "CTL operator not permitted here";
962943
auto &binary_expr = to_binary_expr(expr);
963944
expr.type() = bool_typet{};
964-
typecheck_expr_rec(binary_expr.lhs(), mode);
965-
typecheck_expr_rec(binary_expr.rhs(), mode);
966945
convert_expr_to(binary_expr.lhs(), expr.type());
967946
convert_expr_to(binary_expr.rhs(), expr.type());
968947
}
@@ -975,8 +954,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
975954
<< "LTL operator not permitted here";
976955
auto &binary_expr = to_binary_expr(expr);
977956
expr.type() = bool_typet{};
978-
typecheck_expr_rec(binary_expr.lhs(), mode);
979-
typecheck_expr_rec(binary_expr.rhs(), mode);
980957
convert_expr_to(binary_expr.lhs(), expr.type());
981958
convert_expr_to(binary_expr.rhs(), expr.type());
982959
}
@@ -996,7 +973,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
996973
else if(expr.id() == ID_unary_minus)
997974
{
998975
auto &uminus_expr = to_unary_minus_expr(expr);
999-
typecheck_expr_rec(uminus_expr.op(), mode);
1000976
auto &op_type = uminus_expr.op().type();
1001977

1002978
if(op_type.id() == ID_range)
@@ -1024,8 +1000,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
10241000
else if(expr.id() == ID_smv_swconst)
10251001
{
10261002
auto &binary_expr = to_binary_expr(expr);
1027-
typecheck_expr_rec(binary_expr.lhs(), mode);
1028-
typecheck_expr_rec(binary_expr.rhs(), mode);
10291003
PRECONDITION(binary_expr.lhs().is_constant());
10301004
PRECONDITION(binary_expr.rhs().is_constant());
10311005
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1038,8 +1012,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
10381012
else if(expr.id() == ID_smv_uwconst)
10391013
{
10401014
auto &binary_expr = to_binary_expr(expr);
1041-
typecheck_expr_rec(binary_expr.lhs(), mode);
1042-
typecheck_expr_rec(binary_expr.rhs(), mode);
10431015
PRECONDITION(binary_expr.lhs().is_constant());
10441016
PRECONDITION(binary_expr.rhs().is_constant());
10451017
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1056,8 +1028,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
10561028
auto &binary_expr = to_binary_expr(expr);
10571029

10581030
// The LHS must be a word type.
1059-
typecheck_expr_rec(binary_expr.lhs(), mode);
1060-
10611031
binary_expr.type() = binary_expr.lhs().type();
10621032

10631033
if(binary_expr.type().id() == ID_signedbv)
@@ -1077,8 +1047,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
10771047
}
10781048

10791049
// The RHS must be an integer constant
1080-
typecheck_expr_rec(binary_expr.rhs(), mode);
1081-
10821050
if(
10831051
binary_expr.rhs().type().id() != ID_range &&
10841052
binary_expr.rhs().type().id() != ID_natural)
@@ -1112,9 +1080,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
11121080
{
11131081
auto &binary_expr = to_binary_expr(expr);
11141082

1115-
typecheck_expr_rec(binary_expr.lhs(), mode);
1116-
typecheck_expr_rec(binary_expr.rhs(), mode);
1117-
11181083
if(
11191084
binary_expr.lhs().type().id() != ID_signedbv &&
11201085
binary_expr.lhs().type().id() != ID_unsignedbv)
@@ -1139,7 +1104,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
11391104
else if(expr.id() == ID_smv_sizeof)
11401105
{
11411106
auto &op = to_unary_expr(expr).op();
1142-
typecheck_expr_rec(op, mode);
11431107
if(op.type().id() == ID_signedbv || op.type().id() == ID_unsignedbv)
11441108
{
11451109
auto bits = to_bitvector_type(op.type()).get_width();
@@ -1154,8 +1118,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
11541118
else if(expr.id() == ID_smv_resize)
11551119
{
11561120
auto &binary_expr = to_binary_expr(expr);
1157-
typecheck_expr_rec(binary_expr.lhs(), mode);
1158-
typecheck_expr_rec(binary_expr.rhs(), mode);
11591121
PRECONDITION(binary_expr.rhs().is_constant());
11601122
auto &lhs_type = binary_expr.lhs().type();
11611123
auto new_bits =
@@ -1174,8 +1136,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
11741136
else if(expr.id() == ID_smv_extend)
11751137
{
11761138
auto &binary_expr = to_binary_expr(expr);
1177-
typecheck_expr_rec(binary_expr.lhs(), mode);
1178-
typecheck_expr_rec(binary_expr.rhs(), mode);
11791139
PRECONDITION(binary_expr.rhs().is_constant());
11801140
auto &lhs_type = binary_expr.lhs().type();
11811141
auto old_bits = to_bitvector_type(lhs_type).get_width();
@@ -1196,7 +1156,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
11961156
{
11971157
// a reinterpret cast
11981158
auto &op = to_unary_expr(expr).op();
1199-
typecheck_expr_rec(op, mode);
12001159
if(op.type().id() == ID_signedbv)
12011160
expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
12021161
else
@@ -1209,7 +1168,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
12091168
{
12101169
// a reinterpret cast
12111170
auto &op = to_unary_expr(expr).op();
1212-
typecheck_expr_rec(op, mode);
12131171
if(op.type().id() == ID_unsignedbv)
12141172
expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
12151173
else

0 commit comments

Comments
 (0)