diff options
Diffstat (limited to 'src/uscxml/plugins/datamodel/promela/parser/promela.ypp')
-rw-r--r-- | src/uscxml/plugins/datamodel/promela/parser/promela.ypp | 254 |
1 files changed, 254 insertions, 0 deletions
diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.ypp b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp new file mode 100644 index 0000000..d76b24a --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp @@ -0,0 +1,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 + +%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; + } + | expr { + ctx->ast = $1; + ctx->type = PromelaParser::PROMELA_EXPR; + } + | stmnt_lst { + ctx->ast = $1; + ctx->type = PromelaParser::PROMELA_STMNT; + } + ; + +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); } + ; + + +%% + |