ARM: convert astprov to handle result types

Author: sipma

chb/app/InstrXData.py

@@ -456,7 +456,19 @@ def get_branch_conditions(self) -> Sequence[XXpr]:
                 "XData does not have branch conditions: " + str(self))
 
     def has_instruction_condition(self) -> bool:
-        return "ic" in self.tags
+        return any(s.startswith("ic:") for s in self.tags)
+
+    def get_instruction_condition(self) -> XXpr:
+        for t in self.tags:
+            if t.startswith("ic:"):
+                index = int(t[3:])
+                argval = self.args[index]
+                if argval == -2:
+                    raise UF.CHBError(
+                        "Unexpected error value in instruction condition")
+                return self.xprdictionary.xpr(argval)
+        else:
+            raise UF.CHBError("No instruction condition index found")
 
     def has_condition_block_condition(self) -> bool:
         return "TF" in self.tags
@@ -465,7 +477,25 @@ def has_unknown_instruction_condition(self) -> bool:
         return "uc" in self.tags
 
     def has_base_update(self) -> bool:
-        return "bu" in self.tags
+        return any(s.startswith("vbu:") for s in self.tags)
+
+    def get_base_update_var(self) -> XVariable:
+        vbutag = next(t for t in self.tags if t.startswith("vbu:"))
+        vix = int(vbutag[4:])
+        vbuval = self.args[vix]
+        if vbuval == -2:
+            raise UF.CHBError(
+                "Unexpected error value in base-update variable")
+        return self.xprdictionary.variable(vbuval)
+
+    def get_base_update_xpr(self) -> XXpr:
+        xbutag = next(t for t in self.tags if t.startswith("xbu:"))
+        xix = int(xbutag[4:])
+        xbuval = self.args[xix]
+        if xbuval == -2:
+            raise UF.CHBError(
+                "Unexpected error value in base-update expression")
+        return self.xprdictionary.xpr(xbuval)
 
     @property
     def is_aggregate_jumptable(self) -> bool:

chb/arm/ARMCallOpcode.py

@@ -32,7 +32,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.arm.ARMOperandKind import ARMOperandKind, ARMAbsoluteOp
 
@@ -64,18 +64,27 @@
     from chb.invariants.XXpr import XXpr, XprConstant, XprVariable
 
 
-class ARMCallOpcodeXData:
+class ARMCallOpcodeXData(ARMOpcodeXData):
+    """
+    xdata format: a:x[2n]xr[n]dh, call   (n arguments)
+    -------------------------------------------------
+    xprs[0..2n-1]: (arg location expr, arg value expr) * n
+    xprs[2n]: call target expression
+    rdefs[0..n-1]: arg location reaching definitions
+    uses[0]: lhs
+    useshigh[0]: lhs
+    """
 
     def __init__(
             self,
             xdata: InstrXData,
             ixd: "InterfaceDictionary") -> None:
-        self._xdata = xdata
+        ARMOpcodeXData.__init__(self, xdata)
         self._ixd = ixd
 
     @property
-    def is_ok(self) -> bool:
-        return self._xdata.is_ok
+    def vrd(self) -> "XVariable":
+        return self.var(0, "vrd")
 
     @property
     def argument_count(self) -> int:
@@ -101,6 +110,12 @@ def arguments(self) -> List["XXpr"]:
             arguments.append(x)
         return arguments
 
+    @property
+    def argumentxvars(self) -> List["XXpr"]:
+        argcount = self.argument_count
+        return [x for x in self._xdata.xprs_r[argcount:2 * argcount]
+                if x is not None]
+
     @property
     def calltarget(self) -> "CallTarget":
         return self._xdata.call_target(self._ixd)
@@ -109,7 +124,8 @@ def calltarget(self) -> "CallTarget":
     def annotation(self) -> str:
         tgt = str(self.calltarget)
         args = ", ".join(str(x) for x in self.arguments)
-        return "call " + str(tgt) + "(" + args + ")"
+        call = "call " + str(tgt) + "(" + args + ")"
+        return self.add_instruction_condition(call)
 
 
 class ARMCallOpcode(ARMOpcode):
@@ -118,15 +134,7 @@ class ARMCallOpcode(ARMOpcode):
     tags[1]: <c>
     args[0]: index of target operand in armdictionary
 
-    xdata format: a:x[2n]xr[n]dh, call   (n arguments)
-    -------------------------------------------------
-    xprs[0..2n-1]: (arg location expr, arg value expr) * n
-    xprs[2n]: call target expression
-    rdefs[0..n-1]: arg location reaching definitions
-    uses[0]: lhs
-    useshigh[0]: lhs
-
-    or (if call target is not known):
+    (if call target is not known):
     xdata format: a:xxxxx
     ---------------------
     vars[0]: return value variable
