aboutsummaryrefslogtreecommitdiff
path: root/tools/verification
diff options
context:
space:
mode:
Diffstat (limited to 'tools/verification')
-rw-r--r--tools/verification/rv/src/in_kernel.c65
-rw-r--r--tools/verification/rvgen/__main__.py10
-rw-r--r--tools/verification/rvgen/rvgen/dot2k.py4
-rw-r--r--tools/verification/rvgen/rvgen/ltl2ba.py9
-rw-r--r--tools/verification/rvgen/rvgen/templates/dot2k/main.c4
5 files changed, 51 insertions, 41 deletions
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();
}
/*
generated by cgit