diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_memory_image.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_memory_image.ml | 315 |
1 files changed, 0 insertions, 315 deletions
diff --git a/lib/ocaml_rts/linksem/elf_memory_image.ml b/lib/ocaml_rts/linksem/elf_memory_image.ml deleted file mode 100644 index d408c358..00000000 --- a/lib/ocaml_rts/linksem/elf_memory_image.ml +++ /dev/null @@ -1,315 +0,0 @@ -(*Generated by Lem from elf_memory_image.lem.*) -open Lem_basic_classes -open Lem_function -open Lem_string -open Lem_tuple -open Lem_bool -open Lem_list -open Lem_sorting -open Lem_map -(*import Set*) -open Lem_num -open Lem_maybe -open Lem_assert_extra - -open Byte_sequence -open Default_printing -open Error -open Missing_pervasives -open Show -open Endianness - -open Elf_header -open Elf_file -open Elf_interpreted_section -open Elf_interpreted_segment -open Elf_section_header_table -open Elf_program_header_table -open Elf_symbol_table -open Elf_types_native_uint -open Elf_relocation -open String_table - -open Memory_image -open Abis - -type elf_memory_image = any_abi_feature annotated_memory_image - -let elf_section_is_special0 s f:bool= (not (Nat_big_num.equal s.elf64_section_type sht_progbits) - && not (Nat_big_num.equal s.elf64_section_type sht_nobits)) - -(*val noop_reloc : forall 'abifeature. natural -> ((maybe elf64_symbol_table_entry -> natural) * (annotated_memory_image 'abifeature -> maybe natural))*) -let noop_reloc0 r:((elf64_symbol_table_entry)option ->Nat_big_num.num)*('abifeature annotated_memory_image ->(Nat_big_num.num)option)= ((fun r_type ->Nat_big_num.of_int 8), (fun sym_val -> None)) - -let empty_elf_memory_image:(any_abi_feature)annotated_memory_image= ({ - elements = (Pmap.empty compare) - ; by_range = (Pset.empty (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare)) - ; by_tag = (Pset.empty (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))))) -}) - -(* HMM. For the elf_ident, I don't really want to express it this way. - * I want something more bidirectional: something that can tell me - * not only that a given ident is valid for a given ABI, but also, - * to *construct* an ident for a given abstract ELF file satisfying x. - * This is very much like a lens. - * - * Similarly for relocs, I might want a way to map back to an allowable - * *concrete* representation, from some *abstract* description of the - * reloc's intent (i.e. a symbol binding: "point this reference at symbol - * Foo"), given the constraints imposed by the ABI (such as "use only - * RELA, not rel". FIXME: figure out how to lensify what we're doing. *) - -type elf_range_tag = any_abi_feature range_tag - -let null_section_header_table:elf_file_feature= (ElfSectionHeaderTable([])) -let null_program_header_table:elf_file_feature= (ElfProgramHeaderTable([])) -let null_elf_header:elf64_header= ({ - elf64_ident = ([]) - ; elf64_type = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_machine = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_version = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_entry = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_phoff = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_shoff = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; 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 0))) - ; elf64_phentsize= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_phnum = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_shentsize= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_shnum = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_shstrndx = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - }) - -(* Here we build the image of a file in file offset space. - * To transform to memory space, we - * - * - switch positions to be addresses - * - switch lengths of nobits etc. to be memory lengths - * - PROBLEM: an offset might map to >1 virtual address. - * So we have to clone it as multiple elements. - * Each gets a label identifying the "file feature" it came from - * -- i.e. sections, ELF header, SHT and PHT are all file features. - * - PROBLEM: the memory image might only contain part of an element. - * We need to reflect this truncatedness somehow in the label. - * - * Is the offset-space view really useful? - * SORT OF: want to be able to make an image out of relocatable ELF files - * that have no address assignments or phdrs yet. - * AHA. NO. This is not an offset-space view; it's a sectionwise memory view. - * All allocatable sections become elements with Nothing as their address. - * The remainder of the ELF file *should* be represented as labels. - * But, hmm, some stuff like the ELF header and SHT will likely get discarded. - * - * In short, we should work entirely with memory space. - * Then - * - * - do we want to encode the aliasing of multiple virtual addresses - * down to single "features" in offset-space, like multiple mappings - * of the ELF header, say? - *) - -(*val offset_to_vaddr_mappings : elf64_file -> natural -> list (natural * elf64_interpreted_segment)*) -let offset_to_vaddr_mappings f off:(Nat_big_num.num*elf64_interpreted_segment)list= - (Lem_list.mapMaybe (fun ph -> - if Nat_big_num.greater_equal off ph.elf64_segment_offset - && Nat_big_num.less off (Nat_big_num.add ph.elf64_segment_base ph.elf64_segment_size) - then Some ( Nat_big_num.add ph.elf64_segment_base ( Nat_big_num.sub_nat off ph.elf64_segment_offset), ph) - else None - ) f.elf64_file_interpreted_segments) - -(*val gensym : string -> string*) -let gensym hint:string= hint (* FIXME: remember duplicates *) - -(*val extract_symbol : (elf64_symbol_table * string_table * natural) -> natural -> maybe (string * elf64_symbol_table_entry)*) -let extract_symbol symtab_triple symidx:(string*elf64_symbol_table_entry)option= - (let (symtab, strtab, scnidx) = symtab_triple - in - (match Ml_bindings.list_index_big_int symidx symtab with - Some ent -> - (match (get_string_at (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_name)) strtab) with - Success str -> Some (str, ent) - | Fail _ -> Some ("", ent) (* ELF doesn't distinguish "no string" from "empty string" *) - ) - | None -> None - )) - -(*val extract_satisfying_symbols : (elf64_symbol_table * string_table * natural) -> - (elf64_symbol_table_entry -> bool) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*) -let extract_satisfying_symbols symtab_triple pred:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list= - (let (symtab, strtab, scnidx) = symtab_triple - in - (*let _ = Missing_pervasives.errln ("extracting satisfying symbols from symtab index " ^ (show scnidx) ^ ", size " - ^ (show (length symtab)) ) - in*) - mapMaybei (fun symidx -> (fun ent -> - ((match (get_string_at (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_name)) strtab) with - Success str -> - (* exclude those that don't match *) - if (pred ent) - then Some(str, ent, scnidx, symidx) - else None - | Fail s -> (*let _ = Missing_pervasives.errln ("couldn't get string from strtab of symtab with index " ^ (show scnidx) - ^ ": " ^ s) in *) - None - )) - )) symtab) - -(*val extract_all_symbols : (elf64_symbol_table * string_table * natural) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*) -let extract_all_symbols symtab_triple:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list= (extract_satisfying_symbols symtab_triple (fun _ -> true)) - -let definitions_pred:elf64_symbol_table_entry ->bool= (fun ent -> not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_shndx)) stn_undef)) -let references_pred:elf64_symbol_table_entry ->bool= (fun ent -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_shndx)) stn_undef && (not (is_elf64_null_entry ent))) - -(*val extract_definitions_from_symtab_of_type : natural -> elf64_file -> list symbol_definition*) -let extract_definitions_from_symtab_of_type t e:(symbol_definition)list= - ((match (find_elf64_symtab_by_type t e >>= (fun symtab -> ( - let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list) - = (extract_satisfying_symbols symtab definitions_pred) - in - let (extracted : symbol_definition list) - = (mapMaybei (fun i -> (fun (str, ent, scnidx, symidx) -> Some { - def_symname = str - ; def_syment = ent - ; def_sym_scn = scnidx - ; def_sym_idx = symidx - ; def_linkable_idx =(Nat_big_num.of_int 0) - })) allsyms) - in return extracted - ))) with Fail _ -> [] | Success x -> x )) - -(*val extract_references_from_symtab_of_type : natural -> elf64_file -> list symbol_reference*) -let extract_references_from_symtab_of_type t e:(symbol_reference)list= - ((match (find_elf64_symtab_by_type t e >>= (fun symtab -> ( - let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list) - = (extract_satisfying_symbols symtab references_pred) - in - let (extracted : symbol_reference list) = - (mapMaybei (fun symidx -> (fun (str, ent, scnidx, symidx) -> Some { - ref_symname = str - ; ref_syment = ent - ; ref_sym_scn = scnidx - ; ref_sym_idx = symidx - })) allsyms) - in - (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length allsyms)) ^ " undefined references: " - ^ (show (List.map (fun (str, _, scnidx, symidx) -> (str, scnidx, symidx)) allsyms)) ^ "\n") -(* ^ " (syminds " - ^ (show (List.map (fun extracted -> extracted.ref_sym_idx) x)) ^ ", symnames " - ^ (show (List.map (fun extracted -> extracted.ref_symname) x)) ^ ")") *) - - in*) return extracted - ))) with Fail _ -> [] | Success x -> x )) - -(*val extract_all_relocs : string -> elf64_file -> list (natural (* scn *) * natural (* rel idx *) * natural (* rel src scn *) * elf64_relocation_a)*) -let extract_all_relocs fname1 e:(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*elf64_relocation_a)list= - (let (all_rel_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 -> - if Nat_big_num.equal isec1.elf64_section_type sht_rel then Some (i, isec1) else None - )) e.elf64_file_interpreted_sections) - in - (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rel_sections)) ^ - " rel sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rel_sections)) ^ ")") - in*) - let (all_rela_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 -> - if Nat_big_num.equal isec1.elf64_section_type sht_rela then Some (i, isec1) else None - )) e.elf64_file_interpreted_sections) - in - (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rela_sections)) ^ - " rela sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rela_sections)) ^ ")") - in*) - let rel_to_rela = (fun rel -> { - elf64_ra_offset = (rel.elf64_r_offset) - ; elf64_ra_info = (rel.elf64_r_info) - ; elf64_ra_addend = (Nat_big_num.to_int64(Nat_big_num.of_int 0)) - }) - in - let endian = (get_elf64_header_endianness e.elf64_file_header) - in - (* Build per-section lists of rels paired with their originating section id. - * We also pair each element with its index *in that section*, and then flatten - * the whole lot using mapConcat. *) - let (all_rels_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) -> - (match read_elf64_relocation_section isec1.elf64_section_size endian isec1.elf64_section_body - with - Success (relocs, _) -> - (*let _ = Missing_pervasives.errln ("Rel section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^ - " entries") - in*) - mapMaybei (fun idx1 -> (fun rel -> Some (scn, idx1, isec1.elf64_section_info, rel_to_rela rel))) relocs - | Fail _ -> [] - )) all_rel_sections) - in - let (all_relas_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) -> - (match read_elf64_relocation_a_section isec1.elf64_section_size endian isec1.elf64_section_body - with - Success (relocs, _) -> - (*let _ = Missing_pervasives.errln ("Rela section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^ - " entries") - in*) - mapMaybei (fun idx1 -> (fun rela -> Some (scn, idx1, isec1.elf64_section_info, rela))) relocs - | Fail _ -> [] - )) all_rela_sections) - in - List.rev_append (List.rev all_rels_list) all_relas_list) - -(*val extract_all_relocs_as_symbol_references : string -> elf64_file -> list symbol_reference_and_reloc_site*) -let extract_all_relocs_as_symbol_references fname1 e:(symbol_reference_and_reloc_site)list= -(let all_relocs = (extract_all_relocs fname1 e) - in - let all_symtab_triples_by_scnidx = (mapMaybei (fun scnidx -> (fun isec1 -> - if Nat_big_num.equal isec1.elf64_section_type sht_symtab - then - let found = (find_elf64_symbols_by_symtab_idx scnidx e) - in - (match found with - Fail _ -> None - | Success triple -> Some (scnidx, triple) - ) - else None - )) e.elf64_file_interpreted_sections) - in - let (all_extracted_symtabs_by_scnidx : ( (Nat_big_num.num, ( (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *))list))Pmap.map)) - = (List.fold_left (fun acc -> (fun (scnidx, triple) -> Pmap.add scnidx (extract_all_symbols triple) acc)) (Pmap.empty Nat_big_num.compare) all_symtab_triples_by_scnidx) - in - (*let _ = Missing_pervasives.errln ("All extracted symtabs by scnidx: " ^ (show (Set_extra.toList (Map.toSet all_extracted_symtabs_by_scnidx)))) - in*) - let ref_for_relocation_a_in_section_index = (fun rel_scn_idx -> (fun rel_idx -> (fun rela -> - let rela_isec = ((match Ml_bindings.list_index_big_int rel_scn_idx e.elf64_file_interpreted_sections with - Some x -> x - | None -> failwith "relocation references nonexistent section" - )) - in - let symtab_idx = (rela_isec.elf64_section_link) - in - (match Pmap.lookup symtab_idx all_extracted_symtabs_by_scnidx with - None -> failwith "referenced symtab does not exist" - | Some quads -> - let sym_idx = (get_elf64_relocation_a_sym rela) - in - let maybe_quad = (Ml_bindings.list_index_big_int sym_idx quads) - in - (match maybe_quad with - Some(symname, syment, scnidx, symidx) -> { - ref_symname = symname - ; ref_syment = syment - ; ref_sym_scn = symtab_idx - ; ref_sym_idx = sym_idx - } - | None -> failwith "reloc references symbol that does not exist" (*("reloc at index " ^ (show rel_idx) ^ " references symbol (index " ^ (show sym_idx) ^ - ") that does not exist: symtab (index " ^ (show symtab_idx) ^ ") has " ^ (show (length quads)) ^ " entries")*) - ) - ) - ))) - in - (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length all_relocs)) ^ " reloc references (rel_scn, rel_idx, src_scn): " - ^ (show (List.map (fun (rel_scn, rel_idx, srcscn, rela) -> (rel_scn, rel_idx, srcscn)) all_relocs)) ^ "\n") - in*) - Lem_list.map (fun (scn, idx1, srcscn, rela) -> { - ref = ( (* NOTE that a reference is not necessarily to an undefined symbol! *)ref_for_relocation_a_in_section_index scn idx1 rela) - ; maybe_reloc = (Some - { ref_relent = rela - ; ref_rel_scn = scn - ; ref_rel_idx = idx1 - ; ref_src_scn = srcscn (* what section does the reference come from? it's the 'info' link of the rel section header *) - }) - ; maybe_def_bound_to = None - }) all_relocs) |