arch/arm32_binaries

Define a set predicates to abstract from ARM32 specific instruction set and characteristics

thumb_sym(Name:symbol)

Mapping symbol names from elf: e.g., $t, $a, $d, etc.

See https://sourceware.org/binutils/docs/as/ARM-Mapping-Symbols.htm

arm_sym(Name:symbol)

data_sym(Name:symbol)

movw_movt(EA:address, Reg:register, Val:number, Operation:symbol)

Either movw r, #N or movt r, #N

movw_movt_pair(EA_movw:address, EA_movt:address, Value:number)

E.g., EA_movw: movw reg, N

EA_movt: movt reg, M

=> reg’s Value = N | (M << 16)

plt_bx_pc(EA:address, Function:symbol)

E.g.,

bx pc // thumb b.n XXX or nop // thumb add ip, pc, #0, #12 add ip, ip, #16, #20 ldr pc, [ip, #2640]

plt_entry_arm_candidate(EA_entry:address, EA_jump:address, Function:symbol, EA_reloc:address)

EA_entry: The address of the PLT entry EA_jump: The address of the last jump instruction in the PLT entry Function: The external function that the PLT entry forwards EA_reloc: The destination address of the PLT entry

symbol_minus_symbol_candidate_arm(EA:address, Size:unsigned, Symbol1:address, Symbol2:address, Scale:unsigned, Offset:number)

This rule is shared by init_symbol_minus_symbol_candidate_arm and cinf_symbol_minus_symbol_candidate_arm.

WARNING: Predicate not present in compiled Datalog program (Dead Code)

arm_jump_table_candidate_start(EA_access:address, EA_jump:address, RegIndex:reg_nullable, Reference:address, TableStart:address, EntrySize:unsigned, Type:symbol, Scale:unsigned, Offset:number)

Represents the first entry of an ARM jump table.

Attributes:

  • EA_access: address of instruction that accesses the jump table entries

  • EA_jump: address of jump instruction

  • RegIndex: register used for indexing into the jumptable. May be “NONE” if the index reg is pre-multiplied.

  • Reference: relative base for offsets (if the Type is rel_*, 0 otherwise)

  • TableStart: address of first table entry

  • EntrySize: size of entries

  • Type: “absolute”, “rel_signed”, or “rel_unsigned”

  • Offset: “1” if the jump table pattern requires “+1” for symbol-symbol Thumb targets in symbolic expression

arm_jump_table_candidate(EA_jump:address, Reference:address, TableStart:address, EntryAddr:address, EntrySize:unsigned, TargetAddr:address, TableLimit:address, Type:symbol, Scale:unsigned)

Represents an entry in an ARM jump table.

Attributes:

  • EA_jump: address of jump instruction

  • Reference: relative base for offsets (if the Type is rel_*, 0 otherwise)

  • TableStart: address of first table entry

  • EntryAddr: address of table entry

  • EntrySize: size of entries

  • TargetAddr: resolved target of the jump

  • TableLimit: first address that cannot be part of the jump table

  • Type: “absolute”, “rel_signed”, or “rel_unsigned”

arm_jump_table_data_block_limit(EA_jmp:address, TableStart:address, Limit:address)

Addresses at which jump table data blocks should be split

litpool_ref(EA:address, EA_ldr:address, RefAddr:address, Offset:unsigned, Size:unsigned, OpIndex:operand_index)

Instruction at address EA accesses a literal pool located at LitPoolAddr

EA: EA of the instruction containing the literal-pool label.

Note that for ADR/LDR case, EA is the address of ADR. For other cases, EA is the address of the load instruction.

EA_ldr: EA of the load instruction that actually accesses the literal pool

EA = EA_ldr for non-ADR/LDR case

RefAddr: The address of referenced label Offset: This is for handling the ADR/LDR case:

adr BaseReg, Label ldr Reg, [BaseReg, Offset]

For other cases, Offset is 0. The actual literal pool address would be RefAddr + Offset.

Size: The whole size of the literal pool entry accessed by the instruction

at EA_ldr: E.g., 1 for LDRB

2 for LDRH 4 for LDR 8 for LDRD 8 for VLDR N*4 for LDM R, {R1,…,RN}

OpIndex: The index of operand for literal-pool label.

E.g., 1 for LDR, 2 for LDRD, 1 for ADR