[aorai] be more strict in parsing rules to avoid conflicts

src/plugins/aorai/tests/ya/metavariables-incompatible.ya

@@ -4,6 +4,6 @@
 
 $x : int;
 
-a : { CALL(main)* } -> b;
+a : { [CALL(main)]* } -> b;
 
 b : -> b;

src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle

@@ -72,11 +72,11 @@ enum aorai_OpStatusList {
        ensures 0 ≡ S1;
      
      behavior buch_state_S2_in:
-       assumes 1 ≡ S1 ∧ 1 ≢ 0;
+       assumes 1 ≡ S1;
        ensures 1 ≡ S2;
      
      behavior buch_state_S2_out:
-       assumes 0 ≡ S1 ∨ 1 ≡ 0;
+       assumes 0 ≡ S1;
        ensures 0 ≡ S2;
      
      behavior buch_state_main_0_out:
@@ -106,7 +106,6 @@ enum aorai_OpStatusList {
 /*@ requires 1 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ main_0;
     
     behavior Buchi_property_behavior:
-      ensures 1 ≡ S2 ⇒ 1 ≢ 0;
       ensures 1 ≡ S1 ∨ 0 ≡ S1;
       ensures 1 ≡ S2 ∨ 0 ≡ S2;
       ensures 0 ≡ main_0;
@@ -186,7 +185,6 @@ int decode_int(char *s)
 
 /*@ ghost
   /@ requires (1 ≡ S1 ∨ 1 ≡ S2) ∧ 0 ≡ main_0;
-     requires 1 ≡ S1 ⇒ 1 ≢ 0;
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_factorial;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
@@ -195,11 +193,11 @@ int decode_int(char *s)
        ensures 0 ≡ S1;
      
      behavior buch_state_S2_in:
-       assumes 1 ≡ S2 ∨ (1 ≡ S1 ∧ 1 ≢ 0);
+       assumes 1 ≡ S2 ∨ 1 ≡ S1;
        ensures 1 ≡ S2;
      
      behavior buch_state_S2_out:
-       assumes 0 ≡ S2 ∧ (0 ≡ S1 ∨ 1 ≡ 0);
+       assumes 0 ≡ S2 ∧ 0 ≡ S1;
        ensures 0 ≡ S2;
      
      behavior buch_state_main_0_out:
@@ -241,11 +239,11 @@ int decode_int(char *s)
        ensures 0 ≡ S1;
      
      behavior buch_state_S2_in:
-       assumes 1 ≡ S2 ∨ (1 ≡ S1 ∧ 1 ≢ 0);
+       assumes 1 ≡ S2 ∨ 1 ≡ S1;
        ensures 1 ≡ S2;
      
      behavior buch_state_S2_out:
-       assumes 0 ≡ S2 ∧ (0 ≡ S1 ∨ 1 ≡ 0);
+       assumes 0 ≡ S2 ∧ 0 ≡ S1;
        ensures 0 ≡ S2;
      
      behavior buch_state_main_0_out:
@@ -273,7 +271,6 @@ int decode_int(char *s)
 */
 
 /*@ requires (1 ≡ S1 ∨ 1 ≡ S2) ∧ 0 ≡ main_0;
-    requires 1 ≡ S1 ⇒ 1 ≢ 0;
     requires 1 ≡ S2 ∨ 0 ≡ S2;
     requires 1 ≡ S1 ∨ 0 ≡ S1;
     requires 0 ≤ value ≤ 12;
@@ -356,11 +353,11 @@ int factorial(int value)
        ensures 0 ≡ S1;
      
      behavior buch_state_S2_in:
-       assumes 1 ≡ S1 ∧ 1 ≢ 0;
+       assumes 1 ≡ S1;
        ensures 1 ≡ S2;
      
      behavior buch_state_S2_out:
-       assumes 0 ≡ S1 ∨ 1 ≡ 0;
+       assumes 0 ≡ S1;
        ensures 0 ≡ S2;
      
      behavior buch_state_main_0_out:
@@ -392,7 +389,6 @@ int factorial(int value)
     ensures \result ≡ 0 ∨ \result ≡ 1;
     
     behavior Buchi_property_behavior:
-      ensures 1 ≡ S2 ⇒ 1 ≢ 0;
       ensures 1 ≡ S1 ∨ 0 ≡ S1;
       ensures 1 ≡ S2 ∨ 0 ≡ S2;
       ensures 0 ≡ main_0;

src/plugins/aorai/tests/ya/test_factorial.ya

@@ -5,7 +5,7 @@ main : { !CALL(factorial) } -> S1
      |                      -> S2
      ;
 S1   : { !CALL(factorial) } -> S1
-     | { 1 }                -> S2
+     | { true }                -> S2
      ;
 S2   : {!CALL(factorial) && COR(factorial) } -> S1
      | { COR(factorial) }                    -> S2

src/plugins/aorai/yaparser.mly

@@ -148,8 +148,6 @@ type pre_cond = Behavior of string | Pre of Promelaast.condition
 %token OTHERWISE
 %token EOF
 
-%left OR AND
-%nonassoc NOT
 %left STAR
 %left DOT
 %left LSQUARE
@@ -254,7 +252,6 @@ seq:
 ;
 
 guard:
-  | single_cond { to_seq $1 }
   | LSQUARE non_empty_seq RSQUARE { $2 }
   | IDENTIFIER pre_cond LPAREN seq RPAREN post_cond
       { let pre_cond =
@@ -289,15 +286,16 @@ guard:
 
 pre_cond:
   | COLUMNCOLUMN IDENTIFIER { Behavior $2 }
-  | LBRACELBRACE single_cond RBRACERBRACE { Pre $2 }
+  | LBRACELBRACE cond RBRACERBRACE { Pre $2 }
 ;
 
 post_cond:
   | /* epsilon */ { None }
-  | LBRACELBRACE single_cond RBRACERBRACE { Some $2 }
+  | LBRACELBRACE cond RBRACERBRACE { Some $2 }
 ;
 
 seq_elt:
+  | cond { to_seq $1 }
   | guard repetition {
     let min, max = $2 in
     match $1 with
@@ -321,17 +319,23 @@ repetition:
   | LCURLY arith_relation COMMA RCURLY { Some $2, None }
   | LCURLY COMMA arith_relation RCURLY { None, Some $3 }
 
-single_cond:
+cond:
+  | conjunction OR cond { POr ($1,$3) }
+  | conjunction { $1 }
+
+conjunction:
+  | atomic_cond AND conjunction { PAnd($1,$3) }
+  | atomic_cond { $1 }
+
+atomic_cond:
   | CALLORRETURN_OF  LPAREN IDENTIFIER RPAREN
       { POr (PCall ($3,None), PReturn $3) }
   | CALL_OF  LPAREN IDENTIFIER RPAREN { PCall ($3,None) }
   | RETURN_OF  LPAREN IDENTIFIER RPAREN { PReturn $3 }
   | TRUE { PTrue }
   | FALSE { PFalse }
-  | NOT single_cond { PNot $2 }
-  | single_cond AND single_cond { PAnd ($1,$3) }
-  | single_cond OR single_cond { POr ($1,$3) }
-  | LPAREN single_cond RPAREN { $2 }
+  | NOT atomic_cond { PNot $2 }
+  | LPAREN cond RPAREN { $2 }
   | logic_relation { $1 }
 ;
 
@@ -342,7 +346,7 @@ logic_relation
   | arith_relation LE arith_relation { PRel(Le, $1, $3) }
   | arith_relation GE arith_relation { PRel(Ge, $1, $3) }
   | arith_relation NEQ arith_relation { PRel(Neq, $1, $3) }
-  | arith_relation { PRel (Neq, $1, PCst(IntConstant "0")) }
+/*  | arith_relation { PRel (Neq, $1, PCst(IntConstant "0")) } */
   ;
 
 arith_relation
@@ -352,9 +356,9 @@ arith_relation
   ;
 
 arith_relation_mul
-  : arith_relation_mul SLASH access_or_const { PBinop(Bdiv,$1,$3) }
-  | arith_relation_mul STAR access_or_const { PBinop(Bmul, $1, $3) }
-  | arith_relation_mul PERCENT access_or_const { PBinop(Bmod, $1, $3) }
+  : arith_relation_mul SLASH arith_relation_bw { PBinop(Bdiv,$1,$3) }
+  | arith_relation_mul STAR arith_relation_bw { PBinop(Bmul, $1, $3) }
+  | arith_relation_mul PERCENT arith_relation_bw { PBinop(Bmod, $1, $3) }
   | arith_relation_bw { $1 }
   ;
 
@@ -382,7 +386,7 @@ access_leaf
   : STAR access { PUnop (Ustar,$2) }
   | IDENTIFIER LPAREN RPAREN DOT IDENTIFIER { PPrm($1,$5) }
   | IDENTIFIER { PVar $1 }
-  | LPAREN access RPAREN { $2 }
+  | LPAREN arith_relation RPAREN { $2 }
   | METAVAR { PMetavar $1 }
   ;