blob: ff2bba61afb69d22f7b02978d0259a0d5ca50f15 (
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
|
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 |>
|
