[CakeML-dev] ROFS FFI

Hugo Férée H.Feree at kent.ac.uk
Mon Mar 27 17:01:34 UTC 2017



Le 27/03/2017 à 17:45, Ramana Kumar a écrit :
> OK great! Thanks Hugo for looking into this on the new branch and moving
> towards removing the eof FFI call. I also think that's the right way to go.
> 
> By the way I'm curious about what was wrong with the C code when #255
> was open. I don't think we identified a discrepancy between the FFI
> model and the implementation, which is a little disturbing.
That's apparently a very common C mistake: fgetc outputs an int, which
can represent a char, or EOF. And EOF is encoded as -1, so if you cast
this into a char, EOF becomes 255. Thus, (c = fgetc(...)) == EOF becomes
true when the genuine 255 char is read.

> 
> On 27 Mar 2017 16:44, "Hugo Férée" <H.Feree at kent.ac.uk
> <mailto:H.Feree at kent.ac.uk>> wrote:
> 
>     Hi Ramana,
> 
> 
> 
>     Le 27/03/2017 à 15:26, Ramana Kumar a écrit :
>     > Hi all,
>     >
>     > If you've been following the comments on this issue:
>     >
>     > https://github.com/CakeML/cakeml/issues/255
>     <https://github.com/CakeML/cakeml/issues/255>
>     >
>     > You may have noticed that there are some problems with our read only
>     > file system model and its implementation in C. I'd like to open this
>     > discussion up to more people, because I think maybe Hugo and I
>     disagree
>     > or have misunderstood each other.
>     I think we understood each other, it's just that I wanted to fix the
>     issue illustrated by cat first.
>     I pushed two 1-line commits:
>     a) casts the char read by fgetc to int
>     b) removes the EOF check in the ffi for fgetc because this check is done
>     twice.
> 
>     >
>     > Specifically what I would like is comments on the following two items:
>     >
>     > 1. Should we remove the isEof FFI call for the filesystem? For
>     stdin we
>     > removed this kind of call, because it's not natural in C, and instead
>     > made getc return a status bit.
>     I agree. It would be somehow closer to the behaviour of fgetc in C.
>     >
>     > 2. Can someone with a fresh pair of eyes check the correspondence
>     > between the FFI model in rofsFFITheory and the C functions that are
>     > supposed to implement it in basis_ffi.c? My impression is that Hugo's
>     > latest changes break the correspondence.
>     b) probably broke that, yes. I'll make a "ffieof" branch to fix that.
>     >
>     > An addendum to point 1, which I think Scott has advocated
>     previously, is
>     > should we move to a more uniform I/O model in which both file
>     > descriptors and stream descriptors are treated the same? So
>     putchar and
>     > fputc could be modelled by exactly the same HOL function, for example.
>     > (I think this requires a more substantial redesign of the FFI models.)
>     I agree. This would also be the case for writing to stderr.
>     >
>     > Cheers,
>     > Ramana
>     >
>     >
>     > _______________________________________________
>     > Developers mailing list
>     > Developers at cakeml.org <mailto:Developers at cakeml.org>
>     > https://lists.cakeml.org/listinfo/developers
>     <https://lists.cakeml.org/listinfo/developers>
>     >
> 
>     _______________________________________________
>     Developers mailing list
>     Developers at cakeml.org <mailto:Developers at cakeml.org>
>     https://lists.cakeml.org/listinfo/developers
>     <https://lists.cakeml.org/listinfo/developers>
> 
> 



More information about the Developers mailing list