diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/abis/abis.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/abis/abis.ml | 1420 |
1 files changed, 0 insertions, 1420 deletions
diff --git a/lib/ocaml_rts/linksem/abis/abis.ml b/lib/ocaml_rts/linksem/abis/abis.ml deleted file mode 100644 index 0cbd92d8..00000000 --- a/lib/ocaml_rts/linksem/abis/abis.ml +++ /dev/null @@ -1,1420 +0,0 @@ -(*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 <puts@got.plt> - 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 <check_one_fd.part.0> - - * ... 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]) - |