Liftingsupport

chb/arm/opcodes/ARMBitFieldInsert.py

@@ -53,8 +53,18 @@
 class ARMBitFieldInsertXData(ARMOpcodeXData):
     """BFI <rd> <rn>"""
 
-    def __init__(self, xdata: InstrXData) -> None:
+    def __init__(self, xdata: InstrXData, lsb: int, width: int) -> None:
         ARMOpcodeXData.__init__(self, xdata)
+        self._lsb = lsb
+        self._width = width
+
+    @property
+    def lsb(self) -> int:
+        return self._lsb
+
+    @property
+    def width(self) -> int:
+        return self._width
 
     @property
     def vrd(self) -> "XVariable":
@@ -68,6 +78,23 @@ def xrd(self) -> "XXpr":
     def xrn(self) -> "XXpr":
         return self.xpr(1, "xrn")
 
+    @property
+    def annotation(self) -> str:
+        lhs = str(self.vrd)
+        rhs1 = str(self.xrd)
+        rhs2 = str(self.xrn)
+        assign = (
+            lhs
+            + " := bit-field-insert("
+            + rhs1
+            + ", "
+            + rhs2
+            + ", lsb:"
+            + str(self.lsb)
+            + ", width:"
+            + str(self.width))
+        return self.add_instruction_condition(assign)
+
 
 @armregistry.register_tag("BFI", ARMOpcode)
 class ARMBitFieldInsert(ARMOpcode):
@@ -123,30 +150,8 @@ def width(self) -> int:
         return self.args[2]
 
     def annotation(self, xdata: InstrXData) -> str:
