package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/sail_interface.ml.html
Source file sail_interface.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213(*Generated by Lem from adaptors/sail_interface.lem.*) open Lem_basic_classes open Lem_function open Lem_list open Lem_maybe open Lem_num open Lem_string open Lem_tuple open Lem_assert_extra open Byte_sequence open Error open Missing_pervasives open Show open Elf_header open Elf_file open Elf_interpreted_section open Elf_interpreted_segment open String_table open Elf_symbol_table open Elf_program_header_table open Elf_types_native_uint open Hex_printing type executable_process_image = | ELF_Class_32 of elf32_executable_process_image | ELF_Class_64 of elf64_executable_process_image (*val string_of_segment_provenance : segment_provenance -> string*) let string_of_segment_provenance p:string= ((match p with | FromELF -> "Segment from ELF file" | AutoGenerated -> "Segment auto generated" )) (*val string_of_executable_process_image : executable_process_image -> string*) let string_of_executable_process_image img2:string= ((match img2 with | ELF_Class_32 (segs, entry_point, machine_type) -> let machine_type = (string_of_elf_machine_architecture machine_type) in let entry_point = (unsafe_hex_string_of_natural 16 entry_point) in let segs = (Lem_list.map (fun (seg, prov) -> let prov = (string_of_segment_provenance prov) in let seg = (string_of_elf32_interpreted_segment seg) in "Segment provenance: " ^ (prov ^ ("\n" ^ seg)) ) segs) in unlines ( List.rev_append (List.rev [ "32-bit ELF executable image" ; ("Machine type: " ^ machine_type) ; ("Entry point: " ^ entry_point) ; "" ]) segs) | ELF_Class_64 (segs, entry_point, machine_type) -> let machine_type = (string_of_elf_machine_architecture machine_type) in let entry_point = (unsafe_hex_string_of_natural 16 entry_point) in let segs = (intercalate "\n" (Lem_list.map (fun (seg, prov) -> let prov = (string_of_segment_provenance prov) in let seg = (string_of_elf64_interpreted_segment seg) in "Segment provenance: " ^ (prov ^ ("\n" ^ seg)) ) segs)) in unlines ( List.rev_append (List.rev [ "64-bit ELF executable image" ; ("Machine type: " ^ machine_type) ; ("Entry point: " ^ entry_point) ; "" ]) segs) )) (*val populate : string -> error executable_process_image*) let populate fname1:(executable_process_image)error= (bind ( (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "populate: ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun ef5 -> if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then bind (Elf_file.get_elf32_executable_image ef5) (fun img2 -> return (ELF_Class_32 img2)) else fail "populate: not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun ef5 -> if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then bind (Elf_file.get_elf64_executable_image ef5) (fun img2 -> return (ELF_Class_64 img2)) else fail "populate: not a statically linked executable") else fail "populate: ELF class unrecognised" )))) (*val populate' : byte_sequence -> error executable_process_image*) let populate' bs0:(executable_process_image)error= (bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "populate': ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun ef5 -> if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then bind (Elf_file.get_elf32_executable_image ef5) (fun img2 -> return (ELF_Class_32 img2)) else fail "populate': not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun ef5 -> if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then bind (Elf_file.get_elf64_executable_image ef5) (fun img2 -> return (ELF_Class_64 img2)) else fail "populate': not a statically linked executable") else fail "populate': ELF class unrecognised" ))) (*val obtain_global_symbol_init_info : string -> error global_symbol_init_info*) let obtain_global_symbol_init_info fname1:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error= (bind ( (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "obtain_global_symbol_init_info: ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 -> if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> return init1) else fail "obtain_global_symbol_init_info: not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 -> if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> return init1) else fail "obtain_global_symbol_init_info: not a statically linked executable") else fail "obtain_global_symbol_init_info: ELF class unrecognised" )))) (*val obtain_global_symbol_init_info' : byte_sequence -> error global_symbol_init_info*) let obtain_global_symbol_init_info' bs0:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error= (bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "obtain_global_symbol_init_info': ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 -> if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> return init1) else fail "obtain_global_symbol_init_info': not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 -> if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> return init1) else fail "obtain_global_symbol_init_info': not a statically linked executable") else fail "obtain_global_symbol_init_info': ELF class unrecognised" ))) (*val populate_and_obtain_global_symbol_init_info : string -> error (elf_file * executable_process_image * global_symbol_init_info)*) let populate_and_obtain_global_symbol_init_info fname1:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error= (bind ( (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "populate_and_obtain_global_symbol_init_info: ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 -> if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf32_executable_image f1) (fun img2 -> return ((ELF_File_32 f1), (ELF_Class_32 img2), init1))) else fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 -> if (* hack *) true (* Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table*) then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf64_executable_image f1) (fun img2 -> return ((ELF_File_64 f1), (ELF_Class_64 img2), init1))) else fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable") else fail "populate_and_obtain_global_symbol_init_info: ELF class unrecognised" )))) (*val populate_and_obtain_global_symbol_init_info' : byte_sequence -> error (elf_file * executable_process_image * global_symbol_init_info)*) let populate_and_obtain_global_symbol_init_info' bs0:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error= (bind ( (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness)) (fun (ident, bs) -> (match Lem_list.list_index ident 4 with | None -> fail "populate_and_obtain_global_symbol_init_info': ELF ident transcription error" | Some c -> (* Calculate whether we are dealing with a 32- or 64-bit file based on * what we have read... *) if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 -> if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf32_executable_image f1) (fun img2 -> return ((ELF_File_32 f1), (ELF_Class_32 img2), init1))) else fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable") else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 -> if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf64_executable_image f1) (fun img2 -> return ((ELF_File_64 f1), (ELF_Class_64 img2), init1))) else fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable") else fail "populate_and_obtain_global_symbol_init_info': ELF class unrecognised" )))