Re: [RFC PATCH 10/17] verification/rvgen: Add support for Hybrid Automata

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2025-08-25 at 11:55 +0200, Nam Cao wrote:
> On Thu, Aug 14, 2025 at 05:08:02PM +0200, Gabriele Monaco wrote:
> >                  for i in event.split("\\n"):
> > +                    if ";" in i:
> > +                        # if the event contains a constraint
> > (hybrid automata),
> > +                        # it will be separated by a ";":
> > +                        # "sched_switch;x<1000;reset(x)"
> > +                        line = i.split(";")
> > +                        i = line.pop(0)
> > +                        if len(line) > 2:
> > +                            raise ValueError("Only 1 constraint
> > and 1 reset are supported")
> > +                        envs += self.__extract_env_var(line)
> >                      events.append(i)
> 
> How about we get rid of the (if ";"), and just split it:
> 
> for i in event.split("\\n"):
>     # if the event contains a constraint (hybrid automata),
>     # it will be separated by a ";":
>     # "sched_switch;x<1000;reset(x)"
>     line = i.split(";")
>     events.append(line.pop(0))
>     if len(line) > 2:
>             raise ValueError("Only 1 constraint and 1 reset are
> supported")
>         envs += self.__extract_env_var(line)
> 

Right, that's neater, thanks.

> > +            else:
> > +                # state labels have the format:
> > +                # "enable_fired" [label =
> > "enable_fired\ncondition"];
> > +                #  ----- label is here -----^^^^^
> > +                # label and node name must be the same, condition
> > is optional
> > +                state =
> > self.__dot_lines[cursor].split("label")[1].split('"')[1]
> 
> I know I complained about regex last week, but for this case I think
> regex is more suitable:
> 
> state = re.findall(r'".*?" \[label = "([^"]*)"\]',
> self.__dot_lines[cursor])[0]
> 

Yeah I guess I opened the pandora box already..
Also thinking about the ply parser, it'd probably end up relying on
regex too.
I may just set up the things in this patch (use regex where too complex
without) and re-evaluate the whole things with ply later on.

> > +                if "\\n" in state:
> > +                    line = state.split("\\n")
> > +                    line.pop(0)
> > +                    if len(line) > 1:
> > +                        raise ValueError("Only 1 constraint is
> > supported in the state")
> > +                    envs +=
> > self.__extract_env_var([line[0].replace(" ", "")])
> 
> Same as above, I think we can just split without the if check.
> 
> >              cursor += 1
> >  
> > -        return sorted(set(events))
> > -
> > -    def __create_matrix(self):
> > +        return sorted(set(events)), sorted(set(envs))
> > +
> > +    def _split_constraint_expr(self, constr: list[str]) ->
> > Iterator[tuple[str,
> > +                                                                  
> >         str | None]]:
> > +        """
> > +        Get a list of strings of the type constr1 && constr2 and
> > returns a list of
> > +        constraints and separators:
> > [[constr1,"&&"],[constr2,None]]
> > +        """
> > +        exprs = []
> > +        seps = []
> > +        for c in constr:
> > +            while "&&" in c or "||" in c:
> > +                a = c.find("&&")
> > +                o = c.find("||")
> > +                pos = a if o < 0 or 0 < a < o else o
> > +                exprs.append(c[:pos].replace(" ", ""))
> > +                seps.append(c[pos:pos+2].replace(" ", ""))
> > +                c = c[pos+2:].replace(" ", "")
> > +            exprs.append(c)
> > +            seps.append(None)
> > +        return zip(exprs, seps)
> 
> If && and || are the only things you intend to support, then this is
> probably okay. But if the syntax will ever be extended (e.g.
> brackets),
> this becomes unreadable really fast.
> 
> Perhaps a "real" parser which converts the input string into abstract
> syntax tree is something worth considering.

Yeah totally, I'm going to stick to the "simple" syntax for now and
then rewrite the whole thing with a proper parser.

> 
> > +    def is_event_constraint(self, key: tuple[int, int] | int) ->
> > bool:
> > +        """
> > +        Given the key in self.constraints return true if it is an
> > event
> > +        constraint, false if it is a state constraint
> > +        """
> > +        return isinstance(key, tuple)
> 
> I don't love this. A few years from now, someone could change state
> constraint to be a tuple, or change event contraint to not be tuple,
> and things break in confusing ways.
> 
> Perhaps an explicit variable to store contraint type information
> instead?

Mmh good point, I'll look into that.

> 
> > -    def __get_enum_states_content(self):
> > +    def __get_enum_states_content(self) -> list[str]:
> >          buff = []
> >          buff.append("\t%s%s = 0," % (self.initial_state,
> > self.enum_suffix))
> >          for state in self.states:
> > @@ -36,7 +37,7 @@ class Dot2c(Automata):
> >  
> >          return buff
> >  
> > -    def format_states_enum(self):
> > +    def format_states_enum(self) -> list[str]:
> >          buff = []
> >          buff.append("enum %s {" % self.enum_states_def)
> >          buff += self.__get_enum_states_content()
> > @@ -58,7 +59,7 @@ class Dot2c(Automata):
> >  
> >          return buff
> >  
> > -    def format_events_enum(self):
> > +    def format_events_enum(self) -> list[str]:
> 
> These changes should be in your type annotation patch?

Right, probably coming from yet another rebase, having a look.

> 
> >          buff = []
> >          buff.append("enum %s {" % self.enum_events_def)
> >          buff += self.__get_enum_events_content()
> > @@ -66,7 +67,43 @@ class Dot2c(Automata):
> >  
> >          return buff
> >  
> > -    def get_minimun_type(self):
> > +    def __get_non_stored_envs(self) -> list[str]:
> > +        return [ e for e in self.envs if e not in self.env_stored
> > ]
> > +
> > +    def __get_enum_envs_content(self) -> list[str]:
> > +        buff = []
> > +        first = True
> > +        # We first place env variables that have a u64 storage.
> > +        # Those are limited by MAX_HA_ENV_LEN, other variables
> > +        # are read only and don't require a storage.
> > +        unstored = self.__get_non_stored_envs()
> > +        for env in list(self.env_stored) + unstored:
> > +            if first:
> > +                buff.append("\t%s%s = 0," % (env,
> > self.enum_suffix))
> > +                first = False
> > +            else:
> > +                buff.append("\t%s%s," % (env, self.enum_suffix))
> 
> The "= 0" assignment for the first enum is not required right?
> Perhaps you can get rid of the 'first" thingy, and just do
> 
> for env in list(self.env_stored) + unstored:
>     buff.append("\t%s%s," % (env, self.enum_suffix))
> 

Right, that's covered by the standard, we could just remove it.

> > +        match unit:
> > +            case "us":
> > +                value *= 1000
> > +            case "ms":
> > +                value *= 1000000
> > +            case "s":
> > +                value *= 1000000000
> 
> Since when did Python have this? Nice!

I think it was 3.10 . Honestly, it hasn't had it for way too long!

Thanks,
Gabriele