[PATCH 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>
---
 tools/verification/rvgen/rvgen/ltl2ba.py | 189 +++++++++--------------
 1 file changed, 70 insertions(+), 119 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 7f538598a868..b2dee2dbe257 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,8 +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
+import lark
 from .automata import AutomataError
 
 # Grammar:
@@ -30,42 +29,38 @@ 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_0-9]+/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
 
 class GraphNode:
     uid = 0
@@ -432,90 +427,46 @@ 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[1])
+
+    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(Variable(args))
+
+    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)
+    spec = Transform().transform(spec)
 
     rule = None
     subexpr = {}
-- 
2.47.3