public inbox for linux-kernel@vger.kernel.org
 help / color / mirror / Atom feed
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

  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