Treat arithmetic overflow in non-spec code as an error rather than as uninterpreted #111
Conversation
|
could you explain & document the new ErasureMode and InferMode concepts? What problem are they solving, and how do they solve it? |
source/vir/src/ast_to_sst.rs
Outdated
| @@ -21,6 +21,9 @@ type Arg = (Exp, Typ); | |||
| type Args = Arc<Vec<Arg>>; | |||
|
|
|||
| pub(crate) struct State { | |||
| // View exec/proof code as spec | |||
| // (used for is_const functions, where we let Rust --compile check for overflow) | |||
There was a problem hiding this comment.
Not a huge fan of the idea of relying on --compile for stuff like this. (If I'm a developer, I'd want to get an error for this early, before trying to verify everything else.)
Are there other things we rely on --compile for? Could we make at least make a TODO item to handle this in VIR?
There was a problem hiding this comment.
Ok, this is now fixed.
| // the mode of e + 1 a priori | ||
| // - we check the left side e + 1 before we check the right side s, | ||
| // so when we first reach e + 1, we don't yet know that "<"'s right side is spec | ||
| // Therefore, we use Cell to delay the decision about the erasure expected mode of e + 1. |
There was a problem hiding this comment.
so is it right to say that the "erasure expected mode" is really the actual "final decision" about the mode?
And the mode returned by check_expr is more like a "pre-mode" or an approximation of the mode in some circumstances?
There was a problem hiding this comment.
The mode returned by check_expr is the tightest possible mode that the expression can have (if both exec and spec are possible, return exec). Outer expressions might relax this mode (relax exec to proof, relax exec to spec, or relax proof to spec) via the "subsumption rule" described in https://github.com/Chris-Hawblitzel/rust/wiki/Three-kinds-of-code-...-specification,-proof,-and-executable . This is like subtyping, where a type checker computes the most precise subtype for an expression, but might later relax this type to a supertype like Object.
Because operations like + and < can operate in different modes, there's more than one possible "final decision" that we could choose. The erasure chooses a decision biased towards spec whenever possible in order to erase as much code as possible. So you could call the erasure decision the "final decision" about the mode. The checker doesn't care, but the erasure does.
| // Example: | ||
| // fn test(#[exec] e: u64, #[spec] s: u64) { | ||
| // if e + 1 < s { ... } | ||
| // } |
There was a problem hiding this comment.
I don't wanna hold up the PR with too much design discussion - but I wonder if we should require the user to be explicit in this case? e.g., if they want to create a proof if statement in the middle of exec code, they should have to write it like this:
#[proof] if e + 1 < s { ... }Not just to make the mode-checking code easier, but also to keep user code clearer and more explicit
There was a problem hiding this comment.
Vale does it this way (you have to write "ghost if"). Dafny prefers to infer the ghostness. I think we should have this discussion, but it's a broader discussion. For example, it could be argued that all proof code inside an exec function has to be marked as #[proof], even just calls to lemmas, to make the code easier for people to read and understand. But then again, maybe not. We should probably start a discussion page.
…onst declarations
This should make it easier to diagnose verification failures caused by potential integer overflow. See #45 .