package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/byte_sequence.ml.html
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)))