Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cat truncates binary files #255

Closed
hferee opened this issue Mar 23, 2017 · 8 comments

Comments

@hferee
Copy link
Contributor

commented Mar 23, 2017

cake_cat seems to handle text files correctly by truncates some binary files (e.g. cake_cat itself).

My guess is that there is an error in rofsFFI.eof.

@hferee hferee added the bug label Mar 23, 2017
@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 23, 2017

I'm pretty sure the cat example does not use the isEof FFI call at all.

Are any of the other FFI calls implemented incorrectly?

@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 23, 2017

Actually of course it does use isEof in the definition of FileIO.fgetc. So OK, we must examine the implementation of all four FFI calls...

@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 23, 2017

I would propose that the isEof call is removed, though, and instead make fgetc return an error bit (similarly to getChar).

@hferee

This comment has been minimized.

Copy link
Contributor Author

commented Mar 24, 2017

The issue is that eof is mapped to 255w and conversely, 255w is later read as eof, even when it was a genuine 255 byte. I'll try to fix that.

@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 25, 2017

I would suggest you remove the eof ffi call altogether and amend fgetc to be more like getchar (i.e. return a status bit). This is a much better model of what the C library naturally provides.

@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 25, 2017

By the way, the problem can't be in any of the cat or mlfileio functions, and can only be a discrepancy between the four FFI functions defined in rofsFFI and their implementation in basis_ffi.c. Why? Because the top-level theorem for cat talks directly about the whole contents of the files in the filesystem (i.e., it's declarative, not operational). There are no assumptions about those contents not containing 255w bytes. If you can't point to a specific discrepancy between one of the FFI functions and and their C implementations, then I think we might have a serious problem...

hferee added a commit that referenced this issue Mar 27, 2017
@hferee

This comment has been minimized.

Copy link
Contributor Author

commented Mar 27, 2017

The issue was that the result of fgetc was cast to a char in ffiisEof and ffifgetc, forcing EOF (= -1) to be converted to 0x255.

@hferee hferee closed this Mar 27, 2017
@xrchz

This comment has been minimized.

Copy link
Member

commented Mar 27, 2017

Ugh - this "fix" breaks the relationship between the FFI model (in rofsFFI) and the C code. The C function ffifgetc needs to implement the HOL function ffi_fgetc - this is not checked by any proofs but is assumed by all our top-level correctness theorems. It is not at all obvious now that the C function is implementing its specification, indeed it looks like it probably is not.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.