ARM: convert astprov to handle result types

Author: sipma

chb/arm/ARMOpcode.py

@@ -141,6 +141,7 @@ def add_instruction_condition(self, s: str) -> str:
         else:
             return s
 
+    @property
     def is_writeback(self) -> bool:
         return self.xdata.has_base_update()
 

chb/arm/opcodes/ARMBitwiseAnd.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,11 +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 ARMBitwiseAndXData(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 result(self) -> "XXpr":
+        return self.xpr(2, "result")
+
+    @property
+    def rresult(self) -> "XXpr":
+        return self.xpr(3, "rresult")
+
+    @property
+    def result_simplified(self) -> str:
+        return simplify_result(
+            self.xdata.args[3], self.xdata.args[4], 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("AND", ARMOpcode)
@@ -96,18 +135,11 @@ def mnemonic_extension(self) -> str:
         return cc + wide
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        result = xdata.xprs[2]
-        rresult = xdata.xprs[3]
-        xresult = simplify_result(xdata.args[3], xdata.args[4], 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 = ARMBitwiseAndXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -140,8 +172,14 @@ def ast_prov(
 
         # high-level assignment
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[3]
+        xd = ARMBitwiseAndXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
+
+        lhs = xd.vrd
+        rhs = xd.rresult
 
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh

chb/arm/opcodes/ARMCompare.py

@@ -132,7 +132,6 @@ def ast_prov(
                 List[AST.ASTInstruction], List[AST.ASTInstruction]]:
         """Creates assignments of the subtraction performed with lhs ignored."""
 
-        xd = ARMCompareXData(xdata)
         annotations: List[str] = [iaddr, "CMP"]
 
         # low-level assignment
@@ -150,6 +149,7 @@ def ast_prov(
 
         # high-level assignment
 
+        xd = ARMCompareXData(xdata)
         if not xd.is_ok:
             chklogger.logger.error(
                 "Error value encountered at address %s", iaddr)

chb/arm/opcodes/ARMCompareNegative.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,11 +39,38 @@
 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 ARMCompareNegativeXData(ARMOpcodeXData):
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def xrm(self) -> "XXpr":
+        return self.xpr(1, "xrm")
+
+    @property
+    def result(self) -> "XXpr":
+        return self.xpr(2, "result")
+
+    @property
+    def annotation(self) -> str:
+        ann = "compare-negative " + str(self.xrn) + " and " + str(self.xrm)
+        ann += " (" + str(self.result) + ")"
+        return self.add_instruction_condition(ann)
 
 
 @armregistry.register_tag("CMN", ARMOpcode)
@@ -65,10 +92,7 @@ class ARMCompareNegative(ARMOpcode):
     rdefs[1]: xrm
     """
 
-    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, 2, "CompareNegative")
 
@@ -81,23 +105,11 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args]
 
     def annotation(self, xdata: InstrXData) -> str:
-        rhs1 = str(xdata.xprs[0])
-        rhs2 = str(xdata.xprs[1])
-        result = str(xdata.xprs[2])
-        ann = (
-            "compare-negative "
-            + str(rhs1)
-            + " and "
-            + str(rhs2)
-            + " ("
-            + str(result))
-        if xdata.has_unknown_instruction_condition():
-            return "if ? then " + ann
-        elif xdata.has_instruction_condition():
-            c = str(xdata.xprs[1])
-            return "if " + c + " then " + ann
+        xd = ARMCompareNegativeXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return ann
+            return "Error value"
 
     def ast_prov(
             self,
@@ -124,7 +136,13 @@ def ast_prov(
 
         # high-level assignment
 
-        rhs = xdata.xprs[2]
+        xd = ARMCompareNegativeXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
+
+        rhs = xd.result
         rdefs = xdata.reachingdefs
 
         hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)