diff options
Diffstat (limited to 'src')
26 files changed, 3146 insertions, 788 deletions
diff --git a/src/Makefile b/src/Makefile index 647df7f8..ab44b174 100644 --- a/src/Makefile +++ b/src/Makefile @@ -21,16 +21,22 @@ 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/ + cp -p -r ../../system-v-abi/src/libraries elf_model/libraries -power: sail interpreter - mkdir -p _build/test +elf: + $(MAKE) -C elf_model ocaml_native mkdir -p _build/elf_model - cp -p test/* _build/test/ - cp -p elf_model/* _build/elf_model + cp -p elf_model/*.cmi _build/elf_model/ + cp -p elf_model/*.cmx _build/elf_model/ + cp -p elf_model/*.o _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 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 string_table.cmx elf_section_header_table.cmx elf_executable_file3.cmx elf_executable_file4.cmx elf_interpreted_segment.cmx elf_executable_file5.cmx sail_interface.cmx + ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIB) -a -o elf_extract.cmxa missing_pervasives.cmx \ +show.cmx endianness.cmx error.cmx ml_bindings.cmx default_printing.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx string_table.cmx elf_section_header_table.cmx elf_interpreted_segment.cmx elf_symbol_table.cmx elf_executable_file3.cmx elf_linking_file2.cmx elf_linking_file3.cmx elf_relocation.cmx sail_interface.cmx + + +power: sail interpreter elf + mkdir -p _build/test + cp -p test/* _build/test/ cd _build/test ;\ ../../sail.native -lem_ast power.sail ;\ $(LEM) -ocaml -only_changed_output -lib ../lem_interp/ power.lem;\ diff --git a/src/elf_model/Makefile b/src/elf_model/Makefile index 42e17cce..dbf653f6 100644 --- a/src/elf_model/Makefile +++ b/src/elf_model/Makefile @@ -1,19 +1,76 @@ 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 + ../../lem/lem -ocaml -only_changed_output missing_pervasives.lem show.lem endianness.lem default_printing.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_symbol_table.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_linking_file2.lem elf_linking_file3.lem elf_relocation.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 + rm -rf missing_pervasives.ml show.ml endianness.ml bitstring_local.ml default_printing.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_interpreted_segment.ml elf_symbol_table.ml elf_executable_file5.ml elf_linking_file2.ml elf_linking_file3.ml elf_relocation.ml elf_symbol_table.ml sail_interface.ml main.ml + make -C libraries clean + rm -rf elf_section_header.ml elf_symbol_table.ml + rm -rf *~ + rm -rf *.cmi *.cmo + +camlp4: + camlp4 '-I' '/home/dpm/.opam/4.01.0/lib/ocaml/camlp4' '-I' '/home/dpm/.opam/4.01.0/lib/bitstring' '-parser' 'o' '-parser' 'op' '-printer' 'p' 'unix.cma' 'bitstring.cma' 'bitstring_persistent.cma' 'pa_bitstring.cmo' pa_o.cmo pr_o.cmo -oml_bindings.ml 'ml_bindings_camlp4_sugared.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 + ocamlfind ocamlc \ +-I libraries/batteries/_build/src \ +-I libraries/bitstring \ +-I libraries/uint/_build/lib \ +-I ../../lem/ocaml-lib/_build/ \ +unix.cma nums.cma batteries.cma uint.cma bitstring.cma nat_num.cmo \ +lem.cmo lem_function.cmo lem_list.cmo \ +missing_pervasives.ml \ +show.ml endianness.ml error.ml ml_bindings.ml default_printing.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_interpreted_segment.ml elf_symbol_table.ml elf_executable_file3.ml elf_linking_file2.ml elf_linking_file3.ml elf_relocation.ml sail_interface.ml main.ml \ +-dllpath libraries/uint/_build/lib -dllpath libraries/bitstring -package bitstring -package uint -package batteries + +ocaml_native: + ocamlfind ocamlopt \ +-I ../../../lem/ocaml-lib/_build/ \ +-package bitstring -package uint -package batteries \ +nums.cmxa unix.cmxa batteries.cmxa uint.cmxa bitstring.cmxa ../../../lem/ocaml-lib/_build/extract.cmxa \ +missing_pervasives.ml \ +show.ml endianness.ml error.ml ml_bindings.ml default_printing.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_interpreted_segment.ml elf_symbol_table.ml elf_executable_file3.ml elf_linking_file2.ml elf_linking_file3.ml elf_relocation.ml sail_interface.ml main.ml + + +ocaml_with_ocamlbuild: + ocamlbuild -classic-display \ + -X libraries -X ocaml-obsolete \ + -cflag -g \ + -cflags -I,libraries/batteries/_build_src \ + -cflags -I,../libraries/bitstring \ + -cflags -I,libraries/uint/_build/lib \ + -cflags -dllpath,libraries/uint/_build/lib \ + -cflags -dllpath,libraries/bitstring \ + main.byte + +ocaml_with_ocamlbuild_native: + ocamlbuild -classic-display \ + -X libraries -X ocaml-obsolete \ + -cflag -g \ + -cflags -I,../../../../lem/ocaml-lib/_build/ \ + -cflags -I,libraries/batteries/_build_src \ + -cflags -I,libraries/bitstring \ + -cflags -I,libraries/uint/_build/lib \ + -cflags -dllpath,libraries/uint/_build/lib \ + -cflags -dllpath,libraries/bitstring \ + main.native + + +clean_with_ocamlbuild: + ocamlbuild -classic-display -clean + 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 + ocamlfind ocamlc -package bitstring -package batteries -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 default_printing.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_interpreted_segment.ml elf_symbol_table.ml elf_executable_file3.ml elf_executable_file5.ml elf_linking_file2.ml elf_linking_file3.ml elf_relocation.ml sail_interface.ml main.ml + +oldall: lem-model camlp4 ocaml -all: lem-model ocaml +all: ocaml execute: ./a.out @@ -21,4 +78,3 @@ execute: go: all execute go-debug: lem-model stacktrace execute - diff --git a/src/elf_model/default_printing.lem b/src/elf_model/default_printing.lem new file mode 100644 index 00000000..d22e0fec --- /dev/null +++ b/src/elf_model/default_printing.lem @@ -0,0 +1,27 @@ +(** [default_printing] module is a small utility module providing default + * printing functions for when ABI-specific functions are not available. + * These functions were constantly being redefined and reused all over the + * place hence their placement in this module. + *) +open import Function + +(** [default_os_specific_print] is a default print function for OS specific + * functionality. + *) +val default_os_specific_print : forall 'a. 'a -> string +let default_os_specific_print = + (const "*Default OS specific print*") + +(** [default_proc_specific_print] is a default print function for processor specific + * functionality. + *) +val default_proc_specific_print : forall 'a. 'a -> string +let default_proc_specific_print = + (const "*Default processor specific print*") + +(** [default_user_specific_print] is a default print function for user specific + * functionality. + *) +val default_user_specific_print : forall 'a. 'a -> string +let default_user_specific_print = + (const "*Default user specific print*")
\ No newline at end of file diff --git a/src/elf_model/elf_executable_file3.lem b/src/elf_model/elf_executable_file3.lem index 07a2fdc1..56b2b611 100644 --- a/src/elf_model/elf_executable_file3.lem +++ b/src/elf_model/elf_executable_file3.lem @@ -5,9 +5,12 @@ open import String open import Elf_executable_file2 open import Elf_header +open import Elf_interpreted_segment open import Elf_types open import Elf_section_header_table +open import Elf_symbol_table open import Elf_program_header_table +open import String_table open import Bitstring open import Error @@ -208,4 +211,295 @@ let string_of_elf64_executable_file3 hdr_bdl pht_bdl sht_bdl f3 = ; sht ; "**Body:" ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_executable_file3_body) - ]
\ No newline at end of file + ] + +val get_elf32_section_header_string_table : elf32_executable_file3 -> error string_table +let get_elf32_section_header_string_table f3 = + let bs0 = f3.elf32_executable_file3_body in + match f3.elf32_executable_file3_section_header_table with + | Nothing -> return String_table.empty + | Just sht -> + let idx = nat_of_elf32_half f3.elf32_executable_file3_header.elf32_shstrndx in + match List.index sht idx with + | Nothing -> fail "get_elf32_string_table: 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 (String_table.mk_string_table strings Missing_pervasives.null_char) + end + end + +val get_elf64_section_header_string_table : elf64_executable_file3 -> error string_table +let get_elf64_section_header_string_table f3 = + let bs0 = f3.elf64_executable_file3_body in + match f3.elf64_executable_file3_section_header_table with + | Nothing -> return String_table.empty + | Just sht -> + let idx = nat_of_elf64_half f3.elf64_executable_file3_header.elf64_shstrndx in + match List.index sht idx with + | Nothing -> fail "get_elf64_string_table: 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 (String_table.mk_string_table strings Missing_pervasives.null_char) + end + end + +val get_elf32_symbol_string_table : elf32_executable_file3 -> error string_table +let get_elf32_symbol_string_table f3 = + let bs0 = f3.elf32_executable_file3_body in + let hdr = f3.elf32_executable_file3_header in + match f3.elf32_executable_file3_section_header_table with + | Nothing -> return String_table.empty + | Just sht -> + let strtabs = Missing_pervasives.mapMaybei (fun index sect -> + if nat_of_elf32_word sect.elf32_sh_type = sht_strtab then + if index = nat_of_elf32_half hdr.elf32_shstrndx then + Nothing + else + Just sect + else + Nothing) sht + in + let strings = List.map (fun 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 bs1 = Bitstring.offset_and_cut offset size bs0 in + let strings = Bitstring.string_of_bitstring bs1 in + String_table.mk_string_table strings Missing_pervasives.null_char) strtabs + in + String_table.concat strings + end + +val get_elf64_symbol_string_table : elf64_executable_file3 -> error string_table +let get_elf64_symbol_string_table f3 = + let bs0 = f3.elf64_executable_file3_body in + let hdr = f3.elf64_executable_file3_header in + match f3.elf64_executable_file3_section_header_table with + | Nothing -> return String_table.empty + | Just sht -> + let strtabs = Missing_pervasives.mapMaybei (fun index sect -> + if nat_of_elf64_word sect.elf64_sh_type = sht_strtab then + if index = nat_of_elf64_half hdr.elf64_shstrndx then + Nothing + else + Just sect + else + Nothing) sht + in + let strings = List.map (fun 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 bs1 = Bitstring.offset_and_cut offset size bs0 in + let strings = Bitstring.string_of_bitstring bs1 in + String_table.mk_string_table strings Missing_pervasives.null_char) strtabs + in + String_table.concat strings + end + +val get_elf32_interpreted_segments : elf32_executable_file3 -> error (list elf32_interpreted_segment) +let get_elf32_interpreted_segments f3 = + let pht = f3.elf32_executable_file3_program_header_table in + let bdy = f3.elf32_executable_file3_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 + mapM (fun sg -> + if sg.elf32_segment_memsz < sg.elf32_segment_size then + fail "get_elf32_interpreted_segments: memory size of segment cannot be less than file size" + else + return sg) segs + +val get_elf64_interpreted_segments : elf64_executable_file3 -> error (list elf64_interpreted_segment) +let get_elf64_interpreted_segments f3 = + let pht = f3.elf64_executable_file3_program_header_table in + let bdy = f3.elf64_executable_file3_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 + mapM (fun sg -> + if sg.elf64_segment_memsz < sg.elf64_segment_size then + fail "get_elf64_interpreted_segments: memory size of segment cannot be less than file size" + else + return sg) segs + +type executable_process_image = + list (bitstring * nat) * nat + +val get_elf32_executable_image : elf32_executable_file3 -> error executable_process_image +let get_elf32_executable_image f3 = + let entr = f3.elf32_executable_file3_header.elf32_entry in + get_elf32_interpreted_segments f3 >>= fun segs -> + match List.filter (fun sg -> sg.elf32_segment_type = elf_pt_load) segs with + | [] -> fail "get_elf32_executable_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 [segs]. *) + 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 "get_elf32_executable_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf32_addr entr) + end + +val get_elf64_executable_image : elf64_executable_file3 -> error executable_process_image +let get_elf64_executable_image f3 = + let entr = f3.elf64_executable_file3_header.elf64_entry in + get_elf64_interpreted_segments f3 >>= fun segs -> + match List.filter (fun sg -> sg.elf64_segment_type = elf_pt_load) segs with + | [] -> fail "get_elf64_executable_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 [segs]. *) + 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 "get_elf64_executable_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf64_addr entr) + end + +val get_elf32_symbol_table : elf32_executable_file3 -> error elf32_symbol_table +let get_elf32_symbol_table f3 = + let bs0 = f3.elf32_executable_file3_body in + let hdr = f3.elf32_executable_file3_header in + let endian = get_elf32_header_endianness hdr in + match f3.elf32_executable_file3_section_header_table with + | Nothing -> return [] + | Just sects -> + let symtabs = List.filter (fun sect -> + nat_of_elf32_word sect.elf32_sh_type = sht_symtab) sects + in + if List.length symtabs = 0 then + return [] + else if List.length symtabs = 1 then + match List.index symtabs 0 with + | Nothing -> fail "get_elf32_symbol_table: invariant failed" + | Just symtab -> + let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in + let size = nat_of_elf32_word symtab.elf32_sh_size * 8 in + let relevant = Bitstring.offset_and_cut offset size bs0 in + read_elf32_symbol_table endian relevant + end + else + fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" + end + +val get_elf64_symbol_table : elf64_executable_file3 -> error elf64_symbol_table +let get_elf64_symbol_table f3 = + let bs0 = f3.elf64_executable_file3_body in + let hdr = f3.elf64_executable_file3_header in + let endian = get_elf64_header_endianness hdr in + match f3.elf64_executable_file3_section_header_table with + | Nothing -> return [] + | Just sects -> + let symtabs = List.filter (fun sect -> + nat_of_elf64_word sect.elf64_sh_type = sht_symtab) sects + in + if List.length symtabs = 0 then + return [] + else if List.length symtabs = 1 then + match List.index symtabs 0 with + | Nothing -> fail "get_elf64_symbol_table: invariant failed" + | Just symtab -> + let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in + let size = nat_of_elf64_xword symtab.elf64_sh_size * 8 in + let relevant = Bitstring.offset_and_cut offset size bs0 in + read_elf64_symbol_table endian relevant + end + else + fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" + end + +val get_elf32_dynamic_symbol_table : elf32_executable_file3 -> error elf32_symbol_table +let get_elf32_dynamic_symbol_table f3 = + let bs0 = f3.elf32_executable_file3_body in + let hdr = f3.elf32_executable_file3_header in + let endian = get_elf32_header_endianness hdr in + match f3.elf32_executable_file3_section_header_table with + | Nothing -> return [] + | Just sects -> + let symtabs = List.filter (fun sect -> + nat_of_elf32_word sect.elf32_sh_type = sht_dynsym) sects + in + if List.length symtabs = 0 then + return [] + else if List.length symtabs = 1 then + match List.index symtabs 0 with + | Nothing -> fail "get_elf32_symbol_table: invariant failed" + | Just symtab -> + let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in + let size = nat_of_elf32_word symtab.elf32_sh_size * 8 in + let relevant = Bitstring.offset_and_cut offset size bs0 in + read_elf32_symbol_table endian relevant + end + else + fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" + end + +val get_elf64_dynamic_symbol_table : elf64_executable_file3 -> error elf64_symbol_table +let get_elf64_dynamic_symbol_table f3 = + let bs0 = f3.elf64_executable_file3_body in + let hdr = f3.elf64_executable_file3_header in + let endian = get_elf64_header_endianness hdr in + match f3.elf64_executable_file3_section_header_table with + | Nothing -> return [] + | Just sects -> + let symtabs = List.filter (fun sect -> + nat_of_elf64_word sect.elf64_sh_type = sht_dynsym) sects + in + if List.length symtabs = 0 then + return [] + else if List.length symtabs = 1 then + match List.index symtabs 0 with + | Nothing -> fail "get_elf64_symbol_table: invariant failed" + | Just symtab -> + let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in + let size = nat_of_elf64_xword symtab.elf64_sh_size * 8 in + let relevant = Bitstring.offset_and_cut offset size bs0 in + read_elf64_symbol_table endian relevant + end + else + fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" + end
\ No newline at end of file diff --git a/src/elf_model/elf_file1.lem b/src/elf_model/elf_file1.lem index ff2bba61..16ad63a3 100644 --- a/src/elf_model/elf_file1.lem +++ b/src/elf_model/elf_file1.lem @@ -1,4 +1,5 @@ open import Basic_classes +open import Bool open import String open import Endianness @@ -101,6 +102,34 @@ 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 +(** [is_relocatable_elf32_file1] tests whether the ELF file is a relocatable +* file type. +*) +val is_relocatable_elf32_file1 : elf32_file1 -> bool +let is_relocatable_elf32_file1 f1 = + nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_rel + +(** [is_relocatable_elf64_file1] tests whether the ELF file is a relocatable +* file type. +*) +val is_relocatable_elf64_file1 : elf64_file1 -> bool +let is_relocatable_elf64_file1 f1 = + nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_rel + +(** [is_linkable_elf32_file1] tests whether the ELF file is a linkable (shared + * object or relocatable) file type. + *) +val is_linkable_elf32_file1 : elf32_file1 -> bool +let is_linkable_elf32_file1 f1 = + is_shared_object_elf32_file1 f1 || is_relocatable_elf32_file1 f1 + +(** [is_linkable_elf64_file1] tests whether the ELF file is a linkable (shared + * object or relocatable) file type. + *) +val is_linkable_elf64_file1 : elf64_file1 -> bool +let is_linkable_elf64_file1 f1 = + is_shared_object_elf64_file1 f1 || is_relocatable_elf64_file1 f1 + (** [read_elf32_file1 bs] lazily unfolds [bs] revealing the ELF file's header, * leaving all other data uninterpreted. *) diff --git a/src/elf_model/elf_header.lem b/src/elf_model/elf_header.lem index 35aa4a37..3fbe0af9 100644 --- a/src/elf_model/elf_header.lem +++ b/src/elf_model/elf_header.lem @@ -6,6 +6,7 @@ open import Maybe open import Num open import String +open import Default_printing open import Endianness open import Elf_types @@ -89,6 +90,8 @@ let elf_ma_386 : nat = 3 let elf_ma_ppc : nat = 20 (** IBM PowerPC 64 *) let elf_ma_ppc64 : nat = 21 +(** AMD x86-64 *) +let elf_ma_x86_64 : nat = 62 (** [string_of_elf_machine_architecture m] produces a string representation of * the numeric encoding [m] of the ELF machine architecture. @@ -101,6 +104,8 @@ let string_of_elf_machine_architecture m = "IBM PowerPC" else if m = elf_ma_ppc64 then "IBM PowerPC 64" + else if m = elf_ma_x86_64 then + "AMD x86-64" else "Other architecture" @@ -651,14 +656,14 @@ let string_of_elf64_header (os, proc) hdr = 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*")) + (default_os_specific_print, + default_proc_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*")) + (default_os_specific_print, + default_proc_specific_print) instance (Show elf32_header) let show = string_of_elf32_header_default diff --git a/src/elf_model/elf_linking_file2.lem b/src/elf_model/elf_linking_file2.lem index df69b5c9..4242f8d6 100644 --- a/src/elf_model/elf_linking_file2.lem +++ b/src/elf_model/elf_linking_file2.lem @@ -1,13 +1,149 @@ +open import Basic_classes +open import Bool +open import Maybe +open import Num + open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String +open import Elf_file1 open import Elf_header open import Elf_section_header_table - -open import Maybe +open import Elf_types 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 + <| elf32_linking_file2_header : elf32_header + ; elf32_linking_file2_body : bitstring + ; elf32_linking_file2_section_header_table : elf32_section_header_table + |> + +class (HasElf32LinkingFile2 'a) + val get_elf32_linking_file2 : 'a -> elf32_linking_file2 +end + +instance (HasElf32LinkingFile2 elf32_linking_file2) + let get_elf32_linking_file2 f2 = f2 +end + +instance (HasElf32File1 elf32_linking_file2) + let get_elf32_file1 f2 = + <| elf32_file1_header = f2.elf32_linking_file2_header; + elf32_file1_body = f2.elf32_linking_file2_body |> +end + +instance (HasElf32Header elf32_linking_file2) + let get_elf32_header f2 = f2.elf32_linking_file2_header +end + +instance (HasElf32SectionHeaderTable elf32_linking_file2) + let get_elf32_section_header_table f2 = Just f2.elf32_linking_file2_section_header_table +end + +type elf64_linking_file2 = + <| elf64_linking_file2_header : elf64_header + ; elf64_linking_file2_body : bitstring + ; elf64_linking_file2_section_header_table : elf64_section_header_table + |> + +class (HasElf64LinkingFile2 'a) + val get_elf64_linking_file2 : 'a -> elf64_linking_file2 +end + +instance (HasElf64LinkingFile2 elf64_linking_file2) + let get_elf64_linking_file2 f2 = f2 +end + +instance (HasElf64File1 elf64_linking_file2) + let get_elf64_file1 f2 = + <| elf64_file1_header = f2.elf64_linking_file2_header; + elf64_file1_body = f2.elf64_linking_file2_body |> +end + +instance (HasElf64Header elf64_linking_file2) + let get_elf64_header f2 = f2.elf64_linking_file2_header +end + +instance (HasElf64SectionHeaderTable elf64_linking_file2) + let get_elf64_section_header_table f2 = Just f2.elf64_linking_file2_section_header_table +end + +val refine_elf32_file1 : elf32_file1 -> error elf32_linking_file2 +let refine_elf32_file1 f1 = + if not (is_linkable_elf32_file1 f1) then + fail "refine_elf32_file1: not a linkable file" + else + let hdr = f1.elf32_file1_header in + let endian = get_elf32_header_endianness hdr in + let bs1 = f1.elf32_file1_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 + fail "refine_elf32_file1: section header table not present" + 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_linking_file2_header = hdr; + elf32_linking_file2_body = bs1; + elf32_linking_file2_section_header_table = sht |> + +val read_elf32_linking_file2 : bitstring -> error elf32_linking_file2 +let read_elf32_linking_file2 bs0 = + read_elf32_file1 bs0 >>= refine_elf32_file1 + +val string_of_elf32_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf32_linking_file2 -> string +let string_of_elf32_linking_file2 hdr_bdl sht_bdl f2 = + unlines [ + "\n*Type elf32_linking_file2:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f2.elf32_linking_file2_header + ; "**Program header table:" + ; string_of_elf32_section_header_table sht_bdl f2.elf32_linking_file2_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_linking_file2_body) + ] + +val refine_elf64_file1 : elf64_file1 -> error elf64_linking_file2 +let refine_elf64_file1 f1 = + if not (is_linkable_elf64_file1 f1) then + fail "refine_elf64_file1: not a linkable file" + else + let hdr = f1.elf64_file1_header in + let endian = get_elf64_header_endianness hdr in + let bs1 = f1.elf64_file1_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 + fail "refine_elf64_file1: section header table not present" + 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_linking_file2_header = hdr; + elf64_linking_file2_body = bs1; + elf64_linking_file2_section_header_table = sht |> + +val read_elf64_linking_file2 : bitstring -> error elf64_linking_file2 +let read_elf64_linking_file2 bs0 = + read_elf64_file1 bs0 >>= refine_elf64_file1 + +val string_of_elf64_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf64_linking_file2 -> string +let string_of_elf64_linking_file2 hdr_bdl sht_bdl f2 = + unlines [ + "\n*Type elf64_linking_file2:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f2.elf64_linking_file2_header + ; "**Program header table:" + ; string_of_elf64_section_header_table sht_bdl f2.elf64_linking_file2_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_linking_file2_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_linking_file3.lem b/src/elf_model/elf_linking_file3.lem new file mode 100644 index 00000000..edb97be4 --- /dev/null +++ b/src/elf_model/elf_linking_file3.lem @@ -0,0 +1,181 @@ +open import Basic_classes +open import Maybe +open import Num + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +open import Elf_header +open import Elf_linking_file2 +open import Elf_program_header_table +open import Elf_section_header_table +open import Elf_types + +type elf32_linking_file3 = + <| elf32_linking_file3_header : elf32_header + ; elf32_linking_file3_program_header_table : maybe elf32_program_header_table + ; elf32_linking_file3_body : bitstring + ; elf32_linking_file3_section_header_table : elf32_section_header_table + |> + +class (HasElf32LinkingFile3 'a) + val get_elf32_linking_file3 : 'a -> elf32_linking_file3 +end + +instance (HasElf32LinkingFile3 elf32_linking_file3) + let get_elf32_linking_file3 f3 = f3 +end + +instance (HasElf32LinkingFile2 elf32_linking_file3) + let get_elf32_linking_file2 f3 = + <| elf32_linking_file2_header = f3.elf32_linking_file3_header; + elf32_linking_file2_body = f3.elf32_linking_file3_body; + elf32_linking_file2_section_header_table = f3.elf32_linking_file3_section_header_table |> +end + +instance (HasElf32Header elf32_linking_file3) + let get_elf32_header f3 = f3.elf32_linking_file3_header +end + +instance (HasElf32SectionHeaderTable elf32_linking_file3) + let get_elf32_section_header_table f3 = Just f3.elf32_linking_file3_section_header_table +end + +instance (HasElf32ProgramHeaderTable elf32_linking_file3) + let get_elf32_program_header_table f3 = f3.elf32_linking_file3_program_header_table +end + +val refine_elf32_linking_file2 : elf32_linking_file2 -> error elf32_linking_file3 +let refine_elf32_linking_file2 f2 = + let hdr = f2.elf32_linking_file2_header in + let sht = f2.elf32_linking_file2_section_header_table in + let endian = get_elf32_header_endianness hdr in + let bs1 = f2.elf32_linking_file2_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 + return <| elf32_linking_file3_header = hdr; + elf32_linking_file3_program_header_table = Nothing; + elf32_linking_file3_section_header_table = sht; + elf32_linking_file3_body = bs1 |> + 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_linking_file3_header = hdr; + elf32_linking_file3_program_header_table = Just pht; + elf32_linking_file3_section_header_table = sht; + elf32_linking_file3_body = bs1 |> + +val read_elf32_linking_file3 : bitstring -> error elf32_linking_file3 +let read_elf32_linking_file3 bs0 = + read_elf32_linking_file2 bs0 >>= refine_elf32_linking_file2 + +val string_of_elf32_linking_file3 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf32_linking_file3 -> string +let string_of_elf32_linking_file3 hdr_bdl sht_bdl pht_bdl f3 = + let pht = + match f3.elf32_linking_file3_program_header_table with + | Nothing -> "\tNo program header table present" + | Just pht -> string_of_elf32_program_header_table pht_bdl pht + end + in + unlines [ + "\n*Type elf32_linking_file3:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f3.elf32_linking_file3_header + ; "**Program header table:" + ; pht + ; "**Section header table:" + ; string_of_elf32_section_header_table sht_bdl f3.elf32_linking_file3_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_linking_file3_body) + ] + +type elf64_linking_file3 = + <| elf64_linking_file3_header : elf64_header + ; elf64_linking_file3_program_header_table : maybe elf64_program_header_table + ; elf64_linking_file3_body : bitstring + ; elf64_linking_file3_section_header_table : elf64_section_header_table + |> + +class (HasElf64LinkingFile3 'a) + val get_elf64_linking_file3 : 'a -> elf64_linking_file3 +end + +instance (HasElf64LinkingFile3 elf64_linking_file3) + let get_elf64_linking_file3 f3 = f3 +end + +instance (HasElf64LinkingFile2 elf64_linking_file3) + let get_elf64_linking_file2 f3 = + <| elf64_linking_file2_header = f3.elf64_linking_file3_header; + elf64_linking_file2_body = f3.elf64_linking_file3_body; + elf64_linking_file2_section_header_table = f3.elf64_linking_file3_section_header_table |> +end + +instance (HasElf64Header elf64_linking_file3) + let get_elf64_header f3 = f3.elf64_linking_file3_header +end + +instance (HasElf64SectionHeaderTable elf64_linking_file3) + let get_elf64_section_header_table f3 = Just f3.elf64_linking_file3_section_header_table +end + +instance (HasElf64ProgramHeaderTable elf64_linking_file3) + let get_elf64_program_header_table f3 = f3.elf64_linking_file3_program_header_table +end + +val refine_elf64_linking_file2 : elf64_linking_file2 -> error elf64_linking_file3 +let refine_elf64_linking_file2 f2 = + let hdr = f2.elf64_linking_file2_header in + let sht = f2.elf64_linking_file2_section_header_table in + let endian = get_elf64_header_endianness hdr in + let bs1 = f2.elf64_linking_file2_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 + return <| elf64_linking_file3_header = hdr; + elf64_linking_file3_program_header_table = Nothing; + elf64_linking_file3_section_header_table = sht; + elf64_linking_file3_body = bs1 |> + 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_linking_file3_header = hdr; + elf64_linking_file3_program_header_table = Just pht; + elf64_linking_file3_section_header_table = sht; + elf64_linking_file3_body = bs1 |> + +val read_elf64_linking_file3 : bitstring -> error elf64_linking_file3 +let read_elf64_linking_file3 bs0 = + read_elf64_linking_file2 bs0 >>= refine_elf64_linking_file2 + +val string_of_elf64_linking_file3 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf64_linking_file3 -> string +let string_of_elf64_linking_file3 hdr_bdl sht_bdl pht_bdl f3 = + let pht = + match f3.elf64_linking_file3_program_header_table with + | Nothing -> "\tNo program header table present" + | Just pht -> string_of_elf64_program_header_table pht_bdl pht + end + in + unlines [ + "\n*Type elf64_linking_file3:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f3.elf64_linking_file3_header + ; "**Program header table:" + ; pht + ; "**Section header table:" + ; string_of_elf64_section_header_table sht_bdl f3.elf64_linking_file3_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_linking_file3_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_linking_file4.lem b/src/elf_model/elf_linking_file4.lem new file mode 100644 index 00000000..15528696 --- /dev/null +++ b/src/elf_model/elf_linking_file4.lem @@ -0,0 +1,193 @@ +open import Maybe +open import Num + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +open import Elf_header +open import Elf_linking_file3 +open import Elf_types +open import Elf_program_header_table +open import Elf_section_header_table +open import String_table + +type elf32_linking_file4 = + <| elf32_linking_file4_header : elf32_header + ; elf32_linking_file4_program_header_table : maybe elf32_program_header_table + ; elf32_linking_file4_body : bitstring + ; elf32_linking_file4_section_header_table : elf32_section_header_table + ; elf32_linking_file4_section_header_string_table : string_table + |> + +class (HasElf32LinkingFile4 'a) + val get_elf32_linking_file4 : 'a -> elf32_linking_file4 +end + +instance (HasElf32LinkingFile4 elf32_linking_file4) + let get_elf32_linking_file4 f4 = f4 +end + +instance (HasElf32LinkingFile3 elf32_linking_file4) + let get_elf32_linking_file3 f4 = + <| elf32_linking_file3_header = f4.elf32_linking_file4_header; + elf32_linking_file3_program_header_table = f4.elf32_linking_file4_program_header_table; + elf32_linking_file3_body = f4.elf32_linking_file4_body; + elf32_linking_file3_section_header_table = f4.elf32_linking_file4_section_header_table |> +end + +instance (HasElf32Header elf32_linking_file4) + let get_elf32_header f4 = f4.elf32_linking_file4_header +end + +instance (HasElf32ProgramHeaderTable elf32_linking_file4) + let get_elf32_program_header_table f4 = f4.elf32_linking_file4_program_header_table +end + +instance (HasElf32SectionHeaderTable elf32_linking_file4) + let get_elf32_section_header_table f4 = Just f4.elf32_linking_file4_section_header_table +end + +instance (HasElf32SectionHeaderStringTable elf32_linking_file4) + let get_elf32_section_header_string_table f4 = f4.elf32_linking_file4_section_header_string_table +end + +val refine_elf32_linking_file3 : elf32_linking_file3 -> error elf32_linking_file4 +let refine_elf32_linking_file3 f3 = + let hdr = f3.elf32_linking_file3_header in + let pht = f3.elf32_linking_file3_program_header_table in + let sht = f3.elf32_linking_file3_section_header_table in + let bs0 = f3.elf32_linking_file3_body in + let idx = nat_of_elf32_half hdr.elf32_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> fail "refine_elf32_linking_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_linking_file4_header = hdr; + elf32_linking_file4_program_header_table = pht; + elf32_linking_file4_section_header_table = sht; + elf32_linking_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf32_linking_file4_body = bs0 |> + end + +val read_elf32_linking_file4 : bitstring -> error elf32_linking_file4 +let read_elf32_linking_file4 bs0 = + read_elf32_linking_file3 bs0 >>= refine_elf32_linking_file3 + +val string_of_elf32_linking_file4 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf32_linking_file4 -> string +let string_of_elf32_linking_file4 hdr_bdl sht_bdl pht_bdl f4 = + let pht = + match f4.elf32_linking_file4_program_header_table with + | Nothing -> "\tNo program header table present" + | Just pht -> string_of_elf32_program_header_table pht_bdl pht + end + in + unlines [ + "\n*Type elf32_linking_file4" + ; "**Header" + ; string_of_elf32_header hdr_bdl f4.elf32_linking_file4_header + ; "**Program header table:" + ; pht + ; "**Section header table:" + ; string_of_elf32_section_header_table' sht_bdl f4.elf32_linking_file4_section_header_string_table f4.elf32_linking_file4_section_header_table + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf32_linking_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf32_linking_file4_body) + ] + +type elf64_linking_file4 = + <| elf64_linking_file4_header : elf64_header + ; elf64_linking_file4_program_header_table : maybe elf64_program_header_table + ; elf64_linking_file4_body : bitstring + ; elf64_linking_file4_section_header_table : elf64_section_header_table + ; elf64_linking_file4_section_header_string_table : string_table + |> + +class (HasElf64LinkingFile4 'a) + val get_elf64_linking_file4 : 'a -> elf64_linking_file4 +end + +instance (HasElf64LinkingFile4 elf64_linking_file4) + let get_elf64_linking_file4 f4 = f4 +end + +instance (HasElf64LinkingFile3 elf64_linking_file4) + let get_elf64_linking_file3 f4 = + <| elf64_linking_file3_header = f4.elf64_linking_file4_header; + elf64_linking_file3_program_header_table = f4.elf64_linking_file4_program_header_table; + elf64_linking_file3_body = f4.elf64_linking_file4_body; + elf64_linking_file3_section_header_table = f4.elf64_linking_file4_section_header_table |> +end + +instance (HasElf64Header elf64_linking_file4) + let get_elf64_header f4 = f4.elf64_linking_file4_header +end + +instance (HasElf64ProgramHeaderTable elf64_linking_file4) + let get_elf64_program_header_table f4 = f4.elf64_linking_file4_program_header_table +end + +instance (HasElf64SectionHeaderTable elf64_linking_file4) + let get_elf64_section_header_table f4 = Just f4.elf64_linking_file4_section_header_table +end + +instance (HasElf64SectionHeaderStringTable elf64_linking_file4) + let get_elf64_section_header_string_table f4 = f4.elf64_linking_file4_section_header_string_table +end + +val refine_elf64_linking_file3 : elf64_linking_file3 -> error elf64_linking_file4 +let refine_elf64_linking_file3 f3 = + let hdr = f3.elf64_linking_file3_header in + let pht = f3.elf64_linking_file3_program_header_table in + let sht = f3.elf64_linking_file3_section_header_table in + let bs0 = f3.elf64_linking_file3_body in + let idx = nat_of_elf64_half hdr.elf64_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> fail "refine_elf64_linking_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_linking_file4_header = hdr; + elf64_linking_file4_program_header_table = pht; + elf64_linking_file4_section_header_table = sht; + elf64_linking_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf64_linking_file4_body = bs0 |> + end + +val read_elf64_linking_file4 : bitstring -> error elf64_linking_file4 +let read_elf64_linking_file4 bs0 = + read_elf64_linking_file3 bs0 >>= refine_elf64_linking_file3 + +val string_of_elf64_linking_file4 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf64_linking_file4 -> string +let string_of_elf64_linking_file4 hdr_bdl sht_bdl pht_bdl f4 = + let pht = + match f4.elf64_linking_file4_program_header_table with + | Nothing -> "\tNo program header table present" + | Just pht -> string_of_elf64_program_header_table pht_bdl pht + end + in + unlines [ + "\n*Type elf64_linking_file4" + ; "**Header" + ; string_of_elf64_header hdr_bdl f4.elf64_linking_file4_header + ; "**Program header table:" + ; pht + ; "**Section header table:" + ; string_of_elf64_section_header_table' sht_bdl f4.elf64_linking_file4_section_header_string_table f4.elf64_linking_file4_section_header_table + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf64_linking_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf64_linking_file4_body) + ]
\ No newline at end of file diff --git a/src/elf_model/elf_relocation.lem b/src/elf_model/elf_relocation.lem new file mode 100644 index 00000000..3bfdd54c --- /dev/null +++ b/src/elf_model/elf_relocation.lem @@ -0,0 +1,42 @@ +open import Num + +open import Elf_types + +type elf32_relocation = + <| elf32_r_offset : elf32_addr (** Address at which to relocate *) + ; elf32_r_info : elf32_word (** Symbol table index/type of relocation to apply *) + |> + +type elf32_relocation_a = + <| elf32_ra_offset : elf32_addr (** Address at which to relocate *) + ; elf32_ra_info : elf32_word (** Symbol table index/type of reloation to apply *) + ; elf32_ra_addend : elf32_sword (** Addend used to compute value to be stored *) + |> + +type elf64_relocation = + <| elf64_r_offset : elf64_addr (** Address at which to relocate *) + ; elf64_r_info : elf64_xword (** Symbol table index/type of relocation to apply *) + |> + +type elf64_relocation_a = + <| elf64_ra_offset : elf64_addr (** Address at which to relocate *) + ; elf64_ra_info : elf64_xword (** Symbol table index/type of reloation to apply *) + ; elf64_ra_addend : elf64_sxword (** Addend used to compute value to be stored *) + |> + +val elf32_relocation_r_sym : elf32_word -> nat +let elf32_relocation_r_sym w = + nat_of_elf32_word (elf32_word_rshift w 8) + +val elf32_relocation_r_type : elf32_word -> nat +let elf32_relocation_r_type w = + nat_of_unsigned_char (unsigned_char_of_elf32_word w) + +val elf64_relocation_r_sym : elf64_xword -> nat +let elf64_relocation_r_sym w = + nat_of_elf64_xword (elf64_xword_rshift w 32) + +val elf64_relocation_r_type : elf64_xword -> nat +let elf64_relocation_r_type w = + let magic = (65536 * 65536) - 1 in (* 0xffffffffL *) + nat_of_elf64_xword (elf64_xword_land w (elf64_xword_of_int64 magic))
\ No newline at end of file diff --git a/src/elf_model/elf_section_header.ml b/src/elf_model/elf_section_header.ml deleted file mode 100644 index 1a73d35f..00000000 --- a/src/elf_model/elf_section_header.ml +++ /dev/null @@ -1,298 +0,0 @@ -(*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_symbol_table.lem b/src/elf_model/elf_symbol_table.lem new file mode 100644 index 00000000..54521157 --- /dev/null +++ b/src/elf_model/elf_symbol_table.lem @@ -0,0 +1,249 @@ +open import Basic_classes +open import Bool +open import List +open import Maybe +open import String +open import Tuple + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show + +open import Elf_types +open import Endianness +open import String_table + +(** Undefined symbol index *) + +let stn_undef : nat = 0 + +(** Symbol binding *) + +let stb_local : nat = 0 +let stb_global : nat = 1 +let stb_weak : nat = 2 +let stb_loos : nat = 10 +let stb_hios : nat = 12 +let stb_loproc : nat = 13 +let stb_hiproc : nat = 15 + +val string_of_symbol_binding : nat -> (nat -> string) -> (nat -> string) -> string +let string_of_symbol_binding m os proc = + if m = stb_local then + "STB_LOCAL" + else if m = stb_global then + "STB_GLOBAL" + else if m = stb_weak then + "STB_WEAK" + else if m >= stb_loos && m <= stb_hios then + os m + else if m >= stb_loproc && m <= stb_hiproc then + proc m + else + "Invalid symbol binding" + +(** Symbol types *) + +let stt_notype : nat = 0 +let stt_object : nat = 1 +let stt_func : nat = 2 +let stt_section : nat = 3 +let stt_file : nat = 4 +let stt_common : nat = 5 +let stt_tls : nat = 6 +let stt_loos : nat = 10 +let stt_hios : nat = 12 +let stt_loproc : nat = 13 +let stt_hiproc : nat = 15 + +val string_of_symbol_type : nat -> (nat -> string) -> (nat -> string) -> string +let string_of_symbol_type m os proc = + if m = stt_notype then + "STT_NOTYPE" + else if m = stt_object then + "STT_OBJECT" + else if m = stt_func then + "STT_FUNC" + else if m = stt_section then + "STT_SECTION" + else if m = stt_file then + "STT_FILE" + else if m = stt_common then + "STT_COMMON" + else if m = stt_tls then + "STT_TLS" + else if m >= stt_loos && m <= stt_hios then + os m + else if m >= stt_loproc && m <= stt_hiproc then + proc m + else + "Invalid symbol type" + +(** Symbol visibility *) + +let stv_default : nat = 0 +let stv_internal : nat = 1 +let stv_hidden : nat = 2 +let stv_protected : nat = 3 + +val string_of_symbol_visibility : nat -> string +let string_of_symbol_visibility m = + if m = stv_default then + "STV_DEFAULT" + else if m = stv_internal then + "STV_INTERNAL" + else if m = stv_hidden then + "STV_HIDDEN" + else if m = stv_protected then + "STV_PROTECTED" + else + "Invalid symbol visibility" + +(** ELF32 symbol table type *) + +type elf32_symbol_table_entry = + <| elf32_st_name : elf32_word + ; elf32_st_value : elf32_addr + ; elf32_st_size : elf32_word + ; elf32_st_info : unsigned_char + ; elf32_st_other : unsigned_char + ; elf32_st_shndx : elf32_half + |> + +(** Extraction of symbol table data *) + +(* Functions below common to 32- and 64-bit! *) + +val get_symbol_binding : unsigned_char -> nat +let get_symbol_binding entry = + nat_of_unsigned_char (unsigned_char_rshift entry 4) + +val get_symbol_type : unsigned_char -> nat +let get_symbol_type entry = + nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 15)) (* 0xf *) + +val get_symbol_info : unsigned_char -> unsigned_char -> nat +let get_symbol_info entry0 entry1 = + nat_of_unsigned_char (unsigned_char_plus + (unsigned_char_lshift entry0 4) (unsigned_char_land entry1 + (unsigned_char_of_nat 15))) (*0xf*) + +val get_symbol_visibility : unsigned_char -> nat +let get_symbol_visibility entry = + nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 3)) (* 0x3*) + +type symtab_print_bundle = (nat -> string) * (nat -> string) + +val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string +let string_of_elf32_symbol_table_entry entry = + unlines [ + "\t" ^ "Name: " ^ show entry.elf32_st_name + ; "\t" ^ "Value: " ^ show entry.elf32_st_value + ; "\t" ^ "Size: " ^ show entry.elf32_st_size + ; "\t" ^ "Info: " ^ show entry.elf32_st_info + ; "\t" ^ "Other: " ^ show entry.elf32_st_other + ; "\t" ^ "Shndx: " ^ show entry.elf32_st_shndx + ] + +type elf32_symbol_table = list elf32_symbol_table_entry + +val string_of_elf32_symbol_table : elf32_symbol_table -> string +let string_of_elf32_symbol_table symtab = + unlines (List.map string_of_elf32_symbol_table_entry symtab) + +class (HasElf32SymbolTable 'a) + val get_elf32_symbol_table : 'a -> elf32_symbol_table +end + +val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring) +let read_elf32_symbol_table_entry endian bs0 = + read_elf32_word endian bs0 >>= fun (st_name, bs0) -> + read_elf32_addr endian bs0 >>= fun (st_value, bs0) -> + read_elf32_word endian bs0 >>= fun (st_size, bs0) -> + read_unsigned_char endian bs0 >>= fun (st_info, bs0) -> + read_unsigned_char endian bs0 >>= fun (st_other, bs0) -> + read_elf32_half endian bs0 >>= fun (st_shndx, bs0) -> + return (<| elf32_st_name = st_name; elf32_st_value = st_value; + elf32_st_size = st_size; elf32_st_info = st_info; + elf32_st_other = st_other; elf32_st_shndx = st_shndx |>, bs0) + +val read_elf32_symbol_table : endianness -> bitstring -> error elf32_symbol_table +let rec read_elf32_symbol_table endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf32_symbol_table_entry endian bs0 >>= fun (head, bs0) -> + read_elf32_symbol_table endian bs0 >>= fun tail -> + return (head::tail) + +(** ELF64 symbol table type *) + +type elf64_symbol_table_entry = + <| elf64_st_name : elf64_word + ; elf64_st_info : unsigned_char + ; elf64_st_other : unsigned_char + ; elf64_st_shndx : elf64_half + ; elf64_st_value : elf64_addr + ; elf64_st_size : elf64_xword + |> + +val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string +let string_of_elf64_symbol_table_entry entry = + unlines [ + "\t" ^ "Name: " ^ show entry.elf64_st_name + ; "\t" ^ "Info: " ^ show entry.elf64_st_info + ; "\t" ^ "Other: " ^ show entry.elf64_st_other + ; "\t" ^ "Shndx: " ^ show entry.elf64_st_shndx + ; "\t" ^ "Value: " ^ show entry.elf64_st_value + ; "\t" ^ "Size: " ^ show entry.elf64_st_size + ] + +type elf64_symbol_table = list elf64_symbol_table_entry + +val string_of_elf64_symbol_table : elf64_symbol_table -> string +let string_of_elf64_symbol_table symtab = + unlines (List.map string_of_elf64_symbol_table_entry symtab) + +class (HasElf64SymbolTable 'a) + val get_elf64_symbol_table : 'a -> elf64_symbol_table +end + +val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring) +let read_elf64_symbol_table_entry endian bs0 = + read_elf64_word endian bs0 >>= fun (st_name, bs0) -> + read_unsigned_char endian bs0 >>= fun (st_info, bs0) -> + read_unsigned_char endian bs0 >>= fun (st_other, bs0) -> + read_elf64_half endian bs0 >>= fun (st_shndx, bs0) -> + read_elf64_addr endian bs0 >>= fun (st_value, bs0) -> + read_elf64_xword endian bs0 >>= fun (st_size, bs0) -> + return (<| elf64_st_name = st_name; elf64_st_info = st_info; + elf64_st_other = st_other; elf64_st_shndx = st_shndx; + elf64_st_value = st_value; elf64_st_size = st_size |>, bs0) + +val read_elf64_symbol_table : endianness -> bitstring -> error elf64_symbol_table +let rec read_elf64_symbol_table endian bs0 = + if length bs0 = 0 then + return [] + else + read_elf64_symbol_table_entry endian bs0 >>= fun (head, bs0) -> + read_elf64_symbol_table endian bs0 >>= fun tail -> + return (head::tail) + +val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> error (list (string * nat)) +let get_elf32_symbol_image_address symtab strtab = + mapM (fun entry -> + let name = nat_of_elf32_word entry.elf32_st_name in + let addr = nat_of_elf32_addr entry.elf32_st_value in + String_table.get_string_at name strtab >>= fun str -> + return (str, addr) + ) symtab + +val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> error (list (string * nat)) +let get_elf64_symbol_image_address symtab strtab = + mapM (fun entry -> + let name = nat_of_elf64_word entry.elf64_st_name in + let addr = nat_of_elf64_addr entry.elf64_st_value in + String_table.get_string_at name strtab >>= fun str -> + return (str, addr) + ) symtab
\ No newline at end of file diff --git a/src/elf_model/elf_symbol_table.ml b/src/elf_model/elf_symbol_table.ml index a2fed159..369629b0 100644 --- a/src/elf_model/elf_symbol_table.ml +++ b/src/elf_model/elf_symbol_table.ml @@ -2,245 +2,249 @@ open Lem_basic_classes open Lem_bool open Lem_list -open Lem_num +open Lem_maybe open Lem_string +open Lem_tuple -open Bitstring -open Elf_section_header -open Elf_types +open Bitstring_local open Error +open Missing_pervasives open Show -(** Symbol table indices *) +open Elf_types +open Endianness +open String_table + +(** Undefined symbol index *) -(** 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. - *) +(** Symbol binding *) + 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. *) +(*val string_of_symbol_binding : nat -> (nat -> string) -> (nat -> string) -> string*) +let string_of_symbol_binding m os proc = +(if m = stb_local then + "STB_LOCAL" + else if m = stb_global then + "STB_GLOBAL" + else if m = stb_weak then + "STB_WEAK" + else if (m >= stb_loos) && (m <= stb_hios) then + os m + else if (m >= stb_loproc) && (m <= stb_hiproc) then + proc m + else + "Invalid symbol binding") + +(** 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. - *) +(*val string_of_symbol_type : nat -> (nat -> string) -> (nat -> string) -> string*) +let string_of_symbol_type m os proc = +(if m = stt_notype then + "STT_NOTYPE" + else if m = stt_object then + "STT_OBJECT" + else if m = stt_func then + "STT_FUNC" + else if m = stt_section then + "STT_SECTION" + else if m = stt_file then + "STT_FILE" + else if m = stt_common then + "STT_COMMON" + else if m = stt_tls then + "STT_TLS" + else if (m >= stt_loos) && (m <= stt_hios) then + os m + else if (m >= stt_loproc) && (m <= stt_hiproc) then + proc m + else + "Invalid symbol type") + +(** Symbol visibility *) + 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. *) +(*val string_of_symbol_visibility : nat -> string*) +let string_of_symbol_visibility m = +(if m = stv_default then + "STV_DEFAULT" + else if m = stv_internal then + "STV_INTERNAL" + else if m = stv_hidden then + "STV_HIDDEN" + else if m = stv_protected then + "STV_PROTECTED" + else + "Invalid symbol visibility") + +(** ELF32 symbol table 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 + { elf32_st_name : Uint32.t + ; elf32_st_value : Uint32.t + ; elf32_st_size : Uint32.t + ; elf32_st_info : Uint32.t + ; elf32_st_other : Uint32.t + ; elf32_st_shndx : Uint32.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))) - )) + +(** Extraction of symbol table data *) + +(* Functions below common to 32- and 64-bit! *) + +(*val get_symbol_binding : unsigned_char -> nat*) +let get_symbol_binding entry = +(Uint32.to_int (Uint32.shift_right entry( 4))) + +(*val get_symbol_type : unsigned_char -> nat*) +let get_symbol_type entry = +(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 15)))) (* 0xf *) + +(*val get_symbol_info : unsigned_char -> unsigned_char -> nat*) +let get_symbol_info entry0 entry1 = +(Uint32.to_int (Uint32.add + (Uint32.shift_left entry0( 4)) (Uint32.logand entry1 + (Uint32.of_int( 15))))) (*0xf*) + +(*val get_symbol_visibility : unsigned_char -> nat*) +let get_symbol_visibility entry = +(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 3)))) (* 0x3*) + +type symtab_print_bundle = (int -> string) * (int -> string) + +(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*) +let string_of_elf32_symbol_table_entry entry = +(unlines [ +("\t" ^ ("Name: " ^ Uint32.to_string entry.elf32_st_name)) + ; ("\t" ^ ("Value: " ^ Uint32.to_string entry.elf32_st_value)) + ; ("\t" ^ ("Size: " ^ Uint32.to_string entry.elf32_st_size)) + ; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf32_st_info)) + ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf32_st_other)) + ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf32_st_shndx)) + ]) 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) "")) +(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*) +let string_of_elf32_symbol_table symtab = +(unlines (List.map string_of_elf32_symbol_table_entry symtab)) + +type 'a hasElf32SymbolTable_class={ + get_elf32_symbol_table_method : 'a -> elf32_symbol_table +} + +(*val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)*) +let read_elf32_symbol_table_entry endian bs0 = +(Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_name, bs0) -> + Ml_bindings.read_elf32_addr endian bs0 >>= (fun (st_value, bs0) -> + Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_size, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> + Ml_bindings.read_elf32_half endian bs0 >>= (fun (st_shndx, bs0) -> + return ({ elf32_st_name = st_name; elf32_st_value = st_value; + elf32_st_size = st_size; elf32_st_info = st_info; + elf32_st_other = st_other; elf32_st_shndx = st_shndx }, bs0)))))))) + +(*val read_elf32_symbol_table : endianness -> bitstring -> error elf32_symbol_table*) +let rec read_elf32_symbol_table endian bs0 = +(if Bitstring.bitstring_length bs0 = 0 then + return [] + else + read_elf32_symbol_table_entry endian bs0 >>= (fun (head, bs0) -> + read_elf32_symbol_table endian bs0 >>= (fun tail -> + return (head::tail)))) + +(** ELF64 symbol table type *) + +type elf64_symbol_table_entry = + { elf64_st_name : Uint32.t + ; elf64_st_info : Uint32.t + ; elf64_st_other : Uint32.t + ; elf64_st_shndx : Uint32.t + ; elf64_st_value : Uint64.t + ; elf64_st_size : Uint64.t + } + +(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*) +let string_of_elf64_symbol_table_entry entry = +(unlines [ +("\t" ^ ("Name: " ^ Uint32.to_string entry.elf64_st_name)) + ; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf64_st_info)) + ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf64_st_other)) + ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf64_st_shndx)) + ; ("\t" ^ ("Value: " ^ Uint64.to_string entry.elf64_st_value)) + ; ("\t" ^ ("Size: " ^ Uint64.to_string entry.elf64_st_size)) + ]) + +type elf64_symbol_table = elf64_symbol_table_entry list + +(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*) +let string_of_elf64_symbol_table symtab = +(unlines (List.map string_of_elf64_symbol_table_entry symtab)) + +type 'a hasElf64SymbolTable_class={ + get_elf64_symbol_table_method : 'a -> elf64_symbol_table +} + +(*val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)*) +let read_elf64_symbol_table_entry endian bs0 = +(Ml_bindings.read_elf64_word endian bs0 >>= (fun (st_name, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> + Ml_bindings.read_elf64_half endian bs0 >>= (fun (st_shndx, bs0) -> + Ml_bindings.read_elf64_addr endian bs0 >>= (fun (st_value, bs0) -> + Ml_bindings.read_elf64_xword endian bs0 >>= (fun (st_size, bs0) -> + return ({ elf64_st_name = st_name; elf64_st_info = st_info; + elf64_st_other = st_other; elf64_st_shndx = st_shndx; + elf64_st_value = st_value; elf64_st_size = st_size }, bs0)))))))) + +(*val read_elf64_symbol_table : endianness -> bitstring -> error elf64_symbol_table*) +let rec read_elf64_symbol_table endian bs0 = +(if Bitstring.bitstring_length bs0 = 0 then + return [] + else + read_elf64_symbol_table_entry endian bs0 >>= (fun (head, bs0) -> + read_elf64_symbol_table endian bs0 >>= (fun tail -> + return (head::tail)))) + +(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> error (list (string * nat))*) +let get_elf32_symbol_image_address symtab strtab = +(mapM (fun entry -> + let name = (Uint32.to_int entry.elf32_st_name) in + let addr = (Uint32.to_int entry.elf32_st_value) in + String_table.get_string_at name strtab >>= (fun str -> + return (str, addr)) + ) symtab) + +(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> error (list (string * nat))*) +let get_elf64_symbol_image_address symtab strtab = +(mapM (fun entry -> + let name = (Uint32.to_int entry.elf64_st_name) in + let addr = (Uint64.to_int entry.elf64_st_value) in + String_table.get_string_at name strtab >>= (fun str -> + return (str, addr)) + ) symtab)
\ No newline at end of file diff --git a/src/elf_model/elf_types.lem b/src/elf_model/elf_types.lem index d35a9713..ec50346f 100644 --- a/src/elf_model/elf_types.lem +++ b/src/elf_model/elf_types.lem @@ -59,7 +59,7 @@ 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_rshift = `Uint32.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` @@ -185,13 +185,17 @@ 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 elf32_word_rshift : elf32_word -> nat -> elf32_word val read_elf32_word : endianness -> bitstring -> error (elf32_word * bitstring) +val unsigned_char_of_elf32_word : elf32_word -> unsigned_char 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` +declare ocaml target_rep function elf32_word_rshift = `Uint32.shift_right` +declare ocaml target_rep function unsigned_char_of_elf32_word = `` instance (Show elf32_word) let show = string_of_elf32_word @@ -264,10 +268,16 @@ 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) +val elf64_xword_rshift : elf64_xword -> nat -> elf64_xword +val elf64_xword_land : elf64_xword -> elf64_xword -> elf64_xword +val elf64_xword_of_int64 : int64 -> elf64_xword 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` +declare ocaml target_rep function elf64_xword_rshift = `Uint64.shift_right` +declare ocaml target_rep function elf64_xword_land = `Uint64.logand` +declare ocaml target_rep function elf64_xword_of_int64 = `Uint64.of_int64` instance (Show elf64_xword) let show = string_of_elf64_xword diff --git a/src/elf_model/libraries/Makefile b/src/elf_model/libraries/Makefile new file mode 100644 index 00000000..1745dbdd --- /dev/null +++ b/src/elf_model/libraries/Makefile @@ -0,0 +1,23 @@ +dummy: all + +extract: + mkdir batteries bitstring uint + tar -zxvf batteries-2.2.tar.gz -C batteries --strip-components=1 + tar -zxvf bitstring.tar.gz -C bitstring --strip-components=1 + tar -zxvf uint.tar.gz -C uint --strip-components=1 + +clean: + rm -rf batteries bitstring uint + +make-batteries: + make -C batteries all + +make-uint: + make -C uint configure + make -C uint all + +make-bitstring: + cd bitstring && ./configure + make -C bitstring + +all: extract make-batteries make-bitstring make-uint
\ No newline at end of file diff --git a/src/elf_model/libraries/batteries-2.2.tar.gz b/src/elf_model/libraries/batteries-2.2.tar.gz Binary files differnew file mode 100644 index 00000000..d88b8c8f --- /dev/null +++ b/src/elf_model/libraries/batteries-2.2.tar.gz diff --git a/src/elf_model/libraries/bitstring.tar.gz b/src/elf_model/libraries/bitstring.tar.gz Binary files differnew file mode 100644 index 00000000..42a2c19f --- /dev/null +++ b/src/elf_model/libraries/bitstring.tar.gz diff --git a/src/elf_model/libraries/uint.tar.gz b/src/elf_model/libraries/uint.tar.gz Binary files differnew file mode 100644 index 00000000..21a3a379 --- /dev/null +++ b/src/elf_model/libraries/uint.tar.gz diff --git a/src/elf_model/main.lem b/src/elf_model/main.lem index a7e7a709..501657cc 100644 --- a/src/elf_model/main.lem +++ b/src/elf_model/main.lem @@ -3,6 +3,7 @@ open import String open import Tuple open import Bitstring +open import Default_printing open import Error open import Missing_pervasives open import Show @@ -11,31 +12,31 @@ 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 Elf_linking_file2 +open import Elf_linking_file3 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) + (default_os_specific_print, default_proc_specific_print) let default_pht_bdl = - (default_os, default_proc) + (default_os_specific_print, default_proc_specific_print) let default_sht_bdl = - (default_os, default_proc, default_user) + (default_os_specific_print, default_proc_specific_print, default_user_specific_print) 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 + let res = + Bitstring.acquire "test/power64-executable-2" >>= fun bs0 -> + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf64_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf64_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= fun strs -> + let _ = Missing_pervasives.print (show strs) in + return f1 + in + match res with + | Fail err -> Missing_pervasives.print ("[!]: " ^ err) + | Success _ -> Missing_pervasives.print "Success..." + end diff --git a/src/elf_model/missing_pervasives.lem b/src/elf_model/missing_pervasives.lem index 308c43c3..e0b493fe 100644 --- a/src/elf_model/missing_pervasives.lem +++ b/src/elf_model/missing_pervasives.lem @@ -14,6 +14,27 @@ let rec intercalate sep xs = | x::xs -> x::sep::intercalate sep xs end +(** [mapMaybei f xs] maps a function expecting an index (the position in the list + * [xs] that it is currently viewing) and producing a [maybe] type across a list. + * Elements that produce [Nothing] under [f] are discarded in the output, whilst + * those producing [Just e] for some [e] are kept. + *) +val mapMaybei' : forall 'a 'b. (nat -> 'a -> maybe 'b) -> nat -> list 'a -> list 'b +let rec mapMaybei' f idx xs = + match xs with + | [] -> [] + | x::xs -> + match f idx x with + | Nothing -> mapMaybei' f (1 + idx) xs + | Just e -> e :: mapMaybei' f (1 + idx) xs + end + end + +val mapMaybei : forall 'a 'b. (nat -> 'a -> maybe 'b) -> list 'a -> list 'b + +let mapMaybei f xs = + mapMaybei' f 0 xs + (** [unlines xs] concatenates a list of strings [xs], placing each entry * on a new line. *) @@ -52,4 +73,4 @@ declare ocaml target_rep function string_of_nat = `string_of_int` * 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 +declare ocaml target_rep function string_suffix = `Ml_bindings.string_suffix` diff --git a/src/elf_model/ml_bindings.ml b/src/elf_model/ml_bindings.ml index 0dd4d152..c2923c2e 100644 --- a/src/elf_model/ml_bindings.ml +++ b/src/elf_model/ml_bindings.ml @@ -1,323 +1,1274 @@ open Endianness + open Error - -let decimal_string_of_int64 e = - let i = Int64.to_int e in - string_of_int i -;; - + +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 i = Int64.to_int e in Printf.sprintf "0x%x" i + let partition_bitstring size bitstring = - Bitstring.takebits size bitstring, Bitstring.dropbits 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) - + 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 (__pabitstring_data_1001, __pabitstring_original_off_1004, + __pabitstring_original_len_1005) = + bs in + let __pabitstring_off_1002 = __pabitstring_original_off_1004 + and __pabitstring_len_1003 = __pabitstring_original_len_1005 in + let __pabitstring_off_aligned_1006 = (__pabitstring_off_1002 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1006; + let __pabitstring_result_1007 = ref None + in + ((try + (if __pabitstring_len_1003 >= 8 + then + (let v = + if __pabitstring_off_aligned_1006 + then + (let o = (__pabitstring_original_off_1004 lsr 3) + 0 + in + Char.code (String.unsafe_get __pabitstring_data_1001 o)) + else + Bitstring.extract_char_unsigned __pabitstring_data_1001 + __pabitstring_off_1002 __pabitstring_len_1003 8 in + let __pabitstring_off_1002 = __pabitstring_off_1002 + 8 + and __pabitstring_len_1003 = __pabitstring_len_1003 - 8 + in + match v with + | unsigned when true -> + (__pabitstring_result_1007 := + Some (return ((Uint32.of_int unsigned), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1007 := Some (Fail "read_unsigned_char_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1007 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 28, 2)))) + 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 (__pabitstring_data_1008, __pabitstring_original_off_1011, + __pabitstring_original_len_1012) = + bs in + let __pabitstring_off_1009 = __pabitstring_original_off_1011 + and __pabitstring_len_1010 = __pabitstring_original_len_1012 in + let __pabitstring_off_aligned_1013 = (__pabitstring_off_1009 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1013; + let __pabitstring_result_1014 = ref None + in + ((try + (if __pabitstring_len_1010 >= 8 + then + (let v = + if __pabitstring_off_aligned_1013 + then + (let o = (__pabitstring_original_off_1011 lsr 3) + 0 + in + Char.code (String.unsafe_get __pabitstring_data_1008 o)) + else + Bitstring.extract_char_unsigned __pabitstring_data_1008 + __pabitstring_off_1009 __pabitstring_len_1010 8 in + let __pabitstring_off_1009 = __pabitstring_off_1009 + 8 + and __pabitstring_len_1010 = __pabitstring_len_1010 - 8 + in + match v with + | unsigned when true -> + (__pabitstring_result_1014 := + Some (return ((Uint32.of_int unsigned), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1014 := Some (Fail "read_unsigned_char_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1014 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 34, 2)))) + let read_unsigned_char endian bs = - let cut, rest = partition_bitstring 8 bs in + 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 -;; - + | 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 (__pabitstring_data_1015, __pabitstring_original_off_1018, + __pabitstring_original_len_1019) = + bs in + let __pabitstring_off_1016 = __pabitstring_original_off_1018 + and __pabitstring_len_1017 = __pabitstring_original_len_1019 in + let __pabitstring_off_aligned_1020 = (__pabitstring_off_1016 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1020; + let __pabitstring_result_1021 = ref None + in + ((try + (if __pabitstring_len_1017 >= 32 + then + (let v = + if __pabitstring_off_aligned_1020 + then + (let o = (__pabitstring_original_off_1018 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1015 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1015 __pabitstring_off_1016 + __pabitstring_len_1017 32 in + let __pabitstring_off_1016 = __pabitstring_off_1016 + 32 + and __pabitstring_len_1017 = __pabitstring_len_1017 - 32 + in + match v with + | addr when true -> + (__pabitstring_result_1021 := + Some (return ((Uint32.of_int32 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1021 := Some (Fail "read_elf32_addr_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1021 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 52, 2)))) + 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 (__pabitstring_data_1022, __pabitstring_original_off_1025, + __pabitstring_original_len_1026) = + bs in + let __pabitstring_off_1023 = __pabitstring_original_off_1025 + and __pabitstring_len_1024 = __pabitstring_original_len_1026 in + let __pabitstring_off_aligned_1027 = (__pabitstring_off_1023 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1027; + let __pabitstring_result_1028 = ref None + in + ((try + (if __pabitstring_len_1024 >= 32 + then + (let v = + if __pabitstring_off_aligned_1027 + then + (let o = (__pabitstring_original_off_1025 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1022 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1022 __pabitstring_off_1023 + __pabitstring_len_1024 32 in + let __pabitstring_off_1023 = __pabitstring_off_1023 + 32 + and __pabitstring_len_1024 = __pabitstring_len_1024 - 32 + in + match v with + | addr when true -> + (__pabitstring_result_1028 := + Some (return ((Uint32.of_int32 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1028 := Some (Fail "read_elf32_addr_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1028 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 58, 2)))) + 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 (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 (__pabitstring_data_1029, __pabitstring_original_off_1032, + __pabitstring_original_len_1033) = + bs in + let __pabitstring_off_1030 = __pabitstring_original_off_1032 + and __pabitstring_len_1031 = __pabitstring_original_len_1033 in + let __pabitstring_off_aligned_1034 = (__pabitstring_off_1030 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1034; + let __pabitstring_result_1035 = ref None + in + ((try + (if __pabitstring_len_1031 >= 64 + then + (let v = + if __pabitstring_off_aligned_1034 + then + (let o = (__pabitstring_original_off_1032 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_le_unsigned + __pabitstring_data_1029 o zero) + else + Bitstring.extract_int64_le_unsigned + __pabitstring_data_1029 __pabitstring_off_1030 + __pabitstring_len_1031 64 in + let __pabitstring_off_1030 = __pabitstring_off_1030 + 64 + and __pabitstring_len_1031 = __pabitstring_len_1031 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1035 := + Some (return ((Uint64.of_int64 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1035 := Some (Fail "read_elf64_addr_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1035 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 71, 2)))) + 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 (__pabitstring_data_1036, __pabitstring_original_off_1039, + __pabitstring_original_len_1040) = + bs in + let __pabitstring_off_1037 = __pabitstring_original_off_1039 + and __pabitstring_len_1038 = __pabitstring_original_len_1040 in + let __pabitstring_off_aligned_1041 = (__pabitstring_off_1037 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1041; + let __pabitstring_result_1042 = ref None + in + ((try + (if __pabitstring_len_1038 >= 64 + then + (let v = + if __pabitstring_off_aligned_1041 + then + (let o = (__pabitstring_original_off_1039 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_be_unsigned + __pabitstring_data_1036 o zero) + else + Bitstring.extract_int64_be_unsigned + __pabitstring_data_1036 __pabitstring_off_1037 + __pabitstring_len_1038 64 in + let __pabitstring_off_1037 = __pabitstring_off_1037 + 64 + and __pabitstring_len_1038 = __pabitstring_len_1038 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1042 := + Some (return ((Uint64.of_int64 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1042 := Some (Fail "read_elf64_addr_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1042 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 77, 2)))) + let read_elf64_addr endian bs = - let cut, rest = partition_bitstring 64 bs in + 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 -;; - + | 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 (__pabitstring_data_1043, __pabitstring_original_off_1046, + __pabitstring_original_len_1047) = + bs in + let __pabitstring_off_1044 = __pabitstring_original_off_1046 + and __pabitstring_len_1045 = __pabitstring_original_len_1047 in + let __pabitstring_off_aligned_1048 = (__pabitstring_off_1044 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1048; + let __pabitstring_result_1049 = ref None + in + ((try + (if __pabitstring_len_1045 >= 32 + then + (let v = + if __pabitstring_off_aligned_1048 + then + (let o = (__pabitstring_original_off_1046 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1043 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1043 __pabitstring_off_1044 + __pabitstring_len_1045 32 in + let __pabitstring_off_1044 = __pabitstring_off_1044 + 32 + and __pabitstring_len_1045 = __pabitstring_len_1045 - 32 + in + match v with + | off when true -> + (__pabitstring_result_1049 := + Some (return ((Uint32.of_int32 off), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1049 := Some (Fail "read_elf32_off_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1049 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 94, 2)))) + 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 (__pabitstring_data_1050, __pabitstring_original_off_1053, + __pabitstring_original_len_1054) = + bs in + let __pabitstring_off_1051 = __pabitstring_original_off_1053 + and __pabitstring_len_1052 = __pabitstring_original_len_1054 in + let __pabitstring_off_aligned_1055 = (__pabitstring_off_1051 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1055; + let __pabitstring_result_1056 = ref None + in + ((try + (if __pabitstring_len_1052 >= 32 + then + (let v = + if __pabitstring_off_aligned_1055 + then + (let o = (__pabitstring_original_off_1053 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1050 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1050 __pabitstring_off_1051 + __pabitstring_len_1052 32 in + let __pabitstring_off_1051 = __pabitstring_off_1051 + 32 + and __pabitstring_len_1052 = __pabitstring_len_1052 - 32 + in + match v with + | off when true -> + (__pabitstring_result_1056 := + Some (return ((Uint32.of_int32 off), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1056 := Some (Fail "read_elf32_off_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1056 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 100, 2)))) + let read_elf32_off endian bs = - let cut, rest = partition_bitstring 32 bs in + 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 -;; - + | 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 (__pabitstring_data_1057, __pabitstring_original_off_1060, + __pabitstring_original_len_1061) = + bs in + let __pabitstring_off_1058 = __pabitstring_original_off_1060 + and __pabitstring_len_1059 = __pabitstring_original_len_1061 in + let __pabitstring_off_aligned_1062 = (__pabitstring_off_1058 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1062; + let __pabitstring_result_1063 = ref None + in + ((try + (if __pabitstring_len_1059 >= 64 + then + (let v = + if __pabitstring_off_aligned_1062 + then + (let o = (__pabitstring_original_off_1060 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_le_unsigned + __pabitstring_data_1057 o zero) + else + Bitstring.extract_int64_le_unsigned + __pabitstring_data_1057 __pabitstring_off_1058 + __pabitstring_len_1059 64 in + let __pabitstring_off_1058 = __pabitstring_off_1058 + 64 + and __pabitstring_len_1059 = __pabitstring_len_1059 - 64 + in + match v with + | off when true -> + (__pabitstring_result_1063 := + Some (return ((Uint64.of_int64 off), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1063 := Some (Fail "read_elf64_off_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1063 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 113, 2)))) + 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 (__pabitstring_data_1064, __pabitstring_original_off_1067, + __pabitstring_original_len_1068) = + bs in + let __pabitstring_off_1065 = __pabitstring_original_off_1067 + and __pabitstring_len_1066 = __pabitstring_original_len_1068 in + let __pabitstring_off_aligned_1069 = (__pabitstring_off_1065 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1069; + let __pabitstring_result_1070 = ref None + in + ((try + (if __pabitstring_len_1066 >= 64 + then + (let v = + if __pabitstring_off_aligned_1069 + then + (let o = (__pabitstring_original_off_1067 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_be_unsigned + __pabitstring_data_1064 o zero) + else + Bitstring.extract_int64_be_unsigned + __pabitstring_data_1064 __pabitstring_off_1065 + __pabitstring_len_1066 64 in + let __pabitstring_off_1065 = __pabitstring_off_1065 + 64 + and __pabitstring_len_1066 = __pabitstring_len_1066 - 64 + in + match v with + | off when true -> + (__pabitstring_result_1070 := + Some (return ((Uint64.of_int64 off), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1070 := Some (Fail "read_elf64_off_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1070 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 119, 2)))) + let read_elf64_off endian bs = - let cut, rest = partition_bitstring 64 bs in + 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 -;; - + | 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 (__pabitstring_data_1071, __pabitstring_original_off_1074, + __pabitstring_original_len_1075) = + bs in + let __pabitstring_off_1072 = __pabitstring_original_off_1074 + and __pabitstring_len_1073 = __pabitstring_original_len_1075 in + let __pabitstring_off_aligned_1076 = (__pabitstring_off_1072 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1076; + let __pabitstring_result_1077 = ref None + in + ((try + (if __pabitstring_len_1073 >= 16 + then + (let v = + if __pabitstring_off_aligned_1076 + then + (let o = (__pabitstring_original_off_1074 lsr 3) + 0 + in + Bitstring.extract_fastpath_int16_le_unsigned + __pabitstring_data_1071 o) + else + Bitstring.extract_int_le_unsigned __pabitstring_data_1071 + __pabitstring_off_1072 __pabitstring_len_1073 16 in + let __pabitstring_off_1072 = __pabitstring_off_1072 + 16 + and __pabitstring_len_1073 = __pabitstring_len_1073 - 16 + in + match v with + | half when true -> + (__pabitstring_result_1077 := + Some (return ((Uint32.of_int half), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1077 := Some (Fail "read_elf32_half_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1077 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 137, 2)))) + 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 (__pabitstring_data_1078, __pabitstring_original_off_1081, + __pabitstring_original_len_1082) = + bs in + let __pabitstring_off_1079 = __pabitstring_original_off_1081 + and __pabitstring_len_1080 = __pabitstring_original_len_1082 in + let __pabitstring_off_aligned_1083 = (__pabitstring_off_1079 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1083; + let __pabitstring_result_1084 = ref None + in + ((try + (if __pabitstring_len_1080 >= 16 + then + (let v = + if __pabitstring_off_aligned_1083 + then + (let o = (__pabitstring_original_off_1081 lsr 3) + 0 + in + Bitstring.extract_fastpath_int16_be_unsigned + __pabitstring_data_1078 o) + else + Bitstring.extract_int_be_unsigned __pabitstring_data_1078 + __pabitstring_off_1079 __pabitstring_len_1080 16 in + let __pabitstring_off_1079 = __pabitstring_off_1079 + 16 + and __pabitstring_len_1080 = __pabitstring_len_1080 - 16 + in + match v with + | half when true -> + (__pabitstring_result_1084 := + Some (return ((Uint32.of_int half), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1084 := Some (Fail "read_elf32_half_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1084 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 143, 2)))) + let read_elf32_half endian bs = - let cut, rest = partition_bitstring 16 bs in + 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 -;; - + | 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 (__pabitstring_data_1085, __pabitstring_original_off_1088, + __pabitstring_original_len_1089) = + bs in + let __pabitstring_off_1086 = __pabitstring_original_off_1088 + and __pabitstring_len_1087 = __pabitstring_original_len_1089 in + let __pabitstring_off_aligned_1090 = (__pabitstring_off_1086 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1090; + let __pabitstring_result_1091 = ref None + in + ((try + (if __pabitstring_len_1087 >= 16 + then + (let v = + if __pabitstring_off_aligned_1090 + then + (let o = (__pabitstring_original_off_1088 lsr 3) + 0 + in + Bitstring.extract_fastpath_int16_le_unsigned + __pabitstring_data_1085 o) + else + Bitstring.extract_int_le_unsigned __pabitstring_data_1085 + __pabitstring_off_1086 __pabitstring_len_1087 16 in + let __pabitstring_off_1086 = __pabitstring_off_1086 + 16 + and __pabitstring_len_1087 = __pabitstring_len_1087 - 16 + in + match v with + | half when true -> + (__pabitstring_result_1091 := + Some (return ((Uint32.of_int half), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1091 := Some (Fail "read_elf64_half_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1091 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 156, 2)))) + 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 (__pabitstring_data_1092, __pabitstring_original_off_1095, + __pabitstring_original_len_1096) = + bs in + let __pabitstring_off_1093 = __pabitstring_original_off_1095 + and __pabitstring_len_1094 = __pabitstring_original_len_1096 in + let __pabitstring_off_aligned_1097 = (__pabitstring_off_1093 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1097; + let __pabitstring_result_1098 = ref None + in + ((try + (if __pabitstring_len_1094 >= 16 + then + (let v = + if __pabitstring_off_aligned_1097 + then + (let o = (__pabitstring_original_off_1095 lsr 3) + 0 + in + Bitstring.extract_fastpath_int16_be_unsigned + __pabitstring_data_1092 o) + else + Bitstring.extract_int_be_unsigned __pabitstring_data_1092 + __pabitstring_off_1093 __pabitstring_len_1094 16 in + let __pabitstring_off_1093 = __pabitstring_off_1093 + 16 + and __pabitstring_len_1094 = __pabitstring_len_1094 - 16 + in + match v with + | half when true -> + (__pabitstring_result_1098 := + Some (return ((Uint32.of_int half), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1098 := Some (Fail "read_elf64_half_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1098 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 162, 2)))) + let read_elf64_half endian bs = - let cut, rest = partition_bitstring 16 bs in + 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 -;; - + | 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 (__pabitstring_data_1099, __pabitstring_original_off_1102, + __pabitstring_original_len_1103) = + bs in + let __pabitstring_off_1100 = __pabitstring_original_off_1102 + and __pabitstring_len_1101 = __pabitstring_original_len_1103 in + let __pabitstring_off_aligned_1104 = (__pabitstring_off_1100 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1104; + let __pabitstring_result_1105 = ref None + in + ((try + (if __pabitstring_len_1101 >= 32 + then + (let v = + if __pabitstring_off_aligned_1104 + then + (let o = (__pabitstring_original_off_1102 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1099 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1099 __pabitstring_off_1100 + __pabitstring_len_1101 32 in + let __pabitstring_off_1100 = __pabitstring_off_1100 + 32 + and __pabitstring_len_1101 = __pabitstring_len_1101 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1105 := + Some (return ((Uint32.of_int32 word), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1105 := Some (Fail "read_elf32_word_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1105 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 180, 2)))) + 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 (__pabitstring_data_1106, __pabitstring_original_off_1109, + __pabitstring_original_len_1110) = + bs in + let __pabitstring_off_1107 = __pabitstring_original_off_1109 + and __pabitstring_len_1108 = __pabitstring_original_len_1110 in + let __pabitstring_off_aligned_1111 = (__pabitstring_off_1107 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1111; + let __pabitstring_result_1112 = ref None + in + ((try + (if __pabitstring_len_1108 >= 32 + then + (let v = + if __pabitstring_off_aligned_1111 + then + (let o = (__pabitstring_original_off_1109 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1106 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1106 __pabitstring_off_1107 + __pabitstring_len_1108 32 in + let __pabitstring_off_1107 = __pabitstring_off_1107 + 32 + and __pabitstring_len_1108 = __pabitstring_len_1108 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1112 := + Some (return ((Uint32.of_int32 word), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1112 := Some (Fail "read_elf32_word_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1112 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 186, 2)))) + let read_elf32_word endian bs = - let cut, rest = partition_bitstring 32 bs in + 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 -;; - + | 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 (__pabitstring_data_1113, __pabitstring_original_off_1116, + __pabitstring_original_len_1117) = + bs in + let __pabitstring_off_1114 = __pabitstring_original_off_1116 + and __pabitstring_len_1115 = __pabitstring_original_len_1117 in + let __pabitstring_off_aligned_1118 = (__pabitstring_off_1114 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1118; + let __pabitstring_result_1119 = ref None + in + ((try + (if __pabitstring_len_1115 >= 32 + then + (let v = + if __pabitstring_off_aligned_1118 + then + (let o = (__pabitstring_original_off_1116 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1113 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1113 __pabitstring_off_1114 + __pabitstring_len_1115 32 in + let __pabitstring_off_1114 = __pabitstring_off_1114 + 32 + and __pabitstring_len_1115 = __pabitstring_len_1115 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1119 := + Some (return ((Uint32.of_int32 word), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1119 := Some (Fail "read_elf64_word_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1119 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 199, 2)))) + 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 (__pabitstring_data_1120, __pabitstring_original_off_1123, + __pabitstring_original_len_1124) = + bs in + let __pabitstring_off_1121 = __pabitstring_original_off_1123 + and __pabitstring_len_1122 = __pabitstring_original_len_1124 in + let __pabitstring_off_aligned_1125 = (__pabitstring_off_1121 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1125; + let __pabitstring_result_1126 = ref None + in + ((try + (if __pabitstring_len_1122 >= 32 + then + (let v = + if __pabitstring_off_aligned_1125 + then + (let o = (__pabitstring_original_off_1123 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1120 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1120 __pabitstring_off_1121 + __pabitstring_len_1122 32 in + let __pabitstring_off_1121 = __pabitstring_off_1121 + 32 + and __pabitstring_len_1122 = __pabitstring_len_1122 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1126 := + Some (return ((Uint32.of_int32 word), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1126 := Some (Fail "read_elf64_word_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1126 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 205, 2)))) + let read_elf64_word endian bs = - let cut, rest = partition_bitstring 32 bs in + 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 -;; - + | 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 (__pabitstring_data_1127, __pabitstring_original_off_1130, + __pabitstring_original_len_1131) = + bs in + let __pabitstring_off_1128 = __pabitstring_original_off_1130 + and __pabitstring_len_1129 = __pabitstring_original_len_1131 in + let __pabitstring_off_aligned_1132 = (__pabitstring_off_1128 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1132; + let __pabitstring_result_1133 = ref None + in + ((try + (if __pabitstring_len_1129 >= 32 + then + (let v = + if __pabitstring_off_aligned_1132 + then + (let o = (__pabitstring_original_off_1130 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1127 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1127 __pabitstring_off_1128 + __pabitstring_len_1129 32 in + let __pabitstring_off_1128 = __pabitstring_off_1128 + 32 + and __pabitstring_len_1129 = __pabitstring_len_1129 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1133 := Some (return (word, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1133 := Some (Fail "read_elf32_sword_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1133 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 223, 2)))) + let read_elf32_sword_be bs rest = - bitmatch bs with - | { word : 32 : bigendian } -> return (word, rest) - | { _ } -> Fail "read_elf32_sword_be" -;; - + let (__pabitstring_data_1134, __pabitstring_original_off_1137, + __pabitstring_original_len_1138) = + bs in + let __pabitstring_off_1135 = __pabitstring_original_off_1137 + and __pabitstring_len_1136 = __pabitstring_original_len_1138 in + let __pabitstring_off_aligned_1139 = (__pabitstring_off_1135 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1139; + let __pabitstring_result_1140 = ref None + in + ((try + (if __pabitstring_len_1136 >= 32 + then + (let v = + if __pabitstring_off_aligned_1139 + then + (let o = (__pabitstring_original_off_1137 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1134 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1134 __pabitstring_off_1135 + __pabitstring_len_1136 32 in + let __pabitstring_off_1135 = __pabitstring_off_1135 + 32 + and __pabitstring_len_1136 = __pabitstring_len_1136 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1140 := Some (return (word, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1140 := Some (Fail "read_elf32_sword_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1140 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 229, 2)))) + let read_elf32_sword endian bs = - let cut, rest = partition_bitstring 32 bs in + 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 -;; - + | 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 (__pabitstring_data_1141, __pabitstring_original_off_1144, + __pabitstring_original_len_1145) = + bs in + let __pabitstring_off_1142 = __pabitstring_original_off_1144 + and __pabitstring_len_1143 = __pabitstring_original_len_1145 in + let __pabitstring_off_aligned_1146 = (__pabitstring_off_1142 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1146; + let __pabitstring_result_1147 = ref None + in + ((try + (if __pabitstring_len_1143 >= 32 + then + (let v = + if __pabitstring_off_aligned_1146 + then + (let o = (__pabitstring_original_off_1144 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_le_unsigned + __pabitstring_data_1141 o zero) + else + Bitstring.extract_int32_le_unsigned + __pabitstring_data_1141 __pabitstring_off_1142 + __pabitstring_len_1143 32 in + let __pabitstring_off_1142 = __pabitstring_off_1142 + 32 + and __pabitstring_len_1143 = __pabitstring_len_1143 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1147 := Some (return (word, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1147 := Some (Fail "read_elf64_sword_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1147 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 242, 2)))) + let read_elf64_sword_be bs rest = - bitmatch bs with - | { word : 32 : bigendian } -> return (word, rest) - | { _ } -> Fail "read_elf64_sword_be" -;; - + let (__pabitstring_data_1148, __pabitstring_original_off_1151, + __pabitstring_original_len_1152) = + bs in + let __pabitstring_off_1149 = __pabitstring_original_off_1151 + and __pabitstring_len_1150 = __pabitstring_original_len_1152 in + let __pabitstring_off_aligned_1153 = (__pabitstring_off_1149 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1153; + let __pabitstring_result_1154 = ref None + in + ((try + (if __pabitstring_len_1150 >= 32 + then + (let v = + if __pabitstring_off_aligned_1153 + then + (let o = (__pabitstring_original_off_1151 lsr 3) + 0 in + let zero = Int32.of_int 0 + in + Bitstring.extract_fastpath_int32_be_unsigned + __pabitstring_data_1148 o zero) + else + Bitstring.extract_int32_be_unsigned + __pabitstring_data_1148 __pabitstring_off_1149 + __pabitstring_len_1150 32 in + let __pabitstring_off_1149 = __pabitstring_off_1149 + 32 + and __pabitstring_len_1150 = __pabitstring_len_1150 - 32 + in + match v with + | word when true -> + (__pabitstring_result_1154 := Some (return (word, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1154 := Some (Fail "read_elf64_sword_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1154 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 248, 2)))) + let read_elf64_sword endian bs = - let cut, rest = partition_bitstring 32 bs in + 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 -;; - + | 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 (__pabitstring_data_1155, __pabitstring_original_off_1158, + __pabitstring_original_len_1159) = + bs in + let __pabitstring_off_1156 = __pabitstring_original_off_1158 + and __pabitstring_len_1157 = __pabitstring_original_len_1159 in + let __pabitstring_off_aligned_1160 = (__pabitstring_off_1156 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1160; + let __pabitstring_result_1161 = ref None + in + ((try + (if __pabitstring_len_1157 >= 64 + then + (let v = + if __pabitstring_off_aligned_1160 + then + (let o = (__pabitstring_original_off_1158 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_le_unsigned + __pabitstring_data_1155 o zero) + else + Bitstring.extract_int64_le_unsigned + __pabitstring_data_1155 __pabitstring_off_1156 + __pabitstring_len_1157 64 in + let __pabitstring_off_1156 = __pabitstring_off_1156 + 64 + and __pabitstring_len_1157 = __pabitstring_len_1157 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1161 := + Some (return ((Uint64.of_int64 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1161 := Some (Fail "read_elf64_xword_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1161 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 265, 2)))) + 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 (__pabitstring_data_1162, __pabitstring_original_off_1165, + __pabitstring_original_len_1166) = + bs in + let __pabitstring_off_1163 = __pabitstring_original_off_1165 + and __pabitstring_len_1164 = __pabitstring_original_len_1166 in + let __pabitstring_off_aligned_1167 = (__pabitstring_off_1163 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1167; + let __pabitstring_result_1168 = ref None + in + ((try + (if __pabitstring_len_1164 >= 64 + then + (let v = + if __pabitstring_off_aligned_1167 + then + (let o = (__pabitstring_original_off_1165 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_be_unsigned + __pabitstring_data_1162 o zero) + else + Bitstring.extract_int64_be_unsigned + __pabitstring_data_1162 __pabitstring_off_1163 + __pabitstring_len_1164 64 in + let __pabitstring_off_1163 = __pabitstring_off_1163 + 64 + and __pabitstring_len_1164 = __pabitstring_len_1164 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1168 := + Some (return ((Uint64.of_int64 addr), rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1168 := Some (Fail "read_elf64_xword_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1168 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 271, 2)))) + let read_elf64_xword endian bs = - let cut, rest = partition_bitstring 64 bs in + 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 -;; - + | 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 (__pabitstring_data_1169, __pabitstring_original_off_1172, + __pabitstring_original_len_1173) = + bs in + let __pabitstring_off_1170 = __pabitstring_original_off_1172 + and __pabitstring_len_1171 = __pabitstring_original_len_1173 in + let __pabitstring_off_aligned_1174 = (__pabitstring_off_1170 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1174; + let __pabitstring_result_1175 = ref None + in + ((try + (if __pabitstring_len_1171 >= 64 + then + (let v = + if __pabitstring_off_aligned_1174 + then + (let o = (__pabitstring_original_off_1172 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_le_unsigned + __pabitstring_data_1169 o zero) + else + Bitstring.extract_int64_le_unsigned + __pabitstring_data_1169 __pabitstring_off_1170 + __pabitstring_len_1171 64 in + let __pabitstring_off_1170 = __pabitstring_off_1170 + 64 + and __pabitstring_len_1171 = __pabitstring_len_1171 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1175 := Some (return (addr, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1175 := Some (Fail "read_elf64_sxword_le"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1175 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 288, 2)))) + let read_elf64_sxword_be bs rest = - bitmatch bs with - | { addr : 64 : bigendian } -> return (addr, rest) - | { _ } -> Fail "read_elf64_sxword_be" -;; - + let (__pabitstring_data_1176, __pabitstring_original_off_1179, + __pabitstring_original_len_1180) = + bs in + let __pabitstring_off_1177 = __pabitstring_original_off_1179 + and __pabitstring_len_1178 = __pabitstring_original_len_1180 in + let __pabitstring_off_aligned_1181 = (__pabitstring_off_1177 land 7) = 0 + in + (ignore __pabitstring_off_aligned_1181; + let __pabitstring_result_1182 = ref None + in + ((try + (if __pabitstring_len_1178 >= 64 + then + (let v = + if __pabitstring_off_aligned_1181 + then + (let o = (__pabitstring_original_off_1179 lsr 3) + 0 in + let zero = Int64.of_int 0 + in + Bitstring.extract_fastpath_int64_be_unsigned + __pabitstring_data_1176 o zero) + else + Bitstring.extract_int64_be_unsigned + __pabitstring_data_1176 __pabitstring_off_1177 + __pabitstring_len_1178 64 in + let __pabitstring_off_1177 = __pabitstring_off_1177 + 64 + and __pabitstring_len_1178 = __pabitstring_len_1178 - 64 + in + match v with + | addr when true -> + (__pabitstring_result_1182 := Some (return (addr, rest)); + raise Exit) + | _ -> ()) + else (); + __pabitstring_result_1182 := Some (Fail "read_elf64_sxword_be"); + raise Exit) + with | Exit -> ()); + match !__pabitstring_result_1182 with + | Some x -> x + | None -> + raise (Match_failure ("ml_bindings_camlp4_sugared.ml", 294, 2)))) + let read_elf64_sxword endian bs = - let cut, rest = partition_bitstring 64 bs in + 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 -;; - + | 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 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 + 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 + (try Some (String.sub str index ((String.length str) - index)) + with | _ -> None) + + diff --git a/src/elf_model/ml_bindings_camlp4_sugared.ml b/src/elf_model/ml_bindings_camlp4_sugared.ml new file mode 100644 index 00000000..0dd4d152 --- /dev/null +++ b/src/elf_model/ml_bindings_camlp4_sugared.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/sail_interface.lem b/src/elf_model/sail_interface.lem index 7bfad805..6c474fa7 100644 --- a/src/elf_model/sail_interface.lem +++ b/src/elf_model/sail_interface.lem @@ -12,10 +12,14 @@ open import Missing_pervasives open import Show open import Elf_header -open import Elf_executable_file5 +open import Elf_executable_file3 open import Elf_types -val populate : string -> list (bitstring * nat) * nat +type elf_class + = ELF_Class_32 + | ELF_Class_64 + +val populate : string -> executable_process_image * elf_class let populate fname = let res = (* Acquire the data from the file... *) @@ -29,11 +33,13 @@ let populate fname = * 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 + Elf_executable_file3.read_elf32_executable_file3 bs0 >>= fun ef5 -> + Elf_executable_file3.get_elf32_executable_image ef5 >>= fun (chunks, entry) -> + return ((chunks, entry), ELF_Class_32) 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 + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun ef5 -> + Elf_executable_file3.get_elf64_executable_image ef5 >>= fun (chunks, entry) -> + return ((chunks, entry), ELF_Class_64) else fail "populate: ELF class unrecognised" end @@ -41,4 +47,74 @@ let populate fname = match res with | Fail err -> failwith err | Success chunks -> chunks + end + +val obtain_symbol_to_address_mapping : string -> list (string * nat) +let obtain_symbol_to_address_mapping 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_file3.read_elf32_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf32_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf32_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= fun strs -> + return strs + else if nat_of_unsigned_char c = Elf_header.elf_class_64 then + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf64_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf64_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= fun strs -> + return strs + else + fail "obtain_symbol_to_address_mapping: ELF class unrecognised" + end + in + match res with + | Fail err -> failwith err + | Success strs -> strs + end + +val populate_and_obtain_symbol_to_address_mapping : string -> ((executable_process_image * elf_class) * list (string * nat)) +let populate_and_obtain_symbol_to_address_mapping 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_file3.read_elf32_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf32_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf32_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= fun strs -> + Elf_executable_file3.get_elf32_executable_image f1 >>= fun (chunks, entry) -> + return (((chunks, entry), ELF_Class_32), strs) + else if nat_of_unsigned_char c = Elf_header.elf_class_64 then + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf64_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf64_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= fun strs -> + Elf_executable_file3.get_elf64_executable_image f1 >>= fun (chunks, entry) -> + return (((chunks, entry), ELF_Class_64), strs) + else + fail "populate_and_obtain_symbol_to_address_mapping: ELF class unrecognised" + end + in + match res with + | Fail err -> failwith err + | Success res -> res end
\ No newline at end of file diff --git a/src/elf_model/show.lem b/src/elf_model/show.lem index b9d45f08..95a3b648 100644 --- a/src/elf_model/show.lem +++ b/src/elf_model/show.lem @@ -4,6 +4,7 @@ open import Function open import List +open import Maybe open import Num open import String @@ -44,7 +45,7 @@ end *) val string_of_list : forall 'a. Show 'a => list 'a -> string let string_of_list l = - let result = intercalate "," (map show l) in + let result = intercalate "," (List.map show l) in let folded = foldr (^) "" result in "[" ^ folded ^ "]" @@ -52,6 +53,17 @@ instance forall 'a. Show 'a => (Show (list 'a)) let show = string_of_list end +val string_of_maybe : forall 'a. Show 'a => maybe 'a -> string +let string_of_maybe m = + match m with + | Nothing -> "Nothing" + | Just e -> "Just " ^ show e + end + +instance forall 'a. Show 'a => (Show (maybe 'a)) + let show = string_of_maybe +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 index 8cfe5056..105c5f43 100644 --- a/src/elf_model/string_table.lem +++ b/src/elf_model/string_table.lem @@ -1,3 +1,4 @@ +open import Basic_classes open import List open import Maybe open import Num @@ -40,6 +41,22 @@ let get_base_string tbl = | Strings (sep, base) -> base end +(** [concat xs] concatenates several string tables into one providing they all + * have the same delimiting character. + *) +val concat : list string_table -> error string_table +let concat xs = + match xs with + | [] -> return empty + | x::xs -> + let delim = get_delimiting_character x in + if (List.all (fun x -> get_delimiting_character x = delim) (x::xs)) then + let base = List.foldr (^) "" (List.map get_base_string (x::xs)) in + return (mk_string_table base delim) + else + fail "concat: string tables must have same delimiting characters" + end + (** [get_strings tbl] obtains the strings stored in the table, separated using * the designated separator as a delimiting character. *) diff --git a/src/test/run_power.ml b/src/test/run_power.ml index 83f6549c..96f64efe 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -277,7 +277,7 @@ let run () = end; if !eager_eval then Run_interp_model.debug := true; if !test_format then Run_interp_model.debug := false; - let (locations,start_address) = populate !file in + let ((locations,start_address),_) = populate !file in let total_size = (List.length locations) in if not(!test_format) then eprintf "Loading binary into memory (%d sections)... %!" total_size; |