RFC: Add support for functions that might panic

[gmorenz]

This adds a new attribute may_panic(condition) in which you can specify conditions under which a function might panic. It compiles this down to a whyml exception, which works to check that that spec is actually followed. The attribute doesn't require that the function panics if the condition is true, it just gives it the option to.

It remains the case that by default a function may not panic - just now because it raises an exception that isn't declared, instead of hitting an absurd.

This probably deserves a fair bit of scrutiny, both from a "is this even a good idea" point of view, as well as from an implementation point of view. I'm not particularly familiar with either creusot or whyml, and it's definitely possible that this isn't as good an idea as it seems to me. I'm also not particularly familiar with the internals I'm modifying, and I may have missed something.

It's also

• [ ] Missing tests (and I've barely tested it manually)
• [ ] In need of at least a few more extern_specs (e.g. for the actual panic function)
• [ ] Unclear if we should consider things like std::process::abort as a panic
• [ ] Adding raises { Panic.Panic -> false } and use prelude.Panic even where those could be omitted (maybe acceptable, it doesn't seem to hurt)
• [ ] Fails to prove if you add #[may_panic(anything_other_than_false)] to functions that don't have a panic somewhere within them (unreachable panics work though), thanks to whyml apparently checking that... I'm not sure what to do about this short of a fairly laborious approach of only emitting the raises attribute if we call something with a raises attribute.

I think it's in a place where it makes sense to ask for feedback on it though - is this something creusot is interested in supporting?

[xldenis]

Hi!

Thanks for this proposal, on the broad strokes I'm not against this, but I do have a key question: when do you envision this being useful? What kinds of properties & programs are you expecting to prove?

With a feature like this we would also need to think through handling of unwind paths, which Creusot currently ignores by compiling with panic=abort.

Fails to prove if you add #[may_panic(anything_other_than_false)] to functions that don't have a panic somewhere within them (unreachable panics work though), thanks to whyml apparently checking that... I'm not sure what to do about this short of a fairly laborious approach of only emitting the raises attribute if we call something with a raises attribute.

A trivial solution would be for may_panic to secretly add an unreachable panic.

This probably deserves a fair bit of scrutiny, both from a "is this even a good idea" point of view, as well as from an implementation point of view.

Indeed, I would like to discuss this with @jhjourdan, but it would be helpful if you had a motivating example to provide.

[gmorenz]

What I'm trying to use it for right now is to prove code correct that in turn proves that certain turing machines don't halt, as part of this. This comes up in two ways

• There's code that I'm fine with it crashing (if it crashes for the right reason, that would even be an interesting result), but I want to prove it isn't returning an incorrect result. It is impractical to prove that the code can't crash, because that would require knowing the value of BB5. Even for places where it is practical to prove it, it is unnecessary, if it does crash I'll find out and fix it. I suspect this part of the motivation generalizes pretty widely to a variety of more common programming tasks.
• I need to impose limits of the size of certain values from a practical perspective (e.g. because I'm using fixed sized ints in the actual implementation), but I don't want to admit to the proof system for deciders that you're only allowed to call machine.step() i32::MAX times. Saying that it might crash if you do that seems like a practical way forward. I'm not sure whether this use case generalizes very much. Edit: And I could probably work around this part if I needed to in other ways.

[jhjourdan]

Hi, thanks for the proposal!

My initial opinion on this was that Creusot should actually not guarantee the absence of panic, but only try to ensure it as a "best effort". While this might be surprising for a verification tool not to guarantee the absence of crash, I think it is actually very natural. Indeed:

• Panics are, in a way "gentle crashes": they should properly free resources, and not cause undefined behaviors.
• In a sense, guaranteeing the absence of panics is a lost cause, since we will never guarantee the absence of stack overflows or out-of-memory conditions.
• There are many cases where we actually want to perform dynamic checks that guarantee the correctness of the result computed by a program, but then what should the program do if such a test fails? Using an error monad everywhere is surely non-optimal, and raising a panic seems to be a good solution when we don't expect the test to fail in practice.

That being said, I know that people disagree with me on this point, and consider this opinion as heretic since "a verification tool should prevent bugs". So, indeed, the option you are proposing seems a good trade-off. We could even improve the spec of e.g., unwrap or array accesses by discarding the bound checking by Creusot if the user does not care about panics.

[gmorenz]

Thanks for the replies :)

With a feature like this we would also need to think through handling of unwind paths, which Creusot currently ignores by compiling with panic=abort.

This is a good point. What I'm proposing does work with panic=abort, but it's not entirely obvious that it can't break things if panic=unwind (especially if panics are caught, but we might have to think about drop handlers as well). It's also not obvious to me that it can break things, I'm just not confident enough in my mental model of creusot to say either way so I probably need to defer to one of you.

Catching panics is a bit of a curious question, because rust doesn't really guarantee that you can catch them. I guess this can be done by modelling panics as "unwind or abort" and having catch_unwind and intrinsics::try say that they may_panic if the function they are called on does, or maybe introduce a second kind of exception for aborts and say they may_abort if the function they are called on may_panic (which goes back to the process::abort question).

In a sense, guaranteeing the absence of panics is a lost cause, since we will never guarantee the absence of stack overflows or out-of-memory conditions.

This is true, unfortunately it's still true with this proposal. Regardless of what a functions may_panic says, stack overflows will always cause it to panic. Theoretically we could handle other OOM conditions by annotating every function that allocates as may_panic(true), but that would make this pretty useless for most programs... I could imagine the same kinds of projects interested in the try_new api's being interested in a flag that does that.

We could even improve the spec of e.g., unwrap

The one example spec change I included in the initial PR is actually this :) Also what I've been using to test with on toy examples.

[xldenis]

My initial opinion on this was that Creusot should actually not guarantee the absence of panic, but only try to ensure it as a "best effort".

know that people disagree with me on this point, and consider this opinion as heretic since "a verification tool should prevent bugs".

While preventing all bugs is a laudable goal, I think it's more important for a verification tool to be clear about what bugs it can prevent, saying 'we prevent X Y & Z under conditions A, B, C' is already a good step forward. More specifically, having some facilities to reason about panics shores up this argument, it allows us to be more precise about what bugs / panics we can prevent and where they can come from. As @gmorenz said, we could even prove the absence of memory allocation panics if we were so inclined.

Anyways, I think you're fine to continue working on this @gmorenz, it seems like there's an agreement that some form of this should be added. We'll see about the details as they come up :)

[gmorenz]

This is still a draft and all the previous caveats still apply (though I've manually tested this locally quite a bit more since when I originally posted about it). The push I just made was mostly just rebasing the previous work on master. No real need to review it further yet.

The only thing that might be worth looking at now is the "Reduce code duplication" commit, that's a bit orthogonal to the rest of this but it becomes more worthwhile with us adding a fourth type of contract term, hence why I'm suggesting including it with the rest.

[xldenis]

The only thing that might be worth looking at now is the "Reduce code duplication" commit, that's a bit orthogonal to the rest of this but it becomes more worthwhile with us adding a fourth type of contract term, hence why I'm suggesting including it with the rest.

I looked at that commit, it seems good, I would encourage you to post it in a separate PR so we can merge it earlier.

[xldenis]

I'm closing this as the branch is stale, it can be re-introduced if the interest is there.