Added support for comparison and arithmetic expressions.

We need to add support for smod to Kleaver.


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

2 files changed, 178 insertions, 137 deletions

diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index da61a8f5..0d955bf8 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -203,8 +203,8 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "?"             { return QUESTION_TOK; }
 
 
-"bit0"          { return FALSE_TOK; }
-"bit1"          { return TRUE_TOK; }
+"bit0"          { return BIT0_TOK; }
+"bit1"          { return BIT1_TOK; }
 
 "concat"        { return BVCONCAT_TOK; }
 "extract"       { return BVEXTRACT_TOK; }
@@ -236,6 +236,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "bvsdiv"        { return BVSDIV_TOK; }
 "bvsrem"        { return BVSREM_TOK; }
 "bvsmod"        { return BVSMOD_TOK; }
+
 "bvshl"         { return BVSHL_TOK; }
 "bvlshr"        { return BVLSHR_TOK; }
 "bvashr"        { return BVASHR_TOK; }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 6b7a1978..12284d89 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -97,7 +97,7 @@ int smtliberror(const char *s)
 */
 
 %type <node> an_formula an_logical_formula an_atom prop_atom
-%type <node> an_term basic_term an_fun
+%type <node> an_term basic_term an_fun an_arithmetic_fun an_pred
 %type <str> logic_name status attribute user_value annotation annotations
 
 
@@ -154,8 +154,9 @@ int smtliberror(const char *s)
 %token EOF_TOK
 %token PAT_TOK
 
-%token FALSE_TOK
-%token TRUE_TOK
+
+%token BIT0_TOK
+%token BIT1_TOK
 
 %token BVCONCAT_TOK
 %token BVEXTRACT_TOK
@@ -485,68 +486,6 @@ an_logical_formula:
     {
       $$ = EqExpr::create($3, $4);
     }
-  | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
-    {
-      $$ = Expr::createNot($3);
-    }
-  | LPAREN_TOK NOT_TOK an_formula annotations RPAREN_TOK
-    {
-      $$ = Expr::createNot($3);
-    }
-
-  | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = Expr::createImplies($3, $4);
-    }
-  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = Expr::createImplies($3, $4);
-    }
-
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK
-    {
-      $$ = SelectExpr::create($3, $4, $5);
-    }
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = SelectExpr::create($3, $4, $5);
-    }
-
-  | LPAREN_TOK AND_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = AndExpr::create($3, $4);
-    }
-  | LPAREN_TOK AND_TOK an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = AndExpr::create($3, $4);
-    }
-
-  | LPAREN_TOK OR_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = OrExpr::create($3, $4);
-    }
-  | LPAREN_TOK OR_TOK an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = OrExpr::create($3, $4);
-    }
-
-  | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = XorExpr::create($3, $4);
-    }
-  | LPAREN_TOK XOR_TOK an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = XorExpr::create($3, $4);
-    }
-
-  | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = EqExpr::create($3, $4);
-    }
-  | LPAREN_TOK IFF_TOK an_formula an_formula annotations RPAREN_TOK
-    {
-      $$ = EqExpr::create($3, $4);
-    }
 ;
 
 
@@ -604,38 +543,17 @@ an_atom:
     {
       $$ = $1;
     }
-/*
   | LPAREN_TOK prop_atom annotations RPAREN_TOK 
     {
       $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK
-    {
-      if ($4->size() == 1 && (*$4)[0] == "transclose" &&
-          $3->size() == 2) {
-        $$ = new CVC3::Expr(VC->listExpr("_TRANS_CLOSURE",
-                                        *$2, (*$3)[0], (*$3)[1]));
-      }
-      else {
-        std::vector<CVC3::Expr> tmp;
-        tmp.push_back(*$2);
-        tmp.insert(tmp.end(), $3->begin(), $3->end());
-        $$ = new CVC3::Expr(VC->listExpr(tmp));
-      }
-      delete $2;
-      delete $3;
-      delete $4;
     }
-  | LPAREN_TOK pred_symb an_terms RPAREN_TOK
+  
+  | an_pred
     {
-      std::vector<CVC3::Expr> tmp;
-      tmp.push_back(*$2);
-      tmp.insert(tmp.end(), $3->begin(), $3->end());
-      $$ = new CVC3::Expr(VC->listExpr(tmp));
-      delete $2;
-      delete $3;
+      $$ = $1;
     }
+
+/*
   | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK
     {
       $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
@@ -690,19 +608,156 @@ prop_atom:
 */
 ;  
 
