Vscode Extension Timeout Handling #60
Conversation
src/main.rs
Outdated
| @@ -595,105 +601,137 @@ fn verify_files_main( | |||
|
|
|||
| let mut num_proven: usize = 0; | |||
| let mut num_failures: usize = 0; | |||
| let mut wrapping_up: bool = false; | |||
There was a problem hiding this comment.
Add a comment here saying that this is set to true if we had a timeout and just need to mark all remaining procs as unknown.
src/servers/mod.rs
Outdated
| @@ -72,6 +73,9 @@ pub trait Server: Send { | |||
| result: &mut SmtVcCheckResult<'ctx>, | |||
| translate: &mut TranslateExprs<'smt, 'ctx>, | |||
| ) -> Result<(), ServerError>; | |||
|
|
|||
| // Sends an unknown verification result for the not checked proc with the given span. | |||
There was a problem hiding this comment.
This should probably be a rustdoc comment with ///?
| @@ -720,7 +742,7 @@ fn verify_files_main( | |||
| match res { | |||
| Ok(_) => Ok(()), | |||
| Err(VerifyError::LimitError(_)) | Err(VerifyError::Interrupted) => { | |||
| wrapping_up = true; | |||
| limit_interrupt_error = Some(res.unwrap_err()); | |||
There was a problem hiding this comment.
Why not bind the err in the pattern matching and use that instead of doing res.unwrap_err()?
| Vcgen { tcx, explanation } | ||
| pub fn new( | ||
| tcx: &'tcx TyCtx, | ||
| explanation: Option<VcExplanation>, |
There was a problem hiding this comment.
nit: use order tcx, thenlimits_ref, then the optional explanation
| @@ -504,6 +504,10 @@ fn verify_files_main( | |||
| server: &mut dyn Server, | |||
| user_files: &[FileId], | |||
| ) -> Result<bool, VerifyError> { | |||
| // Limit errors or interrupts are saved here. Then rest of the procs are marked as unknown. | |||
There was a problem hiding this comment.
While this seems to work, I find this somewhat error-prone and ugly. What do you think of this idea: We first register all source units in the server and mark them as unprocessed/unfinished/WIP. Then, when one proc results in a timeout, it is a) easy to mark all others as unknown in the UI, b) easy to identify the culprit (by distinguishing timeout vs unfinished), c) impossible to forget handling the LimitErrors/Interrupted in each loop.
Hopefully that idea can avoid all of those extra match statements that were necessary to introduce in this patch.
| @@ -65,7 +71,12 @@ pub fn pretty_vc_value<'smt, 'ctx>( | |||
| |_ident| expr_true.clone(), | |||
| ); | |||
| let mut res = subst_expr; | |||
| apply_subst(translate.ctx.tcx(), &mut res); | |||
| let deadline = Instant::now() + Duration::from_millis(1); | |||
| let _ = apply_subst( | |||
There was a problem hiding this comment.
Why do you discard the result here? Please add a comment
This PR adds the following features: