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

Support for FFI-divergence in CF #513

Merged
merged 19 commits into from Aug 22, 2018

Conversation

Projects
None yet
3 participants
@IlmariReissumies
Contributor

IlmariReissumies commented Aug 21, 2018

Among other things, I hope this would allow work on issue #260 to move forward.

Johannes Aaman Pohjola and others added some commits Aug 15, 2018

Johannes Aaman Pohjola
Start updating CF to allow reasoning about FFI divergence
Work in progress -- many proofs in cfScript are currently broken.
Make basis and ffi-divergence play nice together
...at least up to and including TextIOProof.

It's nice to see that, with some minor tweak of xlet_auto
and friends, the proofs in basis require only very minor changes
to account for the addition of FFI divergence --- as should be the case,
since nothing in basis FFI-diverges. Mostly boils down to an extra
xsimpl here and there to discharge trivial ==f> side-conditions
generated by xlet_auto.

Some of the specs of higher-order functions could be generalised to
account for FFI-divergence. For example, the spec of map f xs could
say that it FFI-diverges if some for some x in xs, f(x) FFI-diverges.
However, this is likely to cause nothing but pain for the 99% of use
cases where map does not thus diverge; more thinking needed to determine
when to bother making specs that account for divergence in basis.
Add an FFI call to exit w/ non-zero status
Also add an entry-point for it: Runtime.exit

Reasoning about it in CF works, but with a few silly quirks:
- requires the RUNTIME resource to be present in the assumptions,
  even though the RUNTIME's state is just ().
- the post-condition must mention the empty byte array that was
  allocated in Runtime.exit to make the FFI call

The other option would be to add exit to one of the existing
resources (STDIO, COMMANDLINE) but it doesn't fit very well
thematically in either.
@myreen

This comment has been minimized.

Show comment
Hide comment
@myreen

myreen Aug 16, 2018

Contributor

I don't understand why SEP_EXISTS loc. W8ARRAY loc [] is required.

I'm asking because app specifications allow for unused parts to
be left out from postconditions. That's the purpose of h_g in the
definition of app:
https://github.com/CakeML/cakeml/blob/cf-ffidiv/characteristic/cfAppScript.sml#L21

Contributor

myreen commented on basis/RuntimeProofScript.sml in 6c2a29d Aug 16, 2018

I don't understand why SEP_EXISTS loc. W8ARRAY loc [] is required.

I'm asking because app specifications allow for unused parts to
be left out from postconditions. That's the purpose of h_g in the
definition of app:
https://github.com/CakeML/cakeml/blob/cf-ffidiv/characteristic/cfAppScript.sml#L21

This comment has been minimized.

Show comment
Hide comment
@IlmariReissumies

IlmariReissumies Aug 17, 2018

Contributor

You're right, thanks. Removing it. (The proof then becomes uglier -- it seems the xffi tactic assumes I want to keep the W8ARRAY in the postcondition, which is a reasonable assumption for most FFI calls)

Contributor

IlmariReissumies replied Aug 17, 2018

You're right, thanks. Removing it. (The proof then becomes uglier -- it seems the xffi tactic assumes I want to keep the W8ARRAY in the postcondition, which is a reasonable assumption for most FFI calls)

IlmariReissumies added some commits Aug 17, 2018

Make Runtime.exit spec less messy
Thanks to @myreen for pointing out which parts were unneeded.
Prove a call_main_thm for FFI-diverging program
Todo: one that works for programs that either FFI-diverge or
terminate successfully.
Prove a version of whole_prog_spec_semantics_prog for ffidiv
In the future, it would be much nicer to have a theorem that supports
programs that can either FFI-diverge or terminate normally.
Make whole_prog_thm automation support ffi-diverging programs
The automation checks whether the conclusion of your goal is a
whole_prog_spec or a whole_prog_ffidiv_spec and then uses
slightly different rules in a few steps depending on that.

This mechanism assumes that your CF spec is either a POSTf or a
POSTv -- there is currently no support for things written with POST
that can do either.

However, a simple workaround for this is to prove two specs:
one for POSTf and one for POSTv (under appropriately different
assumptions), call whole_prog_thm separately with the two
corresponding whole_prog_spec thms. Then (if desired) a semantics
theorem about all executions can be constructed from those two
by case analysis.
Make helloErrProg exit with non-zero exit code after printing
This is mainly to make sure that the adaptations to whole_prog_thm
for FFI divergence are visited by regression tests.
@myreen

This comment has been minimized.

Show comment
Hide comment
@myreen

myreen Aug 21, 2018

Contributor

Currently, the exit-with-failure function is called Runtime.exit() in the CakeML basis. To me, this choice of name doesn't signal that the error code will be EXIT_FAILURE on the C side in basis_ffi.c.

I think a name such as Runtime.abort() would be more intuitive. Alternatively, one could have the Runtime.exit function take an argument just like the exit function in C code.

Contributor

myreen commented Aug 21, 2018

Currently, the exit-with-failure function is called Runtime.exit() in the CakeML basis. To me, this choice of name doesn't signal that the error code will be EXIT_FAILURE on the C side in basis_ffi.c.

I think a name such as Runtime.abort() would be more intuitive. Alternatively, one could have the Runtime.exit function take an argument just like the exit function in C code.

@xrchz

This comment has been minimized.

Show comment
Hide comment
@xrchz

xrchz Aug 21, 2018

Member

+1 for exit that takes a status argument.

Member

xrchz commented Aug 21, 2018

+1 for exit that takes a status argument.

Make Runtime.exit take an int argument for the exit code
Also make a Runtime.abort() for exit code 1.

@xrchz xrchz merged commit aaf2ed8 into master Aug 22, 2018

1 check failed

cakeml-regression-test regression test failed
Details

@xrchz xrchz deleted the cf-ffidiv branch Aug 22, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment