#!/usr/bin/env python3
"""Position-independence lint: the property that lets the identical image run
from any slot, asserted from the built ELF and its object.

  1. No absolute jmp/call — -mrelax normally guarantees it, but a branch that
     grows out of relaxation range would break it silently.
  2. Nothing flash-resident to address: the image is .text alone, so there is
     no table whose runtime address has to be reconstructed.
  3. The image is byte-identical when linked at a different base. This is
     position independence itself rather than a proxy for it — an absolute
     address anywhere in the image would move with the link and show up as a
     differing byte.

Usage: check_pi.py <objdump> <objcopy> <cxx> <mcu> <elf> <object> <text_start_hex>
"""

import os
import re
import subprocess
import sys
import tempfile


def fail(message):
    print(f"FAIL: {message}")
    sys.exit(1)


def main():
    objdump, objcopy, cxx, mcu, elf, obj, text_start = sys.argv[1:]
    text_start = int(text_start, 0)

    listing = subprocess.run([objdump, "-d", elf], capture_output=True, text=True, check=True).stdout
    absolute = [line for line in listing.splitlines() if re.search(r"\t(jmp|call)\t", line)]
    if absolute:
        fail("absolute control flow in the image:\n" + "\n".join(absolute))

    # Allocated flash beyond .text would be data the running copy has to find.
    # Only ALLOC sections reach the device at all; .comment and the debug
    # sections ride along in the ELF container and are never flashed. objdump
    # prints each section's flags on the line following its header.
    headers = subprocess.run([objdump, "-h", elf], capture_output=True, text=True, check=True).stdout.splitlines()
    for index, line in enumerate(headers):
        fields = line.split()
        if len(fields) < 6 or not fields[0].isdigit():
            continue
        name, size = fields[1], int(fields[2], 16)
        flags = headers[index + 1] if index + 1 < len(headers) else ""
        if "ALLOC" not in flags or not size:
            continue
        if name not in (".text", ".noinit", ".bss"):
            fail(f"flash-resident section {name} ({size} bytes): the image must be .text alone")

    # Relink at a different base and compare the bytes.
    with tempfile.TemporaryDirectory() as work:
        elsewhere = text_start - 0x200 if text_start >= 0x200 else text_start + 0x200
        images = []
        for base, tag in ((text_start, "here"), (elsewhere, "there")):
            relinked = os.path.join(work, f"{tag}.elf")
            binary = os.path.join(work, f"{tag}.bin")
            subprocess.run(
                [cxx, f"-mmcu={mcu}", "-nostartfiles", f"-Wl,--section-start=.text={base:#x}",
                 "-Wl,--defsym=pureboot_app=0", "-mrelax", obj, "-o", relinked],
                check=True, capture_output=True)
            subprocess.run([objcopy, "-O", "binary", relinked, binary], check=True)
            images.append(open(binary, "rb").read())
        if images[0] != images[1]:
            differing = [i for i, (a, b) in enumerate(zip(*images)) if a != b]
            fail(f"the image changes when linked at {elsewhere:#x} instead of {text_start:#x}: "
                 f"{len(differing)} byte(s) differ, first at offset {differing[0]:#x}")

    print(f"PI lint: control flow PC-relative, .text only, identical linked at {text_start:#x} and {elsewhere:#x}")


if __name__ == "__main__":
    main()