report multiple errors from modes.rs (#2771)

Author: tjhance

source/rust_verify/src/verifier.rs

@@ -2857,7 +2857,7 @@ impl Verifier {
         let vir_crate =
             vir::autospec::resolve_autospec(&vir_crate).map_err(|e| (vec![e], Vec::new()))?;
         let (vir_crate, erasure_modes, _read_kind_finals) =
-            vir::modes::check_crate(&vir_crate).map_err(|e| (vec![e], Vec::new()))?;
+            vir::modes::check_crate(&vir_crate).map_err(|es| (es, Vec::new()))?;
 
         self.vir_crate = Some(vir_crate.clone());
         self.warning_ctx = Some(Arc::new(warning_ctx));

source/rust_verify_test/tests/consts.rs

@@ -261,7 +261,10 @@ test_verify_one_file! {
             proof { let x = E; }
             0
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot read static with mode exec")
+    } => Err(err) => assert_vir_error_msgs(err, &[
+        "cannot read static with mode exec",
+        "cannot read static with mode exec",
+    ])
 }
 
 test_verify_one_file! {
@@ -275,7 +278,10 @@ test_verify_one_file! {
             proof { let x = E; }
             0
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot read const with mode exec")
+    } => Err(err) => assert_vir_error_msgs(err, &[
+        "cannot read const with mode exec",
+        "cannot read const with mode exec",
+    ])
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/modes.rs

@@ -484,7 +484,10 @@ test_verify_one_file! {
             }
             assert(e);
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot mutate through a spec-mode mutable reference")
+    } => Err(err) => assert_vir_error_msgs(err, &[
+        "cannot mutate through a spec-mode mutable reference",
+        "mutable borrow is not allowed in spec context",
+    ])
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/mut_refs_modes.rs

@@ -1897,7 +1897,10 @@ test_verify_one_file_with_options! {
             }
             assert(u.u == 20);
         }
