Added support for not, zero_extend, and sign_extend to the SMTLIB parser.

Added support for n-ary and, or and xor.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75299 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 60 insertions, 20 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 619d7ff6..d3a8c9ea 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -77,6 +77,43 @@ int SMTParser::StringToInt(const std::string& s) {
 }
 
 
+ExprHandle SMTParser::CreateAnd(std::vector<ExprHandle> kids) {
+  unsigned n_kids = kids.size();
+  assert(n_kids);
+  if (n_kids == 1)
+    return kids[0];
+
+  ExprHandle r = AndExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  for (int i=n_kids-3; i>=0; i--)
+    r = AndExpr::create(kids[i], r);
+  return r;
+}
+
+ExprHandle SMTParser::CreateOr(std::vector<ExprHandle> kids) {
+  unsigned n_kids = kids.size();
+  assert(n_kids);
+  if (n_kids == 1)
+    return kids[0];
+
+  ExprHandle r = OrExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  for (int i=n_kids-3; i>=0; i--)
+    r = OrExpr::create(kids[i], r);
+  return r;
+}
+
+ExprHandle SMTParser::CreateXor(std::vector<ExprHandle> kids) {
+  unsigned n_kids = kids.size();
+  assert(n_kids);
+  if (n_kids == 1)
+    return kids[0];
+
+  ExprHandle r = XorExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  for (int i=n_kids-3; i>=0; i--)
+    r = XorExpr::create(kids[i], r);
+  return r;
+}
+
+
 void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
   // for now, only allow variables which are multiples of 8
   if (w % 8 != 0) {
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index bae4a23f..3d64a9b2 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -60,6 +60,10 @@ class SMTParser : public klee::expr::Parser {
 
   void DeclareExpr(std::string name, Expr::Width w);
 
+  ExprHandle CreateAnd(std::vector<ExprHandle>);
+  ExprHandle CreateOr(std::vector<ExprHandle>);
+  ExprHandle CreateXor(std::vector<ExprHandle>);
+  
 
   typedef std::map<const std::string, ExprHandle> VarEnv;
   typedef std::map<const std::string, ExprHandle> FVarEnv;
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 3fef3e64..7a6485ea 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -76,6 +76,7 @@ int smtliberror(const char *s)
 %union {
   std::string *str;
   klee::expr::ExprHandle node;
+  std::vector<klee::expr::ExprHandle> *vec;
 };
 
 
@@ -98,6 +99,7 @@ int smtliberror(const char *s)
 */
 
 %type <node> an_formula an_logical_formula an_atom prop_atom
+%type <vec> an_formulas
 %type <node> an_term basic_term constant
 %type <node> an_fun an_arithmetic_fun an_bitwise_fun
 %type <node> an_pred
@@ -415,31 +417,27 @@ pred_sig:
 ;
 */
 
-/*
+
 an_formulas:
     an_formula
     {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
+      $$ = new std::vector<klee::expr::ExprHandle>;
+      $$->push_back($1);
     }
   |
     an_formulas an_formula
     {
-      $1->push_back(*$2);
+      $1->push_back($2);
       $$ = $1;
-      delete $2;
     }
 ;
-*/
 
 
 an_logical_formula:
 
     LPAREN_TOK NOT_TOK an_formula annotations
     {
-      //$$ = Expr::createNot($3);
-      $$ = NULL;
+      $$ = NotExpr::create($3);
     }
 
   | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
@@ -452,19 +450,19 @@ an_logical_formula:
       $$ = SelectExpr::create($3, $4, $5);
     }
 
-  | LPAREN_TOK AND_TOK an_formula an_formula annotations
+  | LPAREN_TOK AND_TOK an_formulas annotations
     {
-      $$ = AndExpr::create($3, $4);
+      $$ = PARSER->CreateAnd(*$3);
     }
 
-  | LPAREN_TOK OR_TOK an_formula an_formula annotations
+  | LPAREN_TOK OR_TOK an_formulas annotations
     {
-      $$ = OrExpr::create($3, $4);
+      $$ = PARSER->CreateOr(*$3);
     }
 
-  | LPAREN_TOK XOR_TOK an_formula an_formula annotations
+  | LPAREN_TOK XOR_TOK an_formulas annotations
     {
-      $$ = XorExpr::create($3, $4);
+      $$ = PARSER->CreateXor(*$3);
     }
 
   | LPAREN_TOK IFF_TOK an_formula an_formula annotations
@@ -509,6 +507,7 @@ an_formula:
 ;
 
 
+
 an_atom:
     prop_atom 
     {
@@ -674,9 +673,9 @@ an_arithmetic_fun:
 
 
 an_bitwise_fun:
-    LPAREN_TOK BVNOT_TOK an_term an_term annotations
+    LPAREN_TOK BVNOT_TOK an_term annotations
     {
-      $$ = NULL; // XXX: not supported yet
+      $$ = NotExpr::create($3);
     }
 
   | LPAREN_TOK BVAND_TOK an_term an_term annotations
@@ -695,7 +694,7 @@ an_bitwise_fun:
     }
 
   | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
-    {
+    {      
       $$ = NULL; // TODO
     }
 
@@ -726,12 +725,12 @@ an_bitwise_fun:
  
   | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
     {
-      $$ = NULL; // TODO
+      $$ = ZExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
     }
 
   | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
     {
-      $$ = NULL; // TODO
+      $$ = SExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
     }
 
   | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations