Merge pull request #1382 from diffblue/smv-operator-precedence

SMV: use NuSMV's operator precedence

Author: tautschnig

CHANGELOG

@@ -3,6 +3,8 @@
 
 * SMV: removed legacy keywords EXTERN and switch
 
+* SMV: use NuSMV's operator precedence, as opposed to CMU SMV's
+
 # EBMC 5.11
 
 * SystemVerilog: $unit::

regression/ebmc/smv-netlist/assignment.desc

@@ -1,7 +1,7 @@
 CORE
 assignment.sv
 --smv-netlist --simple-netlist
-^LTLSPEC G \(\!nondet\[5\]\)$
+^LTLSPEC G \!nondet\[5\]$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-netlist/s_until1.desc

@@ -1,7 +1,7 @@
 CORE
 s_until1.sv
 --smv-netlist
-^LTLSPEC \(\!node144\) U node51$
+^LTLSPEC \!node144 U node51$
 ^LTLSPEC TRUE U node151$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/smv-word-level/smv1.desc

@@ -10,7 +10,7 @@ smv1.smv
 ^INIT range_type = 1$
 ^INIT signed_bit_vector = 0sd20_1$
 ^INIT unsigned_bit_vector = 0ud20_1$
-^TRANS next\(bool_type\) = \(!bool_type\)$
+^TRANS next\(bool_type\) = !bool_type$
 ^TRANS next\(range_type\) = 2$
 ^TRANS next\(signed_bit_vector\) = 0sd20_2$
 ^TRANS next\(unsigned_bit_vector\) = 0ud20_2$

regression/smv/word/bitwise1.desc

@@ -1,8 +1,8 @@
 CORE
 bitwise1.smv
 
-^\[.*\] \(!0ud8_123\) = 0ud8_132: PROVED .*$
-^\[.*\] \(!0sd8_123\) = -0sd8_124: PROVED .*$
+^\[.*\] !0ud8_123 = 0ud8_132: PROVED .*$
+^\[.*\] !0sd8_123 = -0sd8_124: PROVED .*$
 ^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED .*$
 ^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED .*$
 ^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED .*$

regression/smv/word/bitwise1.smv

@@ -1,8 +1,8 @@
 MODULE main
 
 -- negation
-SPEC (!uwconst(123, 8)) = uwconst(132, 8)
-SPEC (!swconst(123, 8)) = swconst(-124, 8)
+SPEC !uwconst(123, 8) = uwconst(132, 8)
+SPEC !swconst(123, 8) = swconst(-124, 8)
 
 -- and
 SPEC (uwconst(123, 8) & uwconst(7, 8)) = uwconst(3, 8)

regression/smv/word/bitwise_not1.desc

@@ -2,8 +2,8 @@ CORE
 bitwise_not1.smv
 
 ^\[spec1\] !\(0ud2_1 = 0ud2_3\): PROVED.*$
-^\[spec2\] \(!0ud2_1\) = 0ud2_3: REFUTED.*$
-^\[spec3\] !\(0ud2_1 = 0ud2_3\): PROVED.*$
+^\[spec2\] !0ud2_1 = 0ud2_3: REFUTED.*$
+^\[spec3\] !0ud2_1 = 0ud2_3: REFUTED.*$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/smv/word/bitwise_not2.desc

@@ -1,10 +1,10 @@
 CORE
 bitwise_not2.smv
 
-^\[spec1\] \(!\(0ud1_1 :: 0ud1_1\)\) = 0ud2_1: REFUTED$
+^\[spec1\] !\(0ud1_1 :: 0ud1_1\) = 0ud2_1: REFUTED$
 ^\[spec2\] \(!0ud1_1\) :: 0ud1_1 = 0ud2_1: PROVED .*$
-^\[spec3\] \(!\(0ud1_1 :: 0ud1_1\)\) = 0ud2_1: REFUTED$
-^\[spec4\] !\(0ud1_1 :: 0ud1_1 = 0ud2_1\): PROVED .*$
+^\[spec3\] \(!0ud1_1\) :: 0ud1_1 = 0ud2_1: PROVED .*$
+^\[spec4\] \(!0ud1_1\) :: 0ud1_1 = 0ud2_1: PROVED .*$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/smvlang/expr2smv_class.h

@@ -40,24 +40,24 @@ class expr2smvt
 
   // In NuSMV 2.6., ! (not)  has a high precedence (above ::), whereas
   // in the CMU SMV implementation it has the same as other boolean operators.
-  // We use the CMU SMV precedence for !.
+  // We use the NuSMV precedence for !.
   // Like CMU SMV, we give the same precedence to -> and <->, to avoid ambiguity.
   // Note that the precedence of mod in the CMU SMV differs from NuSMV's.
   // We use NuSMV's.
   enum class precedencet
   {
     MAX = 16,
     INDEX = 15,   // [ ] , [ : ]
-    CONCAT = 14,  // ::
+    NOT = 14,     // !
     UMINUS = 13,  // - (unary minus)
-    MULT = 12,    // * / mod
-    PLUS = 11,    // + -
-    SHIFT = 10,   // << >>
-    UNION = 9,    // union
-    IN = 8,       // in
-    REL = 7,      // = != < > <= >=
-    TEMPORAL = 6, // AX, AF, etc.
-    NOT = 5,      // !
+    CONCAT = 12,  // ::
+    MULT = 11,    // * / mod
+    PLUS = 10,    // + -
+    SHIFT = 9,    // << >>
+    UNION = 8,    // union
+    IN = 7,       // in
+    REL = 6,      // = != < > <= >=
+    TEMPORAL = 5, // AX, AF, etc.
     AND = 4,      // &
     OR = 3,       // | xor xnor
     IF = 2,       // (• ? • : •)
@@ -79,6 +79,26 @@ class expr2smvt
     -> <->
   */
 
+  /* From https://nusmv.fbk.eu/userman/v27/nusmv.pdf
+
+  The order of parsing precedence for operators from high to low is:
+    [ ] , [ : ]
+    !
+    - (unary minus)
+    ::
+    * / mod
+    + -
+    << >>
+    union
+    in
+    = != < > <= >=
+    &
+    | xor xnor
+    (• ? • : •)
+    <->
+    ->
+  */
+
   struct resultt
   {
     resultt(precedencet _p, std::string _s) : p(_p), s(std::move(_s))

src/smvlang/parser.y

@@ -288,21 +288,19 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_n
 %right IMPLIES_Token
 %left  EQUIV_Token
 %left  IF_Token
-%left  xor_Token xnor_Token
-%left  OR_Token
+%left  OR_Token xor_Token xnor_Token
 %left  AND_Token
-%left  NOT_Token
 %left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token H_Token O_Token S_Token T_Token X_Token Y_Token Z_Token EBF_Token ABF_Token EBG_Token ABG_Token
 %left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
 %left  union_Token
 %left  in_Token
 %left  DOTDOT_Token /* precedence not documented */
-%left  mod_Token /* Precedence from CMU SMV, different from NuSMV */
 %left  LTLT_Token GTGT_Token
 %left  PLUS_Token MINUS_Token
-%left  TIMES_Token DIVIDE_Token
+%left  TIMES_Token DIVIDE_Token mod_Token /* mod precedence from NuSMV, different from CMU SMV */
 %left  COLONCOLON_Token
 %left  UMINUS           /* supplies precedence for unary minus */
+%left  NOT_Token /* precedence from NuSMV, different from CMU SMV */
 %left  DOT_Token '[' '('
 
 %%