Add in elf model from Dominic/Stephen. Make run_power build again. Does not effectively use elf model yet

1 files changed, 118 insertions, 0 deletions

diff --git a/src/elf_model/elf_file1.lem b/src/elf_model/elf_file1.lem
new file mode 100644
index 00000000..ff2bba61
--- /dev/null
+++ b/src/elf_model/elf_file1.lem
@@ -0,0 +1,118 @@
+open import Basic_classes
+open import String
+
+open import Endianness
+
+open import Elf_header
+open import Elf_types
+
+open import Bitstring
+open import Error
+open import Missing_pervasives
+open import Show
+
+(** Type [elf32_file1] represents the first lazy unfolding of the structure
+  * of an ELF file, wherein the ELF header is populated and all other data
+  * is left uninterpreted.
+  *)
+type elf32_file1 =
+  <| elf32_file1_header : elf32_header (** The ELF header (mandatory) *)
+   ; elf32_file1_body   : bitstring    (** Uninterpreted data *)
+   |>
+
+class (HasElf32File1 'a)
+  val get_elf32_file1 : 'a -> elf32_file1
+end
+
+instance (HasElf32File1 elf32_file1)
+  let get_elf32_file1 f1 = f1
+end
+
+instance (HasElf32Header elf32_file1)
+  let get_elf32_header file1 = file1.elf32_file1_header
+end
+
+(** Type [elf64_file1] represents the first lazy unfolding of the structure
+  * of an ELF file, wherein the ELF header is populated and all other data
+  * is left uninterpreted.
+  *)
+type elf64_file1 =
+  <| elf64_file1_header : elf64_header (** The ELF header (mandatory) *)
+   ; elf64_file1_body   : bitstring    (** Uninterpreted data *)
+   |>
+
+class (HasElf64File1 'a)
+  val get_elf64_file1 : 'a -> elf64_file1
+end
+
+instance (HasElf64File1 elf64_file1)
+  let get_elf64_file1 f1 = f1
+end
+
+instance (HasElf64Header elf64_file1)
+  let get_elf64_header file1 = file1.elf64_file1_header
+end
+
+val string_of_elf32_file1 : hdr_print_bundle -> elf32_file1 -> string
+let string_of_elf32_file1 hdr_bdl f1 =
+  unlines [
+    "\n*Type elf32_file1:"
+  ; "**Header:"
+  ; string_of_elf32_header hdr_bdl f1.elf32_file1_header
+  ; "Body:"
+  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf32_file1_body)
+  ]
+
+val string_of_elf64_file1 : hdr_print_bundle -> elf64_file1 -> string
+let string_of_elf64_file1 hdr_bdl f1 =
+  unlines [
+    "\n*Type elf64_file1:"
+  ; "**Header:"
+  ; string_of_elf64_header hdr_bdl f1.elf64_file1_header
+  ; "Body:"
+  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf64_file1_body)
+  ]
+
+(** [is_executable_efl32_file1] tests whether the ELF file is an executable
+  * file type.
+  *)
+val is_executable_elf32_file1 : elf32_file1 -> bool
+let is_executable_elf32_file1 f1 =
+  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_exec
+
+(** [is_executable_efl64_file1] tests whether the ELF file is an executable
+  * file type.
+  *)
+val is_executable_elf64_file1 : elf64_file1 -> bool
+let is_executable_elf64_file1 f1 =
+  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_exec
+
+(** [is_shared_object_elf32_file1] tests whether the ELF file is a shared object
+  * file type.
+  *)
+val is_shared_object_elf32_file1 : elf32_file1 -> bool
+let is_shared_object_elf32_file1 f1 =
+  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_dyn
+
+(** [is_shared_object_elf64_file1] tests whether the ELF file is a shared object
+* file type.
+*)
+val is_shared_object_elf64_file1 : elf64_file1 -> bool
+let is_shared_object_elf64_file1 f1 =
+  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_dyn
+
+(** [read_elf32_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
+  * leaving all other data uninterpreted.
+  *)
+val read_elf32_file1 : bitstring -> error elf32_file1
+let read_elf32_file1 bs0 =
+  read_elf32_header bs0 >>= fun (hdr, bs1) ->
+  return <| elf32_file1_header = hdr; elf32_file1_body = bs0 |>
+
+(** [read_elf64_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
+  * leaving all other data uninterpreted.
+  *)
+val read_elf64_file1 : bitstring -> error elf64_file1
+let read_elf64_file1 bs0 =
+  read_elf64_header bs0 >>= fun (hdr, bs1) ->
+  return <| elf64_file1_header = hdr; elf64_file1_body = bs0 |>
\ No newline at end of file