Source file byte_sequence.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
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_string
open Lem_assert_extra
open Error
open Lem_maybe
open Missing_pervasives
open Show
open Byte_sequence_impl
(** [byte_sequence.lem], a list of bytes used for ELF I/O and other basic tasks
* in the ELF model.
*)
type byte_sequence0 = Byte_sequence_wrapper.byte_sequence
let empty:Byte_sequence_wrapper.byte_sequence= Byte_sequence_wrapper.empty
(** [read_char bs0] reads a single byte from byte sequence [bs0] and returns the
* remainder of the byte sequence. Fails if [bs0] is empty.
* TODO: rename to read_byte, probably.
*)
let read_char:Byte_sequence_wrapper.byte_sequence ->(char*Byte_sequence_wrapper.byte_sequence)error= Byte_sequence_wrapper.read_char
(** [find_byte bs b] finds the first occurence of b in bs and gives the index.
* returns [Nothing] if the byte do not appear in bs
*)
let find_byte:Byte_sequence_wrapper.byte_sequence ->char ->(Nat_big_num.num)option= Byte_sequence_wrapper.big_num_find_byte
(** [acquire fname] exhaustively reads in a byte_sequence from a file pointed to
* by filename [fname]. Fails if the file does not exist, or if the transcription
* otherwise fails.
*)
let acquire:string ->(Byte_sequence_wrapper.byte_sequence)error= Byte_sequence_wrapper.acquire
(** [serialise_byte_list fname bs] writes a list of bytes, [bs], to a binary file
* pointed to by filename [fname]. Fails if the transcription fails. Implemented
* as a primitive in OCaml.
*)
let serialise:string ->Byte_sequence_wrapper.byte_sequence ->(unit)error= Byte_sequence_wrapper.serialise
(** [create cnt b] creates a byte sequence of length [cnt] containing only [b].
*)
let create:Nat_big_num.num ->char ->Byte_sequence_wrapper.byte_sequence= Byte_sequence_wrapper.big_num_make
(** [zeros cnt] creates a byte sequence of length [cnt] containing only 0, the
* null byte.
*)
let zeros len:Byte_sequence_wrapper.byte_sequence=
(create len '\000')
(** [length bs0] returns the length of [bs0].
*)
let length0:Byte_sequence_wrapper.byte_sequence ->Nat_big_num.num= Byte_sequence_wrapper.big_num_length
(** [concat bs] concatenates a list of byte sequences, [bs], into a single byte
* sequence, maintaining byte order across the sequences.
*)
let concat:(Byte_sequence_wrapper.byte_sequence)list ->Byte_sequence_wrapper.byte_sequence= Byte_sequence_wrapper.concat
(** [zero_pad_to_length len bs0] pads (on the right) consecutive zeros until the
* resulting byte sequence is [len] long. Returns [bs0] if [bs0] is already of
* greater length than [len].
*)
let zero_pad_to_length:Nat_big_num.num ->Byte_sequence_wrapper.byte_sequence ->Byte_sequence_wrapper.byte_sequence= Byte_sequence_wrapper.big_num_zero_pad_to_length
let byte_sequence_of_byte_list:(char)list ->Byte_sequence_wrapper.byte_sequence= Byte_sequence_wrapper.from_char_list
(** [from_byte_lists bs] concatenates a list of bytes [bs] and creates a byte
* sequence from their contents. Maintains byte order in [bs].
*)
let from_byte_lists l:Byte_sequence_wrapper.byte_sequence=
(concat (Lem_list.map byte_sequence_of_byte_list l))
(** [string_of_byte_sequence bs0] converts byte sequence [bs0] into a string
* representation.
*)
let string_of_byte_sequence:Byte_sequence_wrapper.byte_sequence ->string= Byte_sequence_wrapper.to_string
let char_list_of_byte_sequence:Byte_sequence_wrapper.byte_sequence ->(char)list= Byte_sequence_wrapper.to_char_list
let byte_list_of_byte_sequence:Byte_sequence_wrapper.byte_sequence ->(char)list= Byte_sequence_wrapper.to_char_list
(** [equal bs0 bs1] checks whether two byte sequences, [bs0] and [bs1], are equal.
*)
let equal:Byte_sequence_wrapper.byte_sequence ->Byte_sequence_wrapper.byte_sequence ->bool= Byte_sequence_wrapper.equal
(** [dropbytes cnt bs0] drops [cnt] bytes from byte sequence [bs0]. Fails if
* [cnt] is greater than the length of [bs0].
*)
let dropbytes:Nat_big_num.num ->Byte_sequence_wrapper.byte_sequence ->(Byte_sequence_wrapper.byte_sequence)error= Byte_sequence_wrapper.big_num_dropbytes
(** [takebytes cnt bs0] takes [cnt] bytes from byte sequence [bs0]. Fails if
* [cnt] is greater than the length of [bs0].
*)
let takebytes:Nat_big_num.num ->Byte_sequence_wrapper.byte_sequence ->(Byte_sequence_wrapper.byte_sequence)error= Byte_sequence_wrapper.big_num_takebytes
let takebytes_with_length0:Nat_big_num.num ->Nat_big_num.num ->Byte_sequence_wrapper.byte_sequence ->(Byte_sequence_wrapper.byte_sequence)error= Byte_sequence_impl.takebytes_with_length
(** [read_2_bytes_le bs0] reads two bytes from [bs0], returning them in
* little-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 2.
*)
let read_2_bytes_le bs0:((char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) ->
return ((b1, b0), bs2))))
(** [read_2_bytes_be bs0] reads two bytes from [bs0], returning them in
* big-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 2.
*)
let read_2_bytes_be bs0:((char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) ->
return ((b0, b1), bs2))))
(** [read_4_bytes_le bs0] reads four bytes from [bs0], returning them in
* little-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 4.
*)
let read_4_bytes_le bs0:((char*char*char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) -> Error.bind (read_char bs2) (fun (b2, bs3) -> Error.bind (read_char bs3) (fun (b3, bs4) ->
return ((b3, b2, b1, b0), bs4))))))
(** [read_4_bytes_be bs0] reads four bytes from [bs0], returning them in
* big-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 4.
*)
let read_4_bytes_be bs0:((char*char*char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) -> Error.bind (read_char bs2) (fun (b2, bs3) -> Error.bind (read_char bs3) (fun (b3, bs4) ->
return ((b0, b1, b2, b3), bs4))))))
(** [read_8_bytes_le bs0] reads eight bytes from [bs0], returning them in
* little-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 8.
*)
let read_8_bytes_le bs0:((char*char*char*char*char*char*char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) -> Error.bind (read_char bs2) (fun (b2, bs3) -> Error.bind (read_char bs3) (fun (b3, bs4) -> Error.bind (read_char bs4) (fun (b4, bs5) -> Error.bind (read_char bs5) (fun (b5, bs6) -> Error.bind (read_char bs6) (fun (b6, bs7) -> Error.bind (read_char bs7) (fun (b7, bs8) ->
return ((b7, b6, b5, b4, b3, b2, b1, b0), bs8))))))))))
(** [read_8_bytes_be bs0] reads eight bytes from [bs0], returning them in
* big-endian order, and returns the remainder of [bs0]. Fails if [bs0] has
* length less than 8.
*)
let read_8_bytes_be bs0:((char*char*char*char*char*char*char*char)*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (read_char bs0) (fun (b0, bs1) -> Error.bind (read_char bs1) (fun (b1, bs2) -> Error.bind (read_char bs2) (fun (b2, bs3) -> Error.bind (read_char bs3) (fun (b3, bs4) -> Error.bind (read_char bs4) (fun (b4, bs5) -> Error.bind (read_char bs5) (fun (b5, bs6) -> Error.bind (read_char bs6) (fun (b6, bs7) -> Error.bind (read_char bs7) (fun (b7, bs8) ->
return ((b0, b1, b2, b3, b4, b5, b6, b7), bs8))))))))))
(** [partition pnt bs0] splits [bs0] into two parts at index [pnt]. Fails if
* [pnt] is greater than the length of [bs0].
*)
let partition0 idx1 bs0:(Byte_sequence_wrapper.byte_sequence*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (takebytes idx1 bs0) (fun l -> Error.bind (dropbytes idx1 bs0) (fun r ->
return (l, r))))
let partition_with_length idx1 bs0_length bs0:(Byte_sequence_wrapper.byte_sequence*Byte_sequence_wrapper.byte_sequence)error= (Error.bind (takebytes_with_length0 idx1 bs0_length bs0) (fun l -> Error.bind (dropbytes idx1 bs0) (fun r ->
return (l, r))))
(** [offset_and_cut off cut bs0] first cuts [off] bytes off [bs0], then cuts
* the resulting byte sequence to length [cut]. Fails if [off] is greater than
* the length of [bs0] and if [cut] is greater than the length of the intermediate
* byte sequence.
*)
let offset_and_cut off cut bs0:(Byte_sequence_wrapper.byte_sequence)error= (Error.bind (dropbytes off bs0) (fun bs1 -> Error.bind (takebytes cut bs1) (fun res ->
return res)))