[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