Predicatedinstructions

chb/app/CHVersion.py

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

chb/app/InstrXData.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
@@ -83,7 +83,9 @@ def __init__(
         self._strs: List[str] = []
         self._ints: List[int] = []
         self._reachingdefs: List[Optional[ReachingDefFact]] = []
+        self._reachingdefdoubles: List[Optional[ReachingDefFact]] = []
         self._defuses: List[Optional[DefUse]] = []
+        self._defusedoubles: List[Optional[DefUse]] = []
         self._defuseshigh: List[Optional[DefUseHigh]] = []
         self._flagreachingdefs: List[Optional[FlagReachingDefFact]] = []
 
@@ -222,6 +224,12 @@ def reachingdefs(self) -> List[Optional[ReachingDefFact]]:
             self._expand()
         return self._reachingdefs
 
+    @property
+    def reachingdefdoubles(self) -> List[Optional[ReachingDefFact]]:
+        if not self.expanded:
+            self._expand()
+        return self._reachingdefdoubles
+
     @property
     def flag_reachingdefs(self) -> List[Optional[FlagReachingDefFact]]:
         if not self.expanded:
@@ -234,6 +242,12 @@ def defuses(self) -> List[Optional[DefUse]]:
             self._expand()
         return self._defuses
 
+    @property
+    def defusedoubles(self) -> List[Optional[DefUse]]:
+        if not self.expanded:
+            self._expand()
+        return self._defusedoubles
+
     @property
     def defuseshigh(self) -> List[Optional[DefUseHigh]]:
         if not self.expanded:
@@ -397,11 +411,21 @@ def _expand(self) -> None:
                 rdef = varinvd.var_invariant_fact(arg) if arg >= 0 else None
                 rdef = cast(Optional[ReachingDefFact], rdef)
                 self._reachingdefs.append(rdef)
+            elif c == "m":
+                varinvd = self.varinvdictionary
+                rdefdouble = varinvd.var_invariant_fact(arg) if arg >= 0 else None
+                rdefdouble = cast(Optional[ReachingDefFact], rdefdouble)
+                self._reachingdefdoubles.append(rdefdouble)
             elif c == "d":
                 varinvd = self.varinvdictionary
                 use = varinvd.var_invariant_fact(arg) if arg >= 0 else None
                 use = cast(Optional[DefUse], use)
                 self._defuses.append(use)
+            elif c == "n":
+                varinvd = self.varinvdictionary
+                usedouble = varinvd.var_invariant_fact(arg) if arg >= 0 else None
+                usedouble = cast(Optional[DefUse], usedouble)
+                self._defusedoubles.append(usedouble)
             elif c == "h":
                 varinvd = self.varinvdictionary
                 usehigh = varinvd.var_invariant_fact(arg) if arg > 0 else None
@@ -671,6 +695,42 @@ def is_ternary_assignment(self) -> bool:
     def is_nondet_ternary_assignment(self) -> bool:
         return "agg:ternassign:nd" in self.tags
 
+    @property
+    def is_wide_move(self) -> bool:
+        return "agg:widemove" in self.tags
+
+    @property
+    def is_wide_move_not(self) -> bool:
+        return "agg:widemovenot" in self.tags
+
+    @property
+    def is_wide_add(self) -> bool:
+        return "agg:wideadd" in self.tags
+
+    @property
+    def is_wide_subtract(self) -> bool:
+        return "agg:widesubtract" in self.tags
+
+    @property
+    def is_wide_reversesubtract(self) -> bool:
+        return "agg:widereversesubtract" in self.tags
+
+    @property
+    def is_wide_and(self) -> bool:
+        return "agg:wideand" in self.tags
+
+    @property
+    def is_wide_or(self) -> bool:
+        return "agg:wideor" in self.tags
+
+    @property
+    def is_wide_xor(self) -> bool:
+        return "agg:widexor" in self.tags
+
+    @property
+    def is_wide_op_instruction(self) -> bool:
+        return "wop" in self.tags
+
     @property
     def is_aggregate_jumptable(self) -> bool:
         return "agg-jt" in self.tags

chb/arm/ARMCallOpcode.py

@@ -135,14 +135,21 @@ def cx_arguments(self) -> List["XXpr"]:
     @property
     def argumentxvars(self) -> List["XXpr"]:
         argcount = self.argument_count
+        xprcount = len(self._xdata.xprs_r)
         argvars: List["XXpr"] = []
         for i in range(argcount):
-            x = self._xdata.xprs_r[i + argcount]
-            if x is None:
+            if i + argcount < xprcount:
+                x = self._xdata.xprs_r[i + argcount]
+                if x is None:
+                    raise UF.CHBError(
+                        "Unexpected None-value call argument at index "
+                        + str(i))
+                argvars.append(x)
+            else:
                 raise UF.CHBError(
-                    "Unexpected None-value call argument at index "
-                    + str(i))
-            argvars.append(x)
+                    "argumentxvars: out of range in " + str(self.calltarget)
+                    + "; argcount: " + str(argcount)
+                    + "; xprcount: " + str(xprcount))
         return argvars
 
     def argument(self, index: int) -> Tuple[Optional["XXpr"], Optional[str]]:

chb/arm/ARMInstruction.py

@@ -251,7 +251,7 @@ def annotation(self) -> str:
             return f"subsumed by {aggaddr}"
         elif self.subsumes:
             ann = self.opcode.annotation(self.xdata)
