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