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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
open Pp
open System
let magic_number = 0x436F7121l
let error_corrupted file s =
CErrors.user_err (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
let open_trapping_failure name =
try open_out_bin name
with e when CErrors.noncritical e ->
CErrors.user_err (str "Can't open " ++ str name ++ spc() ++ str "(" ++ CErrors.print e ++ str ").")
type 'a segment = {
name : string;
pos : int64;
len : int64;
hash : Digest.t;
}
type in_handle = {
in_filename : string;
in_channel : in_channel;
in_segments : Obj.t segment CString.Map.t;
}
type out_handle = {
out_filename : string;
out_channel : out_channel;
mutable out_segments : Obj.t segment CString.Map.t;
}
type 'a id = { id : string }
let make_id id = { id }
let input_segment_summary ch =
let nlen = input_int32 ch in
let name = really_input_string ch (Int32.to_int nlen) in
let pos = input_int64 ch in
let len = input_int64 ch in
let hash = Digest.input ch in
{ name; pos; len; hash }
let output_segment_summary ch seg =
let nlen = Int32.of_int (String.length seg.name) in
let () = output_int32 ch nlen in
let () = output_string ch seg.name in
let () = output_int64 ch seg.pos in
let () = output_int64 ch seg.len in
let () = Digest.output ch seg.hash in
()
let rec input_segment_summaries ch n accu =
if Int32.equal n 0l then accu
else
let s = input_segment_summary ch in
let accu = CString.Map.add s.name s accu in
input_segment_summaries ch (Int32.pred n) accu
let marshal_in_segment (type a) h ~segment : a * Digest.t =
let { in_channel = ch } = h in
let s = CString.Map.find segment.id h.in_segments in
let () = LargeFile.seek_in ch s.pos in
let (v : a) = marshal_in h.in_filename ch in
let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in
let h = Digest.input ch in
let () = assert (String.equal h s.hash) in
(v, s.hash)
let marshal_out_segment h ~segment v =
let { out_channel = ch } = h in
let () = assert (not (CString.Map.mem segment.id h.out_segments)) in
let pos = LargeFile.pos_out ch in
let () = Marshal.to_channel ch v [] in
let () = flush ch in
let pos' = LargeFile.pos_out ch in
let len = Int64.sub pos' pos in
let hash =
let in_ch = open_in_bin h.out_filename in
let () = LargeFile.seek_in in_ch pos in
let digest = Digest.channel in_ch (Int64.to_int len) in
let () = close_in in_ch in
digest
in
let () = Digest.output ch hash in
let s = { name = segment.id; pos; len; hash } in
let () = h.out_segments <- CString.Map.add segment.id s h.out_segments in
()
let marshal_out_binary h ~segment =
let { out_channel = ch } = h in
let () = assert (not (CString.Map.mem segment.id h.out_segments)) in
let pos = LargeFile.pos_out ch in
let finish () =
let () = flush ch in
let pos' = LargeFile.pos_out ch in
let len = Int64.sub pos' pos in
let hash =
let in_ch = open_in_bin h.out_filename in
let () = LargeFile.seek_in in_ch pos in
let digest = Digest.channel in_ch (Int64.to_int len) in
let () = close_in in_ch in
digest
in
let () = Digest.output ch hash in
let s = { name = segment.id; pos; len; hash } in
h.out_segments <- CString.Map.add segment.id s h.out_segments
in
ch, finish
let open_in ~file =
try
let ch = open_in_bin file in
let magic = input_int32 ch in
let version = input_int32 ch in
let () =
if not (Int32.equal magic magic_number) then
let e = { filename = file; actual = magic; expected = magic_number } in
raise (Bad_magic_number e)
in
let () =
let expected = Coq_config.vo_version in
if not (Int32.equal version expected) then
let e = { filename = file; actual = version; expected } in
raise (Bad_version_number e)
in
let summary_pos = input_int64 ch in
let () = LargeFile.seek_in ch summary_pos in
let nsum = input_int32 ch in
let seg = input_segment_summaries ch nsum CString.Map.empty in
{ in_filename = file; in_channel = ch; in_segments = seg }
with
| End_of_file -> error_corrupted file "premature end of file"
| Failure s | Sys_error s -> error_corrupted file s
let close_in ch =
close_in ch.in_channel
let get_segment (type a) ch ~(segment : a id) : a segment =
(CString.Map.find segment.id ch.in_segments :> a segment)
let segments ch = ch.in_segments
let open_out ~file =
let ch = open_trapping_failure file in
let () = output_int32 ch magic_number in
let () = output_int32 ch Coq_config.vo_version in
let () = output_int64 ch 0L in
{ out_channel = ch; out_segments = CString.Map.empty; out_filename = file }
let close_out { out_channel = ch; out_segments = seg } =
let () = flush ch in
let pos = LargeFile.pos_out ch in
let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in
let iter _ s = output_segment_summary ch s in
let () = CString.Map.iter iter seg in
let () = LargeFile.seek_out ch 8L in
let () = output_int64 ch pos in
let () = flush ch in
close_out ch