Skip to content

Commit 3ccc28f

Browse files
tautschnigtautschnig
authored
Merge pull request #1511 from diffblue/smv-typecheck-hoist-recursion
SMV type checker: pull up recursion on operands
2 parents d25b571 + 0127b0a commit 3ccc28f

File tree

1 file changed

+19
-69
lines changed

1 file changed

+19
-69
lines changed

‎src/smvlang/smv_typecheck.cpp‎

Lines changed: 19 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -726,6 +726,7 @@ Function: smv_typecheckt::typecheck_expr_rec
726726

727727
void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
728728
{
729+
// pre-traversal
729730
if(expr.id() == ID_smv_next)
730731
{
731732
if(next)
@@ -737,8 +738,15 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
737738
expr = to_unary_expr(expr).op();
738739

739740
typecheck_expr_rec(expr, mode, true);
741+
return;
740742
}
741-
else if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
743+
744+
// typecheck all the operands recursively
745+
for(auto &op : expr.operands())
746+
typecheck_expr_rec(op, mode, next);
747+
748+
// now post-traversal
749+
if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
742750
{
743751
const irep_idt &identifier = expr.get(ID_identifier);
744752

@@ -776,9 +784,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
776784
{
777785
PRECONDITION(!expr.operands().empty());
778786

779-
for(auto &op : expr.operands())
780-
typecheck_expr_rec(op, mode, next);
781-
782787
auto &op0_type = to_multi_ary_expr(expr).op0().type();
783788

784789
// boolean or bit-wise?
@@ -816,8 +821,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
816821
else if(expr.id() == ID_smv_iff)
817822
{
818823
auto &binary_expr = to_binary_expr(expr);
819-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
820-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
821824

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

@@ -839,9 +842,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
839842
}
840843
else if(expr.id()==ID_constraint_select_one)
841844
{
842-
for(auto &op : expr.operands())
843-
typecheck_expr_rec(op, mode, next);
844-
845845
typet op_type;
846846
op_type.make_nil();
847847

@@ -865,9 +865,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
865865
exprt &op0 = to_binary_expr(expr).op0();
866866
exprt &op1 = to_binary_expr(expr).op1();
867867

868-
typecheck_expr_rec(op0, mode, next);
869-
typecheck_expr_rec(op1, mode, next);
870-
871868
typet op_type = type_union(op0.type(), op1.type(), expr.source_location());
872869

873870
convert_expr_to(op0, op_type);
@@ -892,12 +889,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
892889
auto &if_expr = to_if_expr(expr);
893890
auto &true_case = if_expr.true_case();
894891
auto &false_case = if_expr.false_case();
895-
typecheck_expr_rec(if_expr.cond(), mode, next);
896-
convert_expr_to(if_expr.cond(), bool_typet{});
897-
typecheck_expr_rec(true_case, mode, next);
898-
typecheck_expr_rec(false_case, mode, next);
892+
899893
expr.type() =
900894
type_union(true_case.type(), false_case.type(), expr.source_location());
895+
896+
convert_expr_to(if_expr.cond(), bool_typet{});
901897
convert_expr_to(true_case, expr.type());
902898
convert_expr_to(false_case, expr.type());
903899
}
@@ -908,9 +904,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
908904
auto &op0 = to_binary_expr(expr).op0();
909905
auto &op1 = to_binary_expr(expr).op1();
910906

911-
typecheck_expr_rec(op0, mode, next);
912-
typecheck_expr_rec(op1, mode, next);
913-
914907
if(op0.type().id() == ID_range || op0.type().id() == ID_bool)
915908
{
916909
// find proper type for precise arithmetic
@@ -991,9 +984,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
991984
else if(expr.id()==ID_cond)
992985
{
993986
// case ... esac
994-
for(auto &op : expr.operands())
995-
typecheck_expr_rec(op, mode, next);
996-
997987
bool condition = true;
998988

999989
expr.type().make_nil();
@@ -1029,7 +1019,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10291019
<< "CTL operator not permitted here";
10301020
expr.type() = bool_typet();
10311021
auto &op = to_unary_expr(expr).op();
1032-
typecheck_expr_rec(op, mode, next);
10331022
convert_expr_to(op, expr.type());
10341023
}
10351024
else if(
@@ -1041,7 +1030,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10411030
<< "CTL operator not permitted here";
10421031
expr.type() = bool_typet();
10431032
auto &op2 = to_ternary_expr(expr).op2();
1044-
typecheck_expr_rec(op2, mode, next);
10451033
convert_expr_to(op2, expr.type());
10461034
}
10471035
else if(expr.id() == ID_smv_ABU || expr.id() == ID_smv_EBU)
@@ -1052,7 +1040,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10521040
expr.type() = bool_typet();
10531041
for(std::size_t i = 0; i < expr.operands().size(); i++)
10541042
{
1055-
typecheck_expr_rec(expr.operands()[i], mode, next);
10561043
if(i == 0 || i == 3)
10571044
convert_expr_to(expr.operands()[i], expr.type());
10581045
}
@@ -1067,7 +1054,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10671054
<< "LTL operator not permitted here";
10681055
expr.type() = bool_typet{};
10691056
auto &op = to_unary_expr(expr).op();
1070-
typecheck_expr_rec(op, mode, next);
10711057
convert_expr_to(op, expr.type());
10721058
}
10731059
else if(
@@ -1079,8 +1065,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10791065
<< "CTL operator not permitted here";
10801066
auto &binary_expr = to_binary_expr(expr);
10811067
expr.type() = bool_typet{};
1082-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1083-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
10841068
convert_expr_to(binary_expr.lhs(), expr.type());
10851069
convert_expr_to(binary_expr.rhs(), expr.type());
10861070
}
@@ -1093,8 +1077,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
10931077
<< "LTL operator not permitted here";
10941078
auto &binary_expr = to_binary_expr(expr);
10951079
expr.type() = bool_typet{};
1096-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1097-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
10981080
convert_expr_to(binary_expr.lhs(), expr.type());
10991081
convert_expr_to(binary_expr.rhs(), expr.type());
11001082
}
@@ -1108,9 +1090,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
11081090
auto &lhs = to_binary_expr(expr).lhs();
11091091
auto &rhs = to_binary_expr(expr).rhs();
11101092

1111-
typecheck_expr_rec(lhs, mode, next);
1112-
typecheck_expr_rec(rhs, mode, next);
1113-
11141093
// The RHS can be a set or a singleton
11151094
if(rhs.type().id() == ID_smv_set)
11161095
{
@@ -1142,7 +1121,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
11421121
else if(expr.id() == ID_unary_minus)
11431122
{
11441123
auto &uminus_expr = to_unary_minus_expr(expr);
1145-
typecheck_expr_rec(uminus_expr.op(), mode, next);
11461124
auto &op_type = uminus_expr.op().type();
11471125

11481126
if(op_type.id() == ID_range)
@@ -1170,8 +1148,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
11701148
else if(expr.id() == ID_smv_swconst)
11711149
{
11721150
auto &binary_expr = to_binary_expr(expr);
1173-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1174-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
11751151
PRECONDITION(binary_expr.lhs().is_constant());
11761152
PRECONDITION(binary_expr.rhs().is_constant());
11771153
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1184,8 +1160,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
11841160
else if(expr.id() == ID_smv_uwconst)
11851161
{
11861162
auto &binary_expr = to_binary_expr(expr);
1187-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1188-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
11891163
PRECONDITION(binary_expr.lhs().is_constant());
11901164
PRECONDITION(binary_expr.rhs().is_constant());
11911165
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1198,7 +1172,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
11981172
else if(expr.id() == ID_smv_abs)
11991173
{
12001174
auto &op = to_unary_expr(expr).op();
1201-
typecheck_expr_rec(op, mode, next);
12021175
if(op.type().id() == ID_range)
12031176
{
12041177
// ok
@@ -1222,8 +1195,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
12221195
{
12231196
auto &op = to_ternary_expr(expr).op0();
12241197

1225-
typecheck_expr_rec(op, mode, next);
1226-
12271198
if(op.type().id() != ID_unsignedbv && op.type().id() != ID_signedbv)
12281199
{
12291200
throw errort().with_location(op.source_location())
@@ -1232,8 +1203,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
12321203

12331204
auto &high = to_ternary_expr(expr).op1();
12341205

1235-
typecheck_expr_rec(high, OTHER, next);
1236-
12371206
// high must be an integer constant
12381207
if(high.type().id() != ID_range && high.type().id() != ID_natural)
12391208
{
@@ -1250,8 +1219,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
12501219

12511220
auto &low = to_ternary_expr(expr).op2();
12521221

1253-
typecheck_expr_rec(low, OTHER, next);
1254-
12551222
// low must be an integer constant
12561223
if(low.type().id() != ID_range && low.type().id() != ID_natural)
12571224
{
@@ -1277,7 +1244,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
12771244
else if(expr.id() == ID_smv_bool)
12781245
{
12791246
auto &op = to_unary_expr(expr).op();
1280-
typecheck_expr_rec(op, mode, next);
1247+
12811248
if(
12821249
op.type().id() == ID_bool || op.type().id() == ID_unsignedbv ||
12831250
op.type().id() == ID_signedbv || op.type().id() == ID_range)
@@ -1295,7 +1262,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
12951262
auto &multi_ary_expr = to_multi_ary_expr(expr);
12961263
for(auto &op : multi_ary_expr.operands())
12971264
{
1298-
typecheck_expr_rec(op, mode, next);
12991265
if(op.type().id() != ID_bool)
13001266
throw errort().with_location(op.source_location())
13011267
<< "count expects boolean arguments";
@@ -1306,9 +1272,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
13061272
{
13071273
auto &binary_expr = to_binary_expr(expr);
13081274

1309-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1310-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
1311-
13121275
binary_expr.type() = type_union(
13131276
binary_expr.lhs().type(),
13141277
binary_expr.rhs().type(),
@@ -1328,7 +1291,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
13281291
else if(expr.id() == ID_smv_toint)
13291292
{
13301293
auto &op = to_unary_expr(expr).op();
1331-
typecheck_expr_rec(op, mode, next);
1294+
13321295
if(op.type().id() == ID_bool)
13331296
{
13341297
expr.type() = range_typet{0, 1};
@@ -1350,10 +1313,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
13501313
else if(expr.id() == ID_smv_word1)
13511314
{
13521315
auto &op = to_unary_expr(expr).op();
1353-
typecheck_expr_rec(op, mode, next);
1316+
13541317
if(op.type().id() != ID_bool)
13551318
throw errort().with_location(op.source_location())
13561319
<< "word1 expects boolean argument";
1320+
13571321
expr.type() = unsignedbv_typet{1};
13581322
}
13591323
else if(
@@ -1363,8 +1327,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
13631327
auto &binary_expr = to_binary_expr(expr);
13641328

13651329
// The LHS must be a word type.
1366-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1367-
13681330
binary_expr.type() = binary_expr.lhs().type();
13691331

13701332
if(binary_expr.type().id() == ID_signedbv)
@@ -1384,14 +1346,14 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
13841346
}
13851347

13861348
// The RHS must be an integer constant
1387-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
1388-
13891349
if(
13901350
binary_expr.rhs().type().id() != ID_range &&
13911351
binary_expr.rhs().type().id() != ID_natural)
1352+
{
13921353
throw errort().with_location(expr.find_source_location())
13931354
<< "Shift distance must be integer, but got "
13941355
<< to_string(binary_expr.rhs().type());
1356+
}
13951357

13961358
if(binary_expr.rhs().id() != ID_constant)
13971359
throw errort().with_location(expr.find_source_location())
@@ -1419,9 +1381,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
14191381
{
14201382
auto &binary_expr = to_binary_expr(expr);
14211383

1422-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1423-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
1424-
14251384
if(
14261385
binary_expr.lhs().type().id() != ID_signedbv &&
14271386
binary_expr.lhs().type().id() != ID_unsignedbv)
@@ -1446,7 +1405,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
14461405
else if(expr.id() == ID_smv_sizeof)
14471406
{
14481407
auto &op = to_unary_expr(expr).op();
1449-
typecheck_expr_rec(op, mode, next);
1408+
14501409
if(op.type().id() == ID_signedbv || op.type().id() == ID_unsignedbv)
14511410
{
14521411
auto bits = to_bitvector_type(op.type()).get_width();
@@ -1461,8 +1420,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
14611420
else if(expr.id() == ID_smv_resize)
14621421
{
14631422
auto &binary_expr = to_binary_expr(expr);
1464-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1465-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
14661423
PRECONDITION(binary_expr.rhs().is_constant());
14671424
auto &lhs_type = binary_expr.lhs().type();
14681425
auto new_bits =
@@ -1481,8 +1438,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
14811438
else if(expr.id() == ID_smv_extend)
14821439
{
14831440
auto &binary_expr = to_binary_expr(expr);
1484-
typecheck_expr_rec(binary_expr.lhs(), mode, next);
1485-
typecheck_expr_rec(binary_expr.rhs(), mode, next);
14861441
PRECONDITION(binary_expr.rhs().is_constant());
14871442
auto &lhs_type = binary_expr.lhs().type();
14881443
auto old_bits = to_bitvector_type(lhs_type).get_width();
@@ -1503,7 +1458,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
15031458
{
15041459
// a reinterpret cast
15051460
auto &op = to_smv_unsigned_cast_expr(expr).op();
1506-
typecheck_expr_rec(op, mode, next);
15071461
if(op.type().id() == ID_signedbv)
15081462
expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
15091463
else
@@ -1516,7 +1470,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
15161470
{
15171471
// a reinterpret cast
15181472
auto &op = to_smv_signed_cast_expr(expr).op();
1519-
typecheck_expr_rec(op, mode, next);
15201473
if(op.type().id() == ID_unsignedbv)
15211474
expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
15221475
else
@@ -1529,9 +1482,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
15291482
{
15301483
// a set literal
15311484
expr.type() = typet{ID_smv_set};
1532-
1533-
for(auto &op : expr.operands())
1534-
typecheck_expr_rec(op, mode, next);
15351485
}
15361486
else
15371487
{

0 commit comments

Comments
 (0)