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

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

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <20250825100631.uTAyvLwP@linutronix.de>
Date: Mon, 25 Aug 2025 12:06:31 +0200
From: Nam Cao <namcao@...utronix.de>
To: Gabriele Monaco <gmonaco@...hat.com>
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 Thu, Aug 14, 2025 at 05:08:02PM +0200, Gabriele Monaco wrote:
> +    def fill_constr_func(self) -> list[str]:
> +        buff = []
> +        if self.constraints:
> +            buff.append(
> +"""/*
> + * This function is used to validate state transitions.
> + *
> + * It is generated by parsing the model, there is usually no need to change it,
> + * unless conditions were incorrectly specified

If the conditions were incorrectly specified, then they should be fixed in
the automaton, not fixed in this generated C code.

> or too complex for the parser.

Do you have examples of these "too complex" cases? Is there a plan to
handle them?

> + * If the monitor requires a timer, this function is responsible to arm it when
> + * the next state has a constraint and cancel it in any other case. Transitions
> + * to the same state never affect timers.
> + */
> +static bool ha_verify_constraint(struct ha_monitor *ha_mon,
> +\t\t\t\t enum %s curr_state, enum %s event,
> +\t\t\t\t enum %s next_state)
> +{
> +\tbool res = true;
> +""" % (self.enum_states_def, self.enum_events_def, self.enum_states_def))
> +            buff += self.__get_constr_condition()
> +            buff += self.__get_state_constr_condition()
> +            buff.append("""\treturn res;
> +}\n""")
> +        return buff

Nam