Astprovsupport

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250313"
+chbversion: str = "0.3.0-20250314"

chb/arm/opcodes/ARMMultiplyAccumulate.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2021 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
@@ -79,11 +79,11 @@ def xrprd(self) -> "XXpr":
 
     @property
     def result(self) -> "XXpr":
-        return self.xpr(4, "result")
+        return self.xpr(5, "result")
 
     @property
     def rresult(self) -> "XXpr":
-        return self.xpr(5, "rresult")
+        return self.xpr(6, "rresult")
 
     @property
     def result_simplified_p(self) -> str:
@@ -123,9 +123,83 @@ def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
     def operands(self) -> List[ARMOperand]:
         return [self.armd.arm_operand(i) for i in self.args[1:]]
 
+    @property
+    def opargs(self) -> List[ARMOperand]:
+        return [self.armd.arm_operand(i) for i in self.args[1:]]
+
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMMultiplyAccumulateXData(xdata)
         if xd.is_ok:
             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, "MLA"]
+
+        # low-level assignment
+
+        (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree)
+        (ll_rn, _, _) = self.opargs[1].ast_rvalue(astree)
+        (ll_rm, _, _) = self.opargs[2].ast_rvalue(astree)
+        (ll_ra, _, _) = self.opargs[3].ast_rvalue(astree)
+        ll_rhs1 = astree.mk_binary_op("mult", ll_rn, ll_rm)
+        ll_rhs = astree.mk_binary_op("plus",ll_rhs1, ll_ra)
+
+        ll_assign = astree.mk_assign(
+            ll_lhs,
+            ll_rhs,
+            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_ra, [rdefs[2]])
+
+        # high-level assignment
+
+        xd = ARMMultiplyAccumulateXData(xdata)
+        if not xd.is_ok:
+            chklogger.logger.error(
+                "Error value encountered for MLA at %s", iaddr)
+            return ([], [])
+
+        lhs = xd.vrd
+        rhs1 = xd.xrn
+        rhs2 = xd.xrm
+        rhs3 = xd.xra
+        rhs4 = xd.rresult
+
+        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(rhs4, xdata, iaddr, astree)
+
+        hl_assign = astree.mk_assign(
+            hl_lhs,
+            hl_rhs,
+            iaddr=iaddr,
+            bytestring=bytestring,
+            annotations=annotations)
+
+        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(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])
+
+        return ([hl_assign], [ll_assign])

chb/arm/opcodes/ARMStoreRegisterDual.py

@@ -48,6 +48,7 @@
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
     from chb.invariants.VarInvariantFact import ReachingDefFact
+    from chb.invariants.VAssemblyVariable import VMemoryVariable
     from chb.invariants.XVariable import XVariable
     from chb.invariants.XXpr import XXpr
 
@@ -62,12 +63,12 @@ def vmem1(self) -> "XVariable":
         return self.var(0, "vmem1")
 
     @property
-    def vmem2(self) -> "XVariable":
-        return self.var(1, "vmem2")
+    def is_vmem_known(self) -> bool:
+        return self.xdata.vars_r[0] is not None
 
     @property
-    def vrn(self) -> "XVariable":
-        return self.var(2, "vrn")
+    def vmem2(self) -> "XVariable":
+        return self.var(1, "vmem2")
 
     @property
     def xrn(self) -> "XXpr":
@@ -101,17 +102,30 @@ def xaddr1(self) -> "XXpr":
     def xaddr2(self) -> "XXpr":
         return self.xpr(7, "xaddr2")
 
+    @property
+    def is_xaddr_known(self) -> bool:
+        return self.xdata.xprs_r[6] is not None
+
     @property
     def xaddr_updated(self) -> "XXpr":
         return self.xpr(8, "xaddr_updated")
 
     @property
     def annotation(self) -> str:
-        assignment = (
-            str(self.vmem1) + " := " + str(self.xxrt) + "; "
-                + str(self.vmem2) + " := " + str(self.xxrt2))
         wbu = self.writeback_update()
