(*Generated by Lem from abis/abis.lem.*) (** The [abis] module is the top-level module for all ABI related code, including * some generic functionality that works across all ABIs, and a primitive attempt * at abstracting over ABIs for purposes of linking. *) open Lem_basic_classes open Lem_bool open Lem_num open Lem_maybe open Lem_list open Lem_set (*import Map*) open Lem_string open Show open Lem_assert_extra open Error open Missing_pervasives open Elf_file open Elf_header open Elf_interpreted_section open Elf_relocation open Elf_symbol_table open Elf_program_header_table open Elf_section_header_table open Memory_image open Abi_amd64 open Abi_amd64_relocation open Abi_aarch64_le open Abi_aarch64_relocation open Abi_power64 open Abi_power64_relocation open Gnu_ext_abi open Abi_classes open Abi_utilities open Elf_types_native_uint open Memory_image_orderings (** Relocation operators and their validity on a given platform *) (*val is_valid_abi_aarch64_relocation_operator : relocation_operator -> bool*) let is_valid_abi_aarch64_relocation_operator op:bool= ((match op with | Page -> true | G -> true | GDat -> true | GLDM -> true | DTPRel -> true | GTPRel -> true | TPRel -> true | GTLSDesc -> true | Delta -> true | LDM -> true | TLSDesc -> true | Indirect -> true | _ -> false )) (*val is_valid_abi_aarch64_relocation_operator2 : relocation_operator2 -> bool*) let is_valid_abi_aarch64_relocation_operator2 op:bool= ((match op with | GTLSIdx -> true )) (*val is_valid_abi_amd64_relocation_operator : relocation_operator -> bool*) let is_valid_abi_amd64_relocation_operator op:bool= ((match op with | Indirect -> true | _ -> false (* XXX: not sure about this? *) )) (*val is_valid_abi_amd64_relocation_operator2 : relocation_operator2 -> bool*) let is_valid_abi_amd64_relocation_operator2 op:bool= ((match op with | _ -> false )) (*val is_valid_abi_power64_relocation_operator : relocation_operator -> bool*) let is_valid_abi_power64_relocation_operator op:bool= false (* TODO *) (*val is_valid_abi_power64_relocation_operator2 : relocation_operator2 -> bool*) let is_valid_abi_power64_relocation_operator2 op:bool= ((match op with | _ -> false )) (** Misc. ABI related stuff *) type any_abi_feature = Amd64AbiFeature of any_abi_feature amd64_abi_feature | Aarch64LeAbiFeature of aarch64_le_abi_feature (*val anyAbiFeatureCompare : any_abi_feature -> any_abi_feature -> Basic_classes.ordering*) let anyAbiFeatureCompare f1 f2:int= ((match (f1, f2) with (Amd64AbiFeature(af1), Amd64AbiFeature(af2)) -> Abi_amd64.abiFeatureCompare0 af1 af2 |(Amd64AbiFeature(_), _) -> (-1) |(Aarch64LeAbiFeature(af1), Amd64AbiFeature(af2)) -> 1 |(Aarch64LeAbiFeature(af1), Aarch64LeAbiFeature(af2)) -> abiFeatureCompare af1 af2 )) (*val anyAbiFeatureTagEquiv : any_abi_feature -> any_abi_feature -> bool*) let anyAbiFeatureTagEquiv f1 f2:bool= ((match (f1, f2) with (Amd64AbiFeature(af1), Amd64AbiFeature(af2)) -> Abi_amd64.abiFeatureTagEq0 af1 af2 |(Amd64AbiFeature(_), _) -> false |(Aarch64LeAbiFeature(af1), Amd64AbiFeature(af2)) -> false |(Aarch64LeAbiFeature(af1), Aarch64LeAbiFeature(af2)) -> abiFeatureTagEq af1 af2 )) let instance_Basic_classes_Ord_Abis_any_abi_feature_dict:(any_abi_feature)ord_class= ({ compare_method = anyAbiFeatureCompare; isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(anyAbiFeatureCompare f1 f2) (-1)))); isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (anyAbiFeatureCompare f1 f2)(Pset.from_list compare [(-1); 0]))); isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(anyAbiFeatureCompare f1 f2) 1))); isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (anyAbiFeatureCompare f1 f2)(Pset.from_list compare [1; 0])))}) let instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict:(any_abi_feature)abiFeatureTagEquiv_class= ({ abiFeatureTagEquiv_method = anyAbiFeatureTagEquiv}) let make_elf64_header data osabi abiv ma t entry shoff phoff phnum shnum shstrndx:elf64_header= ({ elf64_ident = ([elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3; Uint32.of_string (Nat_big_num.to_string elf_class_64); Uint32.of_string (Nat_big_num.to_string data); Uint32.of_string (Nat_big_num.to_string elf_ev_current); Uint32.of_string (Nat_big_num.to_string osabi); Uint32.of_string (Nat_big_num.to_string abiv); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)); Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))]) ; elf64_type = (Uint32.of_string (Nat_big_num.to_string t)) ; elf64_machine = (Uint32.of_string (Nat_big_num.to_string ma)) ; elf64_version = (Uint32.of_string (Nat_big_num.to_string elf_ev_current)) ; elf64_entry = (Uint64.of_string (Nat_big_num.to_string entry)) ; elf64_phoff = (Uint64.of_string (Nat_big_num.to_string phoff)) ; elf64_shoff = (Uint64.of_string (Nat_big_num.to_string shoff)) ; elf64_flags = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_ehsize = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 64))) ; elf64_phentsize= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 56))) ; elf64_phnum = (Uint32.of_string (Nat_big_num.to_string phnum)) ; elf64_shentsize= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 64))) ; elf64_shnum = (Uint32.of_string (Nat_big_num.to_string shnum)) ; elf64_shstrndx = (Uint32.of_string (Nat_big_num.to_string shstrndx)) }) (*val phdr_flags_from_section_flags : natural -> string -> natural*) let phdr_flags_from_section_flags section_flags sec_name:Nat_big_num.num= (let flags = (Nat_big_num.bitwise_or elf_pf_r (Nat_big_num.bitwise_or (if flag_is_set shf_write section_flags then elf_pf_w else Nat_big_num.of_int 0) (if flag_is_set shf_execinstr section_flags then elf_pf_x else Nat_big_num.of_int 0))) in (*let _ = errln ("Phdr flags of section " ^ sec_name ^ "(ELF section flags 0x " ^ (hex_string_of_natural section_flags) ^ ") are 0x" ^ (hex_string_of_natural flags)) in*) flags) (*val phdr_is_writable : natural -> bool*) let phdr_is_writable flags:bool= (Nat_big_num.equal (Nat_big_num.bitwise_and flags elf_pf_w) elf_pf_w) type can_combine_flags_fn = Nat_big_num.num Pset.set -> Nat_big_num.num option (* FIXME: lift this to a personality function of the GNU linker? * Not sure really... need to try some other linkers. *) (*val load_can_combine_flags : can_combine_flags_fn*) let load_can_combine_flags flagsets:(Nat_big_num.num)option= ( (* The GNU linker happily adds a .rodata section to a RX segment, * but not to a RW segment. So the only clear rule is: if any is writable, * all must be writable. *)let flagslist = (Pset.elements flagsets) in let union_flags = (List.fold_left Nat_big_num.bitwise_or(Nat_big_num.of_int 0) flagslist) in if List.exists phdr_is_writable flagslist then if List.for_all phdr_is_writable flagslist then Some union_flags else None else Some union_flags) (*val tls_can_combine_flags : can_combine_flags_fn*) let tls_can_combine_flags flagsets:(Nat_big_num.num)option= (Some (List.fold_left Nat_big_num.bitwise_or(Nat_big_num.of_int 0) (Pset.elements flagsets))) let maybe_extend_phdr phdr isec1 can_combine_flags:(elf64_program_header_table_entry)option= (let new_p_type = (Nat_big_num.of_string (Uint32.to_string phdr.elf64_p_type)) in let this_section_phdr_flags = (phdr_flags_from_section_flags isec1.elf64_section_flags isec1.elf64_section_name_as_string) in let maybe_extended_flags = (can_combine_flags(Pset.from_list Nat_big_num.compare [ this_section_phdr_flags; Nat_big_num.of_string (Uint32.to_string phdr.elf64_p_flags) ])) in if (Lem.option_equal Nat_big_num.equal maybe_extended_flags None) then (*let _ = errln "flag mismatch" in*) None else let new_p_flags = ((match maybe_extended_flags with Some flags -> flags | _ -> failwith "impossible" )) in (* The new filesz is the file end offset of this section, * minus the existing file start offset of the phdr. * Check that the new section begins after the old offset+filesz. *) if Nat_big_num.less isec1.elf64_section_offset (Nat_big_num.add (Nat_big_num.of_string (Uint64.to_string phdr.elf64_p_offset)) (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_filesz)) then (*let _ = errln "offset went backwards" in*) None else let new_p_filesz = (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_filesz) (if Nat_big_num.equal isec1.elf64_section_type sht_progbits then isec1.elf64_section_size else Nat_big_num.of_int 0)) in (* The new memsz is the virtual address end address of this section, * minus the existing start vaddr of the phdr. * Check that the new section begins after the old vaddr+memsz. *) if Nat_big_num.less isec1.elf64_section_addr (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_vaddr) (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_memsz)) then (*let _ = errln "vaddr went backwards" in*) None else let new_p_memsz = (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_memsz) isec1.elf64_section_size) in let (one_if_zero : Nat_big_num.num -> Nat_big_num.num) = (fun n -> if Nat_big_num.equal n(Nat_big_num.of_int 0) then Nat_big_num.of_int 1 else n) in let new_p_align = (lcm (one_if_zero (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_align)) (one_if_zero isec1.elf64_section_align)) in Some { elf64_p_type = (Uint32.of_string (Nat_big_num.to_string new_p_type)) ; elf64_p_flags = (Uint32.of_string (Nat_big_num.to_string new_p_flags)) ; elf64_p_offset = (phdr.elf64_p_offset) ; elf64_p_vaddr = (phdr.elf64_p_vaddr) ; elf64_p_paddr = (phdr.elf64_p_paddr) ; elf64_p_filesz = (Uint64.of_string (Nat_big_num.to_string new_p_filesz)) ; elf64_p_memsz = (Uint64.of_string (Nat_big_num.to_string new_p_memsz)) ; elf64_p_align = (Uint64.of_string (Nat_big_num.to_string new_p_align)) }) let make_new_phdr isec1 t maxpagesize1 commonpagesize1:elf64_program_header_table_entry= (let rounded_down_offset = (fun isec1 -> round_down_to commonpagesize1 isec1.elf64_section_offset) in let offset_round_down_amount = (fun isec1 -> Nat_big_num.sub_nat isec1.elf64_section_offset (rounded_down_offset isec1)) in let rounded_down_vaddr = (fun isec1 -> round_down_to commonpagesize1 isec1.elf64_section_addr) in let vaddr_round_down_amount = (fun isec1 -> Nat_big_num.sub_nat isec1.elf64_section_addr (rounded_down_vaddr isec1)) in { elf64_p_type = (Uint32.of_string (Nat_big_num.to_string t)) (** Type of the segment *) ; elf64_p_flags = (Uint32.of_string (Nat_big_num.to_string (phdr_flags_from_section_flags isec1.elf64_section_flags isec1.elf64_section_name_as_string))) (** Segment flags *) ; elf64_p_offset = (Uint64.of_string (Nat_big_num.to_string (rounded_down_offset isec1))) (** Offset from beginning of file for segment *) ; elf64_p_vaddr = (Uint64.of_string (Nat_big_num.to_string (rounded_down_vaddr isec1))) (** Virtual address for segment in memory *) ; elf64_p_paddr = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (** Physical address for segment *) ; elf64_p_filesz = (Uint64.of_string (Nat_big_num.to_string (if Nat_big_num.equal isec1.elf64_section_type sht_nobits then Nat_big_num.of_int 0 else Nat_big_num.add isec1.elf64_section_size (offset_round_down_amount isec1)))) (** Size of segment in file, in bytes *) ; elf64_p_memsz = (Uint64.of_string (Nat_big_num.to_string ( Nat_big_num.add isec1.elf64_section_size (vaddr_round_down_amount isec1)))) (** Size of segment in memory image, in bytes *) ; elf64_p_align = (Uint64.of_string (Nat_big_num.to_string (* isec.elf64_section_align *)maxpagesize1)) (** Segment alignment memory for memory and file *) }) (*val make_load_phdrs : forall 'abifeature. natural -> natural -> annotated_memory_image 'abifeature -> list elf64_interpreted_section -> list elf64_program_header_table_entry*) let make_load_phdrs maxpagesize1 commonpagesize1 img2 section_pairs_bare_sorted_by_address:(elf64_program_header_table_entry)list= ( (* accumulate sections into the phdr *)let rev_list = (List.fold_left (fun accum_phdr_list -> (fun isec1 -> ( (* Do we have a current phdr? *) (match accum_phdr_list with [] -> (* no, so make one *) (*let _ = errln ("Starting the first LOAD phdr for section " ^ isec.elf64_section_name_as_string) in*) [make_new_phdr isec1 elf_pt_load maxpagesize1 commonpagesize1] | current_phdr :: more -> (* can we extend it with the current section? *) (match maybe_extend_phdr current_phdr isec1 load_can_combine_flags with None -> (*let _ = errln ("Starting new LOAD phdr for section " ^ isec.elf64_section_name_as_string) in*) (make_new_phdr isec1 elf_pt_load maxpagesize1 commonpagesize1) :: (current_phdr :: more) | Some phdr -> phdr :: more ) ) ))) [] (List.filter (fun isec1 -> flag_is_set shf_alloc isec1.elf64_section_flags && not (flag_is_set shf_tls isec1.elf64_section_flags)) section_pairs_bare_sorted_by_address)) in (*let _ = errln "Successfully made phdrs" in*) List.rev rev_list) (*val tls_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*) let tls_extend a:'abifeature abi= ({ is_valid_elf_header = (a.is_valid_elf_header) ; make_elf_header = (a.make_elf_header) ; reloc = (a.reloc) ; section_is_special = (a.section_is_special) ; section_is_large = (a.section_is_large) ; maxpagesize = (a.maxpagesize) ; minpagesize = (a.minpagesize) ; commonpagesize = (a.commonpagesize) ; symbol_is_generated_by_linker = (a.symbol_is_generated_by_linker) ; make_phdrs = (fun maxpagesize1 -> fun commonpagesize1 -> fun file_type -> fun img2 -> fun section_pairs_bare_sorted_by_address -> ( let rev_list = (List.fold_left (fun accum_phdr_list -> (fun isec1 -> ( (match accum_phdr_list with [] -> (*let _ = errln "Making a new TLS program header" in*) [make_new_phdr isec1 elf_pt_tls maxpagesize1 commonpagesize1] | current_phdr :: more -> (match maybe_extend_phdr current_phdr isec1 tls_can_combine_flags with None -> (make_new_phdr isec1 elf_pt_tls maxpagesize1 commonpagesize1) :: (current_phdr :: more) | Some phdr -> phdr :: more ) ) ))) [] (List.filter (fun isec1 -> flag_is_set shf_alloc isec1.elf64_section_flags && flag_is_set shf_tls isec1.elf64_section_flags) section_pairs_bare_sorted_by_address)) in List.rev_append (List.rev (a.make_phdrs maxpagesize1 commonpagesize1 file_type img2 section_pairs_bare_sorted_by_address)) (List.rev rev_list) )) ; max_phnum = (Nat_big_num.add(Nat_big_num.of_int 1) a.max_phnum) ; guess_entry_point = (a.guess_entry_point) ; pad_data = (a.pad_data) ; pad_code = (a.pad_code) ; generate_support = (a.generate_support) ; concretise_support = (a.concretise_support) ; get_reloc_symaddr = (a.get_reloc_symaddr) }) (* We use these snappily-named functions in relocation calculations. *) (*val make_default_phdrs : forall 'abifeature. natural -> natural -> natural (* file type *) -> annotated_memory_image 'abifeature -> list elf64_interpreted_section -> list elf64_program_header_table_entry*) let make_default_phdrs maxpagesize1 commonpagesize1 t img2 section_pairs_bare_sorted_by_address:(elf64_program_header_table_entry)list= ( (* FIXME: do the shared object and dyn. exec. stuff too *)make_load_phdrs maxpagesize1 commonpagesize1 img2 section_pairs_bare_sorted_by_address) (*val find_start_symbol_address : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => annotated_memory_image 'abifeature -> maybe natural*) let find_start_symbol_address dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2:(Nat_big_num.num)option= ( (* Do we have a symbol called "_start"? *)let all_defs = (Memory_image_orderings.defined_symbols_and_ranges dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2) in let get_entry_point = (fun (maybe_range, symbol_def) -> if symbol_def.def_symname = "_start" then Some (maybe_range, symbol_def) else None ) in let all_entry_points = (Lem_list.mapMaybe get_entry_point all_defs) in (match all_entry_points with [(maybe_range, symbol_def)] -> (match maybe_range with Some (el_name, (el_off, len)) -> (match Pmap.lookup el_name img2.elements with None -> failwith ("_start symbol defined in nonexistent element `" ^ (el_name ^ "'")) | Some el_rec -> (match el_rec.startpos with None -> (*let _ = Missing_pervasives.errln "warning: saw `_start' in element with no assigned address" in *)None | Some x -> (* success! *) Some ( Nat_big_num.add x el_off) ) ) | _ -> (*let _ = Missing_pervasives.errln "warning: `_start' symbol with no range" in*) None ) | [] -> (* no _start symbol *) None | _ -> (*let _ = Missing_pervasives.errln ("warning: saw multiple `_start' symbols: " ^ (let (ranges, defs) = unzip all_entry_points in show ranges)) in *)None )) (*val pad_zeroes : natural -> list byte*) let pad_zeroes n:(char)list= (replicate0 n (Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 0)))) (*val pad_0x90 : natural -> list byte*) let pad_0x90 n:(char)list= (replicate0 n (Char.chr (Nat_big_num.to_int ( Nat_big_num.mul(Nat_big_num.of_int 9)(Nat_big_num.of_int 16))))) (* null_abi captures ABI details common to all ELF-based, System V-based systems. * HACK: for now, specialise to 64-bit ABIs. *) (*val null_abi : abi any_abi_feature*) let null_abi:(any_abi_feature)abi= ({ is_valid_elf_header = is_valid_elf64_header ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none(Nat_big_num.of_int 0) elf_ma_none) ; reloc = noop_reloc ; section_is_special = elf_section_is_special ; section_is_large = (fun s -> (fun f -> false)) ; maxpagesize = (Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 256))(Nat_big_num.of_int 4096)) (* 2MB; bit of a guess, based on gdb and prelink code *) ; minpagesize =(Nat_big_num.of_int 1024) (* bit of a guess again *) ; commonpagesize =(Nat_big_num.of_int 4096) ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_") ; make_phdrs = make_default_phdrs ; max_phnum =(Nat_big_num.of_int 2) ; guess_entry_point = (find_start_symbol_address instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) ; pad_data = pad_zeroes ; pad_code = pad_zeroes ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ()) ; concretise_support = (fun img2 -> img2) ; get_reloc_symaddr = (default_get_reloc_symaddr instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) }) (*val got_entry_ordering : (string * maybe symbol_definition) -> (string * maybe symbol_definition) -> Basic_classes.ordering*) let got_entry_ordering (s1, md1) (s2, md2):int= (compare s1 s2) (* FIXME *) let is_ifunc_def:(symbol_definition)option ->bool= (fun maybe_def -> (match maybe_def with None -> false | Some d -> Nat_big_num.equal (get_elf64_symbol_type d.def_syment) stt_gnu_ifunc )) let amd64_reloc_needs_got_slot:'a ->reloc_site ->(symbol_definition)option ->bool= (fun symref -> fun rr -> fun maybe_def -> if ( Pset.mem(get_elf64_relocation_a_type rr.ref_relent)(Pset.from_list Nat_big_num.compare [ r_x86_64_got32; r_x86_64_gotpcrel; r_x86_64_gottpoff; r_x86_64_gotoff64; r_x86_64_gotpc32 (* ; r_x86_64_gotpc32_tlsdesc *) ])) then true else if is_ifunc_def maybe_def then (* This reference is bound to a STT_GNU_IFUNC definition. * What now needs to happen is as follows. * - we ensure that a GOT entry is generated for this symbol (we do this here); * - we ensure that a PLT entry (specifically .iplt) is generated for the symbol (Below); * - on making the GOT, we also generate a .rela.plt relocation record covering the GOT slot; * - when applying the relocation, of whatever kind, the address of the PLT slot * is the address input to the calculation * - the code marked by the STT_GNU_IFUNC symbol definition is not the function * to call; it's the function that calculates the address of the function to call! * this becomes the addend of the R_X86_64_IRELATIVE Elf64_Rela marking the GOT slot * - note that for static linking, the GOT is usually pre-filled (cf. dynamically when it is filled by JUMP_SLOT relocs). * ... but our GOT entries *must* have corresponding R_X86_64_IRELATIVEs generated *) true else false) let amd64_reloc_needs_plt_slot (symref : symbol_reference_and_reloc_site) rr maybe_def ref_is_statically_linked:bool= (if ( Pset.mem(get_elf64_relocation_a_type rr.ref_relent)(Pset.from_list Nat_big_num.compare [ r_x86_64_plt32 (* NOTE: when generating shared libs, it starts to matter * where the definition is -- anything that is locally interposable * or undefined will need a slot. See amd64_get_reloc_symaddr. *) ])) then not (ref_is_statically_linked rr) else if is_ifunc_def maybe_def then true else (* not a PLT ref *) false) let amd64_find_got_label_and_element img2:((string*(symbol_definition)option)list*element)option= ((match Pmap.lookup ".got" img2.elements with None -> (* got no GOT? okay... *) None | Some got_el -> (* Find the GOT tag. *) let tags_and_ranges = (Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag) in (match tags_and_ranges with [] -> failwith "error: GOT element but no ABI feature GOT tag" | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), _)] -> Some (l, got_el) | _ -> failwith ("multiple GOT elements/tags") ) )) let amd64_find_plt_label_and_element img2:((string*(symbol_definition)option*(any_abi_feature)plt_entry_content_fn)list*element)option= ((match Pmap.lookup ".plt" img2.elements with None -> (* got no PLT? okay... *) None | Some plt_el -> (* Find the PLT tag. *) let tags_and_ranges = (Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0([])))) img2.by_tag) in (match tags_and_ranges with [] -> failwith "error: PLT element but no ABI feature PLT tag" | [(AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0(l))), _)] -> Some (l, plt_el) | _ -> failwith ("multiple PLT elements/tags") ) )) let got_slot_index_for_symname dict_Basic_classes_Eq_a symname got_label:(int)option= (Lem_list.find_index (fun (s, _) -> dict_Basic_classes_Eq_a.isEqual_method s symname) got_label) (*val amd64_get_reloc_symaddr : symbol_definition -> annotated_memory_image any_abi_feature -> maybe reloc_site -> natural*) let amd64_get_reloc_symaddr the_input_def output_img maybe_reloc1:Nat_big_num.num= ( (* The default implementation simply looks up a "matching" symbol in the output image * and calculates its address. * * That's normally fine, even for via-GOT references since their calculations don't * use the symaddr. For via-PLT references, we need to use the PLT slot address. * HMM. Isn't this duplicating the role of functions like amd64_plt_slot_addr? * Recall that we created this get_reloc_symaddr mechanism to deal with IFUNC symbols. * With an IFUNC symbol, we reference it simply using a PC32 relocation, but the address * that gets filled in isn't the IFUNC address; it's the corresponding PLT slot. * HMM: does this happen for other PC32 references? If so, we'll need this mechanism * there. And it certainly does, because relocatable object code never uses PLT32 * relocs. * * I had previously tried to handle this issue in mark_fate_of_relocs, using the * 1-argument ApplyReloc(_) and MakePIC to encode the "replacement". But at that stage, * which is ABI-independent and happens before address assignment?, we can't know enough. *) (* match bound_def_in_input with Nothing -> 0 | Just the_input_def -> *)if is_ifunc_def (Some(the_input_def)) then (* We need to return the address of the "matching" PLT slot. * PLT label entries are (symname, maybe_def, content_fn). *) (match amd64_find_plt_label_and_element output_img with None -> failwith "error: ifunc but no PLT" | Some (l, plt_el) -> (match Lem_list.find_index (fun (symname, _, _) -> symname = the_input_def.def_symname) l with (* FIXME: using symnames seems wrong *) Some idx1 -> (match plt_el.startpos with Some addr -> Nat_big_num.add addr (Nat_big_num.mul (Nat_big_num.of_int idx1)(Nat_big_num.of_int 16)) (* size of a PLT entry *) | None -> failwith "error: PLT has no address assigned" ) | None ->Nat_big_num.of_int 0 ) ) else default_get_reloc_symaddr instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict the_input_def output_img maybe_reloc1) (* end *) (* *) (*val amd64_generate_support : (* list (list reloc_site_resolution) -> *) list (string * annotated_memory_image any_abi_feature) -> annotated_memory_image any_abi_feature*) let amd64_generate_support (* reloc_resolution_lists *) input_fnames_and_imgs:(any_abi_feature)annotated_memory_image= ( (* We generate a basic GOT. At the moment we can only describe the GOT * contents abstractly, not as its binary content, because addresses * have not yet been fixed. * * To do this, we create a set of Abi_amd64.GOTEntry records, one for * each distinct symbol that is referenced by one or more GOT-based relocations. * To enumerate these, we look at all the symbol refs in the image. *)let ref_is_statically_linked = (fun _ -> true) in let (fnames, input_imgs) = (List.split input_fnames_and_imgs) in let tags_and_ranges_by_image = (Lem_list.mapi (fun i -> fun (fname1, img2) -> (i, fname1, Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolRef(null_symbol_reference_and_reloc_site)) img2.by_tag) ) input_fnames_and_imgs) in let refs_via_got = (list_concat_map (fun (i, fname1, tags_and_ranges) -> Lem_list.mapMaybe (fun (tag, maybe_range) -> (match tag with SymbolRef(symref) -> (* Is this ref a relocation we're going to apply, and does it reference the GOT? *) (match (symref.maybe_reloc, symref.maybe_def_bound_to) with (None, _) -> None | (Some rr, Some(ApplyReloc, maybe_def)) -> if amd64_reloc_needs_got_slot symref rr maybe_def then (*let _ = errln ("Saw a via-GOT symbol reference: to `" ^ symref.ref.ref_symname ^ "' coming from linkable " ^ (show i) ^ " (" ^ fname ^ "), logically from section " ^ (show rr.ref_src_scn)) in *) Some (symref.ref.ref_symname, maybe_def) else None | (Some rr, Some(makePIC0, maybe_def)) -> failwith "FIXME: PIC support please" ) | _ -> failwith "impossible: reloc site tag is not a SymbolRef" )) tags_and_ranges) tags_and_ranges_by_image) in let (symnames, maybe_defs) = (List.split refs_via_got) in (*let _ = errln ("GOT includes defs with names: " ^ (show (Set_extra.toList (Set.fromList symnames)))) in*) let got_pairs_set = (Pset.from_list (pairCompare compare (maybeCompare compare)) refs_via_got) in let got_defs_set = (Pset.from_list (maybeCompare compare) maybe_defs) in (* This is where we fix the order of the GOT entries. *) let got_pairs_list = (Pset.elements got_pairs_set) in let got_idx_and_maybe_def_by_symname_map = (Lem_map.fromList (Lem_map.instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) (mapi (fun slot_idx -> fun (symname, maybe_def) -> (symname, (slot_idx, maybe_def))) got_pairs_list)) in let got_ifunc_set = (let x2 =(Pset.from_list (maybeCompare compare) []) in Pset.fold (fun maybe_d x2 -> if is_ifunc_def maybe_d then Pset.add maybe_d x2 else x2) got_defs_set x2) in (* Quirk: what if we have the same def appearing under two different symnames? * This shouldn't happen, at present. * What if we have the same symname related to two different defs? This also * shouldn't happen, because only global symbols go in the GOT, so we don't have * to worry about local symbols with the same name as another symbol. But still, it * could plausibly happen in some situations with weird symbol visibilities or binding. *) (* if Set.size pairs_set <> Set.size defs_set then failwith "something quirky going on with GOT symbol defs and their names" else *) (* let name_def_pairs = List.foldl (fun acc -> fun (idx, symname, (maybe_range, rr)) -> Set.insert ( symname, (match rr.maybe_def_bound_to with Map.lookup symname acc with Nothing -> [item] | Just l -> item :: l end) acc) {} refs_via_got in *) let got_nentries = (Nat_big_num.of_int (Pset.cardinal got_pairs_set)) in let got_entrysize =(Nat_big_num.of_int 8) in (* We also need a PLT... sort of. We need a way to resolve via-PLT relocs. * But we might do so without actually creating a (non-zero-length) PLT. * Again, this is to accommodate the sorts of optimisations the GNU linker does. * * Note that every PLT entry has a corresponding GOT entry. Here we are simply * enumerating the via-PLT relocs that imply a PLT entry. We look their GOT * slots up later, by symbol name. *) let refs_via_plt = (list_concat_map (fun (i, fname1, tags_and_ranges) -> Lem_list.mapMaybe (fun (tag, maybe_range) -> (match tag with SymbolRef(symref) -> (* Is this ref a relocation we're going to apply, and does it reference the GOT? *) (match (symref.maybe_reloc, symref.maybe_def_bound_to) with (None, _) -> None | (Some rr, Some(ApplyReloc, maybe_def)) -> if amd64_reloc_needs_plt_slot symref rr maybe_def ref_is_statically_linked then (*let _ = if is_ifunc_def maybe_def then (* we ensure that a PLT entry (specifically .iplt) is generated for the symbol *) errln ("Saw a reference to IFUNC symbol `" ^ symref.ref.ref_symname ^ "'; ref is coming from linkable " ^ (show i) ^ " (" ^ fname ^ "), relent idx " ^ (show rr.ref_rel_idx) ^ " logically from section " ^ (show rr.ref_src_scn) ) else errln ("Saw a via-PLT symbol reference: to `" ^ symref.ref.ref_symname ^ "' coming from linkable " ^ (show i) ^ " (" ^ fname ^ "), relent idx " ^ (show rr.ref_rel_idx) ^ " logically from section " ^ (show rr.ref_src_scn) ^ match maybe_def with Just _ -> ", with definition" | Nothing -> ", not bound to anything" end ) in*) Some(symref.ref.ref_symname, maybe_def) else None | (Some rr, Some(makePIC0, maybe_def)) -> failwith "FIXME: PIC support please" ) | _ -> failwith "impossible: reloc site tag is not a SymbolRef" )) tags_and_ranges) tags_and_ranges_by_image) in (*let _ = errln ("Saw " ^ (show (length refs_via_plt)) ^ " relocations of a via-PLT type") in*) (* account for the optimisations we did on GOT slots *) let refs_via_plt_having_got_slot = (Lem_list.mapMaybe (fun (symname, _) -> (match Pmap.lookup symname got_idx_and_maybe_def_by_symname_map with Some(idx1, maybe_d) -> Some (symname, idx1, maybe_d) | None -> None ) ) refs_via_plt) in (*let _ = errln ("Saw " ^ (show (length refs_via_plt_having_got_slot)) ^ " relocations of a via-PLT type where we instantiated a GOT slot for the symbol") in*) let (plt_symnames, plt_got_idxs, plt_ref_bound_to_maybe_defs) = (unzip3 refs_via_plt_having_got_slot) in let plt_symnames_excluding_header = (Pset.elements ((Pset.from_list compare plt_symnames))) in (*let _ = errln ("PLT symnames: " ^ (show plt_symnames_excluding_header)) in*) let n_iplt_entries = (Pset.cardinal got_ifunc_set) (* The content of the IPLT entries depends on the address assignment of GOT slots * and the IFUNCs that they reference. We need to reserve space for them here, though. *) in (*let _ = errln ("We think there should be " ^ (show n_iplt_entries) ^ " PLT entries due to references to IFUNC symbols") in*) (* let got_entries_referencing_functions = (List.filter (fun (symname, maybe_def) -> match def with Just d -> d.def_syment | Nothing -> false end) refs_via_got) in *) let plt_needs_header_entry = ((List.length plt_symnames_excluding_header) > n_iplt_entries) in (*let _ = errln ("PLT needs header entry? " ^ (show plt_needs_header_entry)) in*) let total_n_plt_entries = (Nat_big_num.add (if plt_needs_header_entry then Nat_big_num.of_int 1 else Nat_big_num.of_int 0) (Missing_pervasives.length plt_symnames_excluding_header)) in (*let _ = errln ("PLT total entry count: " ^ (show total_n_plt_entries)) in*) let new_by_range =(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [ (Some(".plt", (Nat_big_num.of_int 0, Nat_big_num.mul(Nat_big_num.of_int 16) total_n_plt_entries)), AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0( (* header content fn *) (* the header entry is required only for dynamic linking, which is not supported yet *) (* (if plt_needs_header_entry then ("", Nothing, (((fun (got_base_addr : natural) -> fun (plt_base_addr : natural) -> (0, [byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0]))) : plt_entry_content_fn any_abi_feature)) else ("", Nothing, (((fun (got_base_addr : natural) -> fun (plt_base_addr : natural) -> (0, []))) : plt_entry_content_fn any_abi_feature)) ) ++ *) ( mapi (fun plt_entry_idx_not_counting_header -> (fun symname -> (* We want to label the PLT entry with a function that * - accepts the PLT base address, the GOT base address and the GOT slot number; * - closure-captures whatever else it needs (whether we're inserting a PLT header); * - yields the *full contents of the PLT entry* before relocation. * - recall that PLT entries might be "header" (the special one at the start), * "normal" (to be relocated with R_X86_64_JUMP_SLOT) * or "irelative" (to be relocated with R_X86_64_IRELATIVE). * Q. Why are R_X86_64_JUMP_SLOT necessary? * The PLT entries are doing relative addressing, and * the offset to the GOT entry is known at link time, * so the linker should be able to fill them in. In * fact, it does. HMM. Understand this better. *) (* What is the GOT slot number? *) let (got_slot_idx, maybe_def) = ((match Pmap.lookup symname got_idx_and_maybe_def_by_symname_map with Some(idx1, maybe_d) -> (Nat_big_num.of_int idx1, maybe_d) | None -> failwith ("GOT does not contain symbol `" ^ (symname ^ "' required by PLT entry")) )) in (symname, maybe_def, ((fun (got_base_addr : Nat_big_num.num) -> fun (plt_base_addr : Nat_big_num.num) -> (* Okay, now we can generate the entry. NOTE that we're lexically still in generate_support, * but we'll be called from concretise_support. The code that generates the header * entry is actually in concretise_support. * * If the entry is a normal entry, it looks like * 0x0000000000400410 <+0>: ff 25 02 0c 20 00 jmpq *0x200c02(%rip) # 0x601018 0x0000000000400416 <+6>: 68 00 00 00 00 pushq $0x0 0x000000000040041b <+11>: e9 e0 ff ff ff jmpq 0x400400 * * If the entry is an irelative entry, it looks like * 400350: ff 25 02 fd 2b 00 jmpq *0x2bfd02(%rip) # 6c0058 <_GLOBAL_OFFSET_TABLE_+0x58> 400356: 68 00 00 00 00 pushq $0x0 40035b: e9 00 00 00 00 jmpq 400360 * ... i.e. basically the same but the pushq and jmpq have literal-zero args (they're not used). *) let this_plt_slot_base_addr = (Nat_big_num.add plt_base_addr (Nat_big_num.mul(Nat_big_num.of_int 16) ( Nat_big_num.add(Nat_big_num.of_int plt_entry_idx_not_counting_header) (if plt_needs_header_entry then Nat_big_num.of_int 1 else Nat_big_num.of_int 0)))) in (*let _ = Missing_pervasives.errln ("PLT slot base address for symname `" ^ symname ^ "': 0x" ^ (hex_string_of_natural this_plt_slot_base_addr)) in*) let got_slot_addr = (Nat_big_num.add got_base_addr (Nat_big_num.mul(Nat_big_num.of_int 8) got_slot_idx)) in (*let _ = Missing_pervasives.errln ("GOT slot address for symname `" ^ symname ^ "' (idx " ^ (show got_slot_idx) ^ "): 0x" ^ (hex_string_of_natural got_slot_addr)) in*) let maybe_header_entry_address = (if plt_needs_header_entry then Some(plt_base_addr) else None) in let offset_to_got_slot = (Nat_big_num.sub ( got_slot_addr) (( Nat_big_num.add this_plt_slot_base_addr(Nat_big_num.of_int 6)))) in (*let _ = Missing_pervasives.errln ("PLT's PC-relative index to GOT slot for symname `" ^ symname ^ "' (GOT idx " ^ (show got_slot_idx) ^ ") is (decimal)" ^ (show offset_to_got_slot)) in*) let content_bytes = (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 255)); Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 37))]) (* offset to the GOT entry, from the *next* instruction start, signed 32-bit LE *)(to_le_signed_bytes(Nat_big_num.of_int 4) offset_to_got_slot))) [Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 104))])) (* plt slot number not including header, 32-bit LE *)(to_le_unsigned_bytes(Nat_big_num.of_int 4) ((Nat_big_num.of_int plt_entry_idx_not_counting_header))))) [Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 233))])) (to_le_signed_bytes(Nat_big_num.of_int 4) ( if is_ifunc_def maybe_def then Nat_big_num.of_int 0 else (match maybe_header_entry_address with None -> failwith "normal PLT entry but no PLT header!" | Some header_entry_address -> Nat_big_num.sub ( header_entry_address) (( Nat_big_num.add this_plt_slot_base_addr(Nat_big_num.of_int 16))) ) ))) in (*let _ = errln ("Created a PLT entry consisting of " ^ (show (length content_bytes)) ^ " bytes.") in*) (this_plt_slot_base_addr, content_bytes) (* match maybe_def with Nothing -> 0 | Just sd -> match Memory_image_orderings.find_defs_matching sd img with [] -> failwith ("no matching definitions for PLT entry named " ^ symname) | [(Just(def_el_name, (def_start, def_len)), d)] -> match element_and_offset_to_address (def_el_name, def_start) img with Nothing -> failwith ("PLT: no address for definition offset in element " ^ def_el_name) | Just x -> let _ = errln ("PLT slot for symbol `" ^ symname ^ "' calculated at (non-PLT) address 0x" ^ (hex_string_of_natural x) ^ " (offset 0x" ^ (hex_string_of_natural def_start) ^ " in element " ^ def_el_name ^ ")") in x end | _ -> failwith ("multiple matching definitions for PLT entry named " ^ symname) end end *) ) : any_abi_feature plt_entry_content_fn)) )) plt_symnames) ))) ) ; (Some(".plt", (Nat_big_num.of_int 0, Nat_big_num.mul(Nat_big_num.of_int 16) total_n_plt_entries)), FileFeature(ElfSection(Nat_big_num.of_int 1, { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *) ; elf64_section_type = sht_progbits ; elf64_section_flags = shf_alloc ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *) ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *) ; elf64_section_size = (Nat_big_num.mul(Nat_big_num.of_int 16) total_n_plt_entries) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *) ; elf64_section_link =(Nat_big_num.of_int 0) ; elf64_section_info =(Nat_big_num.of_int 0) ; elf64_section_align =(Nat_big_num.of_int 16) ; elf64_section_entsize =(Nat_big_num.of_int 16) ; elf64_section_body = Byte_sequence.empty (* ignored *) ; elf64_section_name_as_string = ".plt" } ))) (* For each GOT entry that corresponds to a thread-local symbol, we also need to * generate a relocation record. HMM. These new relocation records are ones we don't * yet have decisions for. That might be a problem. * * In fact, this approach is not appropriate for static linking. Just put the offsets * in there when we concretise the GOT. Something like this will be good for * dynamic linking, though. At the moment, creating a SymbolRef at this stage * is problematic because it's not in the bindings list. When we generate shared * objects, we'll have to revisit that code. *) (* (Just(".got", (i * got_entrysize, 8)), SymbolRef( <| ref = <| ref_symname = symname ; ref_syment = sd.def_syment ; ref_sym_scn = 0 ; ref_sym_idx = 0 |> ; maybe_def_bound_to = Just(ApplyReloc, Just sd) ; maybe_reloc = Just( <| ref_relent = <| elf64_ra_offset = elf64_addr_of_natural 0 ; elf64_ra_info = elf64_xword_of_natural r_x86_64_tpoff64 ; elf64_ra_addend = elf64_sxword_of_integer 0 |> ; ref_rel_scn = 0 ; ref_rel_idx = 0 ; ref_src_scn = 0 |> ) |>)) | forall ((i, symname, sd) IN (Set.fromList (mapMaybei (fun i -> fun (symname, maybe_def) -> match maybe_def with Nothing -> Nothing | Just sd -> Just(i, symname, sd) end) refs_via_got))) | get_elf64_symbol_type sd.def_syment = stt_tls *) ; (Some(".got", (Nat_big_num.of_int 0, Nat_big_num.mul got_nentries got_entrysize)), AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(got_pairs_list)))) ; (Some(".got", (Nat_big_num.of_int 0, Nat_big_num.mul got_nentries got_entrysize)), FileFeature(ElfSection(Nat_big_num.of_int 2, { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *) ; elf64_section_type = sht_progbits ; elf64_section_flags = (Nat_big_num.bitwise_or shf_write shf_alloc) ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *) ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *) ; elf64_section_size = (Nat_big_num.mul got_nentries got_entrysize) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *) ; elf64_section_link =(Nat_big_num.of_int 0) ; elf64_section_info =(Nat_big_num.of_int 0) ; elf64_section_align =(Nat_big_num.of_int 8) ; elf64_section_entsize = got_entrysize ; elf64_section_body = Byte_sequence.empty (* ignored *) ; elf64_section_name_as_string = ".got" } ))) ; (* FIXME: I've a feeling _GLOBAL_OFFSET_TABLE_ generally doesn't mark the *start* of the GOT; * it's some distance in. What about .got.plt? *) (Some(".got", (Nat_big_num.of_int 0, Nat_big_num.mul got_nentries got_entrysize)), SymbolDef({ def_symname = "_GLOBAL_OFFSET_TABLE_" ; def_syment = ({ elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* ignored *) ; elf64_st_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* FIXME *) ; elf64_st_other = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* FIXME *) ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))) ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* ignored *) ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string ( Nat_big_num.mul got_nentries got_entrysize))) (* FIXME: start later, smaller size? zero size? *) }) ; def_sym_scn =(Nat_big_num.of_int 1) ; def_sym_idx =(Nat_big_num.of_int 1) ; def_linkable_idx =(Nat_big_num.of_int 0) })) ; (Some(".rela.iplt", (Nat_big_num.of_int 0, (* size of an Elf64_Rela *) Nat_big_num.mul(Nat_big_num.of_int 24) (Nat_big_num.of_int n_iplt_entries))), FileFeature(ElfSection(Nat_big_num.of_int 3, { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *) ; elf64_section_type = sht_rela ; elf64_section_flags = (Nat_big_num.bitwise_or shf_alloc shf_info_link) ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *) ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *) ; elf64_section_size = ( (* size of an Elf64_Rela *)Nat_big_num.mul(Nat_big_num.of_int 24) (Nat_big_num.of_int n_iplt_entries)) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *) ; elf64_section_link =(Nat_big_num.of_int 0) ; elf64_section_info =(Nat_big_num.of_int (* FIXME: want this to be the PLT section shndx *)0) ; elf64_section_align =(Nat_big_num.of_int 8) ; elf64_section_entsize =(Nat_big_num.of_int 24) ; elf64_section_body = Byte_sequence.empty (* ignored *) ; elf64_section_name_as_string = ".rela.iplt" } ))) ]) in { elements = (Pmap.add ".got" { startpos = None ; length1 = (Some ( Nat_big_num.mul got_nentries got_entrysize)) ; contents = ([]) } (Pmap.add ".plt" { startpos = None ; length1 = (let len = (Nat_big_num.mul(Nat_big_num.of_int 16) total_n_plt_entries) in (*let _ = errln ("PLT length in element: " ^ (show len) ^ " bytes") in *) Some ( Nat_big_num.mul(Nat_big_num.of_int 16) total_n_plt_entries)) ; contents = ([]) } (Pmap.add ".rela.iplt" { startpos = None ; length1 = (Some ( (* size of an Elf64_Rela *) Nat_big_num.mul(Nat_big_num.of_int 24) (Nat_big_num.of_int n_iplt_entries))) ; contents = ([]) } (Pmap.empty compare) ))) ; by_tag = (by_tag_from_by_range (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict new_by_range) ; by_range = new_by_range }) (*val amd64_concretise_support : annotated_memory_image any_abi_feature -> annotated_memory_image any_abi_feature*) let amd64_concretise_support orig_img:(any_abi_feature)annotated_memory_image= ( (*let _ = errln "Concretising amd64 ABI support structures" in*) (* Fill in the GOT contents. *)(match amd64_find_got_label_and_element orig_img with None -> orig_img (* no GOT, but that's okay *) | Some (got_l, got_el) -> let got_base_addr = ((match got_el.startpos with Some a -> a | None -> failwith "GOT has no address assigned" )) in let got_entry_bytes_for = (fun img2 -> fun symname -> fun maybe_def -> fun plt_l -> fun maybe_plt_el -> (match maybe_def with None -> replicate0(Nat_big_num.of_int 8) (Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 0))) | Some sd -> (* What should the GOT slot be initialized to point to? * If there's a PLT entry, we should point to that + 6, * i.e. the second instruction. * * If there's not, then it might be a thread-local. *) (match Lem_list.find_index (fun (plt_symname, _, _) -> symname = plt_symname) plt_l with Some plt_slot_idx -> (match maybe_plt_el with None -> failwith "GOT slot with PLT entry but no PLT element" | Some plt_el -> (match plt_el.startpos with Some addr -> natural_to_le_byte_list_padded_to(Nat_big_num.of_int 8) ( Nat_big_num.add (Nat_big_num.add addr ( Nat_big_num.mul(Nat_big_num.of_int plt_slot_idx)(Nat_big_num.of_int 16)))(Nat_big_num.of_int 6)) | None -> failwith ("no PLT!") ) ) | None -> (* Just look for a definition. *) (match Memory_image_orderings.find_defs_matching instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict sd img2 with [] -> failwith ("no matching definitions for GOT entry named " ^ symname) | [(Some(def_el_name, (def_start, def_len)), d)] -> (match element_and_offset_to_address (def_el_name, def_start) img2 with None -> failwith ("no address for definition offset in element " ^ def_el_name) | Some x -> (* If sd is a TLS symbol, we want its offset from the *end* of the * TLS segment. *) (* FIXME: factor out this logic so that it lives in the TLS ABI spec. *) if Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_tls then (* FIXME: the right way to do this is to mark the segments in the image * *first*. They can't have ranges, because they span many elements, * but they can have vaddr ranges as arguments. *) let offs = (i2n_signed( 64) (Nat_big_num.sub(Nat_big_num.of_int 0)(Nat_big_num.of_int 8))) in (*let _ = errln ("GOT slot for TLS symbol `" ^ symname ^ "' created containing offset 0x" ^ (hex_string_of_natural offs)) in*) natural_to_le_byte_list offs else (*let _ = errln ("GOT slot for symbol `" ^ symname ^ "' created pointing to address 0x" ^ (hex_string_of_natural x) ^ " (offset 0x" ^ (hex_string_of_natural def_start) ^ " in element " ^ def_el_name ^ ")") in*) natural_to_le_byte_list_padded_to(Nat_big_num.of_int 8) x ) | _ -> failwith ("multiple matching definitions for GOT entry named " ^ symname) ) ) )) in let concretise_got = (fun img2 -> fun plt_l -> fun maybe_plt_el -> let l = got_l (* Just(got_el_name, (got_start_off, got_len)))] -> *) in (*let _ = errln ("Concretising a GOT of " ^ (show (length l)) ^ " entries.") in*) let got_entry_contents = (Lem_list.map (fun (symname, maybe_def) -> Lem_list.map (fun b -> Some b) (got_entry_bytes_for img2 symname maybe_def plt_l maybe_plt_el)) l) in (* We replace the GOT element's contents with the concrete addresses * of the symbols it should contain. We leave the metadata label in there, * for the relocation logic to find. If we change the order of entries, * change it there too. *) let got_content = (List.concat got_entry_contents) in let new_got_el = ({ contents = got_content ; startpos = (got_el.startpos) ; length1 = (got_el.length1) }) in let new_got_tag = (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l)))) in let got_range = (Some(".got", (Nat_big_num.of_int 0, Nat_big_num.mul(Nat_big_num.of_int 8) (length l)))) in let new_by_tag = (Pset.(union)( Pset.diff(img2.by_tag : (( any_abi_feature range_tag) * ( element_range option)) Pset.set)(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), got_range)]))(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(new_got_tag, got_range)])) in let new_elements_map = (Pmap.add ".got" new_got_el ( Pmap.remove ".got" img2.elements )) in { elements = new_elements_map ; by_tag = new_by_tag ; by_range = (by_range_from_by_tag instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) new_by_tag) }) in (match amd64_find_plt_label_and_element orig_img with None -> concretise_got orig_img [] None (* no PLT, but possibly a GOT *) | Some (plt_l, plt_el) -> let plt_base_addr = ((match plt_el.startpos with Some a -> a | None -> failwith "PLT has no address assigned" )) in let concretise_plt = (fun img2 -> let l = plt_l in (* We replace the PLT element's contents with the concrete entries * for each of the symbols in the table. We leave the metadata label in there, * for the relocation logic to find. If we change the order of entries, * change it there too. *) let all_content = (List.concat (Lem_list.map (fun (_, _, plt_content_fn) -> let (_, content) = (plt_content_fn got_base_addr plt_base_addr) in content ) l)) in (*let _ = errln ("Got " ^ (show (length all_content)) ^ " bytes of PLT content") in let _ = errln ("Generated PLT reserved " ^ (show (match plt_el.length with Just n -> n | Nothing -> failwith "PLT has no length" end)) ^ " bytes of PLT content") in*) let new_plt_el = ({ contents = (Lem_list.map (fun b -> Some b) all_content) ; startpos = (plt_el.startpos) ; length1 = (Some(length all_content)) }) in let new_elements_map = (Pmap.add ".plt" new_plt_el ( Pmap.remove ".plt" img2.elements )) in { elements = new_elements_map ; by_tag = (img2.by_tag) ; by_range = (img2.by_range) }) in let concretise_rela_plt = (fun img2 -> let maybe_rela_plt_el = (Pmap.lookup ".rela.plt" img2.elements) in let maybe_new_rela_plt_el = ((match maybe_rela_plt_el with None -> (* got no .rela.plt? okay... *) (*let _ = errln "No .rela.plt found" in*) None | Some rela_plt_el -> let got_entry_iplt_widget_for = (fun symname -> fun maybe_def -> (match maybe_def with None -> None | Some sd -> if not (Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_gnu_ifunc) then None else Some(fun index_in_got -> (* This is a 24-byte Elf64_Rela. *) let (r_offset : Nat_big_num.num) (* GOT *slot* address! *) = ((match got_el.startpos with None -> failwith "internal error: GOT has no assigned address" | Some addr -> Nat_big_num.add addr ( Nat_big_num.mul(Nat_big_num.of_int 8) index_in_got) )) in let (r_info : Nat_big_num.num) = r_x86_64_irelative in ( List.rev_append (List.rev (List.rev_append (List.rev (natural_to_le_byte_list_padded_to(Nat_big_num.of_int 8) r_offset)) (natural_to_le_byte_list_padded_to(Nat_big_num.of_int 8) r_info))) (* r_addend -- address of the ifunc definition. * NOTE that this is NOT the same as the GOT entry bytes. * It's the actual address of the ifunc, whereas * the GOT entry is initialized to point back into the PLT entry. *)(match Memory_image_orderings.find_defs_matching instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict sd img2 with [] -> failwith ("impossible: IPLT entry widget found matching ifunc definition for " ^ symname) | [(Some(def_el_name, (def_start, def_len)), d)] -> (match element_and_offset_to_address (def_el_name, def_start) img2 with None -> failwith ("no address for ifunc definition offset in element " ^ def_el_name) | Some x -> (* If sd is a TLS symbol, we want its offset from the *end* of the * TLS segment. *) (* FIXME: factor out this logic so that it lives in the TLS ABI spec. *) if not (Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_gnu_ifunc) then failwith "impossible: found ifunc definition that is not an ifunc" else natural_to_le_byte_list_padded_to(Nat_big_num.of_int 8) x ) | _ -> failwith "impossible: more than one ifunc definition" ) )) (* end Just sd *) )) in let rela_iplt_widgets = (Lem_list.map (fun (symname, maybe_def) -> got_entry_iplt_widget_for symname maybe_def) got_l) in let new_content_bytelists = (mapi (fun i -> fun rela_widget -> (match rela_widget with Some f -> f (Nat_big_num.of_int i) | None -> [] ) ) rela_iplt_widgets) in let new_contents = (Lem_list.map (fun b -> Some b) (List.concat new_content_bytelists)) in (*let _ = errln ("Concretised .rela.plt; first 24 bytes: " ^ (show (take 24 new_contents))) in*) Some( { contents = new_contents ; startpos = (rela_plt_el.startpos) ; length1 = (rela_plt_el.length1) } ) )) in let new_elements_map = ((match maybe_new_rela_plt_el with Some new_rela_plt_el -> Pmap.add ".rela.plt" new_rela_plt_el ( Pmap.remove ".rela.plt" img2.elements ) | None -> img2.elements )) in { elements = new_elements_map ; by_tag = (img2.by_tag) ; by_range = (img2.by_range) }) in concretise_rela_plt (concretise_plt (concretise_got orig_img plt_l (Some plt_el))) ) )) (*val amd64_got_slot_idx : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural*) let amd64_got_slot_idx img2 rr:Nat_big_num.num= ( (*let _ = errln ("Looking up GOT slot for symbol " ^ rr.ref.ref_symname) in*)(match Pmap.lookup ".got" img2.elements with None -> (* got no GOT? okay... *) failwith "got no GOT" | Some got_el -> (* Find the GOT tag. *) let tags_and_ranges = (Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag) in (match tags_and_ranges with [] -> failwith "error: GOT element but no ABI feature GOT tag" | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), Some(got_el_name, (got_start_off, got_len)))] -> (* Find the slot corresponding to rr, if we have one. *) let got_addr = ((match got_el.startpos with Some addr -> addr | None -> failwith "GOT has no addr at reloc time" )) in (match rr.maybe_def_bound_to with Some (_, Some(d)) -> (match Lem_list.find_index (fun (symname, maybe_def) -> (Lem.option_equal (=) (Some(d)) maybe_def)) l with Some idx1 -> Nat_big_num.of_int idx1 | None -> failwith ("no GOT slot for reloc against `" ^ (rr.ref.ref_symname ^ "'")) ) | Some(_, None) -> (* HACK: look for the weak symname. Really want more (ref-based) labelling. *) (match Lem_list.find_index (fun (symname, _) -> symname = rr.ref.ref_symname) l with Some idx1 -> Nat_big_num.of_int idx1 | None -> failwith ("no GOT slot for reloc against undefined symbol `" ^ (rr.ref.ref_symname ^ "'")) ) | _ -> failwith "GOT: unbound def" ) | _ -> failwith "got bad GOT" ) )) (*val amd64_got_slot_addr : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural*) let amd64_got_slot_addr img2 rr:Nat_big_num.num= ((match Pmap.lookup ".got" img2.elements with None -> (* got no GOT? okay... *) failwith "got no GOT" | Some got_el -> (* Find the GOT tag. *) let tags_and_ranges = (Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag) in (match tags_and_ranges with [] -> failwith "error: GOT element but no ABI feature GOT tag" | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), Some(got_el_name, (got_start_off, got_len)))] -> (* Find the slot corresponding to rr, if we have one. *) let got_addr = ((match got_el.startpos with Some addr -> addr | None -> failwith "GOT has no addr at reloc time" )) in Nat_big_num.add (Nat_big_num.mul(Nat_big_num.of_int 8) (amd64_got_slot_idx img2 rr)) got_addr | _ -> failwith "got bad GOT" ) )) (*val amd64_plt_slot_addr : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural -> natural*) let amd64_plt_slot_addr img2 rr raw_addr:Nat_big_num.num= ((match Pmap.lookup ".plt" img2.elements with None -> (* got no PLT? okay... under static linking this can happen. We use the actual symbol address of the *) (*let _ = errln "Warning: no PLT, so attempting to use actual symbol address as PLT slot address" in*) (* if raw_addr = 0 then failwith "bailing rather than resolving PLT slot to null address (perhaps conservatively)" else *) raw_addr | Some plt_el -> (* Find the PLT tag. *) let tags_and_ranges = (Multimap.lookupBy0 (instance_Basic_classes_Ord_Memory_image_range_tag_dict instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict (instance_Basic_classes_Ord_tup2_dict Lem_string_extra.instance_Basic_classes_Ord_string_dict (instance_Basic_classes_Ord_tup2_dict instance_Basic_classes_Ord_Num_natural_dict instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0([])))) img2.by_tag) in (match tags_and_ranges with [] -> failwith "error: PLT element but no ABI feature PLT tag" | [(AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0(l))), Some(plt_el_name, (plt_start_off, plt_len)))] -> let plt_addr = ((match plt_el.startpos with Some addr -> addr | None -> failwith "PLT has no addr at reloc time" )) in (* Find the slot corresponding to rr, if we have one. *) (match rr.maybe_def_bound_to with Some (_, Some(d)) -> (match Lem_list.mapMaybe (fun (symname, maybe_def, fn) -> if (Lem.option_equal (=) (Some(d)) maybe_def) then Some fn else None) l with [fn] -> let got_addr = ((match Pmap.lookup ".got" img2.elements with None -> (* got no GOT? okay... *) failwith "got no GOT (applying PLT calculation)" | Some got_el -> (match got_el.startpos with Some addr -> addr | None -> failwith "concrete GOT has no addr" ) )) in let (addr, content) = (fn got_addr plt_addr) in (*let _ = errln ("Calculated PLT slot for `" ^ d.def_symname ^ "', from PLT addr " ^ (hex_string_of_natural plt_addr) ^ " and GOT addr " ^ (hex_string_of_natural got_addr) ^ ", as " ^ (hex_string_of_natural addr)) in*) addr | [] -> (* failwith ("internal error: no PLT entry for reloc against `" ^ rr.ref.ref_symname ^ "'") *) (* If we got no PLT slot, we assume it's because the PLT entry was optimised out. * So we just return the address of the symbol itself. *) (*let _ = errln ("No PLT entry for reloc against `" ^ rr.ref.ref_symname ^ "', which we assume was optimised to avoid the GOT") in*) (match Memory_image_orderings.find_defs_matching instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict d img2 with [] ->Nat_big_num.of_int 0 (* HMM -- should be an error? *) | [(Some(el_name, (start_off, len)), matching_d)] -> (match element_and_offset_to_address (el_name, start_off) img2 with Some a -> a | None -> failwith ("internal error: could not get address for PLT-short-circuited symbol `" ^ (rr.ref.ref_symname ^ "'")) ) | _ -> failwith ("output image has multiple and/or no-location definitions to which via-PLT ref to `" ^ (rr.ref.ref_symname ^ "' could resolve")) ) | _ -> failwith ("internal error: multiple PLT entries for reloc against `" ^ (rr.ref.ref_symname ^ "'")) ) | Some(_, None) ->Nat_big_num.of_int (* weak, so 0 *)0 | _ -> failwith "PLT: unbound def" ) | _ -> failwith "got bad PLT" ) )) (** [amd64_reloc r] yields a function that applies relocations of type [r]. *) (*val amd64_reloc : reloc_fn any_abi_feature*) let amd64_reloc r:bool*((any_abi_feature)annotated_memory_image ->Nat_big_num.num ->symbol_reference_and_reloc_site ->Nat_big_num.num*(Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num))= ((match (string_of_amd64_relocation_type r) with | "R_X86_64_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 0, (fun s -> fun a -> fun e -> e)))))) | "R_X86_64_64" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8, (fun s -> fun a -> fun e -> i2n ( Nat_big_num.add(n2i s) a))))))) | "R_X86_64_PC32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.sub( Nat_big_num.add(n2i s) a) (n2i site_addr)))))))) | "R_X86_64_GOT32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.add(n2i (amd64_got_slot_idx img2 rr)) a))))))) | "R_X86_64_PLT32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_plt_slot_addr img2 rr s)) a) (n2i site_addr))) )))) ) | "R_X86_64_COPY" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (size_of_copy_reloc img2 rr, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GLOB_DAT" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (size_of_def rr, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_JUMP_SLOT" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_RELATIVE" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GOTPCREL" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_got_slot_addr img2 rr)) a) (n2i site_addr))) )))) ) | "R_X86_64_32" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n ( Nat_big_num.add(n2i s) a))))))) | "R_X86_64_32S" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.add(n2i s) a))))))) | "R_X86_64_16" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 2, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_PC16" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 2, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_8" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 1, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_PC8" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 1, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_DTPMOD64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_DTPOFF64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_TPOFF64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> i2n_signed( 64) (Nat_big_num.sub(Nat_big_num.of_int 0)(Nat_big_num.of_int 8))) (* FIXME *)))))) | "R_X86_64_TLSGD" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_TLSLD" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_DTPOFF32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GOTTPOFF" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> i2n_signed( 32) ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_got_slot_addr img2 rr)) a) (n2i site_addr)))))))) | "R_X86_64_TPOFF32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_PC64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GOTOFF64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GOTPC32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_SIZE32" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_SIZE64" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8, (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_GOTPC32_TLSDESC" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_TLSDESC_CALL" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 4 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_TLSDESC" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | "R_X86_64_IRELATIVE" -> (true, (fun img2 -> (fun site_addr -> (fun rr -> (Nat_big_num.of_int 8 (* CHECK *), (fun s -> fun a -> fun e -> e) (* FIXME *)))))) | _ -> failwith "unrecognised relocation" )) (*val sysv_amd64_std_abi : abi any_abi_feature*) let sysv_amd64_std_abi:(any_abi_feature)abi= ({ is_valid_elf_header = header_is_amd64 ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none(Nat_big_num.of_int 0) elf_ma_x86_64) ; reloc = amd64_reloc ; section_is_special = section_is_special0 ; section_is_large = (fun s -> (fun f -> flag_is_set shf_x86_64_large s.elf64_section_flags)) ; maxpagesize =(Nat_big_num.of_int 65536) ; minpagesize =(Nat_big_num.of_int 4096) ; commonpagesize =(Nat_big_num.of_int 4096) (* XXX: DPM, changed from explicit reference to null_abi field due to problems in HOL4. *) ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_") ; make_phdrs = make_default_phdrs ; max_phnum =(Nat_big_num.of_int 2) (* incremented by extensions *) ; guess_entry_point = (find_start_symbol_address instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) ; pad_data = pad_zeroes ; pad_code = pad_0x90 ; generate_support = amd64_generate_support ; concretise_support = amd64_concretise_support ; get_reloc_symaddr = amd64_get_reloc_symaddr }) (*val sysv_aarch64_le_std_abi : abi any_abi_feature*) let sysv_aarch64_le_std_abi:(any_abi_feature)abi= ({ is_valid_elf_header = header_is_aarch64_le ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none(Nat_big_num.of_int 0) elf_ma_aarch64) ; reloc = aarch64_le_reloc ; section_is_special = section_is_special0 ; section_is_large = (fun _ -> (fun _ -> false)) ; maxpagesize = (Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 256))(Nat_big_num.of_int 4096)) (* 2MB; bit of a guess, based on gdb and prelink code *) ; minpagesize =(Nat_big_num.of_int 1024) (* bit of a guess again *) ; commonpagesize =(Nat_big_num.of_int 4096) ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_") ; make_phdrs = make_default_phdrs ; max_phnum =(Nat_big_num.of_int 2) (* incremented by extensions *) ; guess_entry_point = (find_start_symbol_address instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) ; pad_data = pad_zeroes ; pad_code = pad_zeroes ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ()) ; concretise_support = (fun img2 -> img2) ; get_reloc_symaddr = (default_get_reloc_symaddr instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) }) (*val all_abis : list (abi any_abi_feature)*) let all_abis:((any_abi_feature)abi)list= ([sysv_amd64_std_abi; sysv_aarch64_le_std_abi; null_abi])