Implement get models #96
Conversation
The steps should be separated back into functions, this is just for my understanding
| 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.
| .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.
| slicing::{wrap_with_error_message, wrap_with_success_message}, | ||
| }; | ||
|
|
||
| /// Encode the preexpectations as a formula for which a model is a nontrivial bound |
There was a problem hiding this comment.
Dot at end of sentence, and empty line afterward :)
| }; | ||
| let mut block = Spanned::new(body.span, vec![]); | ||
|
|
||
| fn get_combination(direction: Direction) -> ast::expr::BinOpKind { |
There was a problem hiding this comment.
Import BinOpKind normally
| } | ||
|
|
||
| // 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.
|
|
||
| // Turn quantitative formula into a Boolean one | ||
| let builder = ExprBuilder::new(Span::dummy_span()); | ||
| let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); |
There was a problem hiding this comment.
Move the top/bot assignments into the branches below?
| } | ||
| }; | ||
|
|
||
| // 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 :)
| Lsp(VerifyCommand), | ||
| /// Generate shell completions for the Caesar binary. | ||
| ShellCompletions(ShellCompletionsCommand), | ||
| /// Get non-trivial models for preexpectation. |
There was a problem hiding this comment.
"Compute a non-trivial model for the preconditions of each (co)proc."
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.