3285207 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check file size before reading in readFile

3285207Edwin Brady10 years ago

libs/prelude/Prelude/File.idr+35−11

compare with master

unifiedsplit

@@ -6,6 +6,7 @@ import Prelude.Maybe

6import Prelude.Monad

7import Prelude.Chars

8import Prelude.Strings

9+import Prelude.Nat

9import Prelude.Cast

10import Prelude.Cast

10import Prelude.Bool

11import Prelude.Bool

11import Prelude.Basics

12import Prelude.Basics

@@ -26,11 +27,12 @@ data File : Type where

26||| An error from a file operation

27||| An error from a file operation

27-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

28-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

28-- the values correspond!

29-- the values correspond!

30+

31+data FileError = GenericFileError Int -- errno

29−data FileError = FileReadError

32+ | FileReadError

30 | FileWriteError

33 | FileWriteError

31 | FileNotFound

34 | FileNotFound

32 | PermissionDenied

35 | PermissionDenied

33− | GenericFileError Int -- errno

35private

37private

36strError : Int -> String

38strError : Int -> String

@@ -133,6 +135,22 @@ export

133closeFile : File -> IO ()

135closeFile : File -> IO ()

134closeFile (FHandle h) = do_fclose h

136closeFile (FHandle h) = do_fclose h

135

137

138+private

139+do_getFileSize : Ptr -> IO Int

140+do_getFileSize h = foreign FFI_C "fileSize" (Ptr -> IO Int) h

141+

142+||| Return the size of a File

143+||| Returns an error if the File is not an ordinary file (e.g. a directory)

144+||| Also note that this currently returns an Int, which may overflow if the

145+||| file is very big

146+export

147+fileSize : File -> IO (Either FileError Int)

148+fileSize (FHandle h) = do s <- do_getFileSize h

149+ if (s < 0)

150+ then do err <- getFileError

151+ return (Left err)

152+ else return (Right s)

153+

136private

154private

137do_fread : Ptr -> IO' l String

155do_fread : Ptr -> IO' l String

138do_fread h = prim_fread h

156do_fread h = prim_fread h

@@ -233,22 +251,28 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

233 return (p > 0)

251 return (p > 0)

234

252

235||| Read the contents of a file into a string

253||| Read the contents of a file into a string

236−-- might be reading something infinitely long like /dev/null ...

254+||| This checks the size of the file before beginning to read, and only

255+||| reads that many bytes, to ensure that it remains a total function if

256+||| the file is appended to while being read.

257+||| Returns an error if filepath is not a normal file.

237−covering export

258+export

238−readFile : String -> IO (Either FileError String)

259+readFile : (filepath : String) -> IO (Either FileError String)

239readFile fn = do Right h <- openFile fn Read

260readFile fn = do Right h <- openFile fn Read

240 | Left err => return (Left err)

261 | Left err => return (Left err)

262+ Right max <- fileSize h

263+ | Left err => return (Left err)

241− c <- readFile' h ""

264+ c <- readFile' h max ""

242 closeFile h

265 closeFile h

243 return c

266 return c

244 where

267 where

245− covering

246− readFile' : File -> String -> IO (Either FileError String)

268+ readFile' : File -> Int -> String -> IO (Either FileError String)

247− readFile' h contents =

269+ readFile' h max contents =

248 do x <- fEOF h

270 do x <- fEOF h

271+ if not x && max > 0

249− if not x then do Right l <- fGetLine h

272+ then do Right l <- fGetLine h

250 | Left err => return (Left err)

273 | Left err => return (Left err)

274+ assert_total $

251− readFile' h (contents ++ l)

275+ readFile' h (max - cast (length l)) (contents ++ l)

252 else return (Right contents)

276 else return (Right contents)

253

277

254||| Write a string to a file

278||| Write a string to a file

rts/idris_stdfgn.c+16−3

@@ -5,6 +5,7 @@

6#include <fcntl.h>

7#include <errno.h>

8+#include <sys/stat.h>

8#include <stdio.h>

9#include <stdio.h>

9#include <time.h>

10#include <time.h>

@@ -40,6 +41,18 @@ int fileError(void* h) {

40 return ferror(f);

41 return ferror(f);

41}

42}

44+int fileSize(void* h) {

45+ FILE* f = (FILE*)h;

46+ int fd = fileno(f);

47+

48+ struct stat buf;

49+ if (fstat(fd, &buf) == 0) {

50+ return (int)(buf.st_size);

51+ } else {

52+ return -1;

53+ }

54+}

55+

43int idris_writeStr(void* h, char* str) {

56int idris_writeStr(void* h, char* str) {

44 FILE* f = (FILE*)h;

57 FILE* f = (FILE*)h;

45 if (fputs(str, f)) {

58 if (fputs(str, f)) {

@@ -103,13 +116,13 @@ VAL idris_mkFileError(VM* vm) {

103 // Make sure this corresponds to the FileError structure in

116 // Make sure this corresponds to the FileError structure in

104 // Prelude.File

117 // Prelude.File

105 case ENOENT:

118 case ENOENT:

106− idris_constructor(result, vm, 2, 0, 0);

119+ idris_constructor(result, vm, 3, 0, 0);

107 break;

120 break;

108 case EACCES:

121 case EACCES:

109− idris_constructor(result, vm, 3, 0, 0);

122+ idris_constructor(result, vm, 4, 0, 0);

110 break;

123 break;

111 default:

124 default:

112− idris_constructor(result, vm, 4, 1, 0);

125+ idris_constructor(result, vm, 0, 1, 0);

113 idris_setConArg(result, 0, MKINT((intptr_t)errno));

126 idris_setConArg(result, 0, MKINT((intptr_t)errno));

114 break;

127 break;

115 }

128 }

rts/idris_stdfgn.h+4

@@ -12,6 +12,9 @@ void* fileOpen(char* f, char* mode);

12void fileClose(void* h);

13int fileEOF(void* h);

14int fileError(void* h);

15+// Returns a negative number if not a file (e.g. directory or device)

16+int fileSize(void* h);

17+

15// return 0 on success

18// return 0 on success

16int idris_writeStr(void*h, char* str);

19int idris_writeStr(void*h, char* str);

17// construct a file error structure (see Prelude.File) from errno

20// construct a file error structure (see Prelude.File) from errno

@@ -20,6 +23,7 @@ VAL idris_mkFileError(VM* vm);

20void* do_popen(const char* cmd, const char* mode);

23void* do_popen(const char* cmd, const char* mode);

21int fpoll(void* h);

24int fpoll(void* h);

26+

23int idris_eqPtr(void* x, void* y);

27int idris_eqPtr(void* x, void* y);

24int isNull(void* ptr);

28int isNull(void* ptr);

25void* idris_stdin();

29void* idris_stdin();

src/Idris/Core/Execute.hs+9

@@ -376,6 +376,15 @@ execForeign env ctxt arity ty fn xs onfail

376 "The argument to fileClose should be a file handle, but it was " ++

377 show handle ++

378 ". Are all cases covered?"

379+ | Just (FFun "fileSize" [(_,handle)] _) <- foreignFromTT arity ty fn xs

380+ = case handle of

381+ EHandle h -> do size <- execIO $ hFileSize h

382+ let res = ioWrap (EConstant (I (fromInteger size)))

383+ execApp env ctxt res (drop arity xs)

384+ _ -> execFail . Msg $

385+ "The argument to fileSize should be a file handle, but it was " ++

386+ show handle ++

387+ ". Are all cases covered?"

379

388

380 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs

389 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs

381 = case ptr of

390 = case ptr of