Add add option for running why3 though cargo creusot CLI

[dewert99]

I added an experimental --why3 <CMD> flag to to cargo creusot which cause Creusot to run Why3 on the generated mlcfg (automatically including the mlcfg file).
Example usages:
cargo creusot --why3 "prove" TODO, should give a nice error requiring a prover/driver but currently gives a parse error
cargo creusot --why3 "prove -P z3 -a split-vc": Runs Creusot and Why3 prove and reports verifications failures as Rust errors usually pointing to appropriate spans, (TODO issue with spans from inside macros)
cargo creusot --why3 "prove -P z3-ce -a split-vc": Like above but also prints counter examples in a pseudo-Rust syntax (TODO this could be improved by mapping why3 paths to Rust paths).
TODO I'm currently using a hack in printer.rs to get some spans for assignments but this should also be improved
cargo creusot --why3 "ide": Runs creusot and then opens the Why3 ide, (TODO spans don't work because of how I'm using them for "prove" and I need to handle them differently).

[xldenis]

I like this, we've also discussed a project a while ago to have an engineer link why3 directly into cargo creusot, but this gets us 80% there.

[dewert99]

I improved the spans reported by making sure each mlcfg assignment has an associated span, and each mlcfg abort terminator comes directly after asserting false with an appropriate span. I also fixed the issue with spans in macros (but this required adding an extra field to the translation context. I think I was wrong before about the spans when using --why3 "ide", and the problem actually has to do with how Creusot handles relative spans when not using the --ouput-path option (Although I may be able to fix this here or in another PR). Mapping Why3 paths to Rust paths will probably have to wait until the CloneMap conversion process done.

The couterexamples are also somewhat buggy but I think has more to do with Why3 than my changes. Why3 doesn't seem to include values of polymorphic types in its counter examples. It also seems to have z3 run (check-sat) twice (the first time before adding all of the relevant asserions) and then combines counterexamples causing some values to get multiple assignments where some are incorrect.

Do you think this is still useful enough to merge into Creusot in this state? Should I try to fix the issue with relative spans when not using --output-path first?

[xldenis]

Can you explain the purpose of these specific spans? I can be sold on special casing these, but if possible it would be nice to recover the span from a surrounding Expr, Statement or Terminator.

[xldenis]

I also fixed the issue with spans in macros (but this required adding an extra field to the translation context

Oh, with invariant? That's fantastic!

I improved the spans reported by making sure each mlcfg assignment has an associated span, and each mlcfg abort terminator comes directly after asserting false with an appropriate span

I noticed. I'm fine with starting with this, but I'd like to push the spans into proper fields in a follow up, copying the structure of MIR (more generally fMIR needs some cleanup / love).

Mapping Why3 paths to Rust paths will probably have to wait until the CloneMap conversion process done.

I'm getting close, all tests compile to MLCFG, and ~30% are still failing during Why3 typechecking. I'm co-chairing at POPL this week but I expect it to be merged sometime the week after.

Should I try to fix the issue with relative spans when not using --output-path first?

I'm not sure what these issues are and how crippling they are. I'm generally a fan of smaller PRs anyways, so I'd lean to merge and fix afterwards.

[xldenis]

Overall, I'm positive about this work, but ideally, I'd like the spans in fMIR to be handled in a more principled manner.

[dewert99]

Overall, I'm positive about this work, but ideally, I'd like the spans in fMIR to be handled in a more principled manner.

It seems like in MIR spans are attached to Statements and Terminators, but not to RValues Operands or Places, since an fMIR Expr seems to correspond to a MIR RValue or Operand, I would think that maybe it shouldn't get a span. Instead I would think that fMIR Statement::Assign could have a span since it seems like it is the only fMIR Statement to come from a MIR Statement. Does this seem like a reasonable approach?

[xldenis]

Yes this is reasonable. In general our expressions can correspond to multiple rust statements (due to simplifications or optimizations) so it will probably still make sense to have spans on them.

[dewert99]

I modified span_attr to return None when converting DUMMY_SPAN since I think an mlcfg span is still better that span that was being produced before since it gives more information. Does this seem okay?

[xldenis]

Yes, st the very least this gives us indication of where we can improve things.

[xldenis]

Thanks

[xldenis]

? I don't understand this?

[dewert99]

If I didn't add this, Rust wasn't able to infer the type for

    let mut v = args.into_iter().map(|x| P(x)).collect();

The type is supposed to be ThinVec but it isn't pub used in rustc so I couldn't just do let mut v: ThinVec<_> = ...

[xldenis]

cargo creusot --why3 "prove"

Can we upgrade the cargo creusot argument parser here to improve the experience? Something like

cargo creusot why3 prove ?

[dewert99]

Can we upgrade the cargo creusot argument parser here to improve the experience? Something like
cargo creusot why3 prove ?

Maybe somewhat, but I think it is good to be able to send arbitrary options to Why3.
We could potentially have for example cargo creusot why3-prove "-P z3 -a split-vc" if you think that would be better.

[xldenis]

I do, but we can also do that in a follow up.

[jhjourdan]

Many thanks, David, for all the hard work! All in all, I am quite happy with these changes.

There is one thing with which I am not very comfortable in this PR. "why3 prove" is usually not the recommended work flow for using Why3 : the generated VCs often require a few transformations (a series of split_vc / use_th are quite common). While I think it is fine to offer a cargo command for "why3 prove", I think that we should also offer one for "why3 ide" (which you already did), and "why3 replay", the two commands mainly used in the session-based work flow.

[dewert99]

I think that we should also offer one for "why3 ide" (which you already did), and "why3 replay", the two commands mainly used in the session-based work flow.

Would you like me to add "why3 replay" to this PR, or wait for the follow up where I'll switch --why3 "prove .." to --why3-prove "" and then I can add --why3-replay?

[xldenis]

I think we can wait for the follow up, and in case you aren't aware, there is a plan to add why3 play which would be a version of prove with support for sessions and strategies.

[dewert99]

Is there anything I should still do before you merge this PR? (aside from merging and blessing)

[xldenis]

I think we can do other work in follow ups

[dewert99]

I merged and blessed the latest changes. Would you be ok to fix the Why3 sessions and merge this?

[xldenis]

sure, but note that 99% of these can be fixed via cargo test --test why3 -- --replay=obsolete the remaining 1% should as well but sometimes why3 refuses it.

[xldenis]

I'm going to merge this.

In a follow up PR it would be good to see why3_cmd exploded into a subcommand using Clap, so that we can get proper parsing and validation of the commands. At the same time we can offer a command that recognizes strategies using play / replay as appropriate.

Once we've figured out the correct workflow and options, I'd like to eventually just have cargo creusot prove (or even cargo creusot if we're being crazy) which 'does the thing'.