Merge branch 'main' into field-access

source/rust_verify/example/std_test/rc_test.rs

@@ -0,0 +1,44 @@
+use std::rc::Rc;
+
+use vstd::pervasive::runtime_assert;
+use vstd::prelude::*;
+
+verus! {
+
+fn try_unwrap_test() {
+    let r1 = Rc::new(5);
+    let r2 = r1.clone();
+    let result1 = Rc::try_unwrap(r1);
+    assert(result1 is Err ==> result1.unwrap_err() == 5);
+    match result1 {
+        Err(r3) => { runtime_assert(*r3 == 5); },
+        Ok(five) => { assert(five == 5); }, // won't happen
+    };
+    let result2 = Rc::try_unwrap(r2);
+    assert(result2 is Ok ==> result2.unwrap() == 5);
+    match result2 {
+        Err(r4) => { assert(r4 == 5); }, // won't happen
+        Ok(five) => { runtime_assert(five == 5); },
+    }
+
+}
+
+fn into_inner_test() {
+    let r1 = Rc::new(5);
+    let r2 = r1.clone();
+    let result1 = Rc::into_inner(r1);
+    match result1 {
+        Some(five) => {
+            assert(five == 5); // won't happen
+        },
+        None => {
+            let result2 = Rc::into_inner(r2);
+            match result2 {
+                Some(five) => { runtime_assert(five == 5) },
+                None => {},
+            }
+        },
+    }
+}
+
+} // verus!

source/rust_verify/src/config.rs

