Merge branch 'main' into async

Author: Chris-Hawblitzel

source/cargo-verus/src/subcommands.rs

@@ -246,6 +246,19 @@ fn make_cargo_args(opts: &CargoOptions, for_cargo_metadata: bool) -> Vec<String>
         args.push(path.to_string_lossy().into_owned());
     }
 
+    if opts.features.all_features {
+        args.push("--all-features".to_owned());
+    }
+
+    if opts.features.no_default_features {
+        args.push("--no-default-features".to_owned());
+    }
+
+    if !opts.features.features.is_empty() {
+        args.push("--features".to_owned());
+        args.push(opts.features.features.join(" "));
+    }
+
     if !for_cargo_metadata {
         if let Some(path) = &opts.target_dir {
             args.push("--target-dir".to_owned());
@@ -270,19 +283,6 @@ fn make_cargo_args(opts: &CargoOptions, for_cargo_metadata: bool) -> Vec<String>
             args.push(exclude.clone());
         }
 
-        if opts.features.all_features {
-            args.push("--all-features".to_owned());
-        }
-
-        if opts.features.no_default_features {
-            args.push("--no-default-features".to_owned());
-        }
-
-        if !opts.features.features.is_empty() {
-            args.push("--features".to_owned());
-            args.push(opts.features.features.join(" "));
-        }
-
         args.extend(opts.cargo_args.iter().cloned());
     }
 

source/cargo-verus/src/test_utils.rs

@@ -13,6 +13,7 @@ pub struct MockPackage {
     bin_names: Vec<String>,
     example_names: Vec<String>,
     deps: Vec<(DepKind, Option<String>, MockDep)>,
+    features: Vec<String>,
     verus_verify: Option<bool>,
 }
 
@@ -121,6 +122,7 @@ impl MockPackage {
             bin_names: vec![],
             example_names: vec![],
             deps: vec![],
+            features: vec![],
             verus_verify: None,
         }
     }
@@ -145,6 +147,11 @@ impl MockPackage {
         self
     }
 
