elf_binaries

elf_section_type(Name:symbol, Code:unsigned)

This module defines predicates and rules specific of ELF binaries

Used by: data_section, function_pointer_section

elf_pointer_array_section_type(SectionTypeName:symbol)

ELF section types that contain an array of code pointers.

Used by: function_pointer_section

plt_section(name:symbol)

got_section(name:symbol)

plt_entry(EA:address, function:symbol)

There is a PLT jump at address ‘EA’ to external function ‘Function’.

Uses: arch.jump, arch.load_operation, arch.reg_arithmetic_operation, best_ifunc_symbol, got_reference_pointer, hi_load, indirect_jump, instruction, instruction_get_op, instruction_get_src_op, loaded_section, next, op_indirect, op_indirect_mapped, op_regdirect_contains_reg, pc_relative_jump, plt_entry_arm_candidate, plt_entry_candidate, plt_section, reg_jump, relocation, symbol

Used by: resolved_transfer, resolved_transfer_to_symbol

Recursive: unresolved_block, litpool_ref, negative_block_heuristic, reg_def_use.used, contains_implausible_instr_seq, padding_block_candidate, block_instruction_next, arm_jump_table_candidate_start, block_candidate_boundaries, impossible_block, arch.reg_relative_load, wis_schedule, reg_has_base_image, split_load_conflict, possible_target_from, wis_has_prior, straight_line_def_used, __agg_subclause6, init_symbol_minus_symbol_candidate_arm, base_relative_operation, straight_line_last_def, unresolved_interval_order, stack_def_use.live_var_used, unresolved_block_overlap, reg_def_use.ambiguous_block_last_def, correlated_live_reg, litpool_symbolic_operand, data_in_code_propagate, split_load_point, relative_address, __agg_subclause3, cmp_reg_to_reg, plt_block, compare_and_jump_indirect_op_valid, data_block_candidate, reg_def_use.live_var_at_prior_used, no_return_call, split_load_operand, common_tail, no_return_call_refined, value_reg_unsupported, cinf_ldr_add_pc, stack_def_use.last_def_in_block, next_start, block_points_proportional, tls_desc_call, code_in_block, reg_def_use.live_var_used, data_in_code, split_load_for_symbolization, incomplete_block, base_relative_jump, unlikely_have_symbolic_immediate, base_relative_operand, arm_jump_table_candidate, jump_table_candidate_refined, split_load_total_points, next_block_in_byte_interval, discarded_block, reg_def_use.return_val_used, adrp_used, indefinite_litpool_ref, reg_def_use.live_var_def, relative_address_start, reg_def_use.ref_in_block, block_points, arch.extend_load, block_boundaries, data_access, candidate_block_is_padding, instruction_memory_access_size, function_inference.function_entry_initial, indexed_pc_relative_load, wis_schedule_iter, init_ldr_add_pc, call_tls_get_addr, unresolved_interval, data_block_limit, segment_target_range, const_value_reg_used, __agg_single2, compare_and_jump_register, is_padding, jump_table_start, relocation_adjustment_total, stack_def_use.live_var_def, cmp_defines, after_end, reg_has_got, overlap_with_litpool, no_return_call_propagated, invalid, invalid_jump_table_candidate, data_segment, inter_procedural_edge, block_last_instruction, must_fallthrough, padding_block_limit, block_limit, wis_prior, block_overlap, symbol_minus_symbol_litpool_access_pattern, arm_jump_table_block_start, no_return_block, initialized_data_segment, branch_to_calculated_pc_rel_addr, litpool_boundaries, jump_table_target, arm_jump_table_cmp_limit, stack_def_use.block_last_def, no_value_reg_limit, block_heuristic, reg_used_for, possible_target, reg_def_use.live_var_at_block_end, hi_load_prop, indexed_pc_relative_load_relative, relocation_adjustment, arm_jump_table_data_block, composite_data_access, code_in_block_candidate_refined, tls_get_addr, value_reg_edge, value_reg, __agg_subclause7, known_block, resolved_reaches, block, block_next, gp_relative_operand, jump_table_signed, symbolic_expr_from_relocation, reg_def_use.block_last_def, __agg_subclause2, likely_fallthrough, last_value_reg_limit, reg_def_use.flow_def, split_load_candidate, jump_table_max, __agg_single3, jump_table_candidate, compare_and_jump_indirect, block_implies_block, reg_def_use.def_used, reg_reg_arithmetic_operation_defs, next_type, self_contained_segment, arch.simple_data_load, block_total_points, def_used_for_address, relative_jump_table_entry_candidate, may_fallthrough, basic_target, candidate_block_is_not_padding, reg_def_use.last_def_in_block, wis_memo, block_candidate_dependency_edge, stack_def_use.used_in_block, stack_base_reg_move, inferred_main_dispatch, reg_def_use.defined_in_block, stack_def_use.def_used, code_in_block_candidate, overlapping_instruction, arm_jump_table_block_instruction, first_block_in_byte_interval, jump_table_prelude, arm_jump_table_skip_first_entry, contains_plausible_instr_seq, stack_def_use.ref_in_block, transition_block_limit, inferred_main_in_reg, reg_def_use.ambiguous_last_def_in_block, next_end, stack_def_use.live_var_at_block_end, discarded_split_load, simple_data_access_pattern, start_function, got_relative_operand, value_reg_limit, adjusts_stack_in_block, split_load, arm_jump_table_data_block_limit, flags_and_jump_pair, stack_def_use.live_var_used_in_block, litpool_confidence, reg_def_use.used_in_block, jump_table_element_access, __agg_single6, stack_def_use.defined_in_block, stack_def_use.live_var_at_prior_used, plt_entry, reg_def_use.return_block_end, nop_in_padding_candidate, compare_and_jump_immediate

