Codepcrefinement

chb/app/CHVersion.py

@@ -1,3 +1,3 @@
-chbversion: str = "0.3.0-20260802"
+chbversion: str = "0.3.0-20260901"
 
 minimum_required_chb_version = "0.6.0_20260802"

chb/arm/opcodes/ARMCountLeadingZeros.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2025 Aarno Labs LLC
+# Copyright (c) 2021-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
@@ -39,8 +39,9 @@
 import chb.invariants.XXprUtil as XU
 
 import chb.util.fileutil as UF
-
 from chb.util.IndexedTable import IndexedTableValue
+from chb.util.loggingutil import chklogger
+
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
@@ -143,12 +144,6 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "CLZ"]
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[1]
-        rdefs = xdata.reachingdefs
-        defuses = xdata.defuses
-        defuseshigh = xdata.defuseshigh
-
         (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
         (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree)
 
@@ -159,30 +154,22 @@ def ast_prov(
             iaddr=iaddr,
             bytestring=bytestring)
 
-        lhsasts = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-        if len(lhsasts) == 0:
-            raise UF.CHBError(
-                "CountLeadingZeros (CLZ): no lval found")
-
-        if len(lhsasts) > 1:
-            raise UF.CHBError(
-                "CountLeadingZeros (CLZ): multiple lvals in ast: "
-                + ", ".join(str(v) for v in lhsasts))
-
-        hl_lhs = lhsasts[0]
+        xd = ARMCountLeadingZerosXData(xdata)
 
-        rhsasts = XU.xxpr_to_ast_def_exprs(rhs, xdata, iaddr, astree)
-        if len(rhsasts) == 0:
-            raise UF.CHBError(
-                "CountLeadingZeros (CLZ): no argument value found")
+        if xd.is_ok:
+            lhs = xd.vrd
+            rhs = xd.xxrn
+        else:
+            chklogger.logger.error(
+                "Encountered error value for CLZ at address %s", iaddr)
+            return ([], [])
 
-        if len(rhsasts) > 1:
-            raise UF.CHBError(
-                "CountLeadingZeros (CLZ): "
-                + "multiple argument values in asts: "
-                + ", ".join(str(x) for x in rhsasts))
+        rdefs = xdata.reachingdefs
+        defuses = xdata.defuses
+        defuseshigh = xdata.defuseshigh
 
-        hl_rhs = rhsasts[0]
+        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
+        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
 
         if astree.has_variable_intro(iaddr):
             vname = astree.get_variable_intro(iaddr)

chb/cmdline/chkx

@@ -1791,6 +1791,11 @@ def parse() -> argparse.Namespace:
         nargs="*",
         default=[],
         help="list of functions that are new in xname2")
+    relationalcomparecfginfo.add_argument(
+        "--functions_removed",
+        nargs="*",
+        default=[],
+        help="list of function were removed from xname2")
     relationalcomparecfginfo.set_defaults(
         func=R.relational_compare_cfg_info)
 

chb/cmdline/commandutil.py

@@ -1697,10 +1697,13 @@ def results_predicated_instructions(args: argparse.Namespace) -> NoReturn:
 
     app = get_app(path, xfile, xinfo)
 
+    blockcount = 0
+
     blocks: Dict[str, List["BasicBlock"]] = {}
 
     for (faddr, fn) in app.functions.items():
         for b in fn.blocks.values():
+            blockcount += 1
             if b.has_control_flow():
                 blocks.setdefault(faddr, [])
                 blocks[faddr].append(b)
@@ -1711,6 +1714,11 @@ def results_predicated_instructions(args: argparse.Namespace) -> NoReturn:
             print("")
         print("\n\n")
 
+    print("\nNumber of basic blocks with predicated instrs: "
+          + str(len(blocks)) + " out of "
+          + str(blockcount) + " blocks; "
+          + str(100 * len(blocks) / blockcount) + "%")
+
     exit(0)
 
 

chb/cmdline/relationalcmds.py

@@ -1058,7 +1058,7 @@ def relational_compare_proofobligations(args: argparse.Namespace) -> NoReturn:
                     if po2 not in is1pos:
                         comparison.setdefault(iaddr, ([], []))
                         comparison[iaddr][1].append(is2pos[po2])
-                        count += len(i2pos)
+                        count += 1
             else:
                 comparison.setdefault(iaddr, ([], []))
                 comparison[iaddr][0].extend(i1pos)
@@ -1164,6 +1164,7 @@ def relational_compare_cfg_info(args: argparse.Namespace) -> NoReturn:
     xname1: str = args.xname1
     xname2: str = args.xname2
     newfunctions: List[str] = args.newfunctions
+    functionsremoved: List[str] = args.functions_removed
 
     try:
         (path1, xfile1) = UC.get_path_filename(xname1)
@@ -1202,12 +1203,19 @@ def relational_compare_cfg_info(args: argparse.Namespace) -> NoReturn:
     print("app1: " + str(len(cfginfos1)))
     print("app2: " + str(len(cfginfos2)))
 
+    cfginfos1 = [x for x in cfginfos1 if x.faddr not in functionsremoved]
+
     cfginfos2 = [x for x in cfginfos2 if x.faddr not in newfunctions]
 
     cfginfos2 = cfginfos2[:len(cfginfos1)]
 
+    cfgdiffcount = 0
+
     diffcount = 0
 
+    blockdiffs: Dict[int, int] = {}
+    instrdiffs: Dict[int, int] = {}
+
     for (ci1, ci2) in zip(cfginfos1, cfginfos2):
         if (
                 ci1.basic_blocks == ci2.basic_blocks
@@ -1219,13 +1227,23 @@ def relational_compare_cfg_info(args: argparse.Namespace) -> NoReturn:
                 str(ci1.basic_blocks).rjust(8) + "  "
                 + str(ci1.instructions) + " => " + str(ci2.instructions))
             diffcount += 1
+            instrdiff = ci2.instructions - ci1.instructions
+            instrdiffs.setdefault(instrdiff, 0)
+            instrdiffs[instrdiff] += 1
         else:
             cfgdiff = (
                 "diff: " +
                 str(ci1.basic_blocks) + " => " + str(ci2.basic_blocks)
                 + "  "
                 + str(ci1.instructions) + " => " + str(ci2.instructions))
             diffcount += 1
+            cfgdiffcount += 1
+            instrdiff = ci2.instructions - ci1.instructions
+            instrdiffs.setdefault(instrdiff, 0)
+            instrdiffs[instrdiff] += 1
+            blockdiff = ci2.basic_blocks - ci1.basic_blocks
+            blockdiffs.setdefault(blockdiff, 0)
+            blockdiffs[blockdiff] += 1
         if ci1.name is not None and ci2.name is not None and ci1.name == ci2.name:
             name = ci1.name
         elif ci1.name is not None:
@@ -1240,6 +1258,8 @@ def relational_compare_cfg_info(args: argparse.Namespace) -> NoReturn:
               + name)
 
     print("\nNumber of functions different: " + str(diffcount))
+    print("\nNumber of functions added    : " + str(len(newfunctions)))
+    print("\nNumber of functions removed  : " + str(len(functionsremoved)))
 
     exit(0)