tools: type annotations for condition.py

- add type annotations for pylance/strict:
- add some comments
- rename "helper" to something more useful
- add typing assertions where the code makes assumptions about the
  shape of the XML tree. Apart from these added assertions, there
  should be no behaviour change.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

VERSION

@@ -1 +1 @@
-15.0.0
+15.0.0-dev

tools/condition.py

@@ -3,13 +3,29 @@
 # SPDX-License-Identifier: BSD-2-Clause or GPL-2.0-only
 #
 
-def remove_ws_comments(node):
+# Utility functions for processing condition tags in the seL4 xml files
+
+from __future__ import annotations
+
+from typing import List, Sequence, cast
+from xml.dom.minidom import Element
+
+
+def remove_ws_comments(node: Element) -> None:
+    """Remove whitespace and comment nodes from the children of the given node.
+    Assume being called on a condition tag that only has one child element apart
+    from whitespace and comments."""
     for child in list(node.childNodes):
         if child.nodeType == node.COMMENT_NODE or (child.nodeType == node.TEXT_NODE and len(child.data.strip()) == 0):
             node.removeChild(child)
+    # childNodes are of type _ElementChildren where
+    # _ElementChildren: TypeAlias = Element | ProcessingInstruction | Comment | Text | CDATASection
+    # At most one node of type Element should be left. Length is checked elsewhere, only assert type here.
+    assert all(isinstance(child, Element) for child in node.childNodes)
 
 
-def condition_to_cpp(conditions):
+def condition_to_cpp(conditions: Sequence[Element]) -> str:
+    """Convert the given condition tags list (0 or 1 tags) to a C preprocessor expression."""
     n = len(conditions)
     # Expect zero or one <condition> tag in the conditions list.
     assert n <= 1
@@ -23,45 +39,49 @@ def condition_to_cpp(conditions):
     # Expect that a condition tag has exactly one child node.
     assert len(children) == 1
 
-    def helper(expr):
+    def expr_to_cpp(expr: Element) -> str:
         remove_ws_comments(expr)
+        child_elems: list[Element] = cast(List[Element], list(expr.childNodes))
         if expr.tagName == "config":
             cfg_var = expr.getAttribute("var")
             if not cfg_var:
                 raise Exception("Missing or empty config variable")
             return "defined({})".format(cfg_var)
         elif expr.tagName == "not":
-            return "!{}".format(helper(expr.firstChild))
+            return "!{}".format(expr_to_cpp(child_elems[0]))
         else:
             op_str = {'and': ' && ', 'or': ' || '}.get(expr.tagName)
             if op_str:
-                return '(' + op_str.join([helper(e) for e in expr.childNodes]) + ')'
+                return '(' + op_str.join([expr_to_cpp(e) for e in child_elems]) + ')'
 
             raise Exception("Unrecognized element `{}` in condition".format(expr.tagName))
 
-    return helper(children[0])
+    return expr_to_cpp(cast(Element, children[0]))
 
 
-def remove_prefix(text, prefix) -> str:
+def remove_prefix(text: str, prefix: str) -> str:
     if text.startswith(prefix):
         return text[len(prefix):]
     return text
 
 
-def expr_to_bool(expr, values) -> bool:
+def expr_to_bool(expr: Element, values: dict[str, bool]) -> bool:
+    """Evaluate the given condition expression in the provided values environment."""
+    # Cast is safe, because the expr element comes out of remove_ws_comments
+    child_elems: list[Element] = cast(List[Element], list(expr.childNodes))
     if expr.tagName == "and":
-        for child in expr.childNodes:
+        for child in child_elems:
             if not expr_to_bool(child, values):
                 return False
         return True
     elif expr.tagName == "or":
-        for child in expr.childNodes:
+        for child in child_elems:
             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)
+        assert len(child_elems) == 1
+        return not expr_to_bool(child_elems[0], values)
     elif expr.tagName == "config":
         cfg_var = expr.getAttribute("var")
         if not cfg_var:
@@ -71,8 +91,8 @@ def expr_to_bool(expr, values) -> bool:
     raise Exception("Unrecognized element `{}` in condition".format(expr.tagName))
 
 
-# values to match on conditions and resolve them
-def condition_to_bool(conditions, values) -> bool:
+def condition_to_bool(conditions: Sequence[Element], values: dict[str, bool]) -> bool:
+    """Evaluate the given condition tags list (0 or 1 tags) in the provided values environment."""
     n = len(conditions)
     # Expect zero or one <condition> tag in the conditions list.
     assert n <= 1
@@ -86,6 +106,7 @@ def condition_to_bool(conditions, values) -> bool:
     # Expect that a condition tag has exactly one child node.
     assert len(children) == 1
 
-    remove_ws_comments(children[0])
+    child = cast(Element, children[0])
+    remove_ws_comments(child)
 
-    return expr_to_bool(children[0], values)
+    return expr_to_bool(child, values)

tools/reciprocal.py

@@ -13,15 +13,18 @@
 
 # for details on how this script works,
 # see Hacker's delight, Chapter 10, unsigned division.
-from math import floor, ceil
+
+# Note that you need an intermediate value that is 128 bits wide for the
+# multiplication if want to guarantee absence of overflow when you have a 64 bit
+# divisor.
+
+from __future__ import annotations
+
 import argparse
 import sys
