diff options
| -rw-r--r-- | include/rv/da_monitor.h | 139 | ||||
| -rw-r--r-- | include/rv/ha_monitor.h | 91 | ||||
| -rw-r--r-- | include/rv/ltl_monitor.h | 1 | ||||
| -rw-r--r-- | kernel/trace/rv/monitors/deadline/deadline.h | 3 | ||||
| -rw-r--r-- | kernel/trace/rv/monitors/nomiss/nomiss.c | 4 | ||||
| -rw-r--r-- | kernel/trace/rv/monitors/opid/opid.c | 12 | ||||
| -rw-r--r-- | kernel/trace/rv/monitors/stall/stall.c | 4 | ||||
| -rw-r--r-- | tools/verification/rv/src/in_kernel.c | 65 | ||||
| -rw-r--r-- | tools/verification/rvgen/__main__.py | 10 | ||||
| -rw-r--r-- | tools/verification/rvgen/rvgen/dot2k.py | 4 | ||||
| -rw-r--r-- | tools/verification/rvgen/rvgen/ltl2ba.py | 9 | ||||
| -rw-r--r-- | tools/verification/rvgen/rvgen/templates/dot2k/main.c | 4 |
12 files changed, 263 insertions, 83 deletions
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 39765ff6f098..34b8fba9ecd4 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -58,6 +58,15 @@ static struct rv_monitor rv_this; #endif /* + * Hook to allow the implementation of hybrid automata: define it with a + * function that waits for the termination of all monitors background + * activities (e.g. all timers). This hook can sleep. + */ +#ifndef da_monitor_sync_hook +#define da_monitor_sync_hook() +#endif + +/* * Type for the target id, default to int but can be overridden. * A long type can work as hash table key (PER_OBJ) but will be downgraded to * int in the event tracepoint. @@ -77,13 +86,22 @@ static void react(enum states curr_state, enum events event) } /* + * da_monitor_reset_state - reset a monitor and setting it to init state + */ +static inline void da_monitor_reset_state(struct da_monitor *da_mon) +{ + WRITE_ONCE(da_mon->monitoring, 0); + /* Pair with load in __ha_monitor_timer_callback */ + smp_store_release(&da_mon->curr_state, model_get_initial_state()); +} + +/* * da_monitor_reset - reset a monitor and setting it to init state */ static inline void da_monitor_reset(struct da_monitor *da_mon) { da_monitor_reset_hook(da_mon); - da_mon->monitoring = 0; - da_mon->curr_state = model_get_initial_state(); + da_monitor_reset_state(da_mon); } /* @@ -95,8 +113,9 @@ static inline void da_monitor_reset(struct da_monitor *da_mon) static inline void da_monitor_start(struct da_monitor *da_mon) { da_mon->curr_state = model_get_initial_state(); - da_mon->monitoring = 1; da_monitor_init_hook(da_mon); + /* Pairs with smp_load_acquire in da_monitoring(). */ + smp_store_release(&da_mon->monitoring, 1); } /* @@ -104,7 +123,8 @@ static inline void da_monitor_start(struct da_monitor *da_mon) */ static inline bool da_monitoring(struct da_monitor *da_mon) { - return da_mon->monitoring; + /* Pairs with smp_store_release in da_monitor_start(). */ + return smp_load_acquire(&da_mon->monitoring); } /* @@ -157,11 +177,27 @@ static struct da_monitor *da_get_monitor(void) } /* + * __da_monitor_reset_all - reset the single monitor + */ +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) +{ + reset(da_get_monitor()); +} + +/* * da_monitor_reset_all - reset the single monitor */ static void da_monitor_reset_all(void) { - da_monitor_reset(da_get_monitor()); + __da_monitor_reset_all(da_monitor_reset); +} + +/* + * da_monitor_reset_state_all - reset the single monitor + */ +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); } /* @@ -169,7 +205,7 @@ static void da_monitor_reset_all(void) */ static inline int da_monitor_init(void) { - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } @@ -179,8 +215,13 @@ static inline int da_monitor_init(void) static inline void da_monitor_destroy(void) { da_monitor_reset_all(); + da_monitor_sync_hook(); } +#ifndef da_implicit_guard +#define da_implicit_guard() +#endif + #elif RV_MON_TYPE == RV_MON_PER_CPU /* * Functions to define, init and get a per-cpu monitor. @@ -200,25 +241,41 @@ static struct da_monitor *da_get_monitor(void) } /* - * da_monitor_reset_all - reset all CPUs' monitor + * __da_monitor_reset_all - reset all CPUs' monitor */ -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct da_monitor *da_mon; int cpu; for_each_cpu(cpu, cpu_online_mask) { da_mon = per_cpu_ptr(&DA_MON_NAME, cpu); - da_monitor_reset(da_mon); + reset(da_mon); } } /* + * da_monitor_reset_all - reset all CPUs' monitor + */ +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +/* + * da_monitor_reset_state_all - reset all CPUs' monitor + */ +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); +} + +/* * da_monitor_init - initialize all CPUs' monitor */ static inline int da_monitor_init(void) { - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } @@ -228,8 +285,13 @@ static inline int da_monitor_init(void) static inline void da_monitor_destroy(void) { da_monitor_reset_all(); + da_monitor_sync_hook(); } +#ifndef da_implicit_guard +#define da_implicit_guard() guard(migrate)() +#endif + #elif RV_MON_TYPE == RV_MON_PER_TASK /* * Functions to define, init and get a per-task monitor. @@ -267,19 +329,29 @@ static inline da_id_type da_get_id(struct da_monitor *da_mon) return da_get_target(da_mon)->pid; } -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct task_struct *g, *p; int cpu; read_lock(&tasklist_lock); for_each_process_thread(g, p) - da_monitor_reset(da_get_monitor(p)); + reset(da_get_monitor(p)); for_each_present_cpu(cpu) - da_monitor_reset(da_get_monitor(idle_task(cpu))); + reset(da_get_monitor(idle_task(cpu))); read_unlock(&tasklist_lock); } +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); +} + /* * da_monitor_init - initialize the per-task monitor * @@ -296,12 +368,15 @@ static int da_monitor_init(void) task_mon_slot = slot; - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } /* * da_monitor_destroy - return the allocated slot + * + * Wait for all in-flight handlers before returning the slot to avoid + * out-of-bound accesses. */ static inline void da_monitor_destroy(void) { @@ -309,10 +384,13 @@ static inline void da_monitor_destroy(void) WARN_ONCE(1, "Disabling a disabled monitor: " __stringify(MONITOR_NAME)); return; } - rv_put_task_monitor_slot(task_mon_slot); - task_mon_slot = RV_PER_TASK_MONITOR_INIT; + tracepoint_synchronize_unregister(); da_monitor_reset_all(); + da_monitor_sync_hook(); + + rv_put_task_monitor_slot(task_mon_slot); + task_mon_slot = RV_PER_TASK_MONITOR_INIT; } #elif RV_MON_TYPE == RV_MON_PER_OBJ @@ -483,15 +561,24 @@ static inline void da_destroy_storage(da_id_type id) kfree_rcu(mon_storage, rcu); } -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct da_monitor_storage *mon_storage; int bkt; - rcu_read_lock(); + guard(rcu)(); hash_for_each_rcu(da_monitor_ht, bkt, mon_storage, node) - da_monitor_reset(&mon_storage->rv.da_mon); - rcu_read_unlock(); + reset(&mon_storage->rv.da_mon); +} + +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); } static inline int da_monitor_init(void) @@ -506,13 +593,14 @@ static inline void da_monitor_destroy(void) struct hlist_node *tmp; int bkt; + tracepoint_synchronize_unregister(); + da_monitor_reset_all(); + da_monitor_sync_hook(); /* - * This function is called after all probes are disabled, we need only - * worry about concurrency against old events. + * This function is called after all probes are disabled and no longer + * pending, we can safely assume no concurrent user. */ - synchronize_rcu(); hash_for_each_safe(da_monitor_ht, bkt, tmp, mon_storage, node) { - da_monitor_reset_hook(&mon_storage->rv.da_mon); hash_del_rcu(&mon_storage->node); kfree(mon_storage); } @@ -676,6 +764,7 @@ static inline bool __da_handle_start_run_event(struct da_monitor *da_mon, */ static inline void da_handle_event(enum events event) { + da_implicit_guard(); __da_handle_event(da_get_monitor(), event, 0); } @@ -691,6 +780,7 @@ static inline void da_handle_event(enum events event) */ static inline bool da_handle_start_event(enum events event) { + da_implicit_guard(); return __da_handle_start_event(da_get_monitor(), event, 0); } @@ -702,6 +792,7 @@ static inline bool da_handle_start_event(enum events event) */ static inline bool da_handle_start_run_event(enum events event) { + da_implicit_guard(); return __da_handle_start_run_event(da_get_monitor(), event, 0); } diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h index d59507e8cb30..28d3c74cabfc 100644 --- a/include/rv/ha_monitor.h +++ b/include/rv/ha_monitor.h @@ -28,6 +28,7 @@ static inline void ha_monitor_init_env(struct da_monitor *da_mon); static inline void ha_monitor_reset_env(struct da_monitor *da_mon); static inline void ha_setup_timer(struct ha_monitor *ha_mon); static inline bool ha_cancel_timer(struct ha_monitor *ha_mon); +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon); static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, enum states curr_state, enum events event, @@ -36,6 +37,27 @@ static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, #define da_monitor_event_hook ha_monitor_handle_constraint #define da_monitor_init_hook ha_monitor_init_env #define da_monitor_reset_hook ha_monitor_reset_env +#define da_monitor_sync_hook() synchronize_rcu() + +#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK +/* + * Automatic cleanup handlers for per-task HA monitors, only skip if you know + * what you are doing (e.g. you want to implement cleanup manually in another + * handler doing more things). + */ +static void ha_handle_sched_process_exit(void *data, struct task_struct *p, + bool group_dead); + +#define ha_monitor_enable_hook() \ + rv_attach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \ + ha_handle_sched_process_exit) +#define ha_monitor_disable_hook() \ + rv_detach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \ + ha_handle_sched_process_exit) +#else +#define ha_monitor_enable_hook() ((void)0) +#define ha_monitor_disable_hook() ((void)0) +#endif #include <rv/da_monitor.h> #include <linux/seq_buf.h> @@ -115,6 +137,26 @@ static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer); #define ha_get_ns() 0 #endif /* HA_CLK_NS */ +static bool ha_mon_destroying; + +static int ha_monitor_init(void) +{ + int ret; + + WRITE_ONCE(ha_mon_destroying, false); + ret = da_monitor_init(); + if (ret == 0) + ha_monitor_enable_hook(); + return ret; +} + +static void ha_monitor_destroy(void) +{ + WRITE_ONCE(ha_mon_destroying, true); + ha_monitor_disable_hook(); + da_monitor_destroy(); +} + /* Should be supplied by the monitor */ static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env, u64 time_ns); static bool ha_verify_constraint(struct ha_monitor *ha_mon, @@ -153,12 +195,12 @@ static inline void ha_monitor_init_env(struct da_monitor *da_mon) * Called from a hook in the DA reset functions, it supplies the da_mon * corresponding to the current ha_mon. * Not all hybrid automata require the timer, still clear it for simplicity. + * Monitors that never started have their timer uninitialized, do not stop those. */ static inline void ha_monitor_reset_env(struct da_monitor *da_mon) { struct ha_monitor *ha_mon = to_ha_monitor(da_mon); - /* Initialisation resets the monitor before initialising the timer */ if (likely(da_monitoring(da_mon))) ha_cancel_timer(ha_mon); } @@ -200,6 +242,20 @@ static inline void ha_trace_error_env(struct ha_monitor *ha_mon, { CONCATENATE(trace_error_env_, MONITOR_NAME)(id, curr_state, event, env); } + +#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK +static void ha_handle_sched_process_exit(void *data, struct task_struct *p, + bool group_dead) +{ + struct da_monitor *da_mon = da_get_monitor(p); + + if (likely(da_monitoring(da_mon))) { + da_monitor_reset(da_mon); + ha_cancel_timer_sync(to_ha_monitor(da_mon)); + } +} +#endif + #endif /* RV_MON_TYPE */ /* @@ -237,12 +293,30 @@ static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, return false; } +/* + * __ha_monitor_timer_callback - generic callback representation + * + * This callback runs in an RCU read-side critical section to allow the + * destruction sequence to easily synchronize_rcu() with all pending timers + * after asynchronously disabling them. The ha_mon_destroying check ensures + * any callback entering the RCU section after synchronize_rcu() completes + * will see the flag and bail out immediately. + */ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon) { - enum states curr_state = READ_ONCE(ha_mon->da_mon.curr_state); DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE); - u64 time_ns = ha_get_ns(); - + enum states curr_state; + u64 time_ns; + + guard(rcu)(); + if (unlikely(READ_ONCE(ha_mon_destroying))) + return; + /* Ensure consistent curr_state if we race with da_monitor_reset */ + curr_state = smp_load_acquire(&ha_mon->da_mon.curr_state); + if (unlikely(!da_monitor_handling_event(&ha_mon->da_mon))) + return; + + time_ns = ha_get_ns(); ha_get_env_string(&env_string, ha_mon, time_ns); ha_react(curr_state, EVENT_NONE, env_string.buffer); ha_trace_error_env(ha_mon, model_get_state_name(curr_state), @@ -412,6 +486,10 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return timer_delete(&ha_mon->timer); } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) +{ + timer_delete_sync(&ha_mon->timer); +} #elif HA_TIMER_TYPE == HA_TIMER_HRTIMER /* * Helper functions to handle the monitor timer. @@ -463,6 +541,10 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return hrtimer_try_to_cancel(&ha_mon->hrtimer) == 1; } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) +{ + hrtimer_cancel(&ha_mon->hrtimer); +} #else /* HA_TIMER_NONE */ /* * Start function is intentionally not defined, monitors using timers must @@ -473,6 +555,7 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return false; } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) { } #endif #endif diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index eff60cd61106..38e792401f76 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -77,6 +77,7 @@ static void ltl_monitor_destroy(void) { rv_detach_trace_probe(name, task_newtask, handle_task_newtask); + tracepoint_synchronize_unregister(); rv_put_task_monitor_slot(ltl_monitor_slot); ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; } diff --git a/kernel/trace/rv/monitors/deadline/deadline.h b/kernel/trace/rv/monitors/deadline/deadline.h index 0bbfd2543329..78fca873d61e 100644 --- a/kernel/trace/rv/monitors/deadline/deadline.h +++ b/kernel/trace/rv/monitors/deadline/deadline.h @@ -95,7 +95,8 @@ static inline u8 get_server_type(struct task_struct *tsk) static inline int extract_params(struct pt_regs *regs, long id, pid_t *pid_out) { size_t size = offsetofend(struct sched_attr, sched_flags); - struct sched_attr __user *uattr, attr; + struct sched_attr __user *uattr; + struct sched_attr attr; int new_policy = -1, ret; unsigned long args[6]; diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c index 31f90f3638d8..8ead8783c29f 100644 --- a/kernel/trace/rv/monitors/nomiss/nomiss.c +++ b/kernel/trace/rv/monitors/nomiss/nomiss.c @@ -227,7 +227,7 @@ static int enable_nomiss(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -263,7 +263,7 @@ static void disable_nomiss(void) rv_detach_trace_probe("nomiss", sched_switch, handle_sched_switch); rv_detach_trace_probe("nomiss", sched_wakeup, handle_sched_wakeup); - da_monitor_destroy(); + ha_monitor_destroy(); } static struct rv_monitor rv_this = { diff --git a/kernel/trace/rv/monitors/opid/opid.c b/kernel/trace/rv/monitors/opid/opid.c index 4594c7c46601..3b6a85e815b8 100644 --- a/kernel/trace/rv/monitors/opid/opid.c +++ b/kernel/trace/rv/monitors/opid/opid.c @@ -22,14 +22,8 @@ static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_opid env, u64 time_ns if (env == irq_off_opid) return irqs_disabled(); else if (env == preempt_off_opid) { - /* - * If CONFIG_PREEMPTION is enabled, then the tracepoint itself disables - * preemption (adding one to the preempt_count). Since we are - * interested in the preempt_count at the time the tracepoint was - * hit, we consider 1 as still enabled. - */ if (IS_ENABLED(CONFIG_PREEMPTION)) - return (preempt_count() & PREEMPT_MASK) > 1; + return (preempt_count() & PREEMPT_MASK) > 0; return true; } return ENV_INVALID_VALUE; @@ -73,7 +67,7 @@ static int enable_opid(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -90,7 +84,7 @@ static void disable_opid(void) rv_detach_trace_probe("opid", sched_set_need_resched_tp, handle_sched_need_resched); rv_detach_trace_probe("opid", sched_waking, handle_sched_waking); - da_monitor_destroy(); + ha_monitor_destroy(); } /* diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monitors/stall/stall.c index 9ccfda6b0e73..3c38fb1a0159 100644 --- a/kernel/trace/rv/monitors/stall/stall.c +++ b/kernel/trace/rv/monitors/stall/stall.c @@ -103,7 +103,7 @@ static int enable_stall(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -120,7 +120,7 @@ static void disable_stall(void) rv_detach_trace_probe("stall", sched_switch, handle_sched_switch); rv_detach_trace_probe("stall", sched_wakeup, handle_sched_wakeup); - da_monitor_destroy(); + ha_monitor_destroy(); } static struct rv_monitor rv_this = { diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index 4bb746ea6e17..e6dea4040f8f 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -58,38 +58,40 @@ static int __ikm_read_enable(char *monitor_name) */ static int __ikm_find_monitor_name(char *monitor_name, char *out_name) { - char *available_monitors, container[MAX_DA_NAME_LEN+1], *cursor, *end; - int retval = 1; + char *available_monitors, *cursor, *line; + int len = strlen(monitor_name); + int found = 0; available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); if (!available_monitors) return -1; - cursor = strstr(available_monitors, monitor_name); - if (!cursor) { - retval = 0; - goto out_free; - } + config_is_container = 0; + cursor = available_monitors; + while ((line = strsep(&cursor, "\n"))) { + char *colon = strchr(line, ':'); - for (; cursor > available_monitors; cursor--) - if (*(cursor-1) == '\n') - break; - end = strstr(cursor, "\n"); - memcpy(out_name, cursor, end-cursor); - out_name[end-cursor] = '\0'; - - cursor = strstr(out_name, ":"); - if (cursor) - *cursor = '/'; - else { - sprintf(container, "%s:", monitor_name); - if (strstr(available_monitors, container)) - config_is_container = 1; + if (strcmp(line, monitor_name) && (!colon || strcmp(colon + 1, monitor_name))) + continue; + + strncpy(out_name, line, 2 * MAX_DA_NAME_LEN); + out_name[2 * MAX_DA_NAME_LEN - 1] = '\0'; + + if (colon) { + out_name[colon - line] = '/'; + } else { + /* If there are children, they are on the next line. */ + line = strsep(&cursor, "\n"); + if (line && !strncmp(line, monitor_name, len) && line[len] == ':') + config_is_container = 1; + } + + found = 1; + break; } -out_free: free(available_monitors); - return retval; + return found; } /* @@ -191,8 +193,12 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co nested_name = strstr(name, ":"); if (nested_name) { /* it belongs in container if it starts with "container:" */ - if (container && strstr(name, container) != name) - return 1; + if (container) { + int len = strlen(container); + + if (strncmp(name, container, len) || name[len] != ':') + return 1; + } *nested_name = '/'; ++nested_name; ikm->nested = 1; @@ -215,10 +221,11 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co return -1; } - strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); + strncpy(ikm->name, nested_name, sizeof(ikm->name) - 1); + ikm->name[sizeof(ikm->name) - 1] = '\0'; ikm->enabled = enabled; - strncpy(ikm->desc, desc, MAX_DESCRIPTION); - + strncpy(ikm->desc, desc, sizeof(ikm->desc) - 1); + ikm->desc[sizeof(ikm->desc) - 1] = '\0'; free(desc); return 0; @@ -803,7 +810,7 @@ int ikm_run_monitor(char *monitor_name, int argc, char **argv) if (config_trace) { inst = ikm_setup_trace_instance(nested_name); if (!inst) - return -1; + goto out_free_instance; } retval = ikm_enable(full_name); diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py index 3be7f85fe37b..5c923dc10d0f 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -18,14 +18,16 @@ if __name__ == '__main__': import sys parser = argparse.ArgumentParser(description='Generate kernel rv monitor') - parser.add_argument("-D", "--description", dest="description", required=False) - parser.add_argument("-a", "--auto_patch", dest="auto_patch", + + parent_parser = argparse.ArgumentParser(add_help=False) + parent_parser.add_argument("-D", "--description", dest="description", required=False) + parent_parser.add_argument("-a", "--auto_patch", dest="auto_patch", action="store_true", required=False, help="Patch the kernel in place") subparsers = parser.add_subparsers(dest="subcmd", required=True) - monitor_parser = subparsers.add_parser("monitor") + monitor_parser = subparsers.add_parser("monitor", parents=[parent_parser]) monitor_parser.add_argument('-n', "--model_name", dest="model_name") monitor_parser.add_argument("-p", "--parent", dest="parent", required=False, help="Create a monitor nested to parent") @@ -36,7 +38,7 @@ if __name__ == '__main__': monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True, help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") - container_parser = subparsers.add_parser("container") + container_parser = subparsers.add_parser("container", parents=[parent_parser]) container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) params = parser.parse_args() diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index e6f476b903b0..110cfd69e53a 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -215,14 +215,14 @@ class ha2k(dot2k): def __get_constraint_env(self, constr: str) -> str: """Extract the second argument from an ha_ function""" env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",") - assert env.rstrip(f"_{self.name}") in self.envs + assert env.removesuffix(f"_{self.name}") in self.envs return env def __start_to_invariant_check(self, constr: str) -> str: # by default assume the timer has ns expiration env = self.__get_constraint_env(constr) clock_type = "ns" - if self.env_types.get(env.rstrip(f"_{self.name}")) == "j": + if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j": clock_type = "jiffy" return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index 7f538598a868..016e7cf93bbb 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -122,10 +122,8 @@ class ASTNode: return self.op.expand(self, node, node_set) def __str__(self): - if isinstance(self.op, Literal): - return str(self.op.value) - if isinstance(self.op, Variable): - return self.op.name.lower() + if isinstance(self.op, (Literal, Variable)): + return str(self.op) return "val" + str(self.id) def normalize(self): @@ -382,6 +380,9 @@ class Variable: def __iter__(self): yield from () + def __str__(self): + return self.name.lower() + def negate(self): new = ASTNode(self) return NotOp(new) diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c index bf0999f6657a..889446760e3c 100644 --- a/tools/verification/rvgen/rvgen/templates/dot2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -35,7 +35,7 @@ static int enable_%%MODEL_NAME%%(void) { int retval; - retval = da_monitor_init(); + retval = %%MONITOR_CLASS%%_monitor_init(); if (retval) return retval; @@ -50,7 +50,7 @@ static void disable_%%MODEL_NAME%%(void) %%TRACEPOINT_DETACH%% - da_monitor_destroy(); + %%MONITOR_CLASS%%_monitor_destroy(); } /* |