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, 1420 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/abis/abis.ml b/lib/ocaml_rts/linksem/abis/abis.ml new file mode 100644 index 00000000..0cbd92d8 --- /dev/null +++ b/lib/ocaml_rts/linksem/abis/abis.ml @@ -0,0 +1,1420 @@ +(*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]) + |