bugfix: unhandled shadow case in get_manual_triggers (#2463)

Author: tjhance

source/rust_verify_test/tests/triggers.rs

@@ -549,3 +549,101 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] issue2342 verus_code! {
+        use vstd::prelude::*;
+
+        #[verifier::inline]
+        spec fn unwrap_or(a: Option<int>, b: int) -> int {
+            match a {
+                Some(x) => x,
+                None => b,
+            }
+        }
+
+        spec fn f(opt: Option<int>, opt2: Option<int>) -> (spec_fn(int) -> bool) {
+            |s: int| {
+                match opt {
+                    Some(x) => {
+                        unwrap_or(opt2, 1) == x
+                    },
+                    None => { false }
+                }
+            }
+        }
+
+        fn test() {
+            assert(f(None, None)(0)); // FAILS
+        }
+
+        fn test2() {
+            assert(f(Some(1), None)(0));
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
+test_verify_one_file! {
+    #[test] issue2342_2 verus_code! {
+        use vstd::prelude::*;
+
+        #[verifier::inline]
+        spec fn unwrap_or(a: Option<int>, b: int) -> int {
+            match a {
+                Some(x) => x,
+                None => b,
+            }
+        }
+
+        spec fn f_quant(opt: Option<int>, opt2: Option<int>) -> bool {
+            forall |s: int| {
+                match opt {
+                    Some(x) => {
+                        unwrap_or(opt2, s) == x
+                    },
+                    None => { false }
+                }
+            }
+        }
+
+        fn test3() {
+            assert(f_quant(Some(2), Some(2)));
+        }
+    } => Err(err) => assert_vir_error_msg(err, "Could not automatically infer triggers for this quantifier")
+}
+
+test_verify_one_file! {
+    #[test] issue2123 verus_code! {
+        use vstd::prelude::*;
+
+        pub enum A {
+            Foo { xyz: Result<(), ()> },
+        }
+
+        pub open spec fn foo(a: A) -> Set<nat> {
+            Set::new(|x: nat| {
+                match a {
+                    A::Foo { xyz, .. } => {
+                        let _ = xyz.ok();
+                        true
+                    },
+                }
+            })
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] trigger_with_mixed_outer_quantifier_inner_closure verus_code! {
+        spec fn foo(y: int, z: int) -> bool { y == z }
+
+        spec fn test(x: int) -> bool {
+            forall |y: int| (|z: int| #[trigger] foo(y, z))(x)
+        }
+    } => Err(err) => {
+        assert!(err.warnings.len() == 1);
+        assert!(err.warnings[0].message.contains("#[trigger] on a spec_fn closure is deprecated"));
+        assert!(err.errors.len() == 1);
+        assert!(err.errors[0].message.contains("Could not automatically infer triggers for this quantifier"));
+    }
+}

source/vir/src/sst_visitor.rs

@@ -26,9 +26,24 @@ pub(crate) trait Scoper {
 pub(crate) struct NoScoper;
 impl Scoper for NoScoper {}
 
-pub type VisitorScopeMap = ScopeMap<VarIdent, bool>;
+pub enum BndKind {
+    Let,
+    Quant,
+    Lambda,
+    Choose,
+    /// Used by a pass in triggers.rs to distinguish trigger variables of interest
+    /// that are bound outside the walked expression.
+    OuterTrigger,
+}
+
+pub(crate) struct ScopeEntry {
+    /// Is this a Quant, Choose, or Let?
+    pub bnd_kind: BndKind,
+}
+
+pub type VisitorScopeMap = ScopeMap<VarIdent, ScopeEntry>;
 
-impl Scoper for ScopeMap<VarIdent, bool> {
+impl Scoper for ScopeMap<VarIdent, ScopeEntry> {
     fn push_scope(&mut self) {
         self.push_scope(true);
     }
@@ -38,17 +53,20 @@ impl Scoper for ScopeMap<VarIdent, bool> {
     }
 
     fn insert_binding_typ(&mut self, binder: &VarBinder<Typ>, bnd_source: &Bnd) {
-        let is_triggered = match bnd_source.x {
-            BndX::Quant(..) | BndX::Choose(..) => true,
-            BndX::Lambda(..) => false,
+        let bnd_kind = match bnd_source.x {
+            BndX::Quant(..) => BndKind::Quant,
+            BndX::Choose(..) => BndKind::Choose,
+            BndX::Lambda(..) => BndKind::Lambda,
             BndX::Let(..) => unreachable!(),
         };
-        let _ = self.insert(binder.name.clone(), is_triggered);
+        let entry = ScopeEntry { bnd_kind: bnd_kind };
+        let _ = self.insert(binder.name.clone(), entry);
     }
 
     fn insert_binding_exp(&mut self, binder: &VarBinder<Exp>, bnd_source: &Bnd) {
         assert!(matches!(bnd_source.x, BndX::Let(..)));
-        let _ = self.insert(binder.name.clone(), true);
+        let entry = ScopeEntry { bnd_kind: BndKind::Let };
+        let _ = self.insert(binder.name.clone(), entry);
     }
 }