Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file elf_memory_image.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322(*Generated by Lem from elf_memory_image.lem.*)openLem_basic_classesopenLem_functionopenLem_stringopenLem_tupleopenLem_boolopenLem_listopenLem_sortingopenLem_map(*import Set*)openLem_numopenLem_maybeopenLem_assert_extraopenByte_sequenceopenDefault_printingopenErroropenMissing_pervasivesopenShowopenEndiannessopenElf_headeropenElf_fileopenElf_interpreted_sectionopenElf_interpreted_segmentopenElf_section_header_tableopenElf_program_header_tableopenElf_symbol_tableopenElf_types_native_uintopenElf_relocationopenString_tableopenMemory_imageopenAbistypeelf_memory_image=any_abi_featureannotated_memory_imageletelf_section_is_special0sf:bool=(not(Nat_big_num.equals.elf64_section_typesht_progbits)&¬(Nat_big_num.equals.elf64_section_typesht_nobits))(*val noop_reloc : forall 'abifeature. natural -> ((maybe elf64_symbol_table_entry -> natural) * (annotated_memory_image 'abifeature -> maybe natural))*)letnoop_reloc0r:((elf64_symbol_table_entry)option->Nat_big_num.num)*('abifeatureannotated_memory_image->(Nat_big_num.num)option)=((funr_type->(Nat_big_num.of_int8)),(funsym_val->None))letempty_elf_memory_image:(any_abi_feature)annotated_memory_image=({elements=(Pmap.emptycompare);by_range=(Pset.empty(pairCompare(maybeCompare(pairComparecompare(pairCompareNat_big_num.compareNat_big_num.compare)))compare));by_tag=(Pset.empty(pairComparecompare(maybeCompare(pairComparecompare(pairCompareNat_big_num.compareNat_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. *)typeelf_range_tag=any_abi_featurerange_tagletnull_section_header_table:elf_file_feature=(ElfSectionHeaderTable([]))letnull_program_header_table:elf_file_feature=(ElfProgramHeaderTable([]))letnull_elf_header:elf64_header=({elf64_ident=([]);elf64_type=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_machine=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_version=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_entry=(Uint64_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_phoff=(Uint64_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_shoff=(Uint64_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_flags=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_ehsize=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_phentsize=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_phnum=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_shentsize=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_shnum=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)));elf64_shstrndx=(Uint32_wrapper.of_bigint((Nat_big_num.of_int0)))})(* 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)*)letoffset_to_vaddr_mappingsfoff:(Nat_big_num.num*elf64_interpreted_segment)list=(Lem_list.mapMaybe(funph->ifNat_big_num.greater_equaloffph.elf64_segment_offset&&Nat_big_num.lessoff(Nat_big_num.addph.elf64_segment_baseph.elf64_segment_size)thenSome(Nat_big_num.addph.elf64_segment_base(Nat_big_num.sub_natoffph.elf64_segment_offset),ph)elseNone)f.elf64_file_interpreted_segments)(*val gensym : string -> string*)letgensymhint:string=hint(* FIXME: remember duplicates *)(*val extract_symbol : (elf64_symbol_table * string_table * natural) -> natural -> maybe (string * elf64_symbol_table_entry)*)letextract_symbolsymtab_triplesymidx:(string*elf64_symbol_table_entry)option=(let(symtab,strtab,scnidx)=symtab_triplein(matchMl_bindings.list_index_big_intsymidxsymtabwithSomeent->(match(get_string_at(Uint32_wrapper.to_bigintent.elf64_st_name)strtab)withSuccessstr->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 *))*)letextract_satisfying_symbolssymtab_triplepred:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=(let(symtab,strtab,scnidx)=symtab_triplein(*let _ = Missing_pervasives.errln ("extracting satisfying symbols from symtab index " ^ (show scnidx) ^ ", size "
^ (show (length symtab)) )
in*)mapMaybei(funsymidx->(funent->((match(get_string_at(Uint32_wrapper.to_bigintent.elf64_st_name)strtab)withSuccessstr->(* exclude those that don't match *)if(predent)thenSome(str,ent,scnidx,symidx)elseNone|Fails->(*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 *))*)letextract_all_symbolssymtab_triple:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=(extract_satisfying_symbolssymtab_triple(fun_->true))letdefinitions_pred:elf64_symbol_table_entry->bool=(funent->not(Nat_big_num.equal(Uint32_wrapper.to_bigintent.elf64_st_shndx)stn_undef))letreferences_pred:elf64_symbol_table_entry->bool=(funent->Nat_big_num.equal(Uint32_wrapper.to_bigintent.elf64_st_shndx)stn_undef&&(not(is_elf64_null_entryent)))(*val extract_definitions_from_symtab_of_type : natural -> elf64_file -> list symbol_definition*)letextract_definitions_from_symtab_of_typete:(symbol_definition)list=((match(bind(find_elf64_symtab_by_typete)(funsymtab->(let(allsyms:(string*elf64_symbol_table_entry*Nat_big_num.num(* scnidx *)*Nat_big_num.num(* symidx *))list)=(extract_satisfying_symbolssymtabdefinitions_pred)inlet(extracted:symbol_definitionlist)=(mapMaybei(funi->(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_int0))}))allsyms)inreturnextracted)))withFail_->[]|Successx->x))(*val extract_references_from_symtab_of_type : natural -> elf64_file -> list symbol_reference*)letextract_references_from_symtab_of_typete:(symbol_reference)list=((match(bind(find_elf64_symtab_by_typete)(funsymtab->(let(allsyms:(string*elf64_symbol_table_entry*Nat_big_num.num(* scnidx *)*Nat_big_num.num(* symidx *))list)=(extract_satisfying_symbolssymtabreferences_pred)inlet(extracted:symbol_referencelist)=(mapMaybei(funsymidx->(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*)returnextracted)))withFail_->[]|Successx->x))(*val extract_all_relocs : string -> elf64_file -> list (natural (* scn *) * natural (* rel idx *) * natural (* rel src scn *) * elf64_relocation_a)*)letextract_all_relocsfname1e:(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(funi->(funisec1->ifNat_big_num.equalisec1.elf64_section_typesht_relthenSome(i,isec1)elseNone))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(funi->(funisec1->ifNat_big_num.equalisec1.elf64_section_typesht_relathenSome(i,isec1)elseNone))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*)letrel_to_rela=(funrel->{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_int0)))})inletendian=(get_elf64_header_endiannesse.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)->(matchread_elf64_relocation_sectionisec1.elf64_section_sizeendianisec1.elf64_section_bodywithSuccess(relocs,_)->(*let _ = Missing_pervasives.errln ("Rel section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
" entries")
in*)mapMaybei(funidx1->(funrel->Some(scn,idx1,isec1.elf64_section_info,rel_to_relarel)))relocs|Fail_->[]))all_rel_sections)inlet(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)->(matchread_elf64_relocation_a_sectionisec1.elf64_section_sizeendianisec1.elf64_section_bodywithSuccess(relocs,_)->(*let _ = Missing_pervasives.errln ("Rela section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
" entries")
in*)mapMaybei(funidx1->(funrela->Some(scn,idx1,isec1.elf64_section_info,rela)))relocs|Fail_->[]))all_rela_sections)inList.rev_append(List.revall_rels_list)all_relas_list)(*val extract_all_relocs_as_symbol_references : string -> elf64_file -> list symbol_reference_and_reloc_site*)letextract_all_relocs_as_symbol_referencesfname1e:(symbol_reference_and_reloc_site)list=(letmaybe_guessed_abi=(Lem_list.list_find_opt(funabi1->abi1.is_valid_elf_headere.elf64_file_header)Abis.all_abis)inleta=((matchmaybe_guessed_abiwith|Somea->a|None->failwith"extract_all_relocs_as_symbol_references: unknown ABI"))inletall_relocs=(extract_all_relocsfname1e)inletall_symtab_triples_by_scnidx=(mapMaybei(funscnidx->(funisec1->ifNat_big_num.equalisec1.elf64_section_typesht_symtabthenletfound=(find_elf64_symbols_by_symtab_idxscnidxe)in(matchfoundwithFail_->None|Successtriple->Some(scnidx,triple))elseNone))e.elf64_file_interpreted_sections)inlet(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(funacc->(fun(scnidx,triple)->Pmap.addscnidx(extract_all_symbolstriple)acc))(Pmap.emptyNat_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*)letref_for_relocation_a_in_section_index=(funrel_scn_idx->(funrel_idx->(funrela->letrela_isec=((matchMl_bindings.list_index_big_intrel_scn_idxe.elf64_file_interpreted_sectionswithSomex->x|None->failwith"relocation references nonexistent section"))inletsymtab_idx=(rela_isec.elf64_section_link)in(matchPmap.lookupsymtab_idxall_extracted_symtabs_by_scnidxwithNone->failwith"referenced symtab does not exist"|Somequads->let(_,sym_idx)=(a.parse_reloc_inforela.elf64_ra_info)inletmaybe_quad=(Ml_bindings.list_index_big_intsym_idxquads)in(matchmaybe_quadwithSome(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_indexscnidx1rela);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)