-            dependents = self.xdata.subsumes()
+            dependents = [str(s) for s in self.xdata.subsumes()]
             return ann + " (subsumes [" + ", ".join(dependents) + "])"
         else:
             return self.opcode.annotation(self.xdata)

chb/arm/ARMOpcode.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
@@ -98,6 +98,59 @@ def simplify_result(id1: int, id2: int, x1: XXpr, x2: XXpr) -> str:
     }
 
 
+unary_wopvar_indices = {
+    "vrdlohi": 0,
+    "vrdlo": 1,
+    "vrdhi": 2
+}
+
+unary_wopxpr_indices = {
+    "xrnlo": 0,
+    "xrnhi": 1,
+    "rresultw": 2,
+    "rresultlo": 3,
+    "rresulthi": 4,
+    "xxrnlo": 5,
+    "xxrnhi": 6,
+    "xxrnw": 7
+}
+
+unary_wopcxpr_indices = {
+    "cresultw": 0,
+    "cresultlo": 1,
+    "cresulthi": 2
+}
+
+
+binary_wopvar_indices = {
+    "vrdlohi": 0,
+    "vrdlo": 1,
+    "vrdhi": 2
+}
+
+binary_wopxpr_indices = {
+    "xrnlo": 0,
+    "xrnhi": 1,
+    "xrmlo": 2,
+    "xrmhi": 3,
+    "rresultw": 4,
+    "rresultlo": 5,
+    "rresulthi": 6,
+    "xxrnlo": 7,
+    "xxrnhi": 8,
+    "xxrmlo": 9,
+    "xxrmhi": 10,
+    "xxrnw": 11,
+    "xxrmw": 12
+}
+
+binary_wopcxpr_indices = {
+    "cresultw": 0,
+    "cresultlo": 1,
+    "cresulthi": 2
+}
+
+
 def get_extension(e: str) -> str:
     if e in extensions:
         return extensions[e]
@@ -129,6 +182,20 @@ def var(self, index: int, name: str) -> "XVariable":
                 self.__class__.__name__ + ":" + name + " has an error value")
         return v
 
+    def unary_wopvar(self, name: str) -> "XVariable":
+        if name in unary_wopvar_indices:
+            return self.var(unary_wopvar_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognized")
+
+    def binary_wopvar(self, name: str) -> "XVariable":
+        if name in binary_wopvar_indices:
+            return self.var(binary_wopvar_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognized")
+
     def has_var(self, index: int) -> bool:
         return self.xdata.has_var_r(index)
 
@@ -163,12 +230,38 @@ def xpr(self, index: int, name: str) -> "XXpr":
                 self.__class__.__name__ + ":" + name + " has an error value")
         return x
 
+    def unary_wopxpr(self, name: str) -> "XXpr":
+        if name in unary_wopxpr_indices:
+            return self.xpr(unary_wopxpr_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognized")
+
+    def binary_wopxpr(self, name: str) -> "XXpr":
+        if name in binary_wopxpr_indices:
+            return self.xpr(binary_wopxpr_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognized")
+
     def has_xpr(self, index: int) -> bool:
         return self.xdata.has_xpr_r(index)
 
     def is_xpr_ok(self, index: int) -> bool:
         return self.xdata.is_xpr_ok(index)
 
+    def is_unary_wopxpr_ok(self, name: str) -> bool:
+        if name in unary_wopxpr_indices:
+            return self.is_xpr_ok(unary_wopxpr_indices[name])
+        else:
+            return False
+
+    def is_binary_wopxpr_ok(self, name: str) -> bool:
+        if name in binary_wopxpr_indices:
+            return self.is_xpr_ok(binary_wopxpr_indices[name])
+        else:
+            return False
+
     def cxpr(self, index: int, name: str) -> "XXpr":
         if index >= len(self.xdata.cxprs_r):
             raise UF.CHBError(
@@ -180,12 +273,38 @@ def cxpr(self, index: int, name: str) -> "XXpr":
                 self.__class__.__name__ + ":" + name + " has an error value")
         return cx
 
+    def unary_wopcxpr(self, name: str) -> "XXpr":
+        if name in unary_wopcxpr_indices:
+            return self.cxpr(unary_wopcxpr_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognize")
+
+    def binary_wopcxpr(self, name: str) -> "XXpr":
+        if name in binary_wopcxpr_indices:
+            return self.cxpr(binary_wopcxpr_indices[name], name)
+        else:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " not recognized")
+
     def has_cxpr(self, index: int) -> bool:
         return self.xdata.has_cxpr_r(index)
 
     def is_cxpr_ok(self, index: int) -> bool:
         return self.xdata.is_cxpr_ok(index)
 
+    def is_unary_wopcxpr_ok(self, name: str) -> bool:
+        if name in unary_wopcxpr_indices:
+            return self.is_cxpr_ok(unary_wopcxpr_indices[name])
+        else:
+            return False
+
+    def is_binary_wopcxpr_ok(self, name: str) -> bool:
+        if name in binary_wopcxpr_indices:
+            return self.is_cxpr_ok(binary_wopcxpr_indices[name])
+        else:
+            return False
+
     def has_instruction_condition(self) -> bool:
         return self.xdata.has_instruction_condition()
 

chb/arm/opcodes/ARMAdd.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