Skip to content

Commit 01bf110

Browse files
tjhancetjhance
authored
clean up: well_formed error returns (#2660)
1 parent c0bff71 commit 01bf110

6 files changed

Lines changed: 172 additions & 158 deletions

File tree

‎source/rust_verify/src/verifier.rs‎

Lines changed: 34 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -2814,60 +2814,49 @@ impl Verifier {
28142814
&vir_crate,
28152815
&unpruned_crate,
28162816
&mut *ctxt.diagnostics.borrow_mut(),
2817+
&mut self.deferred_errors,
28172818
&warning_ctx,
28182819
self.args.no_verify,
28192820
self.args.no_cheating,
28202821
);
2821-
let mut first_error: Option<VirErr> = check_crate_result1.err();
2822-
match check_crate_result {
2823-
Ok(check_details) => {
2824-
for (func, failed_proof_notes) in check_details.func_failed_proof_notes {
2825-
self.record_func_failed_proof_notes(
2826-
func,
2827-
failed_proof_notes.into_iter().collect(),
2828-
);
2829-
}
2830-
}
2831-
Err(err) => {
2832-
if first_error.is_none() {
2833-
first_error = Some(err);
2822+
2823+
let check_details = match &check_crate_result {
2824+
Ok(check_details) => check_details,
2825+
Err(e) => &e.check_details,
2826+
};
2827+
for (func, failed_proof_notes) in &check_details.func_failed_proof_notes {
2828+
self.record_func_failed_proof_notes(func.clone(), failed_proof_notes.clone());
2829+
}
2830+
2831+
// Process errors from well_formed checks
2832+
let mut all_wf_errors = vec![];
2833+
if let Err(e) = check_crate_result1 {
2834+
all_wf_errors.push(e);
2835+
}
2836+
if let Err(vir::well_formed::WFErr { errors, boundary_errors, check_details: _ }) =
2837+
check_crate_result
2838+
{
2839+
all_wf_errors.extend(errors);
2840+
for (path, mut err) in boundary_errors.into_iter() {
2841+
let map = ctxt.name_def_id_map.borrow();
2842+
let did = map.get(&path);
2843+
if let Some(did) = did {
2844+
if let Ok(s) = build_boundary_suggestion(&ctxt, *did, &path) {
2845+
err = err.help(format!(
2846+
"The following declaration may resolve this error:\n{}",
2847+
s
2848+
));
2849+
}
28342850
}
2851+
all_wf_errors.push(err);
28352852
}
28362853
}
2854+
if all_wf_errors.len() > 0 {
2855+
return Err((all_wf_errors, ctxt_diagnostics.borrow_mut().drain(..).collect()));
2856+
}
2857+
28372858
for diag in ctxt.diagnostics.borrow_mut().drain(..) {
28382859
match diag {
2839-
vir::ast::VirErrAs::NonBlockingError(err, maybe_p) => {
2840-
// This diagnostic message may be a verification boundary violation.
2841-
// In that case, we want to try to construct a suggestion to deal with the problem.
2842-
2843-
let err = match maybe_p {
2844-
Some(p) => {
2845-
// Try to build a DefId, then check if the corresponding Def is an Adt or Fun-like
2846-
// let did = vir_path_to_def_id(tcx, &ctxt.verus_items, &p);
2847-
let map = ctxt.name_def_id_map.borrow();
2848-
let did = map.get(&p);
2849-
match did {
2850-
Some(did) => match build_boundary_suggestion(&ctxt, *did, &p) {
2851-
Ok(s) => err.help(format!(
2852-
"The following declaration may resolve this error:\n{}",
2853-
s
2854-
)),
2855-
Err(_) => err,
2856-
},
2857-
None => err,
2858-
}
2859-
}
2860-
None => err,
2861-
};
2862-
if first_error.is_none() {
2863-
first_error = Some(err.clone().into())
2864-
} else {
2865-
diagnostics.report_as(&err.to_any(), MessageLevel::Error)
2866-
}
2867-
}
2868-
vir::ast::VirErrAs::NonFatalError(err, _) => {
2869-
self.deferred_errors.push(err);
2870-
}
28712860
vir::ast::VirErrAs::Warning(err) => {
28722861
diagnostics.report_as(&err.to_any(), MessageLevel::Warning)
28732862
}
@@ -2876,9 +2865,6 @@ impl Verifier {
28762865
}
28772866
}
28782867
}
2879-
if let Some(first_error) = first_error {
2880-
return Err((vec![first_error], Vec::new()));
2881-
}
28822868

28832869
let vir_crate =
28842870
vir::autospec::resolve_autospec(&vir_crate).map_err(|e| (vec![e], Vec::new()))?;
@@ -3250,10 +3236,6 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
32503236
vir::ast::VirErrAs::Note(err) => {
32513237
reporter.report_as(&err.to_any(), MessageLevel::Note)
32523238
}
3253-
vir::ast::VirErrAs::NonBlockingError(err, _)
3254-
| vir::ast::VirErrAs::NonFatalError(err, _) => {
3255-
reporter.report_as(&err.to_any(), MessageLevel::Error)
3256-
}
32573239
}
32583240
}
32593241
return rustc_driver::Compilation::Stop;

‎source/rust_verify_test/tests/boundary_suggestions.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ test_verify_one_file! {
1717
bar();
1818
}
1919
}
20-
} => Err(err) => assert_vir_error_msgs(err, &["bar", "foo"])
20+
} => Err(err) => assert_vir_error_msgs(err, &["foo", "bar"])
2121
}
2222
test_verify_one_file! {
2323
#[test] test_assume_specification_simple_suggestion_made code! {

‎source/rust_verify_test/tests/mut_refs_patterns.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3342,6 +3342,7 @@ test_verify_one_file_with_options! {
33423342

33433343
test_verify_one_file_with_options! {
33443344
#[test] not_support_let_pattern_mut_ref_binding_with_or_pat [] => verus_code! {
3345+
use vstd::prelude::*;
33453346
fn test() {
33463347
let x = Some((5, true));
33473348
let Some((ref mut i, true | false)) = x;

‎source/rust_verify_test/tests/safe_api.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,7 @@ test_verify_one_file_with_options! {
243243

244244
test_verify_one_file_with_options! {
245245
#[test] any_returned ["-V check-api-safety"] => verus_code! {
246+
use vstd::prelude::*;
246247
fn foo(y: u32)
247248
requires y > 0
248249
{

‎source/vir/src/messages.rs‎

Lines changed: 4 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -548,51 +548,14 @@ impl MessageX {
548548
}
549549

550550
pub enum MessageAs {
551-
NonBlockingError(Message, Option<crate::ast::Path>),
552-
NonFatalError(Message, Option<crate::ast::Path>),
553551
Warning(Message),
554552
Note(Message),
555553
}
556554

557-
impl MessageAs {
558-
/// Given a primary diagnostic message and an additional message,
555+
impl MessageX {
556+
/// Given a primary error message and an additional error message,
559557
/// fold the spans of the additional message into a new message copied from the original.
560-
pub fn merge(&self, other: &MessageAs) -> MessageAs {
561-
let added_msg = match other {
562-
MessageAs::NonBlockingError(message_x, _)
563-
| MessageAs::NonFatalError(message_x, _)
564-
| MessageAs::Warning(message_x)
565-
| MessageAs::Note(message_x) => message_x,
566-
};
567-
let new_msg_builder = |msg: &Message| {
568-
added_msg.spans.iter().fold(msg.clone(), |acc, v| acc.secondary_span(v))
569-
};
570-
match (self, other) {
571-
(MessageAs::NonBlockingError(orig_msg, p), _) => {
572-
MessageAs::NonBlockingError(new_msg_builder(orig_msg), p.clone())
573-
}
574-
(MessageAs::NonFatalError(orig_msg, p), _) => {
575-
MessageAs::NonFatalError(new_msg_builder(orig_msg), p.clone())
576-
}
577-
(MessageAs::Warning(orig_msg), MessageAs::NonBlockingError(_, p)) => {
578-
MessageAs::NonBlockingError(new_msg_builder(orig_msg), p.clone())
579-
}
580-
(MessageAs::Warning(orig_msg), MessageAs::NonFatalError(_, p)) => {
581-
MessageAs::NonFatalError(new_msg_builder(orig_msg), p.clone())
582-
}
583-
(MessageAs::Warning(orig_msg), _) => MessageAs::Warning(new_msg_builder(orig_msg)),
584-
(MessageAs::Note(orig_msg), MessageAs::NonBlockingError(_, p)) => {
585-
MessageAs::NonBlockingError(new_msg_builder(orig_msg), p.clone())
586-
}
587-
(MessageAs::Note(orig_msg), MessageAs::NonFatalError(_, p)) => {
588-
MessageAs::NonFatalError(new_msg_builder(orig_msg), p.clone())
589-
}
590-
(MessageAs::Note(orig_msg), MessageAs::Warning(..)) => {
591-
MessageAs::Warning(new_msg_builder(orig_msg))
592-
}
593-
(MessageAs::Note(orig_msg), MessageAs::Note(..)) => {
594-
MessageAs::Note(new_msg_builder(orig_msg))
595-
}
596-
}
558+
pub fn merge(self: &Arc<Self>, added_msg: &Message) -> Message {
559+
added_msg.spans.iter().fold(self.clone(), |acc, v| acc.secondary_span(v))
597560
}
598561
}

0 commit comments

Comments
 (0)