@@ -10,7 +10,9 @@ pub enum ShowTriggers {
     Silent,
     Selective,
     Module,
+    AllModules,
     Verbose,
+    VerboseAllModules,
 }
 impl Default for ShowTriggers {
     fn default() -> Self {
@@ -256,10 +258,32 @@ pub fn parse_args_with_imports(
         (LOG_CALL_GRAPH, "Log the call graph"),
     ];
 
-    const OPT_TRIGGERS_SILENT: &str = "triggers-silent";
-    const OPT_TRIGGERS_SELECTIVE: &str = "triggers-selective";
     const OPT_TRIGGERS: &str = "triggers";
-    const OPT_TRIGGERS_VERBOSE: &str = "triggers-verbose";
+    const OPT_TRIGGERS_MODE: &str = "triggers-mode";
+
+    const TRIGGERS_MODE_SILENT: &str = "silent";
+    const TRIGGERS_MODE_SELECTIVE: &str = "selective";
+    const TRIGGERS_MODE_ALL_MODULES: &str = "all-modules";
+    const TRIGGERS_MODE_VERBOSE: &str = "verbose";
+    const TRIGGERS_MODE_VERBOSE_ALL_MODULES: &str = "verbose-all-modules";
+
+    const TRIGGERS_MODE_ITEMS: &[(&str, &str)] = &[
+        (TRIGGERS_MODE_SILENT, "Do not show automatically chosen triggers"),
+        (
+            TRIGGERS_MODE_SELECTIVE,
+            "Show automatically chosen triggers for some potentially ambiguous cases in verified modules (this is the default behavior)",
+        ),
+        (
+            TRIGGERS_MODE_ALL_MODULES,
+            "Show all automatically chosen triggers for verified modules and imported definitions from other modules",
+        ),
+        (TRIGGERS_MODE_VERBOSE, "Show all triggers (manually or auto) for verified modules"),
+        (
+            TRIGGERS_MODE_VERBOSE_ALL_MODULES,
+            "Show all triggers (manually or automatically chosen) for verified modules and imported definitions from other modules",
+        ),
+    ];
+
     const OPT_PROFILE: &str = "profile";
     const OPT_PROFILE_ALL: &str = "profile-all";
     const OPT_COMPILE: &str = "compile";
@@ -385,10 +409,20 @@ pub fn parse_args_with_imports(
         "OPTION=VALUE",
     );
 
-    opts.optflag("", OPT_TRIGGERS_SILENT, "Do not show automatically chosen triggers");
-    opts.optflag("", OPT_TRIGGERS_SELECTIVE, "Show automatically chosen triggers for some potentially ambiguous cases in verified modules (this is the default behavior)");
     opts.optflag("", OPT_TRIGGERS, "Show all automatically chosen triggers for verified modules");
-    opts.optflag("", OPT_TRIGGERS_VERBOSE, "Show all automatically chosen triggers for verified modules and imported definitions from other modules");
+    opts.optopt(
+        "",
+        OPT_TRIGGERS_MODE,
+        {
+            let mut s = "Display triggers:\n".to_owned();
+            for (f, d) in TRIGGERS_MODE_ITEMS {
+                s += format!("--{} {} : {}\n", OPT_TRIGGERS_MODE, *f, d).as_str();
+            }
+            s
+        }
+        .as_str(),
+        &TRIGGERS_MODE_ITEMS.iter().map(|(x, _)| x.to_owned()).collect::<Vec<_>>().join("|"),
+    );
     opts.optflag(
         "",
         OPT_PROFILE,
@@ -593,14 +627,20 @@ pub fn parse_args_with_imports(
             log_triggers: log.get(LOG_TRIGGERS).is_some(),
             log_call_graph: log.get(LOG_CALL_GRAPH).is_some(),
         },
-        show_triggers: if matches.opt_present(OPT_TRIGGERS_VERBOSE) {
-            ShowTriggers::Verbose
-        } else if matches.opt_present(OPT_TRIGGERS) {
+        show_triggers: if matches.opt_present(OPT_TRIGGERS) {
+            if matches.opt_present(OPT_TRIGGERS_MODE) {
+                error("--triggers and --triggers-mode are mutually exclusive".to_owned())
+            }
             ShowTriggers::Module
-        } else if matches.opt_present(OPT_TRIGGERS_SELECTIVE) {
-            ShowTriggers::Selective
-        } else if matches.opt_present(OPT_TRIGGERS_SILENT) {
-            ShowTriggers::Silent
+        } else if let Some(triggers_mode) = matches.opt_str(OPT_TRIGGERS_MODE) {
+            match triggers_mode.as_str() {
+                TRIGGERS_MODE_ALL_MODULES => ShowTriggers::AllModules,
+                TRIGGERS_MODE_SELECTIVE => ShowTriggers::Selective,
+                TRIGGERS_MODE_SILENT => ShowTriggers::Silent,
+                TRIGGERS_MODE_VERBOSE_ALL_MODULES => ShowTriggers::VerboseAllModules,
+                TRIGGERS_MODE_VERBOSE => ShowTriggers::Verbose,
+                _ => error(format!("invalid --triggers-mode {triggers_mode}")),
+            }
         } else {
             ShowTriggers::default()
         },

source/rust_verify/src/verifier.rs

@@ -308,9 +308,10 @@ pub struct Verifier {
 fn report_chosen_triggers(
     diagnostics: &impl air::messages::Diagnostics,
     chosen: &vir::context::ChosenTriggers,
+    automatically: bool,
 ) {
-    diagnostics
-        .report(&note(&chosen.span, "automatically chose triggers for this expression:").to_any());
+    let s = if automatically { "automatically chose" } else { "selected" }.to_owned();
+    diagnostics.report(&note(&chosen.span, s + " triggers for this expression:").to_any());
 
     for (n, trigger) in chosen.triggers.iter().enumerate() {
         let note = format!("  trigger {} of {}:", n + 1, chosen.triggers.len());
@@ -1744,7 +1745,9 @@ impl Verifier {
                         }
 
                         if matches!(query_op, QueryOp::Body(Style::Normal)) {
-                            if (any_invalid && !self.args.no_auto_recommends_check)
+                            if (any_invalid
+                                && !self.args.no_auto_recommends_check
+                                && !any_timed_out)
                                 || function.x.attrs.check_recommends
                             {
                                 function_opgen.retry_with_recommends(&op, any_invalid)?;
@@ -1772,7 +1775,9 @@ impl Verifier {
                         }
 
                         if matches!(query_op, QueryOp::SpecTermination) {
-                            if (any_invalid && !self.args.no_auto_recommends_check)
+                            if (any_invalid
+                                && !self.args.no_auto_recommends_check
+                                && !any_timed_out)
                                 || function.x.attrs.check_recommends
                             {
                                 // Do recommends-checking for the body of the function.
@@ -2466,18 +2471,33 @@ impl Verifier {
             match (
                 self.args.show_triggers,
                 modules_to_verify.iter().find(|m| &m.x.path == &chosen.module).is_some(),
+                chosen.manual,
             ) {
-                (ShowTriggers::Selective, true) if chosen.low_confidence => {
-                    report_chosen_triggers(&reporter, &chosen);
+                (ShowTriggers::Selective, true, false) if chosen.low_confidence => {
+                    report_chosen_triggers(&reporter, &chosen, true);
                     low_confidence_triggers = Some(chosen.span);
                 }
-                (ShowTriggers::Module, true) => {
-                    report_chosen_triggers(&reporter, &chosen);
+                (ShowTriggers::Module, true, false) => {
+                    report_chosen_triggers(&reporter, &chosen, true);
                 }
-                (ShowTriggers::Verbose, _) => {
-                    report_chosen_triggers(&reporter, &chosen);
+                (ShowTriggers::AllModules, _, false) => {
+                    report_chosen_triggers(&reporter, &chosen, true);
                 }
-                _ => {}
+                (ShowTriggers::Verbose, true, _) => {
+                    report_chosen_triggers(&reporter, &chosen, !chosen.manual);
+                }
+                (ShowTriggers::VerboseAllModules, _, _) => {
+                    report_chosen_triggers(&reporter, &chosen, !chosen.manual);
+                }
+                (
+                    ShowTriggers::Selective
+                    | ShowTriggers::Module
+                    | ShowTriggers::AllModules
+                    | ShowTriggers::Silent
+                    | ShowTriggers::Verbose,
+                    _,
+                    _,
+                ) => {}
             }
         }
         if let Some(span) = low_confidence_triggers {

source/rust_verify_test/tests/seqs.rs

@@ -119,26 +119,16 @@ test_verify_one_file! {
         use vstd::seq_lib::*;
 
         proof fn test() {
-            // TODO: seq! is currently defined via repeated pushes.
-            // This has sometimes led to Z3 timeouts, including in this test.
-            // It may be time for a more efficient definition of seq!
-            // (for example, via if/else, as shown below).
-            //let s1 = seq![10, 20, 30, 45, 55, 70];
-            let s1 = Seq::new(6, |i: int|
-                if i == 0 { 10 }
-                else if i == 1 { 20 }
-                else if i == 2 { 30 }
-                else if i == 3 { 45 }
-                else if i == 4 { 55 }
-                else { 70 }
-            );
+            let s1 = seq![10, 20, 30, 45, 55, 70];
             let s2 = s1.filter(|x: int| x < 40);
             let s3 = seq![90, 100];
             let s4 = s3.filter(|x: int| x < 40);
-            // Test for successful broadcast of filter_lemma_broadcast
+            // Test for successful broadcast of filter_lemma
             assert(forall|i: nat| i < s2.len() ==> s2[i as int] < 40);
             // Test for successful broadcast of filter_distributes_over_add
             assert((s1 + s3).filter(|x: int| x < 40) == (s2 + s4));
+            // TODO: the following test will verify even if
+            // push_distributes_over_add is not broadcasted.
             // Test for successful broadcast of push_distributes_over_add
             assert((s2 + s4).push(120) == s2 + s4.push(120));
         }

source/rust_verify_test/tests/triggers.rs

@@ -390,3 +390,58 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_self_in_trigger_in_clone_issue1347 verus_code! {
+        use vstd::*;
+        use vstd::prelude::*;
+
+        struct Node {
+            child: Option<Box<Node>>,
+        }
+
+        impl Node {
+            pub spec fn map(self) -> Map<int, int>;
+        }
+
+        impl Clone for Node {
+            fn clone(&self) -> (res: Self)
+                ensures forall |key: int| #[trigger] self.map().dom().contains(key) ==> key == 3
+            {
+                return Node { child: None }; // FAILS
+            }
+        }
+
+        fn test(n: Node) {
+            let t = n.clone();
+            assert(forall |key: int| n.map().dom().contains(key) ==> key == 3);
+        }
+
+        fn test2(n: Node) {
+            let c = Node::clone;
+            let t = c(&n);
+            assert(forall |key: int| n.map().dom().contains(key) ==> key == 3);
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] test_lets_and_nested_quantifiers_issue1347 verus_code! {
+        spec fn llama(x: int) -> int;
+        spec fn foo(x: int, y: int) -> bool;
+        spec fn bar(x: int) -> bool;
+
+        proof fn test() {
+            let b =
+              forall |x: int| #[trigger] bar(x) ==> ({
+                let y = llama(x);
+                forall |z: int| #[trigger] foo(y, z)
+              });
+
+            assume(b);
+            assume(bar(7));
+            assert(foo(llama(7), 20));
+            assert(foo(llama(7), 21));
+        }
+    } => Ok(())
+}

source/state_machines_macros/src/to_token_stream.rs

@@ -301,6 +301,7 @@ pub fn output_primary_stuff(
     let attrs = &bundle.sm.attrs;
     let code: TokenStream = quote_spanned! { sm.fields_named_ast.span() =>
         #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
+        #[cfg_attr(verus_keep_ghost, verifier::ext_equal)]
         #(#attrs)*
         pub struct State #gen {
             #(#fields),*

source/vir/src/context.rs

@@ -31,6 +31,7 @@ pub struct ChosenTriggers {
     pub span: Span,
     pub triggers: Vec<ChosenTrigger>,
     pub low_confidence: bool,
+    pub manual: bool,
 }
 
 /// Context for across all modules