@@ -135,10 +143,7 @@ class ARMCallOpcode(ARMOpcode):
     rdefs[0]: target reaching definition
     """
 
-    def __init__(
-            self,
-            d: "ARMDictionary",
-            ixval: IndexedTableValue) -> None:
+    def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
         ARMOpcode.__init__(self, d, ixval)
 
     @property
@@ -150,19 +155,10 @@ def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[0])]
 
     def lhs(self, xdata: InstrXData) -> List[XVariable]:
-        if len(xdata.vars) > 0:
-            return [xdata.vars[0]]
-        else:
-            return []
+        return [ARMCallOpcodeXData(xdata, self.ixd).vrd]
 
     def argument_count(self, xdata: InstrXData) -> int:
-        if self.is_call_instruction(xdata):
-            argcount = xdata.call_target_argument_count()
-            if argcount is not None:
-                return argcount
-        chklogger.logger.warning(
-            "Call instruction does not have argument count")
-        return 0
+        return ARMCallOpcodeXData(xdata, self.ixd).argument_count
 
     def has_string_arguments(self, xdata: InstrXData) -> bool:
         return any([x.is_string_reference for x in self.arguments(xdata)])
@@ -175,7 +171,7 @@ def annotated_call_arguments(
         return [x.to_annotated_value() for x in self.arguments(xdata)]
 
     def arguments(self, xdata: InstrXData) -> Sequence[XXpr]:
-        return xdata.xprs[:self.argument_count(xdata)]
+        return ARMCallOpcodeXData(xdata, self.ixd).arguments
 
     def is_call(self, xdata: InstrXData) -> bool:
         return len(xdata.tags) >= 2 and xdata.tags[1] == "call"
@@ -206,11 +202,13 @@ def ast_call_prov(
             chklogger.logger.info("Inlined call omitted at %s", iaddr)
             return ([], [])
 
+        xd = ARMCallOpcodeXData(xdata, self.ixd)
+
         annotations: List[str] = [iaddr, "BL"]
 
         # low-level call data
 
-        lhs = xdata.vars[0]
+        lhs = xd.vrd
         tgt = self.opargs[0]
 
         if not lhs.is_register_variable:
@@ -224,7 +222,7 @@ def ast_call_prov(
         ll_lhs = astree.mk_register_variable_lval(str(lhsreg))
         (ll_tgt, _, _) = tgt.ast_rvalue(astree)
 
-        xprs = xdata.xprs
+        xprs = xd.arguments
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
@@ -284,7 +282,7 @@ def ast_call_prov(
 
         # argument data
 
-        argcount = self.argument_count(xdata)
+        argcount = xd.argument_count
 
         ll_args: List[AST.ASTExpr] = []
         hl_args: List[AST.ASTExpr] = []
@@ -304,8 +302,8 @@ def ast_call_prov(
                 if len(astargtypes) < argcount:
                     astargtypes += ([None] * (argcount - len(astargtypes)))
 
-            xargs = xdata.xprs[:argcount]
-            xvarargs = xdata.xprs[argcount:(2 * argcount)]
+            xargs = xd.arguments
+            xvarargs = xd.argumentxvars
             if len(rdefs) >= argcount:
                 llrdefs = rdefs[:argcount]
                 # x represents the (invariant-enhanced) argument value.
@@ -316,7 +314,8 @@ def ast_call_prov(
                 #  in bytes (note: not the stackpointer at function entry).
                 # rdef represents the reaching definition for the argument
                 #  location.
-                for (x, xv, rdef, argtype) in zip(xargs, xvarargs, llrdefs, astargtypes):
+                for (x, xv, rdef, argtype) in zip(
+                        xargs, xvarargs, llrdefs, astargtypes):
 
                     # low-level argument
 

chb/arm/ARMInstruction.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
@@ -249,11 +249,7 @@ def has_condition_block_condition(self) -> bool:
         return self.xdata.has_condition_block_condition()
 
     def get_instruction_condition(self) -> XXpr:
-        if self.has_instruction_condition():
-            return self.xdata.xprs[2]
-        else:
-            raise UF.CHBError(
-                "Instruction does not have an instruction condition")
+        return self.xdata.get_instruction_condition()
 
     @property
     def memory_accesses(self) -> Sequence[MemoryAccess]:
@@ -392,7 +388,7 @@ def rdef_locations(self) -> Dict[str, List[List[str]]]:
     def lhs_types(self) -> Dict[str, "BCTyp"]:
         result: Dict[str, "BCTyp"] = {}
 
-        vars = self.xdata.vars
+        vars = self.xdata.vars_r
         types = self.xdata.types
         if len(vars) == len(types):
             for (v, ty) in zip(vars, types):

chb/arm/ARMOpcode.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
@@ -26,6 +26,8 @@
 # ------------------------------------------------------------------------------
 """ARM opcodes."""
 
+import inspect
+
 from typing import List, Optional, Sequence, Tuple, TYPE_CHECKING
 
 from chb.api.CallTarget import CallTarget
@@ -55,6 +57,8 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.XVariable import XVariable
+    from chb.invariants.XXpr import XXpr
     from chb.simulation.SimulationState import SimulationState
 
 
@@ -101,6 +105,68 @@ def get_extension(e: str) -> str:
         return e
 
 
+class ARMOpcodeXData:
+
+    def __init__(self, xdata: InstrXData) -> None:
+        self._xdata = xdata
+
+    @property
+    def xdata(self) -> InstrXData:
+        return self._xdata
+
+    @property
+    def is_ok(self) -> bool:
+        return self.xdata.is_ok
+
+    def var(self, index: int, name: str) -> "XVariable":
+        v = self.xdata.vars_r[index]
+        if v is None:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " has an error value")
+        return v
+
+    def xpr(self, index: int, name: str) -> "XXpr":
+        x = self.xdata.xprs_r[index]
+        if x is None:
+            raise UF.CHBError(
+                self.__class__.__name__ + ":" + name + " has an error value")
+        return x
+
+    def add_instruction_condition(self, s: str) -> str:
+        if self.xdata.has_unknown_instruction_condition():
+            return "if ? then " + s
+        elif self.xdata.has_instruction_condition():
+            c = str(self.xdata.get_instruction_condition())
+            return "if " + c + " then " + s
+        else:
+            return s
+
+    def is_writeback(self) -> bool:
+        return self.xdata.has_base_update()
+
+    def get_base_update_var(self) -> "XVariable":
+        if self.is_writeback:
+            return self.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()
+        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()
+            return "; " + str(vbu) + " := " + str(xbu)
+        else:
+            return ""
+
+
 class ARMOpcode(ARMDictionaryRecord):
 
     def __init__(