Relationalprepare

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"

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:

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]] = []

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(),

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(
@@ -969,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
@@ -998,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()
@@ -1061,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)