-    } => Err(err) => assert_vir_error_msg(err, "cannot mutate exec-mode place in proof-code")
+    } => Err(err) => assert_vir_error_msgs(err, &[
+        "cannot mutate exec-mode place in proof-code",
+        "cannot mutate exec-mode place in proof-code",
+    ])
 }
 
 test_verify_one_file_with_options! {

source/rust_verify_test/tests/mut_refs_old.rs

@@ -374,7 +374,10 @@ test_verify_one_file_with_options! {
             assert(*x == 0 && *old(x) == 5) by(nonlinear_arith)
               requires *x == 0 && *old(x) == 5;
         }
-    } => Err(err) => assert_vir_error_msg(err, "`old` is not supported in `nonlinear_arith` assert")
+    } => Err(err) => assert_vir_error_msgs(err, &[
+        "`old` is not supported in `nonlinear_arith` assert",
+        "`old` is not supported in `nonlinear_arith` assert",
+    ])
 }
 
 test_verify_one_file_with_options! {

source/vir/src/modes.rs

@@ -3630,11 +3630,24 @@ fn check_function(
     function: &mut Function,
     rtypes: &ResolutionTypes,
 ) -> Result<(), VirErr> {
-    // Reset this, we only need it per-function
-    record.type_inv_info = TypeInvInfo { ctor_needs_check: HashMap::new() };
-    record.var_modes = HashMap::new();
-    record.temporary_modes = HashMap::new();
-    record.mut_bor_place_modes = HashMap::new();
+    let Record {
+        // Global fields
+        erasure_modes: _,
+        // Per-function fields
+        type_inv_info,
+        read_kind_finals,
+        var_modes,
+        temporary_modes,
+        infer_spec_for_implicit_reborrows,
+        mut_bor_place_modes,
+    } = record;
+    // Reset the fields that are per-function
+    *type_inv_info = TypeInvInfo { ctor_needs_check: HashMap::new() };
+    *read_kind_finals = HashMap::new();
+    *var_modes = HashMap::new();
+    *temporary_modes = HashMap::new();
+    *infer_spec_for_implicit_reborrows = None;
+    *mut_bor_place_modes = HashMap::new();
 
     let mut fun_typing = typing.push_var_scope();
 
@@ -3837,6 +3850,11 @@ fn check_function(
         let mut body_typing = fun_typing.push_ret_mode(ret_mode);
         let mut body_typing = body_typing.push_block_ghostness(Ghost::of_mode(function.x.mode));
         let mut body_typing = body_typing.push_in_pure(pure_spec_fn);
+        let mut body_typing = if function.x.attrs.atomic {
+            body_typing.push_atomic_insts(Some(AtomicInstCollector::new()))
+        } else {
+            body_typing
+        };
 
         assert!(record.infer_spec_for_implicit_reborrows.is_none());
         record.infer_spec_for_implicit_reborrows = Some(HashMap::new());
@@ -3862,6 +3880,14 @@ fn check_function(
             )?;
         }
 
+        if function.x.attrs.atomic {
+            body_typing
+                .atomic_insts
+                .as_ref()
+                .expect("atomic_insts")
+                .validate(&function.span, ValidateCtx::AtomicFunction)?;
+        }
+
         let borrow_spec = record.infer_spec_for_implicit_reborrows.as_ref().expect("borrow_spec");
         if borrow_spec.len() > 0 {
             let mut functionx = function.x.clone();
@@ -3948,7 +3974,7 @@ fn check_function(
     Ok(())
 }
 
-pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes, ReadKindFinals), VirErr> {
+pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes, ReadKindFinals), Vec<VirErr>> {
     let mut funs: HashMap<Fun, Function> = HashMap::new();
     let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
     for function in krate.functions.iter() {
@@ -3984,33 +4010,33 @@ pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes, ReadKindFinals
         infer_spec_for_implicit_reborrows: None,
         mut_bor_place_modes: HashMap::new(),
     };
-    let mut state = State {
-        vars: ScopeMap::new(),
-        in_forall_stmt: false,
-        in_proof_in_spec: false,
-        block_ghostness: Ghost::Exec,
-        ret_mode: None,
-        atomic_insts: None,
-        in_pure: false,
-        in_assert_query: None,
-    };
-    let mut typing = Typing::new(&mut state);
+
     let mut kratex = (**krate).clone();
     let rtypes = ResolutionTypes::new(&ctxt.datatypes);
+    let mut errors = vec![];
     for function in kratex.functions.iter_mut() {
         ctxt.check_ghost_blocks = function.x.attrs.uses_ghost_blocks;
         ctxt.fun_mode = function.x.mode;
-        if function.x.attrs.atomic {
-            let mut typing = typing.push_atomic_insts(Some(AtomicInstCollector::new()));
-            check_function(&ctxt, &mut record, &mut typing, function, &rtypes)?;
-            typing
-                .atomic_insts
-                .as_ref()
-                .expect("atomic_insts")
-                .validate(&function.span, ValidateCtx::AtomicFunction)?;
-        } else {
-            check_function(&ctxt, &mut record, &mut typing, function, &rtypes)?;
+
+        let mut state = State {
+            vars: ScopeMap::new(),
+            in_forall_stmt: false,
+            in_proof_in_spec: false,
+            block_ghostness: Ghost::Exec,
+            ret_mode: None,
+            atomic_insts: None,
+            in_pure: false,
+            in_assert_query: None,
+        };
+        let mut typing = Typing::new(&mut state);
+
+        if let Err(err) = check_function(&ctxt, &mut record, &mut typing, function, &rtypes) {
+            errors.push(err);
         }
     }
-    Ok((Arc::new(kratex), record.erasure_modes, record.read_kind_finals))
+    if errors.len() > 0 {
+        Err(errors)
+    } else {
+        Ok((Arc::new(kratex), record.erasure_modes, record.read_kind_finals))
+    }
 }