Reachingdefs

chb/app/BDictionary.py

@@ -46,7 +46,7 @@
 import chb.util.IndexedTable as IT
 import chb.util.StringIndexedTable as SI
 
-from typing import Callable, List, Tuple, TYPE_CHECKING
+from typing import Callable, List, Optional, Tuple, TYPE_CHECKING
 
 if TYPE_CHECKING:
     from chb.app.AppAccess import AppAccess
@@ -125,6 +125,21 @@ def register(self, ix: int) -> Register:
         return bdregistry.mk_instance(
             self, self.register_table.retrieve(ix), Register)
 
+    def register_index_by_name(self, name: str) -> Optional[int]:
+        ixvalues = self.register_table.values()
+        for ixvalue in ixvalues:
+            if len(ixvalue.tags) >= 2:
+                if ixvalue.tags[1] == name:
+                    return ixvalue.index
+        return None
+
+    def register_by_name(self, name: str) -> Optional[Register]:
+        ix = self.register_index_by_name(name)
+        if ix is not None:
+            return self.register(ix)
+        else:
+            return None
+
     # ----------------------- xml accessors ------------------------------------
 
     def read_xml_string(self, n: ET.Element) -> str:

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250902"
+chbversion: str = "0.3.0-20251011"

chb/app/Function.py

@@ -525,14 +525,36 @@ def instruction(self, iaddr: str) -> Instruction:
         else:
             raise UF.CHBError("No instruction found at address " + iaddr)
 
-    def rdef_locations(self) -> Dict[str, List[List[str]]]:
+    def rdef_location_partition(self) -> Dict[str, List[List[str]]]:
+        """Return a map of registers to partitions of their reaching definitions."""
+
         result: Dict[str, List[List[str]]] = {}
 
         for (iaddr, instr) in self.instructions.items():
             irdefs = instr.rdef_locations()
-            for (reg, rdeflists) in irdefs.items():
+            for (reg, rdeflist) in irdefs.items():
                 result.setdefault(reg, [])
-                result[reg].extend(rdeflists)
+                for rrlist in result[reg]:
+                    if set(rrlist) == set(rdeflist):
+                        break
+                else:
+                    result[reg].append(rdeflist)
+        return result
+
+    def use_location_partition(self) -> Dict[str, List[List[str]]]:
+        """Return a map of registers to partitions of their use locations."""
+
+        result: Dict[str, List[List[str]]] = {}
+
+        for (iaddr, instr) in self.instructions.items():
+            iuses = instr.use_locations()
+            for (reg, uselist) in iuses.items():
+                result.setdefault(reg, [])
+                for rrlist in result[reg]:
+                    if set(rrlist) == set(uselist):
+                        break
+                else:
+                    result[reg].append(uselist)
         return result
 
     def lhs_types(self) -> Dict[str, Dict[str, "BCTyp"]]:
@@ -545,7 +567,6 @@ def lhs_types(self) -> Dict[str, Dict[str, "BCTyp"]]:
             result[iaddr] = {}
             for (vname, vtype) in ilhs_types.items():
                 result[iaddr][vname] = vtype
-
         return result
 
     def globalrefs(self) -> Dict[str, List["GlobalReference"]]:

chb/app/InstrXData.py

@@ -578,6 +578,12 @@ def get_base_update_xpr(self) -> XXpr:
                 "Unexpected error value in base-update expression")
         return self.xprdictionary.xpr(xbuval)
 
+    def is_base_update_xpr_ok(self) -> bool:
+        xbutag = next(t for t in self.tags if t.startswith("xbu:"))
+        xix = int(xbutag[4:])
+        xbuval = self.args[xix]
+        return (xbuval != -2)
+
     def get_base_update_cxpr(self) -> XXpr:
         cbutag = next(t for t in self.tags if t.startswith("cbu:"))
         cix = int(cbutag[4:])

chb/app/Instruction.py

@@ -340,11 +340,16 @@ def ast_switch_condition_prov(
             Optional[AST.ASTExpr], Optional[AST.ASTExpr]]:
         raise UF.CHBError("ast-switch-condition-prov not defined")
 