get_pc_thunk(EA:address, Reg:register)

cie_entry(CieAddr: address, Length:unsigned, CodeAlignmentFactor:unsigned, DataAlignmentFactor:number)

A CIE can be associated to multiple FDEs and it contains information common to all of them. ‘CieAddr’ uniquely identifies the CIE.

Used by: cfi_directive, fde_instruction_ref, last_fde, moved_pc_relative_candidate, symbol_minus_symbol

cie_encoding(CieAddr: address, FdeEncoding:unsigned, LsdaEncoding:unsigned)

cie_encoding complements cie_entry and defines the encodings of the pointers in the FDEs and in the LSDAs associated to this CIE.

Used by: cfi_directive, symbol_minus_symbol, symbol_special_encoding, symbolic_data

cie_personality(CieAddr:address, Personality:address, PersonalityPos:address, PersonalitySize:unsigned, Encoding:unsigned)

The personality routine associated to a CIE entry. This is the procedure that takes care of unwinding the stack and exceptions. For C++ it is typically: ‘__gxx_personality_v0’.

Used by: cfi_directive, labeled_ea, symbol_special_encoding, symbolic_data

fde_entry(FdeAddr: address, Length:unsigned, Cie:address, Start:address, End:address, Lsda:address)

A FDE entry defines how stack unwinding is done in a region of code from ‘start’ to ‘end’. Each FDE points to a parent CIE that contains properties common to multiple FDEs. ‘FdeAddr’ and ‘Length’ determine the location of the FDE entry in the eh_frame section. A FDE entry can have ‘Lsda’ associated that contains exception handling information.

Used by: cfi_directive, endproc_local_index, fde_addresses, fde_block_addresses, fde_instruction_ref, labeled_ea, last_fde, moved_pc_relative_candidate, symbol_minus_symbol, symbol_special_encoding, symbolic_data

fde_pointer_locations(addr:address, startLocation:address, endLocation:address, endSize:unsigned, lsdaLocation:address, lsdaSize:unsigned)

Ancillary predicate that specifies the actual locations of the symbolic expressions in the FDE entry.

Used by: symbol_minus_symbol, symbol_special_encoding, symbolic_data

fde_instruction(FdeAddr:address, Index:unsigned, Size:unsigned, InsnAddr:address, Insn:symbol, Op1:number, Op2:number)

The instructions for stack unwinding are encoded into a dwarf program formed by a list of instructions. Each FDE corresponds to a region in the code and it has its own program. This predicate captures one instruction in that program.

FdeAddr is the address of the FDE and indentifies it uniquely.
Index identifies the instruction within the FDE uniquely.
Size is the size of the instruction in bytes.
InsnAddr is the address where the instruction is located
Insn is the actual opcode of the instruction
Op1 and Op2 are the operands of the instruction.

Used by: cfi_directive, fde_instruction_ref, last_fde_instruction, symbol_minus_symbol

lsda(lsdaAddress:address, callsiteTable:address, callsiteTableEncoding:unsigned, callSiteTableLength:unsigned, typeTable:address, typeTableEncoding:unsigned, landingPadBaseAddress: address)

A LSDA defines the exception information of a region of code (typically a procedure). This is located in section ‘.gcc_except_table’. A LSDA entry contains two main elements a callsite table (see lsda_callsite) and a type table (see lsda_type_entry).

Used by: lsda_symbol_minus_symbol, symbol_special_encoding, symbolic_data

lsda_pointer_locations(lsdaAddress:address, typeTablePointerLocation:address, callsiteTablePointerLoc:address)

Complementary predicate with the locations of the various pointers in a LSDA used for symbolization.

Used by: lsda_symbol_minus_symbol, symbol_special_encoding

lsda_callsite(CallSiteTable_address:address, EA_start:address, Start:address, EA_end:address, End:address, EA_landingPad:address, LandingPad:address, EA_endLandindPad:address)

The range [Start,End) corresponds to the try block and ‘LandingPad’ to the location where the catch block is located. ‘EA_start’, ‘EA_end’ and ‘EA_landingPad’ a the locations of the symbolic expressions in the .gcc_except_table that point to ‘Start’, ‘End’ and ‘LandingPad’ respectively.

Used by: boundary_sym_expr, lsda_callsite_addresses, lsda_symbol_minus_symbol, symbol_special_encoding

lsda_type_entry(lsdaTypeTableAddress:address, index:unsigned, address:address)

The exception handling mechanism chooses which catch block catches an given exception based on the type of the exception. This is done by having references to the types which are encoded in the type table. A lsda_type_entry is an entry in the type table. The “type” is represented as a symbolic expression pointing to ‘address’.

Used by: lsda_symbol_minus_symbol, symbolic_data

arm_exidx_entry(FunctionStart:address, CantUnwind:unsigned)

Address where a function starts according to the ARM exidx table.

This address does not set the low bit for Thumb functions.

Used by: basic_target, block_limit, impossible_block, known_block, negative_block_heuristic

fde_addresses(start:address, end:address)

misaligned_fde_start(start:address, start_adjusted:address)

FDE start points can on occasion be misaligned with the actual start of the function. This has been seen on glibc restore_rt which generates code as follows:

.text .align 16 __restore_rt:

movl $15, %rax syscall

Uses: fde_addresses, instruction, next

Used by: basic_target, fde_block_addresses, known_block

lsda_callsite_addresses(Start:address, End:address, LandingPad:address)

special_encoding(Code:unsigned, Name:symbol)