Conversation
The steps should be separated back into functions, this is just for my understanding
Philipp15b
left a comment
Philipp15b
left a comment
There was a problem hiding this comment.
I think this looks great! I have a bunch of (mostly) minor comments.
src/driver/core_verify.rs
Outdated
| pub fn from_source_unit( | ||
| mut source_unit: SourceUnit, | ||
| depgraph: &mut DepGraph, | ||
| is_get_model_task: bool, |
There was a problem hiding this comment.
This anonymous boolean flag is definitely problematic. Especially because it changes the whole interpretation and guarantees about this object. I recommend:
- Renaming this struct to something like
CoreHeyvlTask(and renaming the file and variable names accordingly) - Having two separate constructors for this object; one is basically the old
from_source_unit(maybe calledfrom_proc_verify), the other would be smth likefrom_proc_pre_model). - Possibly refactor a bit so that the common code is in common functions (esp. the bit about depgraphs).
| Ok(result.prove_result) | ||
| } | ||
|
|
||
| pub fn run_smt_check_sat<'tcx>( |
There was a problem hiding this comment.
A short comment would be great.
src/driver/smt_proof.rs
Outdated
| .local_scope() | ||
| .add_assumptions_to_prover(&mut prover); | ||
|
|
||
| // Add the verification condition |
There was a problem hiding this comment.
A short comment explaining that the verification condition is intentionally added as an assumption instead of an assertion as usually done for verification would be great.
There was a problem hiding this comment.
I am not sure I understand this correctly.
add_assumption adds the value as an assert to the solver. And there is no add_assertion function (or something like it) in the prover struct, as far as I can tell. Maybe the function should be renamed?
There was a problem hiding this comment.
The alternative would be add_provable (which I meant by add_assertion). But I think you want add_assumption.
src/procs/proc_verify.rs
Outdated
| } | ||
|
|
||
| // connect the preexpectations through the correct operator | ||
| let mut build_expr = proc |
There was a problem hiding this comment.
Why not just use a reduce? That seems much simpler and less error-prone
| // Unfolding (applies substitutions) | ||
| quant_task.unfold(options, &limits_ref, &tcx)?; | ||
|
|
||
| // TODO: How to deal with inf/sup quantifier? |
There was a problem hiding this comment.
I guess if the SMT encoder is properly used, then sup/inf will be correctly encoded. Most likely the SMT solver would fail to terminate though.
| } | ||
| }; | ||
|
|
||
| // Create a Boolean verification task with the comparison |
There was a problem hiding this comment.
I think a BoolVcProveTask was intended to be used only in the context of verification (i.e. vc == top/bot), but the operations should be sound here as well, because they're all equivalence transformations (I think).
Please make a note of this in the PR description, I'll refactor that at some point :)
This struct now has two constructors so that it can be used for both verify and pre-model tasks.
2 participants
This adds a command (
get-pre-models) to check whether there are non-trivial models for the preexpectations. For coprocs, this means models where the pre evaluates to < infinity, and for procs, models where the pre evaluates to > 0.The implementation is very similar to that of the
verifycommand.Note:
BoolVcProveTaskis used here not for a verification task, but for a formula that will be checked for satisfiability. This should be refactored at some point.