From 3e085a7cdd0b98a4b1056125ecba6a0d7c974126 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:17:31 +0200 Subject: [PATCH 1/9] test: add C++ parameterized symbols for demangle proof --- test/test.cpp | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/test/test.cpp b/test/test.cpp index 931d82b..e9cccf7 100644 --- a/test/test.cpp +++ b/test/test.cpp @@ -2,6 +2,45 @@ #include #include +namespace demo_symbols +{ +struct Sample +{ + int value; +}; + +int scalar_parameters(int value, double scale, char tag) +{ + if (value > 0 && scale > 0.0 && tag != '\0') + return 1; + return 0; +} + +long pointer_parameters(const int* value, const char* label, bool enabled) +{ + if (!value || !label || !enabled) + return 0; + return (*value > 0 && label[0] != '\0') ? 1L : 0L; +} + +double reference_parameters(const Sample& sample, float ratio, unsigned long count) +{ + if (sample.value > 0 && ratio > 0.0f && count > 0) + return 1.0; + return 0.0; +} + +int overloaded(int value) +{ + return value == 0 ? 0 : 1; +} + +int overloaded(int lhs, int rhs) +{ + return lhs < rhs ? 1 : 0; +} +} // namespace demo_symbols + void toto(void) { char test[100]; @@ -29,6 +68,7 @@ int main(void) int b = 10; int sum = a + b; const bool is_ok = false; + demo_symbols::Sample sample{sum}; if (is_ok) { @@ -39,5 +79,11 @@ int main(void) tutu(); + sum += demo_symbols::scalar_parameters(a, 2.5, 'x'); + sum += static_cast(demo_symbols::pointer_parameters(&sum, "label", true)); + sum += static_cast(demo_symbols::reference_parameters(sample, 1.5f, 3UL)); + sum += demo_symbols::overloaded(sum); + sum += demo_symbols::overloaded(a, b); + return sum; } From 26325b148fb46359682eede14eaebfe187b60100 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:17:47 +0200 Subject: [PATCH 2/9] test: add combined stack analyzer proof helper --- BTP-STACK-ANALYER.py | 469 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 469 insertions(+) create mode 100755 BTP-STACK-ANALYER.py diff --git a/BTP-STACK-ANALYER.py b/BTP-STACK-ANALYER.py new file mode 100755 index 0000000..2dca330 --- /dev/null +++ b/BTP-STACK-ANALYER.py @@ -0,0 +1,469 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for stack_usage_analyzer feature checks. + +The analyzer's human output prints demangled names when --demangle is enabled, +while its JSON report keeps the raw IR symbol names. Running both modes with +--demangle gives a stable tool-level proof without relying on hardcoded fixture +names or external demangling tools. + +The stack-buffer-overflow proof intentionally reuses the repository security +fixture instead of generating temporary C/C++ source. That keeps the proof tied +to the same static-analysis contract exercised by the normal test suite. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Sequence + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +DEFAULT_STACK_BUFFER_FIXTURE = Path("test/security/buffer-overflow/01_buffer_overflow.c") +SUPPORTED_SOURCE_SUFFIXES = { + ".c", + ".cc", + ".cpp", + ".cxx", + ".c++", +} +FUNCTION_LINE_RE = re.compile(r"^Function:\s*(?P.+?)\s*$") + + +@dataclass(frozen=True) +class AnalyzerCommand: + argv: tuple[str, ...] + + +@dataclass(frozen=True) +class FunctionNamePair: + mangled: str + demangled: str + + +@dataclass(frozen=True) +class StackBufferOverflowProof: + fixture: Path + function: str + variable: str + rule_id: str + severity: str + message: str + + +def parse_args(argv: Sequence[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=( + "Run stack_usage_analyzer proof checks for demangling and static " + "stack-buffer overflow diagnostics." + ), + epilog="Extra stack_usage_analyzer arguments can be appended after '--'.", + ) + parser.add_argument( + "source", + nargs="?", + type=Path, + help="C or C++ source file used by the demangle proof.", + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help=( + "Path to stack_usage_analyzer. Defaults to CORETRACE_STACK_ANALYZER " + "or ./build/stack_usage_analyzer." + ), + ) + parser.add_argument( + "--proof", + choices=("demangle", "stack-buffer-overflow", "all"), + default="demangle", + help=( + "Proof to run. 'demangle' keeps the original behavior, " + "'stack-buffer-overflow' uses an existing repository fixture, " + "and 'all' runs both." + ), + ) + parser.add_argument( + "--stack-buffer-fixture", + type=Path, + default=DEFAULT_STACK_BUFFER_FIXTURE, + help=( + "Existing C/C++ fixture used by --proof stack-buffer-overflow. " + "Defaults to test/security/buffer-overflow/01_buffer_overflow.c." + ), + ) + parser.add_argument( + "--only-function", + action="append", + default=[], + help=( + "Forwarded to the analyzer as --only-function= for the " + "demangle proof. Can be repeated." + ), + ) + parser.add_argument( + "--show-analyzer-output", + action="store_true", + help="Print captured analyzer stdout/stderr when the proof succeeds.", + ) + args, analyzer_args = parser.parse_known_args(argv) + args.analyzer_args = analyzer_args + return args + + +def normalize_extra_args(extra_args: Sequence[str]) -> list[str]: + args = list(extra_args) + if args and args[0] == "--": + return args[1:] + return args + + +def validate_analyzer(analyzer: Path) -> None: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + + +def validate_source_file(source: Path) -> None: + if not source.exists(): + raise FileNotFoundError(f"Input source not found: {source}") + if source.suffix.lower() not in SUPPORTED_SOURCE_SUFFIXES: + supported = ", ".join(sorted(SUPPORTED_SOURCE_SUFFIXES)) + raise ValueError(f"Expected a C/C++ source file ({supported}), got: {source}") + + +def build_analyzer_command( + analyzer: Path, + source: Path, + only_functions: Sequence[str], + extra_args: Sequence[str], + *, + output_json: bool, +) -> AnalyzerCommand: + argv = [ + str(analyzer), + str(source), + "--demangle", + "--print-effective-config", + ] + if output_json: + argv.append("--format=json") + for function_name in only_functions: + argv.append(f"--only-function={function_name}") + argv.extend(extra_args) + return AnalyzerCommand(tuple(argv)) + + +def build_stack_buffer_command( + analyzer: Path, + fixture: Path, + extra_args: Sequence[str], +) -> AnalyzerCommand: + argv = [ + str(analyzer), + str(fixture), + "--format=json", + ] + argv.extend(extra_args) + return AnalyzerCommand(tuple(argv)) + + +def run_analyzer(command: AnalyzerCommand) -> subprocess.CompletedProcess[str]: + return subprocess.run( + command.argv, + check=False, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + + +def require_success(result: subprocess.CompletedProcess[str], command: AnalyzerCommand) -> None: + if result.returncode == 0: + return + details = [ + f"Analyzer command failed with exit code {result.returncode}:", + " ".join(command.argv), + ] + if result.stdout: + details.extend(["--- stdout ---", result.stdout.rstrip()]) + if result.stderr: + details.extend(["--- stderr ---", result.stderr.rstrip()]) + raise RuntimeError("\n".join(details)) + + +def require_demangle_enabled(result: subprocess.CompletedProcess[str]) -> None: + effective_config = f"{result.stderr}\n{result.stdout}" + if "demangle: true" not in effective_config: + raise RuntimeError("The analyzer did not report 'demangle: true' in effective config.") + + +def parse_demangled_human_functions(stdout: str) -> list[str]: + names: list[str] = [] + for line in stdout.splitlines(): + match = FUNCTION_LINE_RE.match(line) + if match: + names.append(match.group("name").strip()) + return names + + +def parse_mangled_json_functions(stdout: str) -> list[str]: + payload = parse_json_report(stdout) + functions = payload.get("functions") + if not isinstance(functions, list): + raise ValueError("Analyzer JSON output does not contain a functions array.") + + names: list[str] = [] + for function in functions: + if not isinstance(function, dict): + continue + name = function.get("name") + if isinstance(name, str): + names.append(name) + return names + + +def parse_json_report(stdout: str) -> dict: + payload = json.loads(stdout) + if not isinstance(payload, dict): + raise ValueError("Analyzer JSON output is not a JSON object.") + return payload + + +def strip_llvm_symbol_prefix(symbol: str) -> str: + return symbol[1:] if symbol.startswith("\x01") else symbol + + +def is_itanium_mangled(symbol: str) -> bool: + normalized = strip_llvm_symbol_prefix(symbol) + return normalized.startswith("_Z") or normalized.startswith("__Z") + + +def collect_itanium_pairs(mangled_names: Sequence[str], demangled_names: Sequence[str]) -> list[FunctionNamePair]: + if len(mangled_names) != len(demangled_names): + raise RuntimeError( + "Human and JSON analyzer outputs returned different function counts " + f"({len(demangled_names)} human vs {len(mangled_names)} JSON)." + ) + + pairs: list[FunctionNamePair] = [] + for mangled, demangled in zip(mangled_names, demangled_names): + if not is_itanium_mangled(mangled): + continue + if is_itanium_mangled(demangled) or demangled == mangled: + raise RuntimeError( + "Demangle mode did not produce a stable demangled name for " + f"{mangled!r}; human output was {demangled!r}." + ) + pairs.append(FunctionNamePair(mangled=mangled, demangled=demangled)) + return pairs + + +def collect_stack_buffer_overflow_proofs(payload: dict, fixture: Path) -> list[StackBufferOverflowProof]: + diagnostics = payload.get("diagnostics") + if not isinstance(diagnostics, list): + raise ValueError("Analyzer JSON output does not contain a diagnostics array.") + + proofs: list[StackBufferOverflowProof] = [] + for diagnostic in diagnostics: + if not isinstance(diagnostic, dict): + continue + if diagnostic.get("severity") != "WARNING": + continue + if diagnostic.get("ruleId") != "StackBufferOverflow": + continue + + location = diagnostic.get("location") + details = diagnostic.get("details") + if not isinstance(location, dict) or not isinstance(details, dict): + continue + + message = details.get("message") + variable_aliasing = details.get("variableAliasing") + function = location.get("function") + if not isinstance(message, str) or not isinstance(function, str): + continue + if "stack buffer overflow on variable" not in message: + continue + if "buf" not in message: + continue + if isinstance(variable_aliasing, list) and "buf" not in variable_aliasing: + continue + + proofs.append( + StackBufferOverflowProof( + fixture=fixture, + function=function, + variable="buf", + rule_id="StackBufferOverflow", + severity="WARNING", + message=" ".join(message.split()), + ) + ) + return proofs + + +def print_demangle_result( + source: Path, + human_command: AnalyzerCommand, + json_command: AnalyzerCommand, + pairs: Sequence[FunctionNamePair], +) -> None: + print("Itanium ABI demangle proof: PASS") + print(f"input: {source}") + print("demangle-mode: enabled") + print(f"symbols-found: {len(pairs)}") + for pair in pairs: + print(f"mangled-symbol: {pair.mangled}") + print(f"demangled-symbol: {pair.demangled}") + print(f"human-command: {' '.join(human_command.argv)}") + print(f"json-command: {' '.join(json_command.argv)}") + + +def print_stack_buffer_overflow_result( + command: AnalyzerCommand, + proofs: Sequence[StackBufferOverflowProof], +) -> None: + print("Static stack-buffer overflow proof: PASS") + for proof in proofs: + print(f"fixture: {proof.fixture}") + print(f"rule-id: {proof.rule_id}") + print(f"severity: {proof.severity}") + print(f"function: {proof.function}") + print(f"stack-buffer: {proof.variable}") + print(f"diagnostic: {proof.message}") + print(f"json-command: {' '.join(command.argv)}") + + +def run_demangle_proof( + analyzer: Path, + source: Path, + only_functions: Sequence[str], + extra_args: Sequence[str], + *, + show_analyzer_output: bool, +) -> None: + validate_source_file(source) + + human_command = build_analyzer_command( + analyzer, + source, + only_functions, + extra_args, + output_json=False, + ) + json_command = build_analyzer_command( + analyzer, + source, + only_functions, + extra_args, + output_json=True, + ) + + human_result = run_analyzer(human_command) + require_success(human_result, human_command) + require_demangle_enabled(human_result) + + json_result = run_analyzer(json_command) + require_success(json_result, json_command) + require_demangle_enabled(json_result) + + demangled_names = parse_demangled_human_functions(human_result.stdout) + mangled_names = parse_mangled_json_functions(json_result.stdout) + pairs = collect_itanium_pairs(mangled_names, demangled_names) + if not pairs: + raise RuntimeError( + "No Itanium ABI mangled function symbol was found. A plain C file often emits " + "unmangled C symbols; use a C++ input or a C source with explicit Itanium " + "ABI asm labels to exercise this proof." + ) + + print_demangle_result(source, human_command, json_command, pairs) + + if show_analyzer_output: + print("--- analyzer human stdout ---") + print(human_result.stdout.rstrip()) + if human_result.stderr: + print("--- analyzer human stderr ---") + print(human_result.stderr.rstrip()) + print("--- analyzer json stdout ---") + print(json_result.stdout.rstrip()) + if json_result.stderr: + print("--- analyzer json stderr ---") + print(json_result.stderr.rstrip()) + + +def run_stack_buffer_overflow_proof( + analyzer: Path, + fixture: Path, + extra_args: Sequence[str], + *, + show_analyzer_output: bool, +) -> None: + validate_source_file(fixture) + + command = build_stack_buffer_command(analyzer, fixture, extra_args) + result = run_analyzer(command) + require_success(result, command) + + payload = parse_json_report(result.stdout) + proofs = collect_stack_buffer_overflow_proofs(payload, fixture) + if not proofs: + raise RuntimeError( + "No StackBufferOverflow warning was found for stack-allocated buffer 'buf' " + f"in fixture {fixture}." + ) + + print_stack_buffer_overflow_result(command, proofs) + + if show_analyzer_output: + print("--- analyzer json stdout ---") + print(result.stdout.rstrip()) + if result.stderr: + print("--- analyzer json stderr ---") + print(result.stderr.rstrip()) + + +def main(argv: Sequence[str]) -> int: + args = parse_args(argv) + source = args.source + analyzer = args.analyzer + extra_args = normalize_extra_args(args.analyzer_args) + + try: + validate_analyzer(analyzer) + + if args.proof in ("demangle", "all"): + if source is None: + raise ValueError("The demangle proof requires a C/C++ source argument.") + run_demangle_proof( + analyzer, + source, + args.only_function, + extra_args, + show_analyzer_output=args.show_analyzer_output, + ) + + if args.proof in ("stack-buffer-overflow", "all"): + run_stack_buffer_overflow_proof( + analyzer, + args.stack_buffer_fixture, + extra_args, + show_analyzer_output=args.show_analyzer_output, + ) + + return 0 + except Exception as exc: + print(f"stack_usage_analyzer proof: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From d33a9ad800b2551ace9c836fb344bb41916b2936 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:18:06 +0200 Subject: [PATCH 3/9] test: add F1 stack usage proof script --- BTP-STACK-ANALYZER-F1.py | 396 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 396 insertions(+) create mode 100755 BTP-STACK-ANALYZER-F1.py diff --git a/BTP-STACK-ANALYZER-F1.py b/BTP-STACK-ANALYZER-F1.py new file mode 100755 index 0000000..113dcbb --- /dev/null +++ b/BTP-STACK-ANALYZER-F1.py @@ -0,0 +1,396 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for stack usage analysis features. + +This script reuses repository fixtures and validates stack_usage_analyzer JSON +fields for: + - static stack size and call-chain propagation, + - VLA and alloca dynamic stack usage, + - unknown stack propagation, + - infinite recursion, + - stack pointer escapes. +""" + +from __future__ import annotations + +import argparse +import json +import os +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +ANALYZER_MODES = ("ir", "abi") +GREEN = "\033[32m" +RED = "\033[31m" +PURPLE = "\033[35m" +RESET = "\033[0m" +SEPARATOR = "--------" + + +def feature_reference_from_filename(path: Path) -> str: + marker = "-F" + if marker not in path.stem: + return "[F?]" + suffix = path.stem.rsplit(marker, 1)[1] + digits = "".join(char for char in suffix if char.isdigit()) + return f"[F{digits}]" if digits else "[F?]" + + +FEATURE_REF = feature_reference_from_filename(Path(__file__)) + + +def print_log(*args: object, **kwargs: Any) -> None: + print(FEATURE_REF, *args, **kwargs) + + +@dataclass(frozen=True) +class FixtureSet: + static_stack: Path = Path("test/local-storage/c/stack-callee-caller.c") + vla_unknown: Path = Path("test/vla/vla-unknown-stack.c") + alloca_dynamic: Path = Path("test/alloca/user-controlled.c") + infinite_recursion: Path = Path("test/recursion/c/infinite-recursion.c") + stack_escape: Path = Path("test/escape-stack/return-buf.c") + + +@dataclass(frozen=True) +class AnalyzerResult: + fixture: Path + requested_mode: str + command: tuple[str, ...] + payload: dict[str, Any] + + +@dataclass(frozen=True) +class ProofCheck: + name: str + found: bool + detail: str + + +def parse_args(argv: list[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description="Prove stack usage analysis features using existing test fixtures." + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help="Path to stack_usage_analyzer, or CORETRACE_STACK_ANALYZER.", + ) + parser.add_argument("--static-stack-fixture", type=Path, default=FixtureSet.static_stack) + parser.add_argument("--vla-fixture", type=Path, default=FixtureSet.vla_unknown) + parser.add_argument("--alloca-fixture", type=Path, default=FixtureSet.alloca_dynamic) + parser.add_argument("--recursion-fixture", type=Path, default=FixtureSet.infinite_recursion) + parser.add_argument("--escape-fixture", type=Path, default=FixtureSet.stack_escape) + return parser.parse_args(argv) + + +def run_analyzer(analyzer: Path, fixture: Path, mode: str) -> AnalyzerResult: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + if not fixture.exists(): + raise FileNotFoundError(f"Fixture not found: {fixture}") + + command = (str(analyzer), str(fixture), f"--mode={mode}", "--format=json") + result = subprocess.run(command, check=False, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if result.returncode != 0: + raise RuntimeError( + f"Analyzer failed for {fixture} with exit code {result.returncode}\n" + f"stdout:\n{result.stdout}\n" + f"stderr:\n{result.stderr}" + ) + + payload = json.loads(result.stdout) + if not isinstance(payload, dict): + raise ValueError(f"Analyzer output for {fixture} is not a JSON object.") + return AnalyzerResult(fixture=fixture, requested_mode=mode, command=command, payload=payload) + + +def reported_mode(payload: dict[str, Any]) -> str: + meta = payload.get("meta") + if not isinstance(meta, dict): + return "" + mode = meta.get("mode") + return mode if isinstance(mode, str) else "" + + +def functions_by_name(payload: dict[str, Any]) -> dict[str, dict[str, Any]]: + functions = payload.get("functions") + if not isinstance(functions, list): + raise ValueError("JSON report has no functions array.") + return { + item["name"]: item + for item in functions + if isinstance(item, dict) and isinstance(item.get("name"), str) + } + + +def diagnostics(payload: dict[str, Any]) -> list[dict[str, Any]]: + raw = payload.get("diagnostics") + if not isinstance(raw, list): + raise ValueError("JSON report has no diagnostics array.") + return [item for item in raw if isinstance(item, dict)] + + +def message_of(diag: dict[str, Any]) -> str: + details = diag.get("details") + if not isinstance(details, dict): + return "" + message = details.get("message") + return message if isinstance(message, str) else "" + + +def has_diag( + payload: dict[str, Any], + *, + rule_id: str | None = None, + severity: str | None = None, + function: str | None = None, + message_contains: tuple[str, ...] = (), +) -> bool: + for diag in diagnostics(payload): + if rule_id is not None and diag.get("ruleId") != rule_id: + continue + if severity is not None and diag.get("severity") != severity: + continue + location = diag.get("location") + if function is not None: + if not isinstance(location, dict) or location.get("function") != function: + continue + message = message_of(diag) + if all(needle in message for needle in message_contains): + return True + return False + + +def colored(text: str, color: str) -> str: + return f"{color}{text}{RESET}" + + +def status_label(found: bool) -> str: + return colored("PASS", GREEN) if found else colored("NONE", RED) + + +def require(condition: bool, proof: str, detail: str) -> ProofCheck: + return ProofCheck(name=proof, found=condition, detail=detail) + + +def print_report(result: AnalyzerResult, checks: list[ProofCheck]) -> None: + print_log(SEPARATOR) + print_log(colored(str(result.fixture), PURPLE)) + print_log(f"mode: {reported_mode(result.payload)}") + for check in checks: + print_log(f"- {check.name}: {status_label(check.found)}") + if not check.found: + print_log(f" detail: {check.detail}") + print_log(f"command: {' '.join(result.command)}") + + +def prove_static_stack(result: AnalyzerResult) -> list[ProofCheck]: + funcs = functions_by_name(result.payload) + foo = funcs.get("foo", {}) + bar = funcs.get("bar", {}) + mano = funcs.get("mano", {}) + foo_max = foo.get("maxStack") + bar_max = bar.get("maxStack") + mano_max = mano.get("maxStack") + return [ + require( + foo.get("localStack") == 8192000000 + and foo.get("maxStack") == 8192000000 + and foo.get("exceedsLimit") is True, + "static stack size", + "expected foo to expose a fixed oversized stack frame", + ), + require( + isinstance(foo_max, int) + and isinstance(bar_max, int) + and isinstance(mano_max, int) + and bar_max >= foo_max + and mano_max >= bar_max + and bar.get("exceedsLimit") is True + and mano.get("exceedsLimit") is True, + "static stack propagation", + "expected bar/mano to propagate foo's oversized stack through the call graph", + ), + require( + has_diag( + result.payload, + rule_id="StackFrameTooLarge", + severity="ERROR", + function="mano", + message_contains=("path: mano -> bar -> foo",), + ), + "stack overflow path diagnostic", + "expected call-chain diagnostic mano -> bar -> foo", + ), + ] + + +def prove_vla_unknown(result: AnalyzerResult) -> list[ProofCheck]: + funcs = functions_by_name(result.payload) + consume = funcs.get("consume", {}) + main = funcs.get("main", {}) + main_lower_bound = main.get("maxStackLowerBound") + return [ + require( + consume.get("hasDynamicAlloca") is True + and consume.get("localStackUnknown") is True + and consume.get("maxStackUnknown") is True + and consume.get("localStackLowerBound") == 32, + "VLA dynamic stack size", + "expected consume to have unknown local/max stack with a lower bound", + ), + require( + main.get("localStackUnknown") is False + and main.get("maxStackUnknown") is True + and isinstance(main_lower_bound, int) + and main_lower_bound >= 48, + "unknown stack propagation", + "expected main to propagate unknown stack usage from consume", + ), + require( + has_diag( + result.payload, + rule_id="VLAUsage", + severity="WARNING", + function="consume", + message_contains=("dynamic stack allocation", "VLA"), + ), + "VLA diagnostic", + "expected VLAUsage warning in consume", + ), + require( + has_diag( + result.payload, + rule_id="AllocaUserControlled", + severity="WARNING", + function="consume", + message_contains=("user-controlled alloca size",), + ), + "user-controlled VLA diagnostic", + "expected AllocaUserControlled warning in consume", + ), + ] + + +def prove_alloca(result: AnalyzerResult) -> list[ProofCheck]: + funcs = functions_by_name(result.payload) + foo = funcs.get("foo", {}) + return [ + require( + foo.get("hasDynamicAlloca") is True + and foo.get("localStackUnknown") is True + and foo.get("maxStackUnknown") is True, + "alloca dynamic stack size", + "expected foo to expose dynamic alloca as unknown stack usage", + ), + require( + has_diag( + result.payload, + rule_id="AllocaUserControlled", + severity="WARNING", + function="foo", + message_contains=("variable 'buf'", "stack usage grows with runtime value"), + ), + "alloca diagnostic", + "expected user-controlled alloca warning for buf", + ), + ] + + +def prove_infinite_recursion(result: AnalyzerResult) -> list[ProofCheck]: + funcs = functions_by_name(result.payload) + tutu = funcs.get("tutu", {}) + return [ + require( + tutu.get("isRecursive") is True and tutu.get("hasInfiniteSelfRecursion") is True, + "infinite recursion flags", + "expected tutu to be recursive with unconditional self-recursion", + ), + require( + has_diag( + result.payload, + severity="ERROR", + function="tutu", + message_contains=("unconditional self recursion", "overflow the stack"), + ), + "infinite recursion diagnostic", + "expected error diagnostic for unconditional self recursion", + ), + ] + + +def prove_stack_escape(result: AnalyzerResult) -> list[ProofCheck]: + return [ + require( + has_diag( + result.payload, + rule_id="StackPointerEscape", + severity="WARNING", + function="ret_buf", + message_contains=("address of variable 'buf' escapes", "return statement"), + ), + "stack pointer escape diagnostic", + "expected StackPointerEscape warning for returning buf", + ) + ] + + +def prove_mode(result: AnalyzerResult) -> list[ProofCheck]: + expected = result.requested_mode.upper() + observed = reported_mode(result.payload) + return [ + require( + observed == expected, + f"analyzer mode {expected}", + f"expected JSON meta.mode={expected}, got {observed}", + ) + ] + + +def main(argv: list[str]) -> int: + args = parse_args(argv) + try: + fixtures = FixtureSet( + static_stack=args.static_stack_fixture, + vla_unknown=args.vla_fixture, + alloca_dynamic=args.alloca_fixture, + infinite_recursion=args.recursion_fixture, + stack_escape=args.escape_fixture, + ) + reports: list[tuple[AnalyzerResult, list[ProofCheck]]] = [] + for mode in ANALYZER_MODES: + static = run_analyzer(args.analyzer, fixtures.static_stack, mode) + vla = run_analyzer(args.analyzer, fixtures.vla_unknown, mode) + alloca = run_analyzer(args.analyzer, fixtures.alloca_dynamic, mode) + recursion = run_analyzer(args.analyzer, fixtures.infinite_recursion, mode) + escape = run_analyzer(args.analyzer, fixtures.stack_escape, mode) + reports.extend( + [ + (static, prove_mode(static) + prove_static_stack(static)), + (vla, prove_mode(vla) + prove_vla_unknown(vla)), + (alloca, prove_mode(alloca) + prove_alloca(alloca)), + (recursion, prove_mode(recursion) + prove_infinite_recursion(recursion)), + (escape, prove_mode(escape) + prove_stack_escape(escape)), + ] + ) + all_checks = [check for _, checks in reports for check in checks] + all_found = all(check.found for check in all_checks) + + print_log(f"BTP-STACK-ANALYZER-F1: {status_label(all_found)}") + for result, checks in reports: + print_report(result, checks) + return 0 if all_found else 1 + except Exception as exc: + print_log(f"BTP-STACK-ANALYZER-F1: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From a1be8e69e84cb28e4520644ad1fd7014a8657c6a Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:18:17 +0200 Subject: [PATCH 4/9] test: add F2 advanced stack diagnostics proof script --- BTP-STACK-ANALYZER-F2.py | 315 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 315 insertions(+) create mode 100755 BTP-STACK-ANALYZER-F2.py diff --git a/BTP-STACK-ANALYZER-F2.py b/BTP-STACK-ANALYZER-F2.py new file mode 100755 index 0000000..78a967c --- /dev/null +++ b/BTP-STACK-ANALYZER-F2.py @@ -0,0 +1,315 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for memory intrinsic, aliasing, and const-correctness features. + +The script validates stack_usage_analyzer JSON diagnostics over existing +fixtures for: + - memcpy overflow, + - memset overflow, + - deep aliasing through stack-buffer bounds, + - basic pointer const-correctness suggestions. +""" + +from __future__ import annotations + +import argparse +import json +import os +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +GREEN = "\033[32m" +RED = "\033[31m" +PURPLE = "\033[35m" +RESET = "\033[0m" +SEPARATOR = "--------" + + +def feature_reference_from_filename(path: Path) -> str: + marker = "-F" + if marker not in path.stem: + return "[F?]" + suffix = path.stem.rsplit(marker, 1)[1] + digits = "".join(char for char in suffix if char.isdigit()) + return f"[F{digits}]" if digits else "[F?]" + + +FEATURE_REF = feature_reference_from_filename(Path(__file__)) + + +def print_log(*args: object, **kwargs: Any) -> None: + print(FEATURE_REF, *args, **kwargs) + + +@dataclass(frozen=True) +class FixtureSet: + memcpy_overflow: Path = Path("test/cpy-buffer/bad-usage-memcpy.c") + memset_overflow: Path = Path("test/cpy-buffer/bad-usage-memset.c") + deep_aliasing: Path = Path("test/bound-storage/deep-alias.c") + const_correctness: Path = Path("test/pointer_reference-const_correctness/readonly-pointer.c") + + +@dataclass(frozen=True) +class AnalyzerResult: + fixture: Path + command: tuple[str, ...] + payload: dict[str, Any] + + +@dataclass(frozen=True) +class ProofCheck: + name: str + found: bool + detail: str + + +def parse_args(argv: list[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=( + "Prove memcpy/memset overflow, deep aliasing, and const-correctness " + "features using existing test fixtures." + ) + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help="Path to stack_usage_analyzer, or CORETRACE_STACK_ANALYZER.", + ) + parser.add_argument("--memcpy-fixture", type=Path, default=FixtureSet.memcpy_overflow) + parser.add_argument("--memset-fixture", type=Path, default=FixtureSet.memset_overflow) + parser.add_argument("--deep-alias-fixture", type=Path, default=FixtureSet.deep_aliasing) + parser.add_argument("--const-fixture", type=Path, default=FixtureSet.const_correctness) + return parser.parse_args(argv) + + +def run_analyzer(analyzer: Path, fixture: Path) -> AnalyzerResult: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + if not fixture.exists(): + raise FileNotFoundError(f"Fixture not found: {fixture}") + + command = (str(analyzer), str(fixture), "--format=json") + result = subprocess.run(command, check=False, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if result.returncode != 0: + raise RuntimeError( + f"Analyzer failed for {fixture} with exit code {result.returncode}\n" + f"stdout:\n{result.stdout}\n" + f"stderr:\n{result.stderr}" + ) + + payload = json.loads(result.stdout) + if not isinstance(payload, dict): + raise ValueError(f"Analyzer output for {fixture} is not a JSON object.") + return AnalyzerResult(fixture=fixture, command=command, payload=payload) + + +def diagnostics(payload: dict[str, Any]) -> list[dict[str, Any]]: + raw = payload.get("diagnostics") + if not isinstance(raw, list): + raise ValueError("JSON report has no diagnostics array.") + return [item for item in raw if isinstance(item, dict)] + + +def message_of(diag: dict[str, Any]) -> str: + details = diag.get("details") + if not isinstance(details, dict): + return "" + message = details.get("message") + return message if isinstance(message, str) else "" + + +def variable_aliasing(diag: dict[str, Any]) -> list[str]: + details = diag.get("details") + if not isinstance(details, dict): + return [] + aliases = details.get("variableAliasing") + return [item for item in aliases if isinstance(item, str)] if isinstance(aliases, list) else [] + + +def has_diag( + payload: dict[str, Any], + *, + rule_id: str | None = None, + severity: str | None = None, + function: str | None = None, + message_contains: tuple[str, ...] = (), + aliases_contain: tuple[str, ...] = (), +) -> bool: + for diag in diagnostics(payload): + if rule_id is not None and diag.get("ruleId") != rule_id: + continue + if severity is not None and diag.get("severity") != severity: + continue + location = diag.get("location") + if function is not None: + if not isinstance(location, dict) or location.get("function") != function: + continue + message = message_of(diag) + aliases = variable_aliasing(diag) + if all(needle in message for needle in message_contains) and all( + alias in aliases for alias in aliases_contain + ): + return True + return False + + +def colored(text: str, color: str) -> str: + return f"{color}{text}{RESET}" + + +def status_label(found: bool) -> str: + return colored("PASS", GREEN) if found else colored("NONE", RED) + + +def require(condition: bool, proof: str, detail: str) -> ProofCheck: + return ProofCheck(name=proof, found=condition, detail=detail) + + +def print_report(result: AnalyzerResult, checks: list[ProofCheck]) -> None: + print_log(SEPARATOR) + print_log(colored(str(result.fixture), PURPLE)) + for check in checks: + print_log(f"- {check.name}: {status_label(check.found)}") + if not check.found: + print_log(f" detail: {check.detail}") + print_log(f"command: {' '.join(result.command)}") + + +def prove_memcpy(result: AnalyzerResult) -> list[ProofCheck]: + return [ + require( + has_diag( + result.payload, + severity="WARNING", + function="foo", + message_contains=( + "potential stack buffer overflow in memcpy", + "variable 'buf'", + "destination stack buffer size: 10 bytes", + "requested 20 bytes", + ), + ), + "memcpy overflow", + "expected memcpy overflow warning for buf[10] with 20 requested bytes", + ) + ] + + +def prove_memset(result: AnalyzerResult) -> list[ProofCheck]: + return [ + require( + has_diag( + result.payload, + severity="WARNING", + function="foo", + message_contains=( + "potential stack buffer overflow in memset", + "variable 'buf'", + "destination stack buffer size: 10 bytes", + "requested 100 bytes", + ), + ), + "memset overflow", + "expected memset overflow warning for buf[10] with 100 requested bytes", + ) + ] + + +def prove_deep_aliasing(result: AnalyzerResult) -> list[ProofCheck]: + return [ + require( + has_diag( + result.payload, + rule_id="StackBufferOverflow", + severity="WARNING", + function="deep_alias", + message_contains=( + "potential stack buffer overflow on variable 'buf'", + "alias path: buf -> arraydecay -> p1 -> p2 -> pp", + "array last valid index: 9", + ), + aliases_contain=("buf", "arraydecay", "p1", "p2", "pp"), + ), + "deep aliasing", + "expected stack-buffer overflow through buf -> arraydecay -> p1 -> p2 -> pp", + ) + ] + + +def prove_const_correctness(result: AnalyzerResult) -> list[ProofCheck]: + return [ + require( + has_diag( + result.payload, + rule_id="ConstParameterNotModified.Pointer", + severity="INFO", + function="myfunc", + message_contains=( + "parameter 'param3'", + "current type: int32_t *param3", + "suggested type: const int32_t *param3", + ), + ), + "const-correctness pointer", + "expected const suggestion for param3", + ), + require( + has_diag( + result.payload, + rule_id="ConstParameterNotModified.PointerConstOnly", + severity="INFO", + function="myfunc", + message_contains=( + "parameter 'param4'", + "current type: int32_t * const param4", + "suggested type: const int32_t *param4", + ), + ), + "const-correctness pointer const-only", + "expected const suggestion for param4", + ), + ] + + +def main(argv: list[str]) -> int: + args = parse_args(argv) + try: + fixtures = FixtureSet( + memcpy_overflow=args.memcpy_fixture, + memset_overflow=args.memset_fixture, + deep_aliasing=args.deep_alias_fixture, + const_correctness=args.const_fixture, + ) + results = { + "memcpy": run_analyzer(args.analyzer, fixtures.memcpy_overflow), + "memset": run_analyzer(args.analyzer, fixtures.memset_overflow), + "aliasing": run_analyzer(args.analyzer, fixtures.deep_aliasing), + "const": run_analyzer(args.analyzer, fixtures.const_correctness), + } + + reports = [ + (results["memcpy"], prove_memcpy(results["memcpy"])), + (results["memset"], prove_memset(results["memset"])), + (results["aliasing"], prove_deep_aliasing(results["aliasing"])), + (results["const"], prove_const_correctness(results["const"])), + ] + all_checks = [check for _, checks in reports for check in checks] + all_found = all(check.found for check in all_checks) + + print_log(f"BTP-STACK-ANALYZER-F2: {status_label(all_found)}") + for result, checks in reports: + print_report(result, checks) + return 0 if all_found else 1 + except Exception as exc: + print_log(f"BTP-STACK-ANALYZER-F2: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From 779a5561c9e8a6ce2788defe3d6f05933facca2d Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:20:58 +0200 Subject: [PATCH 5/9] test: add F5 proof for JSON SARIF and human output --- BTP-STACK-ANALYZER-F5.py | 466 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 466 insertions(+) create mode 100644 BTP-STACK-ANALYZER-F5.py diff --git a/BTP-STACK-ANALYZER-F5.py b/BTP-STACK-ANALYZER-F5.py new file mode 100644 index 0000000..8b4ae14 --- /dev/null +++ b/BTP-STACK-ANALYZER-F5.py @@ -0,0 +1,466 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for SARIF, JSON, and human-readable output. + +F5 proves that stack_usage_analyzer can emit: + - human-readable CLI output, + - JSON output suitable for CI automation, + - SARIF output suitable for GUI/security tooling. + +The proof runs the three formats on three existing repository fixtures and +checks that diagnostic counts are consistent across the formats. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any, Sequence + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +DEFAULT_FIXTURES = ( + Path("test/security/buffer-overflow/01_buffer_overflow.c"), + Path("test/cpy-buffer/bad-usage-memcpy.c"), + Path("test/local-storage/c/stack-callee-caller.c"), +) +REPORT_FORMATS = ("human", "json", "sarif") +SUMMARY_RE = re.compile(r"Diagnostics summary: info=(\d+), warning=(\d+), error=(\d+)") +GREEN = "\033[32m" +RED = "\033[31m" +PURPLE = "\033[35m" +RESET = "\033[0m" +SEPARATOR = "--------" + + +def feature_reference_from_filename(path: Path) -> str: + marker = "-F" + if marker not in path.stem: + return "[F?]" + suffix = path.stem.rsplit(marker, 1)[1] + digits = "".join(char for char in suffix if char.isdigit()) + return f"[F{digits}]" if digits else "[F?]" + + +FEATURE_REF = feature_reference_from_filename(Path(__file__)) + + +def print_log(*args: object, **kwargs: Any) -> None: + print(FEATURE_REF, *args, **kwargs) + + +@dataclass(frozen=True) +class AnalyzerOutput: + fixture: Path + report_format: str + command: tuple[str, ...] + stdout: str + stderr: str + returncode: int + + +@dataclass(frozen=True) +class ProofCheck: + name: str + found: bool + detail: str + + +@dataclass(frozen=True) +class FixtureProof: + fixture: Path + outputs: dict[str, AnalyzerOutput] + checks: list[ProofCheck] + + +def parse_args(argv: Sequence[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=( + "Prove SARIF, JSON, and human-readable output across three " + "stack_usage_analyzer fixtures." + ) + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help="Path to stack_usage_analyzer, or CORETRACE_STACK_ANALYZER.", + ) + parser.add_argument( + "--fixture", + action="append", + type=Path, + default=[], + help="Fixture to analyze. Repeat exactly three times to override defaults.", + ) + parser.add_argument( + "--show-analyzer-output", + action="store_true", + help="Compatibility option; captured stdout/stderr are printed by default.", + ) + args, analyzer_args = parser.parse_known_args(argv) + args.analyzer_args = normalize_extra_args(analyzer_args) + return args + + +def normalize_extra_args(extra_args: Sequence[str]) -> list[str]: + args = list(extra_args) + if args and args[0] == "--": + return args[1:] + return args + + +def selected_fixtures(args: argparse.Namespace) -> tuple[Path, Path, Path]: + fixtures = tuple(args.fixture) if args.fixture else DEFAULT_FIXTURES + if len(fixtures) != 3: + raise ValueError(f"F5 proof expects exactly 3 fixtures, got {len(fixtures)}.") + return fixtures # type: ignore[return-value] + + +def validate_inputs(analyzer: Path, fixtures: Sequence[Path]) -> None: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + for fixture in fixtures: + if not fixture.exists(): + raise FileNotFoundError(f"Fixture not found: {fixture}") + + +def run_analyzer( + analyzer: Path, + fixture: Path, + report_format: str, + extra_args: Sequence[str], +) -> AnalyzerOutput: + command = (str(analyzer), str(fixture), f"--format={report_format}", *extra_args) + result = subprocess.run( + command, + check=False, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + return AnalyzerOutput( + fixture=fixture, + report_format=report_format, + command=command, + stdout=result.stdout, + stderr=result.stderr, + returncode=result.returncode, + ) + + +def parse_json_object(output: AnalyzerOutput) -> tuple[dict[str, Any] | None, str | None]: + try: + payload = json.loads(output.stdout) + except json.JSONDecodeError as exc: + return None, str(exc) + if not isinstance(payload, dict): + return None, f"{output.report_format} output is not a JSON object." + return payload, None + + +def json_diagnostics(payload: dict[str, Any] | None) -> list[dict[str, Any]]: + if payload is None: + return [] + diagnostics = payload.get("diagnostics") + if not isinstance(diagnostics, list): + return [] + return [diag for diag in diagnostics if isinstance(diag, dict)] + + +def json_summary_total(payload: dict[str, Any] | None) -> int | None: + if payload is None: + return None + summary = payload.get("diagnosticsSummary") + if not isinstance(summary, dict): + return None + values = [summary.get("info"), summary.get("warning"), summary.get("error")] + if not all(isinstance(value, int) for value in values): + return None + return sum(values) + + +def human_summary_total(stdout: str) -> int | None: + match = SUMMARY_RE.search(stdout) + if match is None: + return None + return sum(int(value) for value in match.groups()) + + +def sarif_runs(payload: dict[str, Any] | None) -> list[dict[str, Any]]: + if payload is None: + return [] + runs = payload.get("runs") + if not isinstance(runs, list): + return [] + return [run for run in runs if isinstance(run, dict)] + + +def sarif_driver(payload: dict[str, Any] | None) -> dict[str, Any]: + runs = sarif_runs(payload) + if not runs: + return {} + tool = runs[0].get("tool") + if not isinstance(tool, dict): + return {} + driver = tool.get("driver") + return driver if isinstance(driver, dict) else {} + + +def sarif_results(payload: dict[str, Any] | None) -> list[dict[str, Any]]: + runs = sarif_runs(payload) + if not runs: + return [] + results = runs[0].get("results") + if not isinstance(results, list): + return [] + return [result for result in results if isinstance(result, dict)] + + +def sarif_rules(payload: dict[str, Any] | None) -> list[dict[str, Any]]: + rules = sarif_driver(payload).get("rules") + if not isinstance(rules, list): + return [] + return [rule for rule in rules if isinstance(rule, dict)] + + +def command_success_check(output: AnalyzerOutput) -> ProofCheck: + return ProofCheck( + name=f"{output.report_format} command completed", + found=output.returncode == 0, + detail=f"expected exit code 0, got {output.returncode}", + ) + + +def validate_human_output(output: AnalyzerOutput) -> list[ProofCheck]: + if output.returncode != 0: + return [command_success_check(output)] + return [ + command_success_check(output), + ProofCheck( + name="human-output mode header", + found=bool(re.search(r"^Mode: (IR|ABI)$", output.stdout, re.MULTILINE)), + detail="expected a readable 'Mode: IR' or 'Mode: ABI' header", + ), + ProofCheck( + name="human-output function blocks", + found="Function:" in output.stdout, + detail="expected at least one readable Function block", + ), + ProofCheck( + name="human-output stack fields", + found="local stack:" in output.stdout and "max stack (including callees):" in output.stdout, + detail="expected local and max stack lines", + ), + ProofCheck( + name="human-output diagnostics summary", + found=human_summary_total(output.stdout) is not None, + detail="expected Diagnostics summary: info=N, warning=N, error=N", + ), + ] + + +def validate_json_output(output: AnalyzerOutput, payload: dict[str, Any] | None, error: str | None) -> list[ProofCheck]: + if output.returncode != 0: + return [command_success_check(output)] + functions = payload.get("functions") if payload else None + diagnostics = json_diagnostics(payload) + first_diag = diagnostics[0] if diagnostics else {} + location = first_diag.get("location") if isinstance(first_diag, dict) else None + details = first_diag.get("details") if isinstance(first_diag, dict) else None + meta = payload.get("meta") if payload else None + return [ + command_success_check(output), + ProofCheck( + name="JSON parseable for CI", + found=payload is not None, + detail=error or "expected parseable JSON object", + ), + ProofCheck( + name="JSON tool metadata", + found=isinstance(meta, dict) + and meta.get("tool") == "ctrace-stack-analyzer" + and isinstance(meta.get("inputFile"), str), + detail="expected meta.tool and meta.inputFile", + ), + ProofCheck( + name="JSON functions array", + found=isinstance(functions, list) and bool(functions), + detail="expected non-empty functions[]", + ), + ProofCheck( + name="JSON diagnostics array", + found=bool(diagnostics) + and isinstance(first_diag.get("ruleId"), str) + and isinstance(first_diag.get("severity"), str) + and isinstance(location, dict) + and isinstance(details, dict), + detail="expected diagnostics[] with ruleId, severity, location, and details", + ), + ProofCheck( + name="JSON diagnostics summary", + found=json_summary_total(payload) is not None, + detail="expected diagnosticsSummary with info/warning/error counters", + ), + ] + + +def validate_sarif_output(output: AnalyzerOutput, payload: dict[str, Any] | None, error: str | None) -> list[ProofCheck]: + if output.returncode != 0: + return [command_success_check(output)] + driver = sarif_driver(payload) + rules = sarif_rules(payload) + results = sarif_results(payload) + first_result = results[0] if results else {} + message = first_result.get("message") if isinstance(first_result, dict) else None + locations = first_result.get("locations") if isinstance(first_result, dict) else None + first_location = locations[0] if isinstance(locations, list) and locations else None + physical = first_location.get("physicalLocation") if isinstance(first_location, dict) else None + return [ + command_success_check(output), + ProofCheck( + name="SARIF parseable for GUI", + found=payload is not None, + detail=error or "expected parseable SARIF JSON object", + ), + ProofCheck( + name="SARIF 2.1.0 envelope", + found=payload is not None + and payload.get("version") == "2.1.0" + and "sarif-2.1.0" in str(payload.get("$schema", "")), + detail="expected SARIF version 2.1.0 and schema URI", + ), + ProofCheck( + name="SARIF tool driver", + found=driver.get("name") == "coretrace-stack-analyzer", + detail="expected tool.driver.name=coretrace-stack-analyzer", + ), + ProofCheck( + name="SARIF rule catalog", + found=bool(rules) and all(isinstance(rule.get("id"), str) for rule in rules), + detail="expected tool.driver.rules[] with rule ids", + ), + ProofCheck( + name="SARIF results for GUI", + found=bool(results) + and isinstance(first_result.get("ruleId"), str) + and isinstance(first_result.get("level"), str) + and isinstance(message, dict) + and isinstance(message.get("text"), str) + and isinstance(physical, dict), + detail="expected results[] with ruleId, level, message.text, and physical location", + ), + ] + + +def validate_cross_format_counts( + human_output: AnalyzerOutput, + json_payload: dict[str, Any] | None, + sarif_payload: dict[str, Any] | None, +) -> list[ProofCheck]: + human_total = human_summary_total(human_output.stdout) + json_total = json_summary_total(json_payload) + json_diag_count = len(json_diagnostics(json_payload)) if json_payload is not None else None + sarif_result_count = len(sarif_results(sarif_payload)) if sarif_payload is not None else None + counts = { + "human": human_total, + "jsonSummary": json_total, + "jsonDiagnostics": json_diag_count, + "sarifResults": sarif_result_count, + } + present = [value for value in counts.values() if value is not None] + return [ + ProofCheck( + name="cross-format diagnostic count consistency", + found=len(present) == 4 and len(set(present)) == 1, + detail=f"expected equal diagnostic counts across formats, got {counts}", + ) + ] + + +def prove_fixture(analyzer: Path, fixture: Path, extra_args: Sequence[str]) -> FixtureProof: + outputs = { + report_format: run_analyzer(analyzer, fixture, report_format, extra_args) + for report_format in REPORT_FORMATS + } + json_payload, json_error = parse_json_object(outputs["json"]) + sarif_payload, sarif_error = parse_json_object(outputs["sarif"]) + + checks: list[ProofCheck] = [] + checks.extend(validate_human_output(outputs["human"])) + checks.extend(validate_json_output(outputs["json"], json_payload, json_error)) + checks.extend(validate_sarif_output(outputs["sarif"], sarif_payload, sarif_error)) + checks.extend(validate_cross_format_counts(outputs["human"], json_payload, sarif_payload)) + return FixtureProof(fixture=fixture, outputs=outputs, checks=checks) + + +def colored(text: str, color: str) -> str: + return f"{color}{text}{RESET}" + + +def status_label(found: bool) -> str: + return colored("PASS", GREEN) if found else colored("NONE", RED) + + +def print_fixture_report(proof: FixtureProof) -> None: + print_log(SEPARATOR) + print_log(colored(str(proof.fixture), PURPLE)) + for check in proof.checks: + print_log(f"- {check.name}: {status_label(check.found)}") + if not check.found: + print_log(f" detail: {check.detail}") + for report_format in REPORT_FORMATS: + command = proof.outputs[report_format].command + print_log(f"{report_format}-command: {' '.join(command)}") + + +def print_captured_outputs(proofs: Sequence[FixtureProof]) -> None: + for proof in proofs: + for report_format in REPORT_FORMATS: + output = proof.outputs[report_format] + print_log(SEPARATOR) + print_log(colored(str(output.fixture), PURPLE)) + print_log(f"format: {report_format.upper()}") + if output.stdout: + print_log("stdout:") + print_output_block(output.stdout) + if output.stderr: + print_log("stderr:") + print_output_block(output.stderr) + + +def print_output_block(output: str) -> None: + for line in output.rstrip().splitlines(): + print_log(line) + + +def main(argv: Sequence[str]) -> int: + args = parse_args(argv) + try: + fixtures = selected_fixtures(args) + validate_inputs(args.analyzer, fixtures) + proofs = [prove_fixture(args.analyzer, fixture, args.analyzer_args) for fixture in fixtures] + all_checks = [check for proof in proofs for check in proof.checks] + all_found = all(check.found for check in all_checks) + + print_log(f"BTP-STACK-ANALYZER-F5: {status_label(all_found)}") + print_log("feature: SARIF/JSON and human-readable output") + print_log(f"files-tested: {len(fixtures)}") + for proof in proofs: + print_fixture_report(proof) + print_log("analyzer-output: enabled") + print_captured_outputs(proofs) + return 0 if all_found else 1 + except Exception as exc: + print_log(f"BTP-STACK-ANALYZER-F5: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From 8ddfe92e77c2af5b42067d0e76ce4682d67207c7 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:21:11 +0200 Subject: [PATCH 6/9] test: add F8 Itanium ABI demangle proof script --- BTP-STACK-ANALYZER-F8.py | 442 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 442 insertions(+) create mode 100644 BTP-STACK-ANALYZER-F8.py diff --git a/BTP-STACK-ANALYZER-F8.py b/BTP-STACK-ANALYZER-F8.py new file mode 100644 index 0000000..99ba0b3 --- /dev/null +++ b/BTP-STACK-ANALYZER-F8.py @@ -0,0 +1,442 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for Itanium ABI mangle/demangle support. + +The proof runs stack_usage_analyzer twice over a C/C++ source file: + - JSON output keeps the raw LLVM/Itanium symbols, e.g. _Z... + - human output with --demangle prints readable C++ signatures. + +The two views are paired to prove that the tool exposes mangled symbols, +demangles them with parameters, and returns stable results across repeated +runs. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any, Sequence + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +DEFAULT_SOURCE = Path("test/test.cpp") +SUPPORTED_SOURCE_SUFFIXES = { + ".c", + ".cc", + ".cpp", + ".cxx", + ".c++", +} +FUNCTION_LINE_RE = re.compile(r"^Function:\s*(?P.+?)\s*$") +GREEN = "\033[32m" +RED = "\033[31m" +PURPLE = "\033[35m" +RESET = "\033[0m" +SEPARATOR = "--------" +EXPECTED_DEFAULT_PAIRS = { + "_ZN12demo_symbols17scalar_parametersEidc": "demo_symbols::scalar_parameters(int, double, char)", + "_ZN12demo_symbols18pointer_parametersEPKiPKcb": "demo_symbols::pointer_parameters(int const*, char const*, bool)", + "_ZN12demo_symbols20reference_parametersERKNS_6SampleEfm": ( + "demo_symbols::reference_parameters(demo_symbols::Sample const&, float, unsigned long)" + ), + "_ZN12demo_symbols10overloadedEi": "demo_symbols::overloaded(int)", + "_ZN12demo_symbols10overloadedEii": "demo_symbols::overloaded(int, int)", +} + + +def feature_reference_from_filename(path: Path) -> str: + marker = "-F" + if marker not in path.stem: + return "[F?]" + suffix = path.stem.rsplit(marker, 1)[1] + digits = "".join(char for char in suffix if char.isdigit()) + return f"[F{digits}]" if digits else "[F?]" + + +FEATURE_REF = feature_reference_from_filename(Path(__file__)) + + +def print_log(*args: object, **kwargs: Any) -> None: + print(FEATURE_REF, *args, **kwargs) + + +@dataclass(frozen=True) +class AnalyzerCommand: + argv: tuple[str, ...] + + +@dataclass(frozen=True) +class AnalyzerOutput: + command: AnalyzerCommand + stdout: str + stderr: str + returncode: int + + +@dataclass(frozen=True) +class FunctionNamePair: + mangled: str + demangled: str + + +@dataclass(frozen=True) +class ProofRun: + source: Path + human: AnalyzerOutput + json_report: AnalyzerOutput + mangled_count: int + demangled_count: int + pairs: tuple[FunctionNamePair, ...] + + +@dataclass(frozen=True) +class ProofCheck: + name: str + found: bool + detail: str + + +def parse_args(argv: Sequence[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description="Prove Itanium ABI mangle/demangle support through stack_usage_analyzer." + ) + parser.add_argument( + "source", + nargs="?", + type=Path, + default=DEFAULT_SOURCE, + help="C or C++ source file used by the proof. Defaults to test/test.cpp.", + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help="Path to stack_usage_analyzer, or CORETRACE_STACK_ANALYZER.", + ) + parser.add_argument( + "--only-function", + action="append", + default=[], + help="Forwarded to the analyzer as --only-function=. Can be repeated.", + ) + parser.add_argument( + "--minimum-symbols", + type=int, + default=1, + help="Minimum number of Itanium symbols required for a PASS.", + ) + parser.add_argument( + "--show-analyzer-output", + action="store_true", + help="Print captured analyzer stdout/stderr when the proof completes.", + ) + args, analyzer_args = parser.parse_known_args(argv) + args.analyzer_args = normalize_extra_args(analyzer_args) + return args + + +def normalize_extra_args(extra_args: Sequence[str]) -> list[str]: + args = list(extra_args) + if args and args[0] == "--": + return args[1:] + return args + + +def validate_inputs(analyzer: Path, source: Path) -> None: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + if not source.exists(): + raise FileNotFoundError(f"Input source not found: {source}") + if source.suffix.lower() not in SUPPORTED_SOURCE_SUFFIXES: + supported = ", ".join(sorted(SUPPORTED_SOURCE_SUFFIXES)) + raise ValueError(f"Expected a C/C++ source file ({supported}), got: {source}") + + +def build_human_command( + analyzer: Path, + source: Path, + only_functions: Sequence[str], + extra_args: Sequence[str], +) -> AnalyzerCommand: + argv = [str(analyzer), str(source), "--demangle", "--print-effective-config"] + for function_name in only_functions: + argv.append(f"--only-function={function_name}") + argv.extend(extra_args) + return AnalyzerCommand(tuple(argv)) + + +def build_json_command( + analyzer: Path, + source: Path, + only_functions: Sequence[str], + extra_args: Sequence[str], +) -> AnalyzerCommand: + argv = [str(analyzer), str(source), "--demangle", "--format=json"] + for function_name in only_functions: + argv.append(f"--only-function={function_name}") + argv.extend(extra_args) + return AnalyzerCommand(tuple(argv)) + + +def run_analyzer(command: AnalyzerCommand) -> AnalyzerOutput: + result = subprocess.run( + command.argv, + check=False, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + return AnalyzerOutput( + command=command, + stdout=result.stdout, + stderr=result.stderr, + returncode=result.returncode, + ) + + +def require_success(output: AnalyzerOutput) -> None: + if output.returncode == 0: + return + message = [ + f"Analyzer failed with exit code {output.returncode}", + f"command: {' '.join(output.command.argv)}", + ] + if output.stdout: + message.extend(["stdout:", output.stdout.rstrip()]) + if output.stderr: + message.extend(["stderr:", output.stderr.rstrip()]) + raise RuntimeError("\n".join(message)) + + +def demangle_enabled(output: AnalyzerOutput) -> bool: + effective_config = f"{output.stdout}\n{output.stderr}" + return "demangle: true" in effective_config + + +def parse_demangled_human_functions(stdout: str) -> list[str]: + names: list[str] = [] + for line in stdout.splitlines(): + match = FUNCTION_LINE_RE.match(line) + if match: + names.append(match.group("name").strip()) + return names + + +def parse_mangled_json_functions(stdout: str) -> list[str]: + payload = json.loads(stdout) + if not isinstance(payload, dict): + raise ValueError("Analyzer JSON output is not a JSON object.") + functions = payload.get("functions") + if not isinstance(functions, list): + raise ValueError("Analyzer JSON output does not contain a functions array.") + + names: list[str] = [] + for function in functions: + if not isinstance(function, dict): + continue + name = function.get("name") + if isinstance(name, str): + names.append(name) + return names + + +def strip_llvm_symbol_prefix(symbol: str) -> str: + return symbol[1:] if symbol.startswith("\x01") else symbol + + +def is_itanium_mangled(symbol: str) -> bool: + normalized = strip_llvm_symbol_prefix(symbol) + return normalized.startswith("_Z") or normalized.startswith("__Z") + + +def collect_itanium_pairs( + mangled_names: Sequence[str], + demangled_names: Sequence[str], +) -> tuple[FunctionNamePair, ...]: + if len(mangled_names) != len(demangled_names): + raise RuntimeError( + "Human and JSON outputs returned different function counts " + f"({len(demangled_names)} human vs {len(mangled_names)} JSON)." + ) + + pairs: list[FunctionNamePair] = [] + for mangled, demangled in zip(mangled_names, demangled_names): + if not is_itanium_mangled(mangled): + continue + pairs.append(FunctionNamePair(mangled=mangled, demangled=demangled)) + return tuple(pairs) + + +def has_parameterized_signature(pair: FunctionNamePair) -> bool: + open_paren = pair.demangled.find("(") + close_paren = pair.demangled.rfind(")") + if open_paren < 0 or close_paren <= open_paren: + return False + parameter_list = pair.demangled[open_paren + 1 : close_paren].strip() + return bool(parameter_list) and parameter_list != "void" + + +def is_default_source(source: Path) -> bool: + try: + return source.resolve() == DEFAULT_SOURCE.resolve() + except FileNotFoundError: + return source == DEFAULT_SOURCE + + +def expected_default_pairs_check(source: Path, only_functions: Sequence[str], pairs: Sequence[FunctionNamePair]) -> ProofCheck | None: + if only_functions or not is_default_source(source): + return None + + by_mangled = {pair.mangled: pair.demangled for pair in pairs} + missing = [ + f"{mangled} -> {demangled}" + for mangled, demangled in EXPECTED_DEFAULT_PAIRS.items() + if by_mangled.get(mangled) != demangled + ] + return ProofCheck( + name="known Itanium ABI fixture signatures", + found=not missing, + detail="missing or mismatched expected fixture pairs: " + "; ".join(missing), + ) + + +def run_proof_once( + analyzer: Path, + source: Path, + only_functions: Sequence[str], + extra_args: Sequence[str], +) -> ProofRun: + human_command = build_human_command(analyzer, source, only_functions, extra_args) + json_command = build_json_command(analyzer, source, only_functions, extra_args) + + human_output = run_analyzer(human_command) + require_success(human_output) + json_output = run_analyzer(json_command) + require_success(json_output) + + demangled_names = parse_demangled_human_functions(human_output.stdout) + mangled_names = parse_mangled_json_functions(json_output.stdout) + pairs = collect_itanium_pairs(mangled_names, demangled_names) + return ProofRun( + source=source, + human=human_output, + json_report=json_output, + mangled_count=len(mangled_names), + demangled_count=len(demangled_names), + pairs=pairs, + ) + + +def build_checks( + first: ProofRun, + second: ProofRun, + *, + only_functions: Sequence[str], + minimum_symbols: int, +) -> list[ProofCheck]: + pairs = first.pairs + checks = [ + ProofCheck( + name="demangle mode enabled", + found=demangle_enabled(first.human), + detail="expected --print-effective-config to contain 'demangle: true'", + ), + ProofCheck( + name="Itanium mangled symbols found", + found=len(pairs) >= minimum_symbols, + detail=f"expected at least {minimum_symbols} Itanium _Z symbol(s), got {len(pairs)}", + ), + ProofCheck( + name="demangled symbols are readable", + found=bool(pairs) + and all(pair.demangled != pair.mangled and not is_itanium_mangled(pair.demangled) for pair in pairs), + detail="expected every Itanium symbol to map to a readable non-_Z function signature", + ), + ProofCheck( + name="parameterized signatures visible", + found=any(has_parameterized_signature(pair) for pair in pairs), + detail="expected at least one demangled function signature with parameters", + ), + ProofCheck( + name="stable repeated output", + found=first.pairs == second.pairs, + detail="expected identical mangled/demangled pairs across two analyzer runs", + ), + ] + + default_check = expected_default_pairs_check(first.source, only_functions, pairs) + if default_check is not None: + checks.append(default_check) + return checks + + +def colored(text: str, color: str) -> str: + return f"{color}{text}{RESET}" + + +def status_label(found: bool) -> str: + return colored("PASS", GREEN) if found else colored("NONE", RED) + + +def print_report(run: ProofRun, checks: Sequence[ProofCheck]) -> None: + all_found = all(check.found for check in checks) + print_log(f"BTP-STACK-ANALYZER-F8: {status_label(all_found)}") + print_log(SEPARATOR) + print_log(colored(str(run.source), PURPLE)) + print_log("feature: Itanium ABI mangle/demangle") + print_log(f"demangle-mode: {'enabled' if demangle_enabled(run.human) else 'disabled'}") + print_log(f"symbols-found: {len(run.pairs)}") + for check in checks: + print_log(f"- {check.name}: {status_label(check.found)}") + if not check.found: + print_log(f" detail: {check.detail}") + for pair in run.pairs: + print_log(f"mangled-symbol: {pair.mangled}") + print_log(f"demangled-symbol: {pair.demangled}") + print_log(f"human-command: {' '.join(run.human.command.argv)}") + print_log(f"json-command: {' '.join(run.json_report.command.argv)}") + + +def print_captured_output(run: ProofRun) -> None: + print_log(SEPARATOR) + print_log("analyzer human stdout:") + print_log(run.human.stdout.rstrip()) + if run.human.stderr: + print_log("analyzer human stderr:") + print_log(run.human.stderr.rstrip()) + print_log("analyzer json stdout:") + print_log(run.json_report.stdout.rstrip()) + if run.json_report.stderr: + print_log("analyzer json stderr:") + print_log(run.json_report.stderr.rstrip()) + + +def main(argv: Sequence[str]) -> int: + args = parse_args(argv) + try: + validate_inputs(args.analyzer, args.source) + first = run_proof_once(args.analyzer, args.source, args.only_function, args.analyzer_args) + second = run_proof_once(args.analyzer, args.source, args.only_function, args.analyzer_args) + checks = build_checks( + first, + second, + only_functions=args.only_function, + minimum_symbols=args.minimum_symbols, + ) + print_report(first, checks) + if args.show_analyzer_output: + print_captured_output(first) + return 0 if all(check.found for check in checks) else 1 + except Exception as exc: + print_log(f"BTP-STACK-ANALYZER-F8: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From f3704035411a814903209ab3f1e9988c19edc8d6 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:21:22 +0200 Subject: [PATCH 7/9] test: add F10 stack buffer overflow proof script --- BTP-STACK-ANALYZER-F10.py | 194 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) create mode 100755 BTP-STACK-ANALYZER-F10.py diff --git a/BTP-STACK-ANALYZER-F10.py b/BTP-STACK-ANALYZER-F10.py new file mode 100755 index 0000000..13ee481 --- /dev/null +++ b/BTP-STACK-ANALYZER-F10.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Proof script for static stack-allocated buffer overflow detection. + +This script validates that stack_usage_analyzer emits a structured +StackBufferOverflow diagnostic for an existing stack buffer fixture. +""" + +from __future__ import annotations + +import argparse +import json +import os +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any + + +DEFAULT_ANALYZER = Path(os.environ.get("CORETRACE_STACK_ANALYZER", "./build/stack_usage_analyzer")) +DEFAULT_FIXTURE = Path("test/security/buffer-overflow/01_buffer_overflow.c") +GREEN = "\033[32m" +RED = "\033[31m" +PURPLE = "\033[35m" +RESET = "\033[0m" +SEPARATOR = "--------" + + +def feature_reference_from_filename(path: Path) -> str: + marker = "-F" + if marker not in path.stem: + return "[F?]" + suffix = path.stem.rsplit(marker, 1)[1] + digits = "".join(char for char in suffix if char.isdigit()) + return f"[F{digits}]" if digits else "[F?]" + + +FEATURE_REF = feature_reference_from_filename(Path(__file__)) + + +def print_log(*args: object, **kwargs: Any) -> None: + print(FEATURE_REF, *args, **kwargs) + + +@dataclass(frozen=True) +class AnalyzerResult: + fixture: Path + command: tuple[str, ...] + payload: dict[str, Any] + + +@dataclass(frozen=True) +class StackBufferProof: + function: str + variable: str + rule_id: str + severity: str + message: str + + +def parse_args(argv: list[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=( + "Prove static overflow detection on stack-allocated buffers using " + "an existing stack_usage_analyzer fixture." + ) + ) + parser.add_argument( + "--analyzer", + type=Path, + default=DEFAULT_ANALYZER, + help="Path to stack_usage_analyzer, or CORETRACE_STACK_ANALYZER.", + ) + parser.add_argument("--fixture", type=Path, default=DEFAULT_FIXTURE) + return parser.parse_args(argv) + + +def run_analyzer(analyzer: Path, fixture: Path) -> AnalyzerResult: + if not analyzer.exists(): + raise FileNotFoundError(f"Analyzer not found: {analyzer}") + if not fixture.exists(): + raise FileNotFoundError(f"Fixture not found: {fixture}") + + command = (str(analyzer), str(fixture), "--format=json") + result = subprocess.run(command, check=False, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if result.returncode != 0: + raise RuntimeError( + f"Analyzer failed for {fixture} with exit code {result.returncode}\n" + f"stdout:\n{result.stdout}\n" + f"stderr:\n{result.stderr}" + ) + + payload = json.loads(result.stdout) + if not isinstance(payload, dict): + raise ValueError(f"Analyzer output for {fixture} is not a JSON object.") + return AnalyzerResult(fixture=fixture, command=command, payload=payload) + + +def diagnostics(payload: dict[str, Any]) -> list[dict[str, Any]]: + raw = payload.get("diagnostics") + if not isinstance(raw, list): + raise ValueError("JSON report has no diagnostics array.") + return [item for item in raw if isinstance(item, dict)] + + +def message_of(diag: dict[str, Any]) -> str: + details = diag.get("details") + if not isinstance(details, dict): + return "" + message = details.get("message") + return message if isinstance(message, str) else "" + + +def aliases_of(diag: dict[str, Any]) -> list[str]: + details = diag.get("details") + if not isinstance(details, dict): + return [] + aliases = details.get("variableAliasing") + return [item for item in aliases if isinstance(item, str)] if isinstance(aliases, list) else [] + + +def find_stack_buffer_overflow(payload: dict[str, Any]) -> StackBufferProof | None: + for diag in diagnostics(payload): + if diag.get("ruleId") != "StackBufferOverflow": + continue + if diag.get("severity") != "WARNING": + continue + + location = diag.get("location") + if not isinstance(location, dict) or location.get("function") != "vuln_off_by_one": + continue + + message = message_of(diag) + aliases = aliases_of(diag) + required_fragments = ( + "potential stack buffer overflow on variable 'buf'", + "size 10", + "alias path: buf", + "index variable may go up to 10", + "array last valid index: 9", + "write access", + ) + if not all(fragment in message for fragment in required_fragments): + continue + if "buf" not in aliases: + continue + + return StackBufferProof( + function="vuln_off_by_one", + variable="buf", + rule_id="StackBufferOverflow", + severity="WARNING", + message=" ".join(message.split()), + ) + return None + + +def colored(text: str, color: str) -> str: + return f"{color}{text}{RESET}" + + +def status_label(found: bool) -> str: + return colored("PASS", GREEN) if found else colored("NONE", RED) + + +def main(argv: list[str]) -> int: + args = parse_args(argv) + try: + result = run_analyzer(args.analyzer, args.fixture) + proof = find_stack_buffer_overflow(result.payload) + found = proof is not None + + print_log(f"BTP-STACK-ANALYZER-F10: {status_label(found)}") + print_log(SEPARATOR) + print_log(colored(str(result.fixture), PURPLE)) + print_log(f"- static stack-buffer overflow: {status_label(found)}") + if proof is None: + print_log(" detail: expected StackBufferOverflow warning for vuln_off_by_one stack buffer 'buf'") + else: + print_log(f" rule-id: {proof.rule_id}") + print_log(f" severity: {proof.severity}") + print_log(f" function: {proof.function}") + print_log(f" stack-buffer: {proof.variable}") + print_log(f" diagnostic: {proof.message}") + print_log(f"command: {' '.join(result.command)}") + return 0 if found else 1 + except Exception as exc: + print_log(f"BTP-STACK-ANALYZER-F10: FAIL: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) From e87342dcc728c57e5f10ac05ac9d7196655e7e20 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:21:33 +0200 Subject: [PATCH 8/9] docs: add issue for BTP stack analyzer proof scripts --- .../btp-stack-analyzer-proof-scripts.md | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 docs/issues/btp-stack-analyzer-proof-scripts.md diff --git a/docs/issues/btp-stack-analyzer-proof-scripts.md b/docs/issues/btp-stack-analyzer-proof-scripts.md new file mode 100644 index 0000000..f7ed951 --- /dev/null +++ b/docs/issues/btp-stack-analyzer-proof-scripts.md @@ -0,0 +1,118 @@ +# Add BTP proof scripts for stack analyzer feature validation + +## Description +Add standalone Python proof scripts that demonstrate selected +`stack_usage_analyzer` capabilities using existing repository fixtures. + +The scripts are intended for human review, BTP validation, and lightweight +feature evidence. They should make the analyzer command, analyzed fixture, +feature reference, PASS/NONE status, and raw evidence visible in the terminal. + +## What was implemented +1. Added `BTP-STACK-ANALYZER-F1.py` for stack usage analysis proof: + - static and propagated stack size, + - dynamic stack size through VLA and `alloca`, + - unknown stack propagation, + - infinite recursion, + - stack pointer escape, + - explicit IR and ABI mode coverage. +2. Added `BTP-STACK-ANALYZER-F2.py` for advanced stack diagnostics proof: + - `memcpy` overflow, + - `memset` overflow, + - deep aliasing, + - basic const-correctness diagnostics. +3. Added `BTP-STACK-ANALYZER-F5.py` for output-format proof: + - three fixtures, + - `--format=human`, + - `--format=json`, + - `--format=sarif`, + - parseable JSON/SARIF checks, + - readable CLI checks, + - cross-format diagnostic count consistency, + - raw output printed for every format. +4. Added `BTP-STACK-ANALYZER-F8.py` for Itanium ABI mangle/demangle proof: + - JSON raw symbol extraction, + - human output with `--demangle`, + - visible mangled and demangled symbols, + - parameterized C++ signatures, + - repeated-run stability. +5. Added `BTP-STACK-ANALYZER-F10.py` for static stack-buffer overflow proof: + - existing stack-buffer fixture, + - `StackBufferOverflow` diagnostic, + - function, variable, severity, rule id, and diagnostic text. +6. Added `BTP-STACK-ANALYER.py` as an earlier combined proof helper for: + - demangle proof, + - static stack-buffer overflow proof. +7. Updated `test/test.cpp` with C++ functions covering multiple parameter shapes + so F8 can prove demangled signatures with parameters and overloads. +8. Standardized proof output: + - feature prefix derived from the script name, e.g. `[F1]`, `[F5]`, `[F8]`, + - purple fixture names, + - green `PASS`, + - red `NONE`, + - `--------` separators between fixture reports. + +## Architecture rationale +- Keep each BTP feature in its own script so each competency maps to one + executable proof artifact. +- Reuse existing repository fixtures instead of generating temporary source + files, preserving alignment with the analyzer test corpus. +- Parse structured JSON/SARIF output with Python `json` instead of relying only + on string matching. +- Keep display logic local to each standalone script to avoid import/path + fragility when scripts are run directly from the repository root. +- Derive feature references from filenames instead of hardcoding `[F1]`, + `[F2]`, etc., so future `BTP-STACK-ANALYZER-F*.py` scripts can reuse the same + pattern. + +## Validation commands +Run the proof scripts: + +```bash +python3 -B BTP-STACK-ANALYZER-F1.py +python3 -B BTP-STACK-ANALYZER-F2.py +python3 -B BTP-STACK-ANALYZER-F5.py +python3 -B BTP-STACK-ANALYZER-F8.py +python3 -B BTP-STACK-ANALYZER-F10.py +``` + +Negative evidence checks: + +```bash +python3 -B BTP-STACK-ANALYZER-F8.py test/security/buffer-overflow/01_buffer_overflow.c +python3 -B BTP-STACK-ANALYZER-F10.py --fixture test/no-error/basic-main.c +``` + +Full test suite previously validated: + +```bash +python3 -B run_test.py --jobs 4 +``` + +Observed result: + +```text +Passed 1671/1671 tests +``` + +## Acceptance criteria +- F1 prints IR and ABI mode evidence and passes all stack-usage checks. +- F2 proves memory intrinsic overflow, deep aliasing, and const-correctness + diagnostics. +- F5 proves human, JSON, and SARIF output over three files and prints the raw + output for every mode. +- F8 proves Itanium ABI mangle/demangle with visible symbols and parameterized + demangled signatures. +- F10 proves static stack-buffer overflow diagnostics on a stack-allocated + buffer. +- Every proof script prints its feature reference before logs. +- `PASS` is green, `NONE` is red, fixture names are purple, and fixture sections + are separated by `--------`. + +## Follow-up +- Decide whether SARIF should remain standard-only or include a custom + `properties.diagnosticsSummary` extension. Current F5 computes the SARIF + summary from `runs[0].results` instead of expecting a non-standard + `diagnosticsSummary` field. +- Consider extracting the repeated color/reference helpers into a shared module + only if these scripts become maintained as a long-term test harness. From 7e7ff1f111ecb09d9137043d61c052615c5dea16 Mon Sep 17 00:00:00 2001 From: Hugo Date: Wed, 15 Jul 2026 17:22:22 +0200 Subject: [PATCH 9/9] chore(style): format code with clang-format --- test/test.cpp | 60 +++++++++++++++++++++++++-------------------------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/test/test.cpp b/test/test.cpp index e9cccf7..718c456 100644 --- a/test/test.cpp +++ b/test/test.cpp @@ -4,41 +4,41 @@ namespace demo_symbols { -struct Sample -{ - int value; -}; - -int scalar_parameters(int value, double scale, char tag) -{ - if (value > 0 && scale > 0.0 && tag != '\0') - return 1; - return 0; -} + struct Sample + { + int value; + }; -long pointer_parameters(const int* value, const char* label, bool enabled) -{ - if (!value || !label || !enabled) + int scalar_parameters(int value, double scale, char tag) + { + if (value > 0 && scale > 0.0 && tag != '\0') + return 1; return 0; - return (*value > 0 && label[0] != '\0') ? 1L : 0L; -} + } -double reference_parameters(const Sample& sample, float ratio, unsigned long count) -{ - if (sample.value > 0 && ratio > 0.0f && count > 0) - return 1.0; - return 0.0; -} + long pointer_parameters(const int* value, const char* label, bool enabled) + { + if (!value || !label || !enabled) + return 0; + return (*value > 0 && label[0] != '\0') ? 1L : 0L; + } -int overloaded(int value) -{ - return value == 0 ? 0 : 1; -} + double reference_parameters(const Sample& sample, float ratio, unsigned long count) + { + if (sample.value > 0 && ratio > 0.0f && count > 0) + return 1.0; + return 0.0; + } -int overloaded(int lhs, int rhs) -{ - return lhs < rhs ? 1 : 0; -} + int overloaded(int value) + { + return value == 0 ? 0 : 1; + } + + int overloaded(int lhs, int rhs) + { + return lhs < rhs ? 1 : 0; + } } // namespace demo_symbols void toto(void)