diff options
Diffstat (limited to 'src')
32 files changed, 4761 insertions, 4 deletions
diff --git a/src/Makefile b/src/Makefile index 21e821ea..cc651e21 100644 --- a/src/Makefile +++ b/src/Makefile @@ -7,15 +7,37 @@ full: sail lib power doc test sail: ocamlbuild sail.native sail_lib.cma sail_lib.cmxa -test: sail +interpreter: + ocamlbuild lem_interp/extract.cmxa + ocamlbuild lem_interp/extract.cma + +test: sail interpreter ocamlbuild test/run_tests.native ./run_tests.native -power: sail - ocamlbuild test/run_power.native +LEM = ~/bitbucket/lem/lem +LEMLIB = ~/bitbucket/lem/ocaml-lib/_build/ + +install_elf: + cp -p ../../system-v-abi/src/*.lem elf_model/ + cp -p ../../system-v-abi/src/*.ml elf_model/ + +power: sail interpreter + mkdir -p _build/test + mkdir -p _build/elf_model + cp -p test/* _build/test/ + cp -p elf_model/* _build/elf_model + cd _build/elf_model ;\ + $(LEM) -ocaml -only_changed_output missing_pervasives.lem show.lem endianness.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_header.lem elf_file1.lem elf_program_header_table.lem elf_executable_file2.lem elf_section_header_table.lem elf_executable_file3.lem string_table.lem elf_executable_file4.lem elf_executable_file5.lem sail_interface.lem main.lem ;\ + ocamlfind ocamlopt -package bitstring.syntax -package batteries -package uint -package bitstring -syntax camlp4o -I $(LEMLIB) nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx -linkpkg missing_pervasives.ml show.ml endianness.ml error.ml ml_bindings.ml bitstring_local.ml elf_types.ml elf_header.ml elf_file1.ml elf_program_header_table.ml elf_executable_file2.ml string_table.ml elf_section_header_table.ml elf_executable_file3.ml elf_executable_file4.ml elf_interpreted_segment.ml elf_executable_file5.ml sail_interface.ml main.ml ;\ + ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIB) -a -o elf_extract.cmxa nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx missing_pervasives.cmx show.cmx endianness.cmx error.cmx ml_bindings.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx + cd _build/test ;\ + ../../sail.native -lem_ast power.sail ;\ + $(LEM) -ocaml -only_changed_output -lib ../lem_interp/ power.lem;\ + ocamlfind ocamlopt -package num -package bitstring -package batteries -package uint -I $(LEMLIB) -I ../lem_interp/ -I ../elf_model/ -linkpkg $(LEMLIB)extract.cmxa ../pprint/src/PPrintLib.cmxa ../lem_interp/extract.cmxa elf_extract.cmxa power.ml run_power.ml -o run_power.native + ln -fs _build/test/run_power.native run_power.native test_power: power - #../../../rsem/idl/power/binary/run.sh ./run_power.native --file ../../../rsem/idl/power/binary/main.bin test_power_interactive: power diff --git a/src/elf_model/Makefile b/src/elf_model/Makefile new file mode 100644 index 00000000..42e17cce --- /dev/null +++ b/src/elf_model/Makefile @@ -0,0 +1,24 @@ +dummy: all + +lem-model: + ../../lem/lem -ocaml -only_changed_output missing_pervasives.lem show.lem endianness.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_header.lem elf_file1.lem elf_program_header_table.lem elf_executable_file2.lem elf_section_header_table.lem elf_executable_file3.lem string_table.lem elf_executable_file4.lem elf_executable_file5.lem sail_interface.lem main.lem + +clean: + rm missing_pervasives.ml show.ml endianness.ml bitstring_local.ml elf_types.ml elf_header.ml elf_file1.ml elf_program_header_table.ml elf_executable_file2.ml elf_section_header_table.ml elf_executable_file3.ml string_table.ml elf_executable_file4.ml elf_interpreted_segment.ml elf_executable_file5.ml sail_interface.ml main.ml + +ocaml: + ocamlfind ocamlc -package bitstring.syntax -package batteries -package uint -syntax camlp4o -I ../../lem/ocaml-lib/_build/ unix.cma bitstring.cma nums.cma nat_num.cmo lem.cmo lem_function.cmo lem_list.cmo -linkpkg missing_pervasives.ml show.ml endianness.ml error.ml ml_bindings.ml bitstring_local.ml elf_types.ml elf_header.ml elf_file1.ml elf_program_header_table.ml elf_executable_file2.ml string_table.ml elf_section_header_table.ml elf_executable_file3.ml elf_executable_file4.ml elf_interpreted_segment.ml elf_executable_file5.ml sail_interface.ml main.ml + +stacktrace: + export OCAMLRUNPARAM=b + ocamlfind ocamlc -package bitstring.syntax -package batteries -syntax camlp4o -I ../../lem/ocaml-lib/_build/ unix.cma bitstring.cma nums.cma nat_num.cmo lem.cmo lem_function.cmo lem_list.cmo -linkpkg -g missing_pervasives.ml show.ml endianness.ml error.ml ml_bindings.ml bitstring_local.ml elf_types.ml elf_header.ml elf_file1.ml elf_program_header_table.ml elf_executable_file2.ml string_table.ml elf_section_header_table.ml elf_executable_file3.ml elf_executable_file4.ml elf_interpreted_segment.ml elf_executable_file5.ml sail_interface.ml main.ml + +all: lem-model ocaml + +execute: + ./a.out + +go: all execute + +go-debug: lem-model stacktrace execute + diff --git a/src/elf_model/bitstring.lem b/src/elf_model/bitstring.lem new file mode 100644 index 00000000..ed9df857 --- /dev/null +++ b/src/elf_model/bitstring.lem @@ -0,0 +1,87 @@ +open import Basic_classes +open import Bool +open import Num +open import Show + +open import Error + +declare {ocaml} rename module = bitstring_local + +type bitstring + +declare ocaml target_rep type bitstring = `Bitstring.bitstring` + +(** [empty] is the empty bitstring. + *) +val empty : bitstring + +declare ocaml target_rep function empty = `Bitstring.empty` + +(** [zeros m] creates a bitstring of length [m] containing all zeros. + *) +val zeros : nat -> bitstring + +declare ocaml target_rep function zeros = `Bitstring.create_bitstring` + +(** [create m c] creates a bitstring of length [m] containing all [c] + * characters. + *) +val create : nat -> char -> bitstring + +declare ocaml target_rep function create = `Bitstring.make_bitstring` + +(** [concat xs] concatenates a list of bitstrings [xs] into a single bitstring. + *) +val concat : list bitstring -> bitstring + +declare ocaml target_rep function concat = `Bitstring.concat` + +(** [acquire fname] acquires a bitstring from a binary file, located at [fname]. + *) +val acquire : string -> error bitstring + +declare ocaml target_rep function acquire = `Ml_bindings.acquire_bitstring` + +(** [length bs0] returns the length of bitstring [bs0]. + *) +val length : bitstring -> nat + +declare ocaml target_rep function length = `Bitstring.bitstring_length` + +(** [partition offset bs0] cuts [bs0] into two pieces at offset [offset]. Throws + * an exception if + *) +val partition : nat -> bitstring -> (bitstring * bitstring) + +declare ocaml target_rep function partition = `Ml_bindings.partition_bitstring` + +(** [offset_and_cut offset size bs0] cuts a [size]-lengthed bitstring out of [bs0] + * at offset [offset]. + *) +val offset_and_cut : nat -> nat -> bitstring -> bitstring +let offset_and_cut offset size bs0 = + let (_, cut) = partition offset bs0 in + let (rel, _) = partition size cut in + rel + +(** [equal bs0 bs1] tests whether [bs0] and [bs1] are equal. + *) +val equal : bitstring -> bitstring -> bool + +declare ocaml target_rep function equal = unsafe_structural_equality + +(** [string_of_bitstring bs0] produces a string-based representation of bitstring + * [bs0]. + *) +val string_of_bitstring : bitstring -> string + +declare ocaml target_rep function string_of_bitstring = `Bitstring.string_of_bitstring` + +instance (Eq bitstring) + let (=) = equal + let (<>) l r = not (equal l r) +end + +instance (Show bitstring) + let show = string_of_bitstring +end diff --git a/src/elf_model/bitstring.ml b/src/elf_model/bitstring.ml new file mode 100644 index 00000000..82eeec18 --- /dev/null +++ b/src/elf_model/bitstring.ml @@ -0,0 +1,18 @@ +(*Generated by Lem from bitstring.lem.*) +open Lem_basic_classes +open Lem_bool +open Lem_num + +(*type bitstring*) + +(*val length : bitstring -> nat*) + +(*val partition : nat -> bitstring -> (bitstring * bitstring)*) + +(*val equal : bitstring -> bitstring -> bool*) + +let instance_Basic_classes_Eq_Bitstring_bitstring_dict =({ + + isEqual_method = (=); + + isInequal_method = (fun l r->not (l = r))}) diff --git a/src/elf_model/bytestring.ml b/src/elf_model/bytestring.ml new file mode 100644 index 00000000..83f5e476 --- /dev/null +++ b/src/elf_model/bytestring.ml @@ -0,0 +1,17 @@ +(*Generated by Lem from bytestring.lem.*) +open Lem_basic_classes +open Lem_bool +open Lem_num + +(*type bitstring*) + +(*val length : bitstring -> nat*) +(*val partition : nat -> bitstring -> (bitstring * bitstring)*) + +(*val equal : bitstring -> bitstring -> bool*) + +let instance_Basic_classes_Eq_Bytestring_bitstring_dict =({ + + isEqual_method = (=); + + isInequal_method = (fun l r->not (l = r))}) diff --git a/src/elf_model/elf.ml b/src/elf_model/elf.ml new file mode 100644 index 00000000..ae78935a --- /dev/null +++ b/src/elf_model/elf.ml @@ -0,0 +1,90 @@ +(*Generated by Lem from elf.lem.*) +open Lem_list +open Lem_list_extra +open Lem_maybe +open Lem_num +open Lem_string + +open Elf_header +open Elf_program_header_table +open Elf_section_header +open Elf_string_table +open Elf_symbol_table + +open Bitstring +open Error + +type linked_elf_file = + { elf_header : elf32_elf_header + ; elf_section_header_table : elf32_section_header_table option + ; elf_program_header_table : elf32_program_header_table + ; elf_string_table : string list + ; elf_dynamic_string_table : string list + ; elf_symbol_table : elf32_symbol_table list + } + +type elf32 + = Linked of linked_elf_file + | Executable + +let is_linked elf = +((match elf with + | Linked _ -> true + | _ -> false + )) + +let is_executable elf = +((match elf with + | Executable -> true + | _ -> false + )) + +let string_of_elf32 elf320 = +((match elf320 with + | Executable -> + List.fold_right (^) [ + "Executable ELF file" + ] "" + | Linked link -> + let shdr = +((match link.elf_section_header_table with + | None -> "No section header table present" + | Some hdr -> string_of_elf32_section_header_table hdr + )) + in + let symtabs = +(List.fold_right (^) (List.map string_of_elf32_symbol_table link.elf_symbol_table) "") + in + List.fold_right (^) [ + string_of_elf32_elf_header (fun x -> "Unsupported") (fun x -> "Unsupported") link.elf_header; "\n\n" + ; string_of_elf32_program_header_table (fun x -> "Unsupported") (fun x -> "Unsupported") link.elf_program_header_table + ; shdr + ; string_of_elf32_string_table link.elf_string_table + ; string_of_elf32_dynamic_string_table link.elf_dynamic_string_table + ; symtabs + ] "\t" + )) + +let read_elf32 bs0 = +(read_elf32_elf_header bs0 >>= (fun (elf_header0, bs1) -> + let (size, entry_size) = (program_header_table_size_and_entry_size elf_header0) in + read_elf32_program_header_table (size * entry_size) bs1 >>= (fun (program_header_table, bs2) -> + (if elf32_elf_header_is_section_table_present elf_header0 then + let (size, entry_size, offset) = (section_header_table_size_and_entry_size_and_offset elf_header0) in + read_elf32_section_header_table size entry_size offset bs0 >>= (fun (section_header_table, bs3) -> + return (Some section_header_table, bs3)) + else + return (None, bs2)) >>= (fun (section_header_table_opt, bs3) -> + let string_tables = (read_elf32_string_tables section_header_table_opt bs0) in + ((match section_header_table_opt with + | None -> return [] + | Some section_header_table -> read_elf32_symbol_tables section_header_table bs0 + )) >>= (fun symbol_table -> + return (Linked ( + { elf_header = elf_header0 + ; elf_section_header_table = section_header_table_opt + ; elf_program_header_table = program_header_table + ; elf_string_table = (List.nth (string_tables)( 1)) + ; elf_dynamic_string_table = (List.nth (string_tables)( 0)) + ; elf_symbol_table = symbol_table + }))))))) diff --git a/src/elf_model/elf_executable_file2.lem b/src/elf_model/elf_executable_file2.lem new file mode 100644 index 00000000..4c539294 --- /dev/null +++ b/src/elf_model/elf_executable_file2.lem @@ -0,0 +1,175 @@ +open import Basic_classes +open import Bool +open import Maybe +open import Num +open import String + +open import Elf_file1 +open import Elf_header +open import Elf_program_header_table +open import Elf_types + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** Type [elf32_executable_file2] represents the lazy unfolding of a 32-bit ELF + * file where the structure of the header, program header table (mandatory). + *) +type elf32_executable_file2 = + <| elf32_executable_file2_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file2_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file2_body : bitstring (** Uninterpreted data *) + |> + +class (HasElf32ExecutableFile2 'a) + val get_elf32_executable_file2 : 'a -> elf32_executable_file2 +end + +instance (HasElf32ExecutableFile2 elf32_executable_file2) + let get_elf32_executable_file2 f2 = f2 +end + +instance (HasElf32File1 elf32_executable_file2) + let get_elf32_file1 f2 = + <| elf32_file1_header = f2.elf32_executable_file2_header; + elf32_file1_body = f2.elf32_executable_file2_body |> +end + +instance (HasElf32Header elf32_executable_file2) + let get_elf32_header f2 = f2.elf32_executable_file2_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file2) + let get_elf32_program_header_table f2 = Just (f2.elf32_executable_file2_program_header_table) +end + +(** Type [elf64_executable_file2] represents the lazy unfolding of a 64-bit ELF + * file where the structure of the header, program header table (mandatory). + *) +type elf64_executable_file2 = + <| elf64_executable_file2_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file2_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file2_body : bitstring (** Uninterpreted data *) + |> + +class (HasElf64ExecutableFile2 'a) + val get_elf64_executable_file2 : 'a -> elf64_executable_file2 +end + +instance (HasElf64ExecutableFile2 elf64_executable_file2) + let get_elf64_executable_file2 f2 = f2 +end + +instance (HasElf64File1 elf64_executable_file2) + let get_elf64_file1 f2 = + <| elf64_file1_header = f2.elf64_executable_file2_header; + elf64_file1_body = f2.elf64_executable_file2_body |> +end + +instance (HasElf64Header elf64_executable_file2) + let get_elf64_header f2 = f2.elf64_executable_file2_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file2) + let get_elf64_program_header_table f2 = Just (f2.elf64_executable_file2_program_header_table) +end + +(** [refine_elf32_file1 f1] refines the [elf31_file1] [f1] adding the + * mandatory program header table to [f1]'s header. Fails if [f1]'s header + * states that no program header table is present, or if there is some other + * transcription error when reading from [f1]'s body. + *) +val refine_elf32_file1 : elf32_file1 -> error elf32_executable_file2 +let refine_elf32_file1 f1 = + if not (is_executable_elf32_file1 f1) then + Fail "refine_elf32_file1: not an executable file type" + else + let hdr = f1.elf32_file1_header in + let endian = get_elf32_header_endianness hdr in + let bs1 = f1.elf32_file1_body in + let pentries = nat_of_elf32_half hdr.elf32_phnum in + let pentry_size = nat_of_elf32_half hdr.elf32_phentsize * 8 in + let psize = pentries * pentry_size in + if psize = 0 then + Fail "refine_elf32_file1: program header table not present" + else + let poffset = nat_of_elf32_off hdr.elf32_phoff * 8 in + let (_, pcut) = partition poffset bs1 in + let (pexact, _) = partition psize pcut in + (* Bitstring irrelevant below as exact size used... *) + read_elf32_program_header_table psize endian pexact >>= fun (pht, _) -> + return <| elf32_executable_file2_header = hdr; + elf32_executable_file2_program_header_table = pht; + elf32_executable_file2_body = bs1 |> + +(** [refine_elf64_file1 f1] refines the [elf31_file1] [f1] adding the + * mandatory program header table to [f1]'s header. Fails if [f1]'s header + * states that no program header table is present, or if there is some other + * transcription error when reading from [f1]'s body. + *) +val refine_elf64_file1 : elf64_file1 -> error elf64_executable_file2 +let refine_elf64_file1 f1 = + if not (is_executable_elf64_file1 f1) then + Fail "refine_elf64_file1: not an executable file type" + else + let hdr = f1.elf64_file1_header in + let endian = get_elf64_header_endianness hdr in + let bs1 = f1.elf64_file1_body in + let pentries = nat_of_elf64_half hdr.elf64_phnum in + let pentry_size = nat_of_elf64_half hdr.elf64_phentsize * 8 in + let psize = pentries * pentry_size in + if psize = 0 then + Fail "refine_elf64_file1: program header table not present" + else + let poffset = nat_of_elf64_off hdr.elf64_phoff * 8 in + let (_, pcut) = partition poffset bs1 in + let (pexact, _) = partition psize pcut in + (* Bitstring irrelevant below as exact size used... *) + read_elf64_program_header_table psize endian pexact >>= fun (pht, _) -> + return <| elf64_executable_file2_header = hdr; + elf64_executable_file2_program_header_table = pht; + elf64_executable_file2_body = bs1 |> + +(** [read_elf32_executable_file2 bs0] creates an [elf32_executable_file2] record + * directly from the bitstring [bs0]. + *) +val read_elf32_executable_file2 : bitstring -> error elf32_executable_file2 +let read_elf32_executable_file2 bs0 = + read_elf32_file1 bs0 >>= refine_elf32_file1 + +(** [read_elf64_executable_file2 bs0] creates an [elf64_executable_file2] record + * directly from the bitstring [bs0]. + *) +val read_elf64_executable_file2 : bitstring -> error elf64_executable_file2 +let read_elf64_executable_file2 bs0 = + read_elf64_file1 bs0 >>= refine_elf64_file1 + +(** [string_of_elf32_executable_file2 os proc f2] creates a string representation of [f2]. + *) +val string_of_elf32_executable_file2 : hdr_print_bundle -> pht_print_bundle -> elf32_executable_file2 -> string +let string_of_elf32_executable_file2 hdr_bdl pht_bdl f2 = + unlines [ + "\n*Type elf32_executable_file2:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f2.elf32_executable_file2_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f2.elf32_executable_file2_program_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_executable_file2_body) + ] + +(** [string_of_elf64_executable_file2 os proc f2] creates a string representation of [f2]. + *) +val string_of_elf64_executable_file2 : hdr_print_bundle -> pht_print_bundle -> elf64_executable_file2 -> string +let string_of_elf64_executable_file2 hdr_bdl pht_bdl f2 = + unlines [ + "\n*Type elf64_executable_file2:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f2.elf64_executable_file2_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f2.elf64_executable_file2_program_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_executable_file2_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_executable_file3.lem b/src/elf_model/elf_executable_file3.lem new file mode 100644 index 00000000..07a2fdc1 --- /dev/null +++ b/src/elf_model/elf_executable_file3.lem @@ -0,0 +1,211 @@ +open import Basic_classes +open import Num +open import Maybe +open import String + +open import Elf_executable_file2 +open import Elf_header +open import Elf_types +open import Elf_section_header_table +open import Elf_program_header_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** Type [elf32_executable_file3] represents the lazy unfolding of a 32-bit ELF + * file where the header, program header table and optional section header table + * have been filled in, with all other data being left uninterpreted. + *) +type elf32_executable_file3 = + <| elf32_executable_file3_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file3_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file3_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) + ; elf32_executable_file3_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf32ExecutableFile3 'a) + val get_elf32_executable_file3 : 'a -> elf32_executable_file3 +end + +instance (HasElf32ExecutableFile3 elf32_executable_file3) + let get_elf32_executable_file3 f3 = f3 +end + +instance (HasElf32ExecutableFile2 elf32_executable_file3) + let get_elf32_executable_file2 f3 = + <| elf32_executable_file2_header = f3.elf32_executable_file3_header; + elf32_executable_file2_program_header_table = f3.elf32_executable_file3_program_header_table; + elf32_executable_file2_body = f3.elf32_executable_file3_body |> +end + +instance (HasElf32Header elf32_executable_file3) + let get_elf32_header f3 = f3.elf32_executable_file3_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file3) + let get_elf32_program_header_table f3 = + Just (f3.elf32_executable_file3_program_header_table) +end + +instance (HasElf32SectionHeaderTable elf32_executable_file3) + let get_elf32_section_header_table f3 = + f3.elf32_executable_file3_section_header_table +end + +(** Type [elf64_executable_file3] represents the lazy unfolding of a 64-bit ELF + * file where the header, program header table and optional section header table + * have been filled in, with all other data being left uninterpreted. + *) +type elf64_executable_file3 = + <| elf64_executable_file3_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file3_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file3_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) + ; elf64_executable_file3_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf64ExecutableFile3 'a) + val get_elf64_executable_file3 : 'a -> elf64_executable_file3 +end + +instance (HasElf64ExecutableFile3 elf64_executable_file3) + let get_elf64_executable_file3 f3 = f3 +end + +instance (HasElf64ExecutableFile2 elf64_executable_file3) + let get_elf64_executable_file2 f3 = + <| elf64_executable_file2_header = f3.elf64_executable_file3_header; + elf64_executable_file2_program_header_table = f3.elf64_executable_file3_program_header_table; + elf64_executable_file2_body = f3.elf64_executable_file3_body |> +end + +instance (HasElf64Header elf64_executable_file3) + let get_elf64_header f3 = f3.elf64_executable_file3_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file3) + let get_elf64_program_header_table f3 = + Just (f3.elf64_executable_file3_program_header_table) +end + +instance (HasElf64SectionHeaderTable elf64_executable_file3) + let get_elf64_section_header_table f3 = + f3.elf64_executable_file3_section_header_table +end + +(** [refine_elf32_executable_file2 f2] refines an elf32_executable_file2 [f2] into + * an elf32_executable_file3 by adding the optional section header table. + *) +val refine_elf32_executable_file2 : elf32_executable_file2 -> error elf32_executable_file3 +let refine_elf32_executable_file2 f2 = + let hdr = f2.elf32_executable_file2_header in + let pht = f2.elf32_executable_file2_program_header_table in + let endian = get_elf32_header_endianness hdr in + let bs1 = f2.elf32_executable_file2_body in + let sentries = nat_of_elf32_half hdr.elf32_shnum in + let sentry_size = nat_of_elf32_half hdr.elf32_shentsize * 8 in + let ssize = sentries * sentry_size in + if ssize = 0 then + return <| elf32_executable_file3_header = hdr; + elf32_executable_file3_program_header_table = pht; + elf32_executable_file3_section_header_table = Nothing; + elf32_executable_file3_body = bs1 |> + else + let soffset = nat_of_elf32_off hdr.elf32_shoff * 8 in + let (_, scut) = partition soffset bs1 in + let (sexact, _) = partition ssize scut in + (* Bitstring irrelevant below as exact size used... *) + read_elf32_section_header_table ssize endian sexact >>= fun (sht, _) -> + return <| elf32_executable_file3_header = hdr; + elf32_executable_file3_program_header_table = pht; + elf32_executable_file3_section_header_table = Just sht; + elf32_executable_file3_body = bs1 |> + +(** [refine_elf64_executable_file2 f2] refines an elf64_executable_file2 [f2] into + * an elf64_executable_file3 by adding the optional section header table. + *) +val refine_elf64_executable_file2 : elf64_executable_file2 -> error elf64_executable_file3 +let refine_elf64_executable_file2 f2 = + let hdr = f2.elf64_executable_file2_header in + let pht = f2.elf64_executable_file2_program_header_table in + let endian = get_elf64_header_endianness hdr in + let bs1 = f2.elf64_executable_file2_body in + let sentries = nat_of_elf64_half hdr.elf64_shnum in + let sentry_size = nat_of_elf64_half hdr.elf64_shentsize * 8 in + let ssize = sentries * sentry_size in + if ssize = 0 then + return <| elf64_executable_file3_header = hdr; + elf64_executable_file3_program_header_table = pht; + elf64_executable_file3_section_header_table = Nothing; + elf64_executable_file3_body = bs1 |> + else + let soffset = nat_of_elf64_off hdr.elf64_shoff * 8 in + let (_, scut) = partition soffset bs1 in + let (sexact, _) = partition ssize scut in + (* Bitstring irrelevant below as exact size used... *) + read_elf64_section_header_table ssize endian sexact >>= fun (sht, _) -> + return <| elf64_executable_file3_header = hdr; + elf64_executable_file3_program_header_table = pht; + elf64_executable_file3_section_header_table = Just sht; + elf64_executable_file3_body = bs1 |> + +(** [read_elf32_executable_file3 bs0] reads an elf32_executable_file3 from + * bitstring [bs0]. + *) +val read_elf32_executable_file3 : bitstring -> error elf32_executable_file3 +let read_elf32_executable_file3 bs0 = + read_elf32_executable_file2 bs0 >>= refine_elf32_executable_file2 + +(** [read_elf64_executable_file3 bs0] reads an elf64_executable_file3 from + * bitstring [bs0]. + *) +val read_elf64_executable_file3 : bitstring -> error elf64_executable_file3 +let read_elf64_executable_file3 bs0 = + read_elf64_executable_file2 bs0 >>= refine_elf64_executable_file2 + +(** string_of_elf32_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3] + * creates a string representation of [f3]. + *) +val string_of_elf32_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file3 -> string +let string_of_elf32_executable_file3 hdr_bdl pht_bdl sht_bdl f3 = + let sht = + match f3.elf32_executable_file3_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf32_section_header_table sht_bdl sht + end + in + unlines [ + "\n*Type elf32_executable_file3:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f3.elf32_executable_file3_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f3.elf32_executable_file3_program_header_table + ; "**Section header table:" + ; sht + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_executable_file3_body) + ] + +(** string_of_elf64_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3] + * creates a string representation of [f3]. + *) +val string_of_elf64_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file3 -> string +let string_of_elf64_executable_file3 hdr_bdl pht_bdl sht_bdl f3 = + let sht = + match f3.elf64_executable_file3_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf64_section_header_table sht_bdl sht + end + in + unlines [ + "\n*Type elf64_executable_file3:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f3.elf64_executable_file3_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f3.elf64_executable_file3_program_header_table + ; "**Section header table:" + ; sht + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_executable_file3_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_executable_file4.lem b/src/elf_model/elf_executable_file4.lem new file mode 100644 index 00000000..c6a6b345 --- /dev/null +++ b/src/elf_model/elf_executable_file4.lem @@ -0,0 +1,249 @@ +open import Maybe +open import Num + +open import Elf_executable_file3 +open import Elf_header +open import Elf_program_header_table +open import Elf_section_header_table +open import Elf_types +open import String_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +(** Type [elf32_executable_file4] represents the lazy unfolding of a 32-bit ELF + * file where the header, program header table and optional section header table + * have been filled in, along with the section header string table, with all + * other data being left uninterpreted. + *) +type elf32_executable_file4 = + <| elf32_executable_file4_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file4_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file4_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) + ; elf32_executable_file4_section_header_string_table : string_table + ; elf32_executable_file4_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf32ExecutableFile4 'a) + val get_elf32_executable_file4 : 'a -> elf32_executable_file4 +end + +instance (HasElf32ExecutableFile4 elf32_executable_file4) + let get_elf32_executable_file4 f4 = f4 +end + +instance (HasElf32ExecutableFile3 elf32_executable_file4) + let get_elf32_executable_file3 f4 = + <| elf32_executable_file3_header = f4.elf32_executable_file4_header; + elf32_executable_file3_program_header_table = f4.elf32_executable_file4_program_header_table; + elf32_executable_file3_section_header_table = f4.elf32_executable_file4_section_header_table; + elf32_executable_file3_body = f4.elf32_executable_file4_body |> +end + +instance (HasElf32Header elf32_executable_file4) + let get_elf32_header f4 = f4.elf32_executable_file4_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file4) + let get_elf32_program_header_table f4 = + Just (f4.elf32_executable_file4_program_header_table) +end + +instance (HasElf32SectionHeaderTable elf32_executable_file4) + let get_elf32_section_header_table f4 = + f4.elf32_executable_file4_section_header_table +end + +instance (HasElf32SectionHeaderStringTable elf32_executable_file4) + let get_elf32_section_header_string_table f4 = + f4.elf32_executable_file4_section_header_string_table +end + +(** Type [elf64_executable_file4] represents the lazy unfolding of a 64-bit ELF + * file where the header, program header table and optional section header table + * have been filled in, along with the section header string table, with all + * other data being left uninterpreted. + *) +type elf64_executable_file4 = + <| elf64_executable_file4_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file4_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file4_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) + ; elf64_executable_file4_section_header_string_table : string_table + ; elf64_executable_file4_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf64ExecutableFile4 'a) + val get_elf64_executable_file4 : 'a -> elf64_executable_file4 +end + +instance (HasElf64ExecutableFile4 elf64_executable_file4) + let get_elf64_executable_file4 f4 = f4 +end + +instance (HasElf64ExecutableFile3 elf64_executable_file4) + let get_elf64_executable_file3 f4 = + <| elf64_executable_file3_header = f4.elf64_executable_file4_header; + elf64_executable_file3_program_header_table = f4.elf64_executable_file4_program_header_table; + elf64_executable_file3_section_header_table = f4.elf64_executable_file4_section_header_table; + elf64_executable_file3_body = f4.elf64_executable_file4_body |> +end + +instance (HasElf64Header elf64_executable_file4) + let get_elf64_header f4 = f4.elf64_executable_file4_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file4) + let get_elf64_program_header_table f4 = + Just (f4.elf64_executable_file4_program_header_table) +end + +instance (HasElf64SectionHeaderTable elf64_executable_file4) + let get_elf64_section_header_table f4 = + f4.elf64_executable_file4_section_header_table +end + +instance (HasElf64SectionHeaderStringTable elf64_executable_file4) + let get_elf64_section_header_string_table f4 = + f4.elf64_executable_file4_section_header_string_table +end + +(** [refine_elf32_executable_file3 f3] refines an elf32_executable_file3 [f3], adding the + * section header string table, to obtain an elf32_executable_file4. May fail if + * the offset stored in the ELF header indicating where the string table is stored is + * invalid. + *) +val refine_elf32_executable_file3 : elf32_executable_file3 -> error elf32_executable_file4 +let refine_elf32_executable_file3 f3 = + let hdr = f3.elf32_executable_file3_header in + let pht = f3.elf32_executable_file3_program_header_table in + let sht = f3.elf32_executable_file3_section_header_table in + let bs0 = f3.elf32_executable_file3_body in + match sht with + | Nothing -> + return <| elf32_executable_file4_header = hdr; + elf32_executable_file4_program_header_table = pht; + elf32_executable_file4_section_header_table = Nothing; + elf32_executable_file4_section_header_string_table = String_table.empty; + elf32_executable_file4_body = bs0 |> + | Just sht -> + let idx = nat_of_elf32_half hdr.elf32_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> Fail "refine_elf32_executable_file3: invalid offset into section header table" + | Just sect -> + let offset = nat_of_elf32_off sect.elf32_sh_offset * 8 in + let size = nat_of_elf32_word sect.elf32_sh_size * 8 in + let (_, cut) = Bitstring.partition offset bs0 in + let (rel, _) = Bitstring.partition size cut in + let strings = Bitstring.string_of_bitstring rel in + return <| elf32_executable_file4_header = hdr; + elf32_executable_file4_program_header_table = pht; + elf32_executable_file4_section_header_table = Just sht; + elf32_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf32_executable_file4_body = bs0 |> + end + end + +(** [refine_elf64_executable_file3 f3] refines an elf64_executable_file3 [f3], adding the + * section header string table, to obtain an elf64_executable_file4. May fail if + * the offset stored in the ELF header indicating where the string table is stored is + * invalid. + *) +val refine_elf64_executable_file3 : elf64_executable_file3 -> error elf64_executable_file4 +let refine_elf64_executable_file3 f3 = + let hdr = f3.elf64_executable_file3_header in + let pht = f3.elf64_executable_file3_program_header_table in + let sht = f3.elf64_executable_file3_section_header_table in + let bs0 = f3.elf64_executable_file3_body in + match sht with + | Nothing -> + return <| elf64_executable_file4_header = hdr; + elf64_executable_file4_program_header_table = pht; + elf64_executable_file4_section_header_table = Nothing; + elf64_executable_file4_section_header_string_table = String_table.empty; + elf64_executable_file4_body = bs0 |> + | Just sht -> + let idx = nat_of_elf64_half hdr.elf64_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> fail "refine_elf32_executable_file3: invalid offset into section header table" + | Just sect -> + let offset = nat_of_elf64_off sect.elf64_sh_offset * 8 in + let size = nat_of_elf64_xword sect.elf64_sh_size * 8 in + let (_, cut) = Bitstring.partition offset bs0 in + let (rel, _) = Bitstring.partition size cut in + let strings = Bitstring.string_of_bitstring rel in + return <| elf64_executable_file4_header = hdr; + elf64_executable_file4_program_header_table = pht; + elf64_executable_file4_section_header_table = Just sht; + elf64_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf64_executable_file4_body = bs0 |> + end + end + +(** [read_elf32_executable_file4 bs0] reads an [elf32_executable_file4] in from + * bitstring [bs0]. + *) +val read_elf32_executable_file4 : bitstring -> error elf32_executable_file4 +let read_elf32_executable_file4 bs0 = + read_elf32_executable_file3 bs0 >>= refine_elf32_executable_file3 + +(** [read_elf64_executable_file4 bs0] reads an [elf64_executable_file4] in from + * bitstring [bs0]. + *) +val read_elf64_executable_file4 : bitstring -> error elf64_executable_file4 +let read_elf64_executable_file4 bs0 = + read_elf64_executable_file3 bs0 >>= refine_elf64_executable_file3 + +(** [string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string + * based representation of elf32_executable_file4 [f4]. + *) +val string_of_elf32_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file4 -> string +let string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4 = + let sht = + match f4.elf32_executable_file4_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf32_section_header_table' sht_bdl f4.elf32_executable_file4_section_header_string_table sht + end + in + unlines [ + "\n*Type elf32_executable_file4" + ; "**Header" + ; string_of_elf32_header hdr_bdl f4.elf32_executable_file4_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f4.elf32_executable_file4_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf32_executable_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf32_executable_file4_body) + ] + +(** [string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string + * based representation of elf64_executable_file4 [f4]. + *) +val string_of_elf64_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file4 -> string +let string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4 = + let sht = + match f4.elf64_executable_file4_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf64_section_header_table' sht_bdl f4.elf64_executable_file4_section_header_string_table sht + end + in + unlines [ + "\n*Type elf64_executable_file4" + ; "**Header" + ; string_of_elf64_header hdr_bdl f4.elf64_executable_file4_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f4.elf64_executable_file4_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf64_executable_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf64_executable_file4_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_executable_file5.lem b/src/elf_model/elf_executable_file5.lem new file mode 100644 index 00000000..164cccb6 --- /dev/null +++ b/src/elf_model/elf_executable_file5.lem @@ -0,0 +1,339 @@ +open import Basic_classes +open import List +open import Maybe +open import Num +open import Tuple + +open import Elf_executable_file4 +open import Elf_header +open import Elf_interpreted_segment +open import Elf_program_header_table +open import Elf_section_header_table +open import Elf_types +open import String_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +(** Type [elf32_executable_file5] is an elf32_executable_file4 type where segments + * have been read from the program header table and interpreted. A process + * image can be obtained from this type. + *) +type elf32_executable_file5 = + <| elf32_executable_file5_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file5_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file5_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) + ; elf32_executable_file5_section_header_string_table : string_table (** The section header string table *) + ; elf32_executable_file5_segments : list elf32_interpreted_segment (** The list of segments as described by the program header table *) + ; elf32_executable_file5_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf32ExecutableFile5 'a) + val get_elf32_executable_file5 : 'a -> elf32_executable_file5 +end + +instance (HasElf32ExecutableFile5 elf32_executable_file5) + let get_elf32_executable_file5 f5 = f5 +end + +instance (HasElf32ExecutableFile4 elf32_executable_file5) + let get_elf32_executable_file4 f5 = + <| elf32_executable_file4_header = f5.elf32_executable_file5_header; + elf32_executable_file4_program_header_table = f5.elf32_executable_file5_program_header_table; + elf32_executable_file4_section_header_table = f5.elf32_executable_file5_section_header_table; + elf32_executable_file4_section_header_string_table = f5.elf32_executable_file5_section_header_string_table; + elf32_executable_file4_body = f5.elf32_executable_file5_body |> +end + +instance (HasElf32Header elf32_executable_file5) + let get_elf32_header f5 = f5.elf32_executable_file5_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file5) + let get_elf32_program_header_table f5 = Just (f5.elf32_executable_file5_program_header_table) +end + +instance (HasElf32SectionHeaderTable elf32_executable_file5) + let get_elf32_section_header_table f5 = f5.elf32_executable_file5_section_header_table +end + +instance (HasElf32SectionHeaderStringTable elf32_executable_file5) + let get_elf32_section_header_string_table f5 = f5.elf32_executable_file5_section_header_string_table +end + +(** Type [elf64_executable_file5] is an elf64_executable_file4 type where segments + * have been read from the program header table and interpreted. A process + * image can be obtained from this type. + *) +type elf64_executable_file5 = + <| elf64_executable_file5_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file5_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file5_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) + ; elf64_executable_file5_section_header_string_table : string_table (** The section header string table *) + ; elf64_executable_file5_segments : list elf64_interpreted_segment (** The list of segments as described by the program header table *) + ; elf64_executable_file5_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf64ExecutableFile5 'a) + val get_elf64_executable_file5 : 'a -> elf64_executable_file5 +end + +instance (HasElf64ExecutableFile5 elf64_executable_file5) + let get_elf64_executable_file5 f5 = f5 +end + +instance (HasElf64ExecutableFile4 elf64_executable_file5) + let get_elf64_executable_file4 f5 = + <| elf64_executable_file4_header = f5.elf64_executable_file5_header; + elf64_executable_file4_program_header_table = f5.elf64_executable_file5_program_header_table; + elf64_executable_file4_section_header_table = f5.elf64_executable_file5_section_header_table; + elf64_executable_file4_section_header_string_table = f5.elf64_executable_file5_section_header_string_table; + elf64_executable_file4_body = f5.elf64_executable_file5_body |> +end + +instance (HasElf64Header elf64_executable_file5) + let get_elf64_header f5 = f5.elf64_executable_file5_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file5) + let get_elf64_program_header_table f5 = Just (f5.elf64_executable_file5_program_header_table) +end + +instance (HasElf64SectionHeaderTable elf64_executable_file5) + let get_elf64_section_header_table f5 = f5.elf64_executable_file5_section_header_table +end + +instance (HasElf64SectionHeaderStringTable elf64_executable_file5) + let get_elf64_section_header_string_table f5 = f5.elf64_executable_file5_section_header_string_table +end + +(** [refine_elf32_executable_file4 f4] refines an elf32_executable_file4 [f4] into + * an elf32_executable_file5 by adding the interpreted segment field. Fails + * if an interpreted segment has a memory size smaller than its associated + * file size, an invalidation of the ELF spec. + *) +val refine_elf32_executable_file4 : elf32_executable_file4 -> error elf32_executable_file5 +let refine_elf32_executable_file4 f4 = + let pht = f4.elf32_executable_file4_program_header_table in + let bdy = f4.elf32_executable_file4_body in + let segs = + List.map (fun ph -> + let offset = nat_of_elf32_off ph.elf32_p_offset * 8 in + let size = nat_of_elf32_word ph.elf32_p_filesz * 8 in + let relevant = Bitstring.offset_and_cut offset size bdy in + let vaddr = nat_of_elf32_addr ph.elf32_p_vaddr in + let memsz = nat_of_elf32_word ph.elf32_p_memsz * 8 in + let typ = nat_of_elf32_word ph.elf32_p_type in + let flags = elf32_interpret_program_header_flags ph.elf32_p_flags in + <| elf32_segment_body = relevant; + elf32_segment_type = typ; + elf32_segment_size = size; + elf32_segment_memsz = memsz; + elf32_segment_base = vaddr; + elf32_segment_flags = flags |> + ) pht + in + let segs = + mapM (fun sg -> + if sg.elf32_segment_memsz < sg.elf32_segment_size then + Fail "refine_elf32_executable_file4: memory size of segment cannot be less than file size" + else + return sg) segs + in + segs >>= fun segs -> + return <| + elf32_executable_file5_header = f4.elf32_executable_file4_header; + elf32_executable_file5_program_header_table = f4.elf32_executable_file4_program_header_table; + elf32_executable_file5_section_header_table = f4.elf32_executable_file4_section_header_table; + elf32_executable_file5_section_header_string_table = f4.elf32_executable_file4_section_header_string_table; + elf32_executable_file5_segments = segs; + elf32_executable_file5_body = f4.elf32_executable_file4_body |> + +(** [refine_elf64_executable_file4 f4] refines an elf64_executable_file4 [f4] into + * an elf64_executable_file5 by adding the interpreted segment field. Fails + * if an interpreted segment has a memory size smaller than its associated + * file size, an invalidation of the ELF spec. + *) +val refine_elf64_executable_file4 : elf64_executable_file4 -> error elf64_executable_file5 +let refine_elf64_executable_file4 f4 = + let pht = f4.elf64_executable_file4_program_header_table in + let bdy = f4.elf64_executable_file4_body in + let segs = + List.map (fun ph -> + let offset = nat_of_elf64_off ph.elf64_p_offset * 8 in + let size = nat_of_elf64_xword ph.elf64_p_filesz * 8 in + let relevant = Bitstring.offset_and_cut offset size bdy in + let vaddr = nat_of_elf64_addr ph.elf64_p_vaddr in + let memsz = nat_of_elf64_xword ph.elf64_p_memsz * 8 in + let typ = nat_of_elf64_word ph.elf64_p_type in + let flags = elf64_interpret_program_header_flags ph.elf64_p_flags in + <| elf64_segment_body = relevant; + elf64_segment_type = typ; + elf64_segment_size = size; + elf64_segment_memsz = memsz; + elf64_segment_base = vaddr; + elf64_segment_flags = flags |> + ) pht + in + let segs = + mapM (fun sg -> + if sg.elf64_segment_memsz < sg.elf64_segment_size then + fail "refine_elf64_executable_file4: memory size of segment cannot be less than file size" + else + return sg) segs + in + segs >>= fun segs -> + return <| + elf64_executable_file5_header = f4.elf64_executable_file4_header; + elf64_executable_file5_program_header_table = f4.elf64_executable_file4_program_header_table; + elf64_executable_file5_section_header_table = f4.elf64_executable_file4_section_header_table; + elf64_executable_file5_section_header_string_table = f4.elf64_executable_file4_section_header_string_table; + elf64_executable_file5_segments = segs; + elf64_executable_file5_body = f4.elf64_executable_file4_body |> + +(** [read_elf32_executable_file5 bs0] reads an elf32_executable_file5 from bitstring + * [bs0]. + *) +val read_elf32_executable_file5 : bitstring -> error elf32_executable_file5 +let read_elf32_executable_file5 bs0 = + read_elf32_executable_file4 bs0 >>= refine_elf32_executable_file4 + +(** [read_elf64_executable_file5 bs0] reads an elf64_executable_file5 from bitstring + * [bs0]. + *) +val read_elf64_executable_file5 : bitstring -> error elf64_executable_file5 +let read_elf64_executable_file5 bs0 = + read_elf64_executable_file4 bs0 >>= refine_elf64_executable_file4 + +(** [elf32_construct_image f5] constructs a memory image from an elf32_executable5 object + * [f5]. The function returns the following: + * * A list of bytes with a corresponding address where they should be located + * in the program image and, + * * The entry point for the process. All addresses in the aforementioned list + * should be interpreted wrt this address. + * [construct_image] fails if a loadable segment has a memory size smaller than + * its associated file size, an error according to the ELF spec. This should + * never happen as relevant checks are made when refining an elf_executable_file4 + * into an elf_executable_file5. The function may also fail if there are no loadable + * segments in this executable file, again an error. + * By the ELF specification, you may assume that the list of bitstring, elf32_addr + * pairs is sorted ascending on the second component, i.e. that all pairs are in + * order of the address at which point they should be loaded in memory. + *) +val elf32_construct_image : elf32_executable_file5 -> error (list (bitstring * nat) * nat) +let elf32_construct_image f5 = + let segs = f5.elf32_executable_file5_segments in + let entr = f5.elf32_executable_file5_header.elf32_entry in + match List.filter (fun sg -> sg.elf32_segment_type = elf_pt_load) segs with + | [] -> fail "elf32_construct_image: an executable ELF file must have at least one loadable segment" + | load -> + mapM (fun sg -> + if sg.elf32_segment_memsz = 0 then + return [] + else if sg.elf32_segment_memsz = sg.elf32_segment_size then + return [(sg.elf32_segment_body, sg.elf32_segment_base)] + else if sg.elf32_segment_size < sg.elf32_segment_memsz then + (* Cannot be negative due to check in constructing [f5]. *) + let diff = sg.elf32_segment_memsz - sg.elf32_segment_size in + let zeros = Bitstring.zeros diff in + let addr = sg.elf32_segment_base + sg.elf32_segment_size in + return [(sg.elf32_segment_body, sg.elf32_segment_base); (zeros, addr)] + else + fail "elf32_construct_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf32_addr entr) + end + +(** [elf64_construct_image f5] constructs a memory image from an elf64_executable5 object + * [f5]. The function returns the following: + * * A list of bytes with a corresponding address where they should be located + * in the program image and, + * * The entry point for the process. All addresses in the aforementioned list + * should be interpreted wrt this address. + * [construct_image] fails if a loadable segment has a memory size smaller than + * its associated file size, an error according to the ELF spec. This should + * never happen as relevant checks are made when refining an elf_executable_file4 + * into an elf_executable_file5. The function may also fail if there are no loadable + * segments in this executable file, again an error. + * By the ELF specification, you may assume that the list of bitstring, elf32_addr + * pairs is sorted ascending on the second component, i.e. that all pairs are in + * order of the address at which point they should be loaded in memory. + *) +val elf64_construct_image : elf64_executable_file5 -> error (list (bitstring * nat) * nat) +let elf64_construct_image f5 = + let segs = f5.elf64_executable_file5_segments in + let entr = f5.elf64_executable_file5_header.elf64_entry in + match List.filter (fun sg -> sg.elf64_segment_type = elf_pt_load) segs with + | [] -> fail "elf64_construct_image: an executable ELF file must have at least one loadable segment" + | load -> + mapM (fun sg -> + if sg.elf64_segment_memsz = 0 then + return [] + else if sg.elf64_segment_memsz = sg.elf64_segment_size then + return [(sg.elf64_segment_body, sg.elf64_segment_base)] + else if sg.elf64_segment_size < sg.elf64_segment_memsz then + (* Cannot be negative due to check in constructing [f5]. *) + let diff = sg.elf64_segment_memsz - sg.elf64_segment_size in + let zeros = Bitstring.zeros diff in + let addr = sg.elf64_segment_base + sg.elf64_segment_size in + return [(sg.elf64_segment_body, sg.elf64_segment_base); (zeros, addr)] + else + fail "elf64_construct_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf64_addr entr) + end + +(** [string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string + * representation of elf32_executable_file5 [f5] using user-supplied print bundles. + *) +val string_of_elf32_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file5 -> string +let string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5 = + let sht = + match f5.elf32_executable_file5_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf32_section_header_table' sht_bdl f5.elf32_executable_file5_section_header_string_table sht + end + in + unlines [ + "\n*Type elf32_executable_file5" + ; "**Header" + ; string_of_elf32_header hdr_bdl f5.elf32_executable_file5_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f5.elf32_executable_file5_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf32_executable_file5_section_header_string_table)) + ; "**Interpreted segments:" + ; unlines (List.map (fun x -> "\n" ^ string_of_elf32_interpreted_segment x) f5.elf32_executable_file5_segments) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf32_executable_file5_body) + ] + +(** [string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string + * representation of elf64_executable_file5 [f5] using user-supplied print bundles. + *) +val string_of_elf64_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file5 -> string +let string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5 = + let sht = + match f5.elf64_executable_file5_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf64_section_header_table' sht_bdl f5.elf64_executable_file5_section_header_string_table sht + end + in + unlines [ + "\n*Type elf64_executable_file5" + ; "**Header" + ; string_of_elf64_header hdr_bdl f5.elf64_executable_file5_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f5.elf64_executable_file5_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf64_executable_file5_section_header_string_table)) + ; "**Interpreted segments:" + ; unlines (List.map (fun x -> "\n" ^ string_of_elf64_interpreted_segment x) f5.elf64_executable_file5_segments) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf64_executable_file5_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_file1.lem b/src/elf_model/elf_file1.lem new file mode 100644 index 00000000..ff2bba61 --- /dev/null +++ b/src/elf_model/elf_file1.lem @@ -0,0 +1,118 @@ +open import Basic_classes +open import String + +open import Endianness + +open import Elf_header +open import Elf_types + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** Type [elf32_file1] represents the first lazy unfolding of the structure + * of an ELF file, wherein the ELF header is populated and all other data + * is left uninterpreted. + *) +type elf32_file1 = + <| elf32_file1_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_file1_body : bitstring (** Uninterpreted data *) + |> + +class (HasElf32File1 'a) + val get_elf32_file1 : 'a -> elf32_file1 +end + +instance (HasElf32File1 elf32_file1) + let get_elf32_file1 f1 = f1 +end + +instance (HasElf32Header elf32_file1) + let get_elf32_header file1 = file1.elf32_file1_header +end + +(** Type [elf64_file1] represents the first lazy unfolding of the structure + * of an ELF file, wherein the ELF header is populated and all other data + * is left uninterpreted. + *) +type elf64_file1 = + <| elf64_file1_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_file1_body : bitstring (** Uninterpreted data *) + |> + +class (HasElf64File1 'a) + val get_elf64_file1 : 'a -> elf64_file1 +end + +instance (HasElf64File1 elf64_file1) + let get_elf64_file1 f1 = f1 +end + +instance (HasElf64Header elf64_file1) + let get_elf64_header file1 = file1.elf64_file1_header +end + +val string_of_elf32_file1 : hdr_print_bundle -> elf32_file1 -> string +let string_of_elf32_file1 hdr_bdl f1 = + unlines [ + "\n*Type elf32_file1:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f1.elf32_file1_header + ; "Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf32_file1_body) + ] + +val string_of_elf64_file1 : hdr_print_bundle -> elf64_file1 -> string +let string_of_elf64_file1 hdr_bdl f1 = + unlines [ + "\n*Type elf64_file1:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f1.elf64_file1_header + ; "Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf64_file1_body) + ] + +(** [is_executable_efl32_file1] tests whether the ELF file is an executable + * file type. + *) +val is_executable_elf32_file1 : elf32_file1 -> bool +let is_executable_elf32_file1 f1 = + nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_exec + +(** [is_executable_efl64_file1] tests whether the ELF file is an executable + * file type. + *) +val is_executable_elf64_file1 : elf64_file1 -> bool +let is_executable_elf64_file1 f1 = + nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_exec + +(** [is_shared_object_elf32_file1] tests whether the ELF file is a shared object + * file type. + *) +val is_shared_object_elf32_file1 : elf32_file1 -> bool +let is_shared_object_elf32_file1 f1 = + nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_dyn + +(** [is_shared_object_elf64_file1] tests whether the ELF file is a shared object +* file type. +*) +val is_shared_object_elf64_file1 : elf64_file1 -> bool +let is_shared_object_elf64_file1 f1 = + nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_dyn + +(** [read_elf32_file1 bs] lazily unfolds [bs] revealing the ELF file's header, + * leaving all other data uninterpreted. + *) +val read_elf32_file1 : bitstring -> error elf32_file1 +let read_elf32_file1 bs0 = + read_elf32_header bs0 >>= fun (hdr, bs1) -> + return <| elf32_file1_header = hdr; elf32_file1_body = bs0 |> + +(** [read_elf64_file1 bs] lazily unfolds [bs] revealing the ELF file's header, + * leaving all other data uninterpreted. + *) +val read_elf64_file1 : bitstring -> error elf64_file1 +let read_elf64_file1 bs0 = + read_elf64_header bs0 >>= fun (hdr, bs1) -> + return <| elf64_file1_header = hdr; elf64_file1_body = bs0 |>
\ No newline at end of file diff --git a/src/elf_model/elf_header.lem b/src/elf_model/elf_header.lem new file mode 100644 index 00000000..35aa4a37 --- /dev/null +++ b/src/elf_model/elf_header.lem @@ -0,0 +1,820 @@ +open import Basic_classes +open import Bool +open import Function +open import List +open import Maybe +open import Num +open import String + +open import Endianness + +open import Elf_types + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** 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 = 0 +(** Relocatable file *) +let elf_ft_rel : nat = 1 +(** Executable file *) +let elf_ft_exec : nat = 2 +(** Shared object file *) +let elf_ft_dyn : nat = 3 +(** Core file *) +let elf_ft_core : nat = 4 +(** Operating-system specific *) +let elf_ft_lo_os : nat = 65024 (* 0xfe00 *) +(** Operating-system specific *) +let elf_ft_hi_os : nat = 65279 (* 0xfeff *) +(** Processor specific *) +let elf_ft_lo_proc : nat = 65280 (* 0xff00 *) +(** Processor specific *) +let elf_ft_hi_proc : nat = 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 : (nat -> string) -> (nat -> string) -> nat -> string +let string_of_elf_file_type os_specific proc_specific m = + if m = elf_ft_none then + "No file type" + else if m = elf_ft_rel then + "Relocatable file type" + else if m = elf_ft_exec then + "Executable file type" + else if m = elf_ft_dyn then + "Shared object file type" + else if m = elf_ft_core then + "Core file type" + else if m >= elf_ft_lo_os && m <= elf_ft_hi_os then + os_specific m + else if m >= elf_ft_lo_proc && 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 : nat -> bool +let is_operating_system_specific_object_file_type_value v = + v >= 65024 && v <= 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 : nat -> bool +let is_processor_specific_object_file_type_value v = + v >= 65280 && v <= 65535 + +(** ELF machine architectures (TODO: complete the conversion of the enumeration.) *) + +(** Intel 386 *) +let elf_ma_386 : nat = 3 +(** IBM PowerPC *) +let elf_ma_ppc : nat = 20 +(** IBM PowerPC 64 *) +let elf_ma_ppc64 : nat = 21 + +(** [string_of_elf_machine_architecture m] produces a string representation of + * the numeric encoding [m] of the ELF machine architecture. + *) +val string_of_elf_machine_architecture : nat -> string +let string_of_elf_machine_architecture m = + if m = elf_ma_386 then + "Intel 386 architecture" + else if m = elf_ma_ppc then + "IBM PowerPC" + else if m = elf_ma_ppc64 then + "IBM PowerPC 64" + else + "Other architecture" + +(* XXX: convert these into top-level definitions later... +(** [elf_machine_architecture] enumerates all the supported machine architectures + * in the System V ABI. + *) +type elf_machine_architecture + = ELF_MA_Norc (* Nanoradio optimised RISC *) + | ELF_MA_Cool (* iCelero CoolEngine *) + | ELF_MA_Coge (* Cognitive Smart Memory Processor *) + | ELF_MA_CDP (* Paneve CDP architecture family *) + | ELF_MA_KVARC (* KM211 KVARC processor *) + | ELF_MA_KMX8 (* KM211 KMX8 8-bit processor *) + | ELF_MA_KMX16 (* KM211 KMX16 16-bit processor *) + | ELF_MA_KMX32 (* KM211 KMX32 32-bit processor *) + | ELF_MA_KM32 (* KM211 KM32 32-bit processor *) + | ELF_MA_MCHP_PIC (* Microchip 8-bit PIC(r) family *) + | ELF_MA_XCORE (* XMOS xCORE processor family *) + | ELF_MA_BA2 (* Beyond BA2 CPU architecture *) + | ELF_MA_BA1 (* Beyond BA1 CPU architecture *) + | ELF_MA_5600EX (* Freescale 56800EX Digital Signal Controller (DSC) *) + | ELF_MA_78KOR (* 199 Renesas 78KOR family *) + | ELF_MA_VideoCore5 (* Broadcom VideoCore V processor *) + | ELF_MA_RL78 (* Renesas RL78 family *) + | ELF_MA_Open8 (* Open8 8-bit RISC soft processing core *) + | ELF_MA_ARC_Compact2 (* Synopsys ARCompact V2 *) + | ELF_MA_CoreA_2nd (* KIPO_KAIST Core-A 2nd generation processor family *) + | ELF_MA_CoreA_1st (* KIPO_KAIST Core-A 1st generation processor family *) + | ELF_MA_CloudShield (* CloudShield architecture family *) + | ELF_MA_SLE9X (* Infineon Technologies SLE9X core *) + | ELF_MA_L10M (* Intel L10M *) + | ELF_MA_K10M (* Intel K10M *) + | ELF_MA_AArch64 (* ARM 64-bit architecture (AARCH64) *) + | ELF_MA_AVR32 (* Atmel Corporation 32-bit microprocessor family *) + | ELF_MA_STM8 (* STMicroelectronics STM8 8-bit microcontroller *) + | ELF_MA_TILE64 (* Tilera TILE64 multicore architecture family *) + | ELF_MA_TILEPro (* Tilera TILEPro multicore architecture family *) + | ELF_MA_MicroBlaze (* Xilinix MicroBlaze 32-bit RISC soft processor core *) + | ELF_MA_CUDA (* NVIDIA CUDA architecture *) + | ELF_MA_TILEGx (* Tilera TILE-Gx multicore architecture family *) + | ELF_MA_Cypress (* Cypress M8C microprocessor *) + | ELF_MA_R32C (* Renesas R32C series microprocessors *) + | ELF_MA_TriMedia (* NXP Semiconductors TriMedia architecture family *) + | ELF_MA_QDSP6 (* QUALCOMM DSP6 processor *) + | ELF_MA_8051 (* Intel 8051 and variants *) + | ELF_MA_STXP7X (* STMicroelectronics STxP7x family of configurable and extensible RISC processors *) + | ELF_MA_NDS32 (* Andes Technology compact code size embedded RISC processor family *) + | ELF_MA_eCOG1X (* Cyan Technology eCOG1X family *) + | ELF_MA_MAXQ30 (* Dallas Semiconductor MAXQ30 Core Micro-controllers *) + | ELF_MA_XIMO16 (* New Japan Radio (NJR) 16-bit DSP Processor *) + | ELF_MA_MANIK (* M2000 Reconfigurable RISC Microprocessor *) + | ELF_MA_CrayNV2 (* Cray Inc. NV2 vector architecture *) + | ELF_MA_RX (* Renesas RX family *) + | ELF_MA_METAG (* Imagination Technologies META processor architecture *) + | ELF_MA_MCST_Elbrus (* MCST Elbrus general purpose hardware architecture *) + | ELF_MA_eCOG16 (* Cyan Technology eCOG16 family *) + | ELF_MA_CR16 (* National Semiconductor CompactRISC CR16 16-bit microprocessor *) + | ELF_MA_ETPU (* Freescale Extended Time Processing Unit *) + | ELF_MA_TSK3000 (* Altium TSK3000 core *) + | ELF_MA_RS08 (* Freescale RS08 embedded processor *) + | ELF_MA_SHARC (* Analog Devices SHARC family of 32-bit DSP processors *) + | ELF_MA_eCOG2 (* Cyan Technology eCOG2 microprocessor *) + | ELF_MA_Score7 (* Sunplus S+core7 RISC processor *) + | ELF_MA_DSP24 (* New Japan Radio (NJR) 24-bit DSP Processor *) + | ELF_MA_VideoCore3 (* Broadcom VideoCore III processor *) + | ELF_MA_LatticeMICO32 (* RISC processor for Lattice FPGA architecture *) + | ELF_MA_C17 (* Seiko Epson C17 family *) + | ELF_MA_C6000 (* The Texas Instruments TMS320C6000 DSP family *) + | ELF_MA_C2000 (* The Texas Instruments TMS320C2000 DSP family *) + | ELF_MA_C5500 (* The Texas Instruments TMS320C55x DSP family *) + | ELF_MA_MMDSP_PLUS (* STMicroelectronics 64bit VLIW Data Signal Processor *) + | ELF_MA_ZSP (* LSI Logic 16-bit DSP Processor *) + | ELF_MA_MMIX (* Donald Knuth's educational 64-bit processor *) + | ELF_MA_HUANY (* Harvard University machine-independent object files *) + | ELF_MA_Prism (* SiTera Prism *) + | ELF_MA_AVR (* Atmel AVR 8-bit microcontroller *) + | ELF_MA_FR30 (* Fujitsu FR30 *) + | ELF_MA_D10V (* Mitsubishi D10V *) + | ELF_MA_D30V (* Mitsubishi D30V *) + | ELF_MA_v850 (* NEC v850 *) + | ELF_MA_M32R (* Mitsubishi M32R *) + | ELF_MA_MN10300 (* Matsushita MN10300 *) + | ELF_MA_MN10200 (* Matsushita MN10200 *) + | ELF_MA_pJ (* picoJava *) + | ELF_MA_OpenRISC (* OpenRISC 32-bit embedded processor *) + | ELF_MA_ARC_Compact (* ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5) *) + | ELF_MA_Xtensa (* Tensilica Xtensa Architecture *) + | ELF_MA_VideoCore (* Alphamosaic VideoCore processor *) + | ELF_MA_TMM_GPP (* Thompson Multimedia General Purpose Processor *) + | ELF_MA_NS32K (* National Semiconductor 32000 series *) + | ELF_MA_TPC (* Tenor Network TPC processor *) + | ELF_MA_SNP1K (* Trebia SNP 1000 processor *) + | ELF_MA_ST200 (* STMicroelectronics ST200 microcontroller *) + | ELF_MA_IP2K (* Ubicom IP2xxx microcontroller family *) + | ELF_MA_MAX (* MAX Processor *) + | ELF_MA_CR (* National Semiconductor CompactRISC microprocessor *) + | ELF_MA_F2MC16 (* Fujitsu F2MC16 *) + | ELF_MA_MSP430 (* Texas Instruments embedded microcontroller msp430 *) + | ELF_MA_Blackfin (* Analog Devices Blackfin (DSP) processor *) + | ELF_MA_SE_C33 (* S1C33 Family of Seiko Epson processors *) + | ELF_MA_SEP (* Sharp embedded microprocessor *) + | ELF_MA_Arca (* Arca RISC Microprocessor *) + | ELF_MA_Unicore (* Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University *) + | ELF_MA_eXcess (* eXcess: 16/32/64-bit configurable embedded CPU *) + | ELF_MA_DXP (* Icera Semiconductor Inc. Deep Execution Processor *) + | ELF_MA_Altera_Nios2 (* Altera Nios II soft-core processor *) + | ELF_MA_CRX (* National Semiconductor CompactRISC CRX microprocessor *) + | ELF_MA_XGATE (* Motorola XGATE embedded processor *) + | ELF_MA_C166 (* Infineon C16x/XC16x processor *) + | ELF_MA_M16C (* Renesas M16C series microprocessors *) + | ELF_MA_dsPIC30F (* Microchip Technology dsPIC30F Digital Signal Controller *) + | ELF_MA_CE (* Freescale Communication Engine RISC core *) + | ELF_MA_M32C (* Renesas M32C series microprocessors *) + | ELF_MA_None (* No machine *) + | ELF_MA_M32 (* AT&T WE 32100 *) + | ELF_MA_SPARC (* SPARC *) + | ELF_MA_386 (* Intel 80386 *) + | ELF_MA_68K (* Motorola 68000 *) + | ELF_MA_88K (* Motorola 88000 *) + | ELF_MA_860 (* Intel 80860 *) + | ELF_MA_MIPS (* MIPS I Architecture *) + | ELF_MA_S370 (* IBM System/370 Processor *) + | ELF_MA_MIPS_RS3_LE (* MIPS RS3000 Little-endian *) + | ELF_MA_PARISC (* Hewlett-Packard PA-RISC *) + | ELF_MA_VPP500 (* Fujitsu VPP500 *) + | ELF_MA_SPARC32PLUS (* Enhanced instruction set SPARC *) + | ELF_MA_960 (* Intel 80960 *) + | ELF_MA_PPC (* PowerPC *) + | ELF_MA_PPC64 (* 64-bit PowerPC *) + | ELF_MA_S390 (* IBM System/390 Processor *) + | ELF_MA_SPU (* IBM SPU/SPC *) + | ELF_MA_V800 (* NEC V800 *) + | ELF_MA_FR20 (* Fujitsu FR20 *) + | ELF_MA_RH32 (* TRW RH-32 *) + | ELF_MA_RCE (* Motorola RCE *) + | ELF_MA_ARM (* ARM 32-bit architecture (AARCH32) *) + | ELF_MA_Alpha (* Digital Alpha *) + | ELF_MA_SH (* Hitachi SH *) + | ELF_MA_SPARCv9 (* SPARC Version 9 *) + | ELF_MA_TriCore (* Siemens TriCore embedded processor *) + | ELF_MA_ARC (* Argonaut RISC Core, Argonaut Technologies Inc. *) + | ELF_MA_H8_300 (* Hitachi H8/300 *) + | ELF_MA_H8_300H (* Hitachi H8/300H *) + | ELF_MA_H8S (* Hitachi H8S *) + | ELF_MA_H8_500 (* Hitachi H8/500 *) + | ELF_MA_IA_64 (* Intel IA-64 processor architecture *) + | ELF_MA_MIPS_X (* Stanford MIPS-X *) + | ELF_MA_ColdFire (* Motorola ColdFire *) + | ELF_MA_68HC12 (* Motorola M68HC12 *) + | ELF_MA_MMA (* Fujitsu MMA Multimedia Accelerator *) + | ELF_MA_PCP (* Siemens PCP *) + | ELF_MA_nCPU (* Sony nCPU embedded RISC processor *) + | ELF_MA_NDR1 (* Denso NDR1 microprocessor *) + | ELF_MA_StarCore (* Motorola Star*Core processor *) + | ELF_MA_ME16 (* Toyota ME16 processor *) + | ELF_MA_ST100 (* STMicroelectronics ST100 processor *) + | ELF_MA_TinyJ (* Advanced Logic Corp. TinyJ embedded processor family *) + | ELF_MA_X86_64 (* AMD x86-64 architecture *) + | ELF_MA_PDSP (* Sony DSP Processor *) + | ELF_MA_PDP10 (* Digital Equipment Corp. PDP-10 *) + | ELF_MA_PDP11 (* Digital Equipment Corp. PDP-11 *) + | ELF_MA_FX66 (* Siemens FX66 microcontroller *) + | ELF_MA_ST9Plus (* STMicroelectronics ST9+ 8/16 bit microcontroller *) + | ELF_MA_ST7 (* STMicroelectronics ST7 8-bit microcontroller *) + | ELF_MA_68HC16 (* Motorola MC68HC16 Microcontroller *) + | ELF_MA_68HC11 (* Motorola MC68HC11 Microcontroller *) + | ELF_MA_68HC08 (* Motorola MC68HC08 Microcontroller *) + | ELF_MA_68HC05 (* Motorola MC68HC05 Microcontroller *) + | ELF_MA_SVx (* Silicon Graphics SVx *) + | ELF_MA_ST19 (* STMicroelectronics ST19 8-bit microcontroller *) + | ELF_MA_VAX (* Digital VAX *) + | ELF_MA_CRIS (* Axis Communications 32-bit embedded processor *) + | ELF_MA_Javelin (* Infineon Technologies 32-bit embedded processor *) + | ELF_MA_Firepath (* Element 14 64-bit DSP Processor *) + | ELF_MA_Intel209 (* Reserved by Intel *) + | ELF_MA_Intel208 (* Reserved by Intel *) + | ELF_MA_Intel207 (* Reserved by Intel *) + | ELF_MA_Intel206 (* Reserved by Intel *) + | ELF_MA_Intel205 (* Reserved by Intel *) + | ELF_MA_Intel182 (* Reserved by Intel *) + | ELF_MA_ARM184 (* Reserved by ARM *) + | ELF_MA_Reserved6 (* Reserved for future use *) + | ELF_MA_Reserved11 (* Reserved for future use *) + | ELF_MA_Reserved12 (* Reserved for future use *) + | ELF_MA_Reserved13 (* Reserved for future use *) + | ELF_MA_Reserved14 (* Reserved for future use *) + | ELF_MA_Reserved16 (* Reserved for future use *) + | ELF_MA_Reserved24 (* Reserved for future use *) + | ELF_MA_Reserved25 (* Reserved for future use *) + | ELF_MA_Reserved26 (* Reserved for future use *) + | ELF_MA_Reserved27 (* Reserved for future use *) + | ELF_MA_Reserved28 (* Reserved for future use *) + | ELF_MA_Reserved29 (* Reserved for future use *) + | ELF_MA_Reserved30 (* Reserved for future use *) + | ELF_MA_Reserved31 (* Reserved for future use *) + | ELF_MA_Reserved32 (* Reserved for future use *) + | ELF_MA_Reserved33 (* Reserved for future use *) + | ELF_MA_Reserved34 (* Reserved for future use *) + | ELF_MA_Reserved35 (* Reserved for future use *) + | ELF_MA_Reserved121 (* Reserved for future use *) + | ELF_MA_Reserved122 (* Reserved for future use *) + | ELF_MA_Reserved123 (* Reserved for future use *) + | ELF_MA_Reserved124 (* Reserved for future use *) + | ELF_MA_Reserved125 (* Reserved for future use *) + | ELF_MA_Reserved126 (* Reserved for future use *) + | ELF_MA_Reserved127 (* Reserved for future use *) + | ELF_MA_Reserved128 (* Reserved for future use *) + | ELF_MA_Reserved129 (* Reserved for future use *) + | ELF_MA_Reserved130 (* Reserved for future use *) + | ELF_MA_Reserved143 (* Reserved for future use *) + | ELF_MA_Reserved144 (* Reserved for future use *) + | ELF_MA_Reserved145 (* Reserved for future use *) + | ELF_MA_Reserved146 (* Reserved for future use *) + | ELF_MA_Reserved147 (* Reserved for future use *) + | ELF_MA_Reserved148 (* Reserved for future use *) + | ELF_MA_Reserved149 (* Reserved for future use *) + | ELF_MA_Reserved150 (* Reserved for future use *) + | ELF_MA_Reserved151 (* Reserved for future use *) + | ELF_MA_Reserved152 (* Reserved for future use *) + | ELF_MA_Reserved153 (* Reserved for future use *) + | ELF_MA_Reserved154 (* Reserved for future use *) + | ELF_MA_Reserved155 (* Reserved for future use *) + | ELF_MA_Reserved156 (* Reserved for future use *) + | ELF_MA_Reserved157 (* Reserved for future use *) + | ELF_MA_Reserved158 (* Reserved for future use *) + | ELF_MA_Reserved159 (* Reserved for future use *) + | ELF_MA_ReservedExt of nat (* Reserved for future use *) +*) + +(** 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 = 0 +(** Current version *) +let elf_ev_current : nat = 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 : nat -> string +let string_of_elf_version_number m = + if m = elf_ev_none then + "Invalid ELF version" + else if m = elf_ev_current then + "Current ELF version" + 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) = n > 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 = 0 +(** File identification *) +let elf_ii_mag1 : nat = 1 +(** File identification *) +let elf_ii_mag2 : nat = 2 +(** File identification *) +let elf_ii_mag3 : nat = 3 +(** File class *) +let elf_ii_class : nat = 4 +(** Data encoding *) +let elf_ii_data : nat = 5 +(** File version *) +let elf_ii_version : nat = 6 +(** Operating system/ABI identification *) +let elf_ii_osabi : nat = 7 +(** ABI version *) +let elf_ii_abiversion : nat = 8 +(** Start of padding bytes *) +let elf_ii_pad : nat = 9 +(** Size of e*_ident[] *) +let elf_ii_nident : nat = 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 : nat = 127 +(** Position: e*_ident[elf_ii_mag1], 'E' format identifier *) +let elf_mn_mag1 : nat = 69 +(** Position: e*_ident[elf_ii_mag2], 'L' format identifier *) +let elf_mn_mag2 : nat = 76 +(** Position: e*_ident[elf_ii_mag3], 'F' format identifier *) +let elf_mn_mag3 : nat = 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 = 0 +(** 32 bit objects *) +let elf_class_32 : nat = 1 +(** 64 bit objects *) +let elf_class_64 : nat = 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 : nat -> string +let string_of_elf_file_class m = + if m = elf_class_none then + "Invalid ELF file class" + else if m = elf_class_32 then + "32 bit ELF object" + else if m = elf_class_64 then + "64 bit ELF object" + 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 = 0 +(** Two's complement values, least significant byte occupying lowest address *) +let elf_data_2lsb : nat = 1 +(** Two's complement values, most significant byte occupying lowest address *) +let elf_data_2msb : nat = 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 : nat -> string +let string_of_elf_data_encoding m = + if m = elf_data_none then + "Invalid data encoding" + else if m = elf_data_2lsb then + "Two's complement values, LSB at lowest address" + else if m = elf_data_2msb then + "Two's complement values, MSB at lowest address" + 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 = 0 +(** Hewlett-Packard HP-UX *) +let elf_osabi_hpux : nat = 1 +(** NetBSD *) +let elf_osabi_netbsd : nat = 2 +(** GNU *) +let elf_osabi_gnu : nat = 3 +(** Linux, historical alias for GNU *) +let elf_osabi_linux : nat = 3 +(** Sun Solaris *) +let elf_osabi_solaris : nat = 6 +(** AIX *) +let elf_osabi_aix : nat = 7 +(** IRIX *) +let elf_osabi_irix : nat = 8 +(** FreeBSD *) +let elf_osabi_freebsd : nat = 9 +(** Compaq Tru64 Unix *) +let elf_osabi_tru64 : nat = 10 +(** Novell Modesto *) +let elf_osabi_modesto : nat = 11 +(** OpenBSD *) +let elf_osabi_openbsd : nat = 12 +(** OpenVMS *) +let elf_osabi_openvms : nat = 13 +(** Hewlett-Packard Non-stop Kernel *) +let elf_osabi_nsk : nat = 14 +(** Amiga Research OS *) +let elf_osabi_aros : nat = 15 +(** FenixOS highly-scalable multi-core OS *) +let elf_osabi_fenixos : nat = 16 + +(** [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 : nat -> string +let string_of_elf_osabi_version m = + if m = elf_osabi_none then + "No extension or unspecified" + else if m = elf_osabi_netbsd then + "Hewlett-Packard HP-UX" + else if m = elf_osabi_netbsd then + "NetBSD" + else if m = elf_osabi_gnu then + "GNU" + else if m = elf_osabi_linux then + "Linux (GNU alias)" + else if m = elf_osabi_solaris then + "Sun Solaris" + else if m = elf_osabi_aix then + "AIX" + else if m = elf_osabi_irix then + "IRIX" + else if m = elf_osabi_freebsd then + "FreeBSD" + else if m = elf_osabi_tru64 then + "Compaq Tru64 Unix" + else if m = elf_osabi_modesto then + "Novell Modesto" + else if m = elf_osabi_openbsd then + "OpenBSD" + else if m = elf_osabi_openvms then + "OpenVMS" + else if m = elf_osabi_nsk then + "Hewlett-Packard Non-stop Kernel" + else if m = elf_osabi_aros then + "Amiga Research OS" + else if m = elf_osabi_fenixos then + "FenixOS highly-scalable multi-core OS" + else + "Invalid OSABI version" + +(** 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) = n >= 64 && n <= 255 + +(** ELF Header type *) + +(** [ei_nident] is the fixed length of the identification field in the + * [elf32_ehdr] type. + *) +val ei_nident : nat +let ei_nident = 16 + +(** [elf32_header] is the type of headers for 32-bit ELF files. + *) +type elf32_header = + <| elf32_ident : list unsigned_char (** Identification field *) + ; elf32_type : elf32_half (** The object file type *) + ; elf32_machine : elf32_half (** Required machine architecture *) + ; elf32_version : elf32_word (** Object file version *) + ; elf32_entry : elf32_addr (** Virtual address for transfer of control *) + ; elf32_phoff : elf32_off (** Program header table offset in bytes *) + ; elf32_shoff : elf32_off (** Section header table offset in bytes *) + ; elf32_flags : elf32_word (** Processor-specific flags *) + ; elf32_ehsize : elf32_half (** ELF header size in bytes *) + ; elf32_phentsize: elf32_half (** Program header table entry size in bytes *) + ; elf32_phnum : elf32_half (** Number of entries in program header table *) + ; elf32_shentsize: elf32_half (** Section header table entry size in bytes *) + ; elf32_shnum : elf32_half (** Number of entries in section header table *) + ; elf32_shstrndx : elf32_half (** Section header table entry for section name string table *) + |> + +class (HasElf32Header 'a) + val get_elf32_header : 'a -> elf32_header +end + +(** [elf64_header] is the type of headers for 32-bit ELF files. + *) +type elf64_header = + <| elf64_ident : list unsigned_char (** Identification field *) + ; elf64_type : elf64_half (** The object file type *) + ; elf64_machine : elf64_half (** Required machine architecture *) + ; elf64_version : elf64_word (** Object file version *) + ; elf64_entry : elf64_addr (** Virtual address for transfer of control *) + ; elf64_phoff : elf64_off (** Program header table offset in bytes *) + ; elf64_shoff : elf64_off (** Section header table offset in bytes *) + ; elf64_flags : elf64_word (** Processor-specific flags *) + ; elf64_ehsize : elf64_half (** ELF header size in bytes *) + ; elf64_phentsize: elf64_half (** Program header table entry size in bytes *) + ; elf64_phnum : elf64_half (** Number of entries in program header table *) + ; elf64_shentsize: elf64_half (** Section header table entry size in bytes *) + ; elf64_shnum : elf64_half (** Number of entries in section header table *) + ; elf64_shstrndx : elf64_half (** Section header table entry for section name string table *) + |> + +class (HasElf64Header 'a) + val get_elf64_header : 'a -> elf64_header +end + +(** [deduce_endian] deduces the endianness of an ELF file based on the ELF + * header's magic number. + *) +val deduce_endianness : list unsigned_char -> endianness +let deduce_endianness id = + match List.index id 5 with + | Nothing -> Little (* XXX: random default as read of magic number has failed! *) + | Just v -> + if nat_of_unsigned_char v = elf_data_2lsb then + Little + else if nat_of_unsigned_char v = elf_data_2msb then + Big + else + Little (* XXX: random default as value is not valid! *) + end + +val get_elf32_header_endianness : elf32_header -> endianness +let get_elf32_header_endianness hdr = + deduce_endianness (hdr.elf32_ident) + +val get_elf64_header_endianness : elf64_header -> endianness +let get_elf64_header_endianness hdr = + deduce_endianness (hdr.elf64_ident) + +(** 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 -> string) * (nat -> string) + +val string_of_elf32_header : hdr_print_bundle -> elf32_header -> string +let string_of_elf32_header (os, proc) hdr = + unlines [ + "\t" ^ "Magic number: " ^ show hdr.elf32_ident + ; "\t" ^ "Endianness: " ^ show (deduce_endianness hdr.elf32_ident) + ; "\t" ^ "Type: " ^ string_of_elf_file_type os proc (nat_of_elf32_half hdr.elf32_type) + ; "\t" ^ "Version: " ^ string_of_elf_version_number (nat_of_elf32_word hdr.elf32_version) + ; "\t" ^ "Machine: " ^ string_of_elf_machine_architecture (nat_of_elf32_half hdr.elf32_machine) + ; "\t" ^ "Entry point: " ^ show hdr.elf32_entry + ; "\t" ^ "Flags: " ^ show hdr.elf32_flags + ; "\t" ^ "Entries in program header table: " ^ show hdr.elf32_phnum + ; "\t" ^ "Entries in section header table: " ^ show hdr.elf32_shnum + ] + +val string_of_elf64_header : hdr_print_bundle -> elf64_header -> string +let string_of_elf64_header (os, proc) hdr = + unlines [ + "\t" ^ "Magic number: " ^ show hdr.elf64_ident + ; "\t" ^ "Endianness: " ^ show (deduce_endianness hdr.elf64_ident) + ; "\t" ^ "Type: " ^ string_of_elf_file_type os proc (nat_of_elf64_half hdr.elf64_type) + ; "\t" ^ "Version: " ^ string_of_elf_version_number (nat_of_elf64_word hdr.elf64_version) + ; "\t" ^ "Machine: " ^ string_of_elf_machine_architecture (nat_of_elf64_half hdr.elf64_machine) + ; "\t" ^ "Entry point: " ^ show hdr.elf64_entry + ; "\t" ^ "Flags: " ^ show hdr.elf64_flags + ; "\t" ^ "Entries in program header table: " ^ show hdr.elf64_phnum + ; "\t" ^ "Entries in section header table: " ^ show hdr.elf64_shnum + ] + +val string_of_elf32_header_default : elf32_header -> string +let string_of_elf32_header_default = + string_of_elf32_header + ((const "*Default OS specific print*"), + (const "*Default processor specific print*")) + +val string_of_elf64_header_default : elf64_header -> string +let string_of_elf64_header_default = + string_of_elf64_header + ((const "*Default OS specific print*"), + (const "*Default processor specific print*")) + +instance (Show elf32_header) + let show = string_of_elf32_header_default +end + +instance (Show elf64_header) + let show = string_of_elf64_header_default +end + +val read_elf32_header : bitstring -> error (elf32_header * bitstring) +let read_elf32_header bs = + repeatM' ei_nident bs (read_unsigned_char default_endianness) >>= fun (ident, bs) -> + 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 List.index ident 4 with + | Nothing -> fail "read_elf32_header: transcription of ELF identifier failed" + | Just c -> + if nat_of_unsigned_char 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" + end + +val read_elf64_header : bitstring -> error (elf64_header * bitstring) +let read_elf64_header bs = + repeatM' ei_nident bs (read_unsigned_char default_endianness) >>= fun (ident, bs) -> + 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 List.index ident 4 with + | Nothing -> fail "read_elf64_header: transcription of ELF identifier failed" + | Just c -> + if nat_of_unsigned_char 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" + end + +val is_elf32_header_padding_correct : elf32_header -> bool +let is_elf32_header_padding_correct ehdr = + List.index ehdr.elf32_ident 9 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 10 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 11 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 12 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 13 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 14 = Just (unsigned_char_of_nat 0) && + List.index ehdr.elf32_ident 15 = Just (unsigned_char_of_nat 0) + +val is_elf32_header_magic_number_correct : elf32_header -> bool +let is_elf32_header_magic_number_correct ehdr = + List.index ehdr.elf32_ident 0 = Just (unsigned_char_of_nat 127) && + List.index ehdr.elf32_ident 1 = Just (unsigned_char_of_nat 69) && + List.index ehdr.elf32_ident 2 = Just (unsigned_char_of_nat 76) && + List.index ehdr.elf32_ident 3 = Just (unsigned_char_of_nat 70) + +val is_elf32_header_class_correct : elf32_header -> bool +let is_elf32_header_class_correct ehdr = + List.index ehdr.elf32_ident 4 = Just (unsigned_char_of_nat 1) + +val is_elf32_header_version_correct : elf32_header -> bool +let is_elf32_header_version_correct ehdr = + List.index ehdr.elf32_ident 6 = Just (unsigned_char_of_nat 1) + +(** [is_valid_elf32_header] 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 = + List.length ehdr.elf32_ident = ei_nident && + is_elf32_header_magic_number_correct ehdr && + 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 -> nat +let get_elf32_header_program_table_size ehdr = + let phentsize = nat_of_elf32_half ehdr.elf32_phentsize in + let phnum = nat_of_elf32_half ehdr.elf32_phnum in + 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 -> nat +let get_elf64_header_program_table_size ehdr = + let phentsize = nat_of_elf64_half ehdr.elf64_phentsize in + let phnum = nat_of_elf64_half ehdr.elf64_phnum in + 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 = + not (nat_of_elf32_off ehdr.elf32_shoff = 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 = + not (nat_of_elf64_off ehdr.elf64_shoff = 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 -> nat +let get_elf32_header_section_table_size ehdr = + let shentsize = nat_of_elf32_half ehdr.elf32_shentsize in + let shnum = nat_of_elf32_half ehdr.elf32_shnum in + 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 -> nat +let get_elf64_header_section_table_size ehdr = + let shentsize = nat_of_elf64_half ehdr.elf64_shentsize in + let shnum = nat_of_elf64_half ehdr.elf64_shnum in + shentsize * shnum diff --git a/src/elf_model/elf_interpreted_segment.lem b/src/elf_model/elf_interpreted_segment.lem new file mode 100644 index 00000000..81ee74e2 --- /dev/null +++ b/src/elf_model/elf_interpreted_segment.lem @@ -0,0 +1,77 @@ +open import Basic_classes +open import Bool +open import Num +open import String + +open import Elf_types + +open import Bitstring +open import Missing_pervasives +open import Show + +type elf32_interpreted_segment = + <| elf32_segment_body : bitstring (** Body of the segment *) + ; elf32_segment_type : nat (** Type of the segment *) + ; elf32_segment_size : nat (** Size of the segment in bytes *) + ; elf32_segment_memsz : nat (** Size of the segment in memory in bytes *) + ; elf32_segment_base : nat (** Base address of the segment *) + ; elf32_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + |> + +type elf64_interpreted_segment = + <| elf64_segment_body : bitstring (** Body of the segment *) + ; elf64_segment_type : nat (** Type of the segment *) + ; elf64_segment_size : nat (** Size of the segment in bytes *) + ; elf64_segment_memsz : nat (** Size of the segment in memory in bytes *) + ; elf64_segment_base : nat (** Base address of the segment *) + ; elf64_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + |> + +val elf32_interpret_program_header_flags : elf32_word -> (bool * bool * bool) +let elf32_interpret_program_header_flags flags = + let zero = elf32_word_of_int32 0 in + let one = elf32_word_of_int32 1 in + let two = elf32_word_of_int32 2 in + let four = elf32_word_of_int32 4 in + (not (elf32_word_land flags one = zero), + not (elf32_word_land flags two = zero), + not (elf32_word_land flags four = zero)) + +val elf64_interpret_program_header_flags : elf64_word -> (bool * bool * bool) +let elf64_interpret_program_header_flags flags = + let zero = elf64_word_of_int32 0 in + let one = elf64_word_of_int32 1 in + let two = elf64_word_of_int32 2 in + let four = elf64_word_of_int32 4 in + (not (elf64_word_land flags one = zero), + not (elf64_word_land flags two = zero), + not (elf64_word_land flags four = zero)) + +val string_of_flags : (bool * bool * bool) -> string +let string_of_flags flags = + match flags with + | (read, write, execute) -> + bracket [show read; show write; show execute] + end + +val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string +let string_of_elf32_interpreted_segment seg = + unlines [ + "Body of length: " ^ show (Bitstring.length seg.elf32_segment_body) + ; "Segment type: " ^ show seg.elf32_segment_type + ; "Segment size: " ^ show seg.elf32_segment_size + ; "Segment memory size: " ^ show seg.elf32_segment_memsz + ; "Segment base address: " ^ show seg.elf32_segment_base + ; "Segment flags: " ^ string_of_flags seg.elf32_segment_flags + ] + +val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string +let string_of_elf64_interpreted_segment seg = + unlines [ + "Body of length: " ^ show (Bitstring.length seg.elf64_segment_body) + ; "Segment type: " ^ show seg.elf64_segment_type + ; "Segment size: " ^ show seg.elf64_segment_size + ; "Segment memory size: " ^ show seg.elf64_segment_memsz + ; "Segment base address: " ^ show seg.elf64_segment_base + ; "Segment flags: " ^ string_of_flags seg.elf64_segment_flags + ] diff --git a/src/elf_model/elf_linking_file2.lem b/src/elf_model/elf_linking_file2.lem new file mode 100644 index 00000000..df69b5c9 --- /dev/null +++ b/src/elf_model/elf_linking_file2.lem @@ -0,0 +1,13 @@ +open import Bitstring + +open import Elf_header +open import Elf_section_header_table + +open import Maybe + +type elf32_linking_file2 = + <| elf32_executable_file2_header : elf32_header + ; elf32_executable_file2_program_header_table : maybe elf32_program_header_table + ; elf32_executable_file2_body : bitstring + ; elf32_executable_file2_section_header_table : elf32_section_header_table + |>
\ No newline at end of file diff --git a/src/elf_model/elf_program_header_table.lem b/src/elf_model/elf_program_header_table.lem new file mode 100644 index 00000000..ad97d566 --- /dev/null +++ b/src/elf_model/elf_program_header_table.lem @@ -0,0 +1,306 @@ +open import Basic_classes +open import Bool +open import Function +open import List +open import Maybe +open import Num +open import String + +open import Elf_types +open import Endianness + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** Segment types + * + * FIXME: Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t] + * is really needed, hence chokes on huge constants below, which is why they are + * written in the way that they are. + *) + +(** Unused array element. All other members of the structure are undefined. *) +let elf_pt_null : nat = 0 +(** A loadable segment. *) +let elf_pt_load : nat = 1 +(** Dynamic linking information. *) +let elf_pt_dynamic : nat = 2 +(** Specifies the location and size of a null-terminated path name to be used to + * invoke an interpreter. + *) +let elf_pt_interp : nat = 3 +(** Specifies location and size of auxiliary information. *) +let elf_pt_note : nat = 4 +(** Reserved but with unspecified semantics. If the file contains a segment of + * this type then it is to be regarded as non-conformant with the ABI. + *) +let elf_pt_shlib : nat = 5 +(** Specifies the location and size of the program header table. *) +let elf_pt_phdr : nat = 6 +(** Specifies the thread local storage (TLS) template. Need not be supported. *) +let elf_pt_tls : nat = 7 +(** Start of reserved indices for operating system specific semantics. *) +let elf_pt_loos : nat = 128 * 128 * 128 * 256 * 3 (* 1610612736 (* 0x60000000 *) *) +(** End of reserved indices for operating system specific semantics. *) +let elf_pt_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *) +(** Start of reserved indices for processor specific semantics. *) +let elf_pt_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *) +(** End of reserved indices for processor specific semantics. *) +let elf_pt_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *) + +(** [string_of_elf_segment_type os proc st] produces a string representation of + * the coding of an ELF segment type [st] using [os] and [proc] to render OS- + * and processor-specific codings. + *) +val string_of_elf_segment_type : (nat -> string) -> (nat -> string) -> nat -> string +let string_of_elf_segment_type os proc pt = + if pt = elf_pt_null then + "PT_NULL" + else if pt = elf_pt_load then + "PT_LOAD" + else if pt = elf_pt_dynamic then + "PT_DYNAMIC" + else if pt = elf_pt_interp then + "PT_INTERP" + else if pt = elf_pt_note then + "PT_NOTE" + else if pt = elf_pt_shlib then + "PT_SHLIB" + else if pt = elf_pt_phdr then + "PT_PHDR" + else if pt = elf_pt_tls then + "PT_TLS" + else if pt >= elf_pt_loos && pt <= elf_pt_hios then + os pt + else if pt >= elf_pt_loproc && pt <= elf_pt_hiproc then + proc pt + else + "Undefined or invalid segment type" + +(** Program header table entry type *) + +(** Type [elf32_program_header_table_entry] encodes a program header table entry + * for 32-bit platforms. Each entry describes a segment in an executable or + * shared object file. + *) +type elf32_program_header_table_entry = + <| elf32_p_type : elf32_word (** Type of the segment *) + ; elf32_p_offset : elf32_off (** Offset from beginning of file for segment *) + ; elf32_p_vaddr : elf32_addr (** Virtual address for segment in memory *) + ; elf32_p_paddr : elf32_addr (** Physical address for segment *) + ; elf32_p_filesz : elf32_word (** Size of segment in file, in bytes *) + ; elf32_p_memsz : elf32_word (** Size of segment in memory image, in bytes *) + ; elf32_p_flags : elf32_word (** Segment flags *) + ; elf32_p_align : elf32_word (** Segment alignment memory for memory and file *) + |> + +(** Type [elf64_program_header_table_entry] encodes a program header table entry + * for 64-bit platforms. Each entry describes a segment in an executable or + * shared object file. + *) +type elf64_program_header_table_entry = + <| elf64_p_type : elf64_word (** Type of the segment *) + ; elf64_p_flags : elf64_word (** Segment flags *) + ; elf64_p_offset : elf64_off (** Offset from beginning of file for segment *) + ; elf64_p_vaddr : elf64_addr (** Virtual address for segment in memory *) + ; elf64_p_paddr : elf64_addr (** Physical address for segment *) + ; elf64_p_filesz : elf64_xword (** Size of segment in file, in bytes *) + ; elf64_p_memsz : elf64_xword (** Size of segment in memory image, in bytes *) + ; elf64_p_align : elf64_xword (** Segment alignment memory for memory and file *) + |> + +(** [string_of_elf32_program_header_table_entry os proc et] produces a string + * representation of a 32-bit program header table entry using [os] and [proc] + * to render OS- and processor-specific entries. + *) +val string_of_elf32_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf32_program_header_table_entry -> string +let string_of_elf32_program_header_table_entry os proc entry = + unlines [ + "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf32_word entry.elf32_p_type) + ; "\t" ^ "Offset: " ^ show entry.elf32_p_offset + ; "\t" ^ "Virtual address: " ^ show entry.elf32_p_vaddr + ; "\t" ^ "Physical address: " ^ show entry.elf32_p_paddr + ; "\t" ^ "Segment size (bytes): " ^ show entry.elf32_p_filesz + ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf32_p_memsz + ; "\t" ^ "Flags: " ^ show entry.elf32_p_flags + ; "\t" ^ "Alignment: " ^ show entry.elf32_p_align + ] + +(** [string_of_elf64_program_header_table_entry os proc et] produces a string + * representation of a 64-bit program header table entry using [os] and [proc] + * to render OS- and processor-specific entries. + *) +val string_of_elf64_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf64_program_header_table_entry -> string +let string_of_elf64_program_header_table_entry os proc entry = + unlines [ + "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf64_word entry.elf64_p_type) + ; "\t" ^ "Offset: " ^ show entry.elf64_p_offset + ; "\t" ^ "Virtual address: " ^ show entry.elf64_p_vaddr + ; "\t" ^ "Physical address: " ^ show entry.elf64_p_paddr + ; "\t" ^ "Segment size (bytes): " ^ show entry.elf64_p_filesz + ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf64_p_memsz + ; "\t" ^ "Flags: " ^ show entry.elf64_p_flags + ; "\t" ^ "Alignment: " ^ show entry.elf64_p_align + ] + +(** [string_of_elf32_program_header_table_entry_default et] produces a string representation + * of table entry [et] where OS- and processor-specific entries are replaced with + * default strings. + *) +val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string +let string_of_elf32_program_header_table_entry_default = + string_of_elf32_program_header_table_entry + (const "*Default OS specific print*") + (const "*Default processor specific print*") + +(** [string_of_elf64_program_header_table_entry_default et] produces a string representation + * of table entry [et] where OS- and processor-specific entries are replaced with + * default strings. + *) +val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string +let string_of_elf64_program_header_table_entry_default = + string_of_elf64_program_header_table_entry + (const "*Default OS specific print*") + (const "*Default processor specific print*") + +instance (Show elf32_program_header_table_entry) + let show = string_of_elf32_program_header_table_entry_default +end + +instance (Show elf64_program_header_table_entry) + let show = string_of_elf64_program_header_table_entry_default +end + +(** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table + * entry from bitstring [bs0] assuming endianness [endian]. If [bs0] is larger + * than necessary, the excess is returned from the function, too. + *) +val read_elf32_program_header_table_entry : endianness -> bitstring -> error (elf32_program_header_table_entry * bitstring) +let read_elf32_program_header_table_entry endian bs = + read_elf32_word endian bs >>= fun (typ, bs) -> + read_elf32_off endian bs >>= fun (offset, bs) -> + read_elf32_addr endian bs >>= fun (vaddr, bs) -> + read_elf32_addr endian bs >>= fun (paddr, bs) -> + read_elf32_word endian bs >>= fun (filesz, bs) -> + read_elf32_word endian bs >>= fun (memsz, bs) -> + read_elf32_word endian bs >>= fun (flags, bs) -> + read_elf32_word endian bs >>= fun (align, bs) -> + return (<| elf32_p_type = typ; elf32_p_offset = offset; + elf32_p_vaddr = vaddr; elf32_p_paddr = paddr; + elf32_p_filesz = filesz; elf32_p_memsz = memsz; + elf32_p_flags = flags; elf32_p_align = align |>, bs) + +val read_elf64_program_header_table_entry : endianness -> bitstring -> error (elf64_program_header_table_entry * bitstring) +let read_elf64_program_header_table_entry endian bs = + read_elf64_word endian bs >>= fun (typ, bs) -> + read_elf64_word endian bs >>= fun (flags, bs) -> + read_elf64_off endian bs >>= fun (offset, bs) -> + read_elf64_addr endian bs >>= fun (vaddr, bs) -> + read_elf64_addr endian bs >>= fun (paddr, bs) -> + read_elf64_xword endian bs >>= fun (filesz, bs) -> + read_elf64_xword endian bs >>= fun (memsz, bs) -> + read_elf64_xword endian bs >>= fun (align, bs) -> + return (<| elf64_p_type = typ; elf64_p_offset = offset; + elf64_p_vaddr = vaddr; elf64_p_paddr = paddr; + elf64_p_filesz = filesz; elf64_p_memsz = memsz; + elf64_p_flags = flags; elf64_p_align = align |>, bs) + +(** Program header table type *) + +(** Type [elf32_program_header_table] represents a program header table for 32-bit + * ELF files. A program header table is an array (implemented as a list, here) + * of program header table entries. + *) +type elf32_program_header_table = + list elf32_program_header_table_entry + +class (HasElf32ProgramHeaderTable 'a) + val get_elf32_program_header_table : 'a -> maybe elf32_program_header_table +end + +(** Type [elf64_program_header_table] represents a program header table for 64-bit + * ELF files. A program header table is an array (implemented as a list, here) + * of program header table entries. + *) +type elf64_program_header_table = + list elf64_program_header_table_entry + +class (HasElf64ProgramHeaderTable 'a) + val get_elf64_program_header_table : 'a -> maybe elf64_program_header_table +end + +(** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from + * bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed + * to have exactly the correct size for the table. For internal use, only. Use + * [read_elf32_program_header_table] below instead. + *) +let rec read_elf32_program_header_table' endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf32_program_header_table_entry endian bs0 >>= fun (entry, bs1) -> + read_elf32_program_header_table' endian bs1 >>= fun tail -> + return (entry::tail) + +(** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from + * bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed + * to have exactly the correct size for the table. For internal use, only. Use + * [read_elf32_program_header_table] below instead. + *) +let rec read_elf64_program_header_table' endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf64_program_header_table_entry endian bs0 >>= fun (entry, bs1) -> + read_elf64_program_header_table' endian bs1 >>= fun tail -> + return (entry::tail) + +(** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header + * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size]. + * This [table_size] argument should be equal to the number of entries in the + * table multiplied by the fixed entry size. Bitstring [bs0] may be larger than + * necessary, in which case the excess is returned. + *) +val read_elf32_program_header_table : nat -> endianness -> bitstring -> error (elf32_program_header_table * bitstring) +let read_elf32_program_header_table table_size endian bs0 = + let (eat, rest) = partition table_size bs0 in + read_elf32_program_header_table' endian eat >>= fun table -> + return (table, rest) + +(** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header + * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size]. + * This [table_size] argument should be equal to the number of entries in the + * table multiplied by the fixed entry size. Bitstring [bs0] may be larger than + * necessary, in which case the excess is returned. + *) +val read_elf64_program_header_table : nat -> endianness -> bitstring -> error (elf64_program_header_table * bitstring) +let read_elf64_program_header_table table_size endian bs0 = + let (eat, rest) = partition table_size bs0 in + read_elf64_program_header_table' endian eat >>= fun table -> + return (table, rest) + +(** The [pht_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 pht_print_bundle = (nat -> string) * (nat -> string) + +(** [string_of_elf32_program_header_table os proc tbl] produces a string representation + * of program header table [tbl] using [os] and [proc] to render OS- and processor- + * specific entries. + *) +val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string +let string_of_elf32_program_header_table (os, proc) tbl = + unlines (List.map (string_of_elf32_program_header_table_entry os proc) tbl) + +(** [string_of_elf64_program_header_table os proc tbl] produces a string representation + * of program header table [tbl] using [os] and [proc] to render OS- and processor- + * specific entries. + *) +val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string +let string_of_elf64_program_header_table (os, proc) tbl = + unlines (List.map (string_of_elf64_program_header_table_entry os proc) tbl) diff --git a/src/elf_model/elf_section_header.ml b/src/elf_model/elf_section_header.ml new file mode 100644 index 00000000..1a73d35f --- /dev/null +++ b/src/elf_model/elf_section_header.ml @@ -0,0 +1,298 @@ +(*Generated by Lem from elf_section_header.lem.*) +open Lem_basic_classes +open Lem_bool +open Lem_list +open Lem_num +open Lem_string + +open Bitstring +open Error +open Elf_types +open Show + +(** Special section indices. *) + +(** [shn_undef]: marks an undefined, missing or irrelevant section reference. + *) +let shn_undef : int =( 0) +(** [shn_loreserve]: this specifies the lower bound of the range of reserved + * indices. + *) +let shn_loreserve : int =( 65280) (* 0xff00 *) +(** [shn_loproc]: start of the range reserved for processor-specific semantics. + *) +let shn_loproc : int =( 65280) (* 0xff00 *) +(** [shn_hiproc]: end of the range reserved for processor-specific semantics. + *) +let shn_hiproc : int =( 65311) (* 0xff1f *) +(** [shn_loos]: start of the range reserved for operating system-specific + * semantics. + *) +let shn_loos : int =( 65312) (* 0xff20 *) +(** [shn_hios]: end of the range reserved for operating system-specific + * semantics. + *) +let shn_hios : int =( 65343) (* 0xff3f *) +(** [shn_abs]: specifies the absolute values for the corresponding reference. + * Symbols defined relative to section number [shn_abs] have absolute values + * and are not affected by relocation. + *) +let shn_abs : int =( 65521) (* 0xfff1 *) +(** [shn_common]: symbols defined relative to this index are common symbols, + * such as unallocated C external variables. + *) +let shn_common : int =( 65522) (* 0xfff2 *) +(** [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). + *) +let shn_xindex : int =( 65535) (* 0xffff *) +(** [shn_hireserve]: specifies the upper-bound of reserved values. + *) +let shn_hireserve : int =( 65535) (* 0xffff *) + +(*val string_of_special_section_index : nat -> string*) +let string_of_special_section_index i = +(if i = shn_undef then + "SHN_UNDEF" + else if i = shn_loreserve then + "SHN_LORESERVE" + else if (i >= shn_loproc) && (i <= shn_hiproc) then + "SHN_PROCESSOR_SPECIFIC" + else if (i >= shn_loos) && (i <= shn_hios) then + "SHN_OS_SPECIFIC" + else if i = shn_abs then + "SHN_ABS" + else if i = shn_common then + "SHN_COMMON" + else if i = shn_xindex then + "SHN_XINDEX" + else if i = shn_hireserve then + "SHN_HIRESERVE" + else + "SHN UNDEFINED") + +(** Section types. *) + +(** Marks the section header as being inactive. *) +let sht_null : int =( 0) +(** Section holds information defined by the program. *) +let sht_progbits : int =( 1) +(** The following two section types hold a symbol table. An object file may only + * have one symbol table of each of the respective types. The symtab provides + * a place for link editing, whereas the dynsym section holds a minimal set of + * dynamic linking symbols + *) +let sht_symtab : int =( 2) +let sht_dynsym : int =( 11) +(** Section holds a string table *) +let sht_strtab : int =( 3) +(** Section holds relocation entries with explicit addends. An object file may + * have multiple section of this type. + *) +let sht_rela : int =( 4) +(** Section holds a symbol hash table. An object file may only have a single + * hash table. + *) +let sht_hash : int =( 5) +(** Section holds information for dynamic linking. An object file may only have + * a single dynamic section. + *) +let sht_dynamic : int =( 6) +(** Section holds information that marks the file in some way. *) +let sht_note : int =( 7) +(** Section occupies no space in the file but otherwise resembles a progbits + * section. + *) +let sht_nobits : int =( 8) +(** Section holds relocation entries without explicit addends. An object file + * may have multiple section of this type. + *) +let sht_rel : int =( 9) +(** Section type is reserved but has an unspecified meaning. *) +let sht_shlib : int =( 10) +(** Section contains an array of pointers to initialisation functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_init_array : int =( 14) +(** Section contains an array of pointers to termination functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_fini_array : int =( 15) +(** Section contains an array of pointers to initialisation functions that are + * invoked before all other initialisation functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_preinit_array : int =( 16) +(** Section defines a section group, i.e. a set of sections that are related and + * must be treated especially by the linker. May only appear in relocatable + * objects. + *) +let sht_group : int =( 17) +(** Section is associated with sections of type SHT_SYMTAB and is required if + * any of the section header indices referenced by that symbol table contains + * the escape value SHN_XINDEX. + *) +let sht_symtab_shndx : int =( 18) +(** XXX: broken for the time being due to Lem bug. *) +let sht_loos : int =( 0) +let sht_hios : int =( 0) +let sht_loproc : int =( 0) +let sht_hiproc : int =( 0) +let sht_louser : int =( 0) +let sht_hiuser : int =( 0) +(* XXX: constants too big for Lem to parse, apparently! +let sht_loos : nat = 1610612736 (* 0x60000000 *) +let sht_hios : nat = 1879048191 (* 0x6fffffff *) +let sht_loproc : nat = 1879048192 (* 0x70000000 *) +let sht_hiproc : nat = 2147483647 (* 0x7fffffff *) +let sht_louser : nat = 2147483648 (* 0x80000000 *) +let sht_hiuser : nat = 2415919103 (* 0x8fffffff *) +*) + +let string_of_section_type i = +(if i = sht_null then + "SHT_NULL" + else if i = sht_progbits then + "SHT_PROGBITS" + else if i = sht_symtab then + "SHT_SYMTAB" + else if i = sht_strtab then + "SHT_STRTAB" + else if i = sht_rela then + "SHT_RELA" + else if i = sht_hash then + "SHT_HASH" + else if i = sht_dynamic then + "SHT_DYNAMIC" + else if i = sht_note then + "SHT_NOTE" + else if i = sht_nobits then + "SHT_NOBITS" + else if i = sht_rel then + "SHT_REL" + else if i = sht_shlib then + "SHT_SHLIB" + else if i = sht_dynsym then + "SHT_DYNSYM" + else if i = sht_init_array then + "SHT_INIT_ARRAY" + else if i = sht_fini_array then + "SHT_FINI_ARRAY" + else if i = sht_preinit_array then + "SHT_PREINIT_ARRAY" + else if i = sht_group then + "SHT_GROUP" + else if i = sht_symtab_shndx then + "SHT_SYMTAB_SHNDX" + else if (i >= sht_loos) && (i <= sht_hios) then + "SHT_OS_SPECIFIC" + else if (i >= sht_loproc) && (i <= sht_hiproc) then + "SHT_PROCESSOR_SPECIFIC" + else if (i >= sht_louser) && (i <= sht_hiuser) then + "SHT_USER_SPECIFIC" + else + "SHT UNDEFINED") + +(** Section header table entry type. *) + +type elf32_section_header_table_entry = + { elf32_sh_name : Int64.t + ; elf32_sh_type : Int64.t + ; elf32_sh_flags : Int64.t + ; elf32_sh_addr : Int64.t + ; elf32_sh_offset : Int64.t + ; elf32_sh_size : Int64.t + ; elf32_sh_link : Int64.t + ; elf32_sh_info : Int64.t + ; elf32_sh_addralign : Int64.t + ; elf32_sh_entsize : Int64.t + } + +let read_elf32_section_header_table_entry (bs : Bitstring.bitstring) = +(Ml_bindings.read_elf32_word bs >>= (fun (sh_name, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_type, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_flags, bs) -> + Ml_bindings.read_elf32_addr bs >>= (fun (sh_addr, bs) -> + Ml_bindings.read_elf32_off bs >>= (fun (sh_offset, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_size, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_link, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_info, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_addralign, bs) -> + Ml_bindings.read_elf32_word bs >>= (fun (sh_entsize, bs) -> + return + { elf32_sh_name = sh_name + ; elf32_sh_type = sh_type + ; elf32_sh_flags = sh_flags + ; elf32_sh_addr = sh_addr + ; elf32_sh_offset = sh_offset + ; elf32_sh_size = sh_size + ; elf32_sh_link = sh_link + ; elf32_sh_info = sh_info + ; elf32_sh_addralign = sh_addralign + ; elf32_sh_entsize = sh_entsize + }))))))))))) + +let string_of_elf32_section_header_table_entry entry = +(List.fold_right (^) [ + "\t"; "Name: "; Int64.to_string entry.elf32_sh_name + ; "\t"; "Type: "; string_of_section_type (Int64.to_int entry.elf32_sh_type) + ; "\n\t"; "Flags: "; Int64.to_string entry.elf32_sh_flags + ; "\t"; "Address: "; Int64.to_string entry.elf32_sh_addr + ; "\t"; "Size: "; Int64.to_string entry.elf32_sh_size; "\n\n" + ] "") + +let instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict =({ + + show_method = string_of_elf32_section_header_table_entry}) + +(** Section header table type. *) + +type elf32_section_header_table = elf32_section_header_table_entry list +;; + +let rec read_elf32_section_header_table' entry_size bitstring0 = +(if Bitstring.bitstring_length bitstring0 = 0 then + return [] + else + let (eat, rest) = (Utility.partition_bitstring entry_size bitstring0) in + read_elf32_section_header_table_entry eat >>= (fun sect -> + read_elf32_section_header_table' entry_size rest >>= (fun tail -> + return (sect::tail)))) + +(*val read_elf32_section_header_table : nat -> nat -> nat -> bitstring -> error (elf32_section_header_table * bitstring)*) +let read_elf32_section_header_table size entry_size offset bitstring0 = +(let (prefix, relevant) = (Utility.partition_bitstring offset bitstring0) in + let (eat, rest) = (Utility.partition_bitstring (size * entry_size) relevant) in + read_elf32_section_header_table' entry_size eat >>= (fun entries -> + return (entries, rest))) +;; + +(*val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool*) +let elf32_size_correct hdr tbl = +((match Int64.to_int hdr.elf32_sh_size with + | 0 -> true + | m -> m = List.length tbl + )) +;; + +(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*) +let is_valid_elf32_section_header_table tbl = +((match tbl with + | [] -> false + | x::xs -> +(Int64.to_int x.elf32_sh_name = 0) && + ((Int64.to_int x.elf32_sh_type = sht_null) && + ((Int64.to_int x.elf32_sh_flags = 0) && + ((Int64.to_int x.elf32_sh_addr = 0) && + ((Int64.to_int x.elf32_sh_offset = 0) && + ((Int64.to_int x.elf32_sh_info = 0) && + ((Int64.to_int x.elf32_sh_addralign = 0) && + ((Int64.to_int x.elf32_sh_entsize = 0) && + elf32_size_correct x tbl))))))) + (* XXX: more correctness criteria in time *) + )) + +let string_of_elf32_section_header_table (tbl : elf32_section_header_table) : string = +("Section header table:" ^ ("\n" ^ + List.fold_right (^) (List.map string_of_elf32_section_header_table_entry tbl) "")) diff --git a/src/elf_model/elf_section_header_table.lem b/src/elf_model/elf_section_header_table.lem new file mode 100644 index 00000000..669a2dce --- /dev/null +++ b/src/elf_model/elf_section_header_table.lem @@ -0,0 +1,445 @@ +open import Basic_classes +open import Bool +open import Function +open import List +open import Maybe +open import Num +open import String + +open import Elf_types +open import Endianness +open import String_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +(** Special section indices. *) + +(** [shn_undef]: marks an undefined, missing or irrelevant section reference. + *) +let shn_undef : nat = 0 +(** [shn_loreserve]: this specifies the lower bound of the range of reserved + * indices. + *) +let shn_loreserve : nat = 65280 (* 0xff00 *) +(** [shn_loproc]: start of the range reserved for processor-specific semantics. + *) +let shn_loproc : nat = 65280 (* 0xff00 *) +(** [shn_hiproc]: end of the range reserved for processor-specific semantics. + *) +let shn_hiproc : nat = 65311 (* 0xff1f *) +(** [shn_loos]: start of the range reserved for operating system-specific + * semantics. + *) +let shn_loos : nat = 65312 (* 0xff20 *) +(** [shn_hios]: end of the range reserved for operating system-specific + * semantics. + *) +let shn_hios : nat = 65343 (* 0xff3f *) +(** [shn_abs]: specifies the absolute values for the corresponding reference. + * Symbols defined relative to section number [shn_abs] have absolute values + * and are not affected by relocation. + *) +let shn_abs : nat = 65521 (* 0xfff1 *) +(** [shn_common]: symbols defined relative to this index are common symbols, + * such as unallocated C external variables. + *) +let shn_common : nat = 65522 (* 0xfff2 *) +(** [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). + *) +let shn_xindex : nat = 65535 (* 0xffff *) +(** [shn_hireserve]: specifies the upper-bound of reserved values. + *) +let shn_hireserve : nat = 65535 (* 0xffff *) + +val string_of_special_section_index : nat -> string +let string_of_special_section_index i = + if i = shn_undef then + "SHN_UNDEF" + else if i = shn_loreserve then + "SHN_LORESERVE" + else if i >= shn_loproc && i <= shn_hiproc then + "SHN_PROCESSOR_SPECIFIC" + else if i >= shn_loos && i <= shn_hios then + "SHN_OS_SPECIFIC" + else if i = shn_abs then + "SHN_ABS" + else if i = shn_common then + "SHN_COMMON" + else if i = shn_xindex then + "SHN_XINDEX" + else if i = shn_hireserve then + "SHN_HIRESERVE" + else + "SHN UNDEFINED" + +(** Section types. *) + +(** Marks the section header as being inactive. *) +let sht_null : nat = 0 +(** Section holds information defined by the program. *) +let sht_progbits : nat = 1 +(** The following two section types hold a symbol table. An object file may only + * have one symbol table of each of the respective types. The symtab provides + * a place for link editing, whereas the dynsym section holds a minimal set of + * dynamic linking symbols + *) +let sht_symtab : nat = 2 +let sht_dynsym : nat = 11 +(** Section holds a string table *) +let sht_strtab : nat = 3 +(** Section holds relocation entries with explicit addends. An object file may + * have multiple section of this type. + *) +let sht_rela : nat = 4 +(** Section holds a symbol hash table. An object file may only have a single + * hash table. + *) +let sht_hash : nat = 5 +(** Section holds information for dynamic linking. An object file may only have + * a single dynamic section. + *) +let sht_dynamic : nat = 6 +(** Section holds information that marks the file in some way. *) +let sht_note : nat = 7 +(** Section occupies no space in the file but otherwise resembles a progbits + * section. + *) +let sht_nobits : nat = 8 +(** Section holds relocation entries without explicit addends. An object file + * may have multiple section of this type. + *) +let sht_rel : nat = 9 +(** Section type is reserved but has an unspecified meaning. *) +let sht_shlib : nat = 10 +(** Section contains an array of pointers to initialisation functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_init_array : nat = 14 +(** Section contains an array of pointers to termination functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_fini_array : nat = 15 +(** Section contains an array of pointers to initialisation functions that are + * invoked before all other initialisation functions. Each + * pointer is taken as a parameterless function with a void return type. + *) +let sht_preinit_array : nat = 16 +(** Section defines a section group, i.e. a set of sections that are related and + * must be treated especially by the linker. May only appear in relocatable + * objects. + *) +let sht_group : nat = 17 +(** Section is associated with sections of type SHT_SYMTAB and is required if + * any of the section header indices referenced by that symbol table contains + * the escape value SHN_XINDEX. + * + * FIXME: Lem bug as [int] type used throughout Lem codebase, rather than + * [BigInt.t], so Lem chokes on these large constants below, hence the weird + * way in which they are written. + *) +let sht_symtab_shndx : nat = 18 +let sht_loos : nat = 3 * 1024 * 1024 * 512 (* 1610612736 (* 0x60000000 *) *) +let sht_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *) +let sht_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *) +let sht_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *) +let sht_louser : nat = (536870912 * 4) (* 2147483648 (* 0x80000000 *) *) +let sht_hiuser : nat = (603979775 * 4) + 3 (* 2415919103 (* 0x8fffffff *) *) + +val string_of_section_type : (nat -> string) -> (nat -> string) -> + (nat -> string) -> nat -> string +let string_of_section_type os proc user i = + if i = sht_null then + "SHT_NULL" + else if i = sht_progbits then + "SHT_PROGBITS" + else if i = sht_symtab then + "SHT_SYMTAB" + else if i = sht_strtab then + "SHT_STRTAB" + else if i = sht_rela then + "SHT_RELA" + else if i = sht_hash then + "SHT_HASH" + else if i = sht_dynamic then + "SHT_DYNAMIC" + else if i = sht_note then + "SHT_NOTE" + else if i = sht_nobits then + "SHT_NOBITS" + else if i = sht_rel then + "SHT_REL" + else if i = sht_shlib then + "SHT_SHLIB" + else if i = sht_dynsym then + "SHT_DYNSYM" + else if i = sht_init_array then + "SHT_INIT_ARRAY" + else if i = sht_fini_array then + "SHT_FINI_ARRAY" + else if i = sht_preinit_array then + "SHT_PREINIT_ARRAY" + else if i = sht_group then + "SHT_GROUP" + else if i = sht_symtab_shndx then + "SHT_SYMTAB_SHNDX" + else if i >= sht_loos && i <= sht_hios then + os i + else if i >= sht_loproc && i <= sht_hiproc then + proc i + else if i >= sht_louser && i <= sht_hiuser then + user i + else + "Undefined or invalid section type" + +(** Section header table entry type. *) + +(** [elf32_section_header_table_entry] is the type of entries in the section + * header table in 32-bit ELF files. Each entry in the table details a section + * in the body of the ELF file. + *) +type elf32_section_header_table_entry = + <| elf32_sh_name : elf32_word (** Name of the section *) + ; elf32_sh_type : elf32_word (** Type of the section and its semantics *) + ; elf32_sh_flags : elf32_word (** Flags associated with the section *) + ; elf32_sh_addr : elf32_addr (** Address of first byte of section in memory image *) + ; elf32_sh_offset : elf32_off (** Offset from beginning of file of first byte of section *) + ; elf32_sh_size : elf32_word (** Section size in bytes *) + ; elf32_sh_link : elf32_word (** Section header table index link *) + ; elf32_sh_info : elf32_word (** Extra information, contents depends on type of section *) + ; elf32_sh_addralign : elf32_word (** Alignment constraints for section *) + ; elf32_sh_entsize : elf32_word (** Size of each entry in table, if section is one *) + |> + +(** [elf64_section_header_table_entry] is the type of entries in the section + * header table in 64-bit ELF files. Each entry in the table details a section + * in the body of the ELF file. + *) +type elf64_section_header_table_entry = + <| elf64_sh_name : elf64_word (** Name of the section *) + ; elf64_sh_type : elf64_word (** Type of the section and its semantics *) + ; elf64_sh_flags : elf64_xword (** Flags associated with the section *) + ; elf64_sh_addr : elf64_addr (** Address of first byte of section in memory image *) + ; elf64_sh_offset : elf64_off (** Offset from beginning of file of first byte of section *) + ; elf64_sh_size : elf64_xword (** Section size in bytes *) + ; elf64_sh_link : elf64_word (** Section header table index link *) + ; elf64_sh_info : elf64_word (** Extra information, contents depends on type of section *) + ; elf64_sh_addralign : elf64_xword (** Alignment constraints for section *) + ; elf64_sh_entsize : elf64_xword (** Size of each entry in table, if section is one *) + |> + +val read_elf32_section_header_table_entry : endianness -> bitstring -> error (elf32_section_header_table_entry * bitstring) +let read_elf32_section_header_table_entry endian bs = + read_elf32_word endian bs >>= fun (sh_name, bs) -> + read_elf32_word endian bs >>= fun (sh_type, bs) -> + read_elf32_word endian bs >>= fun (sh_flags, bs) -> + read_elf32_addr endian bs >>= fun (sh_addr, bs) -> + read_elf32_off endian bs >>= fun (sh_offset, bs) -> + read_elf32_word endian bs >>= fun (sh_size, bs) -> + read_elf32_word endian bs >>= fun (sh_link, bs) -> + read_elf32_word endian bs >>= fun (sh_info, bs) -> + read_elf32_word endian bs >>= fun (sh_addralign, bs) -> + read_elf32_word endian bs >>= fun (sh_entsize, bs) -> + return (<| elf32_sh_name = sh_name; elf32_sh_type = sh_type; + elf32_sh_flags = sh_flags; elf32_sh_addr = sh_addr; + elf32_sh_offset = sh_offset; elf32_sh_size = sh_size; + elf32_sh_link = sh_link; elf32_sh_info = sh_info; + elf32_sh_addralign = sh_addralign; elf32_sh_entsize = sh_entsize |>, bs) + + +val read_elf64_section_header_table_entry : endianness -> bitstring -> error (elf64_section_header_table_entry * bitstring) +let read_elf64_section_header_table_entry endian bs = + read_elf64_word endian bs >>= fun (sh_name, bs) -> + read_elf64_word endian bs >>= fun (sh_type, bs) -> + read_elf64_xword endian bs >>= fun (sh_flags, bs) -> + read_elf64_addr endian bs >>= fun (sh_addr, bs) -> + read_elf64_off endian bs >>= fun (sh_offset, bs) -> + read_elf64_xword endian bs >>= fun (sh_size, bs) -> + read_elf64_word endian bs >>= fun (sh_link, bs) -> + read_elf64_word endian bs >>= fun (sh_info, bs) -> + read_elf64_xword endian bs >>= fun (sh_addralign, bs) -> + read_elf64_xword endian bs >>= fun (sh_entsize, bs) -> + return (<| elf64_sh_name = sh_name; elf64_sh_type = sh_type; + elf64_sh_flags = sh_flags; elf64_sh_addr = sh_addr; + elf64_sh_offset = sh_offset; elf64_sh_size = sh_size; + elf64_sh_link = sh_link; elf64_sh_info = sh_info; + elf64_sh_addralign = sh_addralign; elf64_sh_entsize = sh_entsize |>, bs) + +(** The [sht_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 sht_print_bundle = (nat -> string) * (nat -> string) * (nat -> string) + +val string_of_elf32_section_header_table_entry : sht_print_bundle -> elf32_section_header_table_entry -> string +let string_of_elf32_section_header_table_entry (os, proc, user) entry = + unlines [ + "\t" ^ "Name: " ^ show entry.elf32_sh_name + ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type) + ; "\t" ^ "Flags: " ^ show entry.elf32_sh_flags + ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr + ; "\t" ^ "Size: " ^ show entry.elf32_sh_size + ] + +val string_of_elf64_section_header_table_entry : sht_print_bundle -> elf64_section_header_table_entry -> string +let string_of_elf64_section_header_table_entry (os, proc, user) entry = + unlines [ + "\t" ^ "Name: " ^ show entry.elf64_sh_name + ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type) + ; "\t" ^ "Flags: " ^ show entry.elf64_sh_flags + ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr + ; "\t" ^ "Size: " ^ show entry.elf64_sh_size + ] + +val string_of_elf32_section_header_table_entry' : sht_print_bundle -> string_table -> elf32_section_header_table_entry -> string +let string_of_elf32_section_header_table_entry' (os, proc, user) stbl entry = + let name = + match get_string_at (nat_of_elf32_word entry.elf32_sh_name) stbl with + | Fail _ -> "Invalid index into string table" + | Success i -> i + end + in + unlines [ + "\t" ^ "Name: " ^ name + ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type) + ; "\t" ^ "Flags: " ^ show entry.elf32_sh_flags + ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr + ; "\t" ^ "Size: " ^ show entry.elf32_sh_size + ] + +val string_of_elf64_section_header_table_entry' : sht_print_bundle -> string_table -> elf64_section_header_table_entry -> string +let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry = + let name = + match get_string_at (nat_of_elf64_word entry.elf64_sh_name) stbl with + | Fail _ -> "Invalid index into string table" + | Success i -> i + end + in + unlines [ + "\t" ^ "Name: " ^ name + ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type) + ; "\t" ^ "Flags: " ^ show entry.elf64_sh_flags + ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr + ; "\t" ^ "Size: " ^ show entry.elf64_sh_size + ] + +let string_of_elf32_section_header_table_entry_default = + string_of_elf32_section_header_table_entry + ((const "*Default OS specific print*"), + (const "*Default processor specific print*"), + (const "*Default user specific print*")) + +instance (Show elf32_section_header_table_entry) + let show = string_of_elf32_section_header_table_entry_default +end + +let string_of_elf64_section_header_table_entry_default = + string_of_elf64_section_header_table_entry + ((const "*Default OS specific print*"), + (const "*Default processor specific print*"), + (const "*Default user specific print*")) + +instance (Show elf64_section_header_table_entry) + let show = string_of_elf64_section_header_table_entry_default +end + +(** Section header table type. *) + +(** Type [elf32_section_header_table] represents a section header table for 32-bit + * ELF files. A section header table is an array (implemented as a list, here) + * of section header table entries. + *) +type elf32_section_header_table = + list elf32_section_header_table_entry + +class (HasElf32SectionHeaderTable 'a) + val get_elf32_section_header_table : 'a -> maybe elf32_section_header_table +end + +(** Type [elf64_section_header_table] represents a section header table for 64-bit + * ELF files. A section header table is an array (implemented as a list, here) + * of section header table entries. + *) +type elf64_section_header_table = + list elf64_section_header_table_entry + +class (HasElf64SectionHeaderTable 'a) + val get_elf64_section_header_table : 'a -> maybe elf64_section_header_table +end + +let rec read_elf32_section_header_table' endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf32_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> + read_elf32_section_header_table' endian bs1 >>= fun tail -> + return (entry::tail) + +val read_elf32_section_header_table : nat -> endianness -> bitstring -> error (elf32_section_header_table * bitstring) +let read_elf32_section_header_table table_size endian bs0 = + let (eat, rest) = partition table_size bs0 in + read_elf32_section_header_table' endian eat >>= fun entries -> + return (entries, rest) +;; + +let rec read_elf64_section_header_table' endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf64_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> + read_elf64_section_header_table' endian bs1 >>= fun tail -> + return (entry::tail) + +val read_elf64_section_header_table : nat -> endianness -> bitstring -> error (elf64_section_header_table * bitstring) +let read_elf64_section_header_table table_size endian bs0 = + let (eat, rest) = partition table_size bs0 in + read_elf64_section_header_table' endian eat >>= fun entries -> + return (entries, rest) +;; + +val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool +let elf32_size_correct hdr tbl = + match nat_of_elf32_word hdr.elf32_sh_size with + | 0 -> true + | m -> m = List.length tbl + end +;; + +val is_valid_elf32_section_header_table : elf32_section_header_table -> bool +let is_valid_elf32_section_header_table tbl = + match tbl with + | [] -> false + | x::xs -> + nat_of_elf32_word x.elf32_sh_name = 0 && + nat_of_elf32_word x.elf32_sh_type = sht_null && + nat_of_elf32_word x.elf32_sh_flags = 0 && + nat_of_elf32_addr x.elf32_sh_addr = 0 && + nat_of_elf32_off x.elf32_sh_offset = 0 && + nat_of_elf32_word x.elf32_sh_info = 0 && + nat_of_elf32_word x.elf32_sh_addralign = 0 && + nat_of_elf32_word x.elf32_sh_entsize = 0 && + elf32_size_correct x tbl + (* XXX: more correctness criteria in time *) + end + +val string_of_elf32_section_header_table : sht_print_bundle -> elf32_section_header_table -> string +let string_of_elf32_section_header_table sht_bdl tbl = + unlines (List.map (string_of_elf32_section_header_table_entry sht_bdl) tbl) + +val string_of_elf32_section_header_table' : sht_print_bundle -> string_table -> elf32_section_header_table -> string +let string_of_elf32_section_header_table' sht_bdl stbl tbl = + unlines (List.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl) + +val string_of_elf64_section_header_table : sht_print_bundle -> elf64_section_header_table -> string +let string_of_elf64_section_header_table sht_bdl tbl = + unlines (List.map (string_of_elf64_section_header_table_entry sht_bdl) tbl) + +val string_of_elf64_section_header_table' : sht_print_bundle -> string_table -> elf64_section_header_table -> string +let string_of_elf64_section_header_table' sht_bdl stbl tbl = + unlines (List.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl)
\ No newline at end of file diff --git a/src/elf_model/elf_string_table.ml b/src/elf_model/elf_string_table.ml new file mode 100644 index 00000000..0a211385 --- /dev/null +++ b/src/elf_model/elf_string_table.ml @@ -0,0 +1,75 @@ +(*Generated by Lem from elf_string_table.lem.*) +open Elf_header +open Elf_section_header +open Elf_types + +open Bitstring +open Error +open Missing_pervasives + +open Lem_basic_classes +open Lem_list +open Lem_maybe +open Lem_num +open Lem_string +open Show + +let get_strings_of_string_table bs = +(let strings = (Bitstring.string_of_bitstring bs) in + Ml_bindings.split_string_on_char strings '\000') + +let read_elf32_string_table hdr sections bs : ( string list) error = +((match sections with + | None -> return [] + | Some sections -> + let idx = (Int64.to_int hdr.elf32_shstrndx) in + let string_table = (Lem_list.list_index sections idx) in + (match string_table with + | None -> Fail "read_elf32_string_table: string table index too large" + | Some string_table -> + let offset = (Int64.to_int string_table.elf32_sh_offset) in + let size = (Int64.to_int string_table.elf32_sh_size) in + let (_, initial) = (Utility.partition_bitstring (offset * 8) bs) in + let (relevant, _) = (Utility.partition_bitstring (size * 8) initial) in + return (get_strings_of_string_table relevant) + ) + )) + +let rec read_elf32_string_tables' offset_sizes (bs : Bitstring.bitstring) : ( string list) list = +((match offset_sizes with + | [] -> [] + | x::xs -> + let (offset, size) = x in + let (_, relevant) = (Utility.partition_bitstring offset bs) in + let (cut, _) = (Utility.partition_bitstring size relevant) in + let strings = (get_strings_of_string_table cut) in + let tail = (read_elf32_string_tables' xs bs) in + strings::tail + )) + +let read_elf32_string_tables sections bs : ( string list) list = +((match sections with + | None -> [] + | Some sections -> + let offsets_sizes = (List.concat (List.map (fun sect -> + if Int64.to_int sect.elf32_sh_type = sht_strtab then + let offset = ((Int64.to_int sect.elf32_sh_offset) * 8) in + let size = +(let _ = (print_endline ("YYY size: " ^ natShow (Int64.to_int sect.elf32_sh_size * 8))) in + Int64.to_int sect.elf32_sh_size * 8) + in + [(offset, size)] + else + [] + ) sections)) + in + read_elf32_string_tables' offsets_sizes bs + )) + +let string_of_elf32_string_table tbl = +("String table contents:" ^ ("\n\t" ^ +(List.fold_right (^) tbl "" ^ "\n\n"))) + +let string_of_elf32_dynamic_string_table tbl = +("Dynamic string table contents:" ^ ("\n\t" ^ +(List.fold_right (^) tbl "" ^ "\n\n"))) diff --git a/src/elf_model/elf_symbol_table.ml b/src/elf_model/elf_symbol_table.ml new file mode 100644 index 00000000..a2fed159 --- /dev/null +++ b/src/elf_model/elf_symbol_table.ml @@ -0,0 +1,246 @@ +(*Generated by Lem from elf_symbol_table.lem.*) +open Lem_basic_classes +open Lem_bool +open Lem_list +open Lem_num +open Lem_string + +open Bitstring +open Elf_section_header +open Elf_types +open Error +open Show + +(** Symbol table indices *) + +(** Symbol table index is a subscript into the symbol table, which holds + * information needed to locate and relocate a program's symbolic definitions + * and references. Index 0 designates both the first entry in the table and + * serves as the undefined symbol index. [stn_undef] is a mnemonic for that + * undefined symbol. + *) +let stn_undef : int =( 0) + +(** Symbol bindings *) + +(** [elf32_st_bind] unpacks the binding information from the [st_info] field + * in the record type below. + *) +let elf32_st_bind i = +(Int64.to_int (Int64.shift_right i( 4))) +(** [elf64_st_bind] unpacks the binding information from the [st_info] field + * in the record type below. + *) +let elf64_st_bind i = +(Int64.to_int (Int64.shift_right i( 4))) +(** [elf32_st_type] unpacks the type information from the [e32_st_info] field + * in the record type below. + *) +let elf32_st_type i = +(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *) +(** [elf64_st_type] unpacks the type information from the [e64_st_info] field + * in the record type below. + *) +let elf64_st_type i = +(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *) +(** [elf32_st_info] unpacks other information from the [e32_st_info] field in the + * record type below. + *) +let elf32_st_info b t = +(let left = (Int64.shift_left b( 4)) in + let right = (Int64.logand t (Int64.of_int( 15))) in (* 0xf *) + let result = (Int64.add left right) in + Int64.to_int result) +(** [elf64_st_info] unpacks other information from the [e64_st_info] field in the + * record type below. + *) +let elf64_st_info b t = +(let left = (Int64.shift_left b( 4)) in + let right = (Int64.logand t (Int64.of_int( 15))) in (* 0xf *) + let result = (Int64.add left right) in + Int64.to_int result) +(** [stb_local]: local symbols are not visible outside the object file + * containing their definition. + *) +let stb_local : int =( 0) +(** [stb_global]: global symbols are visible to all object files being combined. + *) +let stb_global : int =( 1) +(** [stb_weak]: weak symbols resemble global symbols but their definitions have + * lower precedence. + *) +let stb_weak : int =( 2) +(** [stb_loos]: start of the range reserved for operating-system specific + * semantics. + *) +let stb_loos : int =( 10) +(** [stb_hios]: end of the range reserved for operating-system specific + * semantics. + *) +let stb_hios : int =( 12) +(** [stb_loproc]: start of the range reserved for processor specific semantics. + *) +let stb_loproc : int =( 13) +(** [stb_hiproc]: end of the range reserved for processor specific semantics. + *) +let stb_hiproc : int =( 15) + +(** Symbol types. *) + +(** [stt_notype]: the symbol's type is not specified. + *) +let stt_notype : int =( 0) +(** [stt_object]: the symbol is associated with a data object, such as a + * variable, an array, and so on. + *) +let stt_object : int =( 1) +(** [stt_func]: the symbol is associated with a function or other executable + * code. + *) +let stt_func : int =( 2) +(** [stt_section]: the symbol is associated with a section. + *) +let stt_section : int =( 3) +(** [stt_file]: the symbol's name gives the name of the source file associated + * with the object file. Must have [stb_local] binding and its section index + * must be [shn_abs]. It must also precede the other [stb_local] symbols for + * the file, is present. + *) +let stt_file : int =( 4) +(** [stt_common]: labels an unitialised common block. + *) +let stt_common : int =( 5) +(** [stt_tls]: specifies a thread local storage (TLS) entity. Gives the + * assigned offset of the symbol, not its address. TLS symbols may only be + * referenced by special TLS relocations and TLS relocations may only reference + * symbols with type [stt_tls]. + *) +let stt_tls : int =( 6) +(** [stt_loos]: start of the range reserved for operating-system specific + * semantics. + *) +let stt_loos : int =( 10) +(** [stt_hios]: end of the range reserved for operating-system specific + * semantics. + *) +let stt_hios : int =( 12) +(** [stt_loproc]: start of the range reserved for processor specific + * semantics. + *) +let stt_loproc : int =( 13) +(** [stt_hiproc]: end of the range reserved for processor specific semantics. + *) +let stt_hiproc : int =( 15) + +(** Symbol visibility. *) + +(** [elf32_st_visibility] unpacks visibility information from the [e32_st_other] + * field in the record type below. + *) +(*val elf32_st_visibility : unsigned_char -> nat*) +let elf32_st_visibility o = +(Int64.to_int (Int64.logand o (Int64.of_int( 3)))) (* 0x3 *) + +(** [stv_default]: symbol visibility is as specified by the symbol's binding + * type. Global and weak symbols are visible outside their defining component + * (executable or shared object file). Local symbols are hidden. Global and + * weak symbols are also pre-emptable: they may be pre-empted by definitions + * of the same name in another component. + *) +let stv_default : int =( 0) +(** [stv_internal]: meaning may be further defined by processor supplements to + * further constrain hidden symbols. An internal symbol in a relocatable file + * must be either removed or converted to [stb_local] when the relocatable + * object is included in an executable or shared object by the linker. + *) +let stv_internal : int =( 1) +(** [stv_hidden]: a symbol in the current component is hidden if its name is not + * visible to other components, necessarily protecting the symbol. A hidden + * object may still be referenced from another component if its address is + * passed outside. A hidden symbol in a relocatable object must be either + * removed or converted to [stb_local] when the relocatable file is included in + * an executable or shared object by the linker. + *) +let stv_hidden : int =( 2) +(** [stv_protected]: a protected symbol is visible in other components but is + * not pre-emptable, so that any reference to such a symbol from within the + * defining component must be resolved to the definition in that component. + * A symbol with [stb_local] binding must not have [stv_protected] visibility. + * If a symbol definition with [stv_protected] visibility from a shared object + * file is taken as resolving a reference from an executable or another shared + * object, the [shn_undef] symbol table entry created has [stv_default] + * visibility. + *) +let stv_protected : int =( 3) + +(** The symbol table entry type. *) + +type elf32_symbol_table_entry = + { elf32_st_name : Int64.t + ; elf32_st_value : Int64.t + ; elf32_st_size : Int64.t + ; elf32_st_info0 : Int64.t + ; elf32_st_other : Int64.t + ; elf32_st_shndx : Int64.t + } + +let string_of_elf32_symbol_table_entry entry = +(List.fold_right (^) [ + "\t"; "Name: "; Int64.to_string entry.elf32_st_name + ; "\t"; "Size: "; Int64.to_string entry.elf32_st_size + ; "\n\t"; "Value: "; Int64.to_string entry.elf32_st_value + ; "\t"; "Info: "; Int64.to_string entry.elf32_st_info0; "\n\n" + ] "") + +let read_elf32_symbol_table_entry bitstring6 : elf32_symbol_table_entry error = +(Ml_bindings.read_elf32_word bitstring6 >>= (fun (name, bitstring5) -> + Ml_bindings.read_elf32_addr bitstring5 >>= (fun (value, bitstring4) -> + Ml_bindings.read_elf32_word bitstring4 >>= (fun (size, bitstring3) -> + Ml_bindings.read_unsigned_char bitstring3 >>= (fun (info, bitstring2) -> + Ml_bindings.read_unsigned_char bitstring2 >>= (fun (other, bitstring1) -> + Ml_bindings.read_elf32_half bitstring1 >>= (fun (shndx, bitstring0) -> + let entry = ({ elf32_st_name = name; elf32_st_value = value; elf32_st_size = size; elf32_st_info0 = info; elf32_st_other = other; elf32_st_shndx = shndx }) in + return entry))))))) + +let rec read_elf32_symbol_table_entries bs : ( elf32_symbol_table_entry list) error = +(if Bitstring.bitstring_length bs = 0 then + return [] + else + let (cut, rest) = (Utility.partition_bitstring( 128) bs) in + read_elf32_symbol_table_entry cut >>= (fun head -> + read_elf32_symbol_table_entries rest >>= (fun tail -> + return (head::tail)))) + +let rec read_elf32_symbol_tables' offset_sizes bs = +((match offset_sizes with + | [] -> return [] + | x::xs -> + let (offset, size) = x in + let (_, relevant) = (Utility.partition_bitstring offset bs) in + let (cut, _) = (Utility.partition_bitstring size relevant) in + read_elf32_symbol_table_entries cut >>= (fun head -> + read_elf32_symbol_tables' xs bs >>= (fun tail -> + return (head::tail))) + )) + +type elf32_symbol_table = elf32_symbol_table_entry list + +let read_elf32_symbol_tables sections bs : ( elf32_symbol_table list) error = +(let symtabs = (List.filter (fun sect -> + (Int64.to_int sect.elf32_sh_type = sht_symtab) || + (Int64.to_int sect.elf32_sh_type = sht_dynsym)) sections) + in + let _ = (print_endline ("Symtabs: " ^ natShow (List.length symtabs))) in + let offsets_sizes = (List.map (fun sect -> + let offset = ((Int64.to_int sect.elf32_sh_offset) * 8) in + let size = +(let _ = (print_endline ("YYY size: " ^ natShow (Int64.to_int sect.elf32_sh_size * 8))) in + Int64.to_int sect.elf32_sh_size * 8) + in + (offset, size)) symtabs) + in + read_elf32_symbol_tables' offsets_sizes bs) + +let string_of_elf32_symbol_table tbl = +("Symbol table contents:" ^ ("\n" ^ + List.fold_right (^) (List.map string_of_elf32_symbol_table_entry tbl) "")) diff --git a/src/elf_model/elf_types.lem b/src/elf_model/elf_types.lem new file mode 100644 index 00000000..d35a9713 --- /dev/null +++ b/src/elf_model/elf_types.lem @@ -0,0 +1,292 @@ +open import Num +open import String + +open import Endianness + +open import Bitstring +open import Error +open import Show + +(** unsigned char type and bindings *) + +type unsigned_char + +declare ocaml target_rep type unsigned_char = `Uint32.t` + +(** [string_of_unsigned_char uc] provides a string representation of unsigned + * char [uc] (in base 10). + *) +val string_of_unsigned_char : unsigned_char -> string + +(** [nat_of_unsigned_char uc] converts an unsigned char [uc] into a nat. + *) +val nat_of_unsigned_char : unsigned_char -> nat + +(** [unsigned_char_of_nat n] converts a nat [n] into an unsigned char, wrapping + * around if the size of the nat exceeds the storage capacity of an unsigned + * char. + *) +val unsigned_char_of_nat : nat -> unsigned_char + +(** [unsigned_char_land uc0 uc1] bitwise ANDs two unsigned chars, [uc0] and [uc1] + * together. + *) +val unsigned_char_land : unsigned_char -> unsigned_char -> unsigned_char + +(** [unsigned_char_lshift uc n] performs a left bitshift of [n] places on unsigned + * char [uc]. + *) +val unsigned_char_lshift : unsigned_char -> nat -> unsigned_char + +(** [unsigned_char_rshift uc n] performs a right bitshift of [n] places on unsigned + * char [uc]. + *) +val unsigned_char_rshift : unsigned_char -> nat -> unsigned_char + +(** [unsigned_char_plus uc0 uc1] adds two unsigned chars, [uc0] and [uc1]. + *) +val unsigned_char_plus : unsigned_char -> unsigned_char -> unsigned_char + +(** [read_unsigned_char end bs0] reads an unsigned char from bitstring [bs0] + * assuming endianness [end]. Returns the unsigned char and the remainder of + * the bitstring. Fails if an unsigned char cannot be read from the bitstring, + * e.g. if [bs0] is too small. + *) +val read_unsigned_char : endianness -> bitstring -> error (unsigned_char * bitstring) + +declare ocaml target_rep function string_of_unsigned_char = `Uint32.to_string` +declare ocaml target_rep function nat_of_unsigned_char = `Uint32.to_int` +declare ocaml target_rep function unsigned_char_of_nat = `Uint32.of_int` +declare ocaml target_rep function unsigned_char_land = `Uint32.logand` +declare ocaml target_rep function unsigned_char_lshift = `Uint32.shift_left` +declare ocaml target_rep function unsigned_char_rshift = `Uint64.shift_right` +declare ocaml target_rep function unsigned_char_plus = `Uint32.add` +declare ocaml target_rep function read_unsigned_char = `Ml_bindings.read_unsigned_char` + +instance (Show unsigned_char) + let show = string_of_unsigned_char +end + +(** elf32_addr type and bindings *) + +type elf32_addr + +declare ocaml target_rep type elf32_addr = `Uint32.t` + +val string_of_elf32_addr : elf32_addr -> string +val nat_of_elf32_addr : elf32_addr -> nat +val read_elf32_addr : endianness -> bitstring -> error (elf32_addr * bitstring) + +declare ocaml target_rep function string_of_elf32_addr = `Uint32.to_string` +declare ocaml target_rep function read_elf32_addr = `Ml_bindings.read_elf32_addr` +declare ocaml target_rep function nat_of_elf32_addr = `Uint32.to_int` + +instance (Show elf32_addr) + let show = string_of_elf32_addr +end + +(** elf64_addr type and bindings *) + +type elf64_addr + +declare ocaml target_rep type elf64_addr = `Uint64.t` + +val string_of_elf64_addr : elf64_addr -> string +val nat_of_elf64_addr : elf64_addr -> nat +val read_elf64_addr : endianness -> bitstring -> error (elf64_addr * bitstring) + +declare ocaml target_rep function string_of_elf64_addr = `Uint64.to_string` +declare ocaml target_rep function read_elf64_addr = `Ml_bindings.read_elf64_addr` +declare ocaml target_rep function nat_of_elf64_addr = `Uint64.to_int` + +instance (Show elf64_addr) + let show = string_of_elf64_addr +end + +(** elf32_half type and bindings *) + +type elf32_half + +declare ocaml target_rep type elf32_half = `Uint32.t` + +val string_of_elf32_half : elf32_half -> string +val read_elf32_half : endianness -> bitstring -> error (elf32_half * bitstring) +val nat_of_elf32_half : elf32_half -> nat + +declare ocaml target_rep function string_of_elf32_half = `Uint32.to_string` +declare ocaml target_rep function read_elf32_half = `Ml_bindings.read_elf32_half` +declare ocaml target_rep function nat_of_elf32_half = `Uint32.to_int` + +instance (Show elf32_half) + let show = string_of_elf32_half +end + +(** elf64_half type and bindings *) + +type elf64_half + +declare ocaml target_rep type elf64_half = `Uint32.t` + +val string_of_elf64_half : elf64_half -> string +val read_elf64_half : endianness -> bitstring -> error (elf64_half * bitstring) +val nat_of_elf64_half : elf64_half -> nat + +declare ocaml target_rep function string_of_elf64_half = `Uint32.to_string` +declare ocaml target_rep function read_elf64_half = `Ml_bindings.read_elf64_half` +declare ocaml target_rep function nat_of_elf64_half = `Uint32.to_int` + +instance (Show elf64_half) + let show = string_of_elf64_half +end + +(** elf32_off type and bindings *) + +type elf32_off + +declare ocaml target_rep type elf32_off = `Uint32.t` + +val string_of_elf32_off : elf32_off -> string +val nat_of_elf32_off : elf32_off -> nat +val read_elf32_off : endianness -> bitstring -> error (elf32_off * bitstring) + +declare ocaml target_rep function string_of_elf32_off = `Uint32.to_string` +declare ocaml target_rep function read_elf32_off = `Ml_bindings.read_elf32_off` +declare ocaml target_rep function nat_of_elf32_off = `Uint32.to_int` + +instance (Show elf32_off) + let show = string_of_elf32_off +end + +(** elf64_off type and bindings *) + +type elf64_off + +declare ocaml target_rep type elf64_off = `Uint64.t` + +val string_of_elf64_off : elf64_off -> string +val nat_of_elf64_off : elf64_off -> nat +val read_elf64_off : endianness -> bitstring -> error (elf64_off * bitstring) + +declare ocaml target_rep function string_of_elf64_off = `Uint64.to_string` +declare ocaml target_rep function read_elf64_off = `Ml_bindings.read_elf64_off` +declare ocaml target_rep function nat_of_elf64_off = `Uint64.to_int` + +instance (Show elf64_off) + let show = string_of_elf64_off +end + +(** elf32_word type and bindings *) + +type elf32_word + +declare ocaml target_rep type elf32_word = `Uint32.t` + +val string_of_elf32_word : elf32_word -> string +val nat_of_elf32_word : elf32_word -> nat +val elf32_word_of_int32 : int32 -> elf32_word +val elf32_word_land : elf32_word -> elf32_word -> elf32_word +val read_elf32_word : endianness -> bitstring -> error (elf32_word * bitstring) + +declare ocaml target_rep function string_of_elf32_word = `Uint32.to_string` +declare ocaml target_rep function read_elf32_word = `Ml_bindings.read_elf32_word` +declare ocaml target_rep function nat_of_elf32_word = `Uint32.to_int` +declare ocaml target_rep function elf32_word_of_int32 = `Uint32.of_int32` +declare ocaml target_rep function elf32_word_land = `Uint32.logand` + +instance (Show elf32_word) + let show = string_of_elf32_word +end + +(** elf64_word type and bindings *) + +type elf64_word + +declare ocaml target_rep type elf64_word = `Uint32.t` + +val string_of_elf64_word : elf64_word -> string +val nat_of_elf64_word : elf64_word -> nat +val elf64_word_of_int32 : int32 -> elf64_word +val elf64_word_land : elf64_word -> elf64_word -> elf64_word +val read_elf64_word : endianness -> bitstring -> error (elf64_word * bitstring) + +declare ocaml target_rep function string_of_elf64_word = `Uint32.to_string` +declare ocaml target_rep function read_elf64_word = `Ml_bindings.read_elf64_word` +declare ocaml target_rep function nat_of_elf64_word = `Uint32.to_int` +declare ocaml target_rep function elf64_word_of_int32 = `Uint32.of_int32` +declare ocaml target_rep function elf64_word_land = `Uint32.logand` + +instance (Show elf64_word) + let show = string_of_elf64_word +end + +(** elf32_sword type and bindings *) + +type elf32_sword + +declare ocaml target_rep type elf32_sword = `Int32.t` + +val string_of_elf32_sword : elf32_sword -> string +val nat_of_elf32_sword : elf32_sword -> nat +val read_elf32_sword : endianness -> bitstring -> error (elf32_sword * bitstring) + +declare ocaml target_rep function string_of_elf32_sword = `Int32.to_string` +declare ocaml target_rep function read_elf32_sword = `Ml_bindings.read_elf32_sword` +declare ocaml target_rep function nat_of_elf32_sword = `Int32.to_int` + +instance (Show elf32_sword) + let show = string_of_elf32_sword +end + +(** elf64_sword type and bindings *) + +type elf64_sword + +declare ocaml target_rep type elf64_sword = `Int32.t` + +val string_of_elf64_sword : elf64_sword -> string +val nat_of_elf64_sword : elf64_sword -> nat +val read_elf64_sword : endianness -> bitstring -> error (elf64_sword * bitstring) + +declare ocaml target_rep function string_of_elf64_sword = `Int32.to_string` +declare ocaml target_rep function read_elf64_sword = `Ml_bindings.read_elf64_sword` +declare ocaml target_rep function nat_of_elf64_sword = `Int32.to_int` + +instance (Show elf64_sword) + let show = string_of_elf64_sword +end + +(** elf64_sword type and bindings *) + +type elf64_xword + +declare ocaml target_rep type elf64_xword = `Uint64.t` + +val string_of_elf64_xword : elf64_xword -> string +val nat_of_elf64_xword : elf64_xword -> nat +val read_elf64_xword : endianness -> bitstring -> error (elf64_xword * bitstring) + +declare ocaml target_rep function string_of_elf64_xword = `Uint64.to_string` +declare ocaml target_rep function read_elf64_xword = `Ml_bindings.read_elf64_xword` +declare ocaml target_rep function nat_of_elf64_xword = `Uint64.to_int` + +instance (Show elf64_xword) + let show = string_of_elf64_xword +end + +(** elf64_sxword type and bindings *) + +type elf64_sxword + +declare ocaml target_rep type elf64_sxword = `Int64.t` + +val string_of_elf64_sxword : elf64_sxword -> string +val nat_of_elf64_sxword : elf64_sxword -> nat +val read_elf64_sxword : endianness -> bitstring -> error (elf64_sxword * bitstring) + +declare ocaml target_rep function string_of_elf64_sxword = `Int64.to_string` +declare ocaml target_rep function read_elf64_sxword = `Ml_bindings.read_elf64_sxword` +declare ocaml target_rep function nat_of_elf64_sxword = `Int64.to_int` + +instance (Show elf64_sxword) + let show = string_of_elf64_sxword +end
\ No newline at end of file diff --git a/src/elf_model/endianness.lem b/src/elf_model/endianness.lem new file mode 100644 index 00000000..9adba6cd --- /dev/null +++ b/src/elf_model/endianness.lem @@ -0,0 +1,35 @@ +(** [endian.lem] defines a type for describing the endianness of an ELF file, + * and functions and other operations over that type. + *) + +open import String + +open import Show + +(** Type [endianness] describes the endianness of an ELF file. This is deduced from + * the first few bytes (magic number, etc.) of the ELF header. + *) +type endianness + = Big (* Big endian *) + | Little (* Little endian *) + +(** [default_endianness] is a default endianness to use when reading in the ELF header + * before we have deduced from its entries what the rest of the file is encoded + * with. + *) +val default_endianness : endianness +let default_endianness = Little + +(** [string_of_endianness e] produces a string representation of the [endianness] value + * [e]. + *) +val string_of_endianness : endianness -> string +let string_of_endianness e = + match e with + | Big -> "Big" + | Little -> "Little" + end + +instance (Show endianness) + let show = string_of_endianness +end
\ No newline at end of file diff --git a/src/elf_model/error.lem b/src/elf_model/error.lem new file mode 100644 index 00000000..ca34a5d4 --- /dev/null +++ b/src/elf_model/error.lem @@ -0,0 +1,86 @@ +open import List +open import Num +open import String + +open import Show + +(** [error] is a type used to represent potentially failing computations. [Success] + * marks a successful completion of a computation, whilst [Fail err] marks a failure, + * with [err] as the reason. + *) +type error 'a + = Success of 'a + | Fail of string + +(** [return] is the monadic lifting function for [error], representing a successful + * computation. + *) +val return : forall 'a. 'a -> error 'a +let return r = Success r + +(** [fail err] represents a failing computation, with error message [err]. + *) +val fail : forall 'a. string -> error 'a +let fail err = Fail err + +(** [(>>=)] is the monadic binding function for [error]. + *) +val (>>=) : forall 'a 'b. error 'a -> ('a -> error 'b) -> error 'b +let (>>=) x f = + match x with + | Success s -> f s + | Fail err -> Fail err + end + +(** [repeatM count action] fails if [action] is a failing computation, or + * successfully produces a list [count] elements long, where each element is + * the value successfully returned by [action]. + *) +val repeatM : forall 'a. nat -> error 'a -> error (list 'a) +let rec repeatM count action = + match count with + | 0 -> return [] + | m -> + action >>= fun head -> + repeatM (m - 1) action >>= fun tail -> + return (head::tail) + end + +(** [repeatM' count seed action] is a variant of [repeatM] that acts like [repeatM] + * apart from any successful result returns a tuple whose second component is [seed] + * and whose first component is the same as would be returned by [repeatM]. + *) +val repeatM' : forall 'a 'b. nat -> 'b -> ('b -> error ('a * 'b)) -> error ((list 'a) * 'b) +let rec repeatM' count seed action = + match count with + | 0 -> return ([], seed) + | m -> + action seed >>= fun (head, seed) -> + repeatM' (m - 1) seed action >>= fun (tail, seed) -> + return (head::tail, seed) + end + +(** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs]. + *) +val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b) +let rec mapM f xs = + match xs with + | [] -> return [] + | x::xs -> + f x >>= fun hd -> + mapM f xs >>= fun tl -> + return (hd::tl) + end + +(** [string_of_error err] produces a string representation of [err]. + *) +val string_of_error : forall 'a. Show 'a => error 'a -> string +let string_of_error e = + match e with + | Fail err -> "Fail: " ^ err + | Success s -> show s + end + +instance forall 'a. Show 'a => (Show (error 'a)) + let show = string_of_error +end
\ No newline at end of file diff --git a/src/elf_model/error.ml b/src/elf_model/error.ml new file mode 100644 index 00000000..1e3557f3 --- /dev/null +++ b/src/elf_model/error.ml @@ -0,0 +1,88 @@ +(*Generated by Lem from error.lem.*) +open Lem_list +open Lem_num +open Lem_string + +open Show + +(** [error] is a type used to represent potentially failing computations. [Success] + * marks a successful completion of a computation, whilst [Fail err] marks a failure, + * with [err] as the reason. + *) +type 'a error + = Success of 'a + | Fail of string + +(** [return] is the monadic lifting function for [error], representing a successful + * computation. + *) +(*val return : forall 'a. 'a -> error 'a*) +let return r = (Success r) + +(** [fail err] represents a failing computation, with error message [err]. + *) +(*val fail : forall 'a. string -> error 'a*) +let fail err = (Fail err) + +(** [(>>=)] is the monadic binding function for [error]. + *) +(*val >>= : forall 'a 'b. error 'a -> ('a -> error 'b) -> error 'b*) +let (>>=) x f = +((match x with + | Success s -> f s + | Fail err -> Fail err + )) + +(** [repeatM count action] fails if [action] is a failing computation, or + * successfully produces a list [count] elements long, where each element is + * the value successfully returned by [action]. + *) +(*val repeatM : forall 'a. nat -> error 'a -> error (list 'a)*) +let rec repeatM count action = +((match count with + | 0 -> return [] + | m -> + action >>= (fun head -> + repeatM ( Nat_num.nat_monus m( 1)) action >>= (fun tail -> + return (head::tail))) + )) + +(** [repeatM' count seed action] is a variant of [repeatM] that acts like [repeatM] + * apart from any successful result returns a tuple whose second component is [seed] + * and whose first component is the same as would be returned by [repeatM]. + *) +(*val repeatM' : forall 'a 'b. nat -> 'b -> ('b -> error ('a * 'b)) -> error ((list 'a) * 'b)*) +let rec repeatM' count seed action = +((match count with + | 0 -> return ([], seed) + | m -> + action seed >>= (fun (head, seed) -> + repeatM' ( Nat_num.nat_monus m( 1)) seed action >>= (fun (tail, seed) -> + return ((head::tail), seed))) + )) + +(** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs]. + *) +(*val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b)*) +let rec mapM f xs = +((match xs with + | [] -> return [] + | x::xs -> + f x >>= (fun hd -> + mapM f xs >>= (fun tl -> + return (hd::tl))) + )) + +(** [string_of_error err] produces a string representation of [err]. + *) +(*val string_of_error : forall 'a. Show 'a => error 'a -> string*) +let string_of_error dict_Show_Show_a e = +((match e with + | Fail err -> "Fail: " ^ err + | Success s -> dict_Show_Show_a.show_method s + )) + +let instance_Show_Show_Error_error_dict dict_Show_Show_a =({ + + show_method = + (string_of_error dict_Show_Show_a)})
\ No newline at end of file diff --git a/src/elf_model/main.lem b/src/elf_model/main.lem new file mode 100644 index 00000000..a7e7a709 --- /dev/null +++ b/src/elf_model/main.lem @@ -0,0 +1,41 @@ +open import Function +open import String +open import Tuple + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +open import Elf_header +open import Elf_file1 +open import Elf_executable_file2 +open import Elf_executable_file3 +open import Elf_executable_file4 +open import Elf_executable_file5 + +open import Sail_interface + +let default_os _ = + "*Default OS specific print*" + +let default_proc _ = + "*Default processor specific print*" + +let default_user _ = + "*Default user specific print*" + +let default_hdr_bdl = + (default_os, default_proc) + +let default_pht_bdl = + (default_os, default_proc) + +let default_sht_bdl = + (default_os, default_proc, default_user) + +let _ = + let (chunks_addr, entry) = Sail_interface.populate "test/power64-executable-1" in + let _ = Missing_pervasives.print ("Entry point: " ^ show entry) in + let _ = Missing_pervasives.print ("#Chunks: " ^ show (List.length chunks_addr)) in + ()
\ No newline at end of file diff --git a/src/elf_model/missing_pervasives.lem b/src/elf_model/missing_pervasives.lem new file mode 100644 index 00000000..308c43c3 --- /dev/null +++ b/src/elf_model/missing_pervasives.lem @@ -0,0 +1,55 @@ +open import Basic_classes +open import Bool +open import List +open import Maybe +open import Num +open import String + +(** [intercalate sep xs] places [sep] between all elements of [xs]. *) +val intercalate : forall 'a. 'a -> list 'a -> list 'a +let rec intercalate sep xs = + match xs with + | [] -> [] + | [x] -> [x] + | x::xs -> x::sep::intercalate sep xs + end + +(** [unlines xs] concatenates a list of strings [xs], placing each entry + * on a new line. + *) +val unlines : list string -> string +let unlines xs = + foldr (^) "" (intercalate "\n" xs) + +(** [bracket xs] concatenates a list of strings [xs], separating each entry with a + * space, and bracketing the resulting string. + *) +val bracket : list string -> string +let bracket xs = + "(" ^ foldr (^) "" (intercalate " " xs) ^ ")" + +(** [null_char] is the null character. *) +val null_char : char + +declare ocaml target_rep function null_char = `'\000'` + +(** [split_string_on_char s c] splits a string [s] into a list of substrings + * on character [c], otherwise returning the singleton list containing [s] + * if [c] is not found in [s]. + *) +val split_string_on_char : string -> char -> list string +declare ocaml target_rep function split_string_on_char = `Ml_bindings.split_string_on_char` + +(** [print s] prints [s] to stdout. *) +val print : string -> unit +declare ocaml target_rep function print = `print_endline` + +(** [string_of_nat m] produces a string representation of natural number [m]. *) +val string_of_nat : nat -> string +declare ocaml target_rep function string_of_nat = `string_of_int` + +(** [string_suffix i s] chops [i] characters off [s], returning a new string. + * Fails if the index is negative, or beyond the end of the string. + *) +val string_suffix : nat -> string -> maybe string +declare ocaml target_rep function string_suffix = `Ml_bindings.string_suffix`
\ No newline at end of file diff --git a/src/elf_model/ml_bindings.ml b/src/elf_model/ml_bindings.ml new file mode 100644 index 00000000..0dd4d152 --- /dev/null +++ b/src/elf_model/ml_bindings.ml @@ -0,0 +1,323 @@ +open Endianness +open Error + +let decimal_string_of_int64 e = + let i = Int64.to_int e in + string_of_int i +;; + +let hex_string_of_int64 (e : Int64.t) : string = + let i = Int64.to_int e in + Printf.sprintf "0x%x" i +;; + +let partition_bitstring size bitstring = + Bitstring.takebits size bitstring, Bitstring.dropbits size bitstring +;; + +let acquire_bitstring path_to_target = + try + let bitstring = Bitstring.bitstring_of_file path_to_target in + return bitstring + with _ -> + Fail ("acquire_bitstring: cannot open file" ^ path_to_target) + +(** Unsigned char type *) + +let read_unsigned_char_le bs rest = + bitmatch bs with + | { unsigned : 8 : littleendian } -> return (Uint32.of_int unsigned, rest) + | { _ } -> Fail "read_unsigned_char_le" +;; + +let read_unsigned_char_be bs rest = + bitmatch bs with + | { unsigned : 8 : bigendian } -> return (Uint32.of_int unsigned, rest) + | { _ } -> Fail "read_unsigned_char_be" +;; + +let read_unsigned_char endian bs = + let cut, rest = partition_bitstring 8 bs in + match endian with + | Little -> read_unsigned_char_le cut rest + | Big -> read_unsigned_char_be cut rest +;; + +(** ELF address type: + * 4 byte unsigned type on 32-bit architectures. + * 8 byte unsigned type on 64-bit architectures. + *) + +let read_elf32_addr_le bs rest = + bitmatch bs with + | { addr : 32 : littleendian } -> return (Uint32.of_int32 addr, rest) + | { _ } -> Fail "read_elf32_addr_le" +;; + +let read_elf32_addr_be bs rest = + bitmatch bs with + | { addr : 32 : bigendian } -> return (Uint32.of_int32 addr, rest) + | { _ } -> Fail "read_elf32_addr_be" +;; + +let read_elf32_addr endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf32_addr_le cut rest + | Big -> read_elf32_addr_be cut rest +;; + +let read_elf64_addr_le bs rest = + bitmatch bs with + | { addr : 64 : littleendian } -> return (Uint64.of_int64 addr, rest) + | { _ } -> Fail "read_elf64_addr_le" +;; + +let read_elf64_addr_be bs rest = + bitmatch bs with + | { addr : 64 : bigendian } -> return (Uint64.of_int64 addr, rest) + | { _ } -> Fail "read_elf64_addr_be" +;; + +let read_elf64_addr endian bs = + let cut, rest = partition_bitstring 64 bs in + match endian with + | Little -> read_elf64_addr_le cut rest + | Big -> read_elf64_addr_be cut rest +;; + +(** ELF offset type: + * 4 byte unsigned type on 32-bit architectures. + * 8 byte unsigned type on 64-bit architectures. + *) +let read_elf32_off_le bs rest = + bitmatch bs with + | { off : 32 : littleendian } -> return (Uint32.of_int32 off, rest) + | { _ } -> Fail "read_elf32_off_le" +;; + +let read_elf32_off_be bs rest = + bitmatch bs with + | { off : 32 : bigendian } -> return (Uint32.of_int32 off, rest) + | { _ } -> Fail "read_elf32_off_be" +;; + +let read_elf32_off endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf32_off_le cut rest + | Big -> read_elf32_off_be cut rest +;; + +let read_elf64_off_le bs rest = + bitmatch bs with + | { off : 64 : littleendian } -> return (Uint64.of_int64 off, rest) + | { _ } -> Fail "read_elf64_off_le" +;; + +let read_elf64_off_be bs rest = + bitmatch bs with + | { off : 64: bigendian } -> return (Uint64.of_int64 off, rest) + | { _ } -> Fail "read_elf64_off_be" +;; + +let read_elf64_off endian bs = + let cut, rest = partition_bitstring 64 bs in + match endian with + | Little -> read_elf64_off_le cut rest + | Big -> read_elf64_off_be cut rest +;; + +(** ELF half word type: + * 2 byte unsigned type on 32-bit architectures. + * 2 byte unsigned type on 64-bit architecutres. + *) + +let read_elf32_half_le bs rest = + bitmatch bs with + | { half : 16 : littleendian } -> return (Uint32.of_int half, rest) + | { _ } -> Fail "read_elf32_half_le" +;; + +let read_elf32_half_be bs rest = + bitmatch bs with + | { half : 16 : bigendian } -> return (Uint32.of_int half, rest) + | { _ } -> Fail "read_elf32_half_be" +;; + +let read_elf32_half endian bs = + let cut, rest = partition_bitstring 16 bs in + match endian with + | Little -> read_elf32_half_le cut rest + | Big -> read_elf32_half_be cut rest +;; + +let read_elf64_half_le bs rest = + bitmatch bs with + | { half : 16 : littleendian } -> return (Uint32.of_int half, rest) + | { _ } -> Fail "read_elf64_half_le" +;; + +let read_elf64_half_be bs rest = + bitmatch bs with + | { half : 16 : bigendian } -> return (Uint32.of_int half, rest) + | { _ } -> Fail "read_elf64_half_be" +;; + +let read_elf64_half endian bs = + let cut, rest = partition_bitstring 16 bs in + match endian with + | Little -> read_elf64_half_le cut rest + | Big -> read_elf64_half_be cut rest +;; + +(** ELF word type: + * 4 byte unsigned type on 32-bit architectures. + * 4 byte unsigned type on 32-bit architectures. + *) + +let read_elf32_word_le bs rest = + bitmatch bs with + | { word : 32 : littleendian } -> return (Uint32.of_int32 word, rest) + | { _ } -> Fail "read_elf32_word_le" +;; + +let read_elf32_word_be bs rest = + bitmatch bs with + | { word : 32 : bigendian } -> return (Uint32.of_int32 word, rest) + | { _ } -> Fail "read_elf32_word_be" +;; + +let read_elf32_word endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf32_word_le cut rest + | Big -> read_elf32_word_be cut rest +;; + +let read_elf64_word_le bs rest = + bitmatch bs with + | { word : 32 : littleendian } -> return (Uint32.of_int32 word, rest) + | { _ } -> Fail "read_elf64_word_le" +;; + +let read_elf64_word_be bs rest = + bitmatch bs with + | { word : 32 : bigendian } -> return (Uint32.of_int32 word, rest) + | { _ } -> Fail "read_elf64_word_be" +;; + +let read_elf64_word endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf64_word_le cut rest + | Big -> read_elf64_word_be cut rest +;; + +(** ELF signed word type: + * 4 byte signed type on 32-bit architectures + * 4 byte signed type on 64-bit architectures + *) + +let read_elf32_sword_le bs rest = + bitmatch bs with + | { word : 32 : littleendian } -> return (word, rest) + | { _ } -> Fail "read_elf32_sword_le" +;; + +let read_elf32_sword_be bs rest = + bitmatch bs with + | { word : 32 : bigendian } -> return (word, rest) + | { _ } -> Fail "read_elf32_sword_be" +;; + +let read_elf32_sword endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf32_sword_le cut rest + | Big -> read_elf32_sword_be cut rest +;; + +let read_elf64_sword_le bs rest = + bitmatch bs with + | { word : 32 : littleendian } -> return (word, rest) + | { _ } -> Fail "read_elf64_sword_le" +;; + +let read_elf64_sword_be bs rest = + bitmatch bs with + | { word : 32 : bigendian } -> return (word, rest) + | { _ } -> Fail "read_elf64_sword_be" +;; + +let read_elf64_sword endian bs = + let cut, rest = partition_bitstring 32 bs in + match endian with + | Little -> read_elf64_sword_le cut rest + | Big -> read_elf64_sword_be cut rest +;; + +(** ELF extra wide word type: + * 8 byte unsigned type on 64-bit architectures. + *) + +let read_elf64_xword_le bs rest = + bitmatch bs with + | { addr : 64 : littleendian } -> return (Uint64.of_int64 addr, rest) + | { _ } -> Fail "read_elf64_xword_le" +;; + +let read_elf64_xword_be bs rest = + bitmatch bs with + | { addr : 64 : bigendian } -> return (Uint64.of_int64 addr, rest) + | { _ } -> Fail "read_elf64_xword_be" +;; + +let read_elf64_xword endian bs = + let cut, rest = partition_bitstring 64 bs in + match endian with + | Little -> read_elf64_xword_le cut rest + | Big -> read_elf64_xword_be cut rest +;; + +(** ELF signed extra wide word type: + * 8 byte signed type on 64-bit architectures. + *) + +let read_elf64_sxword_le bs rest = + bitmatch bs with + | { addr : 64 : littleendian } -> return (addr, rest) + | { _ } -> Fail "read_elf64_sxword_le" +;; + +let read_elf64_sxword_be bs rest = + bitmatch bs with + | { addr : 64 : bigendian } -> return (addr, rest) + | { _ } -> Fail "read_elf64_sxword_be" +;; + +let read_elf64_sxword endian bs = + let cut, rest = partition_bitstring 64 bs in + match endian with + | Little -> read_elf64_sxword_le cut rest + | Big -> read_elf64_sxword_be cut rest +;; + +(** Misc. string operations. *) + +let split_string_on_char strings c = + let enum = BatString.enum strings in + let groups = BatEnum.group (fun char -> char <> c) enum in + let enums = BatEnum.map BatString.of_enum groups in + BatList.of_enum enums +;; + +let string_suffix index str = + if index < 0 || index > String.length str then + None + else + try + Some (String.sub str index (String.length str - index)) + with + | _ -> None +;;
\ No newline at end of file diff --git a/src/elf_model/pre_main.ml b/src/elf_model/pre_main.ml new file mode 100644 index 00000000..02eaf41c --- /dev/null +++ b/src/elf_model/pre_main.ml @@ -0,0 +1,8 @@ +(*Generated by Lem from pre_main.lem.*) +open Show + +open Elf_section_header + +(*val display : elf32_section_header_table -> string*) +let display = (listShow + instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict) diff --git a/src/elf_model/sail_interface.lem b/src/elf_model/sail_interface.lem new file mode 100644 index 00000000..7bfad805 --- /dev/null +++ b/src/elf_model/sail_interface.lem @@ -0,0 +1,44 @@ +open import Basic_classes +open import Function +open import Maybe +open import String +open import Tuple + +open import Assert_extra + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +open import Elf_header +open import Elf_executable_file5 +open import Elf_types + +val populate : string -> list (bitstring * nat) * nat +let populate fname = + let res = + (* Acquire the data from the file... *) + Bitstring.acquire fname >>= fun bs0 -> + (* 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 List.index ident 4 with + | Nothing -> fail "populate: ELF ident transcription error" + | Just c -> + (* Calculate whether we are dealing with a 32- or 64-bit file based on + * what we have read... + *) + if nat_of_unsigned_char c = Elf_header.elf_class_32 then + Elf_executable_file5.read_elf32_executable_file5 bs0 >>= + Elf_executable_file5.elf32_construct_image + else if nat_of_unsigned_char c = Elf_header.elf_class_64 then + Elf_executable_file5.read_elf64_executable_file5 bs0 >>= + Elf_executable_file5.elf64_construct_image + else + fail "populate: ELF class unrecognised" + end + in + match res with + | Fail err -> failwith err + | Success chunks -> chunks + end
\ No newline at end of file diff --git a/src/elf_model/show.lem b/src/elf_model/show.lem new file mode 100644 index 00000000..b9d45f08 --- /dev/null +++ b/src/elf_model/show.lem @@ -0,0 +1,57 @@ +(** [show.lem] exports the typeclass [Show] and associated functions for pretty + * printing arbitrary values. + *) + +open import Function +open import List +open import Num +open import String + +open import Missing_pervasives + +class (Show 'a) + val show : 'a -> string +end + +(** [string_of_bool b] produces a string representation of boolean [b]. + *) +val string_of_bool : bool -> string +let string_of_bool b = + match b with + | true -> "true" + | false -> "false" + end + +instance (Show bool) + let show = string_of_bool +end + +instance (Show string) + let show = id +end + +(** [string_of_pair p] produces a string representation of pair [p]. + *) +val string_of_pair : forall 'a 'b. Show 'a, Show 'b => ('a * 'b) -> string +let string_of_pair (left, right) = + "(" ^ show left ^ ", " ^ show right ^ ")" + +instance forall 'a 'b. Show 'a, Show 'b => (Show ('a * 'b)) + let show = string_of_pair +end + +(** [string_of_list l] produces a string representation of list [l]. + *) +val string_of_list : forall 'a. Show 'a => list 'a -> string +let string_of_list l = + let result = intercalate "," (map show l) in + let folded = foldr (^) "" result in + "[" ^ folded ^ "]" + +instance forall 'a. Show 'a => (Show (list 'a)) + let show = string_of_list +end + +instance (Show nat) + let show = string_of_nat +end diff --git a/src/elf_model/string_table.lem b/src/elf_model/string_table.lem new file mode 100644 index 00000000..8cfe5056 --- /dev/null +++ b/src/elf_model/string_table.lem @@ -0,0 +1,87 @@ +open import List +open import Maybe +open import Num +open import String + +open import Error +open import Missing_pervasives +open import Show + +type string_table + = Strings of (char * string) + +(** [mk_string_table base sep] constructs a string table using [base] as the + * base string and [sep] as the delimiting character to use to split [base] + * when trying to access the string stored in the table using the functions below. + *) +val mk_string_table : string -> char -> string_table +let mk_string_table base sep = + Strings (sep, base) + +(** [empty] is the empty string table with an arbitrary choice of delimiter. + *) +val empty : string_table +let empty = Strings (Missing_pervasives.null_char, "") + +(** [get_delimiating_character tbl] returns the delimiting character associated + * with the string table [tbl], used to split the strings. + *) +val get_delimiting_character : string_table -> char +let get_delimiting_character tbl = + match tbl with + | Strings (sep, base) -> sep + end + +(** [get_base_string tbl] returns the base string of the string table [tbl]. + *) +val get_base_string : string_table -> string +let get_base_string tbl = + match tbl with + | Strings (sep, base) -> base + end + +(** [get_strings tbl] obtains the strings stored in the table, separated using + * the designated separator as a delimiting character. + *) +val get_strings : string_table -> list string +let get_strings tbl = + match tbl with + | Strings (sep, base) -> + Missing_pervasives.split_string_on_char base sep + end + +(** [size tbl] returns the number of strings separated by the designated + * separator in the string table [tbl]. + *) +val size : string_table -> nat +let size tbl = + List.length (get_strings tbl) + +(** [get_string_at index tbl] returns the string starting at character [index] + * from the start of the base string until the first occurrence of the delimiting + * character. + *) +val get_string_at : nat -> string_table -> error string +let get_string_at index tbl = + match Missing_pervasives.string_suffix index (get_base_string tbl) with + | Nothing -> Fail "get_string_at: invalid index into string" + | Just suffix -> + let delim = get_delimiting_character tbl in + let tbl = mk_string_table suffix delim in + match get_strings tbl with + | [] -> Fail "get_string_at: empty string returned" + | x::xs -> return x + end + end + +class (HasElf32SectionHeaderStringTable 'a) + val get_elf32_section_header_string_table : 'a -> string_table +end + +class (HasElf64SectionHeaderStringTable 'a) + val get_elf64_section_header_string_table : 'a -> string_table +end + +instance (Show string_table) + let show tbl = unlines (get_strings tbl) +end
\ No newline at end of file diff --git a/src/elf_model/utility.ml b/src/elf_model/utility.ml new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/src/elf_model/utility.ml @@ -0,0 +1 @@ + diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib new file mode 100644 index 00000000..6230c0e8 --- /dev/null +++ b/src/lem_interp/extract.mllib @@ -0,0 +1,10 @@ +Interp_ast +Interp +Interp_lib +Interp_interface +Interp_inter_imp +Instruction_extractor + +Pretty_interp +Run_interp +Run_interp_model |