forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
fsFFIScript.sml
373 lines (323 loc) · 11.5 KB
/
fsFFIScript.sml
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
(*
Logical model of filesystem and I/O streams
*)
open preamble mlstringTheory cfHeapsBaseTheory MarshallingTheory
val _ = new_theory"fsFFI"
val _ = option_monadsyntax.temp_add_option_monadsyntax();
(* Logical model of filesystem and I/O streams *)
(* regular files and unnamed streams *)
val _ = Datatype` inode = UStream mlstring | File mlstring`
Overload isFile = ``λinode. ∃fnm. inode = File fnm``
val _ = Datatype` mode = ReadMode | WriteMode`;
(* files: a list of file names and their content.
* infds: descriptor * (filename * mode * position)
* numchars: stream of num modeling the nondeterministic output of read and
* write
* maxFD:
* file descriptors are encoded on 8 bytes but there might be OS limits
* so we define this limit as maxFD
* ulimit -n has a usual value of 1024
*)
val _ = Datatype`
IO_fs = <| inode_tbl : (inode # char list) list ;
files : (mlstring # mlstring) list;
infds : (num # (inode # mode # num)) list;
numchars : num llist;
maxFD : num
|>`
val IO_fs_component_equality = theorem"IO_fs_component_equality";
Theorem with_same_numchars:
fs with numchars := fs.numchars = fs
Proof
rw[IO_fs_component_equality]
QED
val get_file_content_def = Define`
get_file_content fs fd =
do
(ino, md, off) <- ALOOKUP fs.infds fd ;
c <- ALOOKUP fs.inode_tbl ino;
return (c, off)
od`
(* find smallest unused descriptor index *)
val nextFD_def = Define`
nextFD fsys = LEAST n. ~ MEM n (MAP FST fsys.infds)
`;
(* adds a new file in infds *)
val openFile_def = Define`
openFile fnm fsys md pos =
let fd = nextFD fsys
in
do
assert (fd <= fsys.maxFD) ;
iname <- ALOOKUP fsys.files fnm;
ALOOKUP fsys.inode_tbl (File iname);
return (fd, fsys with infds := (nextFD fsys, (File iname, md, pos)) :: fsys.infds)
od
`;
val openFileFS_def = Define`
openFileFS fnm fs md pos =
case openFile fnm fs md pos of
NONE => fs
| SOME (_, fs') => fs'
`;
(* adds a new file in infds and truncate it *)
val openFile_truncate_def = Define`
openFile_truncate fnm fsys md =
let fd = nextFD fsys in
do
assert (fd <= fsys.maxFD) ;
iname <- ALOOKUP fsys.files fnm;
ALOOKUP fsys.inode_tbl (File iname);
return (fd, (fsys with infds := (nextFD fsys, (File iname, md, 0)) :: fsys.infds)
with inode_tbl updated_by (AFUPDKEY (File iname) (\x."")))
od `;
(* checks if a descriptor index is in infds *)
val validFD_def = Define`
validFD fd fs ⇔ fd ∈ FDOM (alist_to_fmap fs.infds)
`;
(* increase by n the position in file descriptor and dump numchar's head *)
val bumpFD_def = Define`
bumpFD fd fs n = (fs with infds updated_by (AFUPDKEY fd (I ## I ## ((+) n))))
with numchars := THE(LTL fs.numchars)`
(* reads several chars and update position *)
val read_def = Define`
read fd fs n =
do
(ino, md, off) <- ALOOKUP fs.infds fd ;
assert (md = ReadMode) ;
content <- ALOOKUP fs.inode_tbl ino ;
strm <- LHD fs.numchars;
let k = MIN n (MIN (LENGTH content - off) (SUC strm)) in
return (TAKE k (DROP off content), bumpFD fd fs k)
od `;
(* replaces the content of the file in fs with filename fnm,
* set the position in the file and skip k fsnumchars elements*)
val fsupdate_def = Define`
fsupdate fs fd k pos content =
case ALOOKUP fs.infds fd of NONE => fs | SOME (fnm,_) =>
(fs with <| inode_tbl := AFUPDKEY fnm (K content) fs.inode_tbl;
numchars := THE (LDROP k fs.numchars);
infds := (AFUPDKEY fd (I ## I ## (K pos))) fs.infds|>)`;
(* "The write function returns the number of bytes successfully written into the
* array, which may at times be less than the specified nbytes. It returns -1 if
* an exceptional condition is encountered." *)
(* can it be 0? *)
val write_def = Define`
write fd n chars fs =
do
(ino, md, off) <- ALOOKUP fs.infds fd ;
assert(md = WriteMode) ;
content <- ALOOKUP fs.inode_tbl ino ;
assert(n <= LENGTH chars);
assert(fs.numchars <> [||]);
strm <- LHD fs.numchars;
let k = MIN n strm in
(* an unspecified error occurred *)
return (k, fsupdate fs fd 1 (off + k)
(TAKE off content ++
TAKE k chars ++
DROP (off + k) content))
od `;
(* remove file from infds *)
val closeFD_def = Define`
closeFD fd fsys =
do
(fnm, md, off) <- ALOOKUP fsys.infds fd ;
assert (isFile fnm) ;
return ((), fsys with infds := ADELKEY fd fsys.infds)
od
`;
(* Specification of the FFI functions operating on the above model:
- open_in
- open_out
- read
- write
- close
*)
(* truncate byte list after null byte and convert into char list *)
val getNullTermStr_def = Define`
getNullTermStr (bytes : word8 list) =
let sz = findi 0w bytes
in
if sz = LENGTH bytes then NONE
else SOME(MAP (CHR o w2n) (TAKE sz bytes))
`;
(* read file name from the first non null bytes
* open the file with read access
* return result code in first byte
* write its file descriptor index in the second byte *)
val ffi_open_in_def = Define`
ffi_open_in (conf: word8 list) bytes fs =
do
assert(9 <= LENGTH bytes);
fname <- getNullTermStr conf;
(fd, fs') <- openFile (implode fname) fs ReadMode 0;
return (FFIreturn (0w :: n2w8 fd ++ DROP 9 bytes) fs')
od ++
do
assert(0 < LENGTH bytes);
return (FFIreturn (LUPDATE 1w 0 bytes) fs)
od`;
(* open append:
contents <- ALOOKUP fs.inode_tbl (implode fname);
(fd, fs') <- openFile (implode fname) fs (LENGTH contents);
*)
(* open for writing
* position: the beginning of the file.
* The file is truncated to zero length if it already exists.
* TODO: It is created if it does not already exists.*)
val ffi_open_out_def = Define`
ffi_open_out (conf: word8 list) bytes fs =
do
assert(9 <= LENGTH bytes);
fname <- getNullTermStr conf;
(fd, fs') <- openFile_truncate (implode fname) fs WriteMode;
assert(fd <= 255);
return (FFIreturn (0w :: n2w8 fd ++ DROP 9 bytes) fs')
od ++
do
assert(0 < LENGTH bytes);
return (FFIreturn (LUPDATE 1w 0 bytes) fs)
od`;
(*
* [descriptor index (8 bytes); number of char to read (2 bytes); buffer]
* -> [return code; number of read chars (2 bytes); read chars]
* corresponding system call:
* ssize_t read(int fd, void *buf, size_t count) *)
val ffi_read_def = Define`
ffi_read (conf: word8 list) bytes fs =
(* the buffer contains at least the number of requested bytes *)
case bytes of
| (n1 :: n0 :: pad1 :: pad2 :: tll) =>
do
assert(LENGTH conf = 8);
assert(LENGTH tll >= w22n [n1; n0]);
(l, fs') <- read (w82n conf) fs (w22n [n1; n0]);
(* return ok code and list of chars
* the end of the array may remain unchanged *)
return (FFIreturn
(0w :: n2w2 (LENGTH l) ++ [pad2] ++
MAP (n2w o ORD) l ++
DROP (LENGTH l) tll)
fs')
od ++ return (FFIreturn (LUPDATE 1w 0 bytes) fs)
(* inaccurate: "when an error occurs, [...]
* it is left unspecified whether the file position (if any) changes. *)
| _ => NONE`
(* [descriptor index; number of chars to write; chars to write]
* -> [return code; number of written chars]
* corresponding system call:
* ssize_t write(int fildes, const void *buf, size_t nbytes) *)
val ffi_write_def = Define`
ffi_write (conf:word8 list) bytes fs =
case bytes of
| (n1 :: n0 :: off1 :: off0 :: tll) =>
do
(* the buffer contains at least the number of requested bytes *)
assert(LENGTH conf = 8);
assert(LENGTH tll >= w22n [off1; off0]);
(nw, fs') <- write (w82n conf) (w22n [n1; n0])
(MAP (CHR o w2n) (DROP (w22n [off1; off0]) tll)) fs;
(* return ok code and number of bytes written *)
return (FFIreturn (0w :: n2w2 nw ++ (off0 :: tll)) fs')
(* return error code *)
od ++ return (FFIreturn (LUPDATE 1w 0 bytes) fs)
| _ => NONE`;
(* closes a file given its descriptor index *)
val ffi_close_def = Define`
ffi_close (conf:word8 list) (bytes: word8 list) fs =
do
assert(LENGTH bytes >= 1);
assert(LENGTH conf = 8);
do
(_, fs') <- closeFD (w82n conf) fs;
return (FFIreturn (LUPDATE 0w 0 bytes) fs')
od ++
return (FFIreturn (LUPDATE 1w 0 bytes) fs)
od`;
(* given a file descriptor and an offset, returns 0 and update fs or returns 1
* if an error is met val ffi_seek = Define`
ffi_seek bytes fs =
do
assert(LENGTH bytes = 2);
do
fs' <- seek (w2n (HD bytes)) fs (w2n (HD (TL bytes)));
return(LUPDATE 0w 0 bytes, fs')
od ++
return (LUPDATE 1w 0 bytes, fs)
od`; *)
(* -- *)
(* Packaging up the model as an ffi_part *)
val encode_inode_def = Define`
(encode_inode (UStream s) = Cons (Num 0) ((Str o explode) s)) /\
encode_inode (File s) = Cons (Num 1) ((Str o explode) s)`;
val encode_inode_tbl_def = Define`
encode_inode_tbl tbl = encode_list (encode_pair encode_inode Str) tbl`;
val encode_mode_def = Define`
(encode_mode ReadMode = Num 0) ∧
(encode_mode WriteMode = Num 1)`;
val encode_fds_def = Define`
encode_fds fds =
encode_list (encode_pair Num (encode_pair encode_inode (encode_pair encode_mode Num))) fds`;
val encode_files_def = Define`
encode_files fs = encode_list (encode_pair (Str o explode) (Str o explode)) fs`;
val encode_def = zDefine`
encode fs = Cons
(Cons
(cfFFIType$Cons
(cfFFIType$Cons
(encode_inode_tbl fs.inode_tbl)
(encode_fds fs.infds))
(Stream fs.numchars))
(encode_files fs.files))
(Num fs.maxFD)`
Theorem encode_inode_11[simp]:
!x y. encode_inode x = encode_inode y <=> x = y
Proof
Cases \\ Cases_on `y` \\ fs [encode_inode_def,explode_11]
QED
Theorem encode_inode_tbl_11[simp]:
!xs ys. encode_inode_tbl xs = encode_inode_tbl ys <=> xs = ys
Proof
rw [] \\ eq_tac \\ rw [encode_inode_tbl_def]
\\ drule encode_list_11
\\ fs [encode_pair_def,FORALL_PROD,encode_inode_def]
QED
Theorem encode_mode_11[simp]:
∀x y. encode_mode x = encode_mode y ⇔ x = y
Proof
Cases \\ Cases \\ rw[encode_mode_def]
QED
Theorem encode_fds_11[simp]:
!xs ys. encode_fds xs = encode_fds ys <=> xs = ys
Proof
rw [] \\ eq_tac \\ rw [encode_fds_def]
\\ drule encode_list_11
\\ fs [encode_pair_def,FORALL_PROD,encode_inode_def]
QED
Theorem encode_files_11[simp]:
!xs ys. encode_files xs = encode_files ys <=> xs = ys
Proof
rw [] \\ eq_tac \\ rw [encode_files_def]
\\ drule encode_list_11
\\ fs [encode_pair_def,FORALL_PROD]
QED
Theorem encode_11[simp]:
!x y. encode x = encode y <=> x = y
Proof
fs [encode_def] \\ rw [] \\ eq_tac \\ rw []
\\ fs [IO_fs_component_equality]
QED
val decode_encode = new_specification("decode_encode",["decode"],
prove(``?decode. !cls. decode (encode cls) = SOME cls``,
qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]));
val _ = export_rewrites ["decode_encode"];
val fs_ffi_part_def = Define`
fs_ffi_part =
(encode,decode,
[("open_in",ffi_open_in);
("open_out",ffi_open_out);
("read",ffi_read);
("write",ffi_write);
("close",ffi_close)])`;
val _ = export_theory();