-    def rdef_locations(self) -> Dict[str, List[List[str]]]:
+    def rdef_locations(self) -> Dict[str, List[str]]:
         """Returns for each register, which locations must be combined."""
 
         return {}
 
+    def use_locations(self) -> Dict[str, List[str]]:
+        """Returns for each register defined, which locations use the definition."""
+
+        return {}
+
     def lhs_types(self) -> Dict[str, "BCTyp"]:
         """Returns a mapping from lhs assigned to its type."""
 

chb/arm/ARMAssembly.py

@@ -62,7 +62,7 @@ def opcode(self) -> ARMOpcode:
 
     @property
     def mnemonic(self) -> str:
-        return self.opcode.mnemonic
+        return self.opcode.mnemonic_stem
 
     def mnemonic_extension(self) -> str:
         return self.opcode.mnemonic_extension()

chb/arm/ARMInstruction.py

@@ -411,20 +411,25 @@ def lhs_variables(
     def rhs_expressions(self, filter: Callable[[XXpr], bool]) -> List[XXpr]:
         return [x for x in self.opcode.rhs(self.xdata) if filter(x)]
 
-    def rdef_locations(self) -> Dict[str, List[List[str]]]:
-        result: Dict[str, Dict[str, List[str]]] = {}
+    def rdef_locations(self) -> Dict[str, List[str]]:
+        result: Dict[str, List[str]] = {}
 
         for rdef in self.xdata.reachingdefs:
             if rdef is not None:
-                rdefvar = str(rdef.vardefuse.variable)
-                rdeflocs = [str(s) for s in rdef.valid_deflocations]
-                result.setdefault(rdefvar, {})
-                for sx in rdeflocs:
-                    result[rdefvar].setdefault(sx, [])
-                    for sy in rdeflocs:
-                        if sy not in result[rdefvar][sx]:
-                            result[rdefvar][sx].append(sy)
-        return {x:list(r.values()) for (x, r) in result.items()}
+                rdefvar = str(rdef.variable)
+                rdeflocs = sorted([str(s) for s in rdef.valid_deflocations])
+                result[rdefvar] = rdeflocs
+        return result
+
+    def use_locations(self) -> Dict[str, List[str]]:
+        result: Dict[str, List[str]] = {}
+
+        for use in self.xdata.defuses:
+            if use is not None:
+                usevar = str(use.variable)
+                uselocs = sorted([str(s) for s in use.uselocations])
+                result[usevar] = uselocs
+        return result
 
     def lhs_types(self) -> Dict[str, "BCTyp"]:
         result: Dict[str, "BCTyp"] = {}

chb/arm/ARMOpcode.py

@@ -229,6 +229,9 @@ def get_base_update_xpr(self) -> "XXpr":
             raise UF.CHBError(
                 self.__class__.__name__ + " does not have writeback")
 
+    def is_base_update_xpr_ok(self) -> bool:
+        return self.xdata.is_base_update_xpr_ok()
+
     def get_base_update_cxpr(self) -> "XXpr":
         if self.is_writeback:
             return self.xdata.get_base_update_cxpr()
@@ -239,7 +242,10 @@ def get_base_update_cxpr(self) -> "XXpr":
     def writeback_update(self) -> str:
         if self.xdata.has_base_update():
             vbu = self.get_base_update_var()
-            xbu = self.get_base_update_cxpr()
+            if self.is_base_update_xpr_ok():
+                xbu = str(self.get_base_update_cxpr())
+            else:
+                xbu = "?"
             return "; wbu: " + str(vbu) + " := " + str(xbu)
         else:
             return ""

chb/arm/opcodes/ARMBitwiseBitClear.py

@@ -156,6 +156,15 @@ def operands(self) -> List[ARMOperand]:
     def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args[1: -1]]
 
+    def mnemonic_extension(self) -> str:
+        cc = ARMOpcode.mnemonic_extension(self)
+        wb = "S" if self.is_writeback else ""
+        return wb + cc
+
+    @property
+    def is_writeback(self) -> bool:
+        return self.args[0] == 1
+
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMBitwiseBitClearXData(xdata)
         return xd.annotation

chb/arm/opcodes/ARMLoadCoprocessor.py

@@ -41,6 +41,8 @@
     from chb.arm.ARMDictionary import ARMDictionary
 
 
