diff options
| author | Alasdair Armstrong | 2017-09-07 16:54:20 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-09-07 16:54:20 +0100 |
| commit | 842165c1171fde332bd42e7520338c59a797f76b (patch) | |
| tree | 75b61297b6d9b6e4810542390eb1371afc2f183f /lib/ocaml_rts/linksem/elf_header.ml | |
| parent | 8124c487b576661dfa7a0833415d07d0978bc43e (diff) | |
Add ocaml run-time and updates to sail for ocaml backend
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_header.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_header.ml | 1508 |
1 files changed, 1508 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/elf_header.ml b/lib/ocaml_rts/linksem/elf_header.ml new file mode 100644 index 00000000..d8730e9c --- /dev/null +++ b/lib/ocaml_rts/linksem/elf_header.ml @@ -0,0 +1,1508 @@ +(*Generated by Lem from elf_header.lem.*) +(** [elf_header] includes types, functions and other definitions for working with + * ELF headers. + *) + +open Lem_basic_classes +open Lem_bool +open Lem_function +open Lem_list +open Lem_maybe +open Lem_num +open Lem_string +(*import Set*) + +open Lem_assert_extra + +open Default_printing +open Endianness + +open Elf_types_native_uint + +open Byte_sequence +open Error +open Missing_pervasives +open Show + +(** Special section header table indices *) + +(** [shn_undef]: marks an undefined, missing or irrelevant section reference. + * Present here instead of in elf_section_header_table.lem because a calculation + * below requires this constant (i.e. forward reference in the ELF spec). + *) +let shn_undef : Nat_big_num.num= (Nat_big_num.of_int 0) + +(** [shn_xindex]: an escape value. It indicates the actual section header index + * is too large to fit in the containing field and is located in another + * location (specific to the structure where it appears). Present here instead + * of in elf_section_header_table.lem because a calculation below requires this + * constant (i.e. forward reference in the ELF spec). + *) +let shn_xindex : Nat_big_num.num= (Nat_big_num.of_int 65535) (* 0xffff *) + +(** ELF object file types. Enumerates the ELF object file types specified in the + * System V ABI. Values between [elf_ft_lo_os] and [elf_ft_hi_os] inclusive are + * reserved for operating system specific values typically defined in an + * addendum to the System V ABI for that operating system. Values between + * [elf_ft_lo_proc] and [elf_ft_hi_proc] inclusive are processor specific and + * are typically defined in an addendum to the System V ABI for that processor + * series. + *) + +(** No file type *) +let elf_ft_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** Relocatable file *) +let elf_ft_rel : Nat_big_num.num= (Nat_big_num.of_int 1) +(** Executable file *) +let elf_ft_exec : Nat_big_num.num= (Nat_big_num.of_int 2) +(** Shared object file *) +let elf_ft_dyn : Nat_big_num.num= (Nat_big_num.of_int 3) +(** Core file *) +let elf_ft_core : Nat_big_num.num= (Nat_big_num.of_int 4) +(** Operating-system specific *) +let elf_ft_lo_os : Nat_big_num.num= (Nat_big_num.of_int 65024) (* 0xfe00 *) +(** Operating-system specific *) +let elf_ft_hi_os : Nat_big_num.num= (Nat_big_num.of_int 65279) (* 0xfeff *) +(** Processor specific *) +let elf_ft_lo_proc : Nat_big_num.num= (Nat_big_num.of_int 65280) (* 0xff00 *) +(** Processor specific *) +let elf_ft_hi_proc : Nat_big_num.num= (Nat_big_num.of_int 65535) (* 0xffff *) + +(** [string_of_elf_file_type os proc m] produces a string representation of the + * numeric encoding [m] of the ELF file type. For values reserved for OS or + * processor specific values, the higher-order functions [os] and [proc] are + * used for printing, respectively. + *) +(*val string_of_elf_file_type : (natural -> string) -> (natural -> string) -> natural -> string*) +let string_of_elf_file_type os_specific proc_specific m:string= + (if Nat_big_num.equal m elf_ft_none then + "No file type" + else if Nat_big_num.equal m elf_ft_rel then + "REL (Relocatable file)" + else if Nat_big_num.equal m elf_ft_exec then + "EXEC (Executable file)" + else if Nat_big_num.equal m elf_ft_dyn then + "DYN (Shared object file)" + else if Nat_big_num.equal m elf_ft_core then + "CORE (Core file)" + else if Nat_big_num.greater_equal m elf_ft_lo_os && Nat_big_num.less_equal m elf_ft_hi_os then + os_specific m + else if Nat_big_num.greater_equal m elf_ft_lo_proc && Nat_big_num.less_equal m elf_ft_hi_proc then + proc_specific m + else + "Invalid file type") + +(** [is_operating_specific_file_type_value] checks whether a numeric value is + * reserved by the ABI for operating system-specific purposes. + *) +(*val is_operating_system_specific_object_file_type_value : natural -> bool*) +let is_operating_system_specific_object_file_type_value v:bool= (Nat_big_num.greater_equal + v(Nat_big_num.of_int 65024) && Nat_big_num.less_equal v(Nat_big_num.of_int 65279)) + +(** [is_processor_specific_file_type_value] checks whether a numeric value is + * reserved by the ABI for processor-specific purposes. + *) +(*val is_processor_specific_object_file_type_value : natural -> bool*) +let is_processor_specific_object_file_type_value v:bool= (Nat_big_num.greater_equal + v(Nat_big_num.of_int 65280) && Nat_big_num.less_equal v(Nat_big_num.of_int 65535)) + +(** ELF machine architectures *) + +(** RISC-V *) +let elf_ma_riscv : Nat_big_num.num= (Nat_big_num.of_int 243) +(** AMD GPU architecture *) +let elf_ma_amdgpu : Nat_big_num.num= (Nat_big_num.of_int 224) +(** Moxie processor family *) +let elf_ma_moxie : Nat_big_num.num= (Nat_big_num.of_int 223) +(** FTDI Chip FT32 high performance 32-bit RISC architecture *) +let elf_ma_ft32 : Nat_big_num.num= (Nat_big_num.of_int 222) +(** Controls and Data Services VISIUMcore processor *) +let elf_ma_visium : Nat_big_num.num= (Nat_big_num.of_int 221) +(** Zilog Z80 *) +let elf_ma_z80 : Nat_big_num.num= (Nat_big_num.of_int 220) +(** CSR Kalimba architecture family *) +let elf_ma_kalimba : Nat_big_num.num= (Nat_big_num.of_int 219) +(** Nanoradio optimised RISC *) +let elf_ma_norc : Nat_big_num.num= (Nat_big_num.of_int 218) +(** iCelero CoolEngine *) +let elf_ma_cool : Nat_big_num.num= (Nat_big_num.of_int 217) +(** Cognitive Smart Memory Processor *) +let elf_ma_coge : Nat_big_num.num= (Nat_big_num.of_int 216) +(** Paneve CDP architecture family *) +let elf_ma_cdp : Nat_big_num.num= (Nat_big_num.of_int 215) +(** KM211 KVARC processor *) +let elf_ma_kvarc : Nat_big_num.num= (Nat_big_num.of_int 214) +(** KM211 KMX8 8-bit processor *) +let elf_ma_kmx8 : Nat_big_num.num= (Nat_big_num.of_int 213) +(** KM211 KMX16 16-bit processor *) +let elf_ma_kmx16 : Nat_big_num.num= (Nat_big_num.of_int 212) +(** KM211 KMX32 32-bit processor *) +let elf_ma_kmx32 : Nat_big_num.num= (Nat_big_num.of_int 211) +(** KM211 KM32 32-bit processor *) +let elf_ma_km32 : Nat_big_num.num= (Nat_big_num.of_int 210) +(** Microchip 8-bit PIC(r) family *) +let elf_ma_mchp_pic : Nat_big_num.num= (Nat_big_num.of_int 204) +(** XMOS xCORE processor family *) +let elf_ma_xcore : Nat_big_num.num= (Nat_big_num.of_int 203) +(** Beyond BA2 CPU architecture *) +let elf_ma_ba2 : Nat_big_num.num= (Nat_big_num.of_int 202) +(** Beyond BA1 CPU architecture *) +let elf_ma_ba1 : Nat_big_num.num= (Nat_big_num.of_int 201) +(** Freescale 56800EX Digital Signal Controller (DSC) *) +let elf_ma_5600ex : Nat_big_num.num= (Nat_big_num.of_int 200) +(** 199 Renesas 78KOR family *) +let elf_ma_78kor : Nat_big_num.num= (Nat_big_num.of_int 199) +(** Broadcom VideoCore V processor *) +let elf_ma_videocore5 : Nat_big_num.num= (Nat_big_num.of_int 198) +(** Renesas RL78 family *) +let elf_ma_rl78 : Nat_big_num.num= (Nat_big_num.of_int 197) +(** Open8 8-bit RISC soft processing core *) +let elf_ma_open8 : Nat_big_num.num= (Nat_big_num.of_int 196) +(** Synopsys ARCompact V2 *) +let elf_ma_arc_compact2 : Nat_big_num.num= (Nat_big_num.of_int 195) +(** KIPO_KAIST Core-A 2nd generation processor family *) +let elf_ma_corea_2nd : Nat_big_num.num= (Nat_big_num.of_int 194) +(** KIPO_KAIST Core-A 1st generation processor family *) +let elf_ma_corea_1st : Nat_big_num.num= (Nat_big_num.of_int 193) +(** CloudShield architecture family *) +let elf_ma_cloudshield : Nat_big_num.num= (Nat_big_num.of_int 192) +(** Infineon Technologies SLE9X core *) +let elf_ma_sle9x : Nat_big_num.num= (Nat_big_num.of_int 179) +(** Intel L10M *) +let elf_ma_l10m : Nat_big_num.num= (Nat_big_num.of_int 180) +(** Intel K10M *) +let elf_ma_k10m : Nat_big_num.num= (Nat_big_num.of_int 181) +(** ARM 64-bit architecture (AARCH64) *) +let elf_ma_aarch64 : Nat_big_num.num= (Nat_big_num.of_int 183) +(** Atmel Corporation 32-bit microprocessor family *) +let elf_ma_avr32 : Nat_big_num.num= (Nat_big_num.of_int 185) +(** STMicroelectronics STM8 8-bit microcontroller *) +let elf_ma_stm8 : Nat_big_num.num= (Nat_big_num.of_int 186) +(** Tilera TILE64 multicore architecture family *) +let elf_ma_tile64 : Nat_big_num.num= (Nat_big_num.of_int 187) +(** Tilera TILEPro multicore architecture family *) +let elf_ma_tilepro : Nat_big_num.num= (Nat_big_num.of_int 188) +(** Xilinix MicroBlaze 32-bit RISC soft processor core *) +let elf_ma_microblaze : Nat_big_num.num= (Nat_big_num.of_int 189) +(** NVIDIA CUDA architecture *) +let elf_ma_cuda : Nat_big_num.num= (Nat_big_num.of_int 190) +(** Tilera TILE-Gx multicore architecture family *) +let elf_ma_tilegx : Nat_big_num.num= (Nat_big_num.of_int 191) +(** Cypress M8C microprocessor *) +let elf_ma_cypress : Nat_big_num.num= (Nat_big_num.of_int 161) +(** Renesas R32C series microprocessors *) +let elf_ma_r32c : Nat_big_num.num= (Nat_big_num.of_int 162) +(** NXP Semiconductors TriMedia architecture family *) +let elf_ma_trimedia : Nat_big_num.num= (Nat_big_num.of_int 163) +(** QUALCOMM DSP6 processor *) +let elf_ma_qdsp6 : Nat_big_num.num= (Nat_big_num.of_int 164) +(** Intel 8051 and variants *) +let elf_ma_8051 : Nat_big_num.num= (Nat_big_num.of_int 165) +(** STMicroelectronics STxP7x family of configurable and extensible RISC processors *) +let elf_ma_stxp7x : Nat_big_num.num= (Nat_big_num.of_int 166) +(** Andes Technology compact code size embedded RISC processor family *) +let elf_ma_nds32 : Nat_big_num.num= (Nat_big_num.of_int 167) +(** Cyan Technology eCOG1X family *) +let elf_ma_ecog1x : Nat_big_num.num= (Nat_big_num.of_int 168) +(** Dallas Semiconductor MAXQ30 Core Micro-controllers *) +let elf_ma_maxq30 : Nat_big_num.num= (Nat_big_num.of_int 169) +(** New Japan Radio (NJR) 16-bit DSP Processor *) +let elf_ma_ximo16 : Nat_big_num.num= (Nat_big_num.of_int 170) +(** M2000 Reconfigurable RISC Microprocessor *) +let elf_ma_manik : Nat_big_num.num= (Nat_big_num.of_int 171) +(** Cray Inc. NV2 vector architecture *) +let elf_ma_craynv2 : Nat_big_num.num= (Nat_big_num.of_int 172) +(** Renesas RX family *) +let elf_ma_rx : Nat_big_num.num= (Nat_big_num.of_int 173) +(** Imagination Technologies META processor architecture *) +let elf_ma_metag : Nat_big_num.num= (Nat_big_num.of_int 174) +(** MCST Elbrus general purpose hardware architecture *) +let elf_ma_mcst_elbrus : Nat_big_num.num= (Nat_big_num.of_int 175) +(** Cyan Technology eCOG16 family *) +let elf_ma_ecog16 : Nat_big_num.num= (Nat_big_num.of_int 176) +(** National Semiconductor CompactRISC CR16 16-bit microprocessor *) +let elf_ma_cr16 : Nat_big_num.num= (Nat_big_num.of_int 177) +(** Freescale Extended Time Processing Unit *) +let elf_ma_etpu : Nat_big_num.num= (Nat_big_num.of_int 178) +(** Altium TSK3000 core *) +let elf_ma_tsk3000 : Nat_big_num.num= (Nat_big_num.of_int 131) +(** Freescale RS08 embedded processor *) +let elf_ma_rs08 : Nat_big_num.num= (Nat_big_num.of_int 132) +(** Analog Devices SHARC family of 32-bit DSP processors *) +let elf_ma_sharc : Nat_big_num.num= (Nat_big_num.of_int 133) +(** Cyan Technology eCOG2 microprocessor *) +let elf_ma_ecog2 : Nat_big_num.num= (Nat_big_num.of_int 134) +(** Sunplus S+core7 RISC processor *) +let elf_ma_ccore7 : Nat_big_num.num= (Nat_big_num.of_int 135) +(** New Japan Radio (NJR) 24-bit DSP Processor *) +let elf_ma_dsp24 : Nat_big_num.num= (Nat_big_num.of_int 136) +(** Broadcom VideoCore III processor *) +let elf_ma_videocore3 : Nat_big_num.num= (Nat_big_num.of_int 137) +(** RISC processor for Lattice FPGA architecture *) +let elf_ma_latticemico32 : Nat_big_num.num= (Nat_big_num.of_int 138) +(** Seiko Epson C17 family *) +let elf_ma_c17 : Nat_big_num.num= (Nat_big_num.of_int 139) +(** The Texas Instruments TMS320C6000 DSP family *) +let elf_ma_c6000 : Nat_big_num.num= (Nat_big_num.of_int 140) +(** The Texas Instruments TMS320C2000 DSP family *) +let elf_ma_c2000 : Nat_big_num.num= (Nat_big_num.of_int 141) +(** The Texas Instruments TMS320C55x DSP family *) +let elf_ma_c5500 : Nat_big_num.num= (Nat_big_num.of_int 142) +(** STMicroelectronics 64bit VLIW Data Signal Processor *) +let elf_ma_mmdsp_plus : Nat_big_num.num= (Nat_big_num.of_int 160) +(** LSI Logic 16-bit DSP Processor *) +let elf_ma_zsp : Nat_big_num.num= (Nat_big_num.of_int 79) +(** Donald Knuth's educational 64-bit processor *) +let elf_ma_mmix : Nat_big_num.num= (Nat_big_num.of_int 80) +(** Harvard University machine-independent object files *) +let elf_ma_huany : Nat_big_num.num= (Nat_big_num.of_int 81) +(** SiTera Prism *) +let elf_ma_prism : Nat_big_num.num= (Nat_big_num.of_int 82) +(** Atmel AVR 8-bit microcontroller *) +let elf_ma_avr : Nat_big_num.num= (Nat_big_num.of_int 83) +(** Fujitsu FR30 *) +let elf_ma_fr30 : Nat_big_num.num= (Nat_big_num.of_int 84) +(** Mitsubishi D10V *) +let elf_ma_d10v : Nat_big_num.num= (Nat_big_num.of_int 85) +(** Mitsubishi D30V *) +let elf_ma_d30v : Nat_big_num.num= (Nat_big_num.of_int 86) +(** NEC v850 *) +let elf_ma_v850 : Nat_big_num.num= (Nat_big_num.of_int 87) +(** Mitsubishi M32R *) +let elf_ma_m32r : Nat_big_num.num= (Nat_big_num.of_int 88) +(** Matsushita MN10300 *) +let elf_ma_mn10300 : Nat_big_num.num= (Nat_big_num.of_int 89) +(** Matsushita MN10200 *) +let elf_ma_mn10200 : Nat_big_num.num= (Nat_big_num.of_int 90) +(** picoJava *) +let elf_ma_pj : Nat_big_num.num= (Nat_big_num.of_int 91) +(** OpenRISC 32-bit embedded processor *) +let elf_ma_openrisc : Nat_big_num.num= (Nat_big_num.of_int 92) +(** ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5) *) +let elf_ma_arc_compact : Nat_big_num.num= (Nat_big_num.of_int 93) +(** Tensilica Xtensa Architecture *) +let elf_ma_xtensa : Nat_big_num.num= (Nat_big_num.of_int 94) +(** Alphamosaic VideoCore processor *) +let elf_ma_videocore : Nat_big_num.num= (Nat_big_num.of_int 95) +(** Thompson Multimedia General Purpose Processor *) +let elf_ma_tmm_gpp : Nat_big_num.num= (Nat_big_num.of_int 96) +(** National Semiconductor 32000 series *) +let elf_ma_ns32k : Nat_big_num.num= (Nat_big_num.of_int 97) +(** Tenor Network TPC processor *) +let elf_ma_tpc : Nat_big_num.num= (Nat_big_num.of_int 98) +(** Trebia SNP 1000 processor *) +let elf_ma_snp1k : Nat_big_num.num= (Nat_big_num.of_int 99) +(** STMicroelectronics ST200 microcontroller *) +let elf_ma_st200 : Nat_big_num.num= (Nat_big_num.of_int 100) +(** Ubicom IP2xxx microcontroller family *) +let elf_ma_ip2k : Nat_big_num.num= (Nat_big_num.of_int 101) +(** MAX Processor *) +let elf_ma_max : Nat_big_num.num= (Nat_big_num.of_int 102) +(** National Semiconductor CompactRISC microprocessor *) +let elf_ma_cr : Nat_big_num.num= (Nat_big_num.of_int 103) +(** Fujitsu F2MC16 *) +let elf_ma_f2mc16 : Nat_big_num.num= (Nat_big_num.of_int 104) +(** Texas Instruments embedded microcontroller msp430 *) +let elf_ma_msp430 : Nat_big_num.num= (Nat_big_num.of_int 105) +(** Analog Devices Blackfin (DSP) processor *) +let elf_ma_blackfin : Nat_big_num.num= (Nat_big_num.of_int 106) +(** S1C33 Family of Seiko Epson processors *) +let elf_ma_se_c33 : Nat_big_num.num= (Nat_big_num.of_int 107) +(** Sharp embedded microprocessor *) +let elf_ma_sep : Nat_big_num.num= (Nat_big_num.of_int 108) +(** Arca RISC Microprocessor *) +let elf_ma_arca : Nat_big_num.num= (Nat_big_num.of_int 109) +(** Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University *) +let elf_ma_unicore : Nat_big_num.num= (Nat_big_num.of_int 110) +(** eXcess: 16/32/64-bit configurable embedded CPU *) +let elf_ma_excess : Nat_big_num.num= (Nat_big_num.of_int 111) +(** Icera Semiconductor Inc. Deep Execution Processor *) +let elf_ma_dxp : Nat_big_num.num= (Nat_big_num.of_int 112) +(** Altera Nios II soft-core processor *) +let elf_ma_altera_nios2 : Nat_big_num.num= (Nat_big_num.of_int 113) +(** National Semiconductor CompactRISC CRX microprocessor *) +let elf_ma_crx : Nat_big_num.num= (Nat_big_num.of_int 114) +(** Motorola XGATE embedded processor *) +let elf_ma_xgate : Nat_big_num.num= (Nat_big_num.of_int 115) +(** Infineon C16x/XC16x processor *) +let elf_ma_c166 : Nat_big_num.num= (Nat_big_num.of_int 116) +(** Renesas M16C series microprocessors *) +let elf_ma_m16c : Nat_big_num.num= (Nat_big_num.of_int 117) +(** Microchip Technology dsPIC30F Digital Signal Controller *) +let elf_ma_dspic30f : Nat_big_num.num= (Nat_big_num.of_int 118) +(** Freescale Communication Engine RISC core *) +let elf_ma_ce : Nat_big_num.num= (Nat_big_num.of_int 119) +(** Renesas M32C series microprocessors *) +let elf_ma_m32c : Nat_big_num.num= (Nat_big_num.of_int 120) +(** No machine *) +let elf_ma_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** AT&T WE 32100 *) +let elf_ma_m32 : Nat_big_num.num= (Nat_big_num.of_int 1) +(** SPARC *) +let elf_ma_sparc : Nat_big_num.num= (Nat_big_num.of_int 2) +(** Intel 80386 *) +let elf_ma_386 : Nat_big_num.num= (Nat_big_num.of_int 3) +(** Motorola 68000 *) +let elf_ma_68k : Nat_big_num.num= (Nat_big_num.of_int 4) +(** Motorola 88000 *) +let elf_ma_88k : Nat_big_num.num= (Nat_big_num.of_int 5) +(** Intel 80860 *) +let elf_ma_860 : Nat_big_num.num= (Nat_big_num.of_int 7) +(** MIPS I Architecture *) +let elf_ma_mips : Nat_big_num.num= (Nat_big_num.of_int 8) +(** IBM System/370 Processor *) +let elf_ma_s370 : Nat_big_num.num= (Nat_big_num.of_int 9) +(** MIPS RS3000 Little-endian *) +let elf_ma_mips_rs3_le : Nat_big_num.num= (Nat_big_num.of_int 10) +(** Hewlett-Packard PA-RISC *) +let elf_ma_parisc : Nat_big_num.num= (Nat_big_num.of_int 15) +(** Fujitsu VPP500 *) +let elf_ma_vpp500 : Nat_big_num.num= (Nat_big_num.of_int 17) +(** Enhanced instruction set SPARC *) +let elf_ma_sparc32plus : Nat_big_num.num= (Nat_big_num.of_int 18) +(** Intel 80960 *) +let elf_ma_960 : Nat_big_num.num= (Nat_big_num.of_int 19) +(** PowerPC *) +let elf_ma_ppc : Nat_big_num.num= (Nat_big_num.of_int 20) +(** 64-bit PowerPC *) +let elf_ma_ppc64 : Nat_big_num.num= (Nat_big_num.of_int 21) +(** IBM System/390 Processor *) +let elf_ma_s390 : Nat_big_num.num= (Nat_big_num.of_int 22) +(** IBM SPU/SPC *) +let elf_ma_spu : Nat_big_num.num= (Nat_big_num.of_int 23) +(** NEC V800 *) +let elf_ma_v800 : Nat_big_num.num= (Nat_big_num.of_int 36) +(** Fujitsu FR20 *) +let elf_ma_fr20 : Nat_big_num.num= (Nat_big_num.of_int 37) +(** TRW RH-32 *) +let elf_ma_rh32 : Nat_big_num.num= (Nat_big_num.of_int 38) +(** Motorola RCE *) +let elf_ma_rce : Nat_big_num.num= (Nat_big_num.of_int 39) +(** ARM 32-bit architecture (AARCH32) *) +let elf_ma_arm : Nat_big_num.num= (Nat_big_num.of_int 40) +(** Digital Alpha *) +let elf_ma_alpha : Nat_big_num.num= (Nat_big_num.of_int 41) +(** Hitachi SH *) +let elf_ma_sh : Nat_big_num.num= (Nat_big_num.of_int 42) +(** SPARC Version 9 *) +let elf_ma_sparcv9 : Nat_big_num.num= (Nat_big_num.of_int 43) +(** Siemens TriCore embedded processor *) +let elf_ma_tricore : Nat_big_num.num= (Nat_big_num.of_int 44) +(** Argonaut RISC Core, Argonaut Technologies Inc. *) +let elf_ma_arc : Nat_big_num.num= (Nat_big_num.of_int 45) +(** Hitachi H8/300 *) +let elf_ma_h8_300 : Nat_big_num.num= (Nat_big_num.of_int 46) +(** Hitachi H8/300H *) +let elf_ma_h8_300h : Nat_big_num.num= (Nat_big_num.of_int 47) +(** Hitachi H8S *) +let elf_ma_h8s : Nat_big_num.num= (Nat_big_num.of_int 48) +(** Hitachi H8/500 *) +let elf_ma_h8_500 : Nat_big_num.num= (Nat_big_num.of_int 49) +(** Intel IA-64 processor architecture *) +let elf_ma_ia_64 : Nat_big_num.num= (Nat_big_num.of_int 50) +(** Stanford MIPS-X *) +let elf_ma_mips_x : Nat_big_num.num= (Nat_big_num.of_int 51) +(** Motorola ColdFire *) +let elf_ma_coldfire : Nat_big_num.num= (Nat_big_num.of_int 52) +(** Motorola M68HC12 *) +let elf_ma_68hc12 : Nat_big_num.num= (Nat_big_num.of_int 53) +(** Fujitsu MMA Multimedia Accelerator *) +let elf_ma_mma : Nat_big_num.num= (Nat_big_num.of_int 54) +(** Siemens PCP *) +let elf_ma_pcp : Nat_big_num.num= (Nat_big_num.of_int 55) +(** Sony nCPU embedded RISC processor *) +let elf_ma_ncpu : Nat_big_num.num= (Nat_big_num.of_int 56) +(** Denso NDR1 microprocessor *) +let elf_ma_ndr1 : Nat_big_num.num= (Nat_big_num.of_int 57) +(** Motorola Star*Core processor *) +let elf_ma_starcore : Nat_big_num.num= (Nat_big_num.of_int 58) +(** Toyota ME16 processor *) +let elf_ma_me16 : Nat_big_num.num= (Nat_big_num.of_int 59) +(** STMicroelectronics ST100 processor *) +let elf_ma_st100 : Nat_big_num.num= (Nat_big_num.of_int 60) +(** Advanced Logic Corp. TinyJ embedded processor family *) +let elf_ma_tinyj : Nat_big_num.num= (Nat_big_num.of_int 61) +(** AMD x86-64 architecture *) +let elf_ma_x86_64 : Nat_big_num.num= (Nat_big_num.of_int 62) +(** Sony DSP Processor *) +let elf_ma_pdsp : Nat_big_num.num= (Nat_big_num.of_int 63) +(** Digital Equipment Corp. PDP-10 *) +let elf_ma_pdp10 : Nat_big_num.num= (Nat_big_num.of_int 64) +(** Digital Equipment Corp. PDP-11 *) +let elf_ma_pdp11 : Nat_big_num.num= (Nat_big_num.of_int 65) +(** Siemens FX66 microcontroller *) +let elf_ma_fx66 : Nat_big_num.num= (Nat_big_num.of_int 66) +(** STMicroelectronics ST9+ 8/16 bit microcontroller *) +let elf_ma_st9plus : Nat_big_num.num= (Nat_big_num.of_int 67) +(** STMicroelectronics ST7 8-bit microcontroller *) +let elf_ma_st7 : Nat_big_num.num= (Nat_big_num.of_int 68) +(** Motorola MC68HC16 Microcontroller *) +let elf_ma_68hc16 : Nat_big_num.num= (Nat_big_num.of_int 69) +(** Motorola MC68HC11 Microcontroller *) +let elf_ma_68hc11 : Nat_big_num.num= (Nat_big_num.of_int 70) +(** Motorola MC68HC08 Microcontroller *) +let elf_ma_68hc08 : Nat_big_num.num= (Nat_big_num.of_int 71) +(** Motorola MC68HC05 Microcontroller *) +let elf_ma_68hc05 : Nat_big_num.num= (Nat_big_num.of_int 72) +(** Silicon Graphics SVx *) +let elf_ma_svx : Nat_big_num.num= (Nat_big_num.of_int 73) +(** STMicroelectronics ST19 8-bit microcontroller *) +let elf_ma_st19 : Nat_big_num.num= (Nat_big_num.of_int 74) +(** Digital VAX *) +let elf_ma_vax : Nat_big_num.num= (Nat_big_num.of_int 75) +(** Axis Communications 32-bit embedded processor *) +let elf_ma_cris : Nat_big_num.num= (Nat_big_num.of_int 76) +(** Infineon Technologies 32-bit embedded processor *) +let elf_ma_javelin : Nat_big_num.num= (Nat_big_num.of_int 77) +(** Element 14 64-bit DSP Processor *) +let elf_ma_firepath : Nat_big_num.num= (Nat_big_num.of_int 78) +(** Reserved by Intel *) +let elf_ma_intel209 : Nat_big_num.num= (Nat_big_num.of_int 209) +(** Reserved by Intel *) +let elf_ma_intel208 : Nat_big_num.num= (Nat_big_num.of_int 208) +(** Reserved by Intel *) +let elf_ma_intel207 : Nat_big_num.num= (Nat_big_num.of_int 207) +(** Reserved by Intel *) +let elf_ma_intel206 : Nat_big_num.num= (Nat_big_num.of_int 206) +(** Reserved by Intel *) +let elf_ma_intel205 : Nat_big_num.num= (Nat_big_num.of_int 205) +(** Reserved by Intel *) +let elf_ma_intel182 : Nat_big_num.num= (Nat_big_num.of_int 182) +(** Reserved by ARM *) +let elf_ma_arm184 : Nat_big_num.num= (Nat_big_num.of_int 184) +(** Reserved for future use *) +let elf_ma_reserved6 : Nat_big_num.num= (Nat_big_num.of_int 6) +(** Reserved for future use *) +let elf_ma_reserved11 : Nat_big_num.num= (Nat_big_num.of_int 11) +(** Reserved for future use *) +let elf_ma_reserved12 : Nat_big_num.num= (Nat_big_num.of_int 12) +(** Reserved for future use *) +let elf_ma_reserved13 : Nat_big_num.num= (Nat_big_num.of_int 13) +(** Reserved for future use *) +let elf_ma_reserved14 : Nat_big_num.num= (Nat_big_num.of_int 14) +(** Reserved for future use *) +let elf_ma_reserved16 : Nat_big_num.num= (Nat_big_num.of_int 16) +(** Reserved for future use *) +let elf_ma_reserved24 : Nat_big_num.num= (Nat_big_num.of_int 24) +(** Reserved for future use *) +let elf_ma_reserved25 : Nat_big_num.num= (Nat_big_num.of_int 25) +(** Reserved for future use *) +let elf_ma_reserved26 : Nat_big_num.num= (Nat_big_num.of_int 26) +(** Reserved for future use *) +let elf_ma_reserved27 : Nat_big_num.num= (Nat_big_num.of_int 27) +(** Reserved for future use *) +let elf_ma_reserved28 : Nat_big_num.num= (Nat_big_num.of_int 28) +(** Reserved for future use *) +let elf_ma_reserved29 : Nat_big_num.num= (Nat_big_num.of_int 29) +(** Reserved for future use *) +let elf_ma_reserved30 : Nat_big_num.num= (Nat_big_num.of_int 30) +(** Reserved for future use *) +let elf_ma_reserved31 : Nat_big_num.num= (Nat_big_num.of_int 31) +(** Reserved for future use *) +let elf_ma_reserved32 : Nat_big_num.num= (Nat_big_num.of_int 32) +(** Reserved for future use *) +let elf_ma_reserved33 : Nat_big_num.num= (Nat_big_num.of_int 33) +(** Reserved for future use *) +let elf_ma_reserved34 : Nat_big_num.num= (Nat_big_num.of_int 34) +(** Reserved for future use *) +let elf_ma_reserved35 : Nat_big_num.num= (Nat_big_num.of_int 35) +(** Reserved for future use *) +let elf_ma_reserved121 : Nat_big_num.num= (Nat_big_num.of_int 121) +(** Reserved for future use *) +let elf_ma_reserved122 : Nat_big_num.num= (Nat_big_num.of_int 122) +(** Reserved for future use *) +let elf_ma_reserved123 : Nat_big_num.num= (Nat_big_num.of_int 123) +(** Reserved for future use *) +let elf_ma_reserved124 : Nat_big_num.num= (Nat_big_num.of_int 124) +(** Reserved for future use *) +let elf_ma_reserved125 : Nat_big_num.num= (Nat_big_num.of_int 125) +(** Reserved for future use *) +let elf_ma_reserved126 : Nat_big_num.num= (Nat_big_num.of_int 126) +(** Reserved for future use *) +let elf_ma_reserved127 : Nat_big_num.num= (Nat_big_num.of_int 127) +(** Reserved for future use *) +let elf_ma_reserved128 : Nat_big_num.num= (Nat_big_num.of_int 128) +(** Reserved for future use *) +let elf_ma_reserved129 : Nat_big_num.num= (Nat_big_num.of_int 129) +(** Reserved for future use *) +let elf_ma_reserved130 : Nat_big_num.num= (Nat_big_num.of_int 130) +(** Reserved for future use *) +let elf_ma_reserved143 : Nat_big_num.num= (Nat_big_num.of_int 143) +(** Reserved for future use *) +let elf_ma_reserved144 : Nat_big_num.num= (Nat_big_num.of_int 144) +(** Reserved for future use *) +let elf_ma_reserved145 : Nat_big_num.num= (Nat_big_num.of_int 145) +(** Reserved for future use *) +let elf_ma_reserved146 : Nat_big_num.num= (Nat_big_num.of_int 146) +(** Reserved for future use *) +let elf_ma_reserved147 : Nat_big_num.num= (Nat_big_num.of_int 147) +(** Reserved for future use *) +let elf_ma_reserved148 : Nat_big_num.num= (Nat_big_num.of_int 148) +(** Reserved for future use *) +let elf_ma_reserved149 : Nat_big_num.num= (Nat_big_num.of_int 149) +(** Reserved for future use *) +let elf_ma_reserved150 : Nat_big_num.num= (Nat_big_num.of_int 150) +(** Reserved for future use *) +let elf_ma_reserved151 : Nat_big_num.num= (Nat_big_num.of_int 151) +(** Reserved for future use *) +let elf_ma_reserved152 : Nat_big_num.num= (Nat_big_num.of_int 152) +(** Reserved for future use *) +let elf_ma_reserved153 : Nat_big_num.num= (Nat_big_num.of_int 153) +(** Reserved for future use *) +let elf_ma_reserved154 : Nat_big_num.num= (Nat_big_num.of_int 154) +(** Reserved for future use *) +let elf_ma_reserved155 : Nat_big_num.num= (Nat_big_num.of_int 155) +(** Reserved for future use *) +let elf_ma_reserved156 : Nat_big_num.num= (Nat_big_num.of_int 156) +(** Reserved for future use *) +let elf_ma_reserved157 : Nat_big_num.num= (Nat_big_num.of_int 157) +(** Reserved for future use *) +let elf_ma_reserved158 : Nat_big_num.num= (Nat_big_num.of_int 158) +(** Reserved for future use *) +let elf_ma_reserved159 : Nat_big_num.num= (Nat_big_num.of_int 159) + +(** [string_of_elf_machine_architecture m] produces a string representation of + * the numeric encoding [m] of the ELF machine architecture. + * TODO: finish this . + *) +(*val string_of_elf_machine_architecture : natural -> string*) +let string_of_elf_machine_architecture m:string= + (if Nat_big_num.equal m elf_ma_386 then + "Intel 80386" + else if Nat_big_num.equal m elf_ma_ppc then + "PowerPC" + else if Nat_big_num.equal m elf_ma_ppc64 then + "PowerPC64" + else if Nat_big_num.equal m elf_ma_arm then + "AArch" + else if Nat_big_num.equal m elf_ma_x86_64 then + "Advanced Micro Devices X86-64" + else if Nat_big_num.equal m elf_ma_aarch64 then + "AArch64" + else + "Other architecture") + +(** ELF version numbers. Denotes the ELF version number of an ELF file. Current is + * defined to have a value of 1 with the present specification. Extensions + * may create versions of ELF with higher version numbers. + *) + +(** Invalid version *) +let elf_ev_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** Current version *) +let elf_ev_current : Nat_big_num.num= (Nat_big_num.of_int 1) + +(** [string_of_elf_version_number m] produces a string representation of the + * numeric encoding [m] of the ELF version number. + *) +(*val string_of_elf_version_number : natural -> string*) +let string_of_elf_version_number m:string= + (if Nat_big_num.equal m elf_ev_none then + "Invalid ELF version" + else if Nat_big_num.equal m elf_ev_current then + "1 (current)" + else + "Extended ELF version") + +(** Check that an extended version number is correct (i.e. greater than 1). *) +let is_valid_extended_version_number (n : Nat_big_num.num):bool= (Nat_big_num.greater n(Nat_big_num.of_int 1)) + +(** Identification indices. The initial bytes of an ELF header (and an object + * file) correspond to the e_ident member. + *) + +(** File identification *) +let elf_ii_mag0 : Nat_big_num.num= (Nat_big_num.of_int 0) +(** File identification *) +let elf_ii_mag1 : Nat_big_num.num= (Nat_big_num.of_int 1) +(** File identification *) +let elf_ii_mag2 : Nat_big_num.num= (Nat_big_num.of_int 2) +(** File identification *) +let elf_ii_mag3 : Nat_big_num.num= (Nat_big_num.of_int 3) +(** File class *) +let elf_ii_class : Nat_big_num.num= (Nat_big_num.of_int 4) +(** Data encoding *) +let elf_ii_data : Nat_big_num.num= (Nat_big_num.of_int 5) +(** File version *) +let elf_ii_version : Nat_big_num.num= (Nat_big_num.of_int 6) +(** Operating system/ABI identification *) +let elf_ii_osabi : Nat_big_num.num= (Nat_big_num.of_int 7) +(** ABI version *) +let elf_ii_abiversion : Nat_big_num.num= (Nat_big_num.of_int 8) +(** Start of padding bytes *) +let elf_ii_pad : Nat_big_num.num= (Nat_big_num.of_int 9) +(** Size of e*_ident[] *) +let elf_ii_nident : Nat_big_num.num= (Nat_big_num.of_int 16) + +(** Magic number indices. A file's first 4 bytes hold a ``magic number,'' + * identifying the file as an ELF object file. + *) + +(** Position: e*_ident[elf_ii_mag0], 0x7f magic number *) +let elf_mn_mag0 : Uint32.uint32= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 127))) +(** Position: e*_ident[elf_ii_mag1], 'E' format identifier *) +let elf_mn_mag1 : Uint32.uint32= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 69))) +(** Position: e*_ident[elf_ii_mag2], 'L' format identifier *) +let elf_mn_mag2 : Uint32.uint32= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 76))) +(** Position: e*_ident[elf_ii_mag3], 'F' format identifier *) +let elf_mn_mag3 : Uint32.uint32= (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 70))) + +(** ELf file classes. The file format is designed to be portable among machines + * of various sizes, without imposing the sizes of the largest machine on the + * smallest. The class of the file defines the basic types used by the data + * structures of the object file container itself. + *) + +(** Invalid class *) +let elf_class_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** 32 bit objects *) +let elf_class_32 : Nat_big_num.num= (Nat_big_num.of_int 1) +(** 64 bit objects *) +let elf_class_64 : Nat_big_num.num= (Nat_big_num.of_int 2) + +(** [string_of_elf_file_class m] produces a string representation of the numeric + * encoding [m] of the ELF file class. + *) +(*val string_of_elf_file_class : natural -> string*) +let string_of_elf_file_class m:string= + (if Nat_big_num.equal m elf_class_none then + "Invalid ELF file class" + else if Nat_big_num.equal m elf_class_32 then + "ELF32" + else if Nat_big_num.equal m elf_class_64 then + "ELF64" + else + "Invalid ELF file class") + +(** ELF data encodings. Byte e_ident[elf_ei_data] specifies the encoding of both the + * data structures used by object file container and data contained in object + * file sections. + *) + +(** Invalid data encoding *) +let elf_data_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** Two's complement values, least significant byte occupying lowest address *) +let elf_data_2lsb : Nat_big_num.num= (Nat_big_num.of_int 1) +(** Two's complement values, most significant byte occupying lowest address *) +let elf_data_2msb : Nat_big_num.num= (Nat_big_num.of_int 2) + +(** [string_of_elf_data_encoding m] produces a string representation of the + * numeric encoding [m] of the ELF data encoding. + *) +(*val string_of_elf_data_encoding : natural -> string*) +let string_of_elf_data_encoding m:string= + (if Nat_big_num.equal m elf_data_none then + "Invalid data encoding" + else if Nat_big_num.equal m elf_data_2lsb then + "2's complement, little endian" + else if Nat_big_num.equal m elf_data_2msb then + "2's complement, big endian" + else + "Invalid data encoding") + +(** OS and ABI versions. Byte e_ident[elf_ei_osabi] identifies the OS- or + * ABI-specific ELF extensions used by this file. Some fields in other ELF + * structures have flags and values that have operating system and/or ABI + * specific meanings; the interpretation of those fields is determined by the + * value of this byte. + *) + +(** No extensions or unspecified *) +let elf_osabi_none : Nat_big_num.num= (Nat_big_num.of_int 0) +(** Hewlett-Packard HP-UX *) +let elf_osabi_hpux : Nat_big_num.num= (Nat_big_num.of_int 1) +(** NetBSD *) +let elf_osabi_netbsd : Nat_big_num.num= (Nat_big_num.of_int 2) +(** GNU *) +let elf_osabi_gnu : Nat_big_num.num= (Nat_big_num.of_int 3) +(** Linux, historical alias for GNU *) +let elf_osabi_linux : Nat_big_num.num= (Nat_big_num.of_int 3) +(** Sun Solaris *) +let elf_osabi_solaris : Nat_big_num.num= (Nat_big_num.of_int 6) +(** AIX *) +let elf_osabi_aix : Nat_big_num.num= (Nat_big_num.of_int 7) +(** IRIX *) +let elf_osabi_irix : Nat_big_num.num= (Nat_big_num.of_int 8) +(** FreeBSD *) +let elf_osabi_freebsd : Nat_big_num.num= (Nat_big_num.of_int 9) +(** Compaq Tru64 Unix *) +let elf_osabi_tru64 : Nat_big_num.num= (Nat_big_num.of_int 10) +(** Novell Modesto *) +let elf_osabi_modesto : Nat_big_num.num= (Nat_big_num.of_int 11) +(** OpenBSD *) +let elf_osabi_openbsd : Nat_big_num.num= (Nat_big_num.of_int 12) +(** OpenVMS *) +let elf_osabi_openvms : Nat_big_num.num= (Nat_big_num.of_int 13) +(** Hewlett-Packard Non-stop Kernel *) +let elf_osabi_nsk : Nat_big_num.num= (Nat_big_num.of_int 14) +(** Amiga Research OS *) +let elf_osabi_aros : Nat_big_num.num= (Nat_big_num.of_int 15) +(** FenixOS highly-scalable multi-core OS *) +let elf_osabi_fenixos : Nat_big_num.num= (Nat_big_num.of_int 16) +(** Nuxi CloudABI *) +let elf_osabi_cloudabi : Nat_big_num.num= (Nat_big_num.of_int 17) +(** Stratus technologies OpenVOS *) +let elf_osabi_openvos : Nat_big_num.num= (Nat_big_num.of_int 18) + +(** Checks an architecture defined OSABI version is correct, i.e. in the range + * 64 to 255 inclusive. + *) +let is_valid_architecture_defined_osabi_version (n : Nat_big_num.num):bool= (Nat_big_num.greater_equal + n(Nat_big_num.of_int 64) && Nat_big_num.less_equal n(Nat_big_num.of_int 255)) + +(** [string_of_elf_osabi_version m] produces a string representation of the + * numeric encoding [m] of the ELF OSABI version. + *) +(*val string_of_elf_osabi_version : (natural -> string) -> natural -> string*) +let string_of_elf_osabi_version arch m:string= + (if Nat_big_num.equal m elf_osabi_none then + "UNIX - System V" + else if Nat_big_num.equal m elf_osabi_netbsd then + "Hewlett-Packard HP-UX" + else if Nat_big_num.equal m elf_osabi_netbsd then + "NetBSD" + else if Nat_big_num.equal m elf_osabi_gnu then + "UNIX - GNU" + else if Nat_big_num.equal m elf_osabi_linux then + "Linux" + else if Nat_big_num.equal m elf_osabi_solaris then + "Sun Solaris" + else if Nat_big_num.equal m elf_osabi_aix then + "AIX" + else if Nat_big_num.equal m elf_osabi_irix then + "IRIX" + else if Nat_big_num.equal m elf_osabi_freebsd then + "FreeBSD" + else if Nat_big_num.equal m elf_osabi_tru64 then + "Compaq Tru64 Unix" + else if Nat_big_num.equal m elf_osabi_modesto then + "Novell Modesto" + else if Nat_big_num.equal m elf_osabi_openbsd then + "OpenBSD" + else if Nat_big_num.equal m elf_osabi_openvms then + "OpenVMS" + else if Nat_big_num.equal m elf_osabi_nsk then + "Hewlett-Packard Non-stop Kernel" + else if Nat_big_num.equal m elf_osabi_aros then + "Amiga Research OS" + else if Nat_big_num.equal m elf_osabi_fenixos then + "FenixOS highly-scalable multi-core OS" + else if Nat_big_num.equal m elf_osabi_cloudabi then + "Nuxi CloudABI" + else if Nat_big_num.equal m elf_osabi_openvos then + "Stratus technologies OpenVOS" + else if is_valid_architecture_defined_osabi_version m then + arch m + else + "Invalid OSABI version") + +(** ELF Header type *) + +(** [ei_nident] is the fixed length of the identification field in the + * [elf32_ehdr] type. + *) +(*val ei_nident : natural*) +let ei_nident:Nat_big_num.num= (Nat_big_num.of_int 16) + +(** [elf32_header] is the type of headers for 32-bit ELF files. + *) +type elf32_header = + { elf32_ident : Uint32.uint32 list (** Identification field *) + ; elf32_type : Uint32.uint32 (** The object file type *) + ; elf32_machine : Uint32.uint32 (** Required machine architecture *) + ; elf32_version : Uint32.uint32 (** Object file version *) + ; elf32_entry : Uint32.uint32 (** Virtual address for transfer of control *) + ; elf32_phoff : Uint32.uint32 (** Program header table offset in bytes *) + ; elf32_shoff : Uint32.uint32 (** Section header table offset in bytes *) + ; elf32_flags : Uint32.uint32 (** Processor-specific flags *) + ; elf32_ehsize : Uint32.uint32 (** ELF header size in bytes *) + ; elf32_phentsize: Uint32.uint32 (** Program header table entry size in bytes *) + ; elf32_phnum : Uint32.uint32 (** Number of entries in program header table *) + ; elf32_shentsize: Uint32.uint32 (** Section header table entry size in bytes *) + ; elf32_shnum : Uint32.uint32 (** Number of entries in section header table *) + ; elf32_shstrndx : Uint32.uint32 (** Section header table entry for section name string table *) + } + +(** [elf64_header] is the type of headers for 64-bit ELF files. + *) +type elf64_header = + { elf64_ident : Uint32.uint32 list (** Identification field *) + ; elf64_type : Uint32.uint32 (** The object file type *) + ; elf64_machine : Uint32.uint32 (** Required machine architecture *) + ; elf64_version : Uint32.uint32 (** Object file version *) + ; elf64_entry : Uint64.uint64 (** Virtual address for transfer of control *) + ; elf64_phoff : Uint64.uint64 (** Program header table offset in bytes *) + ; elf64_shoff : Uint64.uint64 (** Section header table offset in bytes *) + ; elf64_flags : Uint32.uint32 (** Processor-specific flags *) + ; elf64_ehsize : Uint32.uint32 (** ELF header size in bytes *) + ; elf64_phentsize: Uint32.uint32 (** Program header table entry size in bytes *) + ; elf64_phnum : Uint32.uint32 (** Number of entries in program header table *) + ; elf64_shentsize: Uint32.uint32 (** Section header table entry size in bytes *) + ; elf64_shnum : Uint32.uint32 (** Number of entries in section header table *) + ; elf64_shstrndx : Uint32.uint32 (** Section header table entry for section name string table *) + } + +(** [is_valid_elf32_header hdr] checks whether header [hdr] is valid, i.e. has + * the correct magic numbers. + * TODO: this should be expanded, presumably, or merged with some of the other + * checks. + *) +(*val is_valid_elf32_header : elf32_header -> bool*) +let is_valid_elf32_header hdr:bool= (listEqualBy (=) +(Lem_list.take( 4) hdr.elf32_ident) [elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3]) + +(** [is_valid_elf64_header hdr] checks whether header [hdr] is valid, i.e. has + * the correct magic numbers. + * TODO: this should be expanded, presumably, or merged with some of the other + * checks. + *) +(*val is_valid_elf64_header : elf64_header -> bool*) +let is_valid_elf64_header hdr:bool= (listEqualBy (=) +(Lem_list.take( 4) hdr.elf64_ident) [elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3]) + +(** [elf32_header_compare hdr1 hdr2] is an ordering comparison function for + * ELF headers suitable for use in sets, finite maps and other ordered + * data types. + *) +(*val elf32_header_compare : elf32_header -> elf32_header -> Basic_classes.ordering*) +let elf32_header_compare h1 h2:int= + (pairCompare (lexicographic_compare Nat_big_num.compare) (lexicographic_compare Nat_big_num.compare) (Lem_list.map (fun u->Nat_big_num.of_string (Uint32.to_string u)) h1.elf32_ident, [Nat_big_num.of_string (Uint32.to_string h1.elf32_type); + Nat_big_num.of_string (Uint32.to_string h1.elf32_machine) ; Nat_big_num.of_string (Uint32.to_string h1.elf32_version) ; + Nat_big_num.of_string (Uint32.to_string h1.elf32_entry) ; Nat_big_num.of_string (Uint32.to_string h1.elf32_phoff) ; Nat_big_num.of_string (Uint32.to_string h1.elf32_shoff) ; + Nat_big_num.of_string (Uint32.to_string h1.elf32_flags) ; Nat_big_num.of_string (Uint32.to_string h1.elf32_ehsize) ; + Nat_big_num.of_string (Uint32.to_string h1.elf32_phentsize); Nat_big_num.of_string (Uint32.to_string h1.elf32_phnum) ; + Nat_big_num.of_string (Uint32.to_string h1.elf32_shentsize); Nat_big_num.of_string (Uint32.to_string h1.elf32_shnum) ; + Nat_big_num.of_string (Uint32.to_string h1.elf32_shstrndx)]) + (Lem_list.map (fun u->Nat_big_num.of_string (Uint32.to_string u)) h2.elf32_ident, [Nat_big_num.of_string (Uint32.to_string h2.elf32_type); + Nat_big_num.of_string (Uint32.to_string h2.elf32_machine) ; Nat_big_num.of_string (Uint32.to_string h2.elf32_version) ; + Nat_big_num.of_string (Uint32.to_string h2.elf32_entry) ; Nat_big_num.of_string (Uint32.to_string h2.elf32_phoff) ; Nat_big_num.of_string (Uint32.to_string h2.elf32_shoff) ; + Nat_big_num.of_string (Uint32.to_string h2.elf32_flags) ; Nat_big_num.of_string (Uint32.to_string h2.elf32_ehsize) ; + Nat_big_num.of_string (Uint32.to_string h2.elf32_phentsize); Nat_big_num.of_string (Uint32.to_string h2.elf32_phnum) ; + Nat_big_num.of_string (Uint32.to_string h2.elf32_shentsize); Nat_big_num.of_string (Uint32.to_string h2.elf32_shnum) ; + Nat_big_num.of_string (Uint32.to_string h2.elf32_shstrndx)])) + +let instance_Basic_classes_Ord_Elf_header_elf32_header_dict:(elf32_header)ord_class= ({ + + compare_method = elf32_header_compare; + + isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_header_compare f1 f2) (-1)))); + + isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_header_compare f1 f2)(Pset.from_list compare [(-1); 0]))); + + isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_header_compare f1 f2) 1))); + + isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_header_compare f1 f2)(Pset.from_list compare [1; 0])))}) + +(** [elf64_header_compare hdr1 hdr2] is an ordering comparison function for + * ELF headers suitable for use in sets, finite maps and other ordered + * data types. + *) +(*val elf64_header_compare : elf64_header -> elf64_header -> Basic_classes.ordering*) +let elf64_header_compare h1 h2:int= + (pairCompare (lexicographic_compare Nat_big_num.compare) (lexicographic_compare Nat_big_num.compare) (Lem_list.map (fun u->Nat_big_num.of_string (Uint32.to_string u)) h1.elf64_ident, [Nat_big_num.of_string (Uint32.to_string h1.elf64_type); + Nat_big_num.of_string (Uint32.to_string h1.elf64_machine) ; Nat_big_num.of_string (Uint32.to_string h1.elf64_version) ; + Ml_bindings.nat_big_num_of_uint64 h1.elf64_entry ; Nat_big_num.of_string (Uint64.to_string h1.elf64_phoff) ; Nat_big_num.of_string (Uint64.to_string h1.elf64_shoff) ; + Nat_big_num.of_string (Uint32.to_string h1.elf64_flags) ; Nat_big_num.of_string (Uint32.to_string h1.elf64_ehsize) ; + Nat_big_num.of_string (Uint32.to_string h1.elf64_phentsize); Nat_big_num.of_string (Uint32.to_string h1.elf64_phnum) ; + Nat_big_num.of_string (Uint32.to_string h1.elf64_shentsize); Nat_big_num.of_string (Uint32.to_string h1.elf64_shnum) ; + Nat_big_num.of_string (Uint32.to_string h1.elf64_shstrndx)]) + (Lem_list.map (fun u->Nat_big_num.of_string (Uint32.to_string u)) h2.elf64_ident, [Nat_big_num.of_string (Uint32.to_string h2.elf64_type); + Nat_big_num.of_string (Uint32.to_string h2.elf64_machine) ; Nat_big_num.of_string (Uint32.to_string h2.elf64_version) ; + Ml_bindings.nat_big_num_of_uint64 h2.elf64_entry ; Nat_big_num.of_string (Uint64.to_string h2.elf64_phoff) ; Nat_big_num.of_string (Uint64.to_string h2.elf64_shoff) ; + Nat_big_num.of_string (Uint32.to_string h2.elf64_flags) ; Nat_big_num.of_string (Uint32.to_string h2.elf64_ehsize) ; + Nat_big_num.of_string (Uint32.to_string h2.elf64_phentsize); Nat_big_num.of_string (Uint32.to_string h2.elf64_phnum) ; + Nat_big_num.of_string (Uint32.to_string h2.elf64_shentsize); Nat_big_num.of_string (Uint32.to_string h2.elf64_shnum) ; + Nat_big_num.of_string (Uint32.to_string h2.elf64_shstrndx)])) + +let instance_Basic_classes_Ord_Elf_header_elf64_header_dict:(elf64_header)ord_class= ({ + + compare_method = elf64_header_compare; + + isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_header_compare f1 f2) (-1)))); + + isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_header_compare f1 f2)(Pset.from_list compare [(-1); 0]))); + + isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_header_compare f1 f2) 1))); + + isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_header_compare f1 f2)(Pset.from_list compare [1; 0])))}) + +(** [is_elf32_executable_file hdr] checks whether the header [hdr] states if the + * ELF file is of executable type. + *) +(*val is_elf32_executable_file : elf32_header -> bool*) +let is_elf32_executable_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf32_type)) elf_ft_exec) + +(** [is_elf64_executable_file hdr] checks whether the header [hdr] states if the + * ELF file is of executable type. + *) +(*val is_elf64_executable_file : elf64_header -> bool*) +let is_elf64_executable_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf64_type)) elf_ft_exec) + +(** [is_elf32_shared_object_file hdr] checks whether the header [hdr] states if the + * ELF file is of shared object type. + *) +(*val is_elf32_shared_object_file : elf32_header -> bool*) +let is_elf32_shared_object_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf32_type)) elf_ft_dyn) + +(** [is_elf64_shared_object_file hdr] checks whether the header [hdr] states if the + * ELF file is of shared object type. + *) +(*val is_elf64_shared_object_file : elf64_header -> bool*) +let is_elf64_shared_object_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf64_type)) elf_ft_dyn) + +(** [is_elf32_relocatable_file hdr] checks whether the header [hdr] states if the + * ELF file is of relocatable type. + *) +(*val is_elf32_relocatable_file : elf32_header -> bool*) +let is_elf32_relocatable_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf32_type)) elf_ft_rel) + +(** [is_elf64_relocatable_file hdr] checks whether the header [hdr] states if the + * ELF file is of relocatable type. + *) +(*val is_elf64_relocatable_file : elf64_header -> bool*) +let is_elf64_relocatable_file hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf64_type)) elf_ft_rel) + +(** [is_elf32_linkable_file hdr] checks whether the header [hdr] states if the + * ELF file is of linkable (shared object or relocatable) type. + *) +(*val is_elf32_linkable_file : elf32_header -> bool*) +let is_elf32_linkable_file hdr:bool= + (is_elf32_shared_object_file hdr || is_elf32_relocatable_file hdr) + +(** [is_elf64_linkable_file hdr] checks whether the header [hdr] states if the + * ELF file is of linkable (shared object or relocatable) type. + *) +(*val is_elf64_linkable_file : elf64_header -> bool*) +let is_elf64_linkable_file hdr:bool= + (is_elf64_shared_object_file hdr || is_elf64_relocatable_file hdr) + +(** [get_elf32_machine_architecture hdr] returns the ELF file's declared machine + * architecture, extracting the information from header [hdr]. + *) +(*val get_elf32_machine_architecture : elf32_header -> natural*) +let get_elf32_machine_architecture hdr:Nat_big_num.num= + (Nat_big_num.of_string (Uint32.to_string hdr.elf32_machine)) + +(** [get_elf64_machine_architecture hdr] returns the ELF file's declared machine + * architecture, extracting the information from header [hdr]. + *) +(*val get_elf64_machine_architecture : elf64_header -> natural*) +let get_elf64_machine_architecture hdr:Nat_big_num.num= + (Nat_big_num.of_string (Uint32.to_string hdr.elf64_machine)) + +(** [get_elf32_osabi hdr] returns the ELF file's declared OS/ABI + * architecture, extracting the information from header [hdr]. + *) +(*val get_elf32_osabi : elf32_header -> natural*) +let get_elf32_osabi hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_osabi) with + | Some osabi -> Nat_big_num.of_string (Uint32.to_string osabi) + | None -> failwith "get_elf32_osabi: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf64_osabi hdr] returns the ELF file's declared OS/ABI + * architecture, extracting the information from header [hdr]. + *) +(*val get_elf64_osabi : elf64_header -> natural*) +let get_elf64_osabi hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_osabi) with + | Some osabi -> Nat_big_num.of_string (Uint32.to_string osabi) + | None -> failwith "get_elf64_osabi: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf32_data_encoding hdr] returns the ELF file's declared data + * encoding, extracting the information from header [hdr]. + *) +(*val get_elf32_data_encoding : elf32_header -> natural*) +let get_elf32_data_encoding hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_data) with + | Some data -> Nat_big_num.of_string (Uint32.to_string data) + | None -> failwith "get_elf32_data_encoding: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf64_data_encoding hdr] returns the ELF file's declared data + * encoding, extracting the information from header [hdr]. + *) +(*val get_elf64_data_encoding : elf64_header -> natural*) +let get_elf64_data_encoding hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_data) with + | Some data -> Nat_big_num.of_string (Uint32.to_string data) + | None -> failwith "get_elf64_data_encoding: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf32_file_class hdr] returns the ELF file's declared file + * class, extracting the information from header [hdr]. + *) +(*val get_elf32_file_class : elf32_header -> natural*) +let get_elf32_file_class hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_class) with + | Some cls -> Nat_big_num.of_string (Uint32.to_string cls) + | None -> failwith "get_elf32_file_class: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf64_file_class hdr] returns the ELF file's declared file + * class, extracting the information from header [hdr]. + *) +(*val get_elf64_file_class : elf64_header -> natural*) +let get_elf64_file_class hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_class) with + | Some cls -> Nat_big_num.of_string (Uint32.to_string cls) + | None -> failwith "get_elf64_file_class: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf32_version_number hdr] returns the ELF file's declared version + * number, extracting the information from header [hdr]. + *) +(*val get_elf32_version_number : elf32_header -> natural*) +let get_elf32_version_number hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_version) with + | Some ver -> Nat_big_num.of_string (Uint32.to_string ver) + | None -> failwith "get_elf32_version_number: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf64_version_number hdr] returns the ELF file's declared version + * number, extracting the information from header [hdr]. + *) +(*val get_elf64_version_number : elf64_header -> natural*) +let get_elf64_version_number hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_version) with + | Some ver -> Nat_big_num.of_string (Uint32.to_string ver) + | None -> failwith "get_elf64_version_number: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [is_valid_elf32_version_number hdr] checks whether an ELF file's declared + * version number matches the current, mandatory version number. + * TODO: this should be merged into [is_valid_elf32_header] to create a single + * correctness check. + *) +(*val is_valid_elf32_version_number : elf32_header -> bool*) +let is_valid_elf32_version_numer hdr:bool= (Nat_big_num.equal +(get_elf32_version_number hdr) elf_ev_current) + +(** [is_valid_elf64_version_number hdr] checks whether an ELF file's declared + * version number matches the current, mandatory version number. + * TODO: this should be merged into [is_valid_elf64_header] to create a single + * correctness check. + *) +(*val is_valid_elf64_version_number : elf64_header -> bool*) +let is_valid_elf64_version_numer hdr:bool= (Nat_big_num.equal +(get_elf64_version_number hdr) elf_ev_current) + +(** [get_elf32_abi_version hdr] returns the ELF file's declared ABI version + * number, extracting the information from header [hdr]. + *) +(*val get_elf32_abi_version : elf32_header -> natural*) +let get_elf32_abi_version hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_abiversion) with + | Some ver -> Nat_big_num.of_string (Uint32.to_string ver) + | None -> failwith "get_elf32_abi_version: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [get_elf64_abi_version hdr] returns the ELF file's declared ABI version + * number, extracting the information from header [hdr]. + *) +(*val get_elf64_abi_version : elf64_header -> natural*) +let get_elf64_abi_version hdr:Nat_big_num.num= + ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_abiversion) with + | Some ver -> Nat_big_num.of_string (Uint32.to_string ver) + | None -> failwith "get_elf64_abi_version: lookup in ident failed" + )) (* Partial: should never return Nothing *) + +(** [deduce_endianness uc] deduces the endianness of an ELF file based on the ELF + * header's magic number [uc]. + *) +(*val deduce_endianness : list unsigned_char -> endianness*) +let deduce_endianness id2:endianness= + ((match Lem_list.list_index id2( 5) with + | None -> failwith "deduce_endianness: read of magic number has failed" + | Some v -> + if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string v)) elf_data_2lsb then + Little + else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string v)) elf_data_2msb then + Big + else + failwith "deduce_endianness: value is not valid" + )) + +(** [get_elf32_header_endianness hdr] returns the endianness of the ELF file + * as declared in its header, [hdr]. + *) +(*val get_elf32_header_endianness : elf32_header -> endianness*) +let get_elf32_header_endianness hdr:endianness= + (deduce_endianness (hdr.elf32_ident)) + +(** [get_elf64_header_endianness hdr] returns the endianness of the ELF file + * as declared in its header, [hdr]. + *) +(*val get_elf64_header_endianness : elf64_header -> endianness*) +let get_elf64_header_endianness hdr:endianness= + (deduce_endianness (hdr.elf64_ident)) + +(** [has_elf32_header_associated_entry_point hdr] checks whether the header + * [hdr] declares an entry point for the program. + *) +(*val has_elf32_header_associated_entry_point : elf32_header -> bool*) +let has_elf32_header_associated_entry_point hdr:bool= (not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string hdr.elf32_entry))(Nat_big_num.of_int 0))) + +(** [has_elf64_header_associated_entry_point hdr] checks whether the header + * [hdr] declares an entry point for the program. + *) +(*val has_elf64_header_associated_entry_point : elf64_header -> bool*) +let has_elf64_header_associated_entry_point hdr:bool= (not (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_entry)(Nat_big_num.of_int 0))) + +(** [has_elf32_header_string_table hdr] checks whether the header + * [hdr] declares whether the program has a string table or not. + *) +(*val has_elf32_header_string_table : elf32_header -> bool*) +let has_elf32_header_string_table hdr:bool= (not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) shn_undef)) + +(** [has_elf64_header_string_table hdr] checks whether the header + * [hdr] declares whether the program has a string table or not. + *) +(*val has_elf64_header_string_table : elf64_header -> bool*) +let has_elf64_header_string_table hdr:bool= (not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) shn_undef)) + +(** [is_elf32_header_section_size_in_section_header_table hdr] checks whether the header + * [hdr] declares whether the section size is too large to fit in the header + * field and is instead stored in the section header table. + *) +(*val is_elf32_header_section_size_in_section_header_table : elf32_header -> bool*) +let is_elf32_header_section_size_in_section_header_table hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf32_shnum))(Nat_big_num.of_int 0)) + +(** [is_elf64_header_section_size_in_section_header_table hdr] checks whether the header + * [hdr] declares whether the section size is too large to fit in the header + * field and is instead stored in the section header table. + *) +(*val is_elf64_header_section_size_in_section_header_table : elf64_header -> bool*) +let is_elf64_header_section_size_in_section_header_table hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf64_shnum))(Nat_big_num.of_int 0)) + +(** [is_elf32_header_string_table_index_in_link hdr] checks whether the header + * [hdr] declares whether the string table index is too large to fit in the + * header's field and is instead stored in the link field of an entry in the + * section header table. + *) +(*val is_elf32_header_string_table_index_in_link : elf32_header -> bool*) +let is_elf32_header_string_table_index_in_link hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) shn_xindex) + +(** [is_elf64_header_string_table_index_in_link hdr] checks whether the header + * [hdr] declares whether the string table index is too large to fit in the + * header's field and is instead stored in the link field of an entry in the + * section header table. + *) +(*val is_elf64_header_string_table_index_in_link : elf64_header -> bool*) +let is_elf64_header_string_table_index_in_link hdr:bool= (Nat_big_num.equal +(Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) shn_xindex) + +(** The [hdr_print_bundle] type is used to tidy up other type signatures. Some of the + * top-level string_of_ functions require six or more functions passed to them, + * which quickly gets out of hand. This type is used to reduce that complexity. + * The first component of the type is an OS specific print function, the second is + * a processor specific print function. + *) +type hdr_print_bundle = (Nat_big_num.num -> string) * (Nat_big_num.num -> string) + +(** [string_of_elf32_header hdr_bdl hdr] returns a string-based representation + * of header [hdr] using the ABI-specific print bundle [hdr_bdl]. + *) +(*val string_of_elf32_header : hdr_print_bundle -> elf32_header -> string*) +let string_of_elf32_header (os, proc) hdr:string= + (unlines [ +("\t" ^ ("Magic number: " ^ string_of_list + instance_Show_Show_Elf_types_native_uint_unsigned_char_dict hdr.elf32_ident)) + ; ("\t" ^ ("Endianness: " ^ string_of_endianness (deduce_endianness hdr.elf32_ident))) + ; ("\t" ^ ("Type: " ^ string_of_elf_file_type os proc (Nat_big_num.of_string (Uint32.to_string hdr.elf32_type)))) + ; ("\t" ^ ("Version: " ^ string_of_elf_version_number (Nat_big_num.of_string (Uint32.to_string hdr.elf32_version)))) + ; ("\t" ^ ("Machine: " ^ string_of_elf_machine_architecture (Nat_big_num.of_string (Uint32.to_string hdr.elf32_machine)))) + ; ("\t" ^ ("Entry point: " ^ Uint32.to_string hdr.elf32_entry)) + ; ("\t" ^ ("Flags: " ^ Uint32.to_string hdr.elf32_flags)) + ; ("\t" ^ ("Entries in program header table: " ^ Uint32.to_string hdr.elf32_phnum)) + ; ("\t" ^ ("Entries in section header table: " ^ Uint32.to_string hdr.elf32_shnum)) + ]) + +(** [string_of_elf64_header hdr_bdl hdr] returns a string-based representation + * of header [hdr] using the ABI-specific print bundle [hdr_bdl]. + *) +(*val string_of_elf64_header : hdr_print_bundle -> elf64_header -> string*) +let string_of_elf64_header (os, proc) hdr:string= + (unlines [ +("\t" ^ ("Magic number: " ^ string_of_list + instance_Show_Show_Elf_types_native_uint_unsigned_char_dict hdr.elf64_ident)) + ; ("\t" ^ ("Endianness: " ^ string_of_endianness (deduce_endianness hdr.elf64_ident))) + ; ("\t" ^ ("Type: " ^ string_of_elf_file_type os proc (Nat_big_num.of_string (Uint32.to_string hdr.elf64_type)))) + ; ("\t" ^ ("Version: " ^ string_of_elf_version_number (Nat_big_num.of_string (Uint32.to_string hdr.elf64_version)))) + ; ("\t" ^ ("Machine: " ^ string_of_elf_machine_architecture (Nat_big_num.of_string (Uint32.to_string hdr.elf64_machine)))) + ; ("\t" ^ ("Entry point: " ^ Uint64.to_string hdr.elf64_entry)) + ; ("\t" ^ ("Flags: " ^ Uint32.to_string hdr.elf64_flags)) + ; ("\t" ^ ("Entries in program header table: " ^ Uint32.to_string hdr.elf64_phnum)) + ; ("\t" ^ ("Entries in section header table: " ^ Uint32.to_string hdr.elf64_shnum)) + ]) + +(** The following are thin wrappers around the pretty-printing functions above + * using a default print bundle for the header. + *) + +(*val string_of_elf32_header_default : elf32_header -> string*) +let string_of_elf32_header_default:elf32_header ->string= + (string_of_elf32_header + (default_os_specific_print, + default_proc_specific_print)) + +(*val string_of_elf64_header_default : elf64_header -> string*) +let string_of_elf64_header_default:elf64_header ->string= + (string_of_elf64_header + (default_os_specific_print, + default_proc_specific_print)) + +let instance_Show_Show_Elf_header_elf32_header_dict:(elf32_header)show_class= ({ + + show_method = string_of_elf32_header_default}) + +let instance_Show_Show_Elf_header_elf64_header_dict:(elf64_header)show_class= ({ + + show_method = string_of_elf64_header_default}) + +(** [read_elf_ident bs0] reads the initial bytes of an ELF file from byte sequence + * [bs0], returning the remainder of the byte sequence too. + * Fails if transcription fails. + *) +(*val read_elf_ident : byte_sequence -> error (list unsigned_char * byte_sequence)*) +let read_elf_ident bs:((Uint32.uint32)list*byte_sequence)error= +(repeatM' ei_nident bs (read_unsigned_char default_endianness)) + +(** [bytes_of_elf32_header hdr] blits an ELF header [hdr] to a byte sequence, + * ready for transcription to a binary file. + *) +(*val bytes_of_elf32_header : elf32_header -> byte_sequence*) +let bytes_of_elf32_header hdr:byte_sequence= + (let endian = (deduce_endianness hdr.elf32_ident) in + Byte_sequence.from_byte_lists [ + Lem_list.map (fun u->Char.chr (Uint32.to_int u)) hdr.elf32_ident + ; bytes_of_elf32_half endian hdr.elf32_type + ; bytes_of_elf32_half endian hdr.elf32_machine + ; bytes_of_elf32_word endian hdr.elf32_version + ; bytes_of_elf32_addr endian hdr.elf32_entry + ; bytes_of_elf32_off endian hdr.elf32_phoff + ; bytes_of_elf32_off endian hdr.elf32_shoff + ; bytes_of_elf32_word endian hdr.elf32_flags + ; bytes_of_elf32_half endian hdr.elf32_ehsize + ; bytes_of_elf32_half endian hdr.elf32_phentsize + ; bytes_of_elf32_half endian hdr.elf32_phnum + ; bytes_of_elf32_half endian hdr.elf32_shentsize + ; bytes_of_elf32_half endian hdr.elf32_shnum + ; bytes_of_elf32_half endian hdr.elf32_shstrndx + ]) + +(** [bytes_of_elf64_header hdr] blits an ELF header [hdr] to a byte sequence, + * ready for transcription to a binary file. + *) +(*val bytes_of_elf64_header : elf64_header -> byte_sequence*) +let bytes_of_elf64_header hdr:byte_sequence= + (let endian = (deduce_endianness hdr.elf64_ident) in + Byte_sequence.from_byte_lists [ + Lem_list.map (fun u->Char.chr (Uint32.to_int u)) hdr.elf64_ident + ; bytes_of_elf64_half endian hdr.elf64_type + ; bytes_of_elf64_half endian hdr.elf64_machine + ; bytes_of_elf64_word endian hdr.elf64_version + ; bytes_of_elf64_addr endian hdr.elf64_entry + ; bytes_of_elf64_off endian hdr.elf64_phoff + ; bytes_of_elf64_off endian hdr.elf64_shoff + ; bytes_of_elf64_word endian hdr.elf64_flags + ; bytes_of_elf64_half endian hdr.elf64_ehsize + ; bytes_of_elf64_half endian hdr.elf64_phentsize + ; bytes_of_elf64_half endian hdr.elf64_phnum + ; bytes_of_elf64_half endian hdr.elf64_shentsize + ; bytes_of_elf64_half endian hdr.elf64_shnum + ; bytes_of_elf64_half endian hdr.elf64_shstrndx + ]) + +(*val is_elf32_header_padding_correct : elf32_header -> bool*) +let is_elf32_header_padding_correct ehdr:bool= ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 9)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 10)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 11)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 12)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 13)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 14)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) && (Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 15)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))))))))) + +(*val is_magic_number_correct : list unsigned_char -> bool*) +let is_magic_number_correct ident:bool= ((Lem.option_equal (=) +(Lem_list.list_index ident( 0)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 127))))) && ((Lem.option_equal (=) +(Lem_list.list_index ident( 1)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 69))))) && ((Lem.option_equal (=) +(Lem_list.list_index ident( 2)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 76))))) && (Lem.option_equal (=) +(Lem_list.list_index ident( 3)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 70)))))))) + +(** [read_elf32_header bs0] reads an ELF header from the byte sequence [bs0]. + * Fails if transcription fails. + *) +(*val read_elf32_header : byte_sequence -> error (elf32_header * byte_sequence)*) +let read_elf32_header bs:(elf32_header*byte_sequence)error= + (read_elf_ident bs >>= (fun (ident, bs) -> + if not (is_magic_number_correct ident) then + fail "read_elf32_header: magic number incorrect" + else + let endian = (deduce_endianness ident) in + read_elf32_half endian bs >>= (fun (typ, bs) -> + read_elf32_half endian bs >>= (fun (machine, bs) -> + read_elf32_word endian bs >>= (fun (version, bs) -> + read_elf32_addr endian bs >>= (fun (entry, bs) -> + read_elf32_off endian bs >>= (fun (phoff, bs) -> + read_elf32_off endian bs >>= (fun (shoff, bs) -> + read_elf32_word endian bs >>= (fun (flags, bs) -> + read_elf32_half endian bs >>= (fun (ehsize, bs) -> + read_elf32_half endian bs >>= (fun (phentsize, bs) -> + read_elf32_half endian bs >>= (fun (phnum, bs) -> + read_elf32_half endian bs >>= (fun (shentsize, bs) -> + read_elf32_half endian bs >>= (fun (shnum, bs) -> + read_elf32_half endian bs >>= (fun (shstrndx, bs) -> + (match Lem_list.list_index ident( 4) with + | None -> fail "read_elf32_header: transcription of ELF identifier failed" + | Some c -> + if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) elf_class_32 then + return ({ elf32_ident = ident; elf32_type = typ; + elf32_machine = machine; elf32_version = version; + elf32_entry = entry; elf32_phoff = phoff; + elf32_shoff = shoff; elf32_flags = flags; + elf32_ehsize = ehsize; elf32_phentsize = phentsize; + elf32_phnum = phnum; elf32_shentsize = shentsize; + elf32_shnum = shnum; elf32_shstrndx = shstrndx }, bs) + else + fail "read_elf32_header: not a 32-bit ELF file" + )))))))))))))))) + +(** [read_elf64_header bs0] reads an ELF header from the byte sequence [bs0]. + * Fails if transcription fails. + *) +(*val read_elf64_header : byte_sequence -> error (elf64_header * byte_sequence)*) +let read_elf64_header bs:(elf64_header*byte_sequence)error= + (read_elf_ident bs >>= (fun (ident, bs) -> + if not (is_magic_number_correct ident) then + fail "read_elf64_header: magic number incorrect" + else + let endian = (deduce_endianness ident) in + read_elf64_half endian bs >>= (fun (typ, bs) -> + read_elf64_half endian bs >>= (fun (machine, bs) -> + read_elf64_word endian bs >>= (fun (version, bs) -> + read_elf64_addr endian bs >>= (fun (entry, bs) -> + read_elf64_off endian bs >>= (fun (phoff, bs) -> + read_elf64_off endian bs >>= (fun (shoff, bs) -> + read_elf64_word endian bs >>= (fun (flags, bs) -> + read_elf64_half endian bs >>= (fun (ehsize, bs) -> + read_elf64_half endian bs >>= (fun (phentsize, bs) -> + read_elf64_half endian bs >>= (fun (phnum, bs) -> + read_elf64_half endian bs >>= (fun (shentsize, bs) -> + read_elf64_half endian bs >>= (fun (shnum, bs) -> + read_elf64_half endian bs >>= (fun (shstrndx, bs) -> + (match Lem_list.list_index ident( 4) with + | None -> fail "read_elf64_header: transcription of ELF identifier failed" + | Some c -> + if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) elf_class_64 then + return ({ elf64_ident = ident; elf64_type = typ; + elf64_machine = machine; elf64_version = version; + elf64_entry = entry; elf64_phoff = phoff; + elf64_shoff = shoff; elf64_flags = flags; + elf64_ehsize = ehsize; elf64_phentsize = phentsize; + elf64_phnum = phnum; elf64_shentsize = shentsize; + elf64_shnum = shnum; elf64_shstrndx = shstrndx }, bs) + else + fail "read_elf64_header: not a 64-bit ELF file" + )))))))))))))))) + +(** [is_elf32_header_class_correct hdr] checks whether the declared file class + * is correct. + *) +(*val is_elf32_header_class_correct : elf32_header -> bool*) +let is_elf32_header_class_correct ehdr:bool= (Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 4)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))))) + +(** [is_elf64_header_class_correct hdr] checks whether the declared file class + * is correct. + *) +(*val is_elf64_header_class_correct : elf64_header -> bool*) +let is_elf64_header_class_correct ehdr:bool= (Lem.option_equal (=) +(Lem_list.list_index ehdr.elf64_ident( 4)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))))) + +(** [is_elf32_header_version_correct hdr] checks whether the declared file version + * is correct. + *) +(*val is_elf32_header_version_correct : elf32_header -> bool*) +let is_elf32_header_version_correct ehdr:bool= (Lem.option_equal (=) +(Lem_list.list_index ehdr.elf32_ident( 6)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))))) + +(** [is_elf64_header_version_correct hdr] checks whether the declared file version + * is correct. + *) +(*val is_elf64_header_version_correct : elf64_header -> bool*) +let is_elf64_header_version_correct ehdr:bool= (Lem.option_equal (=) +(Lem_list.list_index ehdr.elf64_ident( 6)) (Some (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))))) + +(** [is_elf32_header_valid] checks whether an [elf32_header] value is a valid 32-bit + * ELF file header (i.e. [elf32_ident] is [ei_nident] entries long, and other + * constraints on headers). + *) +(*val is_elf32_header_valid : elf32_header -> bool*) +let is_elf32_header_valid ehdr:bool= (Nat_big_num.equal +(Nat_big_num.of_int (List.length ehdr.elf32_ident)) ei_nident && +(is_magic_number_correct ehdr.elf32_ident && +(is_elf32_header_padding_correct ehdr && +(is_elf32_header_class_correct ehdr && + is_elf32_header_version_correct ehdr)))) + +(** [get_elf32_header_program_table_size] calculates the size of the program table + * (entry size x number of entries) based on data in the ELF header. + *) +(*val get_elf32_header_program_table_size : elf32_header -> natural*) +let get_elf32_header_program_table_size ehdr:Nat_big_num.num= + (let phentsize = (Nat_big_num.of_string (Uint32.to_string ehdr.elf32_phentsize)) in + let phnum = (Nat_big_num.of_string (Uint32.to_string ehdr.elf32_phnum)) in Nat_big_num.mul + phentsize phnum) + +(** [get_elf64_header_program_table_size] calculates the size of the program table + * (entry size x number of entries) based on data in the ELF header. + *) +(*val get_elf64_header_program_table_size : elf64_header -> natural*) +let get_elf64_header_program_table_size ehdr:Nat_big_num.num= + (let phentsize = (Nat_big_num.of_string (Uint32.to_string ehdr.elf64_phentsize)) in + let phnum = (Nat_big_num.of_string (Uint32.to_string ehdr.elf64_phnum)) in Nat_big_num.mul + phentsize phnum) + +(** [is_elf32_header_section_table_present] calculates whether a section table + * is present in the ELF file or not. + *) +(*val is_elf32_header_section_table_present : elf32_header -> bool*) +let is_elf32_header_section_table_present ehdr:bool= + (not ( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ehdr.elf32_shoff))(Nat_big_num.of_int 0))) + +(** [is_elf64_header_section_table_present] calculates whether a section table + * is present in the ELF file or not. + *) +(*val is_elf64_header_section_table_present : elf64_header -> bool*) +let is_elf64_header_section_table_present ehdr:bool= + (not ( Nat_big_num.equal(Nat_big_num.of_string (Uint64.to_string ehdr.elf64_shoff))(Nat_big_num.of_int 0))) + +(** [get_elf32_header_section_table_size] calculates the size of the section table + * (entry size x number of entries) based on data in the ELF header. + *) +(*val get_elf32_header_section_table_size : elf32_header -> natural*) +let get_elf32_header_section_table_size ehdr:Nat_big_num.num= + (let shentsize = (Nat_big_num.of_string (Uint32.to_string ehdr.elf32_shentsize)) in + let shnum = (Nat_big_num.of_string (Uint32.to_string ehdr.elf32_shnum)) in Nat_big_num.mul + shentsize shnum) + +(** [get_elf64_header_section_table_size] calculates the size of the section table + * (entry size x number of entries) based on data in the ELF header. + *) +(*val get_elf64_header_section_table_size : elf64_header -> natural*) +let get_elf64_header_section_table_size ehdr:Nat_big_num.num= + (let shentsize = (Nat_big_num.of_string (Uint32.to_string ehdr.elf64_shentsize)) in + let shnum = (Nat_big_num.of_string (Uint32.to_string ehdr.elf64_shnum)) in Nat_big_num.mul + shentsize shnum) |