Source file sail_interface.ml

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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
(*Generated by Lem from adaptors/sail_interface.lem.*)
open Lem_basic_classes
open Lem_function
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
open Lem_tuple

open Lem_assert_extra

open Byte_sequence
open Error
open Missing_pervasives
open Show

open Elf_header
open Elf_file
open Elf_interpreted_section
open Elf_interpreted_segment
open String_table
open Elf_symbol_table
open Elf_program_header_table
open Elf_types_native_uint

open Hex_printing

type executable_process_image =
  | ELF_Class_32 of elf32_executable_process_image
  | ELF_Class_64 of elf64_executable_process_image

(*val string_of_segment_provenance : segment_provenance -> string*)
let string_of_segment_provenance p:string=
   ((match p with
    | FromELF -> "Segment from ELF file"
    | AutoGenerated -> "Segment auto generated"
  ))

(*val string_of_executable_process_image : executable_process_image -> string*)
let string_of_executable_process_image img2:string=
   ((match img2 with
    | ELF_Class_32 (segs, entry_point, machine_type) ->
        let machine_type = (string_of_elf_machine_architecture machine_type) in
        let entry_point  = (unsafe_hex_string_of_natural 16 entry_point) in
        let segs         = (Lem_list.map (fun (seg, prov) ->
                             let prov = (string_of_segment_provenance prov) in
                             let seg  = (string_of_elf32_interpreted_segment seg) in
                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
                           ) segs)
        in
          unlines ( List.rev_append (List.rev [
            "32-bit ELF executable image"
          ; ("Machine type: " ^ machine_type)
          ; ("Entry point: " ^ entry_point)
          ; ""
          ]) segs)
    | ELF_Class_64 (segs, entry_point, machine_type) ->
        let machine_type = (string_of_elf_machine_architecture machine_type) in
        let entry_point  = (unsafe_hex_string_of_natural 16 entry_point) in
        let segs         = (intercalate "\n" (Lem_list.map (fun (seg, prov) ->
                             let prov = (string_of_segment_provenance prov) in
                             let seg  = (string_of_elf64_interpreted_segment seg) in
                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
                           ) segs))
        in
          unlines ( List.rev_append (List.rev [
            "64-bit ELF executable image"
          ; ("Machine type: " ^ machine_type)
          ; ("Entry point: " ^ entry_point)
          ; ""
          ]) segs)
  ))

(*val populate : string -> error executable_process_image*)
let populate fname1:(executable_process_image)error=  (bind (
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "populate: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun ef5 ->
          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then bind (Elf_file.get_elf32_executable_image ef5) (fun img2 ->
            return (ELF_Class_32 img2))
          else
            fail "populate: not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun ef5 ->
          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then bind (Elf_file.get_elf64_executable_image ef5) (fun img2 ->
            return (ELF_Class_64 img2))
          else
            fail "populate: not a statically linked executable")
        else
          fail "populate: ELF class unrecognised"
    ))))

(*val populate' : byte_sequence -> error executable_process_image*)
let populate' bs0:(executable_process_image)error=  (bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "populate': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun ef5 ->
          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then bind (Elf_file.get_elf32_executable_image ef5) (fun img2 ->
            return (ELF_Class_32 img2))
          else
            fail "populate': not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun ef5 ->
          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then bind (Elf_file.get_elf64_executable_image ef5) (fun img2 ->
            return (ELF_Class_64 img2))
          else
            fail "populate': not a statically linked executable")
        else
          fail "populate': ELF class unrecognised"
    )))

(*val obtain_global_symbol_init_info : string -> error global_symbol_init_info*)
let obtain_global_symbol_init_info fname1:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error=  (bind (
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "obtain_global_symbol_init_info: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info: not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info: not a statically linked executable")
        else
          fail "obtain_global_symbol_init_info: ELF class unrecognised"
    ))))

(*val obtain_global_symbol_init_info' : byte_sequence -> error global_symbol_init_info*)
let obtain_global_symbol_init_info' bs0:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error=  (bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "obtain_global_symbol_init_info': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info': not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info': not a statically linked executable")
        else
          fail "obtain_global_symbol_init_info': ELF class unrecognised"
    )))

(*val populate_and_obtain_global_symbol_init_info : string -> error (elf_file * executable_process_image * global_symbol_init_info)*)
let populate_and_obtain_global_symbol_init_info fname1:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error=  (bind (
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1) (fun bs0 -> bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "populate_and_obtain_global_symbol_init_info: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf32_executable_image f1) (fun img2 ->           
            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 ->
          if (* hack *) true (* Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table*) then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf64_executable_image f1) (fun img2 ->
            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
        else
          fail "populate_and_obtain_global_symbol_init_info: ELF class unrecognised"
    ))))

(*val populate_and_obtain_global_symbol_init_info' : byte_sequence -> error (elf_file * executable_process_image * global_symbol_init_info)*)
let populate_and_obtain_global_symbol_init_info' bs0:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence0)option*Nat_big_num.num))list)error=  (bind (
  (* 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 Lem_list.list_index ident 4 with
      | None -> fail "populate_and_obtain_global_symbol_init_info': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_32 then bind (Elf_file.read_elf32_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then bind (Elf_file.get_elf32_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf32_executable_image f1) (fun img2 ->           
            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint c) Elf_header.elf_class_64 then bind (Elf_file.read_elf64_file bs0) (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then bind (Elf_file.get_elf64_file_global_symbol_init f1) (fun init1 -> bind (Elf_file.get_elf64_executable_image f1) (fun img2 ->
            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
        else
          fail "populate_and_obtain_global_symbol_init_info': ELF class unrecognised"
    )))