Liftingsupport

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250404"
+chbversion: str = "0.3.0-20250417"

chb/arm/opcodes/ARMAddCarry.py

@@ -25,7 +25,7 @@
 # SOFTWARE.
 # ------------------------------------------------------------------------------
 
-from typing import List, Tuple, TYPE_CHECKING
+from typing import List, Optional, Tuple, TYPE_CHECKING
 
 from chb.app.InstrXData import InstrXData
 
@@ -45,11 +45,43 @@
 
 if TYPE_CHECKING:
     from chb.arm.ARMDictionary import ARMDictionary
+    from chb.invariants.VarInvariantFact import ReachingDefFact
     from chb.invariants.XVariable import XVariable
     from chb.invariants.XXpr import XXpr
 
 
 class ARMAddCarryXData(ARMOpcodeXData):
+    """Adc <rd> <rn> <rm>  ==> result
+
+    Data format (regular)
+    - variables:
+    0: vrd
+
+    - expressions:
+    0: xrn
+    1: xrm
+    2: result
+    3: rresult (result, rewritten)
+    4: xxrn (xrn, rewritten)
+    5: xxrm (xrm, rewritten)
+
+    - c expressions:
+    0: cresult
+
+    rdefs[0]: xrn
+    rdefs[1]: xrm
+    rdefs[2:..]: reaching definitions for simplified result expression
+    uses[0]: vrd
+    useshigh[0]: vrd
+
+    Data format (as part of jump table)
+    - expressions:
+    0: xrn
+    1: xxrn (xrn, rewritten)
+
+    rdefs[0]: xrn
+    rdefs[1:]: reaching definitions for xxrn
+    """
 
     def __init__(self, xdata: InstrXData) -> None:
         ARMOpcodeXData.__init__(self, xdata)
@@ -70,14 +102,57 @@ def xrm(self) -> "XXpr":
     def result(self) -> "XXpr":
         return self.xpr(2, "result")
 
+    @property
+    def is_result_ok(self) -> bool:
+        return self.is_xpr_ok(2)
+
     @property
     def rresult(self) -> "XXpr":
         return self.xpr(3, "rresult")
 
+    @property
+    def is_rresult_ok(self) -> bool:
+        return self.is_xpr_ok(3)
+
+    @property
+    def cresult(self) -> "XXpr":
+        return self.cxpr(0, "cresult")
+
+    @property
+    def is_cresult_ok(self) -> bool:
+        return self.is_cxpr_ok(0)
+
     @property
     def result_simplified(self) -> str:
-        return simplify_result(
-            self.xdata.args[3], self.xdata.args[4], self.result, self.rresult)
+        if self.is_result_ok and self.is_rresult_ok:
+            return simplify_result(
+                self.xdata.args[3], self.xdata.args[4], self.result, self.rresult)
+        else:
+            return str(self.xrn) + " + " + str(self.xrm)
+
+    @property
+    def xxrn(self) -> "XXpr":
+        return self.xpr(4, "xxrn")
+
+    @property
+    def is_xxrn_ok(self) -> bool:
+        return self.is_xpr_ok(4)
+
+    @property
+    def xxrm(self) -> "XXpr":
+        return self.xpr(5, "xxrm")
+
+    @property
+    def is_xxrm_ok(self) -> bool:
+        return self.is_xpr_ok(5)
+
+    @property
+    def rn_rdef(self) -> Optional["ReachingDefFact"]:
+        return self._xdata.reachingdefs[0]
+
+    @property
+    def rm_rdef(self) -> Optional["ReachingDefFact"]:
+        return self._xdata.reachingdefs[1]
 
     @property
     def annotation(self) -> str:
