ARM: convert annotations to handle result types

Author: sipma

chb/app/InstrXData.py

@@ -497,6 +497,25 @@ def get_base_update_xpr(self) -> XXpr:
                 "Unexpected error value in base-update expression")
         return self.xprdictionary.xpr(xbuval)
 
+    def has_return_xpr(self) -> bool:
+        return any(s.startswith("return:") for s in self.tags)
+
+    def get_return_xpr(self) -> XXpr:
+        rvtag = next(t for t in self.tags if t.startswith("return:"))
+        rvix = int(rvtag[7:])
+        rval = self.args[rvix]
+        if rval == -2:
+            raise UF.CHBError("Unexpected error in return value")
+        return self.xprdictionary.xpr(rval)
+
+    def get_return_xxpr(self) -> XXpr:
+        rvtag = next(t for t in self.tags if t.startswith("return:"))
+        rvix = int(rvtag[7:])
+        rval = self.args[rvix + 1]
+        if rval == -2:
+            raise UF.CHBError("Unexpected error in rewritten return value")
+        return self.xprdictionary.xpr(rval)
+
     @property
     def is_aggregate_jumptable(self) -> bool:
         return "agg-jt" in self.tags

chb/arm/ARMOpcode.py

@@ -146,22 +146,22 @@ def is_writeback(self) -> bool:
 
     def get_base_update_var(self) -> "XVariable":
         if self.is_writeback:
-            return self.get_base_update_var()
+            return self.xdata.get_base_update_var()
         else:
             raise UF.CHBError(
                 self.__class__.__name__ + " does not have writeback")
 
     def get_base_update_xpr(self) -> "XXpr":
         if self.is_writeback:
-            return self.get_base_update_xpr()
+            return self.xdata.get_base_update_xpr()
         else:
             raise UF.CHBError(
                 self.__class__.__name__ + " does not have writeback")
 
     def writeback_update(self) -> str:
         if self.xdata.has_base_update():
-            vbu = self.xdata.get_base_update_var()
-            xbu = self.xdata.get_base_update_xpr()
+            vbu = self.get_base_update_var()
+            xbu = self.get_base_update_xpr()
             return "; " + str(vbu) + " := " + str(xbu)
         else:
             return ""

chb/arm/opcodes/ARMAdd.py

@@ -97,7 +97,7 @@ def rresult(self) -> "XXpr":
     @property
     def result_simplified(self) -> str:
         return simplify_result(
-            self._xdata.args[3], self._xdata.args[4], self.result, self.rresult)
+            self.xdata.args[3], self.xdata.args[4], self.result, self.rresult)
 
     @property
     def xxrn(self) -> "XXpr":

chb/arm/opcodes/ARMBitwiseNot.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021-2024  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.ast.ASTNode as AST
@@ -39,15 +39,50 @@
 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
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMBitwiseNotXData(ARMOpcodeXData):
+
+    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 result(self) -> "XXpr":
+        return self.xpr(1, "result")
+
+    @property
+    def rresult(self) -> "XXpr":
+        return self.xpr(2, "rresult")
+
+    @property
+    def result_simplified(self) -> str:
+        return simplify_result(
+            self.xdata.args[1], self.xdata.args[2], self.result, self.rresult)
+
+    @property
+    def annotation(self) -> str:
+        assignment = str(self.vrd) + " := " + self.result_simplified
+        return self.add_instruction_condition(assignment)
 
 
 @armregistry.register_tag("MVN", ARMOpcode)
-class ARMBitwiseBitwiseNot(ARMOpcode):
+class ARMBitwiseNot(ARMOpcode):
     """Bitwise inverse of a register or immediate value.
 
     MVN{S}<c> <Rd>, <Rm> {, <shift>}
@@ -70,10 +105,7 @@ class ARMBitwiseBitwiseNot(ARMOpcode):
     useshigh[0]: lhs
     """
 
-    def __init__(
-            self,
-            d: "ARMDictionary",
-            ixval: IndexedTableValue) -> None:
+    def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
         ARMOpcode.__init__(self, d, ixval)
         self.check_key(2, 4, "BitwiseNot")
 
