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/archive.ml.html
Source file archive.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(*Generated by Lem from archive.lem.*) open Lem_basic_classes open Lem_bool open Lem_list open Lem_num open Lem_maybe open Lem_string open Show open Lem_assert_extra open Missing_pervasives open Byte_sequence open Error type archive_entry_header = { name : string ; timestamp : Nat_big_num.num ; uid : int ; gid : int ; mode : int ; size : int (* 1GB should be enough *) } type archive_global_header = char list (*val read_archive_entry_header : natural -> byte_sequence -> error (archive_entry_header * natural * byte_sequence)*) let read_archive_entry_header seq_length seq:(archive_entry_header*Nat_big_num.num*Byte_sequence_wrapper.byte_sequence)error= (let magic_bytes = ([Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 96))) (* 0x60 *); Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 10))) (* 0x0a *)]) in let header_length =( (Nat_big_num.of_int 60)) in bind ( (* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *)partition_with_length header_length seq_length seq) (fun (header, rest) -> bind (offset_and_cut( (Nat_big_num.of_int 58))( (Nat_big_num.of_int 2)) header) (fun magic -> bind (offset_and_cut( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 16)) header) (fun name1 -> bind (offset_and_cut( (Nat_big_num.of_int 16))( (Nat_big_num.of_int 12)) header) (fun timestamp_str -> bind (offset_and_cut( (Nat_big_num.of_int 28))( (Nat_big_num.of_int 6)) header) (fun uid_str -> bind (offset_and_cut( (Nat_big_num.of_int 34))( (Nat_big_num.of_int 6)) header) (fun gid_str -> bind (offset_and_cut( (Nat_big_num.of_int 40))( (Nat_big_num.of_int 8)) header) (fun mode_str -> bind (offset_and_cut( (Nat_big_num.of_int 48))( (Nat_big_num.of_int 10)) header) (fun size_str -> let size2 = (natural_of_decimal_string (string_of_byte_sequence size_str)) in (* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *) return ({ name = (string_of_byte_sequence name1); timestamp = (( (Nat_big_num.of_int 0) : Nat_big_num.num)) (* FIXME *); uid = 0 (* FIXME *) ; gid = 0 (* FIXME *) ; mode = 0 (* FIXME *); size = (Nat_big_num.to_int size2) (* FIXME *) }, Nat_big_num.sub_nat seq_length header_length, rest)))))))))) (*val read_archive_global_header : byte_sequence -> error (archive_global_header * byte_sequence)*) let read_archive_global_header bs:((char)list*Byte_sequence_wrapper.byte_sequence)error= (bind ( (* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ") in*)takebytes( (Nat_big_num.of_int 8)) bs) (fun h -> if string_of_byte_sequence h = "!<arch>\n" then bind ( (* let _ = Missing_pervasives.errln ": yes" in *)dropbytes( (Nat_big_num.of_int 8)) bs) (fun t -> return (char_list_of_byte_sequence h, t)) else (* let _ = Missing_pervasives.errln ": no" in *) fail "read_archive_global_header: not an archive")) (*val accum_archive_contents : (list (string * byte_sequence)) -> maybe string -> natural -> byte_sequence -> error (list (string * byte_sequence))*) let rec accum_archive_contents accum extended_filenames whole_seq_length whole_seq:((string*Byte_sequence_wrapper.byte_sequence)list)error= ( (* let _ = Missing_pervasives.errs "Can read a header? " in *)if not (Nat_big_num.equal (Byte_sequence.length0 whole_seq) whole_seq_length) then (assert false) (* invariant: whole_seq_length always equal to length of whole_seq, so the length is only computed one. This "fail" needed for Isabelle termination proofs... *) else (match (read_archive_entry_header whole_seq_length whole_seq) with | Fail _ -> return accum | Success (hdr, (seq_length : Nat_big_num.num), next_bs) -> (* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (Byte_sequence.length next_bs))) in *) let amount_to_drop = (if (hdr.size mod 2) = 0 then (Nat_big_num.of_int hdr.size) else Nat_big_num.add (Nat_big_num.of_int hdr.size)( (Nat_big_num.of_int 1))) in if Nat_big_num.equal amount_to_drop( (Nat_big_num.of_int 0)) then fail "accum_archive_contents: amount to drop from byte sequence is 0" else bind ( (*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*)takebytes (Nat_big_num.of_int hdr.size) next_bs) (fun chunk -> (*let _ = Missing_pervasives.errs ("Processing archive header named " ^ hdr.name) in*) let (new_accum, (new_extended_filenames : string option)) = (let name1 = (Xstring.explode hdr.name) in if (listEqualBy (=) name1 ['/'; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' ']) then (* SystemV symbol lookup table; we skip this *) (accum, extended_filenames) else (match name1 with | x::xs -> if x = '/' then (match xs with | y::ys -> if y = '/' then (accum, Some (string_of_byte_sequence chunk)) else let index = (natural_of_decimal_string (Xstring.implode xs)) in (match extended_filenames with | None -> failwith "corrupt archive: reference to non-existent extended filenames" | Some s -> let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*) (((ext_name, chunk) :: accum), extended_filenames) ) | [] -> let index = (natural_of_decimal_string (Xstring.implode xs)) in (match extended_filenames with | None -> failwith "corrupt archive: reference to non-existent extended filenames" | Some s -> let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*) (((ext_name, chunk) :: accum), extended_filenames) ) ) else (((hdr.name, chunk) :: accum), extended_filenames) | [] -> (((hdr.name, chunk) :: accum), extended_filenames) )) in (match (Byte_sequence.dropbytes amount_to_drop next_bs) with | Fail _ -> return accum | Success new_seq -> accum_archive_contents new_accum new_extended_filenames ( Nat_big_num.sub_nat seq_length amount_to_drop) new_seq )) )) (*val read_archive : byte_sequence -> error (list (string * byte_sequence))*) let read_archive bs:((string*byte_sequence0)list)error= (bind (read_archive_global_header bs) (fun (hdr, seq) -> let result = (accum_archive_contents [] None (Byte_sequence.length0 seq) seq) in (* let _ = Missing_pervasives.errln "Finished reading archive" in *) (match result with Success r -> Success (List.rev r) | Fail x -> Fail x )))