Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file elf_loader.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224(****************************************************************************)(* Sail *)(* *)(* Sail and the Sail architecture models here, comprising all files and *)(* directories except the ASL-derived Sail code in the aarch64 directory, *)(* are subject to the BSD two-clause licence below. *)(* *)(* The ASL derived parts of the ARMv8.3 specification in *)(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *)(* *)(* Copyright (c) 2013-2021 *)(* Kathyrn Gray *)(* Shaked Flur *)(* Stephen Kell *)(* Gabriel Kerneis *)(* Robert Norton-Wright *)(* Christopher Pulte *)(* Peter Sewell *)(* Alasdair Armstrong *)(* Brian Campbell *)(* Thomas Bauereiss *)(* Anthony Fox *)(* Jon French *)(* Dominic Mulligan *)(* Stephen Kell *)(* Mark Wassell *)(* Alastair Reid (Arm Ltd) *)(* *)(* All rights reserved. *)(* *)(* This work was partially supported by EPSRC grant EP/K008528/1 <a *)(* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous *)(* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA *)(* KTF funding, and donations from Arm. This project has received *)(* funding from the European Research Council (ERC) under the European *)(* Union’s Horizon 2020 research and innovation programme (grant *)(* agreement No 789108, ELVER). *)(* *)(* This software was developed by SRI International and the University of *)(* Cambridge Computer Laboratory (Department of Computer Science and *)(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *)(* and FA8750-10-C-0237 ("CTSRD"). *)(* *)(* SPDX-License-Identifier: BSD-2-Clause *)(****************************************************************************)moduleBig_int=Nat_big_numletopt_elf_threads=ref1letopt_elf_entry=refBig_int.zeroletopt_elf_tohost=refBig_int.zero(* the type of elf last loaded, and its symbol map *)typeelf_class=ELF_Class_64|ELF_Class_32letopt_elf_class=refELF_Class_64(* default *)letopt_symbol_map=ref([]:Elf_file.global_symbol_init_info)typeword8=intletescape_charc=ifint_of_charc<=31then'.'elseifint_of_charc>=127then'.'elseclethex_linebs=lethex_charic=(ifimod2==0&&i<>0then" "else"")^Printf.sprintf"%02x"(int_of_charc)inString.concat""(List.mapihex_charbs)^" "^String.concat""(List.map(func->Printf.sprintf"%c"(escape_charc))bs)letbreaknxs=letrechelperacc=function|[]->List.revacc|_::_asxs->helper([Lem_list.takenxs]@acc)(Lem_list.dropnxs)inhelper[]xsletprint_segmentbs=prerr_endline"0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";List.iter(funbs->prerr_endline(hex_linebs))(break16(Byte_sequence.char_list_of_byte_sequencebs))typeelf_segs=|ELF64ofElf_interpreted_segment.elf64_interpreted_segmentlist|ELF32ofElf_interpreted_segment.elf32_interpreted_segmentlistletreadname=letinfo=Sail_interface.populate_and_obtain_global_symbol_init_infonameinprerr_endline"Elf read:";letelf_file,elf_epi,symbol_map=beginmatchinfowith|Error.Fails->failwith(Printf.sprintf"populate_and_obtain_global_symbol_init_info: %s"s)|Error.Success((elf_file:Elf_file.elf_file),(elf_epi:Sail_interface.executable_process_image),(symbol_map:Elf_file.global_symbol_init_info))->(* XXX disabled because it crashes if entry_point overflows an ocaml int :-(
prerr_endline (Sail_interface.string_of_executable_process_image elf_epi);*)(elf_file,elf_epi,symbol_map)endinprerr_endline"\nElf segments:";(* remove all the auto generated segments (they contain only 0s) *)letprune_segmentssegs=Lem_list.mapMaybe(fun(seg,prov)->ifprov=Elf_file.FromELFthenSomesegelseNone)segsinletsegments,e_entry,_e_machine=beginmatch(elf_epi,elf_file)with|Sail_interface.ELF_Class_32(segments,e_entry,e_machine),Elf_file.ELF_File_32_->(ELF32(prune_segmentssegments),e_entry,e_machine)|Sail_interface.ELF_Class_64(segments,e_entry,e_machine),Elf_file.ELF_File_64_->(ELF64(prune_segmentssegments),e_entry,e_machine)|_,_->failwith"cannot handle ELF file"endin(segments,e_entry,symbol_map)letwrite_sail_libpaddribyte=Sail_lib.wram(Big_int.addpaddr(Big_int.of_inti))byteletwrite_mem_zerosstartlen=(* write in order for mem tracing logs *)leti=refBig_int.zeroinwhileBig_int.less!ilendoSail_lib.wram(Big_int.addstart!i)0;i:=Big_int.succ!idoneletwrite_filechanpaddribyte=output_stringchan(Big_int.to_string(Big_int.addpaddr(Big_int.of_inti))^"\n");output_stringchan(string_of_intbyte^"\n")letprint_seg_infooffsetbasepaddrsizememsz=prerr_endline"\nLoading Segment";prerr_endline("Segment offset: "^Printf.sprintf"0x%Lx"(Big_int.to_int64offset));prerr_endline("Segment base address: "^Big_int.to_stringbase);(* NB don't attempt to convert paddr to int64 because on MIPS it is quite likely to exceed signed
64-bit range e.g. addresses beginning 0x9.... Really need to_uint64 or to_string_hex but lem
doesn't have them. *)prerr_endline("Segment physical address: "^Printf.sprintf"0x%Lx"(Big_int.to_int64paddr));prerr_endline("Segment size: "^Printf.sprintf"0x%Lx"(Big_int.to_int64size));prerr_endline("Segment memsz: "^Printf.sprintf"0x%Lx"(Big_int.to_int64memsz))letload_segment?(writer=write_sail_lib)bspaddrbaseoffsetsizememsz=print_seg_infooffsetbasepaddrsizememsz;print_segmentbs;List.iteri(writerpaddr)(List.rev_mapint_of_char(List.rev(Byte_sequence.char_list_of_byte_sequencebs)));write_mem_zeros(Big_int.addpaddrsize)(Big_int.submemszsize)letload_elf?(writer=write_sail_lib)name=letsegments,e_entry,symbol_map=readnameinopt_elf_entry:=e_entry;opt_symbol_map:=symbol_map;ifList.mem_assoc"tohost"symbol_mapthen(let_,_,tohost_addr,_,_=List.assoc"tohost"symbol_mapinopt_elf_tohost:=tohost_addr);matchsegmentswith|ELF64segs->List.iter(funseg->letopenElf_interpreted_segmentinletbs=seg.elf64_segment_bodyinletpaddr=seg.elf64_segment_paddrinletbase=seg.elf64_segment_baseinletoffset=seg.elf64_segment_offsetinletsize=seg.elf64_segment_sizeinletmemsz=seg.elf64_segment_memszinload_segment~writerbspaddrbaseoffsetsizememsz)segs;opt_elf_class:=ELF_Class_64|ELF32segs->List.iter(funseg->letopenElf_interpreted_segmentinletbs=seg.elf32_segment_bodyinletpaddr=seg.elf32_segment_paddrinletbase=seg.elf32_segment_baseinletoffset=seg.elf32_segment_offsetinletsize=seg.elf32_segment_sizeinletmemsz=seg.elf32_segment_memszinload_segment~writerbspaddrbaseoffsetsizememsz)segs;opt_elf_class:=ELF_Class_32letload_binary?(writer=write_sail_lib)addrname=letf=open_in_binnameinletbuf=Buffer.create1024intrywhiletruedoletchar=input_charfinBuffer.add_charbufchardone;assertfalsewith|End_of_file->beginBytes.iteri(funich->writeraddri(int_of_charch))(Buffer.to_bytesbuf);close_infend|exc->close_inf;raiseexc(* The sail model can access this by externing a unit -> int function
as Elf_loader.elf_entry. *)letelf_entry()=!opt_elf_entry(* Used by RISCV sail model test harness for exiting test *)letelf_tohost()=!opt_elf_tohost(* Used to check last loaded elf class. *)letelf_class()=!opt_elf_class(* Lookup the address for a symbol *)letelf_symbolsymbol=ifList.mem_assocsymbol!opt_symbol_mapthen(let_,_,addr,_,_=List.assocsymbol!opt_symbol_mapinSomeaddr)elseNone(* Get all symbols *)letelf_symbols()=!opt_symbol_map