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, 0 insertions, 335 deletions
diff --git a/lib/ocaml_rts/linksem/byte_sequence.ml b/lib/ocaml_rts/linksem/byte_sequence.ml deleted file mode 100644 index 27eb6d81..00000000 --- a/lib/ocaml_rts/linksem/byte_sequence.ml +++ /dev/null @@ -1,335 +0,0 @@ -(*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))}) |