@@ -96,18 +128,11 @@ def is_writeback(self) -> bool:
         return self.args[0] == 1
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        result = xdata.xprs[1]
-        rresult = xdata.xprs[2]
-        xresult = simplify_result(xdata.args[2], xdata.args[1], result, rresult)
-        assignment = lhs + " := " + xresult
-        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
+        xd = ARMBitwiseNotXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -133,9 +158,15 @@ def ast_prov(
             annotations=annotations)
 
         # high-level assignment
+        xd = ARMBitwiseNotXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
+
+        lhs = xd.vrd
+        rhs = xd.rresult
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[2]
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh

chb/arm/opcodes/ARMBitwiseOrNot.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
 
 import chb.ast.ASTNode as AST
@@ -39,11 +39,54 @@
 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:
-    import chb.arm.ARMDictionary
+    from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMBitwiseOrNotXData(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 xrm(self) -> "XXpr":
+        return self.xpr(1, "xrm")
+
+    @property
+    def xrmn(self) -> "XXpr":
+        return self.xpr(2, "xrmn")
+
+    @property
+    def result(self) -> "XXpr":
+        return self.xpr(3, "result")
+
+    @property
+    def rresult(self) -> "XXpr":
+        return self.xpr(4, "rresult")
+
+    @property
+    def result_simplified(self) -> str:
+        return simplify_result(
+            self.xdata.args[4], self.xdata.args[5], self.result, self.rresult)
+
+    @property
+    def annotation(self) -> str:
+        assignment = str(self.vrd) + " := " + self.result_simplified
+        return self.add_instruction_condition(assignment)
 
 
 @armregistry.register_tag("ORN", ARMOpcode)
@@ -74,10 +117,7 @@ class ARMBitwiseOrNot(ARMOpcode):
     useshigh[0]: lhs
     """
 
-    def __init__(
-            self,
-            d: "chb.arm.ARMDictionary.ARMDictionary",
-            ixval: IndexedTableValue) -> None:
+    def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
         ARMOpcode.__init__(self, d, ixval)
         self.check_key(2, 4, "BitwiseOrNot")
 
@@ -99,18 +139,11 @@ def is_writeback(self) -> bool:
         return self.args[0] == 1
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        result = xdata.xprs[3]
-        rresult = xdata.xprs[4]
-        xresult = simplify_result(xdata.args[4], xdata.args[5], result, rresult)
-        assignment = lhs + " := " + xresult
-        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
+        xd = ARMBitwiseOrNotXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -122,14 +155,6 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "ORN"]
 
-        lhs = xdata.vars[0]
-        rhs1 = xdata.xprs[0]
-        rhs2 = xdata.xprs[1]
-        rhs4 = xdata.xprs[4]
-        rdefs = xdata.reachingdefs
-        defuses = xdata.defuses
-        defuseshigh = xdata.defuseshigh
-
         (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
         (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree)
         (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree)
@@ -143,27 +168,21 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        lhsasts = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-        if len(lhsasts) == 0:
-            raise UF.CHBError("BitwiseOrNot (ORN): no lval found")
-
-        if len(lhsasts) > 1:
-            raise UF.CHBError(
-                "BitwiseOrNot (ORN): multiple lvals found: "
-                + ", ".join(str(v) for v in lhsasts))
-
-        hl_lhs = lhsasts[0]
+        xd = ARMBitwiseOrNotXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
 
-        rhsasts = XU.xxpr_to_ast_def_exprs(rhs4, xdata, iaddr, astree)
-        if len(rhsasts) == 0:
-            raise UF.CHBError("BitwiseOrNot (ORN): no lval found")
+        lhs = xd.vrd
+        rhs = xd.rresult
 
-        if len(rhsasts) > 1:
-            raise UF.CHBError(
-                "BitwiseOrNot (ORN): multiple rhs values found: "
-                + ", ".join(str(v) for v 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)
 
         hl_assign = astree.mk_assign(
             hl_lhs,