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
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
let 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))) ; Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 10))) ]) in
let =( (Nat_big_num.of_int 60)) in bind (
partition_with_length header_length seq_length seq) (fun (, 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
return ({ name = (string_of_byte_sequence name1); timestamp = (( (Nat_big_num.of_int 0) : Nat_big_num.num)) ;
uid = 0 ; gid = 0 ; mode = 0 ;
size = (Nat_big_num.to_int size2) }, Nat_big_num.sub_nat seq_length header_length, rest))))))))))
let bs:((char)list*Byte_sequence_wrapper.byte_sequence)error= (bind (
takebytes( (Nat_big_num.of_int 8)) bs) (fun h ->
if string_of_byte_sequence h = "!<arch>\n" then bind (
dropbytes( (Nat_big_num.of_int 8)) bs) (fun t ->
return (char_list_of_byte_sequence h, t))
else
fail "read_archive_global_header: not an archive"))
let rec accum_archive_contents accum extended_filenames whole_seq_length whole_seq:((string*Byte_sequence_wrapper.byte_sequence)list)error=
(
if not (Nat_big_num.equal (Byte_sequence.length0 whole_seq) whole_seq_length) then
(assert false)
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 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 (
takebytes (Nat_big_num.of_int hdr.size) next_bs) (fun chunk ->
let (new_accum, (new_extended_filenames : string option)) =
(let name1 = (Xstring.explode hdr.name) in
if (listEqualBy (=) name1 ['/'; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' ']) then
(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
(((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
(((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
))
))
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
(match result with
Success r -> Success (List.rev r)
| Fail x -> Fail x
)))