Export invocation numbers to JSON file

Co-authored-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>

tmp

CMakeLists.txt

@@ -35,6 +35,7 @@ RequireTool(CONFIG_GEN_PATH config_gen.py)
 RequireTool(BF_GEN_PATH bitfield_gen.py)
 RequireTool(HARDWARE_GEN_PATH hardware_gen.py)
 RequireTool(INVOCATION_ID_GEN_PATH invocation_header_gen.py)
+RequireTool(INVOCATION_JSON_GEN_PATH invocation_json_gen.py)
 RequireTool(SYSCALL_ID_GEN_PATH syscall_header_gen.py)
 RequireTool(XMLLINT_PATH xmllint.sh)
 
@@ -430,6 +431,37 @@ gen_invocation_header(
 list(APPEND xml_headers "${header_dest}")
 list(APPEND gen_files_list "${header_dest}")
 
+get_absolute_source_or_binary(
+    invocations_absolute "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/interfaces/object-api.xml"
+)
+get_absolute_source_or_binary(
+    arch_invocations_absolute
+    "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/arch_include/${KernelArch}/interfaces/object-api-arch.xml"
+)
+get_absolute_source_or_binary(
+    sel4_arch_invocations_absolute
+    "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/sel4_arch_include/${KernelSel4Arch}/interfaces/object-api-sel4-arch.xml"
+)
+
+add_custom_command(
+    OUTPUT generated/invocations_all.json
+    COMMAND rm -f generated/invocations_all.json
+    COMMAND
+        "${PYTHON3}" "${INVOCATION_JSON_GEN_PATH}"
+        --gen_config gen_config/kernel/gen_config.json
+        --invocations "${invocations_absolute}"
+        --arch_invocations "${arch_invocations_absolute}"
+        --sel4_arch_invocations "${sel4_arch_invocations_absolute}"
+        --dest generated/invocations_all.json
+    DEPENDS
+        "gen_config/kernel/gen_config.json"
+        "${INVOCATION_JSON_GEN_PATH}"
+        "${invocations_absolute}"
+        "${arch_invocations_absolute}"
+        "${sel4_arch_invocations_absolute}"
+)
+list(APPEND gen_files_list "generated/invocations_all.json")
+
 set(syscall_xml_base "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/api")
 set(syscall_dest "gen_headers/arch/api/syscall.h")
 if(KernelIsMCS)

tools/condition.py

@@ -40,3 +40,46 @@ def condition_to_cpp(conditions):
             raise Exception("Unrecognized element `{}` in condition".format(expr.tagName))
 
     return helper(children[0])
+
+
+def expr_to_bool(expr, values) -> bool:
+    if expr.tagName == "and":
+        for child in expr.childNodes:
+            if not expr_to_bool(child, values):
+                return False
+        return True
+    elif expr.tagName == "or":
+        for chlid in expr.childNodes:
+            if expr_to_bool(child, values):
+                return True
+        return False
+    elif expr.tagName == "not":
+        assert len(expr.childNodes) == 1
+        return not expr_to_bool(expr.childNodes[0], values)
+    elif expr.tagName == "config":
+        cfg_var = expr.getAttribute("var")
+        if not cfg_var:
+            raise Exception("Missing or empty config variable")
+
+        return values[cfg_var.removeprefix("CONFIG_")]
+    raise Exception("Unrecognized element `{}` in condition".format(expr.tagName))
+
+
+# values to match on conditions and resolve them
+def condition_to_bool(conditions, values) -> bool:
+    n = len(conditions)
+    # Expect zero or one <condition> tag in the conditions list.
+    assert n <= 1
+    if n == 0:
+        return True
+
+    remove_ws_comments(conditions[0])
+    children = conditions[0].childNodes
+    if not children or len(children) == 0:
+        return True
+    # Expect that a condition tag has exactly one child node.
+    assert len(children) == 1
+
+    remove_ws_comments(children[0])
+
+    return expr_to_bool(children[0], values)

tools/invocation_json_gen.py

@@ -0,0 +1,65 @@
+#!/usr/bin/env python3
+#
+# Copyright 2024, UNSW Sydney
+#
+# SPDX-License-Identifier: BSD-2-Clause or GPL-2.0-only
+#
+
+import argparse
+import json
+import xml.dom.minidom
+from condition import condition_to_bool
+
+
+def parse_args():
+    parser = argparse.ArgumentParser(description='Generate JSON file containing list of seL4 \
+                                    invocations.')
+    parser.add_argument('--gen_config', type=argparse.FileType('r'),
+                        help="Location of gen_config JSON file", required=True)
+    parser.add_argument('--invocations', type=argparse.FileType('r'),
+                        help='Location of XML file with invocation definitions', required=True)
+    parser.add_argument('--arch_invocations', type=argparse.FileType('r'),
+                        help='Location of XML file with arch invocation defintions', required=True)
+    parser.add_argument('--sel4_arch_invocations', type=argparse.FileType('r'),
+                        help='Location of XML file with seL4 arch invocation definitions', required=True)
+    parser.add_argument('--dest', type=argparse.FileType('w+'),
+                        help='Location of JSON file to store invocations', required=True)
+
+    return parser.parse_args()
+
+
+def xml_to_json_invocations(xml, gen_config, counter, invocations_dict, ):
+    for method in xml.getElementsByTagName("method"):
+        label = str(method.getAttribute("id"))
+        exists = condition_to_bool(method.getElementsByTagName("condition"), gen_config)
+        if exists:
+            invocations_dict[label] = counter
+            counter += 1
+
+    return counter
+
+
+if __name__ == "__main__":
+    args = parse_args()
+
+    try:
+        invocations = xml.dom.minidom.parse(args.invocations)
+        arch_invocations = xml.dom.minidom.parse(args.arch_invocations)
+        sel4_arch_invocations = xml.dom.minidom.parse(args.sel4_arch_invocations)
+    except:
+        print('Error: invalid XML file provided', file=sys.stderr)
+        sys.exit(1)
+
+    try:
+        gen_config = json.load(args.gen_config)
+    except:
+        print('Error: invalid JSON file provided', file=sys.stderr)
+        sys.exit(1)
+
+    invocations_dict = {}
+    counter = 1
+    counter = xml_to_json_invocations(invocations, gen_config, counter, invocations_dict)
+    counter = xml_to_json_invocations(sel4_arch_invocations, gen_config, counter, invocations_dict)
+    counter = xml_to_json_invocations(arch_invocations, gen_config, counter, invocations_dict)
+
+    json.dump(invocations_dict, args.dest)