diff options
Diffstat (limited to 'stp/parser/PL.lex')
| -rw-r--r-- | stp/parser/PL.lex | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/stp/parser/PL.lex b/stp/parser/PL.lex new file mode 100644 index 00000000..e9358a0e --- /dev/null +++ b/stp/parser/PL.lex @@ -0,0 +1,128 @@ +%{ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#include <iostream> +#include "../AST/AST.h" +#include "parsePL_defs.h" + +extern char *yytext; +extern int yyerror (const char *msg); +%} + +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%x COMMENT +%x STRING_LITERAL +LETTER ([a-zA-Z]) +HEX ([0-9a-fA-F]) +BITS ([0-1]) +DIGIT ([0-9]) +OPCHAR (['?\_$]) +ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) +%% + +[()[\]{},.;:'!#?_=] { return yytext[0];} + +[\n] { /*Skip new line */ } +[ \t\r\f] { /* skip whitespace */ } +0b{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} +0bin{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} +0h{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} +0hex{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} +{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} + +"%" { BEGIN COMMENT;} +<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */} +<COMMENT>. { /* stay in comment mode */} + +"ARRAY" { return ARRAY_TOK; } +"OF" { return OF_TOK; } +"WITH" { return WITH_TOK; } +"AND" { return AND_TOK;} +"NAND" { return NAND_TOK;} +"NOR" { return NOR_TOK;} +"NOT" { return NOT_TOK; } +"OR" { return OR_TOK; } +"/=" { return NEQ_TOK; } + ":=" { return ASSIGN_TOK;} +"=>" { return IMPLIES_TOK; } +"<=>" { return IFF_TOK; } +"XOR" { return XOR_TOK; } +"IF" { return IF_TOK; } +"THEN" { return THEN_TOK; } +"ELSE" { return ELSE_TOK; } +"ELSIF" { return ELSIF_TOK; } +"END" { return END_TOK; } +"ENDIF" { return ENDIF_TOK; } +"BV" { return BV_TOK;} +"BITVECTOR" { return BV_TOK;} +"BOOLEAN" { return BOOLEAN_TOK;} +"<<" { return BVLEFTSHIFT_TOK;} +">>" { return BVRIGHTSHIFT_TOK;} +"BVPLUS" { return BVPLUS_TOK;} +"BVSUB" { return BVSUB_TOK;} +"BVUMINUS" { return BVUMINUS_TOK;} +"BVMULT" { return BVMULT_TOK;} +"BVDIV" { return BVDIV_TOK;} +"BVMOD" { return BVMOD_TOK;} +"SBVDIV" { return SBVDIV_TOK;} +"SBVMOD" { return SBVMOD_TOK;} +"~" { return BVNEG_TOK;} +"&" { return BVAND_TOK;} +"|" { return BVOR_TOK;} +"BVXOR" { return BVXOR_TOK;} +"BVNAND" { return BVNAND_TOK;} +"BVNOR" { return BVNOR_TOK;} +"BVXNOR" { return BVXNOR_TOK;} +"@" { return BVCONCAT_TOK;} +"BVLT" { return BVLT_TOK;} +"BVGT" { return BVGT_TOK;} +"BVLE" { return BVLE_TOK;} +"BVGE" { return BVGE_TOK;} +"BVSLT" { return BVSLT_TOK;} +"BVSGT" { return BVSGT_TOK;} +"BVSLE" { return BVSLE_TOK;} +"BVSGE" { return BVSGE_TOK;} +"BVSX" { return BVSX_TOK;} +"SBVLT" { return BVSLT_TOK;} +"SBVGT" { return BVSGT_TOK;} +"SBVLE" { return BVSLE_TOK;} +"SBVGE" { return BVSGE_TOK;} +"SX" { return BVSX_TOK;} +"BOOLEXTRACT" { return BOOLEXTRACT_TOK;} +"BOOLBV" { return BOOL_TO_BV_TOK;} +"ASSERT" { return ASSERT_TOK; } +"QUERY" { return QUERY_TOK; } +"FALSE" { return FALSELIT_TOK;} +"TRUE" { return TRUELIT_TOK;} +"IN" { return IN_TOK;} +"LET" { return LET_TOK;} +"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK;} +"COUNTERMODEL" { return COUNTEREXAMPLE_TOK;} + "PUSH" { return PUSH_TOK;} + "POP" { return POP_TOK;} + +(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { + BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); + + // Check valuesize to see if it's a prop var. I don't like doing + // type determination in the lexer, but it's easier than rewriting + // the whole grammar to eliminate the term/formula distinction. + yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + //yylval.node = new BEEV::ASTNode(nptr); + if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; +} + +. { yyerror("Illegal input character."); } +%% |