1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
|
/** Subset extracted from spin.y by Stefan Radomski 2014 */
/***** spin: spin.y *****/
/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
/* All Rights Reserved. This software is for educational purposes only. */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code. Permission is given to distribute this code provided that */
/* this introductory message is not removed and no monies are exchanged. */
/* Software written by Gerard J. Holzmann. For tool documentation see: */
/* http://spinroot.com/ */
/* Send all bug-reports and/or questions to: bugs@spinroot.com */
%{
#include "../PromelaParser.h"
#include "promela.tab.hpp"
#include <sys/types.h>
#include <stdarg.h>
#define YYMAXDEPTH 20000 // default is 10000
#define YYDEBUG 1
#define YYERROR_VERBOSE 1
extern int promela_lex (PROMELA_STYPE* yylval_param, PROMELA_LTYPE* yylloc_param, void* yyscanner);
using namespace uscxml;
%}
%pure-parser
%debug
%locations
%file-prefix "promela"
%parse-param { uscxml::PromelaParser* ctx }
%lex-param {void * scanner}
%parse-param {void * scanner}
%define api.prefix promela_
%defines
%union {
uscxml::PromelaParserNode* node;
char* value;
}
%error-verbose
/* %type <node> expr_lst */
%type <node> expr pfld sfld varref decl_lst stmnt_lst vardcl ivar var_list one_decl prargs utype cmpnd
%type <node> stmnt Stmnt const_expr nlst vis arg
%token PML_VAR_ARRAY PML_VARLIST PML_DECL PML_DECLLIST PML_STMNT PML_COLON PML_EXPR PML_NAMELIST
%token '(' ')'
%token '[' ']'
%token '{' '}'
%token PML_ASSERT PML_PRINT PML_PRINTM
%token <value> PML_LEN PML_STRING
%token PML_TYPEDEF PML_MTYPE PML_INLINE PML_RETURN PML_LABEL PML_OF
%token PML_GOTO PML_BREAK PML_ELSE PML_SEMI PML_ARROW
%token PML_IF PML_FI PML_DO PML_OD PML_FOR PML_SELECT PML_IN PML_SEP PML_DOTDOT
%token PML_HIDDEN PML_SHOW PML_ISLOCAL
%token <value> PML_CONST PML_TYPE PML_XU /* val */
%token <value> PML_NAME PML_UNAME PML_PNAME PML_INAME /* sym */
%token PML_CLAIM PML_TRACE PML_INIT PML_LTL /* sym */
%token PML_COMMA PML_UNREC
%right PML_ASGN
%left PML_OR PML_AND
%left PML_BITOR PML_BITXOR PML_BITAND
%left PML_EQ PML_NE
%left PML_GT PML_LT PML_GE PML_LE
%left PML_LSHIFT PML_RSHIFT
%left PML_PLUS PML_MINUS
%left PML_TIMES PML_DIVIDE PML_MODULO
%left PML_INCR PML_DECR
%left PML_COMPL
%right PML_NEG
%left PML_DOT PML_CMPND
%%
/** PROMELA Grammar Rules **/
program :
decl_lst {
ctx->ast = $1;
ctx->type = PromelaParser::PROMELA_DECL;
}
| stmnt_lst {
ctx->ast = $1;
ctx->type = PromelaParser::PROMELA_STMNT;
}
| expr {
ctx->ast = $1;
ctx->type = PromelaParser::PROMELA_EXPR;
}
;
varref : cmpnd { $$ = $1; }
;
pfld : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); }
| PML_NAME '[' expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); }
;
cmpnd : pfld
sfld {
if ($2 != NULL) {
if ($2->type == PML_CMPND) {
$$ = ctx->node(PML_CMPND, 1, $1);
$$->merge($2); delete $2;
} else {
$$ = ctx->node(PML_CMPND, 2, $1, $2);
}
} else {
$$ = $1;
}
}
;
sfld : /* empty */ { $$ = NULL; }
| PML_DOT cmpnd %prec PML_DOT { $$ = $2; }
;
/*
expr_lst: expr { $$ = ctx->node(PML_EXPR, 1, $1); }
| expr PML_SEMI { $$ = ctx->node(PML_EXPR, 1, $1); }
| expr PML_SEMI expr_lst { $$ = ctx->node(PML_EXPR, 2, $1, $3); }
;
*/
expr : '(' expr ')' { $$ = $2; }
| expr PML_PLUS expr { $$ = ctx->node(PML_PLUS, 2, $1, $3); }
| expr PML_MINUS expr { $$ = ctx->node(PML_MINUS, 2, $1, $3); }
| expr PML_TIMES expr { $$ = ctx->node(PML_TIMES, 2, $1, $3); }
| expr PML_DIVIDE expr { $$ = ctx->node(PML_DIVIDE, 2, $1, $3); }
| expr PML_MODULO expr { $$ = ctx->node(PML_MODULO, 2, $1, $3); }
| expr PML_BITAND expr { $$ = ctx->node(PML_BITAND, 2, $1, $3); }
| expr PML_BITXOR expr { $$ = ctx->node(PML_BITXOR, 2, $1, $3); }
| expr PML_BITOR expr { $$ = ctx->node(PML_BITOR, 2, $1, $3); }
| expr PML_GT expr { $$ = ctx->node(PML_GT, 2, $1, $3); }
| expr PML_LT expr { $$ = ctx->node(PML_LT, 2, $1, $3); }
| expr PML_GE expr { $$ = ctx->node(PML_GE, 2, $1, $3); }
| expr PML_LE expr { $$ = ctx->node(PML_LE, 2, $1, $3); }
| expr PML_EQ expr { $$ = ctx->node(PML_EQ, 2, $1, $3); }
| expr PML_NE expr { $$ = ctx->node(PML_NE, 2, $1, $3); }
| expr PML_AND expr { $$ = ctx->node(PML_AND, 2, $1, $3); }
| expr PML_OR expr { $$ = ctx->node(PML_OR, 2, $1, $3); }
| expr PML_LSHIFT expr { $$ = ctx->node(PML_LSHIFT, 2, $1, $3); }
| expr PML_RSHIFT expr { $$ = ctx->node(PML_RSHIFT, 2, $1, $3); }
| PML_NEG expr { $$ = ctx->node(PML_NEG, 1, $2); }
| PML_MINUS expr %prec PML_MINUS { $$ = ctx->node(PML_MINUS, 1, $2); }
| PML_LEN '(' varref ')' { $$ = ctx->node(PML_LEN, 1, $3); }
| varref { $$ = $1; }
| PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); }
| PML_STRING {
/* Non standard promela for string literals */
$$ = ctx->value(PML_STRING, (void*)&(@1), $1); free($1); }
;
vis : /* empty */ { $$ = ctx->node(PML_SHOW, 0); }
| PML_HIDDEN { $$ = ctx->node(PML_HIDDEN, 0); }
| PML_SHOW { $$ = ctx->node(PML_SHOW, 0); }
| PML_ISLOCAL { $$ = ctx->node(PML_ISLOCAL, 0); }
;
one_decl: vis PML_TYPE var_list { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $3); free($2); }
| vis PML_UNAME var_list { $$ = ctx->node(PML_UNAME, 2, $1, $3); }
| vis PML_TYPE PML_ASGN '{' nlst '}' { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $5); free($2); }
| vis utype { $$ = $2; }
;
utype : PML_TYPEDEF PML_NAME '{' decl_lst '}' { $$ = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (void*)&(@2), $2), $4); }
;
decl_lst: one_decl { $$ = $1; }
| one_decl PML_SEMI { $$ = $1; }
| one_decl PML_SEMI decl_lst {
$$ = ctx->node(PML_DECLLIST, 1, $1);
if($3->type == PML_DECLLIST) {
$$->merge($3); delete $3;
} else {
$$->push($3);
}
}
;
var_list: ivar { $$ = ctx->node(PML_VARLIST, 1, $1); }
| ivar PML_COMMA var_list { $$ = ctx->node(PML_VARLIST, 1, $1); $$->merge($3); delete $3; }
;
ivar : vardcl { $$ = $1; }
| vardcl PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); }
;
vardcl : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); }
| PML_NAME PML_COLON PML_CONST { $$ = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (void*)&(@1), $1), ctx->value(PML_CONST, (void*)&(@3), $3)); free($1); free($3); }
| PML_NAME '[' const_expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); }
;
const_expr: PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); }
| PML_MINUS const_expr %prec PML_MINUS { $$ = ctx->node(PML_MINUS, 1, $2); }
| '(' const_expr ')' { $$ = $2; }
| const_expr PML_PLUS const_expr { $$ = ctx->node(PML_PLUS, 2, $1, $3); }
| const_expr PML_MINUS const_expr { $$ = ctx->node(PML_MINUS, 2, $1, $3); }
| const_expr PML_TIMES const_expr { $$ = ctx->node(PML_TIMES, 2, $1, $3); }
| const_expr PML_DIVIDE const_expr { $$ = ctx->node(PML_DIVIDE, 2, $1, $3); }
| const_expr PML_MODULO const_expr { $$ = ctx->node(PML_MODULO, 2, $1, $3); }
;
nlst : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); }
| nlst PML_NAME {
if ($1->type == PML_NAME) {
$$ = ctx->node(PML_NAMELIST, 1, $1);
$$->push(ctx->value(PML_NAME, (void*)&(@2), $2));
} else {
$1->push(ctx->value(PML_NAME, (void*)&(@2), $2));
}
free($2);
}
| nlst PML_COMMA { $$ = $1; }
;
stmnt_lst: stmnt { $$ = $1; }
| stmnt PML_SEMI { $$ = $1; }
| stmnt PML_SEMI stmnt_lst { $$ = ctx->node(PML_STMNT, 2, $1, $3); }
;
stmnt : Stmnt { $$ = $1; }
;
Stmnt : varref PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); }
| varref PML_INCR { $$ = ctx->node(PML_INCR, 1, $1); }
| varref PML_DECR { $$ = ctx->node(PML_DECR, 1, $1); }
| PML_PRINT '(' PML_STRING prargs ')' { $$ = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (void*)&(@3), $3), $4); free($3); }
| PML_PRINT '(' varref ')' { $$ = ctx->node(PML_PRINT, 1, $3); }
| PML_PRINT '(' PML_CONST ')' { $$ = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (void*)&(@3), $3)); free($3); }
| PML_ASSERT expr { $$ = ctx->node(PML_ASSERT, 1, $2); }
| expr { $$ = $1; }
;
prargs : /* empty */ { $$ = ctx->value(0, NULL, ""); }
| PML_COMMA arg { $$ = $2; }
;
arg : expr { $$ = $1; }
| expr PML_COMMA arg { $$ = ctx->node(0, 2, $1, $3); }
;
%%
|