-from past.builtins import xrange
-
-# now unsigned
 
 
-def magicgu(nmax, d):
+def magicgu(nmax: int, d: int) -> tuple[int, int]:
     nc = ((nmax + 1)//d)*d - 1
     nbits = len(bin(nmax)) - 2
     for p in range(0, 2*nbits + 1):
@@ -32,7 +35,7 @@ def magicgu(nmax, d):
     sys.exit(1)
 
 
-def do_div(n):
+def do_div(n: int) -> int:
     return ((n + add_ind) * magic) >> shift_amt
 
 
@@ -49,7 +52,7 @@ if __name__ == "__main__":
 
     print("Doing sanity check")
     # sanity check
-    for i in xrange(2**32-1):
+    for i in range(2**32-1):
         q1, q2 = (i / args.divisor, do_div(i))
         if int(q1) != q2:
             print("Combination failed %d %d %d" % i, q1, q2)

tools/umm.py

@@ -5,14 +5,30 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
+from __future__ import annotations
+
 import sys
 from functools import reduce
+from typing import Callable, Dict, IO, Iterable, Iterator, Tuple, TypeVar, Union
+from typing_extensions import TypeAlias
+
+UmmType: TypeAlias = Union[
+    Tuple[str],                    # Unit
+    Tuple[str, str],               # Word (size) or Base (name)
+    Tuple[str, 'UmmType'],         # Ptr (type)
+    Tuple[str, 'UmmType', str],    # Array of (type, size)
+]
+
+Field: TypeAlias = Tuple[str, UmmType]
+TypeMap: TypeAlias = Dict[str, Iterable[Field]]
+
+T = TypeVar('T')
+
 
 # We assume length tp > 0
 
-
-def parse_type(tps):
-    def helper(tps):
+def parse_type(tps: list[str]) -> UmmType:
+    def helper(tps: list[str]) -> tuple[UmmType, list[str]]:
         tp = tps[0]
         rest = tps[1:]
 
@@ -28,7 +44,7 @@ def parse_type(tps):
 
         elif tp == 'Array':
             tp2, rest = helper(rest)
-            # arrays are Array ... sz
+            # arrays are Array, type, size
             return ('Array', tp2, rest[0]), rest[1:]
 
         else:
@@ -37,8 +53,8 @@ def parse_type(tps):
     return helper(tps)[0]
 
 
-def splitBy(f, xs):
-    def fold(acc, v):
+def splitBy(f: Callable[[T], bool], xs: Iterable[T]) -> list[list[T]]:
+    def fold(acc: tuple[list[list[T]], list[T]], v: T) -> tuple[list[list[T]], list[T]]:
         if f(v):
             acc[0].append(acc[1])
             return (acc[0], [])
@@ -49,8 +65,8 @@ def splitBy(f, xs):
     return (reduce(fold, xs, ([], [])))[0]
 
 
-def handle_one_struct(s):
-    def hdl_fld(f):
+def handle_one_struct(s: list[str]) -> tuple[str, Iterator[Field]]:
+    def hdl_fld(f: str) -> Field:
         fl, tp = f.split(':')
         return (fl.lstrip(), parse_type(tp.split(' ')))
 
@@ -58,26 +74,31 @@ def handle_one_struct(s):
     return (name, map(hdl_fld, s[1:]))
 
 
-def dict_from_list(ls):
-    a = {}
+def dict_from_list(ls: Iterable[tuple[str, Iterable[Field]]]) -> TypeMap:
+    a: TypeMap = {}
     for k, v in ls:
         a[k] = v
 
     return a
 
 
-def is_base(x):
+def is_base(x: UmmType) -> bool:
     return (x[0] == 'Base')
 
 
-def base_name(x):
+def base_name(x: UmmType) -> str:
+    assert is_base(x) and len(x) == 2 and isinstance(x[1], str)
     return x[1]
 
 
-def paths_to_type(mp, f, start):
+def paths_to_type(
+    mp: TypeMap,
+    f: Callable[[UmmType], bool],
+    start: str,
+) -> list[tuple[list[str], UmmType]]:
     # This assumes that membership is a DAG which is the case in C
 
-    def handle_one(fld):
+    def handle_one(fld: Field) -> list[tuple[list[str], UmmType]]:
         name, tp = fld
         if f(tp):
             return [([start + '.' + name], tp)]
@@ -90,7 +111,7 @@ def paths_to_type(mp, f, start):
             return []
 
     # init case
-    start_tp = ('Base', start)
+    start_tp: UmmType = ('Base', start)
     if f(start_tp):
         return [([], start_tp)]
     else:
@@ -98,7 +119,7 @@ def paths_to_type(mp, f, start):
         return (reduce(lambda x, y: x + y, res))
 
 
-def build_types(file):
+def build_types(file: str) -> TypeMap:
     in_file = open(file, 'r', encoding='utf-8')
 
     lines = map(lambda x: x.rstrip(), in_file.readlines())
@@ -113,19 +134,17 @@ def build_types(file):
     return sts
 
 
-def print_graph(filename, out_file):
+def print_graph(filename: str, out_file: IO[str]) -> None:
     mp = build_types(filename)
 
     print('digraph types {', file=out_file)
-    for k, flds in mp.iteritems():
+    for k, flds in mp.items():
         for fld, tp in flds:
             # if is_base(tp):
             print('\t "%s" -> "%s" [label="%s"]' % (k, base_name(tp), fld),
                   file=out_file)
     print('}', file=out_file)
 
-# Toplevel
-
 
 if __name__ == '__main__':
     print_graph('umm_types.txt', sys.stdout)