darling-lol/tools/riot-lsem-model/extract-lsem.py

#!/usr/bin/env python3
"""Copy the shipped process-local Mach semaphore code out of mach_traps.c into lsem-shipped.inc.

The host model (lsem-model.c) compiles this file instead of a hand-written copy, so the model always exercises the
code that ships: the (name, generation, value) table, the trap entry points and the create/destroy wrappers are
extracted verbatim. Only the platform edges (raw syscalls, darlingserver RPCs, logging) are shimmed by the model.

The extraction is deliberately strict: every function must be found exactly once and the token take must still be the
generation-checked compare-exchange on the value+generation word. If somebody changes the shipped protocol, this
fails instead of silently modelling something else.

Usage: python3 extract-lsem.py [path/to/mach_traps.c]   (writes build/riot-lsem-model/lsem-shipped.inc; run.sh does all steps)
"""
from pathlib import Path
import re
import sys

HERE = Path(__file__).resolve().parent
ROOT = HERE.parent.parent
OUT_DIR = ROOT / 'build/riot-lsem-model'
DEFAULT_SRC = (ROOT / 'build/darling-src/src/external/xnu/darling/src/libsystem_kernel/emulation/'
               'src/xnu_syscall/mach/impl/mach_traps.c')

BLOCK_START = '#define LSEM_SLOTS'
BLOCK_END = 'static volatile int lsem_lock;'

# In dependency order (the trap entry points are declared in the model's shim section, so post_signal may call one).
FUNCTIONS = [
    'lsem_log',
    'lsem_decide',
    'lsem_hash',
    'lsem_capture',
    'lsem_find',
    'lsem_table_lock',
    'lsem_table_unlock',
    'lsem_insert',
    'lsem_remove',
    'lsem_signal',
    'lsem_signal_all',
    'lsem_signal_thread',
    'lsem_post_signal',
    'lsem_wait',
    'semaphore_create',
    'semaphore_destroy',
    '__darling_local_semaphores_after_fork',
    'semaphore_signal_trap_impl',
    'semaphore_signal_all_trap_impl',
    'semaphore_signal_thread_trap_impl',
    'semaphore_wait_trap_impl',
    'semaphore_wait_signal_trap_impl',
    'semaphore_timedwait_trap_impl',
    'semaphore_timedwait_signal_trap_impl',
]

# Assertions on the extracted text: the model must not model a protocol the shipped code no longer uses.
REQUIRED = [
    'compare_exchange_n(&s->pv.pair',       # the generation-checked token take
    'old - 1',                              # ... that decrements the value
    '(unsigned int) (old >> 32) != gen',    # ... after checking the generation it loaded
    'LSEM_FUTEX_PRIVATE',                   # every futex is process-private
    'LSEM_TOMB_VALUE',                      # the destroy tombstone is a negative value ...
    '(int) (unsigned int) old < 0',         # ... that no operation can take for a live count
    '__darling_local_semaphores_after_fork',
    # the destroy itself must write that value, not a literal (a positive tombstone is the in-flight bug)
    '(((old >> 32) + 1) << 32) | (unsigned int) LSEM_TOMB_VALUE',
]
# A positive tombstone literal anywhere is the bug this task fixed: fail loudly instead of modelling it.
FORBIDDEN = ['0x40000000']


def extract_block(lines):
    start = end = None
    for i, line in enumerate(lines):
        if line.startswith(BLOCK_START) and start is None:
            start = i
        if line.strip() == BLOCK_END:
            end = i
    if start is None or end is None or end <= start:
        sys.exit('extract-lsem: the LSEM define/table block was not found')
    return lines[start:end + 1]


def extract_function(lines, name):
    pattern = re.compile(r'^[ \t]*(?:static[ \t]+)?(?:inline[ \t]+)?[A-Za-z_][A-Za-z0-9_ \t\*]*\b'
                         + re.escape(name) + r'[ \t]*\(')
    hits = []
    for i, line in enumerate(lines):
        if pattern.match(line) and ';' not in line:
            for j in range(i, min(i + 400, len(lines))):
                if lines[j].rstrip('\n') == '}':
                    hits.append((i, j))
                    break
    if len(hits) != 1:
        sys.exit(f'extract-lsem: expected exactly one definition of {name}, found {hits}')
    i, j = hits[0]
    first = i
    while first > 0 and (lines[first - 1].strip() == 'VISIBLE'
                         or lines[first - 1].startswith('__attribute__')):
        first -= 1
    return lines[first:j + 1]


def main():
    src = Path(sys.argv[1]) if len(sys.argv) > 1 else DEFAULT_SRC
    lines = src.read_text().splitlines(keepends=True)
    chunks = [['/* generated by extract-lsem.py from ' + str(src) + ' -- do not edit */\n\n'],
              extract_block(lines)]
    for name in FUNCTIONS:
        chunks.append(['\n'])
        chunks.append(extract_function(lines, name))
    text = ''.join(''.join(chunk) for chunk in chunks)
    for needle in REQUIRED:
        if needle not in text:
            sys.exit(f'extract-lsem: the shipped code no longer contains {needle!r}: review the model')
    for needle in FORBIDDEN:
        if needle in text:
            sys.exit(f'extract-lsem: the shipped code contains {needle!r}, which is the fixed bug: review the model')
    OUT_DIR.mkdir(parents=True, exist_ok=True)
    out = OUT_DIR / 'lsem-shipped.inc'
    out.write_text(text)
    print(f'extract-lsem: wrote {out} ({len(text.splitlines())} lines, {len(FUNCTIONS)} functions)')


if __name__ == '__main__':
    main()