Liftingsupport

chb/app/CHVersion.py

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

chb/arm/opcodes/ARMStoreMultipleIncrementAfter.py

@@ -45,7 +45,8 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
-    from chb.invariants.VAssemblyVariable import VRegisterVariable
+    from chb.invariants.VAssemblyVariable import (
+        VRegisterVariable, VMemoryVariable)
     from chb.invariants.XVariable import XVariable
     from chb.invariants.XXpr import XXpr, XprConstant, XprVariable
 
@@ -417,28 +418,23 @@ def ast_prov(
         if xdata.instruction_subsumes():
             return self.ast_prov_ldmstmcopy(astree, iaddr, bytestring, xdata)
 
-        else:
+        xd = ARMStoreMultipleIncrementAfterXData(xdata)
+        if not xd.is_ok:
             chklogger.logger.error(
-                "AST conversion of STM not yet supported at address %s",
-                iaddr)
+                "STM: Error value encountered at address %s", iaddr)
             return ([], [])
 
-        regcount = len(xdata.reachingdefs) - 1
+        annotations: List[str] = [iaddr, "STM"]
+
+        '''
         baselhs = xdata.vars[0]
-        memlhss = xdata.vars[1:]
         baserhs = xdata.xprs[0]
         baseresult = xdata.xprs[1]
         baseresultr = xdata.xprs[2]
-        regrhss = xdata.xprs[3:3 + regcount]
-        #rregrhss = xdata.xprs[3 + regcount:3 + (2 * regcount)]
         baserdef = xdata.reachingdefs[0]
-        regrdefs = xdata.reachingdefs[1:]
         baseuses = xdata.defuses[0]
-        memuses = xdata.defuses[1:]
         baseuseshigh = xdata.defuseshigh[0]
-        memuseshigh = xdata.defuseshigh[1:]
-
-        annotations: List[str] = [iaddr, "STMIA"]
+        '''
 
         # low-level assignments
 
@@ -448,6 +444,12 @@ def ast_prov(
         (baselval, _, _) = self.opargs[0].ast_lvalue(astree)
         (baserval, _, _) = self.opargs[0].ast_rvalue(astree)
 
+        memlhss = xd.memlhss
+        regrhss = xd.rhss
+        regrdefs = xdata.reachingdefs[1:]
+        memuses = xdata.defuses[1:]
+        memuseshigh = xdata.defuseshigh[1:]
+
         regsop = self.opargs[1]
         registers = regsop.registers
         base_offset = 0
@@ -469,10 +471,11 @@ def ast_prov(
 
             # high-level assignments
 
-            lhs = memlhss[i]
-            rhs = regrhss[i]
-            hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
-            hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+            memlhs = memlhss[i]
+            regrhs = regrhss[i]
+
+            hl_lhs = XU.xvariable_to_ast_lval(memlhs, xdata, iaddr, astree)
+            hl_rhs = XU.xxpr_to_ast_def_expr(regrhs, xdata, iaddr, astree)
             hl_assign = astree.mk_assign(
                 hl_lhs,
                 hl_rhs,
@@ -491,6 +494,13 @@ def ast_prov(
 
             base_offset += 4
 
+            if (
+                    (memlhs.is_memory_variable
+                     and cast("VMemoryVariable",
+                              memlhs.denotation).base.is_basevar)):
+                astree.add_expose_instruction(hl_assign.instrid)
+
+        '''
         if self.writeback:
 
             # low-level base assignment
@@ -528,5 +538,6 @@ def ast_prov(
             astree.add_expr_reachingdefs(ll_base_rhs, [baserdef])
             astree.add_lval_defuses(hl_base_lhs, baseuses)
             astree.add_lval_defuses_high(hl_base_lhs, baseuseshigh)
+        '''
 
         return (hl_instrs, ll_instrs)

chb/invariants/VMemoryOffset.py

@@ -146,6 +146,10 @@ def __init__(
     def is_no_offset(self) -> bool:
         return True
 
+    @property
+    def is_constant_value_offset(self) -> bool:
+        return True
+
     def offsetvalue(self) -> int:
         return 0