Per-object monitors can allocate memory dynamically and such memory is required for the lifetime of the object, then it should be freed with the appropriate call.
Force the generation scripts to add a cleanup function the user will need to wire to the appropriate event (e.g. sched_process_exit for tasks). This can be safely removed if the object will never cease to exist before disabling the monitor (e.g. if following only static variables). Signed-off-by: Gabriele Monaco <[email protected]> --- tools/verification/rvgen/rvgen/dot2k.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index 110cfd69e..3060aa4b9 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -17,6 +17,9 @@ from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError class dot2k(Monitor, Dot2c): template_dir = "dot2k" + # only needed for the per-obj cleanup hook + cleanup_marker = "obj_cleanup" + def __init__(self, file_path, MonitorType, extra_params={}): self.monitor_type = MonitorType Monitor.__init__(self, extra_params) @@ -56,18 +59,30 @@ class dot2k(Monitor, Dot2c): buff.append(f"\tda_{handle}({event}{self.enum_suffix});") buff.append("}") buff.append("") + if self.monitor_type == "per_obj": + buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */") + buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tint id = /* XXX: how do I get the id? */;") + buff.append("\tda_destroy_storage(id);") + buff.append("}") + buff.append("") return '\n'.join(buff) def fill_tracepoint_attach_probe(self) -> str: buff = [] for event in self.events: buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") return '\n'.join(buff) def fill_tracepoint_detach_helper(self) -> str: buff = [] for event in self.events: buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") return '\n'.join(buff) def fill_model_h_header(self) -> list[str]: -- 2.54.0
