ARM: convert astprov to handle result types

Author: sipma

chb/arm/ARMInstruction.py

@@ -418,7 +418,6 @@ def to_string(
             pesp = str(self.stackpointer_offset) + "  " if sp else ""
             popcode = (
                 self.opcodetext.ljust(opcodewidth) if opcodetxt else "")
-            print("DEBUG: " + pesp + pbytes + popcode + self.annotation)
             return pesp + pbytes + popcode + self.annotation
         except Exception as e:
             print(

chb/arm/opcodes/ARMAdd.py

@@ -207,7 +207,6 @@ def ast_prov(
             xdata: InstrXData) -> Tuple[
                 List[AST.ASTInstruction], List[AST.ASTInstruction]]:
 
-        xd = ARMAddXData(xdata)
         annotations: List[str] = [iaddr, "ADD"]
 
         # low-level assignment
@@ -231,6 +230,7 @@ def ast_prov(
 
         # high-level assignment
 
+        xd = ARMAddXData(xdata)
         if not xdata.is_ok:
             chklogger.logger.error("Error value encountered at %s", iaddr)
             return ([], [])

chb/arm/opcodes/ARMAddCarry.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
@@ -40,11 +40,49 @@
 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 ARMAddCarryXData(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("ADC", ARMOpcode)
@@ -73,10 +111,7 @@ class ARMAddCarry(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, "AddCarry")
 
@@ -99,18 +134,11 @@ def mnemonic_extension(self) -> str:
         return wb + 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 = ARMAddCarryXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -131,6 +159,8 @@ def ast_prov(
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
+        # low-level assignment
+
         (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree)
         (ll_op1, _, _) = self.operands[1].ast_rvalue(astree)
         (ll_op2, _, _) = self.operands[2].ast_rvalue(astree)
@@ -143,27 +173,29 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        lhsasts = XU.xvariable_to_ast_lvals(lhs, xdata, astree)
-        if len(lhsasts) == 0:
-            raise UF.CHBError("Adc: no lval found")
+        rdefs = xdata.reachingdefs
+
+        astree.add_expr_reachingdefs(ll_op1, [rdefs[0]])
+        astree.add_expr_reachingdefs(ll_op2, [rdefs[1]])
 
-        if len(lhsasts) > 1:
-            raise UF.CHBError(
-                "Adc: multiple lvals in ast: "
-                + ", ".join(str(v) for v in lhsasts))
+        # high-level assignment
 
-        hl_lhs = lhsasts[0]
+        xd = ARMAddCarryXData(xdata)
+        if not xdata.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
 
-        rhsasts = XU.xxpr_to_ast_def_exprs(rhs3, xdata, iaddr, astree)
-        if len(rhsasts) == 0:
-            raise UF.CHBError("Adc: no rhs value found")
+        lhs = xd.vrd
+        rhs1 = xd.xrn
+        rhs2 = xd.xrm
+        rhs3 = xd.rresult
 
-        if len(rhsasts) > 1:
-            raise UF.CHBError(
-                "Multiple rhs values found for Adc: "
-                + ", ".join(str(v) for v in rhsasts))
+        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(rhs3, xdata, iaddr, astree)
 
         hl_assign = astree.mk_assign(
             hl_lhs,
@@ -172,14 +204,12 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        astree.add_reg_definition(iaddr, hl_lhs, hl_rhs)
         astree.add_instr_mapping(hl_assign, ll_assign)
         astree.add_instr_address(hl_assign, [iaddr])
         astree.add_expr_mapping(hl_rhs, ll_rhs)
         astree.add_lval_mapping(hl_lhs, ll_lhs)
-        astree.add_expr_reachingdefs(ll_rhs, [rdefs[0], rdefs[1]])
-        astree.add_expr_reachingdefs(ll_op1, [rdefs[0]])
-        astree.add_expr_reachingdefs(ll_op2, [rdefs[1]])
+        astree.add_expr_reachingdefs(hl_rhs, rdefs[2:])
+        astree.add_expr_reachingdefs(ll_rhs, rdefs[:2])
         astree.add_lval_defuses(hl_lhs, defuses[0])
         astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
 

chb/arm/opcodes/ARMAdr.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,32 @@
 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 ARMAdrXData(ARMOpcodeXData):
+
+    def __init__(self, xdata: InstrXData) -> None:
+        ARMOpcodeXData.__init__(self, xdata)
+
+    @property
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
+
+    @property
+    def ximm(self) -> "XXpr":
+        return self.xpr(0, "ximm")
+
+    @property
+    def annotation(self) -> str:
+        assignment = str(self.vrd) + " := " + str(self.ximm)
+        return self.add_instruction_condition(assignment)
 
 
 @armregistry.register_tag("ADR", ARMOpcode)
@@ -65,10 +86,7 @@ class ARMAdr(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, 2, "Adr")
 
@@ -81,16 +99,11 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args]
 
     def annotation(self, xdata: InstrXData) -> str:
-        lhs = str(xdata.vars[0])
-        result = str(xdata.xprs[0])
-        assignment = lhs + " := " + result
-        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 = ARMAdrXData(xdata)
+        if xd.is_ok:
+            return xd.annotation
         else:
-            return assignment
+            return "Error value"
 
     def ast_prov(
             self,
@@ -116,8 +129,14 @@ def ast_prov(
 
         # high-level assignment
 
-        lhs = xdata.vars[0]
-        rhs = xdata.xprs[0]
+        xd = ARMAdrXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Encountered error value at address %s", iaddr)
+            return ([], [])
+
+        lhs = xd.vrd
+        rhs = xd.ximm
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh