3285207 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check file size before reading in readFile

readFile will only read up to the size of the file when it started reading, which means it's total again. fileSize may have overflow issues - later it would be better for this to return an Integer rather than an Int

commit328520780845eacdd3e52ca6c36cf4cc52caafbf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 19 Jun 2016, 12:04 (10 years ago) parent4c83174

4 files changed+64−14

compare with master

unifiedsplit

libs/prelude/Prelude/File.idr+35−11 rts/idris_stdfgn.c+16−3 rts/idris_stdfgn.h+4 src/Idris/Core/Execute.hs+9

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

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

66import Prelude.Monad

77import Prelude.Chars

88import Prelude.Strings

9+import Prelude.Nat

910import Prelude.Cast

1011import Prelude.Bool

1112import Prelude.Basics

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

2627||| An error from a file operation

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

2829-- the values correspond!

29−data FileError = FileReadError

30+

31+data FileError = GenericFileError Int -- errno

32+ | FileReadError

3033 | FileWriteError

3134 | FileNotFound

3235 | PermissionDenied

33− | GenericFileError Int -- errno

3436

3537private

3638strError : Int -> String

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

133135closeFile : File -> IO ()

134136closeFile (FHandle h) = do_fclose h

135137

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+

136154private

137155do_fread : Ptr -> IO' l String

138156do_fread h = prim_fread h

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

233251 return (p > 0)

234252

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

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

237−covering export

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

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.

258+export

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

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

240261 | Left err => return (Left err)

241− c <- readFile' h ""

262+ Right max <- fileSize h

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

264+ c <- readFile' h max ""

242265 closeFile h

243266 return c

244267 where

245− covering

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

247− readFile' h contents =

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

269+ readFile' h max contents =

248270 do x <- fEOF h

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

271+ if not x && max > 0

272+ then do Right l <- fGetLine h

250273 | Left err => return (Left err)

251− readFile' h (contents ++ l)

274+ assert_total $

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

252276 else return (Right contents)

253277

254278||| Write a string to a file

rts/idris_stdfgn.c+16−3

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

66#include <fcntl.h>

77#include <errno.h>

8+#include <sys/stat.h>

89#include <stdio.h>

910#include <time.h>

1011

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

4041 return ferror(f);

4142}

4243

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+

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

4457 FILE* f = (FILE*)h;

4558 if (fputs(str, f)) {

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

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

104117 // Prelude.File

105118 case ENOENT:

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

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

107120 break;

108121 case EACCES:

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

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

110123 break;

111124 default:

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

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

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

114127 break;

115128 }

rts/idris_stdfgn.h+4

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

1212void fileClose(void* h);

1313int fileEOF(void* h);

1414int fileError(void* h);

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

16+int fileSize(void* h);

17+

1518// return 0 on success

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

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

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

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

2124int fpoll(void* h);

2225

26+

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

2428int isNull(void* ptr);

2529void* idris_stdin();

src/Idris/Core/Execute.hs+9

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

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

377377 show handle ++

378378 ". 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?"

379388

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

381390 = case ptr of