+@armregistry.register_tag("LDC2", ARMOpcode)
+@armregistry.register_tag("LDC2L", ARMOpcode)
 @armregistry.register_tag("LDCL", ARMOpcode)
 @armregistry.register_tag("LDC", ARMOpcode)
 class ARMLoadCoprocessor(ARMOpcode):

chb/arm/opcodes/ARMLoadRegisterByte.py

@@ -198,6 +198,10 @@ def operands(self) -> List[ARMOperand]:
     def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[i]) for i in [0, 1, 2, 3]]
 
+    @property
+    def is_write_back(self) -> bool:
+        return self.opargs[3].is_write_back
+
     def lhs(self, xdata: InstrXData) -> List[XVariable]:
         xd = ARMLoadRegisterByteXData(xdata)
         return [xd.vrt]
@@ -324,6 +328,11 @@ def has_cast() -> bool:
                 annotations=annotations)
             ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign]
 
+            if not xd.is_base_update_xpr_ok():
+                chklogger.logger.error(
+                    "LDRB: Error encountered for writeback address at address %s", iaddr)
+                return ([], ll_assigns)
+
             basereg = xd.get_base_update_var()
             newaddr = xd.get_base_update_xpr()
             hl_addr_lhs = XU.xvariable_to_ast_lval(basereg, xdata, iaddr, astree)

chb/arm/opcodes/ARMLoadRegisterHalfword.py

@@ -193,6 +193,10 @@ def operands(self) -> List[ARMOperand]:
     def opargs(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[i]) for i in [0, 1, 2, 3]]
 
+    @property
+    def is_write_back(self) -> bool:
+        return self.opargs[3].is_write_back
+
     def lhs(self, xdata: InstrXData) -> List[XVariable]:
         xd = ARMLoadRegisterHalfwordXData(xdata)
         return [xd.vrt]

chb/arm/opcodes/ARMLoadRegisterSignedByte.py

