From ada2f9e6fc8a6c5211a82886e88c96068ad0286b Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 22 Jul 2026 11:37:04 -0700 Subject: [PATCH 01/20] USER: add wide-op aggregates to userdata --- chb/userdata/UserHints.py | 109 +++++++++++++++++++++++++++++++++++++- 1 file changed, 108 insertions(+), 1 deletion(-) 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] From 0e255ff00360e43f9b7104fb1cbd36ea1947c063 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 24 Jul 2026 17:01:30 -0700 Subject: [PATCH 02/20] CMD: simple command to retrieve predicated instructions --- chb/cmdline/chkx | 5 +++++ chb/cmdline/commandutil.py | 35 +++++++++++++++++++++++++++++++++++ 2 files changed, 40 insertions(+) diff --git a/chb/cmdline/chkx b/chb/cmdline/chkx index 45414529..67c25ec8 100755 --- a/chb/cmdline/chkx +++ b/chb/cmdline/chkx @@ -1109,6 +1109,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..348b0dd9 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 @@ -1677,6 +1678,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.""" From 1623a397271a96590680da5dca5831113d0664da Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 24 Jul 2026 17:02:37 -0700 Subject: [PATCH 03/20] ARM:xdata support for arm aggregates --- chb/app/InstrXData.py | 22 +- chb/arm/ARMInstruction.py | 2 +- chb/arm/opcodes/ARMAdd.py | 2 +- chb/arm/opcodes/ARMAddCarry.py | 126 ++++++++++- chb/arm/opcodes/ARMMove.py | 69 +++++- chb/arm/opcodes/ARMReverseSubtractCarry.py | 232 ++++++++++++++++++++- chb/arm/opcodes/ARMStoreRegisterDual.py | 13 +- chb/arm/opcodes/ARMSubtractCarry.py | 130 +++++++++++- 8 files changed, 581 insertions(+), 15 deletions(-) diff --git a/chb/app/InstrXData.py b/chb/app/InstrXData.py index b7ba00cd..79b999db 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 @@ -671,6 +671,26 @@ 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_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_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/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/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..f8a8f844 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 @@ -81,11 +81,48 @@ class ARMAddCarryXData(ARMOpcodeXData): rdefs[0]: xrn rdefs[1:]: reaching definitions for xxrn + + Aggregate: ARMWideAdd + + - variables + 0: vrdlo + 1: vrdhi + + - expressions + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + 4: rresult + 5: rresultlo + 6: rresulthi + 7: xxrnlo + 8: xxrnhi + 9: xxrmlo + 10: xxrmhi + 11: xxrn_w + 12: xxrm_w + + - c exressions + 0: cresult_w + 1: cresultlo + 2: cresulthi + + rdefs: + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + """ 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 +191,94 @@ def rn_rdef(self) -> Optional["ReachingDefFact"]: def rm_rdef(self) -> Optional["ReachingDefFact"]: return self._xdata.reachingdefs[1] + # Wide add aggregate + + @property + def vrdlo(self) -> "XVariable": + return self.var(0, "vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.var(1, "vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.xpr(0, "xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.xpr(1, "xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.xpr(2, "xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.xpr(3, "xrmhi") + + @property + def rresult_w(self) -> "XXpr": + return self.xpr(4, "rresult") + + @property + def rresultlo(self) -> "XXpr": + return self.xpr(5, "rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.xpr(6, "rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.xpr(7, "xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.xpr(8, "xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.xpr(9, "xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.xpr(10, "xxrmhi") + + @property + def xxrn_w(self) -> "XXpr": + return self.xpr(11, "xxrn_w") + + @property + def xxrm_w(self) -> "XXpr": + return self.xpr(12, "xxrm_w") + + @property + def cresult_w(self) -> "XXpr": + return self.cxpr(0, "cresult") + + @property + def is_cresult_w_ok(self) -> bool: + return self.is_cxpr_ok(0) + + @property + def cresultlo(self) -> "XXpr": + return self.cxpr(1, "cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.cxpr(2, "cresulthi") + @property def annotation(self) -> str: - assignment = str(self.vrd) + " := " + self.result_simplified + if self.is_wide_add: + lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" + rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" + rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" + cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" + assignment = lhs + " := " + rhs1 + " + " + rhs2 + cx + else: + assignment = str(self.vrd) + " := " + self.result_simplified return self.add_instruction_condition(assignment) diff --git a/chb/arm/opcodes/ARMMove.py b/chb/arm/opcodes/ARMMove.py index 06d1071c..b0547a91 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,24 @@ class ARMMoveXData(ARMOpcodeXData): - predicate/ternary: 0: p + + Aggregate: WideMove: + + - variables: + 0: vrdlo + 1: vrdhi + + - expressions + 0: xrnlo + 1: xrnhi + 2: xxrnlo + 3: xxrnhi + 4: xxrn + + - c expressions + 0: cresult + 1: cresultlo + 2: cresulthi """ def __init__(self, xdata: InstrXData) -> None: @@ -97,6 +115,14 @@ def __init__(self, xdata: InstrXData) -> None: def vrd(self) -> "XVariable": return self.var(0, "vrd") + @property + def vrdlo(self) -> "XVariable": # agg:widemove + return self.var(0, "vrdlo") + + @property + def vrdhi(self) -> "XVariable": # agg:widemove + return self.var(1, "vrdhi") + @property def is_predicate_assign(self) -> bool: return self.xdata.is_predicate_assignment @@ -113,6 +139,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,6 +155,26 @@ def result(self) -> "XXpr": def is_result_ok(self) -> bool: return self.is_xpr_ok(1) + @property + def xrnlo(self) -> "XXpr": # agg:widemove + return self.xpr(0, "xrnlo") + + @property + def xrnhi(self) -> "XXpr": # agg:widemove + return self.xpr(1, "xrnhi") + + @property + def xxrnlo(self) -> "XXpr": # agg:widemove + return self.xpr(2, "xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": # agg:widemove + return self.xpr(3, "xxrnhi") + + @property + def xxrn(self) -> "XXpr": # agg:widemove + return self.xpr(4, "xxrn") + @property def cresult(self) -> "XXpr": return self.cxpr(0, "cresult") @@ -133,6 +183,14 @@ def cresult(self) -> "XXpr": def is_cresult_ok(self) -> bool: return self.is_cxpr_ok(0) + @property + def cresultlo(self) -> "XXpr": # agg:widemove + return self.cxpr(1, "cresultlo") + + @property + def cresulthi(self) -> "XXpr": # agg:widemove + return self.cxpr(2, "cresulthi") + @property def predicate(self) -> "XXpr": # known to be valid @@ -199,6 +257,13 @@ def ternary_assignment_ann(self) -> str: + ")") return str(self.vrd) + " := " + rhs + cpred + @property + def wide_move_ann(self) -> str: + lhs = "(" + str(self.vrdlo) + ", " + str(self.vrdhi) + ")" + rhs = "(" + str(self.xxrnlo) + ", " + str(self.xxrnhi) + ") = " + str(self.xxrn) + cx = str(self.cresult) + return lhs + " = " + rhs + " (C: " + cx + ")" + @property def annotation(self) -> str: if self.xdata.instruction_is_subsumed(): @@ -207,6 +272,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") + ")" diff --git a/chb/arm/opcodes/ARMReverseSubtractCarry.py b/chb/arm/opcodes/ARMReverseSubtractCarry.py index 08c66e10..81983e51 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,240 @@ # 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 + + Aggregate: ARMWideReverseSubtract + + - variables + 0: vrdlo + 1: vrdhi + + - expressions + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + 4: rresult + 5: rresultlo + 6: rresulthi + 7: xxrnlo + 8: xxrnhi + 9: xxrmlo + 10: xxrmhi + 11: xxrn_w + 12: xxrm_w + + - c exressions + 0: cresult_w + 1: cresultlo + 2: cresulthi + + rdefs: + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + + + """ + + 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 add aggregate + + @property + def vrdlo(self) -> "XVariable": + return self.var(0, "vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.var(1, "vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.xpr(0, "xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.xpr(1, "xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.xpr(2, "xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.xpr(3, "xrmhi") + + @property + def rresult_w(self) -> "XXpr": + return self.xpr(4, "rresult") + + @property + def rresultlo(self) -> "XXpr": + return self.xpr(5, "rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.xpr(6, "rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.xpr(7, "xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.xpr(8, "xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.xpr(9, "xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.xpr(10, "xxrmhi") + + @property + def xxrn_w(self) -> "XXpr": + return self.xpr(11, "xxrn_w") + + @property + def xxrm_w(self) -> "XXpr": + return self.xpr(12, "xxrm_w") + + @property + def cresult_w(self) -> "XXpr": + return self.cxpr(0, "cresult") + + @property + def is_cresult_w_ok(self) -> bool: + return self.is_cxpr_ok(0) + + @property + def cresultlo(self) -> "XXpr": + return self.cxpr(1, "cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.cxpr(2, "cresulthi") + + @property + def annotation(self) -> str: + if self.is_wide_reverse_subtract: + lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" + rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" + rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" + cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" + assignment = lhs + " := " + rhs2 + " - " + rhs1 + 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 +286,15 @@ 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 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..3edfd239 100644 --- a/chb/arm/opcodes/ARMSubtractCarry.py +++ b/chb/arm/opcodes/ARMSubtractCarry.py @@ -49,6 +49,45 @@ class ARMSubtractCarryXData(ARMOpcodeXData): + """ + Aggregate: ARMWideSubtract + + - variables + 0: vrdlo + 1: vrdhi + + - expressions + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + 4: rresult + 5: rresultlo + 6: rresulthi + 7: xxrnlo + 8: xxrnhi + 9: xxrmlo + 10: xxrmhi + + - c exressions + 0: cresult + 1: cresultlo + 2: cresulthi + + rdefs: + 0: xrnlo + 1: xrnhi + 2: xrmlo + 3: xrmhi + + """ + + 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": @@ -75,9 +114,94 @@ 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 vrdlo(self) -> "XVariable": + return self.var(0, "vrdlo") + + @property + def vrdhi(self) -> "XVariable": + return self.var(1, "vrdhi") + + @property + def xrnlo(self) -> "XXpr": + return self.xpr(0, "xrnlo") + + @property + def xrnhi(self) -> "XXpr": + return self.xpr(1, "xrnhi") + + @property + def xrmlo(self) -> "XXpr": + return self.xpr(2, "xrmlo") + + @property + def xrmhi(self) -> "XXpr": + return self.xpr(3, "xrmhi") + + @property + def rresult_w(self) -> "XXpr": + return self.xpr(4, "rresult") + + @property + def rresultlo(self) -> "XXpr": + return self.xpr(5, "rresultlo") + + @property + def rresulthi(self) -> "XXpr": + return self.xpr(6, "rresulthi") + + @property + def xxrnlo(self) -> "XXpr": + return self.xpr(7, "xxrnlo") + + @property + def xxrnhi(self) -> "XXpr": + return self.xpr(8, "xxrnhi") + + @property + def xxrmlo(self) -> "XXpr": + return self.xpr(9, "xxrmlo") + + @property + def xxrmhi(self) -> "XXpr": + return self.xpr(10, "xxrmhi") + + @property + def xxrn_w(self) -> "XXpr": + return self.xpr(11, "xxrn_w") + + @property + def xxrm_w(self) -> "XXpr": + return self.xpr(12, "xxrm_w") + + @property + def cresult_w(self) -> "XXpr": + return self.cxpr(0, "cresult") + + @property + def is_cresult_w_ok(self) -> bool: + return self.is_cxpr_ok(0) + + @property + def cresultlo(self) -> "XXpr": + return self.cxpr(1, "cresultlo") + + @property + def cresulthi(self) -> "XXpr": + return self.cxpr(2, "cresulthi") + @property def annotation(self) -> str: - assignment = str(self.vrd) + " := " + self.result_simplified + if self.is_wide_subtract: + lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" + rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" + rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" + cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" + assignment = lhs + " := " + rhs1 + " - " + rhs2 + cx + else: + assignment = str(self.vrd) + " := " + self.result_simplified return self.add_instruction_condition(assignment) @@ -103,6 +227,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 "" From 629235329f2ec1a5f89aba0b1b49cd4326e1a1b4 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 30 Jul 2026 00:34:29 -0700 Subject: [PATCH 04/20] CMD: add command-line switch for float-abi hard/soft --- chb/cmdline/AnalysisManager.py | 8 ++++++++ chb/cmdline/chkx | 4 ++++ chb/cmdline/commandutil.py | 2 ++ 3 files changed, 14 insertions(+) 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 67c25ec8..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, diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index 348b0dd9..0a9d696a 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -405,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 @@ -563,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: From 71309b399d8a51f108538029175ef431ca45709f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 30 Jul 2026 00:36:32 -0700 Subject: [PATCH 05/20] AST:ARM: add more double-registers --- chb/ast/ASTNode.py | 4 ++-- chb/ast/CustomASTSupport.py | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) 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..f8bf7af0 100644 --- a/chb/ast/CustomASTSupport.py +++ b/chb/ast/CustomASTSupport.py @@ -37,7 +37,10 @@ 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 floating point / adv simd registers arm_fp_sp_register_sizes: Dict[str, int] = { From bdc6ceae817c22ba908f14f474f4e27a219d3178 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 30 Jul 2026 00:37:35 -0700 Subject: [PATCH 06/20] INV: add support for sign-extension operator --- chb/invariants/XXprUtil.py | 3 +++ 1 file changed, 3 insertions(+) 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 " From 07ab003875b93cf59b80e84a5948bb74b0737538 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 30 Jul 2026 00:39:51 -0700 Subject: [PATCH 07/20] XDATA: add support for wide operations --- chb/app/CHVersion.py | 4 ++-- chb/app/InstrXData.py | 40 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 2 deletions(-) diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index a872b4c5..df499605 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-20260729" -minimum_required_chb_version = "0.6.0_20260617" +minimum_required_chb_version = "0.6.0_20260728" diff --git a/chb/app/InstrXData.py b/chb/app/InstrXData.py index 79b999db..6a3cce43 100644 --- a/chb/app/InstrXData.py +++ b/chb/app/InstrXData.py @@ -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 @@ -675,6 +699,10 @@ def is_nondet_ternary_assignment(self) -> bool: 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 @@ -687,6 +715,18 @@ def is_wide_subtract(self) -> bool: 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 From 3e0284ce2890d15af63eb101dfab3b11ddf02148 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 30 Jul 2026 00:43:59 -0700 Subject: [PATCH 08/20] ARM: add xdata accessors for wide operations --- chb/arm/ARMCallOpcode.py | 17 ++++-- chb/arm/ARMOpcode.py | 121 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 132 insertions(+), 6 deletions(-) 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/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() From 758af5f5a6192e587caed4c4d6e8685a9bba4388 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 12:40:25 -0700 Subject: [PATCH 09/20] ARM:add support for wide-and --- chb/arm/opcodes/ARMBitwiseAnd.py | 235 ++++++++++++++++++++++++++++++- 1 file changed, 229 insertions(+), 6 deletions(-) diff --git a/chb/arm/opcodes/ARMBitwiseAnd.py b/chb/arm/opcodes/ARMBitwiseAnd.py index 000ae69c..5e46b103 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,116 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMBitwiseAndXData(xdata) return xd.annotation + def ast_prov_subsumed( + 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.""" + + annotations: List[str] = [iaddr, "AND (subsumed)"] + + # 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) + + rdefs = xdata.reachingdefs + + astree.add_expr_reachingdefs(ll_rhs1, [rdefs[0]]) + astree.add_expr_reachingdefs(ll_rhs2, [rdefs[1]]) + + return ([], [ll_assign]) + + 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) + + rdefs = xdata.reachingdefs + + astree.add_expr_reachingdefs(ll_rhs1, [rdefs[0]]) + astree.add_expr_reachingdefs(ll_rhs2, [rdefs[1]]) + + # 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) + rhs = ll_rhs + + 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(ll_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 +388,23 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: + if xdata.instruction_is_subsumed(): + return self.ast_prov_subsumed(astree, iaddr, bytestring, xdata) + + 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 From 03376b80135ed0502afab2493c09dac275241857 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 13:02:42 -0700 Subject: [PATCH 10/20] ARM: add support for wide-xor --- chb/arm/opcodes/ARMBitwiseAnd.py | 37 +---- chb/arm/opcodes/ARMBitwiseExclusiveOr.py | 186 ++++++++++++++++++++++- 2 files changed, 183 insertions(+), 40 deletions(-) diff --git a/chb/arm/opcodes/ARMBitwiseAnd.py b/chb/arm/opcodes/ARMBitwiseAnd.py index 5e46b103..f3dab5d5 100644 --- a/chb/arm/opcodes/ARMBitwiseAnd.py +++ b/chb/arm/opcodes/ARMBitwiseAnd.py @@ -270,38 +270,6 @@ def annotation(self, xdata: InstrXData) -> str: xd = ARMBitwiseAndXData(xdata) return xd.annotation - def ast_prov_subsumed( - 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.""" - - annotations: List[str] = [iaddr, "AND (subsumed)"] - - # 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) - - rdefs = xdata.reachingdefs - - astree.add_expr_reachingdefs(ll_rhs1, [rdefs[0]]) - astree.add_expr_reachingdefs(ll_rhs2, [rdefs[1]]) - - return ([], [ll_assign]) - def ast_prov_wide_and( self, astree: ASTInterface, @@ -366,7 +334,7 @@ def ast_prov_wide_and( 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(ll_rhs, rdefdoubles) + 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]) @@ -388,9 +356,6 @@ def ast_prov( xdata: InstrXData) -> Tuple[ List[AST.ASTInstruction], List[AST.ASTInstruction]]: - if xdata.instruction_is_subsumed(): - return self.ast_prov_subsumed(astree, iaddr, bytestring, xdata) - xd = ARMBitwiseAndXData(xdata) if xdata.instruction_subsumes(): diff --git a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py index c62d86e8..bcebbd0b 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,70 @@ 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) + + rhs = xd.cresultw if xd.is_cresultw_ok else xd.rresultw + 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, @@ -168,6 +330,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) From fd5db8c58b49c732ee8e55bc236e66f4a50692e2 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 15:18:42 -0700 Subject: [PATCH 11/20] ARM: add support for wide-not --- chb/arm/opcodes/ARMBitwiseAnd.py | 2 +- chb/arm/opcodes/ARMBitwiseExclusiveOr.py | 9 +- chb/arm/opcodes/ARMBitwiseNot.py | 167 ++++++++++++++++++++++- 3 files changed, 174 insertions(+), 4 deletions(-) diff --git a/chb/arm/opcodes/ARMBitwiseAnd.py b/chb/arm/opcodes/ARMBitwiseAnd.py index f3dab5d5..7f28c8f5 100644 --- a/chb/arm/opcodes/ARMBitwiseAnd.py +++ b/chb/arm/opcodes/ARMBitwiseAnd.py @@ -311,7 +311,7 @@ def ast_prov_wide_and( chklogger.logger.warning( "AND: Encountered error value for wide-and rhs at address %s", iaddr) - rhs = ll_rhs + return ([], [ll_assign]) lhs = xd.vrdlohi rdefdoubles = xdata.reachingdefdoubles diff --git a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py index bcebbd0b..0f8c70f5 100644 --- a/chb/arm/opcodes/ARMBitwiseExclusiveOr.py +++ b/chb/arm/opcodes/ARMBitwiseExclusiveOr.py @@ -284,8 +284,15 @@ def ast_prov_wide_xor( xd = ARMBitwiseExclusiveOrXData(xdata) - rhs = xd.cresultw if xd.is_cresultw_ok else xd.rresultw 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 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) From 57b34c62cb8a0ccf76312725b7f1a4010a16aacf Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 15:25:34 -0700 Subject: [PATCH 12/20] ARM: add support for wide-or --- chb/arm/opcodes/ARMBitwiseOr.py | 196 ++++++++++++++++++++++++++++++-- 1 file changed, 188 insertions(+), 8 deletions(-) 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 From c0f083618994ea693e6a8b8e4f9d161151e5469b Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 15:33:01 -0700 Subject: [PATCH 13/20] ARM: add support for wide-add --- chb/arm/opcodes/ARMAddCarry.py | 178 +++++++++++++++++++++------------ 1 file changed, 114 insertions(+), 64 deletions(-) diff --git a/chb/arm/opcodes/ARMAddCarry.py b/chb/arm/opcodes/ARMAddCarry.py index f8a8f844..11bc8516 100644 --- a/chb/arm/opcodes/ARMAddCarry.py +++ b/chb/arm/opcodes/ARMAddCarry.py @@ -81,39 +81,6 @@ class ARMAddCarryXData(ARMOpcodeXData): rdefs[0]: xrn rdefs[1:]: reaching definitions for xxrn - - Aggregate: ARMWideAdd - - - variables - 0: vrdlo - 1: vrdhi - - - expressions - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - 4: rresult - 5: rresultlo - 6: rresulthi - 7: xxrnlo - 8: xxrnhi - 9: xxrmlo - 10: xxrmhi - 11: xxrn_w - 12: xxrm_w - - - c exressions - 0: cresult_w - 1: cresultlo - 2: cresulthi - - rdefs: - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - """ def __init__(self, xdata: InstrXData) -> None: @@ -193,90 +160,97 @@ def rm_rdef(self) -> Optional["ReachingDefFact"]: # Wide add aggregate + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + @property def vrdlo(self) -> "XVariable": - return self.var(0, "vrdlo") + return self.binary_wopvar("vrdlo") @property def vrdhi(self) -> "XVariable": - return self.var(1, "vrdhi") + return self.binary_wopvar("vrdhi") @property def xrnlo(self) -> "XXpr": - return self.xpr(0, "xrnlo") + return self.binary_wopxpr("xrnlo") @property def xrnhi(self) -> "XXpr": - return self.xpr(1, "xrnhi") + return self.binary_wopxpr("xrnhi") @property def xrmlo(self) -> "XXpr": - return self.xpr(2, "xrmlo") + return self.binary_wopxpr("xrmlo") @property def xrmhi(self) -> "XXpr": - return self.xpr(3, "xrmhi") + return self.binary_wopxpr("xrmhi") @property - def rresult_w(self) -> "XXpr": - return self.xpr(4, "rresult") + 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.xpr(5, "rresultlo") + return self.binary_wopxpr("rresultlo") @property def rresulthi(self) -> "XXpr": - return self.xpr(6, "rresulthi") + return self.binary_wopxpr("rresulthi") @property def xxrnlo(self) -> "XXpr": - return self.xpr(7, "xxrnlo") + return self.binary_wopxpr("xxrnlo") @property def xxrnhi(self) -> "XXpr": - return self.xpr(8, "xxrnhi") + return self.binary_wopxpr("xxrnhi") @property def xxrmlo(self) -> "XXpr": - return self.xpr(9, "xxrmlo") + return self.binary_wopxpr("xxrmlo") @property def xxrmhi(self) -> "XXpr": - return self.xpr(10, "xxrmhi") + return self.binary_wopxpr("xxrmhi") @property - def xxrn_w(self) -> "XXpr": - return self.xpr(11, "xxrn_w") + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") @property - def xxrm_w(self) -> "XXpr": - return self.xpr(12, "xxrm_w") + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") @property - def cresult_w(self) -> "XXpr": - return self.cxpr(0, "cresult") + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") @property - def is_cresult_w_ok(self) -> bool: - return self.is_cxpr_ok(0) + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") @property def cresultlo(self) -> "XXpr": - return self.cxpr(1, "cresultlo") + return self.binary_wopcxpr("cresultlo") @property def cresulthi(self) -> "XXpr": - return self.cxpr(2, "cresulthi") + return self.binary_wopcxpr("cresulthi") @property def annotation(self) -> str: if self.is_wide_add: - lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" - rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" - rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" - cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" - assignment = lhs + " := " + rhs1 + " + " + rhs2 + cx + 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) @@ -334,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(ll_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, @@ -342,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 @@ -370,8 +422,6 @@ def has_cast() -> bool: 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: rhs = xd.cresult xrhs = xd.rresult From a6f3c1cea6ac366e4011090005b64f350e5f6ce0 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 16:17:57 -0700 Subject: [PATCH 14/20] ARM: add support for wide-reverse-subtract --- chb/arm/opcodes/ARMAddCarry.py | 2 +- chb/arm/opcodes/ARMReverseSubtractCarry.py | 249 +++++++++++++++------ 2 files changed, 186 insertions(+), 65 deletions(-) diff --git a/chb/arm/opcodes/ARMAddCarry.py b/chb/arm/opcodes/ARMAddCarry.py index 11bc8516..2026c4ac 100644 --- a/chb/arm/opcodes/ARMAddCarry.py +++ b/chb/arm/opcodes/ARMAddCarry.py @@ -366,7 +366,7 @@ def ast_prov_wide_add( 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(ll_rhs, rdefdoubles) + astree.add_expr_reachingdefs(hl_rhs, rdefdoubles) astree.add_lval_defuses(hl_lhs, defusedoubles[0]) astree.add_lval_defuses_high(hl_lhs, defuseshigh[0]) diff --git a/chb/arm/opcodes/ARMReverseSubtractCarry.py b/chb/arm/opcodes/ARMReverseSubtractCarry.py index 81983e51..fc4400e0 100644 --- a/chb/arm/opcodes/ARMReverseSubtractCarry.py +++ b/chb/arm/opcodes/ARMReverseSubtractCarry.py @@ -62,40 +62,6 @@ class ARMReverseSubtractCarryXData(ARMOpcodeXData): - c expressions: 0: cresult - - Aggregate: ARMWideReverseSubtract - - - variables - 0: vrdlo - 1: vrdhi - - - expressions - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - 4: rresult - 5: rresultlo - 6: rresulthi - 7: xxrnlo - 8: xxrnhi - 9: xxrmlo - 10: xxrmhi - 11: xxrn_w - 12: xxrm_w - - - c exressions - 0: cresult_w - 1: cresultlo - 2: cresulthi - - rdefs: - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - - """ def __init__(self, xdata: InstrXData) -> None: @@ -165,92 +131,99 @@ def xxrm(self) -> "XXpr": def is_xxrm_ok(self) -> bool: return self.is_xpr_ok(5) - # Wide add aggregate + # Wide reverse subtract aggregate + + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") @property def vrdlo(self) -> "XVariable": - return self.var(0, "vrdlo") + return self.binary_wopvar("vrdlo") @property def vrdhi(self) -> "XVariable": - return self.var(1, "vrdhi") + return self.binary_wopvar("vrdhi") @property def xrnlo(self) -> "XXpr": - return self.xpr(0, "xrnlo") + return self.binary_wopxpr("xrnlo") @property def xrnhi(self) -> "XXpr": - return self.xpr(1, "xrnhi") + return self.binary_wopxpr("xrnhi") @property def xrmlo(self) -> "XXpr": - return self.xpr(2, "xrmlo") + return self.binary_wopxpr("xrmlo") @property def xrmhi(self) -> "XXpr": - return self.xpr(3, "xrmhi") + return self.binary_wopxpr("xrmhi") @property - def rresult_w(self) -> "XXpr": - return self.xpr(4, "rresult") + 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.xpr(5, "rresultlo") + return self.binary_wopxpr("rresultlo") @property def rresulthi(self) -> "XXpr": - return self.xpr(6, "rresulthi") + return self.binary_wopxpr("rresulthi") @property def xxrnlo(self) -> "XXpr": - return self.xpr(7, "xxrnlo") + return self.binary_wopxpr("xxrnlo") @property def xxrnhi(self) -> "XXpr": - return self.xpr(8, "xxrnhi") + return self.binary_wopxpr("xxrnhi") @property def xxrmlo(self) -> "XXpr": - return self.xpr(9, "xxrmlo") + return self.binary_wopxpr("xxrmlo") @property def xxrmhi(self) -> "XXpr": - return self.xpr(10, "xxrmhi") + return self.binary_wopxpr("xxrmhi") @property - def xxrn_w(self) -> "XXpr": - return self.xpr(11, "xxrn_w") + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") @property - def xxrm_w(self) -> "XXpr": - return self.xpr(12, "xxrm_w") + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") @property - def cresult_w(self) -> "XXpr": - return self.cxpr(0, "cresult") + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") @property - def is_cresult_w_ok(self) -> bool: - return self.is_cxpr_ok(0) + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") @property def cresultlo(self) -> "XXpr": - return self.cxpr(1, "cresultlo") + return self.binary_wopcxpr("cresultlo") @property def cresulthi(self) -> "XXpr": - return self.cxpr(2, "cresulthi") + return self.binary_wopcxpr("cresulthi") @property def annotation(self) -> str: if self.is_wide_reverse_subtract: - lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" - rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" - rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" - cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" - assignment = lhs + " := " + rhs2 + " - " + rhs1 + cx + 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) @@ -298,3 +271,151 @@ def mnemonic_extension(self) -> str: def annotation(self, xdata: InstrXData) -> str: 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]) From 26f5612267e347f52cce618a720656976c229be8 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 16:41:47 -0700 Subject: [PATCH 15/20] ARM: add support for wide-subtract --- chb/arm/opcodes/ARMAddCarry.py | 17 +-- chb/arm/opcodes/ARMSubtractCarry.py | 212 ++++++++++++++++++---------- 2 files changed, 142 insertions(+), 87 deletions(-) diff --git a/chb/arm/opcodes/ARMAddCarry.py b/chb/arm/opcodes/ARMAddCarry.py index 2026c4ac..2cf89ad1 100644 --- a/chb/arm/opcodes/ARMAddCarry.py +++ b/chb/arm/opcodes/ARMAddCarry.py @@ -417,33 +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()) - - 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/ARMSubtractCarry.py b/chb/arm/opcodes/ARMSubtractCarry.py index 3edfd239..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 @@ -49,38 +49,6 @@ class ARMSubtractCarryXData(ARMOpcodeXData): - """ - Aggregate: ARMWideSubtract - - - variables - 0: vrdlo - 1: vrdhi - - - expressions - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - 4: rresult - 5: rresultlo - 6: rresulthi - 7: xxrnlo - 8: xxrnhi - 9: xxrmlo - 10: xxrmhi - - - c exressions - 0: cresult - 1: cresultlo - 2: cresulthi - - rdefs: - 0: xrnlo - 1: xrnhi - 2: xrmlo - 3: xrmhi - - """ def __init__(self, xdata: InstrXData) -> None: ARMOpcodeXData.__init__(self, xdata) @@ -109,6 +77,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( @@ -116,90 +96,97 @@ def result_simplified(self) -> str: # Wide subtract aggregate + @property + def vrdlohi(self) -> "XVariable": + return self.binary_wopvar("vrdlohi") + @property def vrdlo(self) -> "XVariable": - return self.var(0, "vrdlo") + return self.binary_wopvar("vrdlo") @property def vrdhi(self) -> "XVariable": - return self.var(1, "vrdhi") + return self.binary_wopvar("vrdhi") @property def xrnlo(self) -> "XXpr": - return self.xpr(0, "xrnlo") + return self.binary_wopxpr("xrnlo") @property def xrnhi(self) -> "XXpr": - return self.xpr(1, "xrnhi") + return self.binary_wopxpr("xrnhi") @property def xrmlo(self) -> "XXpr": - return self.xpr(2, "xrmlo") + return self.binary_wopxpr("xrmlo") @property def xrmhi(self) -> "XXpr": - return self.xpr(3, "xrmhi") + return self.binary_wopxpr("xrmhi") + + @property + def rresultw(self) -> "XXpr": + return self.binary_wopxpr("rresultw") @property - def rresult_w(self) -> "XXpr": - return self.xpr(4, "rresult") + def is_rresultw_ok(self) -> bool: + return self.is_binary_wopxpr_ok("rresultw") @property def rresultlo(self) -> "XXpr": - return self.xpr(5, "rresultlo") + return self.binary_wopxpr("rresultlo") @property def rresulthi(self) -> "XXpr": - return self.xpr(6, "rresulthi") + return self.binary_wopxpr("rresulthi") @property def xxrnlo(self) -> "XXpr": - return self.xpr(7, "xxrnlo") + return self.binary_wopxpr("xxrnlo") @property def xxrnhi(self) -> "XXpr": - return self.xpr(8, "xxrnhi") + return self.binary_wopxpr("xxrnhi") @property def xxrmlo(self) -> "XXpr": - return self.xpr(9, "xxrmlo") + return self.binary_wopxpr("xxrmlo") @property def xxrmhi(self) -> "XXpr": - return self.xpr(10, "xxrmhi") + return self.binary_wopxpr("xxrmhi") @property - def xxrn_w(self) -> "XXpr": - return self.xpr(11, "xxrn_w") + def xxrnw(self) -> "XXpr": + return self.binary_wopxpr("xxrnw") @property - def xxrm_w(self) -> "XXpr": - return self.xpr(12, "xxrm_w") + def xxrmw(self) -> "XXpr": + return self.binary_wopxpr("xxrmw") @property - def cresult_w(self) -> "XXpr": - return self.cxpr(0, "cresult") + def cresultw(self) -> "XXpr": + return self.binary_wopcxpr("cresultw") @property - def is_cresult_w_ok(self) -> bool: - return self.is_cxpr_ok(0) + def is_cresultw_ok(self) -> bool: + return self.is_binary_wopcxpr_ok("cresultw") @property def cresultlo(self) -> "XXpr": - return self.cxpr(1, "cresultlo") + return self.binary_wopcxpr("cresultlo") @property def cresulthi(self) -> "XXpr": - return self.cxpr(2, "cresulthi") + return self.binary_wopcxpr("cresulthi") @property def annotation(self) -> str: if self.is_wide_subtract: - lhs = "(" + str(self.vrdhi) + ", " + str(self.vrdlo) + ")" - rhs1 = "(" + str(self.xxrnhi) + ", " + str(self.xxrnlo) + ")" - rhs2 = "(" + str(self.xxrmhi) + ", " + str(self.xxrmlo) + ")" - cx = " (C: " + (str(self.cresult_w) if self.is_cresult_w_ok else "None") + ")" - assignment = lhs + " := " + rhs1 + " - " + rhs2 + cx + 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) @@ -248,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, @@ -256,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 @@ -279,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, @@ -312,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]) From 452cc094393366d9c69c71d53f8cd75d61e17d47 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 16:56:45 -0700 Subject: [PATCH 16/20] ARM: add support for wide-move --- chb/arm/opcodes/ARMMove.py | 161 ++++++++++++++++++++++++------------- 1 file changed, 105 insertions(+), 56 deletions(-) diff --git a/chb/arm/opcodes/ARMMove.py b/chb/arm/opcodes/ARMMove.py index b0547a91..7e154c14 100644 --- a/chb/arm/opcodes/ARMMove.py +++ b/chb/arm/opcodes/ARMMove.py @@ -89,23 +89,6 @@ class ARMMoveXData(ARMOpcodeXData): - predicate/ternary: 0: p - Aggregate: WideMove: - - - variables: - 0: vrdlo - 1: vrdhi - - - expressions - 0: xrnlo - 1: xrnhi - 2: xxrnlo - 3: xxrnhi - 4: xxrn - - - c expressions - 0: cresult - 1: cresultlo - 2: cresulthi """ def __init__(self, xdata: InstrXData) -> None: @@ -116,12 +99,16 @@ def vrd(self) -> "XVariable": return self.var(0, "vrd") @property - def vrdlo(self) -> "XVariable": # agg:widemove - return self.var(0, "vrdlo") + def vrdlohi(self) -> "XVariable": + return self.unary_wopvar("vrdlohi") + + @property + def vrdlo(self) -> "XVariable": + return self.unary_wopvar("vrdlo") @property - def vrdhi(self) -> "XVariable": # agg:widemove - return self.var(1, "vrdhi") + def vrdhi(self) -> "XVariable": + return self.unary_wopvar("vrdhi") @property def is_predicate_assign(self) -> bool: @@ -156,40 +143,64 @@ def is_result_ok(self) -> bool: return self.is_xpr_ok(1) @property - def xrnlo(self) -> "XXpr": # agg:widemove - return self.xpr(0, "xrnlo") + 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 xrnhi(self) -> "XXpr": # agg:widemove - return self.xpr(1, "xrnhi") + def rresulthi(self) -> "XXpr": + return self.unary_wopxpr("rresulthi") @property - def xxrnlo(self) -> "XXpr": # agg:widemove - return self.xpr(2, "xxrnlo") + def xxrnlo(self) -> "XXpr": + return self.unary_wopxpr("xxrnlo") @property - def xxrnhi(self) -> "XXpr": # agg:widemove - return self.xpr(3, "xxrnhi") + def xxrnhi(self) -> "XXpr": + return self.unary_wopxpr("xxrnhi") @property - def xxrn(self) -> "XXpr": # agg:widemove - return self.xpr(4, "xxrn") + 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 cresultlo(self) -> "XXpr": # agg:widemove - return self.cxpr(1, "cresultlo") + 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": # agg:widemove - return self.cxpr(2, "cresulthi") + def cresulthi(self) -> "XXpr": + return self.unary_wopcxpr("cresulthi") @property def predicate(self) -> "XXpr": @@ -259,9 +270,9 @@ def ternary_assignment_ann(self) -> str: @property def wide_move_ann(self) -> str: - lhs = "(" + str(self.vrdlo) + ", " + str(self.vrdhi) + ")" - rhs = "(" + str(self.xxrnlo) + ", " + str(self.xxrnhi) + ") = " + str(self.xxrn) - cx = str(self.cresult) + 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 @@ -346,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 - astree.add_expr_reachingdefs(ll_rhs_f, rdefs) + xd = ARMMoveXData(xdata) - return ([], [ll_assign]) + 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]) + + 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]) def ast_prov_predicate_assign( self, @@ -431,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]) @@ -533,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(): @@ -547,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 " From c1e385d1143fde8e95faa5d0d3a0a754c49faba5 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 17:48:21 -0700 Subject: [PATCH 17/20] ARM: add support for wide-LDRD --- chb/arm/opcodes/ARMLoadRegisterDual.py | 91 +++++++++++++++++++++++--- 1 file changed, 83 insertions(+), 8 deletions(-) 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) From c3da5541237a650d1c501a3781cf9fd41e2fb5a9 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 18:23:54 -0700 Subject: [PATCH 18/20] AST: add more arm double-registers --- chb/ast/CustomASTSupport.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/chb/ast/CustomASTSupport.py b/chb/ast/CustomASTSupport.py index f8bf7af0..ffb524ee 100644 --- a/chb/ast/CustomASTSupport.py +++ b/chb/ast/CustomASTSupport.py @@ -41,6 +41,8 @@ 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] = { From d2865157b16dcb652b8106d1fa42080d4dacc4b5 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 18:24:34 -0700 Subject: [PATCH 19/20] ARM: add wide-op support for SMULL, UMULL --- chb/arm/opcodes/ARMLoadRegisterSignedByte.py | 4 +- chb/arm/opcodes/ARMSignedMultiplyLong.py | 94 +++++++-------- chb/arm/opcodes/ARMUnsignedMultiplyLong.py | 117 +++++++------------ 3 files changed, 91 insertions(+), 124 deletions(-) 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/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/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]) From 0d3d40bca26034a3229fa0d5855a4cc0fcce4bb3 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 2 Aug 2026 23:56:36 -0700 Subject: [PATCH 20/20] CHB:ARM: fix BitwiseAnd --- chb/app/CHVersion.py | 4 ++-- chb/arm/opcodes/ARMBitwiseAnd.py | 5 ----- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index df499605..31856ce1 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ -chbversion: str = "0.3.0-20260729" +chbversion: str = "0.3.0-20260802" -minimum_required_chb_version = "0.6.0_20260728" +minimum_required_chb_version = "0.6.0_20260802" diff --git a/chb/arm/opcodes/ARMBitwiseAnd.py b/chb/arm/opcodes/ARMBitwiseAnd.py index 7f28c8f5..a676af9f 100644 --- a/chb/arm/opcodes/ARMBitwiseAnd.py +++ b/chb/arm/opcodes/ARMBitwiseAnd.py @@ -294,11 +294,6 @@ def ast_prov_wide_and( bytestring=bytestring, annotations=annotations) - rdefs = xdata.reachingdefs - - astree.add_expr_reachingdefs(ll_rhs1, [rdefs[0]]) - astree.add_expr_reachingdefs(ll_rhs2, [rdefs[1]]) - # high-level assignment xd = ARMBitwiseAndXData(xdata)