verification/dot2c: Remove superfluous enum assignment and add last comma

The header files generated by dot2c currently create enums for states
and events assigning the first element to 0. This is superfluous as it
happens automatically if no value is specified.
Also it doesn't add a comma to the last enum elements, which slightly
complicates the diff if states or events are added.

Remove the assignment to 0 and add a comma to last elements, this
simplifies the logic for the code generator.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20251126104241.291258-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
This commit is contained in:
Gabriele Monaco 2025-11-26 11:42:38 +01:00
parent 0d2405a086
commit 3d2bfeeef3
11 changed files with 94 additions and 106 deletions

View File

@ -8,21 +8,21 @@
#define MONITOR_NAME nrp #define MONITOR_NAME nrp
enum states_nrp { enum states_nrp {
preempt_irq_nrp = 0, preempt_irq_nrp,
any_thread_running_nrp, any_thread_running_nrp,
nested_preempt_nrp, nested_preempt_nrp,
rescheduling_nrp, rescheduling_nrp,
state_max_nrp state_max_nrp,
}; };
#define INVALID_STATE state_max_nrp #define INVALID_STATE state_max_nrp
enum events_nrp { enum events_nrp {
irq_entry_nrp = 0, irq_entry_nrp,
sched_need_resched_nrp, sched_need_resched_nrp,
schedule_entry_nrp, schedule_entry_nrp,
schedule_entry_preempt_nrp, schedule_entry_preempt_nrp,
event_max_nrp event_max_nrp,
}; };
struct automaton_nrp { struct automaton_nrp {
@ -38,38 +38,38 @@ static const struct automaton_nrp automaton_nrp = {
"preempt_irq", "preempt_irq",
"any_thread_running", "any_thread_running",
"nested_preempt", "nested_preempt",
"rescheduling" "rescheduling",
}, },
.event_names = { .event_names = {
"irq_entry", "irq_entry",
"sched_need_resched", "sched_need_resched",
"schedule_entry", "schedule_entry",
"schedule_entry_preempt" "schedule_entry_preempt",
}, },
.function = { .function = {
{ {
preempt_irq_nrp, preempt_irq_nrp,
preempt_irq_nrp, preempt_irq_nrp,
nested_preempt_nrp, nested_preempt_nrp,
nested_preempt_nrp nested_preempt_nrp,
}, },
{ {
any_thread_running_nrp, any_thread_running_nrp,
rescheduling_nrp, rescheduling_nrp,
any_thread_running_nrp, any_thread_running_nrp,
INVALID_STATE INVALID_STATE,
}, },
{ {
nested_preempt_nrp, nested_preempt_nrp,
preempt_irq_nrp, preempt_irq_nrp,
any_thread_running_nrp, any_thread_running_nrp,
any_thread_running_nrp any_thread_running_nrp,
}, },
{ {
preempt_irq_nrp, preempt_irq_nrp,
rescheduling_nrp, rescheduling_nrp,
any_thread_running_nrp, any_thread_running_nrp,
any_thread_running_nrp any_thread_running_nrp,
}, },
}, },
.initial_state = preempt_irq_nrp, .initial_state = preempt_irq_nrp,

View File

@ -8,25 +8,25 @@
#define MONITOR_NAME opid #define MONITOR_NAME opid
enum states_opid { enum states_opid {
disabled_opid = 0, disabled_opid,
enabled_opid, enabled_opid,
in_irq_opid, in_irq_opid,
irq_disabled_opid, irq_disabled_opid,
preempt_disabled_opid, preempt_disabled_opid,
state_max_opid state_max_opid,
}; };
#define INVALID_STATE state_max_opid #define INVALID_STATE state_max_opid
enum events_opid { enum events_opid {
irq_disable_opid = 0, irq_disable_opid,
irq_enable_opid, irq_enable_opid,
irq_entry_opid, irq_entry_opid,
preempt_disable_opid, preempt_disable_opid,
preempt_enable_opid, preempt_enable_opid,
sched_need_resched_opid, sched_need_resched_opid,
sched_waking_opid, sched_waking_opid,
event_max_opid event_max_opid,
}; };
struct automaton_opid { struct automaton_opid {
@ -43,7 +43,7 @@ static const struct automaton_opid automaton_opid = {
"enabled", "enabled",
"in_irq", "in_irq",
"irq_disabled", "irq_disabled",
"preempt_disabled" "preempt_disabled",
}, },
.event_names = { .event_names = {
"irq_disable", "irq_disable",
@ -52,7 +52,7 @@ static const struct automaton_opid automaton_opid = {
"preempt_disable", "preempt_disable",
"preempt_enable", "preempt_enable",
"sched_need_resched", "sched_need_resched",
"sched_waking" "sched_waking",
}, },
.function = { .function = {
{ {
@ -62,7 +62,7 @@ static const struct automaton_opid automaton_opid = {
INVALID_STATE, INVALID_STATE,
irq_disabled_opid, irq_disabled_opid,
disabled_opid, disabled_opid,
disabled_opid disabled_opid,
}, },
{ {
irq_disabled_opid, irq_disabled_opid,
@ -71,7 +71,7 @@ static const struct automaton_opid automaton_opid = {
preempt_disabled_opid, preempt_disabled_opid,
enabled_opid, enabled_opid,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -80,7 +80,7 @@ static const struct automaton_opid automaton_opid = {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
in_irq_opid, in_irq_opid,
in_irq_opid in_irq_opid,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -89,7 +89,7 @@ static const struct automaton_opid automaton_opid = {
disabled_opid, disabled_opid,
INVALID_STATE, INVALID_STATE,
irq_disabled_opid, irq_disabled_opid,
INVALID_STATE INVALID_STATE,
}, },
{ {
disabled_opid, disabled_opid,
@ -98,7 +98,7 @@ static const struct automaton_opid automaton_opid = {
INVALID_STATE, INVALID_STATE,
enabled_opid, enabled_opid,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
}, },
.initial_state = disabled_opid, .initial_state = disabled_opid,

View File

@ -8,18 +8,18 @@
#define MONITOR_NAME sco #define MONITOR_NAME sco
enum states_sco { enum states_sco {
thread_context_sco = 0, thread_context_sco,
scheduling_context_sco, scheduling_context_sco,
state_max_sco state_max_sco,
}; };
#define INVALID_STATE state_max_sco #define INVALID_STATE state_max_sco
enum events_sco { enum events_sco {
sched_set_state_sco = 0, sched_set_state_sco,
schedule_entry_sco, schedule_entry_sco,
schedule_exit_sco, schedule_exit_sco,
event_max_sco event_max_sco,
}; };
struct automaton_sco { struct automaton_sco {
@ -33,12 +33,12 @@ struct automaton_sco {
static const struct automaton_sco automaton_sco = { static const struct automaton_sco automaton_sco = {
.state_names = { .state_names = {
"thread_context", "thread_context",
"scheduling_context" "scheduling_context",
}, },
.event_names = { .event_names = {
"sched_set_state", "sched_set_state",
"schedule_entry", "schedule_entry",
"schedule_exit" "schedule_exit",
}, },
.function = { .function = {
{ thread_context_sco, scheduling_context_sco, INVALID_STATE }, { thread_context_sco, scheduling_context_sco, INVALID_STATE },

View File

@ -8,19 +8,19 @@
#define MONITOR_NAME scpd #define MONITOR_NAME scpd
enum states_scpd { enum states_scpd {
cant_sched_scpd = 0, cant_sched_scpd,
can_sched_scpd, can_sched_scpd,
state_max_scpd state_max_scpd,
}; };
#define INVALID_STATE state_max_scpd #define INVALID_STATE state_max_scpd
enum events_scpd { enum events_scpd {
preempt_disable_scpd = 0, preempt_disable_scpd,
preempt_enable_scpd, preempt_enable_scpd,
schedule_entry_scpd, schedule_entry_scpd,
schedule_exit_scpd, schedule_exit_scpd,
event_max_scpd event_max_scpd,
}; };
struct automaton_scpd { struct automaton_scpd {
@ -34,13 +34,13 @@ struct automaton_scpd {
static const struct automaton_scpd automaton_scpd = { static const struct automaton_scpd automaton_scpd = {
.state_names = { .state_names = {
"cant_sched", "cant_sched",
"can_sched" "can_sched",
}, },
.event_names = { .event_names = {
"preempt_disable", "preempt_disable",
"preempt_enable", "preempt_enable",
"schedule_entry", "schedule_entry",
"schedule_exit" "schedule_exit",
}, },
.function = { .function = {
{ can_sched_scpd, INVALID_STATE, INVALID_STATE, INVALID_STATE }, { can_sched_scpd, INVALID_STATE, INVALID_STATE, INVALID_STATE },

View File

@ -8,19 +8,19 @@
#define MONITOR_NAME snep #define MONITOR_NAME snep
enum states_snep { enum states_snep {
non_scheduling_context_snep = 0, non_scheduling_context_snep,
scheduling_contex_snep, scheduling_contex_snep,
state_max_snep state_max_snep,
}; };
#define INVALID_STATE state_max_snep #define INVALID_STATE state_max_snep
enum events_snep { enum events_snep {
preempt_disable_snep = 0, preempt_disable_snep,
preempt_enable_snep, preempt_enable_snep,
schedule_entry_snep, schedule_entry_snep,
schedule_exit_snep, schedule_exit_snep,
event_max_snep event_max_snep,
}; };
struct automaton_snep { struct automaton_snep {
@ -34,26 +34,26 @@ struct automaton_snep {
static const struct automaton_snep automaton_snep = { static const struct automaton_snep automaton_snep = {
.state_names = { .state_names = {
"non_scheduling_context", "non_scheduling_context",
"scheduling_contex" "scheduling_contex",
}, },
.event_names = { .event_names = {
"preempt_disable", "preempt_disable",
"preempt_enable", "preempt_enable",
"schedule_entry", "schedule_entry",
"schedule_exit" "schedule_exit",
}, },
.function = { .function = {
{ {
non_scheduling_context_snep, non_scheduling_context_snep,
non_scheduling_context_snep, non_scheduling_context_snep,
scheduling_contex_snep, scheduling_contex_snep,
INVALID_STATE INVALID_STATE,
}, },
{ {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
non_scheduling_context_snep non_scheduling_context_snep,
}, },
}, },
.initial_state = non_scheduling_context_snep, .initial_state = non_scheduling_context_snep,

View File

@ -8,18 +8,18 @@
#define MONITOR_NAME snroc #define MONITOR_NAME snroc
enum states_snroc { enum states_snroc {
other_context_snroc = 0, other_context_snroc,
own_context_snroc, own_context_snroc,
state_max_snroc state_max_snroc,
}; };
#define INVALID_STATE state_max_snroc #define INVALID_STATE state_max_snroc
enum events_snroc { enum events_snroc {
sched_set_state_snroc = 0, sched_set_state_snroc,
sched_switch_in_snroc, sched_switch_in_snroc,
sched_switch_out_snroc, sched_switch_out_snroc,
event_max_snroc event_max_snroc,
}; };
struct automaton_snroc { struct automaton_snroc {
@ -33,12 +33,12 @@ struct automaton_snroc {
static const struct automaton_snroc automaton_snroc = { static const struct automaton_snroc automaton_snroc = {
.state_names = { .state_names = {
"other_context", "other_context",
"own_context" "own_context",
}, },
.event_names = { .event_names = {
"sched_set_state", "sched_set_state",
"sched_switch_in", "sched_switch_in",
"sched_switch_out" "sched_switch_out",
}, },
.function = { .function = {
{ INVALID_STATE, own_context_snroc, INVALID_STATE }, { INVALID_STATE, own_context_snroc, INVALID_STATE },

View File

@ -8,17 +8,17 @@
#define MONITOR_NAME sssw #define MONITOR_NAME sssw
enum states_sssw { enum states_sssw {
runnable_sssw = 0, runnable_sssw,
signal_wakeup_sssw, signal_wakeup_sssw,
sleepable_sssw, sleepable_sssw,
sleeping_sssw, sleeping_sssw,
state_max_sssw state_max_sssw,
}; };
#define INVALID_STATE state_max_sssw #define INVALID_STATE state_max_sssw
enum events_sssw { enum events_sssw {
sched_set_state_runnable_sssw = 0, sched_set_state_runnable_sssw,
sched_set_state_sleepable_sssw, sched_set_state_sleepable_sssw,
sched_switch_blocking_sssw, sched_switch_blocking_sssw,
sched_switch_in_sssw, sched_switch_in_sssw,
@ -27,7 +27,7 @@ enum events_sssw {
sched_switch_yield_sssw, sched_switch_yield_sssw,
sched_wakeup_sssw, sched_wakeup_sssw,
signal_deliver_sssw, signal_deliver_sssw,
event_max_sssw event_max_sssw,
}; };
struct automaton_sssw { struct automaton_sssw {
@ -43,7 +43,7 @@ static const struct automaton_sssw automaton_sssw = {
"runnable", "runnable",
"signal_wakeup", "signal_wakeup",
"sleepable", "sleepable",
"sleeping" "sleeping",
}, },
.event_names = { .event_names = {
"sched_set_state_runnable", "sched_set_state_runnable",
@ -54,7 +54,7 @@ static const struct automaton_sssw automaton_sssw = {
"sched_switch_suspend", "sched_switch_suspend",
"sched_switch_yield", "sched_switch_yield",
"sched_wakeup", "sched_wakeup",
"signal_deliver" "signal_deliver",
}, },
.function = { .function = {
{ {
@ -66,7 +66,7 @@ static const struct automaton_sssw automaton_sssw = {
INVALID_STATE, INVALID_STATE,
runnable_sssw, runnable_sssw,
runnable_sssw, runnable_sssw,
runnable_sssw runnable_sssw,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -77,7 +77,7 @@ static const struct automaton_sssw automaton_sssw = {
INVALID_STATE, INVALID_STATE,
signal_wakeup_sssw, signal_wakeup_sssw,
signal_wakeup_sssw, signal_wakeup_sssw,
runnable_sssw runnable_sssw,
}, },
{ {
runnable_sssw, runnable_sssw,
@ -88,7 +88,7 @@ static const struct automaton_sssw automaton_sssw = {
sleeping_sssw, sleeping_sssw,
signal_wakeup_sssw, signal_wakeup_sssw,
runnable_sssw, runnable_sssw,
sleepable_sssw sleepable_sssw,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -99,7 +99,7 @@ static const struct automaton_sssw automaton_sssw = {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
runnable_sssw, runnable_sssw,
INVALID_STATE INVALID_STATE,
}, },
}, },
.initial_state = runnable_sssw, .initial_state = runnable_sssw,

View File

@ -8,26 +8,26 @@
#define MONITOR_NAME sts #define MONITOR_NAME sts
enum states_sts { enum states_sts {
can_sched_sts = 0, can_sched_sts,
cant_sched_sts, cant_sched_sts,
disable_to_switch_sts, disable_to_switch_sts,
enable_to_exit_sts, enable_to_exit_sts,
in_irq_sts, in_irq_sts,
scheduling_sts, scheduling_sts,
switching_sts, switching_sts,
state_max_sts state_max_sts,
}; };
#define INVALID_STATE state_max_sts #define INVALID_STATE state_max_sts
enum events_sts { enum events_sts {
irq_disable_sts = 0, irq_disable_sts,
irq_enable_sts, irq_enable_sts,
irq_entry_sts, irq_entry_sts,
sched_switch_sts, sched_switch_sts,
schedule_entry_sts, schedule_entry_sts,
schedule_exit_sts, schedule_exit_sts,
event_max_sts event_max_sts,
}; };
struct automaton_sts { struct automaton_sts {
@ -46,7 +46,7 @@ static const struct automaton_sts automaton_sts = {
"enable_to_exit", "enable_to_exit",
"in_irq", "in_irq",
"scheduling", "scheduling",
"switching" "switching",
}, },
.event_names = { .event_names = {
"irq_disable", "irq_disable",
@ -54,7 +54,7 @@ static const struct automaton_sts automaton_sts = {
"irq_entry", "irq_entry",
"sched_switch", "sched_switch",
"schedule_entry", "schedule_entry",
"schedule_exit" "schedule_exit",
}, },
.function = { .function = {
{ {
@ -63,7 +63,7 @@ static const struct automaton_sts automaton_sts = {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
scheduling_sts, scheduling_sts,
INVALID_STATE INVALID_STATE,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -71,7 +71,7 @@ static const struct automaton_sts automaton_sts = {
cant_sched_sts, cant_sched_sts,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -79,7 +79,7 @@ static const struct automaton_sts automaton_sts = {
in_irq_sts, in_irq_sts,
switching_sts, switching_sts,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
{ {
enable_to_exit_sts, enable_to_exit_sts,
@ -87,7 +87,7 @@ static const struct automaton_sts automaton_sts = {
enable_to_exit_sts, enable_to_exit_sts,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
can_sched_sts can_sched_sts,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -95,7 +95,7 @@ static const struct automaton_sts automaton_sts = {
in_irq_sts, in_irq_sts,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
{ {
disable_to_switch_sts, disable_to_switch_sts,
@ -103,7 +103,7 @@ static const struct automaton_sts automaton_sts = {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
{ {
INVALID_STATE, INVALID_STATE,
@ -111,7 +111,7 @@ static const struct automaton_sts automaton_sts = {
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE, INVALID_STATE,
INVALID_STATE INVALID_STATE,
}, },
}, },
.initial_state = can_sched_sts, .initial_state = can_sched_sts,

View File

@ -8,18 +8,18 @@
#define MONITOR_NAME wip #define MONITOR_NAME wip
enum states_wip { enum states_wip {
preemptive_wip = 0, preemptive_wip,
non_preemptive_wip, non_preemptive_wip,
state_max_wip state_max_wip,
}; };
#define INVALID_STATE state_max_wip #define INVALID_STATE state_max_wip
enum events_wip { enum events_wip {
preempt_disable_wip = 0, preempt_disable_wip,
preempt_enable_wip, preempt_enable_wip,
sched_waking_wip, sched_waking_wip,
event_max_wip event_max_wip,
}; };
struct automaton_wip { struct automaton_wip {
@ -33,12 +33,12 @@ struct automaton_wip {
static const struct automaton_wip automaton_wip = { static const struct automaton_wip automaton_wip = {
.state_names = { .state_names = {
"preemptive", "preemptive",
"non_preemptive" "non_preemptive",
}, },
.event_names = { .event_names = {
"preempt_disable", "preempt_disable",
"preempt_enable", "preempt_enable",
"sched_waking" "sched_waking",
}, },
.function = { .function = {
{ non_preemptive_wip, INVALID_STATE, INVALID_STATE }, { non_preemptive_wip, INVALID_STATE, INVALID_STATE },

View File

@ -8,18 +8,18 @@
#define MONITOR_NAME wwnr #define MONITOR_NAME wwnr
enum states_wwnr { enum states_wwnr {
not_running_wwnr = 0, not_running_wwnr,
running_wwnr, running_wwnr,
state_max_wwnr state_max_wwnr,
}; };
#define INVALID_STATE state_max_wwnr #define INVALID_STATE state_max_wwnr
enum events_wwnr { enum events_wwnr {
switch_in_wwnr = 0, switch_in_wwnr,
switch_out_wwnr, switch_out_wwnr,
wakeup_wwnr, wakeup_wwnr,
event_max_wwnr event_max_wwnr,
}; };
struct automaton_wwnr { struct automaton_wwnr {
@ -33,12 +33,12 @@ struct automaton_wwnr {
static const struct automaton_wwnr automaton_wwnr = { static const struct automaton_wwnr automaton_wwnr = {
.state_names = { .state_names = {
"not_running", "not_running",
"running" "running",
}, },
.event_names = { .event_names = {
"switch_in", "switch_in",
"switch_out", "switch_out",
"wakeup" "wakeup",
}, },
.function = { .function = {
{ running_wwnr, INVALID_STATE, not_running_wwnr }, { running_wwnr, INVALID_STATE, not_running_wwnr },

View File

@ -28,11 +28,11 @@ class Dot2c(Automata):
def __get_enum_states_content(self) -> list[str]: def __get_enum_states_content(self) -> list[str]:
buff = [] buff = []
buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix)) buff.append("\t%s%s," % (self.initial_state, self.enum_suffix))
for state in self.states: for state in self.states:
if state != self.initial_state: if state != self.initial_state:
buff.append("\t%s%s," % (state, self.enum_suffix)) buff.append("\t%s%s," % (state, self.enum_suffix))
buff.append("\tstate_max%s" % (self.enum_suffix)) buff.append("\tstate_max%s," % (self.enum_suffix))
return buff return buff
@ -46,15 +46,10 @@ class Dot2c(Automata):
def __get_enum_events_content(self) -> list[str]: def __get_enum_events_content(self) -> list[str]:
buff = [] buff = []
first = True
for event in self.events: for event in self.events:
if first: buff.append("\t%s%s," % (event, self.enum_suffix))
buff.append("\t%s%s = 0," % (event, self.enum_suffix))
first = False
else:
buff.append("\t%s%s," % (event, self.enum_suffix))
buff.append("\tevent_max%s" % self.enum_suffix) buff.append("\tevent_max%s," % self.enum_suffix)
return buff return buff
@ -97,18 +92,11 @@ class Dot2c(Automata):
buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def)) buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
return buff return buff
def __get_string_vector_per_line_content(self, buff: list[str]) -> str: def __get_string_vector_per_line_content(self, entries: list[str]) -> str:
first = True buff = []
string = "" for entry in entries:
for entry in buff: buff.append(f"\t\t\"{entry}\",")
if first: return "\n".join(buff)
string = string + "\t\t\"" + entry
first = False;
else:
string = string + "\",\n\t\t\"" + entry
string = string + "\""
return string
def format_aut_init_events_string(self) -> list[str]: def format_aut_init_events_string(self) -> list[str]:
buff = [] buff = []
@ -152,7 +140,7 @@ class Dot2c(Automata):
if y != nr_events-1: if y != nr_events-1:
line += ",\n" if linetoolong else ", " line += ",\n" if linetoolong else ", "
else: else:
line += "\n\t\t}," if linetoolong else " }," line += ",\n\t\t}," if linetoolong else " },"
buff.append(line) buff.append(line)
return '\n'.join(buff) return '\n'.join(buff)
@ -179,12 +167,12 @@ class Dot2c(Automata):
line = "" line = ""
first = True first = True
for state in self.states: for state in self.states:
if first == False: if not first:
line = line + ', ' line = line + ', '
else: else:
first = False first = False
if self.final_states.__contains__(state): if state in self.final_states:
line = line + '1' line = line + '1'
else: else:
line = line + '0' line = line + '0'