From 771506753e6d171ecd8f0b7a9f5057a61e6e6eb8 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 26 Jun 2026 15:49:35 -0700 Subject: [PATCH 1/3] REL: add newfunctions to relational prepare --- chb/cmdline/PatchResults.py | 21 ++++++++++++++++++++- chb/cmdline/relationalcmds.py | 6 ++++++ 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/chb/cmdline/PatchResults.py b/chb/cmdline/PatchResults.py index aee95079..af08fd74 100644 --- a/chb/cmdline/PatchResults.py +++ b/chb/cmdline/PatchResults.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023-2025 Aarno Labs, LLC +# Copyright (c) 2023-2026 Aarno Labs, LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -324,6 +324,13 @@ def is_trampoline(self) -> bool: def is_new_function(self) -> bool: return self.patchkind == "NewFunction" + @property + def get_new_function_address(self) -> Optional[str]: + if self.is_new_function: + return self.details.payload.vahex + else: + return None + @property def is_supported(self) -> bool: return self.is_trampoline @@ -418,6 +425,18 @@ def events(self) -> List[PatchEvent]: def trampoline_payload_addresses(self) -> List[str]: return [str(e.payload.vahex) for e in self.events if e.has_payload()] + @property + def new_functions(self) -> List[str]: + result: List[str] = [] + for ev in self.events: + if ev.is_new_function: + faddr = ev.get_new_function_address + if faddr is not None: + result.append(faddr) + else: + chklogger.logger.warning("NewFunction event in patch-results without address") + return result + @property def trampoline_addresses(self) -> List[Dict[str, str]]: result: List[Dict[str, str]] = [] diff --git a/chb/cmdline/relationalcmds.py b/chb/cmdline/relationalcmds.py index 9807603e..be537cb5 100644 --- a/chb/cmdline/relationalcmds.py +++ b/chb/cmdline/relationalcmds.py @@ -185,6 +185,11 @@ def relational_prepare_command(args: argparse.Namespace) -> NoReturn: with open(xpatchresults, "r") as fp: patchresultsdata = json.load(fp) + newfunctions: List[str] = [] + if patchresultsdata is not None: + patchresults = PatchResults(patchresultsdata) + newfunctions = patchresults.new_functions + xcomparison = compare_executable_content( path1, xfile1, path2, xfile2, is_thumb, patchresultsdata) @@ -281,6 +286,7 @@ def relational_prepare_command(args: argparse.Namespace) -> NoReturn: fncount1 = stats1.function_count if len(stats1.fns_included) > 0: fns_include = stats1.fns_included + fns_include.extend(newfunctions) include_callees = stats1.include_callees if include_callees: UC.print_status_update( From 29be0d6f130928d1d495f395ee7b364643e618c5 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 30 Jun 2026 10:00:06 -0700 Subject: [PATCH 2/3] REL: add new functions to relational compare proofobligations --- chb/cmdline/chkx | 27 +++++++++++++++++++++++++++ chb/cmdline/relationalcmds.py | 31 ++++++++++++++++++++++++++++++- 2 files changed, 57 insertions(+), 1 deletion(-) diff --git a/chb/cmdline/chkx b/chb/cmdline/chkx index 2a0a6f31..45414529 100755 --- a/chb/cmdline/chkx +++ b/chb/cmdline/chkx @@ -1267,6 +1267,30 @@ def parse() -> argparse.Namespace: # -- report proof obligations report_proofobligations = reportparsers.add_parser("proofobligations") report_proofobligations.add_argument("xname", help="name of executable") + report_proofobligations.add_argument( + "--functions", + action="store_true", + default=False, + help="add per-function breakdown sorted by open count") + report_proofobligations.add_argument( + "--open", + action="store_true", + default=False, + help="show open proof obligations per function with predicate detail") + report_proofobligations.add_argument( + "--details", + action="store_true", + default=False, + help="include status message for each open proof obligation (implies --open)") + report_proofobligations.add_argument( + "--json", + action="store_true", + default=False, + help="output all proof obligations as a flat JSON record to stdout") + report_proofobligations.add_argument( + "-o", "--output", + metavar="FILE", + help="save JSON output to FILE (implies --json)") report_proofobligations.set_defaults(func=REP.report_proofobligations) # --- report unresolved @@ -1708,6 +1732,9 @@ def parse() -> argparse.Namespace: "xname1", help="name of first (original) executable (assumed analyzed)") relationalcomparepos.add_argument( "xname2", help="name of second (patched) executable (assumed analyzed)") + relationalcomparepos.add_argument( + "--patch_results_file", + help="name of patch results (required if there are new functions") relationalcomparepos.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), diff --git a/chb/cmdline/relationalcmds.py b/chb/cmdline/relationalcmds.py index be537cb5..663cdc50 100644 --- a/chb/cmdline/relationalcmds.py +++ b/chb/cmdline/relationalcmds.py @@ -975,6 +975,7 @@ def relational_compare_proofobligations(args: argparse.Namespace) -> NoReturn: # arguments xname1: str = args.xname1 xname2: str = args.xname2 + xpatchresults: Optional[str] = args.patch_results_file loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -1004,6 +1005,16 @@ def relational_compare_proofobligations(args: argparse.Namespace) -> NoReturn: app1 = UC.get_app(path1, xfile1, xinfo1) app2 = UC.get_app(path2, xfile2, xinfo2) + patchresultsdata: Optional[Dict[str, Any]] = None + if xpatchresults is not None: + with open(xpatchresults, "r") as fp: + patchresultsdata = json.load(fp) + + newfunctions: List[str] = [] + if patchresultsdata is not None: + patchresults = PatchResults(patchresultsdata) + newfunctions = patchresults.new_functions + relanalysis = RelationalAnalysis(app1, app2) functionschanged = relanalysis.functions_changed() @@ -1067,12 +1078,30 @@ def relational_compare_proofobligations(args: argparse.Namespace) -> NoReturn: for po in diffs[0]: print(" " + str(po.xpo).ljust(64) + str(po.status).rjust(10)) print(" patched") + print(" " + str(f2fn.instructions[iaddr].annotation)) for po in diffs[1]: - print(" " + str(f2fn.instructions[iaddr].annotation)) print(" " + str(po.xpo).ljust(64) + str(po.status).rjust(10)) print("\nProof obligations unchanged: " + str(unchanged)) print("~" * 80) + if len(newfunctions) > 0: + print("\n\nNew functions introduced:") + for faddr in newfunctions: + print("-" * 80) + print("Function " + faddr) + fn = app2.function(faddr) + fpos = fn.proofobligations.proofobligations + if len(fpos) == 0: + print(" no proof obligations") + print("-" * 80) + continue + for (iaddr, ipos) in fpos.items(): + print(" " + iaddr) + print(" " + str(fn.instructions[iaddr].annotation)) + for po in ipos: + print(" " + str(po.xpo).ljust(64) + str(po.status).rjust(10)) + print("-" * 80) + print("\nTotal number of proof obligations changed: " + str(count)) exit(0) From d5d9436d3f81cd6ee539ee68b8d545e34faa509b Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 30 Jun 2026 10:00:24 -0700 Subject: [PATCH 3/3] REP: expand proof obligations report --- chb/app/CHVersion.py | 2 +- chb/app/FnProofObligations.py | 37 +++++ chb/cmdline/reportcmds.py | 262 +++++++++++++++++++++++++++++++--- 3 files changed, 278 insertions(+), 23 deletions(-) diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index 45357d1a..a872b4c5 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ -chbversion: str = "0.3.0-20260625" +chbversion: str = "0.3.0-20260630" minimum_required_chb_version = "0.6.0_20260617" diff --git a/chb/app/FnProofObligations.py b/chb/app/FnProofObligations.py index bc661179..1681dfb9 100644 --- a/chb/app/FnProofObligations.py +++ b/chb/app/FnProofObligations.py @@ -47,10 +47,47 @@ "o": "open", "dis": "safe", "del": "delegated", + "glob": "global", + "req": "request", "local": "delegated-local", "v": "violation" } +xpo_tag_names: Dict[str, str] = { + "ab": "allocation-base", + "b": "buffer", + "bw": "block-write", + "e": "enum", + "errno": "sets-errno", + "fp": "function-pointer", + "fr": "freed", + "ga": "global-address", + "ha": "heap-address", + "i": "initialized", + "ifs": "input-format-string", + "inv": "invalidated", + "ir": "initialized-range", + "nm": "new-memory", + "nn": "not-null", + "nng": "non-negative", + "no": "no-overlap", + "nt": "null-terminated", + "nu": "null", + "nz": "not-zero", + "ofs": "output-format-string", + "pos": "positive", + "rofs": "restricted-output-format-string", + "sa": "stack-address", + "st": "starts-thread", + "t": "tainted", + "tc": "trusted-os-cmd-string", + "tfa": "trusted-os-cmd-fmt-arg-string", + "tfs": "trusted-os-cmd-fmt-string", + "ts": "trusted-string", + "v": "valid-mem", + "x": "relational-expr", +} + class POStatus: def __init__(self, xpod: "FnXPODictionary", node: ET.Element) -> None: diff --git a/chb/cmdline/reportcmds.py b/chb/cmdline/reportcmds.py index 7285ec29..67084908 100644 --- a/chb/cmdline/reportcmds.py +++ b/chb/cmdline/reportcmds.py @@ -49,6 +49,7 @@ from chb.app.Callgraph import Callgraph from chb.app.Instruction import Instruction +from chb.app.FnProofObligations import po_status_strings, xpo_tag_names from chb.app.XPOPredicate import XPOTrustedOsCmdFmtString, XPOTrustedOsCmdString from chb.arm.ARMInstruction import ARMInstruction @@ -729,7 +730,11 @@ def report_proofobligations(args: argparse.Namespace) -> NoReturn: # arguments xname: str = args.xname - + xfunctions: bool = args.functions + xopen: bool = args.open + xdetails: bool = args.details + xoutput: Optional[str] = args.output + xjson: bool = args.json or (xoutput is not None) try: (path, xfile) = UC.get_path_filename(xname) UF.check_analysis_results(path, xfile) @@ -739,32 +744,245 @@ def report_proofobligations(args: argparse.Namespace) -> NoReturn: xinfo = XI.XInfo() xinfo.load(path, xfile) - app = UC.get_app(path, xfile, xinfo) - proofobligations: Dict[str, Dict[str, int]] = {} # type -> status -> count + status_order = ["dis", "local", "del", "glob", "req", "v", "o"] + # two-line column headers: status_line1 is the upper row, status_line2 the lower + status_line1 = { + "dis": "safe", + "del": "delegated", + "glob": "global", + "req": "request", + "o": "open", + "local": "delegated", + "v": "violated", + } + status_line2 = { + "local": "local", + } + + # global_counts: xpo_tag -> status_tag -> count + global_counts: Dict[str, Dict[str, int]] = {} + # fn_counts: faddr -> status_tag -> count + fn_counts: Dict[str, Dict[str, int]] = {} + # fn_open_pos: faddr -> iaddr -> list of open ProofObligations + fn_open_pos: Dict[str, Dict[str, List]] = {} + # fn_detail_pos: faddr -> iaddr -> list of safe/delegated ProofObligations + fn_detail_pos: Dict[str, Dict[str, List]] = {} + # fn_labels: faddr -> display string + fn_labels: Dict[str, str] = {} + + detail_statuses = {"dis", "local", "del"} + + # flat list of records for --json export + po_records: List[Dict] = [] for fn in app.functions.values(): - polist = fn.proofobligations.proofobligations.values() - for pos in polist: + faddr = fn.faddr + fn_counts[faddr] = {} + fn_open_pos[faddr] = {} + fn_detail_pos[faddr] = {} + fn_labels[faddr] = ( + faddr + " (" + fn.name + ")" if fn.has_name() else faddr) + fn_instrs = fn.instructions if xjson else {} + for pos in fn.proofobligations.proofobligations.values(): for po in pos: - proofobligations.setdefault(po.xpo.tags[0], {}) - proofobligations[po.xpo.tags[0]].setdefault(po.status.tag, 0) - proofobligations[po.xpo.tags[0]][po.status.tag] += 1 - - print("Proof obligation counts") - print("type".ljust(8) + "discharged".rjust(10) + "delegated".rjust(10) + - "global".rjust(10) + "request".rjust(10) + "open".rjust(10)) - print("-" * 58) - for (xpotag, xpodata) in sorted(proofobligations.items()): - line: List[str] = [] - line.append(xpotag.ljust(8)) - for x in ["dis", "del", "glob", "req", "o"]: - if x in xpodata: - line.append(str(xpodata[x]).rjust(10)) - else: - line.append(" ".rjust(10)) - print("".join(line)) + tag = po.xpo.tags[0] + status = po.status.tag + global_counts.setdefault(tag, {}) + global_counts[tag].setdefault(status, 0) + global_counts[tag][status] += 1 + fn_counts[faddr].setdefault(status, 0) + fn_counts[faddr][status] += 1 + if po.is_open: + fn_open_pos[faddr].setdefault(po.iaddr, []) + fn_open_pos[faddr][po.iaddr].append(po) + if xdetails and status in detail_statuses: + fn_detail_pos[faddr].setdefault(po.iaddr, []) + fn_detail_pos[faddr][po.iaddr].append(po) + if xjson: + instr = fn_instrs.get(po.iaddr) + status_name = po_status_strings.get(status, status) + if po.msg != "none": + msg: Optional[str] = po.msg + elif po.status.is_delegated_local: + msg = "delegated to " + po.status.get_iaddr() + else: + msg = None + po_records.append({ + "faddr": faddr, + "fname": fn.name if fn.has_name() else None, + "iaddr": po.iaddr, + "instruction": instr.annotation if instr else None, + "predicate": str(po.xpo), + "predicate_type": xpo_tag_names.get(tag, tag), + "status": status_name, + "msg": msg, + }) + + active_statuses = [ + s for s in status_order + if any(s in v for v in global_counts.values())] + + total_fns = len(fn_counts) + total_pos = sum(cnt for sd in global_counts.values() for cnt in sd.values()) + + # --- JSON export --- + if xjson: + result = json.dumps({ + "binary": xname, + "functions": total_fns, + "total": total_pos, + "proof_obligations": po_records, + }, indent=2) + if xoutput is not None: + with open(xoutput, "w") as f: + f.write(result) + else: + print(result) + exit(0) + + col_w = 12 + tag_col_w = max( + (len(xpo_tag_names.get(t, t)) for t in global_counts), + default=20) + 2 + + # --- global summary --- + print(f"\nProof obligations: {xname} ({total_fns} functions, {total_pos} total)") + + def build_header(label: str, label_w: int) -> Tuple[str, str]: + """Return (line1, line2) for a two-line column header block.""" + h1 = label.ljust(label_w) + h2 = " " * label_w + for s in active_statuses: + h1 += status_line1[s].rjust(col_w) + h2 += status_line2.get(s, "").rjust(col_w) + h1 += "total".rjust(col_w) + h2 += " " * col_w + return h1, h2 + + header, header2 = build_header("Type", tag_col_w) + sep = "-" * len(header) + + print("\n" + header) + if "local" in active_statuses: + print(header2) + print(sep) + + totals: Dict[str, int] = {s: 0 for s in active_statuses} + for xpotag in sorted(global_counts, key=lambda t: xpo_tag_names.get(t, t)): + sdata = global_counts[xpotag] + fullname = xpo_tag_names.get(xpotag, xpotag) + line = fullname.ljust(tag_col_w) + row_total = 0 + for s in active_statuses: + cnt = sdata.get(s, 0) + row_total += cnt + totals[s] += cnt + line += (str(cnt) if cnt > 0 else "").rjust(col_w) + line += str(row_total).rjust(col_w) + print(line) + + print(sep) + total_line = "Total".ljust(tag_col_w) + grand_total = 0 + for s in active_statuses: + grand_total += totals[s] + total_line += str(totals[s]).rjust(col_w) + total_line += str(grand_total).rjust(col_w) + print(total_line) + + # --- per-function breakdown --- + if xfunctions: + fn_label_w = max( + (len(lbl) for lbl in fn_labels.values()), default=20) + 2 + + fn_header, fn_header2 = build_header("Function", fn_label_w) + fn_sep = "-" * len(fn_header) + + print("\n\nPer-function breakdown (sorted by open count, descending):\n") + print(fn_header) + if "local" in active_statuses: + print(fn_header2) + print(fn_sep) + + for faddr in sorted( + fn_counts, + key=lambda a: (-fn_counts[a].get("o", 0), a)): + sdata = fn_counts[faddr] + row_total = sum(sdata.values()) + if row_total == 0: + continue + line = fn_labels[faddr].ljust(fn_label_w) + for s in active_statuses: + cnt = sdata.get(s, 0) + line += (str(cnt) if cnt > 0 else "").rjust(col_w) + line += str(row_total).rjust(col_w) + print(line) + + # --- open proof obligation detail --- + if xopen: + fns_with_open = [ + faddr for faddr in fn_open_pos if fn_open_pos[faddr]] + if not fns_with_open: + print("\n\nNo open proof obligations.") + else: + print("\n\nOpen proof obligations:\n") + for faddr in sorted( + fns_with_open, + key=lambda a: (-fn_counts[a].get("o", 0), a)): + open_pos = fn_open_pos[faddr] + fn_instrs = app.functions[faddr].instructions + print(" " + fn_labels[faddr] + ":") + for iaddr in sorted(open_pos): + instr = fn_instrs.get(iaddr) + instr_text = instr.annotation if instr else "?" + print(" " + iaddr + " " + instr_text) + for po in open_pos[iaddr]: + line = " " + str(po.xpo) + if xdetails and po.msg != "none": + line += " [" + po.msg + "]" + print(line) + print() + + # --- safe / delegated proof obligation detail --- + if xdetails: + fns_with_detail = [ + faddr for faddr in fn_detail_pos if fn_detail_pos[faddr]] + if not fns_with_detail: + print("\n\nNo discharged or delegated proof obligations.") + else: + print("\n\nDischarged and delegated proof obligations:\n") + for faddr in sorted(fns_with_detail): + detail_pos = fn_detail_pos[faddr] + fn_instrs = app.functions[faddr].instructions + print(" " + fn_labels[faddr] + ":") + for status_tag in ["dis", "local", "del"]: + status_name = po_status_strings.get(status_tag, status_tag) + group = [ + (iaddr, po) + for iaddr, pos in sorted(detail_pos.items()) + for po in pos + if po.status.tag == status_tag] + if not group: + continue + print(" " + status_name + ":") + current_iaddr = None + for iaddr, po in group: + if iaddr != current_iaddr: + current_iaddr = iaddr + instr = fn_instrs.get(iaddr) + instr_text = instr.annotation if instr else "?" + print(" " + iaddr + " " + instr_text) + if po.msg != "none": + msg = po.msg + elif po.status.is_delegated_local: + msg = "delegated to " + po.status.get_iaddr() + else: + msg = "" + suffix = " [" + msg + "]" if msg else "" + print(" " + str(po.xpo) + suffix) + print() exit(0)