linux-kernel - [PATCH 2/2] verification/rvgen: Support the 'next' operator

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-Id: <9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de>
Date: Fri, 11 Jul 2025 15:17:38 +0200
From: Nam Cao <namcao@...utronix.de>
To: Steven Rostedt <rostedt@...dmis.org>,
	John Ogness <john.ogness@...utronix.de>,
	Masami Hiramatsu <mhiramat@...nel.org>,
	Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
	Gabriele Monaco <gmonaco@...hat.com>,
	linux-trace-kernel@...r.kernel.org,
	linux-kernel@...r.kernel.org
Cc: Nam Cao <namcao@...utronix.de>
Subject: [PATCH 2/2] verification/rvgen: Support the 'next' operator

The 'next' operator is a unary operator. It is defined as: "next time, the
operand must be true".

Support this operator. For RV monitors, "next time" means the next
invocation of ltl_validate().

Signed-off-by: Nam Cao <namcao@...utronix.de>
---
 .../trace/rv/linear_temporal_logic.rst        |  1 +
 tools/verification/rvgen/rvgen/ltl2ba.py      | 26 +++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
index 57f107fcf6dd..9eee09d9cacf 100644
--- a/Documentation/trace/rv/linear_temporal_logic.rst
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -41,6 +41,7 @@ Operands (opd):
 Unary Operators (unop):
     always
     eventually
+    next
     not
 
 Binary Operators (binop):
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index d11840af7f5f..f14e6760ac3d 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -19,6 +19,7 @@ from ply.yacc import yacc
 # Unary Operators (unop):
 #       always
 #       eventually
+#       next
 #       not
 #
 # Binary Operators (binop):
@@ -35,6 +36,7 @@ tokens = (
    'UNTIL',
    'ALWAYS',
    'EVENTUALLY',
+   'NEXT',
    'VARIABLE',
    'LITERAL',
    'NOT',
@@ -48,6 +50,7 @@ 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'
@@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp):
         # ![]F == <>(!F)
         return EventuallyOp(self.child.negate()).normalize()
 
+class NextOp(UnaryOp):
+    def normalize(self):
+        return self
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # not (next A) == next (not A)
+        self.child = self.child.negate()
+        return self
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        tmp = GraphNode(node.incoming,
+                        node.new,
+                        node.old | {n},
+                        node.next | {n.op.child})
+        return tmp.expand(node_set)
+
 class NotOp(UnaryOp):
     def __str__(self):
         return "!" + str(self.child)
@@ -452,12 +475,15 @@ 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:
-- 
2.39.5