Skip to content

Commit b872a3f

Browse files
tautschnigtautschnig
authored
Merge pull request #907 from diffblue/smv-parser-cleanup
SMV: removing typing from parser
2 parents 7c49dd9 + 8a54d3a commit b872a3f

File tree

3 files changed

+54
-61
lines changed

3 files changed

+54
-61
lines changed

‎regression/smv/define/define1.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
KNOWNBUG
1+
CORE broken-smt-backend
22
define1.smv
33

44
^EXIT=0$
55
^SIGNAL=0$
66
--
77
--
8-
This yields a type error.

‎regression/smv/define/define1.smv

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,7 @@ MODULE main
33
DEFINE a := 1;
44

55
VAR b : 1..4;
6+
ASSIGN init(b) := 2;
67
ASSIGN next(b) := a + 1;
8+
9+
LTLSPEC G b=2

‎src/smvlang/parser.y

Lines changed: 50 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -85,49 +85,40 @@ Function: init
8585

8686
/// binary TODO[docu]
8787
static void binary(YYSTYPE & x_result, YYSTYPE & y_lhs, const irep_idt &id,
88-
YYSTYPE &z_rhs, const typet &t)
88+
YYSTYPE &z_rhs)
8989
{
9090
init(x_result, id);
91-
stack_expr(x_result).type() = t;
9291
auto &lhs = stack_expr(y_lhs);
9392
auto &rhs = stack_expr(z_rhs);
9493
stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
9594
}
9695

97-
/// binary TODO[docu]
98-
static void binary_arith(YYSTYPE & x_result, YYSTYPE & y_lhs,
99-
const irep_idt &id, YYSTYPE &z_rhs)
100-
{
101-
init(x_result, id);
102-
auto &lhs = stack_expr(y_lhs);
103-
DATA_INVARIANT(lhs.type().id() != ID_nil, "arith expr without lhs type");
104-
stack_expr(x_result).type() = lhs.type();
105-
auto &rhs = stack_expr(z_rhs);
106-
stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
107-
}
108-
109-
/*******************************************************************\
96+
/*******************************************************************\
11097
111-
Function: j_binary
98+
Function: j_binary
11299
113-
Inputs:
100+
Inputs:
114101
115-
Outputs:
102+
Outputs:
116103
117-
Purpose:
104+
Purpose:
118105
119-
\*******************************************************************/
106+
\*******************************************************************/
120107

121-
static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id,
122-
YYSTYPE &op2, const typet &t) {
123-
if (stack_expr(op1).id() == id) {
124-
dest = op1;
125-
mto(dest, op2);
126-
} else if (stack_expr(op2).id() == id) {
127-
dest = op2;
128-
mto(dest, op1);
129-
} else
130-
binary(dest, op1, id, op2, t);
108+
static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id, YYSTYPE &op2)
109+
{
110+
if(stack_expr(op1).id() == id)
111+
{
112+
dest = op1;
113+
mto(dest, op2);
114+
}
115+
else if(stack_expr(op2).id() == id)
116+
{
117+
dest = op2;
118+
mto(dest, op1);
119+
}
120+
else
121+
binary(dest, op1, id, op2);
131122
}
132123

