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
|
(*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 string_of_byte_sequence : byte_sequence -> string*)
let string_of_byte_sequence0 seq:string=
((match seq with
| Sequence bs -> Xstring.implode (Lem_list.map (fun x-> x) bs)
))
(*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)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
(* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *)
partition_with_length header_length seq_length seq >>= (fun (header, rest) ->
offset_and_cut(Nat_big_num.of_int 58)(Nat_big_num.of_int 2) header >>= (fun magic ->
offset_and_cut(Nat_big_num.of_int 0)(Nat_big_num.of_int 16) header >>= (fun name1 ->
offset_and_cut(Nat_big_num.of_int 16)(Nat_big_num.of_int 12) header >>= (fun timestamp_str ->
offset_and_cut(Nat_big_num.of_int 28)(Nat_big_num.of_int 6) header >>= (fun uid_str ->
offset_and_cut(Nat_big_num.of_int 34)(Nat_big_num.of_int 6) header >>= (fun gid_str ->
offset_and_cut(Nat_big_num.of_int 40)(Nat_big_num.of_int 8) header >>= (fun mode_str ->
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_sequence0 size_str)) in
(* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *)
return ({ name = (string_of_byte_sequence0 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 seq:((char)list*byte_sequence)error=
((match seq with
| Sequence bs ->
(* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ")
in*)
let chars = (Lem_list.map (fun x-> x) (take0(Nat_big_num.of_int 8) bs)) in
if Xstring.implode chars = "!<arch>\n" then
(* let _ = Missing_pervasives.errln ": yes" in *)
return (chars, Sequence(drop0(Nat_big_num.of_int 8) bs))
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)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), seq) ->
(match seq with
| Sequence next_bs ->
(* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (List.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
(*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*)
let chunk = (Sequence(Lem_list.take hdr.size next_bs))
in
(*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_sequence0 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 seq) 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_sequence)list)error=
(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
)))
|
