diff options
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 22 | ||||
| -rw-r--r-- | lib/SMT/SMTParser.h | 2 | ||||
| -rw-r--r-- | lib/SMT/smtlib.lex | 2 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 32 |
4 files changed, 43 insertions, 15 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 6e40978a..619d7ff6 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -77,6 +77,28 @@ int SMTParser::StringToInt(const std::string& s) { } +void SMTParser::DeclareExpr(std::string name, Expr::Width w) { + // for now, only allow variables which are multiples of 8 + if (w % 8 != 0) { + cout << "BitVec not multiple of 8 (" << w << "). Need to update code.\n"; + exit(1); + } + + std::cout << "Declaring " << name << " of width " << w << "\n"; + + Array *arr = new Array(name, w / 8); + + ref<Expr> *kids = new ref<Expr>[w/8]; + for (unsigned i=0; i < w/8; i++) + kids[i] = ReadExpr::create(UpdateList(arr, NULL), + ConstantExpr::create(i, 32)); + ref<Expr> var = ConcatExpr::createN(w/8, kids); + delete [] kids; + + AddVar(name, var); +} + + ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) { cerr << "In GetConstExpr(): val=" << val << ", base=" << (unsigned)base << ", width=" << w << "\n"; assert(base == 2 || base == 10 || base == 16); diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index 1e24122f..bae4a23f 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -58,6 +58,8 @@ class SMTParser : public klee::expr::Parser { int StringToInt(const std::string& s); ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w); + void DeclareExpr(std::string name, Expr::Width w); + typedef std::map<const std::string, ExprHandle> VarEnv; typedef std::map<const std::string, ExprHandle> FVarEnv; diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex index f5633716..c614c683 100644 --- a/lib/SMT/smtlib.lex +++ b/lib/SMT/smtlib.lex @@ -154,6 +154,8 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) SMTParser::parserTemp->lineNum++; } <USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smtlibtext); } +"BitVec" { return BITVEC_TOK; } + "true" { return TRUE_TOK; } "false" { return FALSE_TOK; } "ite" { return ITE_TOK; } diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index febf76cd..3fef3e64 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -102,7 +102,7 @@ int smtliberror(const char *s) %type <node> an_fun an_arithmetic_fun an_bitwise_fun %type <node> an_pred %type <str> logic_name status attribute user_value annotation annotations -%type <str> var fvar +%type <str> var fvar symb %token <str> NUMERAL_TOK %token <str> SYM_TOK @@ -114,6 +114,8 @@ int smtliberror(const char *s) %token <str> BVBIN_TOK %token <str> BVHEX_TOK +%token BITVEC_TOK + %token TRUE_TOK %token FALSE_TOK %token ITE_TOK @@ -264,12 +266,13 @@ bench_attribute: { // XXX? } +*/ - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK + | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK { - //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); - //delete $4; + PARSER->DeclareExpr(*$5, atoi($8->c_str())); } +/* | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); @@ -435,7 +438,8 @@ an_logical_formula: LPAREN_TOK NOT_TOK an_formula annotations { - $$ = Expr::createNot($3); + //$$ = Expr::createNot($3); + $$ = NULL; } | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations @@ -843,18 +847,11 @@ basic_term: { $$ = PARSER->GetVar(*$1); } -/* - | fun_symb + | symb { - if ($1->size() == 1) { - $$ = new CVC3::Expr(((*$1)[0])); - } - else { - $$ = new CVC3::Expr(VC->listExpr(*$1)); - } - delete $1; + std::cout << "SYMBOL " << *$1 << "\n"; + $$ = PARSER->GetVar(*$1); } -*/ ; @@ -966,5 +963,10 @@ fvar: } ; +symb: + SYM_TOK + { + $$ = $1; + } %% |