133124
/*******************************************************************\
@@ -431,7 +422,7 @@ assignments: assignment
431422

432423
assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
433424
{
434-
binary($$, $3, ID_equal, $6, bool_typet{});
425+
binary($$, $3, ID_equal, $6);
435426

436427
if(stack_expr($1).id()==ID_smv_next)
437428
{
@@ -486,7 +477,7 @@ define : assignment_var BECOMES_Token formula ';'
486477
DATA_INVARIANT(false, "unexpected variable class");
487478
}
488479

489-
binary($$, $1, ID_equal, $3, bool_typet{});
480+
binary($$, $1, ID_equal, $3);
490481
PARSER.module->add_define(stack_expr($$));
491482
}
492483
;
@@ -500,7 +491,7 @@ term : variable_name
500491
| '{' formula_list '}' { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
501492
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
502493
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
503-
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5, stack_expr($5).type()); }
494+
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
504495
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
505496
| NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
506497
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
@@ -511,41 +502,41 @@ term : variable_name
511502
| SWITCH_Token '(' variable_name ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
512503
| MINUS_Token term %prec UMINUS
513504
{ init($$, ID_unary_minus); mto($$, $2); }
514-
| term MOD_Token term { binary_arith($$, $1, ID_mod, $3); }
515-
| term TIMES_Token term { binary_arith($$, $1, ID_mult, $3); }
516-
| term DIVIDE_Token term { binary_arith($$, $1, ID_div, $3); }
517-
| term PLUS_Token term { binary_arith($$, $1, ID_plus, $3); }
518-
| term MINUS_Token term { binary_arith($$, $1, ID_minus, $3); }
519-
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3, bool_typet{}); }
520-
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3, bool_typet{}); }
521-
| term XOR_Token term { j_binary($$, $1, ID_xor, $3, bool_typet{}); }
522-
| term OR_Token term { j_binary($$, $1, ID_or, $3, bool_typet{}); }
523-
| term AND_Token term { j_binary($$, $1, ID_and, $3, bool_typet{}); }
505+
| term MOD_Token term { binary($$, $1, ID_mod, $3); }
506+
| term TIMES_Token term { binary($$, $1, ID_mult, $3); }
507+
| term DIVIDE_Token term { binary($$, $1, ID_div, $3); }
508+
| term PLUS_Token term { binary($$, $1, ID_plus, $3); }
509+
| term MINUS_Token term { binary($$, $1, ID_minus, $3); }
510+
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); }
511+
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
512+
| term XOR_Token term { j_binary($$, $1, ID_xor, $3); }
513+
| term OR_Token term { j_binary($$, $1, ID_or, $3); }
514+
| term AND_Token term { j_binary($$, $1, ID_and, $3); }
524515
| NOT_Token term { init($$, ID_not); mto($$, $2); }
525516
| AX_Token term { init($$, ID_AX); mto($$, $2); }
526517
| AF_Token term { init($$, ID_AF); mto($$, $2); }
527518
| AG_Token term { init($$, ID_AG); mto($$, $2); }
528519
| EX_Token term { init($$, ID_EX); mto($$, $2); }
529520
| EF_Token term { init($$, ID_EF); mto($$, $2); }
530521
| EG_Token term { init($$, ID_EG); mto($$, $2); }
531-
| A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5, bool_typet{}); }
532-
| A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5, bool_typet{}); }
533-
| E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5, bool_typet{}); }
534-
| E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5, bool_typet{}); }
522+
| A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5); }
523+
| A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); }
524+
| E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); }
525+
| E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); }
535526
| F_Token term { init($$, ID_F); mto($$, $2); }
536527
| G_Token term { init($$, ID_G); mto($$, $2); }
537528
| X_Token term { init($$, ID_X); mto($$, $2); }
538-
| term U_Token term { binary($$, $1, ID_U, $3, bool_typet{}); }
539-
| term R_Token term { binary($$, $1, ID_R, $3, bool_typet{}); }
540-
| term EQUAL_Token term { binary($$, $1, ID_equal, $3, bool_typet{}); }
541-
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3, bool_typet{}); }
542-
| term LT_Token term { binary($$, $1, ID_lt, $3, bool_typet{}); }
543-
| term LE_Token term { binary($$, $1, ID_le, $3, bool_typet{}); }
544-
| term GT_Token term { binary($$, $1, ID_gt, $3, bool_typet{}); }
545-
| term GE_Token term { binary($$, $1, ID_ge, $3, bool_typet{}); }
546-
| term UNION_Token term { binary($$, $1, ID_smv_union, $3, bool_typet{}); }
547-
| term IN_Token term { binary($$, $1, ID_smv_setin, $3, bool_typet{}); }
548-
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3, bool_typet{}); }
529+
| term U_Token term { binary($$, $1, ID_U, $3); }
530+
| term R_Token term { binary($$, $1, ID_R, $3); }
531+
| term EQUAL_Token term { binary($$, $1, ID_equal, $3); }
532+
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
533+
| term LT_Token term { binary($$, $1, ID_lt, $3); }
534+
| term LE_Token term { binary($$, $1, ID_le, $3); }
535+
| term GT_Token term { binary($$, $1, ID_gt, $3); }
536+
| term GE_Token term { binary($$, $1, ID_ge, $3); }
537+
| term UNION_Token term { binary($$, $1, ID_smv_union, $3); }
538+
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
539+
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
549540
;
550541

551542
formula_list: formula { init($$); mto($$, $1); }
@@ -636,7 +627,7 @@ cases :
636627
;
637628

638629
case : formula ':' formula ';'
639-
{ binary($$, $1, ID_case, $3, stack_expr($3).type()); }
630+
{ binary($$, $1, ID_case, $3); }
640631
;
641632

642633
switches :

0 commit comments

Comments
 (0)