[v1] rv/rvgen: Robustness, modernization, and fixes

[PATCH 13/26] rv/rvgen: fix DOT file validation logic error

Posted by Wander Lairson Costa 2 weeks, 5 days ago

Fix incorrect boolean logic in automata DOT file format validation
that allowed malformed files to pass undetected. The previous
implementation used a logical AND operator where OR was required,
causing the validation to only reject files when both the first
token was not "digraph" AND the second token was not
"state_automaton". This meant a file starting with "digraph" but
having an incorrect second token would incorrectly pass validation.

The corrected logic properly rejects DOT files where either the
first token is not "digraph" or the second token is not
"state_automaton", ensuring that only properly formatted automaton
definition files are accepted for processing. Without this fix,
invalid DOT files could cause downstream parsing failures or
generate incorrect C code for runtime verification monitors.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 9e1c097ad0e4a..7841a6e70bad2 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -59,7 +59,7 @@ class Automata:
         # checking the first line:
         line = dot_lines[cursor].split()
 
-        if (line[0] != "digraph") and (line[1] != "state_automaton"):
+        if (line[0] != "digraph") or (line[1] != "state_automaton"):
             raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
         else:
             cursor += 1
-- 
2.52.0

Re: [PATCH 13/26] rv/rvgen: fix DOT file validation logic error

Posted by Nam Cao 2 weeks, 3 days ago

Wander Lairson Costa <wander@redhat.com> writes:

> Fix incorrect boolean logic in automata DOT file format validation
> that allowed malformed files to pass undetected. The previous
> implementation used a logical AND operator where OR was required,
> causing the validation to only reject files when both the first
> token was not "digraph" AND the second token was not
> "state_automaton". This meant a file starting with "digraph" but
> having an incorrect second token would incorrectly pass validation.
>
> The corrected logic properly rejects DOT files where either the
> first token is not "digraph" or the second token is not
> "state_automaton", ensuring that only properly formatted automaton
> definition files are accepted for processing. Without this fix,
> invalid DOT files could cause downstream parsing failures or
> generate incorrect C code for runtime verification monitors.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Reviewed-by: Nam Cao <namcao@linutronix.de>

Re: [PATCH 13/26] rv/rvgen: fix DOT file validation logic error

Posted by Gabriele Monaco 2 weeks, 5 days ago

On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Fix incorrect boolean logic in automata DOT file format validation
> that allowed malformed files to pass undetected. The previous
> implementation used a logical AND operator where OR was required,
> causing the validation to only reject files when both the first
> token was not "digraph" AND the second token was not
> "state_automaton". This meant a file starting with "digraph" but
> having an incorrect second token would incorrectly pass validation.
> 
> The corrected logic properly rejects DOT files where either the
> first token is not "digraph" or the second token is not
> "state_automaton", ensuring that only properly formatted automaton
> definition files are accepted for processing. Without this fix,
> invalid DOT files could cause downstream parsing failures or
> generate incorrect C code for runtime verification monitors.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Right, that slipped. Thanks!

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> ---
>  tools/verification/rvgen/rvgen/automata.py | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 9e1c097ad0e4a..7841a6e70bad2 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -59,7 +59,7 @@ class Automata:
>          # checking the first line:
>          line = dot_lines[cursor].split()
>  
> -        if (line[0] != "digraph") and (line[1] != "state_automaton"):
> +        if (line[0] != "digraph") or (line[1] != "state_automaton"):
>              raise AutomataError(f"Not a valid .dot format:
> {self.__dot_path}")
>          else:
>              cursor += 1