@@ -135,10 +210,7 @@ def mnemonic_extension(self) -> str:
 
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMAddCarryXData(xdata)
-        if xd.is_ok:
-            return xd.annotation
-        else:
-            return "Error value"
+        return xd.annotation
 
     def ast_prov(
             self,
@@ -150,15 +222,6 @@ def ast_prov(
 
         annotations: List[str] = [iaddr, "ADC"]
 
-        lhs = xdata.vars[0]
-        rhs1 = xdata.xprs[0]
-        rhs2 = xdata.xprs[1]
-        rhssum = xdata.xprs[2]
-        rhs3 = xdata.xprs[3]
-        rdefs = xdata.reachingdefs
-        defuses = xdata.defuses
-        defuseshigh = xdata.defuseshigh
-
         # low-level assignment
 
         (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree)
@@ -180,22 +243,41 @@ def ast_prov(
 
         # high-level assignment
 
+        def has_cast() -> bool:
+            return (
+                astree.has_register_variable_intro(iaddr)
+                and astree.get_register_variable_intro(iaddr).has_cast())
+
         xd = ARMAddCarryXData(xdata)
-        if not xdata.is_ok:
+
+        if xd.is_cresult_ok and xd.is_rresult_ok:
+            rhs = xd.cresult
+            xrhs = xd.rresult
+
+        elif xd.is_rresult_ok:
+            rhs = xd.rresult
+            xrhs = xd.rresult
+
+        elif xd.is_result_ok:
+            rhs = xd.result
+            xrhs = xd.result
+
+        else:
             chklogger.logger.error(
-                "Encountered error value at address %s", iaddr)
-            return ([], [])
+                "ADC: Encountered error value for rhs at address %s", iaddr)
+            return ([], [ll_assign])
 
         lhs = xd.vrd
         rhs1 = xd.xrn
         rhs2 = xd.xrm
-        rhs3 = xd.rresult
+        rrhs1 = xd.xxrn if xd.is_xxrn_ok else xd.xrn
+        rrhs2 = xd.xxrm if xd.is_xxrm_ok else xd.xrm
 
         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(rhs3, xdata, iaddr, astree)
+        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
 
         hl_assign = astree.mk_assign(
             hl_lhs,
@@ -213,4 +295,9 @@ def ast_prov(
         astree.add_lval_defuses(hl_lhs, defuses[0])
         astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
 
+        if astree.has_register_variable_intro(iaddr):
+            rvintro = astree.get_register_variable_intro(iaddr)
+            if rvintro.has_cast():
+                astree.add_expose_instruction(hl_assign.instrid)
+
         return ([hl_assign], [ll_assign])

chb/arm/opcodes/ARMLogicalShiftLeft.py

@@ -151,6 +151,9 @@ def mnemonic(self) -> str:
     def is_writeback(self) -> bool:
         return self.args[0] == 1
 
+    def lsl_xdata(self, xdata: InstrXData) -> ARMLogicalShiftLeftXData:
+        return ARMLogicalShiftLeftXData(xdata)
+
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMLogicalShiftLeftXData(xdata)
         if xd.is_ok:

chb/arm/opcodes/ARMReverseSubtract.py

@@ -111,6 +111,22 @@ def result_simplified(self) -> str:
         else:
             return str(self.xrm) + " - " + str(self.xrn)
 
+    @property
+    def xxrn(self) -> "XXpr":
+        return self.xpr(4, "xxrn")
+
+    @property
+    def is_xxrn_ok(self) -> bool:
+        return self.is_xpr_ok(4)
+
+    @property
+    def xxrm(self) -> "XXpr":
+        return self.xpr(5, "xxrm")
+
+    @property
+    def is_xxrm_ok(self) -> bool:
+        return self.is_xpr_ok(5)
+
     @property
     def annotation(self) -> str:
         cresult = (
@@ -174,6 +190,9 @@ def mnemonic(self) -> str:
     def is_writeback(self) -> bool:
         return self.args[0] == 1
 
+    def rsb_xdata(self, xdata: InstrXData) -> ARMReverseSubtractXData:
+        return ARMReverseSubtractXData(xdata)
+
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMReverseSubtractXData(xdata)
         return xd.annotation

chb/ast/AbstractSyntaxTree.py

@@ -185,6 +185,13 @@ def storageconstructor(self) -> ASTStorageConstructor:
     def set_function_prototype(self, p: AST.ASTVarInfo) -> None:
         self.symboltable.set_function_prototype(p)
 
+    def has_function_prototype(self) -> bool:
+        return self.symboltable.has_function_prototype()
+
+    @property
+    def function_prototype(self) -> Optional[AST.ASTVarInfo]:
+        return self.symboltable.function_prototype
+
     def has_symbol(self, name: str) -> bool:
         return self.symboltable.has_symbol(name)
 

chb/astinterface/ASTInterface.py

@@ -215,6 +215,13 @@ def parameter_abi(self) -> str:
     def srcformals(self) -> List[ASTIFormalVarInfo]:
         return self._srcformals
 
+    def has_function_prototype(self) -> bool:
+        return self.astree.has_function_prototype()
+
+    @property
+    def function_prototype(self) -> Optional[AST.ASTVarInfo]:
+        return self.astree.function_prototype
+
     @property
     def annotations(self) -> Dict[int, List[str]]:
         return self._annotations

chb/astinterface/ASTInterfaceBasicBlock.py

@@ -42,6 +42,8 @@
     from chb.arm.ARMCfgBlock import ARMCfgBlock
     from chb.app.BasicBlock import BasicBlock
     from chb.arm.ARMInstruction import ARMInstruction
+    from chb.arm.opcodes.ARMLogicalShiftLeft import ARMLogicalShiftLeft
+    from chb.arm.opcodes.ARMReverseSubtract import ARMReverseSubtract
     from chb.astinterface.ASTInterface import ASTInterface
 
 
@@ -219,6 +221,18 @@ def trampoline_payload_ast(self, astree: "ASTInterface") -> AST.ASTStmt:
         STRxx R1, <mem>
         MOVxx R1, #1
         MOV   R0
+
+        case 4: fallthrough / exit function (return) on !R0
+        LDR  RO, ...
+        RSBS R1, R0, #0
+        ADC  R0, R0, R1
+        BX   LR
+
+        case 5: fallthrough / goto_xxx
+        MOVxx R1, #1
+        LSL   R0, R1, #2
+        BX    LR
+
         """
         if not self.trampoline:
             raise UF.CHBError("Internal error")
@@ -242,7 +256,7 @@ def trampoline_payload_ast(self, astree: "ASTInterface") -> AST.ASTStmt:
                 brstmt = astree.mk_branch(cc, rstmt, estmt, "0x0")
                 return brstmt
 
-            elif payloadlen == 7:
+            elif payloadlen == 7 or payloadlen == 8:
                 (iaddr3, chkinstr3) = payloadinstrs[-3]
                 (iaddr4, chkinstr4) = payloadinstrs[-4]
                 chkinstr3 = cast("ARMInstruction", chkinstr3)
@@ -273,12 +287,23 @@ def trampoline_payload_ast(self, astree: "ASTInterface") -> AST.ASTStmt:
             if chkinstr3.mnemonic_stem == "MOV":
                 if chkinstr3.has_instruction_condition():
                     condition = chkinstr3.get_instruction_condition()
-                    cstmt = astree.mk_continue_stmt()
-                    estmt = astree.mk_instr_sequence([])
-                    cc = XU.xxpr_to_ast_def_expr(
-                        condition, chkinstr3.xdata, chkinstr3.iaddr, astree)
-                    brstmt = astree.mk_branch(cc, cstmt, estmt, "0x0")
-                    return brstmt
+                    chkopc2 = chkinstr2.opcode
+                    chkopc2 = cast("ARMLogicalShiftLeft", chkopc2)
+                    lslxdata = chkopc2.lsl_xdata(chkinstr2.xdata)
+                    shift = lslxdata.xrm
+                    if str(shift) == "0x1":
+                        cstmt = astree.mk_continue_stmt()
+                        estmt = astree.mk_instr_sequence([])
+                        cc = XU.xxpr_to_ast_def_expr(
+                            condition, chkinstr3.xdata, chkinstr3.iaddr, astree)
+                        brstmt = astree.mk_branch(cc, cstmt, estmt, "0x0")
+                        return brstmt
+                    else:
+                        chklogger.logger.critical(
+                            "trampoline payload cannot be lifted: "
+                            "LSL case %s not yet supported. Contact "
+                            "system maintainer for support",
+                            str(shift))
                 else:
                     chklogger.logger.critical(
                         "trampoline payload cannot be lifted: "
@@ -290,6 +315,32 @@ def trampoline_payload_ast(self, astree: "ASTInterface") -> AST.ASTStmt:
                     + "expected a MOV instruction and not a %s. "
                     + "Contact system maintainer for support.",
                     chkinstr3.mnemonic)
+
+        # case 4
+        elif payloadlen == 4 and chkinstr2.mnemonic_stem == "ADC":
+            (iaddr3, chkinstr3) = payloadinstrs[-3]
+            chkinstr3 = cast("ARMInstruction", chkinstr3)
+            if chkinstr3.mnemonic_stem == "RSB":
+                chkopc3 = chkinstr3.opcode
+                chkopc3 = cast("ARMReverseSubtract", chkopc3)
+                rsbxdata = chkopc3.rsb_xdata(chkinstr3.xdata)
+                cvalue = rsbxdata.xrn
+                if rsbxdata.is_xxrn_ok:
+                    cvalue = rsbxdata.xxrn
+                ccval = XU.xxpr_to_ast_def_expr(
+                    cvalue, chkinstr3.xdata, chkinstr3.iaddr, astree)
+                cc = astree.mk_unary_op("lnot", ccval)
+                rstmt = astree.mk_return_stmt(None)
+                estmt = astree.mk_instr_sequence([])
+                brstmt = astree.mk_branch(cc, rstmt, estmt, "0x0")
+                return brstmt
+            else:
+                chklogger.logger.critical(
+                    "trampoline payload cannot be lifted: "
+                    + "expected an RSB instruction and not a %s. "
+                    + "Contact system maintainer for support.",
+                    chkinstr3.mnemonic)
+
         else:
             chklogger.logger.critical(
                 "trampoline payload cannot be lifted: "

chb/invariants/XXprUtil.py

@@ -568,6 +568,12 @@ def global_variable_to_lval_expression(
                 subfieldkey = subfieldoffset.ckey
                 subfieldastoffset = astree.mk_field_offset(
                     subfieldname, subfieldkey)
+            elif fieldoffset.offset.is_array_index_offset:
+                asubfieldoffset = cast(
+                    "VMemoryOffsetArrayIndexOffset", fieldoffset.offset)
+                subfieldastoffset = array_offset_to_ast_offset(
+                    asubfieldoffset, xdata, iaddr, astree, anonymous=anonymous)
+
             else:
                 chklogger.logger.error(
                     "Index sub offset of global offset %s not yet handled at %s",