diff options
Diffstat (limited to 'tools/verification/rvgen')
| -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 |
4 files changed, 15 insertions, 12 deletions
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(); } /* |