package linksem

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(*Generated by Lem from byte_sequence.lem.*)
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

(*val empty : 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.
  *)
(*val read_char : byte_sequence -> error (byte * byte_sequence)*)
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
*)
(*val find_byte : byte_sequence -> byte -> maybe natural*)
let find_byte:Byte_sequence_wrapper.byte_sequence ->char ->(Nat_big_num.num)option=  Byte_sequence_wrapper.big_num_find_byte

(* There's no generic implementation for those two *)

(** [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.
  *)
(*val acquire : string -> error byte_sequence*)
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.
  *)
(*val serialise : string -> byte_sequence -> error unit*)
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].
  *)
(*val create : natural -> byte -> byte_sequence*)
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.
  *)
(*val zeros : natural -> byte_sequence*)
let zeros len:Byte_sequence_wrapper.byte_sequence=
   (create len '\000')

(** [length bs0] returns the length of [bs0].
  *)
(*val length : byte_sequence -> natural*)
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.
  *)
(*val concat : list byte_sequence -> byte_sequence*)
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].
  *)
(*val zero_pad_to_length : natural -> byte_sequence -> byte_sequence*)
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

(*val byte_sequence_of_byte_list : list byte -> byte_sequence*)
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].
  *)
(*val from_byte_lists : list (list byte) -> byte_sequence*)
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.
  *)
(*val string_of_byte_sequence : byte_sequence -> string*)
let string_of_byte_sequence:Byte_sequence_wrapper.byte_sequence ->string=  Byte_sequence_wrapper.to_string

(*val char_list_of_byte_sequence : byte_sequence -> list char*)
let char_list_of_byte_sequence:Byte_sequence_wrapper.byte_sequence ->(char)list=  Byte_sequence_wrapper.to_char_list

(*val byte_list_of_byte_sequence : byte_sequence -> list byte*)
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.
  *)
(*val equal : byte_sequence -> byte_sequence -> bool*)
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].
  *)
(*val dropbytes : natural -> byte_sequence -> error byte_sequence*)
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].
*)
(*val takebytes : natural -> byte_sequence -> error byte_sequence*)
let takebytes:Nat_big_num.num ->Byte_sequence_wrapper.byte_sequence ->(Byte_sequence_wrapper.byte_sequence)error=  Byte_sequence_wrapper.big_num_takebytes

(*val takebytes_with_length : natural -> natural -> byte_sequence -> error byte_sequence*)
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.
  *)
(*val read_2_bytes_le : byte_sequence -> error ((byte * byte) * byte_sequence)*)
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.
  *)
(*val read_2_bytes_be : byte_sequence -> error ((byte * byte) * byte_sequence)*)
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.
  *)
(*val read_4_bytes_le : byte_sequence -> error ((byte * byte * byte * byte) * byte_sequence)*)
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.
  *)
(*val read_4_bytes_be : byte_sequence -> error ((byte * byte * byte * byte) * byte_sequence)*)
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.
  *)
(*val read_8_bytes_le : byte_sequence -> error ((byte * byte * byte * byte * byte * byte * byte * byte) * byte_sequence)*)
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.
  *)
(*val read_8_bytes_be : byte_sequence -> error ((byte * byte * byte * byte * byte * byte * byte * byte) * byte_sequence)*)
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].
  *)
(*val partition : natural -> byte_sequence -> error (byte_sequence * byte_sequence)*)
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))))

(*val partition_with_length : natural -> natural -> byte_sequence -> error (byte_sequence * byte_sequence)*)
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.
  *)
(*val offset_and_cut : natural -> natural -> byte_sequence -> error 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)))
OCaml

Innovation. Community. Security.