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

1 files changed, 295 insertions, 1 deletions

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