| 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
| ||
|
Message-ID: <6e84cdfe17492f31be8e4373fef7b3e1a37a6779.camel@redhat.com>
Date: Mon, 25 Aug 2025 16:24:13 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>
Cc: linux-kernel@...r.kernel.org, Steven Rostedt <rostedt@...dmis.org>,
linux-trace-kernel@...r.kernel.org, Tomas Glozar <tglozar@...hat.com>, Juri
Lelli <jlelli@...hat.com>, Clark Williams <williams@...hat.com>, John Kacur
<jkacur@...hat.com>
Subject: Re: [RFC PATCH 10/17] verification/rvgen: Add support for Hybrid
Automata
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
Powered by blists - more mailing lists