[PATCH v2 01/13] verification/rvgen: Switch LTL parser to Lark

[Nam Cao]

The LTL parser is built using Ply. However, Ply is no longer
maintained [1].

Switch to use Lark instead. In addition to being actively maintained, Lark
also offers additional features (namely, automatically creating the
abstract syntax tree) which make the parser simpler.

Link: https://github.com/dabeaz/ply/commit/9d7c40099e23ff78f9d86ef69a26c1e8a83e706a [1]
Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
---
v2:
  - fix identifier starting with a digit is allowed [Wander]
  - fixup ast node uid [Gabriele]
  - Fix up Literal AST node construction [Wander, Sashiko]
  - FIx up unary op error message [Sashiko]
  - Add nice exception handling [Gabriele]
---
 tools/verification/rvgen/__main__.py     |   5 +-
 tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++--------------
 2 files changed, 82 insertions(+), 125 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5c923dc10d0f..0915cf86e43b 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -14,6 +14,7 @@ if __name__ == '__main__':
     from rvgen.container import Container
     from rvgen.ltl2k import ltl2k
     from rvgen.automata import AutomataError
+    from rvgen.ltl2ba import LTLError
     import argparse
     import sys
 
@@ -57,8 +58,8 @@ if __name__ == '__main__':
                 sys.exit(1)
         else:
             monitor = Container(vars(params))
-    except AutomataError as e:
-        print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
+    except (AutomataError, LTLError) as e:
+        print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
         sys.exit(1)
 
     print(f"Writing the monitor into the directory {monitor.name}")
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 016e7cf93bbb..7cebda61bce8 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,9 +7,7 @@
 # https://doi.org/10.1007/978-0-387-34892-6_1
 # With extra optimizations
 
-from ply.lex import lex
-from ply.yacc import yacc
-from .automata import AutomataError
+import lark
 
 # Grammar:
 # 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
 #       imply
 #       equivalent
 
-tokens = (
-   'AND',
-   'OR',
-   'IMPLY',
-   'UNTIL',
-   'ALWAYS',
-   'EVENTUALLY',
-   'NEXT',
-   'VARIABLE',
-   'LITERAL',
-   'NOT',
-   'LPAREN',
-   'RPAREN',
-   'ASSIGN',
-)
-
-t_AND = r'and'
-t_OR = r'or'
-t_IMPLY = r'imply'
-t_UNTIL = r'until'
-t_ALWAYS = r'always'
-t_NEXT = r'next'
-t_EVENTUALLY = r'eventually'
-t_VARIABLE = r'[A-Z_0-9]+'
-t_LITERAL = r'true|false'
-t_NOT = r'not'
-t_LPAREN = r'\('
-t_RPAREN = r'\)'
-t_ASSIGN = r'='
-t_ignore_COMMENT = r'\#.*'
-t_ignore = ' \t\n'
-
-def t_error(t):
-    raise AutomataError(f"Illegal character '{t.value[0]}'")
-
-lexer = lex()
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+     | LITERAL
+     | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+     | "eventually"
+     | "next"
+     | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+      | "and"
+      | "or"
+      | "imply"
+
+VARIABLE: /[A-Z_][A-Z0-9_]*/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
+
+class LTLError(Exception):
+    "Exception raised for malformed linear temporal logic"
 
 class GraphNode:
     uid = 0
@@ -97,7 +94,7 @@ class GraphNode:
         return self.id < other.id
 
 class ASTNode:
-    uid = 1
+    uid = 0
 
     def __init__(self, op):
         self.op = op
@@ -433,90 +430,49 @@ class Literal:
         node.old |= {n}
         return node.expand(node_set)
 
-def p_spec(p):
-    '''
-    spec : assign
-         | assign spec
-    '''
-    if len(p) == 3:
-        p[2].append(p[1])
-        p[0] = p[2]
-    else:
-        p[0] = [p[1]]
-
-def p_assign(p):
-    '''
-    assign : VARIABLE ASSIGN ltl
-    '''
-    p[0] = (p[1], p[3])
-
-def p_ltl(p):
-    '''
-    ltl : opd
-        | binop
-        | unop
-    '''
-    p[0] = p[1]
-
-def p_opd(p):
-    '''
-    opd : VARIABLE
-        | LITERAL
-        | LPAREN ltl RPAREN
-    '''
-    if p[1] == "true":
-        p[0] = ASTNode(Literal(True))
-    elif p[1] == "false":
-        p[0] = ASTNode(Literal(False))
-    elif p[1] == '(':
-        p[0] = p[2]
-    else:
-        p[0] = ASTNode(Variable(p[1]))
-
-def p_unop(p):
-    '''
-    unop : ALWAYS ltl
-         | EVENTUALLY ltl
-         | NEXT ltl
-         | NOT ltl
-    '''
-    if p[1] == "always":
-        op = AlwaysOp(p[2])
-    elif p[1] == "eventually":
-        op = EventuallyOp(p[2])
-    elif p[1] == "next":
-        op = NextOp(p[2])
-    elif p[1] == "not":
-        op = NotOp(p[2])
-    else:
-        raise AutomataError(f"Invalid unary operator {p[1]}")
-
-    p[0] = ASTNode(op)
-
-def p_binop(p):
-    '''
-    binop : opd UNTIL ltl
-          | opd AND ltl
-          | opd OR ltl
-          | opd IMPLY ltl
-    '''
-    if p[2] == "and":
-        op = AndOp(p[1], p[3])
-    elif p[2] == "until":
-        op = UntilOp(p[1], p[3])
-    elif p[2] == "or":
-        op = OrOp(p[1], p[3])
-    elif p[2] == "imply":
-        op = ImplyOp(p[1], p[3])
-    else:
-        raise AutomataError(f"Invalid binary operator {p[2]}")
-
-    p[0] = ASTNode(op)
-
-parser = yacc()
+class Transform(lark.visitors.Transformer):
+    def unop(self, node):
+        if node[0] == "always":
+            return ASTNode(AlwaysOp(node[1]))
+        if node[0] == "eventually":
+            return ASTNode(EventuallyOp(node[1]))
+        if node[0] == "next":
+            return ASTNode(NextOp(node[1]))
+        if node[0] == "not":
+            return ASTNode(NotOp(node[1]))
+        raise ValueError("Unknown operator %s" % node[0])
+
+    def binop(self, node):
+        if node[1] == "until":
+            return ASTNode(UntilOp(node[0], node[2]))
+        if node[1] == "and":
+            return ASTNode(AndOp(node[0], node[2]))
+        if node[1] == "or":
+            return ASTNode(OrOp(node[0], node[2]))
+        if node[1] == "imply":
+            return ASTNode(ImplyOp(node[0], node[2]))
+        raise ValueError("Unknown operator %s" % node[1])
+
+    def VARIABLE(self, args):
+        return ASTNode(Variable(args))
+
+    def LITERAL(self, args):
+        return ASTNode(Literal(args == "true"))
+
+    def start(self, node):
+        return node
+
+    def assign(self, node):
+        return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
 
 def parse_ltl(s: str) -> ASTNode:
-    spec = parser.parse(s)
+    try:
+        spec = parser.parse(s)
+    except lark.exceptions.UnexpectedInput as e:
+        raise LTLError(str(e))
+    spec = Transform().transform(spec)
 
     rule = None
     subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
             subexpr[assign[0]] = assign[1]
 
     if rule is None:
-        raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
+        raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
 
     for node in rule:
         if not isinstance(node.op, Variable):
-- 
2.47.3