diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index a872b4c5..31856ce1 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ -chbversion: str = "0.3.0-20260630" +chbversion: str = "0.3.0-20260802" -minimum_required_chb_version = "0.6.0_20260617" +minimum_required_chb_version = "0.6.0_20260802" diff --git a/chb/app/InstrXData.py b/chb/app/InstrXData.py index b7ba00cd..6a3cce43 100644 --- a/chb/app/InstrXData.py +++ b/chb/app/InstrXData.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -83,7 +83,9 @@ def __init__( self._strs: List[str] = [] self._ints: List[int] = [] self._reachingdefs: List[Optional[ReachingDefFact]] = [] + self._reachingdefdoubles: List[Optional[ReachingDefFact]] = [] self._defuses: List[Optional[DefUse]] = [] + self._defusedoubles: List[Optional[DefUse]] = [] self._defuseshigh: List[Optional[DefUseHigh]] = [] self._flagreachingdefs: List[Optional[FlagReachingDefFact]] = [] @@ -222,6 +224,12 @@ def reachingdefs(self) -> List[Optional[ReachingDefFact]]: self._expand() return self._reachingdefs + @property + def reachingdefdoubles(self) -> List[Optional[ReachingDefFact]]: + if not self.expanded: + self._expand() + return self._reachingdefdoubles + @property def flag_reachingdefs(self) -> List[Optional[FlagReachingDefFact]]: if not self.expanded: @@ -234,6 +242,12 @@ def defuses(self) -> List[Optional[DefUse]]: self._expand() return self._defuses + @property + def defusedoubles(self) -> List[Optional[DefUse]]: + if not self.expanded: + self._expand() + return self._defusedoubles + @property def defuseshigh(self) -> List[Optional[DefUseHigh]]: if not self.expanded: @@ -397,11 +411,21 @@ def _expand(self) -> None: rdef = varinvd.var_invariant_fact(arg) if arg >= 0 else None rdef = cast(Optional[ReachingDefFact], rdef) self._reachingdefs.append(rdef) + elif c == "m": + varinvd = self.varinvdictionary + rdefdouble = varinvd.var_invariant_fact(arg) if arg >= 0 else None + rdefdouble = cast(Optional[ReachingDefFact], rdefdouble) + self._reachingdefdoubles.append(rdefdouble) elif c == "d": varinvd = self.varinvdictionary use = varinvd.var_invariant_fact(arg) if arg >= 0 else None use = cast(Optional[DefUse], use) self._defuses.append(use) + elif c == "n": + varinvd = self.varinvdictionary + usedouble = varinvd.var_invariant_fact(arg) if arg >= 0 else None + usedouble = cast(Optional[DefUse], usedouble) + self._defusedoubles.append(usedouble) elif c == "h": varinvd = self.varinvdictionary usehigh = varinvd.var_invariant_fact(arg) if arg > 0 else None @@ -671,6 +695,42 @@ def is_ternary_assignment(self) -> bool: def is_nondet_ternary_assignment(self) -> bool: return "agg:ternassign:nd" in self.tags + @property + def is_wide_move(self) -> bool: + return "agg:widemove" in self.tags + + @property + def is_wide_move_not(self) -> bool: + return "agg:widemovenot" in self.tags + + @property + def is_wide_add(self) -> bool: + return "agg:wideadd" in self.tags + + @property + def is_wide_subtract(self) -> bool: + return "agg:widesubtract" in self.tags + + @property + def is_wide_reversesubtract(self) -> bool: + return "agg:widereversesubtract" in self.tags + + @property + def is_wide_and(self) -> bool: + return "agg:wideand" in self.tags + + @property + def is_wide_or(self) -> bool: + return "agg:wideor" in self.tags + + @property + def is_wide_xor(self) -> bool: + return "agg:widexor" in self.tags + + @property + def is_wide_op_instruction(self) -> bool: + return "wop" in self.tags + @property def is_aggregate_jumptable(self) -> bool: return "agg-jt" in self.tags diff --git a/chb/arm/ARMCallOpcode.py b/chb/arm/ARMCallOpcode.py index d1ccde0f..777bbdec 100644 --- a/chb/arm/ARMCallOpcode.py +++ b/chb/arm/ARMCallOpcode.py @@ -135,14 +135,21 @@ def cx_arguments(self) -> List["XXpr"]: @property def argumentxvars(self) -> List["XXpr"]: argcount = self.argument_count + xprcount = len(self._xdata.xprs_r) argvars: List["XXpr"] = [] for i in range(argcount): - x = self._xdata.xprs_r[i + argcount] - if x is None: + if i + argcount < xprcount: + x = self._xdata.xprs_r[i + argcount] + if x is None: + raise UF.CHBError( + "Unexpected None-value call argument at index " + + str(i)) + argvars.append(x) + else: raise UF.CHBError( - "Unexpected None-value call argument at index " - + str(i)) - argvars.append(x) + "argumentxvars: out of range in " + str(self.calltarget) + + "; argcount: " + str(argcount) + + "; xprcount: " + str(xprcount)) return argvars def argument(self, index: int) -> Tuple[Optional["XXpr"], Optional[str]]: diff --git a/chb/arm/ARMInstruction.py b/chb/arm/ARMInstruction.py index d135d690..15570665 100644 --- a/chb/arm/ARMInstruction.py +++ b/chb/arm/ARMInstruction.py @@ -251,7 +251,7 @@ def annotation(self) -> str: return f"subsumed by {aggaddr}" elif self.subsumes: ann = self.opcode.annotation(self.xdata) - dependents = self.xdata.subsumes() + dependents = [str(s) for s in self.xdata.subsumes()] return ann + " (subsumes [" + ", ".join(dependents) + "])" else: return self.opcode.annotation(self.xdata) diff --git a/chb/arm/ARMOpcode.py b/chb/arm/ARMOpcode.py index c87785bb..8c6662dd 100644 --- a/chb/arm/ARMOpcode.py +++ b/chb/arm/ARMOpcode.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -98,6 +98,59 @@ def simplify_result(id1: int, id2: int, x1: XXpr, x2: XXpr) -> str: } +unary_wopvar_indices = { + "vrdlohi": 0, + "vrdlo": 1, + "vrdhi": 2 +} + +unary_wopxpr_indices = { + "xrnlo": 0, + "xrnhi": 1, + "rresultw": 2, + "rresultlo": 3, + "rresulthi": 4, + "xxrnlo": 5, + "xxrnhi": 6, + "xxrnw": 7 +} + +unary_wopcxpr_indices = { + "cresultw": 0, + "cresultlo": 1, + "cresulthi": 2 +} + + +binary_wopvar_indices = { + "vrdlohi": 0, + "vrdlo": 1, + "vrdhi": 2 +} + +binary_wopxpr_indices = { + "xrnlo": 0, + "xrnhi": 1, + "xrmlo": 2, + "xrmhi": 3, + "rresultw": 4, + "rresultlo": 5, + "rresulthi": 6, + "xxrnlo": 7, + "xxrnhi": 8, + "xxrmlo": 9, + "xxrmhi": 10, + "xxrnw": 11, + "xxrmw": 12 +} + +binary_wopcxpr_indices = { + "cresultw": 0, + "cresultlo": 1, + "cresulthi": 2 +} + + def get_extension(e: str) -> str: if e in extensions: return extensions[e] @@ -129,6 +182,20 @@ def var(self, index: int, name: str) -> "XVariable": self.__class__.__name__ + ":" + name + " has an error value") return v + def unary_wopvar(self, name: str) -> "XVariable": + if name in unary_wopvar_indices: + return self.var(unary_wopvar_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognized") + + def binary_wopvar(self, name: str) -> "XVariable": + if name in binary_wopvar_indices: + return self.var(binary_wopvar_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognized") + def has_var(self, index: int) -> bool: return self.xdata.has_var_r(index) @@ -163,12 +230,38 @@ def xpr(self, index: int, name: str) -> "XXpr": self.__class__.__name__ + ":" + name + " has an error value") return x + def unary_wopxpr(self, name: str) -> "XXpr": + if name in unary_wopxpr_indices: + return self.xpr(unary_wopxpr_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognized") + + def binary_wopxpr(self, name: str) -> "XXpr": + if name in binary_wopxpr_indices: + return self.xpr(binary_wopxpr_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognized") + def has_xpr(self, index: int) -> bool: return self.xdata.has_xpr_r(index) def is_xpr_ok(self, index: int) -> bool: return self.xdata.is_xpr_ok(index) + def is_unary_wopxpr_ok(self, name: str) -> bool: + if name in unary_wopxpr_indices: + return self.is_xpr_ok(unary_wopxpr_indices[name]) + else: + return False + + def is_binary_wopxpr_ok(self, name: str) -> bool: + if name in binary_wopxpr_indices: + return self.is_xpr_ok(binary_wopxpr_indices[name]) + else: + return False + def cxpr(self, index: int, name: str) -> "XXpr": if index >= len(self.xdata.cxprs_r): raise UF.CHBError( @@ -180,12 +273,38 @@ def cxpr(self, index: int, name: str) -> "XXpr": self.__class__.__name__ + ":" + name + " has an error value") return cx + def unary_wopcxpr(self, name: str) -> "XXpr": + if name in unary_wopcxpr_indices: + return self.cxpr(unary_wopcxpr_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognize") + + def binary_wopcxpr(self, name: str) -> "XXpr": + if name in binary_wopcxpr_indices: + return self.cxpr(binary_wopcxpr_indices[name], name) + else: + raise UF.CHBError( + self.__class__.__name__ + ":" + name + " not recognized") + def has_cxpr(self, index: int) -> bool: return self.xdata.has_cxpr_r(index) def is_cxpr_ok(self, index: int) -> bool: return self.xdata.is_cxpr_ok(index) + def is_unary_wopcxpr_ok(self, name: str) -> bool: + if name in unary_wopcxpr_indices: + return self.is_cxpr_ok(unary_wopcxpr_indices[name]) + else: + return False + + def is_binary_wopcxpr_ok(self, name: str) -> bool: + if name in binary_wopcxpr_indices: + return self.is_cxpr_ok(binary_wopcxpr_indices[name]) + else: + return False + def has_instruction_condition(self) -> bool: return self.xdata.has_instruction_condition() diff --git a/chb/arm/opcodes/ARMAdd.py b/chb/arm/opcodes/ARMAdd.py index 37f4ce3b..b92a8d57 100644 --- a/chb/arm/opcodes/ARMAdd.py +++ b/chb/arm/opcodes/ARMAdd.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 diff --git a/chb/arm/opcodes/ARMAddCarry.py b/chb/arm/opcodes/ARMAddCarry.py index 0810bcbf..2cf89ad1 100644 --- a/chb/arm/opcodes/ARMAddCarry.py +++ b/chb/arm/opcodes/ARMAddCarry.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -86,6 +86,10 @@ class ARMAddCarryXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_add(self) -> bool: + return self.xdata.is_wide_add + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -154,9 +158,101 @@ def rn_rdef(self) -> Optional["ReachingDefFact"]: def rm_rdef(self) -> Optional["ReachingDefFact"]: return self._xdata.reachingdefs[1] + # Wide add aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + @property def annotation(self) -> str: - assignment = str(self.vrd) + " := " + self.result_simplified + if self.is_wide_add: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + assignment = str(self.vrd) + " := " + self.result_simplified return self.add_instruction_condition(assignment) @@ -212,6 +308,77 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMAddCarryXData(xdata) return xd.annotation + def ast_prov_wide_add( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "ADC (wide-add)"] + + # low-level assignment + + (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree) + (ll_op1, _, _) = self.operands[1].ast_rvalue(astree) + (ll_op2, _, _) = self.operands[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("plus", ll_op1, ll_op2) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMAddCarryXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for rhs of wide-add at %s", iaddr) + return ([], [ll_assign]) + + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -220,6 +387,13 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + xd = ARMAddCarryXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_add: + return self.ast_prov_wide_add( + astree, iaddr, bytestring, xdata) + annotations: List[str] = [iaddr, "ADC"] # low-level assignment @@ -243,35 +417,18 @@ 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 xd.is_cresult_ok and xd.is_rresult_ok: + if xd.is_cresult_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( "ADC: Encountered error value for rhs at address %s", iaddr) return ([], [ll_assign]) lhs = xd.vrd - rhs1 = xd.xrn - rhs2 = xd.xrm - 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 diff --git a/chb/arm/opcodes/ARMBitwiseAnd.py b/chb/arm/opcodes/ARMBitwiseAnd.py index 000ae69c..a676af9f 100644 --- a/chb/arm/opcodes/ARMBitwiseAnd.py +++ b/chb/arm/opcodes/ARMBitwiseAnd.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -67,6 +67,10 @@ class ARMBitwiseAndXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_and(self) -> bool: + return self.xdata.is_wide_and + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -111,13 +115,105 @@ def result_simplified(self) -> str: else: return str(self.xrn) + " & " + str(self.xrm) + # Wide and aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + @property def annotation(self) -> str: - cresult = ( - " (C: " - + (str(self.cresult) if self.is_cresult_ok else "None") - + ")") - assignment = str(self.vrd) + " := " + self.result_simplified + cresult + if self.is_wide_and: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + cresult = ( + " (C: " + + (str(self.cresult) if self.is_cresult_ok else "None") + + ")") + assignment = str(self.vrd) + " := " + self.result_simplified + cresult return self.add_instruction_condition(assignment) @@ -174,6 +270,79 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMBitwiseAndXData(xdata) return xd.annotation + def ast_prov_wide_and( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "AND (wide-and)"] + + # low-level assignment + + (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) + (ll_rhs1, _, _) = self.opargs[1].ast_rvalue(astree) + (ll_rhs2, _, _) = self.opargs[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("band", ll_rhs1, ll_rhs2) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMBitwiseAndXData(xdata) + + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "AND: Encountered error value for wide-and rhs at address %s", + iaddr) + return ([], [ll_assign]) + + lhs = xd.vrdlohi + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -182,6 +351,20 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + xd = ARMBitwiseAndXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_and: + return self.ast_prov_wide_and( + astree, iaddr, bytestring, xdata) + + else: + chklogger.logger.warning( + "AND instruction at %s is part of an aggregate that is " + + "not yet supported", + iaddr) + return ([], []) + annotations: List[str] = [iaddr, "AND"] # low-level assignment diff --git a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py index c62d86e8..0f8c70f5 100644 --- a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py +++ b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -66,6 +66,10 @@ class ARMBitwiseExclusiveOrXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_xor(self) -> bool: + return self.xdata.is_wide_xor + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -106,11 +110,105 @@ def result_simplified(self) -> str: else: return str(self.result) + # Wide xor aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + @property def annotation(self) -> str: - cr = str(self.cresult) if self.is_cresult_ok else "" - cr = " (C: " + cr + ")" - assignment = str(self.vrd) + " := " + self.result_simplified + cr + if self.is_wide_xor: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + cresult = ( + " (C: " + + (str(self.cresult) if self.is_cresult_ok else "None") + + ")") + assignment = str(self.vrd) + " := " + self.result_simplified + cresult return self.add_instruction_condition(assignment) @@ -158,6 +256,77 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMBitwiseExclusiveOrXData(xdata) return xd.annotation + def ast_prov_wide_xor( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "EOR (wide-xor)"] + + # low-level assignment + + (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree) + (ll_op1, _, _) = self.operands[0].ast_rvalue(astree) + (ll_op2, _, _) = self.operands[0].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("bxor", ll_op1, ll_op2) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMBitwiseExclusiveOrXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for rhs of wide-xor at %s", iaddr) + + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -168,6 +337,22 @@ def ast_prov( annotations: List[str] = [iaddr, "EOR"] + xd = ARMBitwiseExclusiveOrXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_xor: + return self.ast_prov_wide_xor( + astree, iaddr, bytestring, xdata) + + else: + chklogger.logger.warning( + "EOR instruction at %s is part of an aggregate that is " + + " not yet supported", + iaddr) + return ([], []) + + # low-level assignment + (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree) (ll_op1, _, _) = self.operands[0].ast_rvalue(astree) (ll_op2, _, _) = self.operands[0].ast_rvalue(astree) diff --git a/chb/arm/opcodes/ARMBitwiseNot.py b/chb/arm/opcodes/ARMBitwiseNot.py index 01aa3efd..d54956c9 100644 --- a/chb/arm/opcodes/ARMBitwiseNot.py +++ b/chb/arm/opcodes/ARMBitwiseNot.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -54,6 +54,10 @@ class ARMBitwiseNotXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_move_not(self) -> bool: + return self.xdata.is_wide_move_not + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -75,8 +79,83 @@ def result_simplified(self) -> str: return simplify_result( self.xdata.args[2], self.xdata.args[3], self.result, self.rresult) + # Wide Move-Not + + @property + def vrdlohi(self) -> "XVariable": + return self.unary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.unary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.unary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.unary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.unary_wopxpr("xrnhi") + + @property + def rresultw(self) -> "XXpr": + return self.unary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_unary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.unary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.unary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.unary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.unary_wopxpr("xxrnhi") + + @property + def xxrnw(self) -> "XXpr": + return self.unary_wopxpr("xxrnw") + + @property + def cresultw(self) -> "XXpr": + return self.unary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_unary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.unary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.unary_wopcxpr("cresulthi") + + @property + def wide_move_not_ann(self) -> str: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = str(self.cresultw) if self.is_cresultw_ok else "None" + return lhs + " = " + rhs + " (C: " + cx + ")" + @property def annotation(self) -> str: + if self.is_wide_move_not: + return self.wide_move_not_ann assignment = str(self.vrd) + " := " + self.result_simplified return self.add_instruction_condition(assignment) @@ -134,6 +213,77 @@ def annotation(self, xdata: InstrXData) -> str: else: return "Error value" + def ast_prov_wide_move_not( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData + ) -> Tuple[List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "MVN (wide-move-not)"] + + # low-level assignment + + (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) + (ll_op, _, _) = self.opargs[1].ast_rvalue(astree) + ll_rhs = astree.mk_unary_op("bnot", ll_op) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMBitwiseNotXData(xdata) + + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for rhs of wide-not at %s", iaddr) + return ([], [ll_assign]) + + lhs = xd.vrdlohi + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -142,6 +292,20 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + xd = ARMBitwiseNotXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_move_not: + return self.ast_prov_wide_move_not( + astree, iaddr, bytestring, xdata) + + else: + chklogger.logger.warning( + "MVN instruction at %s is part of an aggregate that is " + + "not yet supported", + iaddr) + return ([], []) + annotations: List[str] = [iaddr, "MVN"] # low-level assignment @@ -159,7 +323,6 @@ def ast_prov( # high-level assignment - xd = ARMBitwiseNotXData(xdata) if not xd.is_ok: chklogger.logger.error( "Encountered error value at address %s", iaddr) diff --git a/chb/arm/opcodes/ARMBitwiseOr.py b/chb/arm/opcodes/ARMBitwiseOr.py index d95a1a84..89f26b95 100644 --- a/chb/arm/opcodes/ARMBitwiseOr.py +++ b/chb/arm/opcodes/ARMBitwiseOr.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -66,6 +66,10 @@ class ARMBitwiseOrXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_or(self) -> bool: + return self.xdata.is_wide_or + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -110,13 +114,105 @@ def result_simplified(self) -> str: else: return str(self.xrn) + " | " + str(self.xrm) + # Wide or aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + @property def annotation(self) -> str: - cresult = ( - " (C: " - + (str(self.cresult) if self.is_cresult_ok else "None") - + ")") - assignment = str(self.vrd) + " := " + self.result_simplified + cresult + if self.is_wide_or: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + cresult = ( + " (C: " + + (str(self.cresult) if self.is_cresult_ok else "None") + + ")") + assignment = str(self.vrd) + " := " + self.result_simplified + cresult return self.add_instruction_condition(assignment) @@ -169,6 +265,78 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMBitwiseOrXData(xdata) return xd.annotation + def ast_prov_wide_or( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "ORR (wide-or)"] + + # low-level assignment + + (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) + (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) + (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("bor", ll_op1, ll_op2) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMBitwiseOrXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for rhs value of wide-or at %s", iaddr) + return ([], [ll_assign]) + + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -177,6 +345,20 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + xd = ARMBitwiseOrXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_or: + return self.ast_prov_wide_or( + astree, iaddr, bytestring, xdata) + + else: + chklogger.logger.warning( + "ORR instruction at %s is part of an aggregate that is " + + "not yet supported", + iaddr) + return ([], []) + annotations: List[str] = [iaddr, "ORR"] # low-level assignment @@ -200,8 +382,6 @@ def ast_prov( # high-level assignment - xd = ARMBitwiseOrXData(xdata) - if xd.is_cresult_ok: rhs = xd.cresult diff --git a/chb/arm/opcodes/ARMLoadRegisterDual.py b/chb/arm/opcodes/ARMLoadRegisterDual.py index 7cfb29c9..86948315 100644 --- a/chb/arm/opcodes/ARMLoadRegisterDual.py +++ b/chb/arm/opcodes/ARMLoadRegisterDual.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -60,6 +60,10 @@ class ARMLoadRegisterDualXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_op_instruction(self) -> bool: + return self.xdata.is_wide_op_instruction + @property def vrt(self) -> "XVariable": return self.var(0, "vrt") @@ -76,6 +80,10 @@ def vmem(self) -> "XVariable": def vmem2(self) -> "XVariable": return self.var(3, "vmem2") + @property + def vrdlohi(self) -> "XVariable": + return self.var(4, "vrdlohi") + @property def xrn(self) -> "XXpr": return self.xpr(0, "xrn") @@ -88,10 +96,18 @@ def xrm(self) -> "XXpr": def xmem(self) -> "XXpr": return self.xpr(2, "xmem") + @property + def is_xmem_ok(self) -> bool: + return self.is_xpr_ok(2) + @property def xrmem(self) -> "XXpr": return self.xpr(3, "xrmem") + @property + def is_xrmem_ok(self) -> bool: + return self.is_xpr_ok(3) + @property def xmem2(self) -> "XXpr": return self.xpr(4, "xmem2") @@ -108,11 +124,39 @@ def xaddr1(self) -> "XXpr": def xaddr2(self) -> "XXpr": return self.xpr(7, "xaddr2") + @property + def xrmemw(self) -> "XXpr": + return self.xpr(8, "xrmemw") + + @property + def is_xrmemw_ok(self) -> bool: + return self.is_xpr_ok(8) + + @property + def cxrmemw(self) -> "XXpr": + return self.cxpr(0, "cxrmemw") + + @property + def is_cxrmemw_ok(self) -> bool: + return self.is_cxpr_ok(0) + @property def annotation(self) -> str: - assignment = ( - str(self.vrt) + " := " + str(self.xrmem) + "; " - + str(self.vrt2) + " := " + str(self.xrmem2) ) + if self.is_wide_op_instruction and self.is_xrmem_ok: + assignment = ( + str(self.vrdlohi) + " := " + str(self.xrmemw)) + elif self.is_xrmem_ok: + assignment = ( + str(self.vrt) + " := " + str(self.xrmem) + "; " + + str(self.vrt2) + " := " + str(self.xrmem2) ) + elif self.is_xmem_ok: + assignment = ( + str(self.vrt) + " := " + str(self.xmem) + "; " + + str(self.vrt2) + " := " + str(self.xmem2) ) + else: + assignment = ( + str(self.vrt) + " := *(" + str(self.xaddr1) + "); " + + str(self.vrt2) + " := *(" + str(self.xaddr2) + ")") wbu = self.writeback_update() return self.add_instruction_condition(assignment + wbu) @@ -216,10 +260,7 @@ def rhs(self, xdata: InstrXData) -> List[XXpr]: def annotation(self, xdata: InstrXData) -> str: xd = ARMLoadRegisterDualXData(xdata) - if xd.is_ok: - return xd.annotation - else: - return "Error value" + return xd.annotation def ast_prov( self, @@ -260,6 +301,40 @@ def ast_prov( # high-level assignments + if xd.is_wide_op_instruction: + lhs = xd.vrdlohi + if xd.is_cxrmemw_ok: + rhs = xd.cxrmemw + elif xd.is_xrmemw_ok: + rhs = xd.xrmemw + else: + chklogger.logger.error( + "Encountered error value for wide-LDRD at %s", iaddr) + return ([], [ll_assign1, ll_assign2]) + + defuses = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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_assign1) + astree.add_instr_mapping(hl_assign, ll_assign2) + astree.add_instr_address(hl_assign, [iaddr]) + astree.add_expr_mapping(hl_rhs, ll_rhs1) + astree.add_lval_mapping(hl_lhs, ll_lhs1) + astree.add_lval_defuses(hl_lhs, defuses[0]) + astree.add_lval_defuses_high(hl_lhs, defuseshigh[0]) + + return ([hl_assign], [ll_assign1, ll_assign2]) + if not xd.is_ok: chklogger.logger.error( "Encountered error value at address %s", iaddr) diff --git a/chb/arm/opcodes/ARMLoadRegisterSignedByte.py b/chb/arm/opcodes/ARMLoadRegisterSignedByte.py index 696b99d5..86badb70 100644 --- a/chb/arm/opcodes/ARMLoadRegisterSignedByte.py +++ b/chb/arm/opcodes/ARMLoadRegisterSignedByte.py @@ -227,8 +227,8 @@ def ast_prov( annotations=annotations) ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign] - basereg = xdata.vars[1] - newaddr = xdata.xprs[4] + basereg = xd.get_base_update_var() + newaddr = xd.get_base_update_cxpr() hl_addr_lhs = XU.xvariable_to_ast_lval(basereg, xdata, iaddr, astree) hl_addr_rhs = XU.xxpr_to_ast_def_expr(newaddr, xdata, iaddr, astree) diff --git a/chb/arm/opcodes/ARMMove.py b/chb/arm/opcodes/ARMMove.py index 06d1071c..7e154c14 100644 --- a/chb/arm/opcodes/ARMMove.py +++ b/chb/arm/opcodes/ARMMove.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -88,6 +88,7 @@ class ARMMoveXData(ARMOpcodeXData): - predicate/ternary: 0: p + """ def __init__(self, xdata: InstrXData) -> None: @@ -97,6 +98,18 @@ def __init__(self, xdata: InstrXData) -> None: def vrd(self) -> "XVariable": return self.var(0, "vrd") + @property + def vrdlohi(self) -> "XVariable": + return self.unary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.unary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.unary_wopvar("vrdhi") + @property def is_predicate_assign(self) -> bool: return self.xdata.is_predicate_assignment @@ -113,6 +126,10 @@ def is_ternary_assign(self) -> bool: def is_nondet_ternary_assign(self) -> bool: return self.xdata.is_nondet_ternary_assignment + @property + def is_wide_move(self) -> bool: + return self.xdata.is_wide_move + @property def xrm(self) -> "XXpr": return self.xpr(0, "xrm") @@ -125,14 +142,66 @@ def result(self) -> "XXpr": def is_result_ok(self) -> bool: return self.is_xpr_ok(1) + @property + def xrnlo(self) -> "XXpr": + return self.unary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.unary_wopxpr("xrnhi") + + @property + def rresultw(self) -> "XXpr": + return self.unary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_unary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.unary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.unary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.unary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.unary_wopxpr("xxrnhi") + + @property + def xxrnw(self) -> "XXpr": + return self.unary_wopxpr("xxrnw") + @property def cresult(self) -> "XXpr": return self.cxpr(0, "cresult") + @property + def cresultw(self) -> "XXpr": + return self.unary_wopcxpr("cresultw") + @property def is_cresult_ok(self) -> bool: return self.is_cxpr_ok(0) + @property + def is_cresultw_ok(self) -> bool: + return self.is_unary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.unary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.unary_wopcxpr("cresulthi") + @property def predicate(self) -> "XXpr": # known to be valid @@ -199,6 +268,13 @@ def ternary_assignment_ann(self) -> str: + ")") return str(self.vrd) + " := " + rhs + cpred + @property + def wide_move_ann(self) -> str: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = str(self.cresultw) if self.is_cresultw_ok else "None" + return lhs + " = " + rhs + " (C: " + cx + ")" + @property def annotation(self) -> str: if self.xdata.instruction_is_subsumed(): @@ -207,6 +283,8 @@ def annotation(self) -> str: return self.ternary_assignment_ann() if self.is_predicate_assign or self.is_nondet_predicate_assign: return self.predicate_assignment_ann() + if self.is_wide_move: + return self.wide_move_ann if self.xdata.instruction_subsumes(): return "subsumes " + ", ".join(self.xdata.subsumes()) cx = " (C: " + (str(self.cresult) if self.is_cresult_ok else "None") + ")" @@ -279,36 +357,73 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMMoveXData(xdata) return xd.annotation - def ast_prov_subsumed( + def ast_prov_wide_move( self, astree: ASTInterface, iaddr: str, bytestring: str, - xdata: InstrXData) -> Tuple[ - List[AST.ASTInstruction], List[AST.ASTInstruction]]: - """Return only low-level instruction with low-level condition.""" + xdata: InstrXData + ) -> Tuple[List[AST.ASTInstruction], List[AST.ASTInstruction]]: - annotations: List[str] = [iaddr, "MOV (subsumed)"] + annotations: List[str] = [iaddr, "MOV (wide-move)"] - (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) - (ll_rhs_t, _, _) = self.opargs[1].ast_rvalue(astree) - ll_rhs_f = astree.mk_lval_expr(ll_lhs) + # low-level assignment - cc = self.ast_cc_expr(astree) + (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) + (ll_rhs, _, _) = self.opargs[1].ast_rvalue(astree) - questionx = astree.mk_question(cc, ll_rhs_t, ll_rhs_f) ll_assign = astree.mk_assign( ll_lhs, - questionx, + ll_rhs, iaddr=iaddr, bytestring=bytestring, annotations=annotations) - rdefs = xdata.reachingdefs + # high-level assignment + + xd = ARMMoveXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for wide-move rhs value at %s", iaddr) + return ([], [ll_assign]) + + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[0]) + astree.add_lval_defuses_high(hl_lhs, defuseshigh[0]) - astree.add_expr_reachingdefs(ll_rhs_f, rdefs) + 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 ([], [ll_assign]) + return ([hl_assign], [ll_assign]) def ast_prov_predicate_assign( self, @@ -364,7 +479,7 @@ def ast_prov_predicate_assign( astree.add_expr_mapping(hl_rhs, ll_rhs) astree.add_lval_mapping(hl_lhs, ll_lhs) astree.add_expr_reachingdefs(hl_rhs, rdefs[1:]) - astree.add_expr_reachingdefs(ll_rhs, [rdefs[0]]) + astree.add_expr_reachingdefs(ll_rhs, rdefs) astree.add_lval_defuses(hl_lhs, defuses[0]) astree.add_lval_defuses_high(hl_lhs, defuseshigh[0]) @@ -466,9 +581,6 @@ def ast_prov( return ([], [nopinstr]) - if xdata.instruction_is_subsumed(): - return self.ast_prov_subsumed(astree, iaddr, bytestring, xdata) - xd = ARMMoveXData(xdata) if xdata.instruction_subsumes(): @@ -480,6 +592,10 @@ def ast_prov( return self.ast_prov_ternary_assign( astree, iaddr, bytestring, xdata) + elif xd.is_wide_move: + return self.ast_prov_wide_move( + astree, iaddr, bytestring, xdata) + else: chklogger.logger.warning( "MOV instruction at %s is part of an aggregate that is " diff --git a/chb/arm/opcodes/ARMReverseSubtractCarry.py b/chb/arm/opcodes/ARMReverseSubtractCarry.py index 08c66e10..fc4400e0 100644 --- a/chb/arm/opcodes/ARMReverseSubtractCarry.py +++ b/chb/arm/opcodes/ARMReverseSubtractCarry.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2023 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -25,25 +25,213 @@ # SOFTWARE. # ------------------------------------------------------------------------------ -from typing import List, TYPE_CHECKING +from typing import cast, List, Tuple, TYPE_CHECKING 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 -import chb.util.fileutil as UF +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 if TYPE_CHECKING: from chb.arm.ARMDictionary import ARMDictionary + from chb.arm.ARMOperandKind import ARMShiftedRegisterOp + from chb.invariants.XVariable import XVariable + from chb.invariants.XXpr import XXpr + + +class ARMReverseSubtractCarryXData(ARMOpcodeXData): + """Data format: + - variables: + 0: vrd + + - expressions: + 0: xrn + 1. xrm + 2: result + 3: rresult (result rewritten) + + - c expressions: + 0: cresult + """ + + def __init__(self, xdata: InstrXData) -> None: + ARMOpcodeXData.__init__(self, xdata) + + @property + def is_wide_reverse_subtract(self) -> bool: + return self.xdata.is_wide_reversesubtract + + @property + def vrd(self) -> "XVariable": + return self.var(0, "vrd") + + @property + def xrn(self) -> "XXpr": + return self.xpr(0, "xrn") + + @property + def xrm(self) -> "XXpr": + return self.xpr(1, "xrm") + + @property + 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: + 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.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) + + # Wide reverse subtract aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + + @property + def annotation(self) -> str: + if self.is_wide_reverse_subtract: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + assignment = str(self.vrd) + " := " + self.result_simplified + return self.add_instruction_condition(assignment) @armregistry.register_tag("RSC", ARMOpcode) class ARMReverseSubtractCarry(ARMOpcode): - """Subtracts a value from a register and saves the result in a register. + """Subtracts a value from a register, adds the carry and saves the result in a register. RSC{S} , , # RSC{S} , , {, } @@ -71,10 +259,163 @@ def is_writeback(self) -> bool: def operands(self) -> List[ARMOperand]: return [self.armd.arm_operand(self.args[i]) for i in [1, 2, 3]] + @property + def opargs(self) -> List[ARMOperand]: + return [self.armd.arm_operand(self.args[i]) for i in [1, 2, 3]] + def mnemonic_extension(self) -> str: wb = "S" if self.is_writeback else "" cc = ARMOpcode.mnemonic_extension(self) return wb + cc def annotation(self, xdata: InstrXData) -> str: - return "pending" + xd = ARMReverseSubtractCarryXData(xdata) + return xd.annotation + + def ast_prov_wide_reverse_subtract( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "RSC (wide-reverse-subtract)"] + + # low-level assignment + + (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree) + (ll_op1, _, _) = self.operands[1].ast_rvalue(astree) + (ll_op2, _, _) = self.operands[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("minus", ll_op2, ll_op1) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMReverseSubtractCarryXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value for rhs of wide-reverse-subtract at %s", + iaddr) + return ([], [ll_assign]) + + rdefdoubles= xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + + def ast_prov( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + xd = ARMReverseSubtractCarryXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_reverse_subtract: + return self.ast_prov_wide_reverse_subtract( + astree, iaddr, bytestring, xdata) + + annotations: List[str] = [iaddr, "RSC"] + + # low-level assignment + + (ll_lhs, _, _) = self.operands[0].ast_lvalue(astree) + (ll_op1, _, _) = self.operands[1].ast_rvalue(astree) + (ll_op2, _, _) = self.operands[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("minus", ll_op2, ll_op1) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + rdefs = xdata.reachingdefs + + astree.add_expr_reachingdefs(ll_op1, [rdefs[0]]) + astree.add_expr_reachingdefs(ll_op2, [rdefs[1]]) + + # high-level assignment + + lhs = xd.vrd + if xd.is_cresult_ok: + rhs = xd.cresult + elif xd.is_rresult_ok: + rhs = xd.rresult + else: + chklogger.logger.warning( + "RSC: Encountered error for rhs value at address %s", iaddr) + return ([], [ll_assign]) + + 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) + + 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_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]) diff --git a/chb/arm/opcodes/ARMSignedMultiplyLong.py b/chb/arm/opcodes/ARMSignedMultiplyLong.py index 84b73603..bf8bc528 100644 --- a/chb/arm/opcodes/ARMSignedMultiplyLong.py +++ b/chb/arm/opcodes/ARMSignedMultiplyLong.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -53,13 +53,17 @@ class ARMSignedMultiplyLongXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def vlohi(self) -> "XVariable": + return self.var(0, "vlohi") + @property def vlo(self) -> "XVariable": - return self.var(0, "vlo") + return self.var(1, "vlo") @property def vhi(self) -> "XVariable": - return self.var(1, "vhi") + return self.var(2, "vhi") @property def xrn(self) -> "XXpr": @@ -69,21 +73,37 @@ def xrn(self) -> "XXpr": def xrm(self) -> "XXpr": return self.xpr(1, "xrm") + @property + def result(self) -> "XXpr": + return self.xpr(2, "result") + + @property + def is_result_ok(self) -> bool: + return self.is_xpr_ok(2) + + @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 loresult(self) -> "XXpr": - return self.xpr(2, "loresult") + return self.xpr(3, "loresult") @property def hiresult(self) -> "XXpr": - return self.xpr(3, "hiresult") + return self.xpr(4, "hiresult") @property def loresultr(self) -> "XXpr": - return self.xpr(4, "loresultr") + return self.xpr(5, "loresultr") @property def hiresultr(self) -> "XXpr": - return self.xpr(5, "hiresultr") + return self.xpr(6, "hiresultr") @property def resultlo_simplified(self) -> str: @@ -97,9 +117,8 @@ def resulthi_simplified(self) -> str: @property def annotation(self) -> str: - assignment1 = str(self.vlo) + " := " + self.resultlo_simplified - assignment2 = str(self.vhi) + " := " + self.resulthi_simplified - return self.add_instruction_condition(assignment1 + "; " + assignment2) + assign = str(self.vlohi) + " := " + str(self.result) + return self.add_instruction_condition(assign) @armregistry.register_tag("SMULL", ARMOpcode) @@ -177,52 +196,35 @@ def ast_prov( # high-level assignment xd = ARMSignedMultiplyLongXData(xdata) - if not xd.is_ok: - chklogger.logger.error( - "Encountered error value at address %s", iaddr) - return ([], []) - - lhs = xd.vlo - lhs2 = xd.vhi - rhs1 = xd.xrn - rhs2 = xd.xrm - rhslo = xd.loresult - rhshi = xd.hiresult - - defuses = xdata.defuses + if xd.is_cresult_ok: + rhs = xd.cresult + elif xd.is_result_ok: + rhs = xd.result + else: + if not xd.is_ok: + chklogger.logger.error( + "SMULL: Encountered error value at address %s", iaddr) + return ([], [ll_assign1, ll_assign2]) + + defuses = xdata.defusedoubles defuseshigh = xdata.defuseshigh + lhs = xd.vlohi + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree) - hl_lhs2 = XU.xvariable_to_ast_lval(lhs2, xdata, iaddr, astree) - hl_rhs = XU.xxpr_to_ast_def_expr(rhslo, xdata, iaddr, astree) - hl_rhs2 = XU.xxpr_to_ast_def_expr(rhshi, xdata, iaddr, astree) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree) - hl_assign1 = astree.mk_assign( + hl_assign = astree.mk_assign( hl_lhs, hl_rhs, iaddr=iaddr, bytestring=bytestring, annotations=annotations) - hl_assign2 = astree.mk_assign( - hl_lhs2, - hl_rhs2, - iaddr=iaddr, - bytestring=bytestring, - annotations=annotations) - astree.add_instr_mapping(hl_assign1, ll_assign1) - astree.add_instr_mapping(hl_assign2, ll_assign2) - astree.add_instr_address(hl_assign1, [iaddr]) - astree.add_instr_address(hl_assign2, [iaddr]) - astree.add_expr_mapping(hl_rhs, ll_rhs) - astree.add_expr_mapping(hl_rhs2, ll_rhs2) - astree.add_lval_mapping(hl_lhs, ll_lhs) - astree.add_lval_mapping(hl_lhs2, ll_lhs2) - astree.add_expr_reachingdefs(hl_rhs, rdefs[2:]) - astree.add_expr_reachingdefs(ll_rhs, rdefs[:2]) + astree.add_instr_mapping(hl_assign, ll_assign1) + astree.add_instr_address(hl_assign, [iaddr]) + astree.add_expr_reachingdefs(hl_rhs, rdefs) astree.add_lval_defuses(hl_lhs, defuses[0]) - astree.add_lval_defuses(hl_lhs2, defuses[1]) astree.add_lval_defuses_high(hl_lhs, defuseshigh[0]) - astree.add_lval_defuses_high(hl_lhs2, defuseshigh[1]) - return ([hl_assign1, hl_assign2], [ll_assign1, ll_assign2]) + return ([hl_assign], [ll_assign1, ll_assign2]) diff --git a/chb/arm/opcodes/ARMStoreRegisterDual.py b/chb/arm/opcodes/ARMStoreRegisterDual.py index 8e8f49c4..e75508a3 100644 --- a/chb/arm/opcodes/ARMStoreRegisterDual.py +++ b/chb/arm/opcodes/ARMStoreRegisterDual.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -58,6 +58,10 @@ class ARMStoreRegisterDualXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def is_wide_op_instruction(self) -> bool: + return self.xdata.is_wide_op_instruction + @property def vmem1(self) -> "XVariable": return self.var(0, "vmem1") @@ -110,11 +114,16 @@ def is_xaddr_known(self) -> bool: def xaddr_updated(self) -> "XXpr": return self.xpr(8, "xaddr_updated") + @property + def cxcombined(self) -> "XXpr": + return self.cxpr(0, "cxcombined") + @property def annotation(self) -> str: wbu = self.writeback_update() rhs1 = self.xxrt rhs2 = self.xxrt2 + cxpr = (str(self.cxcombined) if self.is_wide_op_instruction else "") if self.is_ok or self.is_vmem_known: assign1 = str(self.vmem1) + " := " + str(rhs1) assign2 = str(self.vmem2) + " := " + str(rhs2) @@ -125,7 +134,7 @@ def annotation(self) -> str: assigns = assign1 + "; " + assign2 else: assigns = "Error in vmem and xaddr" - return self.add_instruction_condition(assigns + wbu) + return self.add_instruction_condition(assigns + wbu + " (C: " + cxpr + ")") @armregistry.register_tag("STRD", ARMOpcode) diff --git a/chb/arm/opcodes/ARMSubtractCarry.py b/chb/arm/opcodes/ARMSubtractCarry.py index 7f1171af..8b32647d 100644 --- a/chb/arm/opcodes/ARMSubtractCarry.py +++ b/chb/arm/opcodes/ARMSubtractCarry.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -50,6 +50,13 @@ class ARMSubtractCarryXData(ARMOpcodeXData): + def __init__(self, xdata: InstrXData) -> None: + ARMOpcodeXData.__init__(self, xdata) + + @property + def is_wide_subtract(self) -> bool: + return self.xdata.is_wide_subtract + @property def vrd(self) -> "XVariable": return self.var(0, "vrd") @@ -70,14 +77,118 @@ def result(self) -> "XXpr": 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) + # Wide subtract aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.binary_wopvar("vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.binary_wopvar("vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.binary_wopxpr("xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.binary_wopxpr("xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.binary_wopxpr("xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") + + @property + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") + + @property + def rresultlo(self) -> "XXpr": + return self.binary_wopxpr("rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.binary_wopxpr("rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.binary_wopxpr("xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.binary_wopxpr("xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.binary_wopxpr("xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.binary_wopxpr("xxrmhi") + + @property + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") + + @property + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") + + @property + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") + + @property + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") + + @property + def cresultlo(self) -> "XXpr": + return self.binary_wopcxpr("cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.binary_wopcxpr("cresulthi") + @property def annotation(self) -> str: - assignment = str(self.vrd) + " := " + self.result_simplified + if self.is_wide_subtract: + lhs = str(self.vrdlohi) + rhs = str(self.rresultw) + cx = " (C: " + (str(self.cresultw) if self.is_cresultw_ok else "None") + ")" + assignment = lhs + " := " + rhs + cx + else: + assignment = str(self.vrd) + " := " + self.result_simplified return self.add_instruction_condition(assignment) @@ -103,6 +214,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]] + @property + def opargs(self) -> List[ARMOperand]: + return [self.armd.arm_operand(self.args[i]) for i in [1, 2, 3]] + def mnemonic_extension(self) -> str: cc = ARMOpcode.mnemonic_extension(self) wb = "S" if self.is_writeback else "" @@ -120,6 +235,78 @@ def annotation(self, xdata: InstrXData) -> str: else: return "Error value" + def ast_prov_wide_subtract( + self, + astree: ASTInterface, + iaddr: str, + bytestring: str, + xdata: InstrXData) -> Tuple[ + List[AST.ASTInstruction], List[AST.ASTInstruction]]: + + annotations: List[str] = [iaddr, "SBC (wide-subtract)"] + + # low-level assignment + + (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) + (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) + (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) + ll_rhs = astree.mk_binary_op("minus", ll_op1, ll_op2) + + ll_assign = astree.mk_assign( + ll_lhs, + ll_rhs, + iaddr=iaddr, + bytestring=bytestring, + annotations=annotations) + + # high-level assignment + + xd = ARMSubtractCarryXData(xdata) + + lhs = xd.vrdlohi + if xd.is_cresultw_ok: + rhs = xd.cresultw + elif xd.is_rresultw_ok: + rhs = xd.rresultw + else: + chklogger.logger.warning( + "Encountered error value rhs of wide-subtract at %s", iaddr) + return ([], [ll_assign]) + + rdefdoubles = xdata.reachingdefdoubles + if len(rdefdoubles) == 0: + rdefdoubles = xdata.reachingdefs + defusedoubles = xdata.defusedoubles + defuseshigh = xdata.defuseshigh + + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree, rhs=rhs) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, 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, rdefdoubles) + astree.add_expr_reachingdefs(ll_rhs, [rdefdoubles[0]]) + astree.add_lval_defuses(hl_lhs, defusedoubles[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) + + astree.add_expose_instruction(hl_assign.instrid) + + return ([hl_assign], [ll_assign]) + def ast_prov( self, astree: ASTInterface, @@ -128,6 +315,13 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + xd = ARMSubtractCarryXData(xdata) + + if xdata.instruction_subsumes(): + if xd.is_wide_subtract: + return self.ast_prov_wide_subtract( + astree, iaddr, bytestring, xdata) + annotations: List[str] = [iaddr, "SBC"] # low-level assignment @@ -151,22 +345,21 @@ def ast_prov( # high-level assignment - xd = ARMSubtractCarryXData(xdata) - if not xd.is_ok: + lhs = xd.vrd + if xd.is_cresult_ok: + rhs = xd.cresult + elif xd.is_rresult_ok: + rhs = xd.rresult + else: chklogger.logger.error( - "Encountered error value at address %s", iaddr) + "SBC: Encountered error value for rhs value at address %s", iaddr) return ([], []) - lhs = xd.vrd - rhs1 = xd.xrn - rhs2 = xd.xrm - rhs3 = 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(rhs3, xdata, iaddr, astree) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree) hl_assign = astree.mk_assign( hl_lhs, @@ -184,4 +377,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]) diff --git a/chb/arm/opcodes/ARMUnsignedMultiplyLong.py b/chb/arm/opcodes/ARMUnsignedMultiplyLong.py index 72e783b5..62d758b7 100644 --- a/chb/arm/opcodes/ARMUnsignedMultiplyLong.py +++ b/chb/arm/opcodes/ARMUnsignedMultiplyLong.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs LLC +# Copyright (c) 2021-2026 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 @@ -53,13 +53,17 @@ class ARMUnsignedMultiplyLongXData(ARMOpcodeXData): def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) + @property + def vlohi(self) -> "XVariable": + return self.var(0, "vlohi") + @property def vlo(self) -> "XVariable": - return self.var(0, "vlo") + return self.var(1, "vlo") @property def vhi(self) -> "XVariable": - return self.var(1, "vhi") + return self.var(2, "vhi") @property def xrn(self) -> "XXpr": @@ -77,6 +81,18 @@ def result(self) -> "XXpr": 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( @@ -103,12 +119,6 @@ class ARMUnsignedMultiplyLong(ARMOpcode): xdata format: a:vvxxxxrrddhh ---------------------------- - vars[0]: lhs1 (RdLo) - vars[1]: lhs2 (RdHi) - xprs[0]: rhs1 (Rn) - xprs[1]: rhs2 (Rm) - xprs[2]: rhs1 * rhs2 - xprs[3]: rhs1 * rhs2 (simplified) rdefs[1]: rhs1 (Rn) rdefs[2]: rhs2 (Rm) uses[0]: lhs1 (RdLo) @@ -136,35 +146,6 @@ def annotation(self, xdata: InstrXData) -> str: else: return "Error value" - def assembly_ast( - self, - astree: ASTInterface, - iaddr: str, - bytestring: str, - xdata: InstrXData) -> List[AST.ASTInstruction]: - - annotations: List[str] = [iaddr, "UMULL"] - - (rhs1, preinstrs1, postinstrs1) = self.operands[2].ast_rvalue(astree) - (rhs2, preinstrs2, postinstrs2) = self.operands[3].ast_rvalue(astree) - (lhs1, _, _) = self.operands[0].ast_lvalue(astree) - (lhs2, _, _) = self.operands[1].ast_lvalue(astree) - binop = astree.mk_binary_op("mult", rhs1, rhs2) - zero = astree.mk_integer_constant(0) - assign1 = astree.mk_assign( - lhs1, - binop, - iaddr=iaddr, - bytestring=bytestring, - annotations=(annotations + ["low"])) - assign2 = astree.mk_assign( - lhs2, - zero, - iaddr=iaddr, - bytestring=bytestring, - annotations=annotations) - return preinstrs1 + preinstrs2 + [assign1, assign2] + postinstrs1 + postinstrs2 - # -------------------------------------------------------------------------- # Operation # result = UInt(R[n]) * UInt(R[m]); @@ -212,50 +193,34 @@ def ast_prov( # high-level assignments xd = ARMUnsignedMultiplyLongXData(xdata) - if not xd.is_ok: + if xd.is_cresult_ok: + rhs = xd.cresult + elif xd.is_rresult_ok: + rhs = xd.rresult + else: chklogger.logger.error( - "Encountered error value at address %s", iaddr) - return ([], []) - - lhs1 = xd.vlo - lhs2 = xd.vhi - rhs1 = xd.xrn - rhs2 = xd.xrm - result = xd.rresult + "UMULL: Encountered error value at address %s", iaddr) + return ([], [ll_assign_lo, ll_assign_hi]) + + lhs = xd.vlohi rdefs = xdata.reachingdefs - defuses = xdata.defuses + defuses = xdata.defusedoubles defuseshigh = xdata.defuseshigh - hl_lhslo = XU.xvariable_to_ast_lval(lhs1, xdata, iaddr, astree) - hl_lhshi = XU.xvariable_to_ast_lval(lhs2, xdata, iaddr, astree) - - hl_rhslo = XU.xxpr_to_ast_def_expr(result, xdata, iaddr, astree) - hl_rhshi = astree.mk_binary_op( - "lsr", hl_rhslo, astree.mk_integer_constant(32)) + hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree) + hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree) - hl_assign_lo = astree.mk_assign( - hl_lhslo, - hl_rhslo, - iaddr=iaddr, - bytestring=bytestring, - annotations=annotations) - hl_assign_hi = astree.mk_assign( - ll_lhshi, - hl_rhshi, + hl_assign = astree.mk_assign( + hl_lhs, + hl_rhs, iaddr=iaddr, bytestring=bytestring, annotations=annotations) - astree.add_instr_mapping(hl_assign_lo, ll_assign_lo) - astree.add_instr_mapping(hl_assign_hi, ll_assign_hi) - astree.add_instr_address(hl_assign_lo, [iaddr]) - astree.add_expr_mapping(hl_rhslo, ll_lo_result) - astree.add_lval_mapping(hl_lhslo, ll_lhslo) - astree.add_expr_reachingdefs(ll_op1, [rdefs[0]]) - astree.add_expr_reachingdefs(ll_op2, [rdefs[1]]) - astree.add_lval_defuses(hl_lhslo, defuses[0]) - astree.add_lval_defuses(hl_lhshi, defuses[1]) - astree.add_lval_defuses_high(hl_lhslo, defuseshigh[0]) - astree.add_lval_defuses_high(hl_lhshi, defuseshigh[1]) - - return ([hl_assign_lo, hl_assign_hi], [ll_assign_lo, ll_assign_hi]) + astree.add_instr_mapping(hl_assign, ll_assign_lo) + astree.add_instr_address(hl_assign, [iaddr]) + astree.add_expr_reachingdefs(hl_rhs, rdefs) + 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]) diff --git a/chb/ast/ASTNode.py b/chb/ast/ASTNode.py index c7b66ff5..76af620d 100644 --- a/chb/ast/ASTNode.py +++ b/chb/ast/ASTNode.py @@ -211,7 +211,7 @@ def callees(self) -> Set[str]: return set([]) def __str__(self) -> str: - return self.tag + return "tag:" + self.tag class ASTStmt(ASTNode): @@ -2457,7 +2457,7 @@ def index(self, indexer: "ASTIndexer") -> int: def ctype(self, ctyper: "ASTCTyper") -> Optional["ASTTyp"]: return ctyper.ctype_float_typ(self) - def __str_(self) -> str: + def __str__(self) -> str: return floattypes[self.fkind] def __eq__(self, other: Any) -> bool: diff --git a/chb/ast/CustomASTSupport.py b/chb/ast/CustomASTSupport.py index c36b6eaf..ffb524ee 100644 --- a/chb/ast/CustomASTSupport.py +++ b/chb/ast/CustomASTSupport.py @@ -37,7 +37,12 @@ arm32_register_sizes["PC"] = 32 # program counter # ARM32 double registers +arm32_register_sizes["R0_R1"] = 64 arm32_register_sizes["R2_R3"] = 64 +arm32_register_sizes["R4_R5"] = 64 +arm32_register_sizes["R6_R7"] = 64 +arm32_register_sizes["R8_R9"] = 64 +arm32_register_sizes["R10_R11"] = 64 # ARM32 floating point / adv simd registers arm_fp_sp_register_sizes: Dict[str, int] = { diff --git a/chb/cmdline/AnalysisManager.py b/chb/cmdline/AnalysisManager.py index 51708e10..f8784521 100644 --- a/chb/cmdline/AnalysisManager.py +++ b/chb/cmdline/AnalysisManager.py @@ -70,6 +70,7 @@ def __init__( arm: bool = False, power: bool = False, thumb: bool = False, + float_abi: Optional[str] = None, savedatablocks: bool = False, ifilenames: List[str] = [], fns_no_lineq: List[str] = [], @@ -104,6 +105,7 @@ def __init__( self.arm = arm self.power = power self.thumb = thumb + self.float_abi = float_abi self.exclude_debug = exclude_debug self.savedatablocks = savedatablocks self.hints = hints @@ -162,6 +164,8 @@ def extract_executable( cmd.append("-elf") if self.exclude_debug: cmd.append("-exclude_debug") + if self.float_abi: + cmd.extend(["-float-abi", self.float_abi]) if verbose: cmd.append("-verbose") for d in self.deps: @@ -253,6 +257,8 @@ def disassemble( cmd.append("-verbose") if self.thumb: cmd.append("-thumb") + if self.float_abi: + cmd.extend(["-float-abi", self.float_abi]) if self.savedatablocks: cmd.append("-set_datablocks") for d in self.deps: @@ -475,6 +481,8 @@ def _analyze_until_stable( cmd.append("-thumb") if self.power: cmd.append("-power") + if self.float_abi: + cmd.extend(["-float-abi", self.float_abi]) for d in self.deps: cmd.extend(["-summaries", d]) for s in self.so_libraries: diff --git a/chb/cmdline/chkx b/chb/cmdline/chkx index 45414529..4c9370be 100755 --- a/chb/cmdline/chkx +++ b/chb/cmdline/chkx @@ -403,6 +403,10 @@ def parse() -> argparse.Namespace: nargs="*", default=[], help="arm-thumb switch points (format :T or :A)") + analyzecmd.add_argument( + "--float-abi", + choices=["hardfloat", "softfloat"], + help="switch to indicate the presence of VFP/NEON extension (default=hardfloat)") analyzecmd.add_argument( "--iterations", type=int, @@ -1109,6 +1113,11 @@ def parse() -> argparse.Namespace: "function", help="hex address of function") resultsbranchconditions.set_defaults(func=UCC.results_branchconditions) + # --results predicated instructions --- + resultspredinstrs = resultsparsers.add_parser("predicated_instructions") + resultspredinstrs.add_argument("xname", help="name of executable") + resultspredinstrs.set_defaults(func=UCC.results_predicated_instructions) + # --- results structures --- resultsstructs = resultsparsers.add_parser("structs") resultsstructs.add_argument("xname", help="name of executable") diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index ee511239..0a9d696a 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -108,6 +108,7 @@ from chb.x86.X86Access import X86Access if TYPE_CHECKING: + from chb.app.BasicBlock import BasicBlock import chb.app.Instruction import chb.arm.ARMInstruction from chb.bctypes.BCCompInfo import BCCompInfo @@ -404,6 +405,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: save_asm_cfg_info: bool = args.save_asm_cfg_info print_datasections: List[str] = args.print_datasections thumb: List[str] = args.thumb + floatabi: Optional[str] = args.float_abi preamble_cutoff: int = args.preamble_cutoff iterations: int = args.iterations analysisrepeats: int = args.analysisrepeats @@ -562,6 +564,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: use_ssa=xssa, no_varinvs=xnovarinvs, include_arm_extension_registers=xarmextensionregisters, + float_abi=floatabi, thumb=(len(thumb) > 0)) if dodisassemble: @@ -1677,6 +1680,40 @@ def results_branchconditions(args: argparse.Namespace) -> NoReturn: exit(0) +def results_predicated_instructions(args: argparse.Namespace) -> NoReturn: + + # arguments + xname: str = str(args.xname) + + try: + (path, xfile) = get_path_filename(xname) + UF.check_analysis_results(path, xfile) + except UF.CHBError as e: + print_error(str(e.wrap())) + exit(1) + + xinfo = XI.XInfo() + xinfo.load(path, xfile) + + app = get_app(path, xfile, xinfo) + + blocks: Dict[str, List["BasicBlock"]] = {} + + for (faddr, fn) in app.functions.items(): + for b in fn.blocks.values(): + if b.has_control_flow(): + blocks.setdefault(faddr, []) + blocks[faddr].append(b) + for (faddr, blist) in sorted(blocks.items()): + print(faddr) + for b in blist: + print(str(b)) + print("") + print("\n\n") + + exit(0) + + def results_structs(args: argparse.Namespace) -> NoReturn: """Return a json file with struct variables / expressions.""" diff --git a/chb/invariants/XXprUtil.py b/chb/invariants/XXprUtil.py index a4c4e5fc..775cbe9e 100644 --- a/chb/invariants/XXprUtil.py +++ b/chb/invariants/XXprUtil.py @@ -1150,6 +1150,9 @@ def xunary_to_ast_def_expr( else: return astree.mk_address_of(astvar) + if operator == "xf_signextend64": + return xxpr_to_ast_def_expr(xpr, xdata, iaddr, astree, anonymous=anonymous) + if not anonymous: chklogger.logger.error( "AST def conversion of unary expression %s at address %s not yet " diff --git a/chb/userdata/UserHints.py b/chb/userdata/UserHints.py index 65f9ae33..f9641d99 100644 --- a/chb/userdata/UserHints.py +++ b/chb/userdata/UserHints.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2025 Aarno Labs, LLC +# Copyright (c) 2021-2026 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 @@ -36,6 +36,9 @@ a few data items. Currently provided: +- Aggregates + sequences of instructions that represent compiler idioms + - ArgumentConstraints: function arguments and global variables @@ -66,6 +69,9 @@ - InlinedFunctions addresses of functions to be inlined +- InstructionAnnotations + external information on individual instructions (e.g., wide-op) + - NonReturningCalls list of function/instr addresses with calls that do not return (intended for functions that may return in other calls) @@ -138,6 +144,51 @@ def __str__(self) -> str: return self.name +class AggregatesHints(HintsEntry): + """List of records specifying an instruction sequence aggregate.""" + + def __init__(self, aggregates: List[Dict[str, str]]) -> None: + """Format: {anchor:<.>, name:<.>}.""" + + HintsEntry.__init__(self, "aggregates") + self._aggregates = aggregates + self._anchors = [x["anchor"] for x in aggregates] + + @property + def aggregates(self) -> List[Dict[str, str]]: + return self._aggregates + + def has_anchor(self, addr: str) -> bool: + return addr in self._anchors + + def update(self, d: List[Dict[str, str]]) -> None: + for agg in d: + addr = agg.get("anchor", "?") + if not self.has_anchor(addr): + self._aggregates.append(agg) + self._anchors.append(addr) + + def to_xml(self, node: ET.Element) -> None: + xaggregates = ET.Element(self.name) + node.append(xaggregates) + for agg in sorted(self.aggregates, key=lambda r: r["anchor"]): + xagg = ET.Element("agg") + xagg.set("anchor", agg["anchor"]) + xagg.set("name", agg.get("name", "?")) + xaggregates.append(xagg) + + def __str__(self) -> str: + lines: List[str] = [] + lines.append("Aggregates") + lines.append("----------") + for agg in self.aggregates: + lines.append( + " [" + + agg.get("anchor", "?") + ": " + agg.get("name", "?") + + "]") + return "\n".join(lines) + + class ARMArgumentConstraints(HintsEntry): """Mapping of registers to lower/upper bounds per function.""" @@ -1093,6 +1144,46 @@ def __str__(self) -> str: return "\n".join(lines) +class InstructionAnnotationsHints(HintsEntry): + """External information on individual instructions + + Format: + {iaddr:<.>, kind:<.>} + """ + + def __init__(self, instranns: List[Dict[str, str]]) -> None: + HintsEntry.__init__(self, "instruction-annotations") + self._instranns = instranns + self._iaddrs = [x["iaddr"] for x in instranns] + + @property + def instranns(self) -> List[Dict[str, str]]: + return self._instranns + + def update(self, d: List[Dict[str, str]]) -> None: + for iann in d: + if not iann["iaddr"] in self._iaddrs: + self._instranns.append(iann) + self._iaddrs.append(iann["iaddr"]) + + def to_xml(self, node: ET.Element) -> None: + xinstrannotations = ET.Element(self.name) + node.append(xinstrannotations) + for iann in sorted(self.instranns, key=lambda r: r["iaddr"]): + xiann = ET.Element("iann") + xiann.set("iaddr", iann["iaddr"]) + xiann.set("kind", iann.get("kind", "?")) + xinstrannotations.append(xiann) + + def __str__(self) -> str: + lines: List[str] = [] + lines.append("Instruction annotations") + lines.append("-----------------------") + for iann in self.instranns: + lines.append(" [" + iann["iaddr"] + ": " + iann.get("kind", "?") + "]") + return "\n".join(lines) + + class NonReturningCallsHints(HintsEntry): """Call sites where the call does not return. @@ -1618,6 +1709,14 @@ def add_hints(self, hints: Dict[str, Any]) -> None: self._hints.update(hints) + if "aggregates" in hints: + tag = "aggregates" + aggregates: List[Dict[str, str]] = hints[tag] + if tag in self.userdata: + self.userdata[tag].update(aggregates) + else: + self.userdata[tag] = AggregatesHints(aggregates) + if "arg-constraints" in hints: tag = "arg-constraints" argconstraints: Dict[str, Dict[str, Dict[str, int]]] = hints[tag] @@ -1727,6 +1826,14 @@ def add_hints(self, hints: Dict[str, Any]) -> None: else: self.userdata[tag] = TrampolinesHints(entries) + if "instruction-annotations" in hints: + tag = "instruction-annotations" + instranns: List[Dict[str, str]] = hints[tag] + if tag in self.userdata: + self.userdata[tag].update(instranns) + else: + self.userdata[tag] = InstructionAnnotationsHints(instranns) + if "non-returning-calls" in hints: tag = "non-returning-calls" nrcalls: Dict[str, List[str]] = hints[tag]