-/*
-an_comparison_fun:
 
-    LPAREN_TOK IMPLIES_TOK an_term an_term RPAREN_TOK
+an_pred:
+    LPAREN_TOK BVULT_TOK an_term an_term RPAREN_TOK
     {
-      $$ = UltExpr::createImplies($3, $4);
+      $$ = UltExpr::create($3, $4);
     }
-  | LPAREN_TOK IMPLIES_TOK an_term an_term annotations RPAREN_TOK
+  | LPAREN_TOK BVULT_TOK an_term an_term annotations RPAREN_TOK
     {
-      $$ = Expr::createImplies($3, $4);
+      $$ = UltExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVULE_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = UleExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVULE_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = UleExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVUGT_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = UgtExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVUGT_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = UgtExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVUGE_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = UgeExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVUGE_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = UgeExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SltExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SltExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SleExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SleExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SgtExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SgtExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SgeExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SgeExpr::create($3, $4);
     }
 ;
-*/
+
+
+an_arithmetic_fun:
+    LPAREN_TOK BVADD_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = AddExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVADD_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = AddExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSUB_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SubExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSUB_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SubExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVMUL_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = MulExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVMUL_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = MulExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVUDIV_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = UDivExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVUDIV_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = UDivExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVUREM_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = URemExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVUREM_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = URemExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSDIV_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SDivExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSDIV_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SDivExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSREM_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = SRemExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVSREM_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = SRemExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVSMOD_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = NULL; // XXX: unsupported
+    }
+  | LPAREN_TOK BVSREM_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = NULL; // XXX: unsupported
+    }
+;
+
 
 
 an_fun:
@@ -711,48 +766,33 @@ an_fun:
       $$ = $1;
     }
 
+  | an_pred
+    {
+      $$ = $1;
+    }
+
+  | LPAREN_TOK BVCOMP_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+  | LPAREN_TOK BVCOMP_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+ 
+  | an_arithmetic_fun
+    {
+      $$ = $1;
+    }
+
 /*
-      $$ = new std::vector<CVC3::Expr>;
-      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
-        $$->push_back(VC->idExpr("_BVLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
-        $$->push_back(VC->idExpr("_BVLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
-        $$->push_back(VC->idExpr("_BVGE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
-        $$->push_back(VC->idExpr("_BVGT"));
-      }
-      else if (BVENABLED && *$1 == "bvslt") {
-        $$->push_back(VC->idExpr("_BVSLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
-        $$->push_back(VC->idExpr("_BVSLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
-        $$->push_back(VC->idExpr("_BVSGE"));
-      }
-      else if (BVENABLED && *$1 == "bvsgt") {
-        $$->push_back(VC->idExpr("_BVSGT"));
-      }
+
       else if (ARRAYSENABLED && *$1 == "select") {
         $$->push_back(VC->idExpr("_READ"));
       }
       else if (ARRAYSENABLED && *$1 == "store") {
         $$->push_back(VC->idExpr("_WRITE"));
       }
-      else if (BVENABLED && *$1 == "bit0") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(0));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "bit1") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(1));
-        $$->push_back(VC->ratExpr(1));
-      }
       else if (BVENABLED && *$1 == "concat") {
         $$->push_back(VC->idExpr("_CONCAT"));
       }
@@ -911,11 +951,11 @@ an_term:
 
 
 basic_term:
-    TRUE_TOK
+    BIT1_TOK
     {
       $$ = ConstantExpr::create(1, 1);
     }
-  | FALSE_TOK
+  | BIT0_TOK
     { 
       $$ = ConstantExpr::create(0, 1);;
     }