From: Gabriele Monaco <gmonaco@redhat.com>
To: Nam Cao <namcao@linutronix.de>
Cc: Steven Rostedt <rostedt@goodmis.org>,
Wander Lairson Costa <wander@redhat.com>,
linux-trace-kernel@vger.kernel.org,
linux-kernel@vger.kernel.org
Subject: Re: [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark
Date: Wed, 06 May 2026 16:48:17 +0200 [thread overview]
Message-ID: <dba16e4fe794c5aa237f3360fef5fc22ae32c60b.camel@redhat.com> (raw)
In-Reply-To: <361efb610ba7c06b3668a953a6847ea80453c2e3.1777962130.git.namcao@linutronix.de>
Looks good, although I need to put more effort to understand the grammar.
There's an issue parsing events though:
> +class EventLabelParser:
> + grammar = r'''
> + events: event ("\\n" event)*
> +
> + event: name (";" guard)*
> +
> + guard: reset
> + | rule
> + | rule reset
> + | reset rule
> +
> + name: CNAME
> +
> + reset: "reset" "(" ENV ")"
> +
> + %import common.CNAME
> + %import common.WS
> + %ignore WS
> + ''' + ConstraintRule.grammar
> +
> + class GetEvents(lark.visitors.Transformer):
> + def guard(self, args):
> + reset = None
> + rule = None
> + for arg in args:
> + if arg.data == "reset":
> + reset = ConstraintReset(arg.children[0])
> + elif arg.data == "rule":
> + conditions = arg.children
> + rule = ConstraintRule(conditions[0])
> + for i in range(1, len(conditions), 2):
> + rule.chain(conditions[i], conditions[i + 1])
> + return reset, rule
> +
> + def OP(self, args):
> + return args
> +
> + def condition(self, args):
> + return ConstraintCondition(*args)
> +
> + def event(self, args):
> + name = args[0]
> + rule, reset = None, None
> + if len(args) == 2:
> + reset, rule = args[1]
> + return name, reset, rule
I'm not sure if it could be solved better changing the grammar, but this doesn't
work in case we have both a reset and a rule, e.g.:
"event2;env1 == 0;reset(clk)"
It apparently saves only one of them, the other would end up in args[2].
Doing this seems to fix:
diff --git a/tools/verification/rvgen/rvgen/automata.py
b/tools/verification/rvgen/rvgen/automata.py
index cc42b8127fc0..10534f956cc3 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -314,8 +314,11 @@ class EventLabelParser:
def event(self, args):
name = args[0]
rule, reset = None, None
- if len(args) == 2:
- reset, rule = args[1]
+ for _reset, _rule in args[1:]:
+ if _reset:
+ reset = _reset
+ if _rule:
+ rule = _rule
return name, reset, rule
def events(self, args):
Thanks,
Gabriele
next prev parent reply other threads:[~2026-05-06 14:48 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
2026-05-05 6:59 ` [PATCH 01/13] verification/rvgen: Switch LTL parser " Nam Cao
2026-05-06 7:37 ` Gabriele Monaco
2026-05-05 6:59 ` [PATCH 02/13] verification/rvgen: Introduce a parse tree for automata using Lark Nam Cao
2026-05-05 6:59 ` [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark Nam Cao
2026-05-06 14:48 ` Gabriele Monaco [this message]
2026-05-05 6:59 ` [PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark Nam Cao
2026-05-05 6:59 ` [PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() " Nam Cao
2026-05-05 6:59 ` [PATCH 06/13] verification/rvgen: Convert __fill_verify_guards_func() " Nam Cao
2026-05-06 14:51 ` Gabriele Monaco
2026-05-05 6:59 ` [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables Nam Cao
2026-05-06 9:15 ` Gabriele Monaco
2026-05-05 6:59 ` [PATCH 08/13] verification/rvgen: Simplify the generation for " Nam Cao
2026-05-05 6:59 ` [PATCH 09/13] verification/rvgen: Delete __parse_constraint() Nam Cao
2026-05-05 6:59 ` [PATCH 10/13] verification/rvgen: Switch __get_event_variables() to Lark Nam Cao
2026-05-05 6:59 ` [PATCH 11/13] verification/rvgen: Switch __create_matrix() " Nam Cao
2026-05-05 6:59 ` [PATCH 12/13] verification/rvgen: Remove the old state variables Nam Cao
2026-05-05 6:59 ` [PATCH 13/13] verification/rvgen: Remove dead code Nam Cao
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=dba16e4fe794c5aa237f3360fef5fc22ae32c60b.camel@redhat.com \
--to=gmonaco@redhat.com \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-trace-kernel@vger.kernel.org \
--cc=namcao@linutronix.de \
--cc=rostedt@goodmis.org \
--cc=wander@redhat.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox