(*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)