-        return self.add_instruction_condition(assignment + wbu)
+        rhs1 = self.xxrt
+        rhs2 = self.xxrt2
+        if self.is_ok or self.is_vmem_known:
+            assign1 = str(self.vmem1) + " := " + str(rhs1)
+            assign2 = str(self.vmem2) + " := " + str(rhs2)
+            assigns = assign1 + "; " + assign2
+        elif self.is_xaddr_known:
+            assign1 = "*(" + str(self.xaddr1) + ") := " + str(rhs1)
+            assign2 = "*(" + str(self.xaddr2) + ") := " + str(rhs2)
+            assigns = assign1 + "; " + assign2
+        else:
+            assigns = "Error in vmem and xaddr"
+        return self.add_instruction_condition(assigns + wbu)
 
 
 @armregistry.register_tag("STRD", ARMOpcode)
@@ -194,10 +208,7 @@ def register_spills(self, xdata: InstrXData) -> List[str]:
 
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMStoreRegisterDualXData(xdata)
-        if xd.is_ok:
-            return xd.annotation
-        else:
-            return "Error value"
+        return xd.annotation
 
     def assembly_ast(
             self,
@@ -250,27 +261,39 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
-        if not xd.is_ok:
+        # high-level assignments
+
+        if xd.is_ok or xd.is_vmem_known:
+            lhs1 = xd.vmem1
+            lhs2 = xd.vmem2
+            memaddr1 = xd.xaddr1
+            memaddr2 = xd.xaddr2
+            hl_lhs1 = XU.xvariable_to_ast_lval(lhs1, xdata, iaddr, astree)
+            hl_lhs2 = XU.xvariable_to_ast_lval(lhs2, xdata, iaddr, astree)
+
+        elif xd.is_xaddr_known:
+            memaddr1 = xd.xaddr1
+            memaddr2 = xd.xaddr2
+            hl_lhs1 = XU.xmemory_dereference_lval(memaddr1, xdata, iaddr, astree)
+            hl_lhs2 = XU.xmemory_dereference_lval(memaddr2, xdata, iaddr, astree)
+
+        else:
             chklogger.logger.error(
-                "Error value encountered at address %s", iaddr)
+                "STRD: LHS lval and address both have error values: skipping "
+                + "store-dual instruction at address %s",
+                iaddr)
             return ([], [])
 
-        # high-level assignments
         rdefs = xdata.reachingdefs
         deful = xdata.defuses
         defuh = xdata.defuseshigh
 
-        lhs1 = xd.vmem1
-        lhs2 = xd.vmem2
         rhs1 = xd.xxrt
         rhs2 = xd.xxrt2
 
         hl_rhs1 = XU.xxpr_to_ast_def_expr(rhs1, xdata, iaddr, astree)
         hl_rhs2 = XU.xxpr_to_ast_def_expr(rhs2, xdata, iaddr, astree)
 
-        hl_lhs1 = XU.xvariable_to_ast_lval(lhs1, xdata, iaddr, astree)
-        hl_lhs2 = XU.xvariable_to_ast_lval(lhs2, xdata, iaddr, astree)
-
         hl_assign1 = astree.mk_assign(
             hl_lhs1,
             hl_rhs1,
@@ -284,6 +307,15 @@ def ast_prov(
             bytestring=bytestring,
             annotations=annotations)
 
+        if (
+                (not xd.is_vmem_known)
+                or (lhs1.is_memory_variable
+                    and cast("VMemoryVariable", lhs1.denotation).base.is_basevar)
+                or hl_lhs1.offset.is_index_offset
+                or hl_lhs1.offset.is_field_offset):
+            astree.add_expose_instruction(hl_assign1.instrid)
+            astree.add_expose_instruction(hl_assign2.instrid)
+
         # TODO: add writeback update
 
         astree.add_instr_mapping(hl_assign1, ll_assign1)