summaryrefslogtreecommitdiff
path: root/src/elf_model/sail_interface.lem
blob: 6c474fa7c0dff0cbd0377b9e6939c614f4814189 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
open import Basic_classes
open import Function
open import Maybe
open import String
open import Tuple

open import Assert_extra

open import Bitstring
open import Error
open import Missing_pervasives
open import Show

open import Elf_header
open import Elf_executable_file3
open import Elf_types

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... *)
    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 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_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
  in
    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