Pull in updated elf model, make build work again (at least for me)

1 files changed, 181 insertions, 0 deletions

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