ARM: convert astprov to handle result types

Author: sipma

chb/arm/ARMInstruction.py

@@ -309,17 +309,22 @@ def ast_switch_condition_prov(self, astree: ASTInterface) -> Tuple[
             jumptable = cast(
                 "ARMJumpTable", self.armfunction.get_jumptable(self.iaddr))
             indexop = jumptable.index_operand
-            condition = self.xdata.xprs[1]
-            (ll_cond, _, _) = indexop.ast_rvalue(astree)
-            hl_cond = XU.xxpr_to_ast_def_expr(
-                condition, self.xdata, self.iaddr, astree)
-
-            astree.add_expr_mapping(hl_cond, ll_cond)
-            astree.add_expr_reachingdefs(hl_cond, self.xdata.reachingdefs)
-            astree.add_condition_address(
-                ll_cond, (self.xdata.subsumes() + [self.iaddr]))
-
-            return (hl_cond, ll_cond)
+            condition = self.xdata.xprs_r[1]
+            if condition is not None:
+                (ll_cond, _, _) = indexop.ast_rvalue(astree)
+                hl_cond = XU.xxpr_to_ast_def_expr(
+                    condition, self.xdata, self.iaddr, astree)
+
+                astree.add_expr_mapping(hl_cond, ll_cond)
+                astree.add_expr_reachingdefs(hl_cond, self.xdata.reachingdefs)
+                astree.add_condition_address(
+                    ll_cond, (self.xdata.subsumes() + [self.iaddr]))
+
+                return (hl_cond, ll_cond)
+            else:
+                chklogger.logger.error(
+                    "Error value encountered at address %s", self.iaddr)
+                raise UF.CHBError("Jumptable without condition")
 
         else:
             return self.opcode.ast_switch_condition_prov(

chb/arm/opcodes/ARMBitwiseExclusiveOr.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.util.fileutil as UF
@@ -39,11 +39,49 @@
 from chb.astinterface.ASTInterface import ASTInterface
 
 import chb.invariants.XXprUtil as XU
-
 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 ARMBitwiseExclusiveOrXData(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("EOR", ARMOpcode)
@@ -74,10 +112,7 @@ class ARMBitwiseExclusiveOr(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, 5, "BitwiseExclusiveOr")
 
@@ -95,18 +130,11 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args[1: -1]]
 
     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 = ARMBitwiseExclusiveOrXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -137,8 +165,14 @@ def ast_prov(
 
         # high-level assignment
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[3]
+        xd = ARMBitwiseExclusiveOrXData(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/ARMBitwiseNot.py

@@ -73,7 +73,7 @@ def rresult(self) -> "XXpr":
     @property
     def result_simplified(self) -> str:
         return simplify_result(
-            self.xdata.args[1], self.xdata.args[2], self.result, self.rresult)
+            self.xdata.args[2], self.xdata.args[3], self.result, self.rresult)
 
     @property
     def annotation(self) -> str:
@@ -158,6 +158,7 @@ def ast_prov(
             annotations=annotations)
 
         # high-level assignment
+
         xd = ARMBitwiseNotXData(xdata)
         if not xd.is_ok:
             chklogger.logger.error(

chb/arm/opcodes/ARMCompareBranchZero.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
@@ -46,6 +46,41 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XXpr import XXpr
+
+
+class ARMCompareBranchZeroXData(ARMOpcodeXData):
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def xrn(self) -> "XXpr":
+        return self.xpr(0, "xrn")
+
+    @property
+    def txpr(self) -> "XXpr":
+        return self.xpr(1, "txpr")
+
+    @property
+    def fxpr(self) -> "XXpr":
+        return self.xpr(2, "fxpr")
+
+    @property
+    def tcond(self) -> "XXpr":
+        return self.xpr(3, "tcond")
+
+    @property
+    def fcond(self) -> "XXpr":
+        return self.xpr(4, "fcond")
+
+    @property
+    def xtgt(self) -> "XXpr":
+        return self.xpr(5, "xtgt")
+
+    @property
+    def annotation(self) -> str:
+        return "if " + str(self.tcond) + " goto " + str(self.xtgt)
 
 
 @armregistry.register_tag("CBZ", ARMOpcode)
@@ -67,10 +102,7 @@ class ARMCompareBranchZero(ARMOpcode):
     xprs[5]: target
     """
 
-    def __init__(
-            self,
-            d: "ARMDictionary",
-            ixval: IndexedTableValue) -> None:
+    def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
         ARMOpcode.__init__(self, d, ixval)
         self.check_key(1, 2, "CompareBranchZero")
 
@@ -84,14 +116,22 @@ def opargs(self) -> List[ARMOperand]:
 
     def ft_conditions(self, xdata: InstrXData) -> Sequence[XXpr]:
         if xdata.has_branch_conditions():
-            return [xdata.xprs[4], xdata.xprs[3]]
+            xd = ARMCompareBranchZeroXData(xdata)
+            if xd.is_ok:
+                return [xd.fcond, xd.tcond]
+            else:
+                chklogger.logger.warning(
+                    "CBZ: Encountered error condition at address")
+                return []
         else:
             return []
 
     def annotation(self, xdata: InstrXData) -> str:
-        xpr = str(xdata.xprs[3])
-        tgt = str(xdata.xprs[5])
-        return "if " + xpr + " goto " + tgt
+        xd = ARMCompareBranchZeroXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
+        else:
+            return "Error value"
 
     def ast_prov(
             self,

chb/arm/opcodes/ARMLoadRegister.py

@@ -56,22 +56,6 @@ class ARMLoadRegisterXData(ARMOpcodeXData):
 
     def __init__(self, xdata: InstrXData) -> None:
         ARMOpcodeXData.__init__(self, xdata)
-        self._varnames = ["vrt", "vmem"]
-        self._xprnames = ["xrn", "xrm", "xmem", "xrmem", "xaddr"]
-
-    @property
-    def error_value_indices(self) -> Tuple[List[int], List[int]]:
-        return self._xdata.error_values
-
-    @property
-    def error_value_names(self) -> List[str]:
-        result: List[str] = []
-        (vars_e, xprs_e) = self.error_value_indices
-        for i in vars_e:
-            result.append(self._varnames[i])
-        for i in xprs_e:
-            result.append(self._xprnames[i])
-        return result
 
     @property
     def vrt(self) -> "XVariable":
@@ -102,19 +86,19 @@ def xaddr(self) -> "XXpr":
         return self.xpr(4, "xaddr")
 
     @property
-    def is_memval_unknown(self) -> bool:
-        return "xrmem" in self.error_value_names
+    def is_xrmem_unknown(self) -> bool:
+        return self.xdata.xprs_r[3] is None
 
     @property
     def is_address_known(self) -> bool:
-        return "xaddr" not in self.error_value_names
+        return self.xdata.xprs_r[4] is not None
 
     @property
     def annotation(self) -> str:
         wbu = self.writeback_update()
         if self.is_ok:
             assignment = str(self.vrt) + " := " + str(self.xrmem)
-        elif self.is_memval_unknown and self.is_address_known:
+        elif self.is_xrmem_unknown and self.is_address_known:
             assignment = str(self.vrt) + " := *(" + str(self.xaddr) + ")"
         else:
             assignment = "Error value"
@@ -230,7 +214,7 @@ def ast_prov(
             hl_rhs = XU.xxpr_to_ast_def_expr(
                 rhs, xdata, iaddr, astree, memaddr=xaddr)
 
-        elif xd.is_memval_unknown and xd.is_address_known:
+        elif xd.is_xrmem_unknown and xd.is_address_known:
             xaddr = xd.xaddr
             hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
             hl_rhs = XU.xmemory_dereference_lval_expr(