@@ -195,10 +195,6 @@ def ast_prov(
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
-        hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
-        hl_rhs = XU.xxpr_to_ast_def_expr(
-            rhs, xdata, iaddr, astree, size=1, memaddr=xaddr)
-
         hl_assign = astree.mk_assign(
             hl_lhs,
             hl_rhs,

chb/arm/opcodes/ARMMove.py

@@ -340,6 +340,7 @@ def ast_prov_predicate_assign(
             chklogger.logger.warning(
                 "Predicate assignment without associated predicate at "
                 + "address %s", iaddr)
+            astree.add_instr_address(ll_assign, [iaddr])
             return ([], [ll_assign])
 
         rhs = xd.cpredicate if xd.is_cpredicate_ok else xd.xpredicate

chb/arm/opcodes/ARMStoreCoprocessor.py

@@ -43,6 +43,8 @@
 
 @armregistry.register_tag("STCL", ARMOpcode)
 @armregistry.register_tag("STC", ARMOpcode)
+@armregistry.register_tag("STC2", ARMOpcode)
+@armregistry.register_tag("STC2L", ARMOpcode)
 class ARMStoreCoprocessor(ARMOpcode):
     """Stores memory data from a coprocessor to a sequence of addresses.
 

chb/arm/opcodes/ARMStoreRegisterByte.py

@@ -328,6 +328,12 @@ def ast_prov(
                 annotations=annotations)
             ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign]
 
+            if not xd.is_base_update_xpr_ok():
+                chklogger.logger.error(
+                    "STRB: Error encountered fro writeback address at address %s",
+                    iaddr)
+                return ([], ll_assigns)
+
             basereg = xd.get_base_update_var()
             newaddr = xd.get_base_update_xpr()
             hl_addr_lhs = XU.xvariable_to_ast_lval(basereg, xdata, iaddr, astree)

chb/arm/opcodes/ARMUnsignedMultiplyAccumulateLong.py

@@ -25,14 +25,19 @@
 # SOFTWARE.
 # ------------------------------------------------------------------------------
 
-from typing import List, TYPE_CHECKING
+from typing import List, Tuple, TYPE_CHECKING
 
 from chb.app.InstrXData import InstrXData
 
 from chb.arm.ARMDictionaryRecord import armregistry
 from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
 from chb.arm.ARMOperand import ARMOperand
 
+import chb.ast.ASTNode as AST
+from chb.astinterface.ASTInterface import ASTInterface
+
+import chb.invariants.XXprUtil as XU
+
 import chb.util.fileutil as UF
 from chb.util.IndexedTable import IndexedTableValue
 from chb.util.loggingutil import chklogger
@@ -110,6 +115,10 @@ def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
     def operands(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(self.args[i]) for i in [1, 2, 3, 4]]
 
+    @property
+    def opargs(self) -> List[ARMOperand]:
+        return [self.armd.arm_operand(self.args[i]) for i in [1, 2, 3, 4]]
+
     def mnemonic_extension(self) -> str:
         cc = ARMOpcode.mnemonic_extension(self)
         wb = "S" if self.is_writeback else ""
@@ -125,3 +134,82 @@ def annotation(self, xdata: InstrXData) -> str:
             return xd.annotation
         else:
             return "Error value"
+
+    def ast_prov(
+            self,
+            astree: ASTInterface,
+            iaddr: str,
+            bytestring: str,
+            xdata: InstrXData) -> Tuple[
+                List[AST.ASTInstruction], List[AST.ASTInstruction]]:
+
+        annotations: List[str] = [iaddr, "UMLAL"]
+
+        # low-level assignment
+
+        (ll_lhslo, _, _) = self.opargs[0].ast_lvalue(astree)
+        (ll_lhshi, _, _) = self.opargs[1].ast_lvalue(astree)
+        (ll_lo, _, _) = self.opargs[0].ast_rvalue(astree)
+        (ll_hi, _, _) = self.opargs[1].ast_rvalue(astree)
+        (ll_rn, _, _) = self.opargs[2].ast_rvalue(astree)
+        (ll_rm, _, _) = self.opargs[3].ast_rvalue(astree)
+
+        i32 = astree.mk_integer_constant(32)
+        ll_rhs1 = astree.mk_doubleword_sum(ll_hi, ll_lo)
+        ll_rhs2 = astree.mk_binary_op("mult", ll_rn, ll_rm)
+        ll_rhs = astree.mk_binary_op("plus", ll_rhs2, ll_rhs1)
+        ll_rhslo = astree.mk_binary_op("mod", ll_rhs, i32)
+        ll_rhshi = astree.mk_binary_op("div", ll_rhs, i32)
+
+        ll_assign_lo = astree.mk_assign(
+            ll_lhslo,
+            ll_rhslo,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        ll_assign_hi = astree.mk_assign(
+            ll_lhshi,
+            ll_rhshi,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        rdefs = xdata.reachingdefs
+
+        astree.add_expr_reachingdefs(ll_rn, [rdefs[0]])
+        astree.add_expr_reachingdefs(ll_rm, [rdefs[1]])
+        astree.add_expr_reachingdefs(ll_lo, [rdefs[2]])
+        astree.add_expr_reachingdefs(ll_hi, [rdefs[3]])
+
+        # high-level assignment
+
+        xd = ARMUnsignedMultiplyAccumulateLongXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Error value encountered for UMLAL at %s", iaddr)
+            return ([], [])
+
+        hl_lhs = XU.xvariable_to_ast_lval(xd.vlo, xdata, iaddr, astree)
+        hl_rhs = XU.xxpr_to_ast_def_expr(xd.rresult, xdata, iaddr, astree)
+
+        defuses = xdata.defuses
+        defuseshigh = xdata.defuseshigh
+
+        hl_assign = astree.mk_assign(
+            hl_lhs,
+            hl_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        astree.add_instr_mapping(hl_assign, ll_assign_lo)
+        astree.add_instr_mapping(hl_assign, ll_assign_hi)
+        astree.add_instr_address(hl_assign, [iaddr])
+        astree.add_expr_mapping(hl_rhs, ll_rhslo)
+        astree.add_lval_mapping(hl_lhs, ll_lhslo)
+        astree.add_expr_reachingdefs(hl_rhs, rdefs[4:])
+        astree.add_lval_defuses(hl_lhs, defuses[0])
+        astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
+
+        return ([hl_assign], [ll_assign_lo, ll_assign_hi])