-        xd = ARMBitFieldInsertXData(xdata)
-        if xd.is_ok:
-            lhs = str(xd.vrd)
-            rhs1 = str(xd.xrd)
-            rhs2 = str(xd.xrn)
-            assignment = (
-                lhs
-                + " := bit-field-insert("
-                + rhs1
-                + ", "
-                + rhs2
-                + ", lsb:"
-                + str(self.lsb)
-                + ", width:"
-                + str(self.width))
-            if xdata.has_unknown_instruction_condition():
-                return "if ? then " + assignment
-            elif xdata.has_instruction_condition():
-                c = str(xdata.xprs[1])
-                return "if " + c + " then " + assignment
-            else:
-                return assignment
-        else:
-            return "Error value"
+        xd = ARMBitFieldInsertXData(xdata, self.lsb, self.width)
+        return xd.annotation
 
     def ast_prov(
             self,
@@ -168,9 +173,11 @@ def ast_prov(
 
             return ([], [nopinstr])
 
-        lhs = xdata.vars[0]
-        rhs1 = xdata.xprs[0]
-        rhs2 = xdata.xprs[1]
+        xd = ARMBitFieldInsertXData(xdata, self.lsb, self.width)
+
+        lhs = xd.vrd
+        rhs1 = xd.xrd
+        rhs2 = xd.xrn
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh

chb/arm/opcodes/ARMByteReversePackedHalfword.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2023  Aarno Labs LLC
+# Copyright (c) 2021-2025  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
@@ -30,7 +30,7 @@
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 from chb.ast.ARMIntrinsics import ARMIntrinsics
@@ -44,6 +44,37 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XprCompound, XprConstant, XXpr
+
+
+class ARMByteReversePackedHalfwordXData(ARMOpcodeXData):
+    """REV16 <rd> <rm>"""
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrm(self) -> "XXpr":
+        return self.xpr(0, "xrm")
+
+    @property
+    def xxrm(self) -> "XXpr":
+        return self.xpr(1, "xxrm")
+
+    @property
+    def annotation(self) -> str:
+        if self.is_ok:
+            lhs = str(self.vrd)
+            rhs = str(self.xxrm)
+            assign = lhs + " := __rev16(" + str(rhs) + ") intrinsic"
+            return self.add_instruction_condition(assign)
+        else:
+            return "REV16: error"
 
 
 @armregistry.register_tag("REV16", ARMOpcode)
@@ -89,16 +120,8 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args[:-1]]
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        rhs = str(xdata.xprs[1])
-        assignment = lhs + " := __rev16(" + str(rhs) + ") intrinsic"
-        if xdata.has_unknown_instruction_condition():
-            return "if ? then " + assignment
-        elif xdata.has_instruction_condition():
-            c = str(xdata.xprs[1])
-            return "if " + c + " then " + assignment
-        else:
-            return assignment
+        xd = ARMByteReversePackedHalfwordXData(xdata)
+        return xd.annotation
 
     # --------------------------------------------------------------------------
     # Operation

chb/arm/opcodes/ARMMove.py

@@ -92,6 +92,10 @@ def is_cresult_ok(self) -> bool:
 
     @property
     def annotation(self) -> str:
+        if self.xdata.instruction_is_subsumed():
+            return "subsumed by " + self.xdata.subsumed_by()
+        if self.xdata.instruction_subsumes():
+            return "subsumes " + ", ".join(self.xdata.subsumes())
         cx = " (C: " + (str(self.cresult) if self.is_cresult_ok else "None") + ")"
         rhs = str(self.result) if self.is_result_ok else str(self.xrm)
         assignment = str(self.vrd) + " := " + rhs + cx

chb/arm/opcodes/ARMSignedBitFieldExtract.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2022 Aarno Labs LLC
+# Copyright (c) 2021-2025 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
@@ -25,20 +25,50 @@
 # SOFTWARE.
 # ------------------------------------------------------------------------------
 
-from typing import List, TYPE_CHECKING
+from typing import List, Tuple, TYPE_CHECKING
 
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 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
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMSignedBitFieldExtractXData(ARMOpcodeXData):
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xxrn(self) -> "XXpr":
+        return self.xpr(1, "xxrn")
+
+    @property
+    def result_simplified(self) -> str:
+        return simplify_result(
+            self.xdata.args[1], self.xdata.args[2], self.xrn, self.xxrn)
+
+    @property
+    def annotation(self) -> str:
+        assignment = str(self.vrd) + " := " + self.result_simplified
+        return self.add_instruction_condition(assignment)
 
 
 @armregistry.register_tag("SBFX", ARMOpcode)
@@ -64,15 +94,8 @@ def operands(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args]
 
     def annotation(self, xdata: InstrXData) -> str:
-        """xdata format: a:vxx .
-
-        vars[0]: lhs
-        xprs[0]: rhs1
-        xprs[1]: value to be stored (syntactic)
-        """
-
-        lhs = str(xdata.vars[0])
-        result = xdata.xprs[0]
-        rresult = xdata.xprs[1]
-        xresult = simplify_result(xdata.args[1], xdata.args[2], result, rresult)
-        return lhs + " := " + xresult
+        xd = ARMSignedBitFieldExtractXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
+        else:
+            return "Error value"

chb/arm/opcodes/ARMSignedExtendHalfword.py

@@ -77,6 +77,9 @@ def annotation(self, xdata: InstrXData) -> str:
         xprs[1]: rhs (simplified)
         """
 
+        '''
         lhs = str(xdata.vars[0])
         result = str(xdata.xprs[1])
         return lhs + " := " + result
+        '''
+        return "pending"

chb/arm/opcodes/ARMUnsignedExtendAddByte.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021 Aarno Labs LLC
+# Copyright (c) 2021-2025 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
@@ -30,7 +30,7 @@
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
-from chb.arm.ARMOpcode import ARMOpcode, simplify_result
+from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
 import chb.util.fileutil as UF
@@ -39,6 +39,43 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XprCompound, XprConstant, XXpr
+
+
+class ARMUnsignedExtendAddByteXData(ARMOpcodeXData):
+    """
+    Data format:
+    - variables:
+    0: vrd
+
+    - expressions:
+    0: xrn
+    1: xrm
+    """
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xrm(self) -> "XXpr":
+        return self.xpr(1, "xrm")
+
+    @property
+    def annotation(self) -> str:
+        lhs = str(self.vrd)
+        rhs1 = str(self.xrn)
+        rhs2 = str(self.xrm)
+        assign = lhs + " := extend_add_byte(" + rhs1 + ", " + rhs2 + ")"
+        return self.add_instruction_condition(assign)
 
 
 @armregistry.register_tag("UXTAB", ARMOpcode)
@@ -65,14 +102,5 @@ def operands(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[i]) for i in [0, 1, 2]]
 
     def annotation(self, xdata: InstrXData) -> str:
-        """xdata format a:vxx .
-
-        vars[0]: lhs
-        xprs[0]: rhs1
-        xprs[1]: rhs2
-        """
-
-        lhs = str(xdata.vars[0])
-        op1 = str(xdata.xprs[0])
-        op2 = str(xdata.xprs[1])
-        return lhs + ":= extend_add_byte(" + op1 + ", " + op2 + ")"
+        xd = ARMUnsignedExtendAddByteXData(xdata)
+        return xd.annotation