+    pub fn features(mut self, names: impl IntoIterator<Item = impl AsRef<str>>) -> Self {
+        self.features.extend(names.into_iter().map(|n| n.as_ref().to_owned()));
+        self
+    }
+
     pub fn deps(mut self, deps: impl IntoIterator<Item = MockDep>) -> Self {
         self.deps.extend(deps.into_iter().map(|d| (DepKind::Normal, None, d)));
         self
@@ -249,6 +256,12 @@ impl MockPackage {
             manifest_lines.push("".to_owned());
         }
 
+        if !self.features.is_empty() {
+            manifest_lines.push("[features]".to_owned());
+            manifest_lines.extend(self.features);
+            manifest_lines.push("".to_owned());
+        }
+
         if let Some(verus_verify) = self.verus_verify {
             manifest_lines.push("[package.metadata.verus]".to_owned());
             manifest_lines.push(format!("verify = {verus_verify}"));

source/cargo-verus/tests/test_late_args.rs

@@ -248,7 +248,8 @@ fn package_before_release_is_ok() {
 #[test]
 fn features_before_release_is_ok() {
     // --features appearing before --release should work fine
-    let package_dir = MockPackage::new("foo").lib().verify(true).materialize();
+    let package_dir =
+        MockPackage::new("foo").lib().verify(true).features(["default=[]"]).materialize();
 
     let (status, _data) = run_cargo_verus(|cmd| {
         cmd.current_dir(&package_dir).arg("verify");

source/rust_verify/src/rust_to_vir_func.rs

@@ -2969,8 +2969,13 @@ pub(crate) fn check_item_const_or_static<'tcx>(
     if header.require.len() + header.recommend.len() > 0 {
         return err_span(span, "consts cannot have requires/recommends");
     }
-    if ret_mode == Mode::Spec && (header.ensure.0.len() > 0 || header.ensure.1.len() > 0) {
-        return err_span(span, "spec consts cannot have ensures");
+
+    let spec_or_dual = ret_mode == Mode::Spec || func_mode == Mode::Spec;
+    if spec_or_dual && (header.ensure.0.len() > 0 || header.ensure.1.len() > 0) {
+        return err_span(span, "const cannot have `ensures` unless it is `exec const`");
+    }
+    if spec_or_dual && header.returns.is_some() {
+        return err_span(span, "const cannot have `returns` unless it is `exec const`");
     }
 
     let ret_name = air_unique_var(RETURN_VALUE);

source/rust_verify_test/tests/consts.rs

@@ -560,3 +560,10 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] const_with_ensures_issue2175 verus_code! {
+        #[verus_spec(ensures true)]
+        pub const C: char = 'x';
+    } => Err(err) => assert_vir_error_msg(err, "const cannot have `ensures` unless it is `exec const`")
+}

source/rust_verify_test/tests/external_traits.rs

@@ -796,3 +796,32 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_impl_trait_direct_use_error verus_code! {
+        #[verifier::external]
+        trait T1 {}
+
+        #[verifier::external]
+        impl T1 for u8 {}
+
+        #[verifier::external_trait_specification]
+        #[verifier::external_trait_extension(T1Spec via T1SpecImpl)]
+        trait ExT1 {
+            type ExternalTraitSpecificationFor: T1;
+
+            spec fn f() -> bool;
+        }
+
+        impl T1SpecImpl for u8 {
+            spec fn f() -> bool { true }
+        }
+
+        spec fn g() -> bool {
+            <u8 as T1SpecImpl>::f() // should error: cannot use T1SpecImpl directly
+        }
+    } => Err(err) => assert_vir_error_msg(
+        err,
+        "cannot use trait `crate::T1SpecImpl` directly; use `crate::T1Spec` instead"
+    )
+}

source/rust_verify_test/tests/state_machines.rs

@@ -76,6 +76,55 @@ test_verify_one_file! {
     } => Err(e) => assert_vir_error_msg(e, "`birds_eye` only makes sense for tokenized state machines")
 }
 
+test_verify_one_file_with_options! {
+    #[test] test_custom_err_on_subexpression_is_inert ["--expand-errors"] => verus_code! {
+        spec fn custom_requires(a: bool, b: bool) -> bool {
+            (#[verifier(custom_err("Custom error on subexpression"))] a) && b
+        }
+
+        fn caller() {
+            assert(custom_requires(1 == 2, true));
+        }
+    } => Err(err) => {
+        assert!(err.errors[0].message.contains("assertion failed"));
+        assert!(!err.errors.iter().any(|diag| {
+            diag.message.contains("Custom error on subexpression")
+                || diag.rendered.contains("Custom error on subexpression")
+        }));
+    }
+}
+
+test_verify_one_file_with_options! {
+    #[test] test_state_machine_req_custom_err_is_inert ["--expand-errors"] => IMPORTS.to_string() + verus_code_str! {
+        state_machine!{ X {
+            fields {
+                pub i: int,
+            }
+
+            transition!{
+                tr() {
+                    require(pre.i > 0);
+                    update i = pre.i + 1;
+                }
+            }
+        }}
+
+        proof fn assert_tr() {
+            let pre = X::State { i: 0 };
+            let post = X::State { i: 1 };
+            X::show::tr(pre, post);
+            assert(X::State::tr(pre, post));
+        }
+    } => Err(err) => {
+        assert!(err.errors[0].message.contains("precondition not satisfied"));
+        assert!(err.errors[1].message.contains("assertion failed"));
+        assert!(!err.errors.iter().any(|diag| {
+            diag.message.contains("cannot prove this condition holds")
+                || diag.rendered.contains("cannot prove this condition holds")
+        }));
+    }
+}
+
 test_verify_one_file! {
     #[test] test_birds_eye_guard IMPORTS.to_string() + verus_code_str! {
         tokenized_state_machine!{ X {

source/vir/src/traits.rs

@@ -24,6 +24,7 @@ fn demote_one_expr(
     traits: &HashSet<Path>,
     internal_traits: &HashSet<Path>,
     extension_traits: &HashSet<Path>,
+    impl_to_spec_traits: &HashMap<Path, Path>,
     funs: &HashSet<Fun>,
     expr: &Expr,
 ) -> Result<Expr, VirErr> {
@@ -45,6 +46,16 @@ fn demote_one_expr(
             args,
             post_args,
         ) if !traits.contains(&get_trait(fun)) || !funs.contains(fun) => {
+            if let Some(spec_trait) = impl_to_spec_traits.get(&get_trait(fun)) {
+                return Err(error(
+                    &expr.span,
+                    format!(
+                        "cannot use trait `{}` directly; use `{}` instead",
+                        path_as_friendly_rust_name(&get_trait(fun)),
+                        path_as_friendly_rust_name(spec_trait),
+                    ),
+                ));
+            }
             let ct = CallTarget::Fun(
                 CallTargetKind::Static,
                 resolved_fun.clone(),
@@ -137,9 +148,11 @@ pub fn demote_external_traits(
         krate.traits.iter().filter(|t| t.x.proxy.is_none()).map(|t| t.x.name.clone()).collect();
     let funs: HashSet<Fun> = krate.functions.iter().map(|f| f.x.name.clone()).collect();
     let mut extension_traits: HashSet<Path> = HashSet::new();
+    let mut impl_to_spec_traits: HashMap<Path, Path> = HashMap::new();
     for t in krate.traits.iter() {
-        if let Some((extension, _)) = &t.x.external_trait_extension {
+        if let Some((extension, imp)) = &t.x.external_trait_extension {
             extension_traits.insert(extension.clone());
+            impl_to_spec_traits.insert(imp.clone(), extension.clone());
         }
     }
 
@@ -232,7 +245,14 @@ pub fn demote_external_traits(
             &mut map,
             &mut (),
             &|_state, _, expr| {
-                demote_one_expr(&traits, &internal_traits, &extension_traits, &funs, expr)
+                demote_one_expr(
+                    &traits,
+                    &internal_traits,
+                    &extension_traits,
+                    &impl_to_spec_traits,
+                    &funs,
+                    expr,
+                )
             },
             &|_state, _, stmt| Ok(vec![stmt.clone()]),
             &|_state, typ| Ok(typ.clone()),