diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/byte_sequence.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/byte_sequence.ml | 335 |
1 files changed, 335 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/byte_sequence.ml b/lib/ocaml_rts/linksem/byte_sequence.ml new file mode 100644 index 00000000..27eb6d81 --- /dev/null +++ b/lib/ocaml_rts/linksem/byte_sequence.ml @@ -0,0 +1,335 @@ +(*Generated by Lem from byte_sequence.lem.*) +(** [byte_sequence.lem], a list of bytes used for ELF I/O and other basic tasks + * in the ELF model. + *) + +open Lem_basic_classes +open Lem_bool +open Lem_list +open Lem_num +open Lem_string +open Lem_assert_extra + +open Error +open Missing_pervasives +open Show + +(** A [byte_sequence], [bs], denotes a consecutive list of bytes. Can be read + * from or written to a binary file. Most basic type in the ELF formalisation. + *) +type byte_sequence = + Sequence of ( char list) + +(** [byte_list_of_byte_sequence bs] obtains the underlying list of bytes of the + * byte sequence [bs]. + *) +(*val byte_list_of_byte_sequence : byte_sequence -> list byte*) +let byte_list_of_byte_sequence bs0:(char)list= + ((match bs0 with + | Sequence xs -> xs + )) + +(** [compare_byte_sequence bs1 bs2] is an ordering comparison function for byte + * sequences, suitable for constructing sets, maps and other ordered types + * with. + *) +(*val compare_byte_sequence : byte_sequence -> byte_sequence -> ordering*) +let compare_byte_sequence s1 s2:int= +(lexicographic_compare compare_byte (byte_list_of_byte_sequence s1) (byte_list_of_byte_sequence s2)) + +let instance_Basic_classes_Ord_Byte_sequence_byte_sequence_dict:(byte_sequence)ord_class= ({ + + compare_method = compare_byte_sequence; + + isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_byte_sequence f1 f2) (-1)))); + + isLessEqual_method = (fun f1 -> (fun f2 -> let result = (compare_byte_sequence f1 f2) in Lem.orderingEqual result (-1) || Lem.orderingEqual result 0)); + + isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_byte_sequence f1 f2) 1))); + + isGreaterEqual_method = (fun f1 -> (fun f2 -> let result = (compare_byte_sequence f1 f2) in Lem.orderingEqual result 1 || Lem.orderingEqual result 0))}) + +(** [acquire_byte_list fname] exhaustively reads in a list of bytes from a file + * pointed to by filename [fname]. Fails if the file does not exist, or if the + * transcription otherwise fails. Implemented as a primitive in OCaml. + *) +(*val acquire_byte_list : string -> error (list 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. + *) +(*val acquire : string -> error byte_sequence*) +let acquire fname1:(byte_sequence)error= + (Byte_sequence_wrapper.acquire_char_list fname1 >>= (fun bs -> + return (Sequence bs))) + +(** [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_byte_list : string -> list byte -> error unit*) + +(** [serialise fname bs0] writes a byte sequence, [bs0], to a binary file pointed + * to by filename [fname]. Fails if the transcription fails. + *) +(*val serialise : string -> byte_sequence -> error unit*) +let serialise fname1 ss:(unit)error= + ((match ss with + | Sequence ts -> Byte_sequence_wrapper.serialise_char_list fname1 ts + )) + +(** [empty], the empty byte sequence. + *) +(*val empty : byte_sequence*) +let empty:byte_sequence= (Sequence []) + +(** [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 (Sequence ts):(char*byte_sequence)error= + ((match ts with + | [] -> fail "read_char: sequence is empty" + | x::xs -> return (x, Sequence xs) + )) + +(** [repeat cnt b] creates a list of length [cnt] containing only [b]. + * TODO: move into missing_pervasives.lem. + *) +(*val repeat' : natural -> byte -> list byte -> list byte*) +let rec repeat' count c acc:(char)list= + ( + if(Nat_big_num.equal count (Nat_big_num.of_int 0)) then acc else + (repeat' ( Nat_big_num.sub_nat count (Nat_big_num.of_int 1)) c (c :: acc))) + +(*val repeat : natural -> byte -> list byte*) +let repeat count c:(char)list= (repeat' count c []) + +(** [create cnt b] creates a byte sequence of length [cnt] containing only [b]. + *) +(*val create : natural -> byte -> byte_sequence*) +let create count c:byte_sequence= + (Sequence (repeat count c)) + +(** [zeros cnt] creates a byte sequence of length [cnt] containing only 0, the + * null byte. + *) +(*val zeros : natural -> byte_sequence*) +let zeros m:byte_sequence= + (create m '\000') + +(** [length bs0] returns the length of [bs0]. + *) +(*val length : byte_sequence -> natural*) +let length0 (Sequence ts):Nat_big_num.num= + (Nat_big_num.of_int (List.length ts)) + + +(** [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 rec concat0 ts:byte_sequence= + ((match ts with + | [] -> Sequence [] + | ((Sequence x)::xs) -> + (match concat0 xs with + | Sequence tail -> Sequence ( List.rev_append (List.rev x) tail) + ) + )) + +(** [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 len bs:byte_sequence= + (let curlen = (length0 bs) in + if Nat_big_num.greater_equal curlen len then + bs + else + concat0 [bs ; (zeros ( Nat_big_num.sub_nat len curlen))]) + +(** [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 ts:byte_sequence= + (Sequence (List.concat ts)) + +(** [string_of_char_list cs] converts a list of characters into a string. + * Implemented as a primitive in OCaml. + *) +(*val string_of_char_list : list char -> string*) + +(** [char_list_of_byte_list bs] converts byte list [bs] into a list of characters. + * Implemented as a primitive in OCaml and Isabelle. + * TODO: is this actually being used in the Isabelle backend? All string functions + * should be factored out by target-specific definitions. + *) +(*val char_list_of_byte_list : list byte -> list char*) + +(** [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 (Sequence ts):string= + (let cs = ( ts) in + Xstring.implode cs) + +(** [equal bs0 bs1] checks whether two byte sequences, [bs0] and [bs1], are equal. + *) +(*val equal : byte_sequence -> byte_sequence -> bool*) +let rec equal left right:bool= + ((match (left, right) with + | (Sequence [], Sequence []) -> true + | (Sequence (x::xs), Sequence (y::ys)) -> +(x = y) && equal (Sequence xs) (Sequence ys) + | (_, _) -> false + )) + +(** [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 rec dropbytes count (Sequence ts):(byte_sequence)error= + (if Nat_big_num.equal count Nat_big_num.zero then + return (Sequence ts) + else + (match ts with + | [] -> fail "dropbytes: cannot drop more bytes than are contained in sequence" + | x::xs -> dropbytes ( Nat_big_num.sub_nat count(Nat_big_num.of_int 1)) (Sequence xs) + )) + +(*val takebytes_r_with_length: nat -> natural -> byte_sequence -> error byte_sequence*) +let rec takebytes_r_with_length count ts_length (Sequence ts):(byte_sequence)error= + (if Nat_big_num.greater_equal ts_length (Nat_big_num.of_int count) then + return (Sequence (list_take_with_accum count [] ts)) + else + fail "takebytes: cannot take more bytes than are contained in sequence") + +(*val takebytes : natural -> byte_sequence -> error byte_sequence*) +let takebytes count (Sequence ts):(byte_sequence)error= + (let result = (takebytes_r_with_length (Nat_big_num.to_int count) (Missing_pervasives.length ts) (Sequence ts)) in + result) + +(*val takebytes_with_length : natural -> natural -> byte_sequence -> error byte_sequence*) +let takebytes_with_length count ts_length (Sequence ts):(byte_sequence)error= +( + (* let _ = Missing_pervasives.errs ("Trying to take " ^ (show count) ^ " bytes from sequence of " ^ (show (List.length ts)) ^ "\n") in *)let result = (takebytes_r_with_length (Nat_big_num.to_int count) ts_length (Sequence ts)) in + (*let _ = Missing_pervasives.errs ("Succeeded\n") in *) + result) + +(** [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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + 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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + 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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + read_char bs1 >>= (fun (b1, bs2) -> + read_char bs2 >>= (fun (b2, bs3) -> + 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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + read_char bs1 >>= (fun (b1, bs2) -> + read_char bs2 >>= (fun (b2, bs3) -> + 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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + read_char bs1 >>= (fun (b1, bs2) -> + read_char bs2 >>= (fun (b2, bs3) -> + read_char bs3 >>= (fun (b3, bs4) -> + read_char bs4 >>= (fun (b4, bs5) -> + read_char bs5 >>= (fun (b5, bs6) -> + read_char bs6 >>= (fun (b6, bs7) -> + 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)error= + (read_char bs0 >>= (fun (b0, bs1) -> + read_char bs1 >>= (fun (b1, bs2) -> + read_char bs2 >>= (fun (b2, bs3) -> + read_char bs3 >>= (fun (b3, bs4) -> + read_char bs4 >>= (fun (b4, bs5) -> + read_char bs5 >>= (fun (b5, bs6) -> + read_char bs6 >>= (fun (b6, bs7) -> + 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*byte_sequence)error= + (takebytes idx1 bs0 >>= (fun l -> + 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*byte_sequence)error= + (takebytes_with_length idx1 bs0_length bs0 >>= (fun l -> + 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)error= + (dropbytes off bs0 >>= (fun bs1 -> + takebytes cut bs1 >>= (fun res -> + return res))) + +let instance_Show_Show_Byte_sequence_byte_sequence_dict:(byte_sequence)show_class= ({ + + show_method = string_of_byte_sequence}) + +let instance_Basic_classes_Eq_Byte_sequence_byte_sequence_dict:(byte_sequence)eq_class= ({ + + isEqual_method = equal; + + isInequal_method = (fun l r->not (equal l r))}) |