diff --git a/chb/app/BasicBlock.py b/chb/app/BasicBlock.py index 933e8823..023433cb 100644 --- a/chb/app/BasicBlock.py +++ b/chb/app/BasicBlock.py @@ -336,6 +336,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: ... diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index 8f57922e..6f4ed84a 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1 +1 @@ -chbversion: str = "0.3.0-20250714" +chbversion: str = "0.3.0-20250722" diff --git a/chb/app/Function.py b/chb/app/Function.py index 77fc74ab..e251135b 100644 --- a/chb/app/Function.py +++ b/chb/app/Function.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -604,6 +604,7 @@ def to_string( opcodewidth: int = 25, # alignment width for opcode text sp: bool = True, proofobligations: bool = False, + typingrules: bool = False, stacklayout: bool = False) -> str: ... diff --git a/chb/app/Instruction.py b/chb/app/Instruction.py index 97a4308d..b2ff2ec0 100644 --- a/chb/app/Instruction.py +++ b/chb/app/Instruction.py @@ -345,6 +345,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: ... diff --git a/chb/arm/ARMBlock.py b/chb/arm/ARMBlock.py index 1018cd86..9039753d 100644 --- a/chb/arm/ARMBlock.py +++ b/chb/arm/ARMBlock.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -41,6 +41,7 @@ from chb.invariants.XXpr import XXpr if TYPE_CHECKING: + from chb.app.AppAccess import AppAccess from chb.arm.ARMFunction import ARMFunction @@ -55,6 +56,10 @@ def __init__(self, armf: "ARMFunction", xnode: ET.Element) -> None: def armfunction(self) -> "ARMFunction": return self._armf + @property + def app(self) -> "AppAccess": + return self.armfunction.app + @property def armdictionary(self) -> ARMDictionary: return self.armfunction.armdictionary @@ -74,6 +79,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 40, + typingrules: bool = False, sp: bool = True) -> str: lines: List[str] = [] for (ia, instr) in sorted(self.instructions.items()): @@ -81,6 +87,7 @@ def to_string( bytes=bytes, opcodetxt=opcodetxt, opcodewidth=opcodewidth, + typingrules=typingrules, sp=sp) lines.append(str(ia).rjust(10) + " " + pinstr) return "\n".join(lines) diff --git a/chb/arm/ARMFunction.py b/chb/arm/ARMFunction.py index 847af644..87e55cf6 100644 --- a/chb/arm/ARMFunction.py +++ b/chb/arm/ARMFunction.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -59,6 +59,7 @@ import chb.util.fileutil as UF if TYPE_CHECKING: + from chb.app.AppAccess import AppAccess from chb.cmdline.PatchResults import PatchEvent @@ -93,6 +94,10 @@ def __init__( def armdictionary(self) -> ARMDictionary: return self._armd + @property + def app(self) -> "AppAccess": + return self.armdictionary.app + @property def armfunctiondictionary(self) -> FunctionDictionary: if self._armfnd is None: @@ -289,6 +294,7 @@ def to_string( opcodewidth: int = 40, sp: bool = True, proofobligations: bool = False, + typingrules: bool = False, stacklayout: bool = False) -> str: lines: List[str] = [] if stacklayout: @@ -311,6 +317,7 @@ def to_string( bytes=bytes, opcodetxt=opcodetxt, opcodewidth=opcodewidth, + typingrules=typingrules, sp=sp)) lines.append("-" * 80) if self.has_jumptable(self.blocks[b].lastaddr): diff --git a/chb/arm/ARMInstruction.py b/chb/arm/ARMInstruction.py index 5eadeb3c..3230106c 100644 --- a/chb/arm/ARMInstruction.py +++ b/chb/arm/ARMInstruction.py @@ -61,6 +61,7 @@ if TYPE_CHECKING: + from chb.app.AppAccess import AppAccess from chb.arm.ARMBlock import ARMBlock from chb.arm.ARMFunction import ARMFunction from chb.arm.ARMJumpTable import ARMJumpTable @@ -88,6 +89,10 @@ def armfunction(self) -> "ARMFunction": def armdictionary(self) -> ARMDictionary: return self.armblock.armdictionary + @property + def app(self) -> "AppAccess": + return self.armfunction.app + @property def armfunctiondictionary(self) -> "FunctionDictionary": return self.armfunction.armfunctiondictionary @@ -434,13 +439,24 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 40, + typingrules: bool = False, sp: bool = False) -> str: + if typingrules: + lines: List[str] = [] + rulesapplied = self.app.type_constraints.rules_applied_to_instruction( + self.armfunction.faddr, self.iaddr) + for r in sorted(str(r) for r in rulesapplied): + lines.append(" " + str(r)) try: pbytes = self.bytestring.ljust(10) + " " if bytes else "" pesp = str(self.stackpointer_offset) + " " if sp else "" popcode = ( self.opcodetext.ljust(opcodewidth) if opcodetxt else "") - return pesp + pbytes + popcode + self.annotation + codeline = pesp + pbytes + popcode + self.annotation + if len(lines) > 0: + return codeline + "\n " + "\n ".join(lines) + else: + return codeline except Exception as e: print( "Error in instruction: " diff --git a/chb/arm/ARMOperand.py b/chb/arm/ARMOperand.py index 361c4646..d544eac0 100644 --- a/chb/arm/ARMOperand.py +++ b/chb/arm/ARMOperand.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -109,16 +109,22 @@ def offset(self) -> int: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: - return self.opkind.ast_lvalue(astree) + return self.opkind.ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring, vtype=vtype) def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: - return self.opkind.ast_rvalue(astree) + return self.opkind.ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring, vtype=vtype) def __str__(self) -> str: return str(self.opkind) diff --git a/chb/arm/ARMOperandKind.py b/chb/arm/ARMOperandKind.py index 6a2716ee..2b9d9168 100644 --- a/chb/arm/ARMOperandKind.py +++ b/chb/arm/ARMOperandKind.py @@ -184,6 +184,8 @@ def scale_factor(self) -> Optional[int]: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError( @@ -196,6 +198,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError( @@ -230,6 +234,8 @@ def is_register(self) -> bool: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -238,6 +244,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -277,6 +285,8 @@ def name(self) -> str: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -285,6 +295,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -318,6 +330,8 @@ def is_special_register(self) -> bool: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -326,6 +340,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -378,6 +394,8 @@ def index(self) -> int: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -388,6 +406,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -456,6 +476,8 @@ def name(self) -> str: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -464,6 +486,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return ( @@ -597,6 +621,8 @@ def scale_factor(self) -> Optional[int]: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError( @@ -605,6 +631,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: srt = self.shift_rotate @@ -688,6 +716,8 @@ def width(self) -> int: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError( @@ -696,6 +726,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: """ @@ -741,6 +773,8 @@ def is_absolute(self) -> bool: def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return (astree.mk_integer_constant(self.address.get_int()), [], []) @@ -765,6 +799,8 @@ def address(self) -> "AsmAddress": def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: gvname = "gv_" + self.address.get_hex() @@ -854,6 +890,8 @@ def is_index(self) -> bool: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: offset = self.memory_offset.ast_rvalue(astree) @@ -864,7 +902,8 @@ def ast_lvalue( if self.is_write_back: reglv = astree.mk_variable_lval(self.register) - assign = astree.mk_assign(reglv, xindex) + assign = astree.mk_assign( + reglv, xindex, iaddr=iaddr, bytestring=bytestring) if self.is_index: memexp = astree.mk_memref_lval(xindex) return (memexp, [], [assign]) @@ -878,6 +917,8 @@ def ast_lvalue( def ast_addr_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> AST.ASTExpr: xreg = astree.mk_register_variable_expr(self.register, vtype=vtype) offset = self.memory_offset.ast_rvalue(astree) @@ -889,9 +930,12 @@ def ast_addr_rvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: - (lval, preinstrs, postinstrs) = self.ast_lvalue(astree, vtype=vtype) + (lval, preinstrs, postinstrs) = self.ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring, vtype=vtype) rval = astree.mk_lval_expr(lval) return (rval, preinstrs, postinstrs) @@ -940,6 +984,8 @@ def is_immediate(self) -> bool: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError("Immediate operand cannot be an lvalue") @@ -947,6 +993,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return (astree.mk_integer_constant(self.value), [], []) @@ -978,6 +1026,8 @@ def is_fp_constant(self) -> bool: def ast_lvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTLval, List[AST.ASTInstruction], List[AST.ASTInstruction]]: raise UF.CHBError("Floating point constant cannot be an lvalue") @@ -985,6 +1035,8 @@ def ast_lvalue( def ast_rvalue( self, astree: ASTInterface, + iaddr: Optional[str] = None, + bytestring: Optional[str] = None, vtype: Optional[AST.ASTTyp] = None) -> Tuple[ AST.ASTExpr, List[AST.ASTInstruction], List[AST.ASTInstruction]]: return (astree.mk_float_constant(self.floatvalue), [], []) diff --git a/chb/arm/opcodes/ARMBranch.py b/chb/arm/opcodes/ARMBranch.py index 9cd452bb..8e2d149f 100644 --- a/chb/arm/opcodes/ARMBranch.py +++ b/chb/arm/opcodes/ARMBranch.py @@ -263,6 +263,9 @@ def return_value(self, xdata: InstrXData) -> Optional[XXpr]: return None def annotation(self, xdata: InstrXData) -> str: + if self.is_call_instruction(xdata) and xdata.has_call_target(): + return ARMCallOpcode.annotation(self, xdata) + xd = ARMBranchXData(xdata) if xd.is_ok: if self.is_call_instruction(xdata): diff --git a/chb/arm/opcodes/ARMLoadRegister.py b/chb/arm/opcodes/ARMLoadRegister.py index 8c979e96..965f8d3d 100644 --- a/chb/arm/opcodes/ARMLoadRegister.py +++ b/chb/arm/opcodes/ARMLoadRegister.py @@ -232,7 +232,8 @@ def ast_prov( # low-level assignment - (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue(astree) + (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) @@ -318,8 +319,10 @@ def has_cast() -> bool: if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMLoadRegisterByte.py b/chb/arm/opcodes/ARMLoadRegisterByte.py index 9d11095d..ebe843aa 100644 --- a/chb/arm/opcodes/ARMLoadRegisterByte.py +++ b/chb/arm/opcodes/ARMLoadRegisterByte.py @@ -233,7 +233,8 @@ def ast_prov( # low-level assignment - (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue(astree) + (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) @@ -310,8 +311,10 @@ def has_cast() -> bool: if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMLoadRegisterDual.py b/chb/arm/opcodes/ARMLoadRegisterDual.py index 55a1224f..7cfb29c9 100644 --- a/chb/arm/opcodes/ARMLoadRegisterDual.py +++ b/chb/arm/opcodes/ARMLoadRegisterDual.py @@ -236,7 +236,8 @@ def ast_prov( # low-level assignments - (ll_rhs1, ll_pre1, ll_post1) = self.opargs[4].ast_rvalue(astree) + (ll_rhs1, ll_pre1, ll_post1) = self.opargs[4].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_lhs1, _, _) = self.opargs[0].ast_lvalue(astree) ll_assign1 = astree.mk_assign( @@ -246,7 +247,8 @@ def ast_prov( bytestring=bytestring, annotations=annotations) - (ll_rhs2, ll_pre2, ll_post2) = self.opargs[5].ast_rvalue(astree) + (ll_rhs2, ll_pre2, ll_post2) = self.opargs[5].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_lhs2, _, _) = self.opargs[1].ast_lvalue(astree) ll_assign2 = astree.mk_assign( diff --git a/chb/arm/opcodes/ARMLoadRegisterHalfword.py b/chb/arm/opcodes/ARMLoadRegisterHalfword.py index e56e699e..cad1f962 100644 --- a/chb/arm/opcodes/ARMLoadRegisterHalfword.py +++ b/chb/arm/opcodes/ARMLoadRegisterHalfword.py @@ -227,7 +227,8 @@ def ast_prov( # low-level assignment - (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue(astree) + (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) @@ -310,8 +311,10 @@ def has_cast() -> bool: if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMLoadRegisterSignedByte.py b/chb/arm/opcodes/ARMLoadRegisterSignedByte.py index 39be28c7..581f4e8a 100644 --- a/chb/arm/opcodes/ARMLoadRegisterSignedByte.py +++ b/chb/arm/opcodes/ARMLoadRegisterSignedByte.py @@ -155,7 +155,8 @@ def ast_prov( # low-level assignment - (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue(astree) + (ll_rhs, ll_pre, ll_post) = self.opargs[3].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) @@ -217,8 +218,10 @@ def ast_prov( if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMLoadRegisterSignedHalfword.py b/chb/arm/opcodes/ARMLoadRegisterSignedHalfword.py index 569203d6..1d234801 100644 --- a/chb/arm/opcodes/ARMLoadRegisterSignedHalfword.py +++ b/chb/arm/opcodes/ARMLoadRegisterSignedHalfword.py @@ -160,7 +160,8 @@ def ast_prov( annotations: List[str] = [iaddr, "LDRSH"] - (ll_rhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_rvalue(astree) + (ll_rhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) (ll_op1, _, _) = self.opargs[1].ast_rvalue(astree) (ll_op2, _, _) = self.opargs[2].ast_rvalue(astree) (ll_lhs, _, _) = self.opargs[0].ast_lvalue(astree) @@ -218,8 +219,10 @@ def ast_prov( if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMStoreRegister.py b/chb/arm/opcodes/ARMStoreRegister.py index e5e59dbe..a91f2c4c 100644 --- a/chb/arm/opcodes/ARMStoreRegister.py +++ b/chb/arm/opcodes/ARMStoreRegister.py @@ -266,8 +266,10 @@ def ast_prov( # low-level assignment - (ll_rhs, _, _) = self.opargs[0].ast_rvalue(astree) - (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue(astree) + (ll_rhs, _, _) = self.opargs[0].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_assign = astree.mk_assign( ll_lhs, ll_rhs, @@ -353,8 +355,10 @@ def ast_prov( if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMStoreRegisterByte.py b/chb/arm/opcodes/ARMStoreRegisterByte.py index 3a9be3f4..7dccc74d 100644 --- a/chb/arm/opcodes/ARMStoreRegisterByte.py +++ b/chb/arm/opcodes/ARMStoreRegisterByte.py @@ -233,8 +233,10 @@ def ast_prov( # low-level assignment - (ll_rhs, _, _) = self.opargs[0].ast_rvalue(astree) - (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue(astree) + (ll_rhs, _, _) = self.opargs[0].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_assign = astree.mk_assign( ll_lhs, ll_rhs, @@ -313,8 +315,10 @@ def ast_prov( if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/arm/opcodes/ARMStoreRegisterDual.py b/chb/arm/opcodes/ARMStoreRegisterDual.py index f757b148..8e8f49c4 100644 --- a/chb/arm/opcodes/ARMStoreRegisterDual.py +++ b/chb/arm/opcodes/ARMStoreRegisterDual.py @@ -243,10 +243,14 @@ def ast_prov( # low-level assignments - (ll_rhs1, _, _) = self.opargs[0].ast_rvalue(astree) - (ll_rhs2, _, _) = self.opargs[1].ast_rvalue(astree) - (ll_lhs1, ll_pre1, ll_post1) = self.opargs[4].ast_lvalue(astree) - (ll_lhs2, ll_pre2, ll_post2) = self.opargs[5].ast_lvalue(astree) + (ll_rhs1, _, _) = self.opargs[0].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_rhs2, _, _) = self.opargs[1].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_lhs1, ll_pre1, ll_post1) = self.opargs[4].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_lhs2, ll_pre2, ll_post2) = self.opargs[5].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_assign1 = astree.mk_assign( ll_lhs1, diff --git a/chb/arm/opcodes/ARMStoreRegisterHalfword.py b/chb/arm/opcodes/ARMStoreRegisterHalfword.py index 4b35015f..36cfab96 100644 --- a/chb/arm/opcodes/ARMStoreRegisterHalfword.py +++ b/chb/arm/opcodes/ARMStoreRegisterHalfword.py @@ -234,8 +234,10 @@ def ast_prov( # low-level assignment - (ll_rhs, _, _) = self.opargs[0].ast_rvalue(astree) - (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue(astree) + (ll_rhs, _, _) = self.opargs[0].ast_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) + (ll_lhs, ll_preinstrs, ll_postinstrs) = self.opargs[3].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_assign = astree.mk_assign( ll_lhs, ll_rhs, @@ -317,8 +319,10 @@ def ast_prov( if self.opargs[3].is_indirect_register and self.opargs[3].is_write_back: addrop = cast("ARMOffsetAddressOp", self.opargs[3].opkind) - (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue(astree) - ll_addr_rhs = addrop.ast_addr_rvalue(astree) + (ll_addr_lhs, _, _) = self.opargs[1].ast_lvalue( + astree, iaddr=iaddr, bytestring=bytestring) + ll_addr_rhs = addrop.ast_addr_rvalue( + astree, iaddr=iaddr, bytestring=bytestring) ll_addr_assign = astree.mk_assign( ll_addr_lhs, diff --git a/chb/ast/ASTDeserializer.py b/chb/ast/ASTDeserializer.py index b7c92e70..0b16d4b4 100644 --- a/chb/ast/ASTDeserializer.py +++ b/chb/ast/ASTDeserializer.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2022-2024 Aarno Labs LLC +# Copyright (c) 2022-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -289,7 +289,7 @@ def _initialize_function_prototype( astree.set_function_prototype(fprototype) else: raise Exception( - "Index for prototype " + "Deserializer: Index for prototype " + str(index) + " not found in nodes deserialized") @@ -332,25 +332,23 @@ def _initialize_provenance(self, fdata: Dict[str, Any]) -> None: spans = fdata["spans"] rds = prov["reaching-definitions"] - def find_expr_by_id(nodes: Dict[int, AST.ASTNode], exprid: int) -> AST.ASTNode: + def find_expr_by_id( + nodes: Dict[int, AST.ASTNode], exprid: int) -> AST.ASTNode: for node in fdata["ast"]["nodes"]: if "exprid" in node and int(node["exprid"]) == exprid: return nodes[int(node["id"])] else: raise Exception( - "Exprid: " - + str(exprid) - + " not found") + "Deserializer: Exprid: " + str(exprid) + " not found") - def find_instr_by_id(nodes: Dict[int, AST.ASTNode], instrid: int) -> AST.ASTNode: + def find_instr_by_id( + nodes: Dict[int, AST.ASTNode], instrid: int) -> AST.ASTNode: for node in fdata["ast"]["nodes"]: if "instrid" in node and int(node["instrid"]) == instrid: return nodes[int(node["id"])] else: raise Exception( - "Instrid: " - + str(instrid) - + " not found") + "Deserializer: Instrid: " + str(instrid) + " not found") def find_instr_address_by_locationid(locationid: int) -> str: for node in fdata["spans"]: @@ -366,21 +364,37 @@ def find_expr_address_by_exprid(exprid: int) -> str: return node["spans"][0]["base_va"] else: raise Exception( - "No span found for exprid: " + str(exprid)) + "Deserializer: No span found for exprid: " + str(exprid)) result: List[Tuple[str, List[str]]] = [] for (exprid, instrids) in rds.items(): exprnode = find_expr_by_id(nodes, int(exprid)) p_instrs: List[str] = [] for instrid in instrids: - instrnode = cast(AST.ASTInstruction, find_instr_by_id(nodes, instrid)) try: - address = find_instr_address_by_locationid(instrnode.locationid) + instrnode = cast( + AST.ASTInstruction, find_instr_by_id(nodes, instrid)) + except Exception as e: + raise Exception( + "Deserializer: instrnode for instrid " + + str(instrid) + + " and exprid " + + str(exprid) + + " not found") + try: + address = find_instr_address_by_locationid( + instrnode.locationid) except Exception as e: p_instrs.append(str(instrnode) + ": " + str(e)) address = "?" p_instrs.append( - " <" + str(instrid) + "> " + str(instrnode) + " (" + address + ")") + " <" + + str(instrid) + + "> " + + str(instrnode) + + " (" + + address + + ")") result.append((str(exprnode), p_instrs)) self._reachingdefinitions[faddr] = result diff --git a/chb/ast/ASTViewer.py b/chb/ast/ASTViewer.py index 42bbbddd..70f12d38 100644 --- a/chb/ast/ASTViewer.py +++ b/chb/ast/ASTViewer.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -250,7 +250,7 @@ def instr_span(self, instr: AST.ASTInstruction) -> str: if locationid in self.astree.spanmap(): span = self.astree.spanmap()[locationid] else: - span = "?" + span = "?(locationid:" + str(locationid) + ")" return "\\n" + span def visit_assign_instr(self, instr: AST.ASTAssign) -> None: diff --git a/chb/astinterface/ASTIProvenance.py b/chb/astinterface/ASTIProvenance.py index b3d930c4..d3c1c607 100644 --- a/chb/astinterface/ASTIProvenance.py +++ b/chb/astinterface/ASTIProvenance.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2022-2024 Aarno Labs LLC +# Copyright (c) 2022-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -351,6 +351,8 @@ def has_active_lval_defuse_high(self, lvalid: int) -> bool: if lvalid in self.lval_defuses_high: defuseshigh = self.lval_defuses_high[lvalid] locations = [str(x) for x in defuseshigh.uselocations] + if "exit" in locations: + locations.remove("exit") inactivated = self.defuses_high_inactivated_for(lvalid) active = set(locations).difference(inactivated) return len(active) > 0 diff --git a/chb/astinterface/ASTInterfaceBasicBlock.py b/chb/astinterface/ASTInterfaceBasicBlock.py index 809be1a2..eace028a 100644 --- a/chb/astinterface/ASTInterfaceBasicBlock.py +++ b/chb/astinterface/ASTInterfaceBasicBlock.py @@ -92,11 +92,40 @@ def trampoline_payload_roles(self) -> List[str]: @property def instructions(self) -> Dict[str, ASTInterfaceInstruction]: + """Main access to ast representation of instructions. + + The ASTInterfaceInstruction provides both the high-level and + low-level representation of an instruction. It is important + to have only one of these per instruction, because the high-level + and low-level representation are created together, and in the + process the relationship between the high-level and low-level + is recorded in the AbstractSyntaxTree/Provenance data structure. + + If another instruction is created separately (e.g., to only + obtain the high-level or low-level representation), this + relationship may be corrupted. + + Thus, this function should be the only one to create + ASTInterfaceInstruction's. + """ if len(self._instructions) == 0: for (iaddr, instr) in self.basicblock.instructions.items(): self._instructions[iaddr] = ASTInterfaceInstruction(instr) return self._instructions + def has_instruction(self, iaddr: str) -> bool: + return iaddr in self.instructions + + def get_instruction(self, iaddr: str) -> ASTInterfaceInstruction: + if self.has_instruction(iaddr): + return self.instructions[iaddr] + else: + raise UF.CHBError( + "No instruction found at address " + + iaddr + + " in basic block " + + self.basicblock.baddr) + @property def trampoline_instructions( self) -> Dict[str, Dict[str, ASTInterfaceInstruction]]: @@ -171,8 +200,8 @@ def assembly_ast(self, astree: "ASTInterface") -> AST.ASTStmt: def ast_fragment( self, astree: "ASTInterface", frag: "BasicBlockFragment") -> AST.ASTStmt: if frag.is_predicated: - theninstrs = [ASTInterfaceInstruction(i) for i in frag.thenbranch] - elseinstrs = [ASTInterfaceInstruction(i) for i in frag.elsebranch] + theninstrs = [self.get_instruction(i.iaddr) for i in frag.thenbranch] + elseinstrs = [self.get_instruction(i.iaddr) for i in frag.elsebranch] thenstmt = self.linear_block_ast(astree, theninstrs) elsestmt = self.linear_block_ast(astree, elseinstrs) cinstr = theninstrs[0] @@ -187,7 +216,7 @@ def ast_fragment( brcond.exprid, cinstr.iaddr, cinstr.bytestring) return astree.mk_branch(brcond, thenstmt, elsestmt, "0x0") else: - instrs = [ASTInterfaceInstruction(i) for i in frag.linear] + instrs = [self.get_instruction(i.iaddr) for i in frag.linear] return self.linear_ast(astree, instrs) def fragmented_ast(self, astree: "ASTInterface") -> AST.ASTStmt: diff --git a/chb/bctypes/TypeConstraintStore.py b/chb/bctypes/TypeConstraintStore.py index a3d6b903..94161112 100644 --- a/chb/bctypes/TypeConstraintStore.py +++ b/chb/bctypes/TypeConstraintStore.py @@ -24,11 +24,14 @@ # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE # SOFTWARE. # ------------------------------------------------------------------------------ +import xml.etree.ElementTree as ET from typing import cast, Dict, List, Optional, Set, TYPE_CHECKING import chb.bctypes.TypeConstraint as TC +import chb.util.fileutil as UF + if TYPE_CHECKING: from chb.app.AppAccess import AppAccess @@ -231,18 +234,96 @@ def __str__(self) -> str: return "\n".join(lines) +class TypingRule: + + def __init__(self, tcstore: "TypeConstraintStore", xr: ET.Element) -> None: + self._tcstore = tcstore + self._xr = xr + + @property + def tcstore(self) -> "TypeConstraintStore": + return self._tcstore + + @property + def app(self) -> "AppAccess": + return self.tcstore.app + + @property + def iaddr(self) -> str: + return self._xr.get("loc", "0x0") + + @property + def rulename(self) -> str: + return self._xr.get("rule", "?") + + @property + def typeconstraint(self) -> TC.TypeConstraint: + ix = self._xr.get("tc-ix") + if ix is not None: + return self.app.tcdictionary.type_constraint(int(ix)) + else: + raise UF.CHBError("Type constraint without tc index") + + def __str__(self) -> str: + ix = self._xr.get("tc-ix") + return self.rulename + " " + str(ix) + ":" + str(self.typeconstraint) + + class TypeConstraintStore: + """Global store for type constraints. + + Note: The use of this object is currently somewhat conflicted. It was + originally intended for global use, to recover function signatures for + an entire binary. More recently, however, it has been mainly used to + perform type construction for all local variables (registers and stack) + within individual functions to support lifting. This latest use in its + present form does not scale to an entire binary. For now the scaling + issue is solved by resetting the store after each function, which + essentially means that the store, when saved, only holds the constraints + for a single function (the latest processed). + """ def __init__(self, app: "AppAccess") -> None: self._app = app self._constraints: Optional[List[TC.TypeConstraint]] = None self._functionconstraints: Dict[str, FunctionTypeConstraints] = {} self._functionregconstraints: Dict[str, FunctionRegisterConstraints] = {} + self._rules_applied: Optional[Dict[str, Dict[str, List[TypingRule]]]] = None @property def app(self) -> "AppAccess": return self._app + @property + def rules_applied(self) -> Dict[str, Dict[str, List[TypingRule]]]: + if self._rules_applied is None: + self._rules_applied = {} + tcstore = UF.get_typeconstraint_store_xnode( + self.app.path, self.app.filename) + if tcstore is not None: + rules = tcstore.find("rules-applied") + if rules is not None: + for xf in rules.findall("function"): + faddr = xf.get("faddr", "0x0") + self._rules_applied[faddr] = {} + for xr in xf.findall("rule"): + rule = TypingRule(self, xr) + self._rules_applied[faddr].setdefault(rule.iaddr, []) + self._rules_applied[faddr][rule.iaddr].append(rule) + + return self._rules_applied + + def rules_applied_to_instruction( + self, faddr: str, iaddr: str) -> List[TypingRule]: + result: List[TypingRule] = [] + if faddr in self.rules_applied: + if iaddr in self.rules_applied[faddr]: + for r in self.rules_applied[faddr][iaddr]: + if r.typeconstraint.is_var_constraint: + continue + result.append(r) + return result + @property def constraints(self) -> List[TC.TypeConstraint]: if self._constraints is None: diff --git a/chb/cmdline/chkx b/chb/cmdline/chkx index 2309085f..3947584f 100755 --- a/chb/cmdline/chkx +++ b/chb/cmdline/chkx @@ -953,6 +953,10 @@ def parse() -> argparse.Namespace: "--proofobligations", action="store_true", help="include proofobligations at the top of the function") + resultsfunction.add_argument( + "--typingrules", + action="store_true", + help="include typing rules applied after each instruction") resultsfunction.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index d6662554..ce93ab68 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -1099,6 +1099,7 @@ def results_function(args: argparse.Namespace) -> NoReturn: txtoutput: bool = not xjson stacklayout: bool = args.stacklayout proofobligations: bool = args.proofobligations + typingrules: bool = args.typingrules loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -1161,6 +1162,7 @@ def results_function(args: argparse.Namespace) -> NoReturn: sp=True, opcodetxt=True, proofobligations=proofobligations, + typingrules=typingrules, stacklayout=stacklayout, opcodewidth=opcodewidth)) except UF.CHBError as e: diff --git a/chb/mips/MIPSBlock.py b/chb/mips/MIPSBlock.py index 1108be7a..d86ed7f1 100644 --- a/chb/mips/MIPSBlock.py +++ b/chb/mips/MIPSBlock.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020 Henny Sipma -# Copyright (c) 2021-2022 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -140,6 +140,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: lines: List[str] = [] for (ia, instr) in sorted(self.instructions.items()): diff --git a/chb/mips/MIPSFunction.py b/chb/mips/MIPSFunction.py index 1482a8eb..daf9eee2 100644 --- a/chb/mips/MIPSFunction.py +++ b/chb/mips/MIPSFunction.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020-2021 Henny Sipma -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -340,6 +340,7 @@ def to_string( opcodewidth: int = 25, sp: bool = True, proofobligations: bool = False, + typingrules: bool = False, stacklayout: bool = False) -> str: lines: List[str] = [] if stacklayout: diff --git a/chb/mips/MIPSInstruction.py b/chb/mips/MIPSInstruction.py index ca7a906b..54fbdb2b 100644 --- a/chb/mips/MIPSInstruction.py +++ b/chb/mips/MIPSInstruction.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020-2021 Henny Sipma -# Copyright (c) 2021-2023 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -361,6 +361,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: pbytes = self.bytestring + " " if bytes else "" pesp = str(self.stackpointer_offset) + ' ' if sp else '' diff --git a/chb/pwr/PowerBlock.py b/chb/pwr/PowerBlock.py index e10437e8..872f9040 100644 --- a/chb/pwr/PowerBlock.py +++ b/chb/pwr/PowerBlock.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023 Aarno Labs LLC +# Copyright (c) 2023-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -72,6 +72,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 40, + typingrules: bool = False, sp: bool = True) -> str: lines: List[str] = [] for (ia, instr) in sorted(self.instructions.items()): diff --git a/chb/pwr/PowerFunction.py b/chb/pwr/PowerFunction.py index a45bf987..c7f5e2ba 100644 --- a/chb/pwr/PowerFunction.py +++ b/chb/pwr/PowerFunction.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023 Aarno Labs LLC +# Copyright (c) 2023-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -182,6 +182,7 @@ def to_string( opcodewidth: int = 40, sp: bool = True, proofobligations: bool = False, + typingrules: bool = False, stacklayout: bool = False) -> str: lines: List[str] = [] if stacklayout: diff --git a/chb/pwr/PowerInstruction.py b/chb/pwr/PowerInstruction.py index 159b01a1..74b78f95 100644 --- a/chb/pwr/PowerInstruction.py +++ b/chb/pwr/PowerInstruction.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023 Aarno Labs LLC +# Copyright (c) 2023-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -239,6 +239,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 40, + typingrules: bool = False, sp: bool = False) -> str: try: pbytes = self.bytestring.ljust(10) + " " if bytes else "" diff --git a/chb/userdata/UserHints.py b/chb/userdata/UserHints.py index 472e143f..33867586 100644 --- a/chb/userdata/UserHints.py +++ b/chb/userdata/UserHints.py @@ -591,6 +591,53 @@ def __str__(self) -> str: + (("; typename: " + self.typename) if self.typename else "")) +class TypingRule: + + def __init__(self, d: Dict[str, Any]) -> None: + self._d = d + + @property + def typingrule(self) -> Dict[str, Any]: + return self._d + + @property + def action(self) -> str: + a = self.typingrule.get("action", "?") + if a in ["enable", "disable"]: + return a + else: + raise UF.CHBError("Action in typing rule not recognized: " + a) + + @property + def locs(self) -> List[str]: + locs = self.typingrule.get("locs", []) + if len(locs) == 0: + raise UF.CHBError("No locations specified in typing rule") + else: + return locs + + @property + def name(self) -> str: + if "name" in self.typingrule: + return self.typingrule["name"] + else: + raise UF.CHBError("Name is missing in typing rule") + + def to_xml(self, node: ET.Element) -> None: + xtyrule = ET.Element("typingrule") + node.append(xtyrule) + xtyrule.set("name", self.name) + xtyrule.set("action", self.action) + xtyrule.set("locs", ",".join(self.locs)) + + def __str__(self) -> str: + return ( + "action: " + self.action + + "; locs: [" + ", ".join(self.locs) + "]" + + "; name: " + self.name) + + + class FunctionAnnotation: def __init__(self, fnannotation: Dict[str, Any]) -> None: @@ -623,6 +670,14 @@ def register_variable_introductions(self) -> Dict[str, RegisterVarIntro]: result[rvi.iaddr] = rvi return result + @property + def typingrules(self) -> List[TypingRule]: + result: List[TypingRule] = [] + for d in self.fnannotation.get("typing-rules", []): + tr = TypingRule(d) + result.append(tr) + return result + def has_register_variable_introduction(self, iaddr: str) -> bool: return iaddr in self.register_variable_introductions @@ -654,6 +709,11 @@ def to_xml(self, node: ET.Element) -> None: node.append(xregintros) for rvintro in self.register_variable_introductions.values(): rvintro.to_xml(xregintros) + if len(self.typingrules) > 0: + xtypingrules = ET.Element("typing-rules") + node.append(xtypingrules) + for tr in self.typingrules: + tr.to_xml(xtypingrules) def __str__(self) -> str: lines: List[str] = [] diff --git a/chb/util/fileutil.py b/chb/util/fileutil.py index 181e20e1..4720eb10 100644 --- a/chb/util/fileutil.py +++ b/chb/util/fileutil.py @@ -5,7 +5,7 @@ # The MIT License (MIT) # # Copyright (c) 2016-2020 Kestrel Technology LLC -# Copyright (c) 2021-2024 Aarno Labs LLC +# Copyright (c) 2021-2025 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -562,6 +562,24 @@ def get_tcdictionary_xnode(path: str, xfile: str) -> ET.Element: return get_chb_xnode(filename, "type-constraint-dictionary") +def get_typeconstraint_store_filename(path: str, xfile: str) -> str: + fdir = get_results_dir(path, xfile) + return get_chb_filename(fdir, xfile, "tcstore.xml") + + +def has_typeconstraint_store_file(path: str, xfile: str) -> bool: + filename = get_typeconstraint_store_filename(path, xfile) + return os.path.isfile(filename) + + +def get_typeconstraint_store_xnode(path: str, xfile: str) -> Optional[ET.Element]: + if has_typeconstraint_store_file(path, xfile): + filename = get_typeconstraint_store_filename(path, xfile) + return get_chb_xnode(filename, "type-constraint-store") + else: + return None + + def get_bcdictionary_filename(path: str, xfile: str) -> str: fdir = get_analysis_dir(path, xfile) return get_chb_filename(fdir, xfile, "bcdict.xml") diff --git a/chb/x86/X86Block.py b/chb/x86/X86Block.py index d2292b85..ca04e74e 100644 --- a/chb/x86/X86Block.py +++ b/chb/x86/X86Block.py @@ -5,7 +5,7 @@ # The MIT License (MIT) # # Copyright (c) 2016-2020 Kestrel Technology LLC -# Copyrigth (c) 2021-2023 Aarno Labs, LLC +# Copyrigth (c) 2021-2025 Aarno Labs, LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -114,6 +114,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: lines: List[str] = [] for (ia, instr) in sorted( diff --git a/chb/x86/X86Function.py b/chb/x86/X86Function.py index 5e34e4cc..a5ce767f 100644 --- a/chb/x86/X86Function.py +++ b/chb/x86/X86Function.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020 Henny Sipma -# Copyright (c) 2021-2023 Aarno Labs, LLC +# Copyright (c) 2021-2025 Aarno Labs, LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -439,6 +439,7 @@ def to_string( opcodewidth: int = 25, sp: bool = True, proofobligations: bool = False, + typingrules: bool = False, stacklayout: bool = False) -> str: lines: List[str] = [] for b in sorted(self.blocks, key=lambda b:int(b, 16)): diff --git a/chb/x86/X86Instruction.py b/chb/x86/X86Instruction.py index b11b9a38..8d51892b 100644 --- a/chb/x86/X86Instruction.py +++ b/chb/x86/X86Instruction.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020 Henny Sipma -# Copyright (c) 2021-2023 Aarno Labs, LLC +# Copyright (c) 2021-2025 Aarno Labs, LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -384,6 +384,7 @@ def to_string( bytes: bool = False, opcodetxt: bool = True, opcodewidth: int = 25, + typingrules: bool = False, sp: bool = True) -> str: pesp = str(self.stackpointer_offset) + ' ' if sp else '' pbytes = self.bytestring.ljust(20) if bytes else ''