Support for Primitive Proptests

Cargo.lock

@@ -588,6 +588,13 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "proptest"
+version = "0.1.0"
+dependencies = [
+ "kani",
+]
+
 [[package]]
 name = "pulldown-cmark"
 version = "0.9.1"

Cargo.toml

@@ -38,6 +38,7 @@ strip = "debuginfo"
 members = [
   "library/kani",
   "library/std",
+  "library/proptest",
   "tools/bookrunner",
   "tools/compiletest",
   "tools/make-kani-release",

kani-compiler/build.rs

@@ -66,4 +66,5 @@ pub fn main() {
     setup_lib(&out_dir, &lib_out, "kani_macros");
     setup_lib(&out_dir, &lib_out, "std");
     println!("cargo:rustc-env=KANI_LIB_PATH={}", lib_out);
+    println!("cargo:rustc-env=TARGET={}", env::var("TARGET").unwrap());
 }

kani-compiler/src/main.rs

@@ -47,6 +47,11 @@ fn rustc_gotoc_flags(lib_path: &str) -> Vec<String> {
     // for more details.
     let kani_std_rlib = PathBuf::from(lib_path).join("libstd.rlib");
     let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
+
+    let build_target = env!("TARGET"); // see build.rs
+    let kani_extern_lib_path =
+        PathBuf::from(lib_path).join(format!("../../../../../{}/debug/deps", build_target));
+
     let args = vec![
         "-C",
         "overflow-checks=on",
@@ -65,12 +70,19 @@ fn rustc_gotoc_flags(lib_path: &str) -> Vec<String> {
         "crate-attr=feature(register_tool)",
         "-Z",
         "crate-attr=register_tool(kanitool)",
+        // Prints expanded macro. For proptest devops only, remove after done
+        // "-Z",
+        // "unpretty=expanded",
         "-L",
         lib_path,
         "--extern",
         "kani",
         "--extern",
         kani_std_wrapper.as_str(),
+        "-L",
+        kani_extern_lib_path.to_str().unwrap(),
+        "--extern",
+        "proptest",
     ];
     args.iter().map(|s| s.to_string()).collect()
 }

kani-driver/build.rs

@@ -9,5 +9,9 @@ fn main() {
     // https://doc.rust-lang.org/cargo/reference/environment-variables.html#environment-variables-cargo-sets-for-crates
     // https://doc.rust-lang.org/cargo/reference/environment-variables.html#environment-variables-cargo-sets-for-build-scripts
     // So "repeat" the info from build script (here) to our crate's build environment.
-    println!("cargo:rustc-env=TARGET={}", var("TARGET").unwrap());
+
+    let target = var("TARGET").unwrap();
+    let out_dir = var("OUT_DIR").unwrap();
+    println!("cargo:rustc-env=KANI_EXTERN_DIR={}/../../../../{}/debug/deps", out_dir, target);
+    println!("cargo:rustc-env=TARGET={}", target);
 }

kani-driver/src/call_cargo.rs

@@ -38,6 +38,8 @@ impl KaniSession {
         let target_dir = self.args.target_dir.as_ref().unwrap_or(&find_target_dir()).clone();
         let outdir = target_dir.join(build_target).join("debug/deps");
 
+        let kani_extern_lib_path = PathBuf::from(std::env!("KANI_EXTERN_DIR"));
+
         let flag_env = {
             let rustc_args = self.kani_rustc_flags();
             crate::util::join_osstring(&rustc_args, " ")
@@ -82,9 +84,15 @@ impl KaniSession {
 
         Ok(CargoOutputs {
             outdir: outdir.clone(),
-            symtabs: glob(&outdir.join("*.symtab.json"))?,
-            metadata: glob(&outdir.join("*.kani-metadata.json"))?,
-            restrictions: self.args.restrict_vtable().then_some(outdir),
+            symtabs: glob(&outdir.join("*.symtab.json"))?
+                .into_iter()
+                .chain(glob(&kani_extern_lib_path.join("*.symtab.json"))?)
+                .collect(),
+            metadata: glob(&outdir.join("*.kani-metadata.json"))?
+                .into_iter()
+                .chain(glob(&kani_extern_lib_path.join("*.kani-metadata.json"))?)
+                .collect(),
+            restrictions: self.args.restrict_vtable().then(|| outdir),
         })
     }
 }

library/kani/src/invariant.rs

@@ -52,6 +52,30 @@ empty_invariant!(f64);
 
 empty_invariant!(());
 
+macro_rules! tuple_invariant {
+    ($($fld:tt : $typ:ident),*) => {
+        unsafe impl<$($typ : Invariant),*> Invariant for ($($typ,)*) {
+           #[inline(always)]
+            fn is_valid(&self) -> bool {
+                ($(self.$fld.is_valid() &&)* true)
+            }
+        }
+    }
+}
+
+tuple_invariant!(0: A);
+tuple_invariant!(0: A, 1: B);
+tuple_invariant!(0: A, 1: B, 2: C);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G, 7: H);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G, 7: H, 8: I);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G, 7: H, 8: I, 9: J);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G, 7: H, 8: I, 9: J, 10: K);
+tuple_invariant!(0: A, 1: B, 2: C, 3: D, 4: E, 5: F, 6: G, 7: H, 8: I, 9: J, 10: K, 11: L);
+
 unsafe impl Invariant for bool {
     #[inline(always)]
     fn is_valid(&self) -> bool {

library/proptest/Cargo.toml

@@ -0,0 +1,14 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "proptest"
+version = "0.1.0"
+edition = "2021"
+publish = false
+license = "MIT OR Apache-2.0"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[target.'cfg(not(kani))'.dependencies]
+kani = { path = "../kani" }

library/proptest/src/arbitrary/_alloc/alloc.rs

@@ -0,0 +1,59 @@
+//-
+// Copyright 2017, 2018 The proptest developers
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+// Modifications Copyright Kani Contributors
+// See GitHub history for details
+
+//! Arbitrary implementations for `std::hash`.
+
+use core::cmp;
+use core::ops::Range;
+use core::usize;
+
+multiplex_alloc!(::alloc::alloc, ::std::alloc);
+
+use crate::arbitrary::*;
+use crate::strategy::statics::static_map;
+use crate::strategy::*;
+
+arbitrary!(self::alloc::Global; self::alloc::Global);
+
+// Not Debug.
+//lazy_just!(System, || System);
+
+arbitrary!(self::alloc::Layout, SFnPtrMap<(Range<u8>, StrategyFor<usize>), Self>;
+    // 1. align must be a power of two and <= (1 << 31):
+    // 2. "when rounded up to the nearest multiple of align, must not overflow".
+    static_map((0u8..32u8, any::<usize>()), |(align_power, size)| {
+        let align = 1usize << align_power;
+        let max_size = 0usize.wrapping_sub(align);
+        // Not quite a uniform distribution due to clamping,
+        // but probably good enough
+        self::alloc::Layout::from_size_align(cmp::min(max_size, size), align).unwrap()
+    })
+);
+
+arbitrary!(self::alloc::AllocError, Just<Self>; Just(self::alloc::AllocError));
+/* 2018-07-28 CollectionAllocErr is not currently available outside of using
+ * the `alloc` crate, which would require a different nightly feature. For now,
+ * disable.
+arbitrary!(alloc::collections::CollectionAllocErr, TupleUnion<(WA<Just<Self>>, WA<Just<Self>>)>;
+           prop_oneof![Just(alloc::collections::CollectionAllocErr::AllocErr),
+                       Just(alloc::collections::CollectionAllocErr::CapacityOverflow)]);
+ */
+
+#[cfg(test)]
+mod test {
+    multiplex_alloc!(::alloc::alloc, ::std::alloc);
+
+    no_panic_test!(
+        layout => self::alloc::Layout,
+        alloc_err => self::alloc::AllocErr
+        //collection_alloc_err => alloc::collections::CollectionAllocErr
+    );
+}

library/proptest/src/arbitrary/_alloc/borrow.rs

@@ -0,0 +1,29 @@
+//-
+// Copyright 2017, 2018 The proptest developers
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+// Modifications Copyright Kani Contributors
+// See GitHub history for details
+
+//! Arbitrary implementations for std::borrow.
+
+use crate::std_facade::fmt;
+use crate::std_facade::{Cow, ToOwned};
+use core::borrow::Borrow;
+
+use crate::arbitrary::{any_with, Arbitrary, SMapped};
+use crate::strategy::statics::static_map;
+
+arbitrary!(
+    [A: Arbitrary + Borrow<B>, B: ToOwned<Owned = A> + fmt::Debug + ?Sized]
+    Cow<'static, B>, SMapped<A, Self>, A::Parameters;
+    args => static_map(any_with::<A>(args), Cow::Owned)
+);
+
+lift1!([Borrow<B> + 'static, B: ToOwned<Owned = A> + fmt::Debug + ?Sized]
+    Cow<'static, B>; base => static_map(base, Cow::Owned)
+);

library/proptest/src/arbitrary/_alloc/boxed.rs

@@ -0,0 +1,21 @@
+//-
+// Copyright 2017, 2018 The proptest developers
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+// Modifications Copyright Kani Contributors
+// See GitHub history for details
+
+//! Arbitrary implementations for `std::boxed`.
+
+use crate::std_facade::Box;
+
+wrap_from!(Box);
+
+#[cfg(test)]
+mod test {
+    no_panic_test!(boxed => Box<u8>);
+}

library/proptest/src/arbitrary/_alloc/char.rs

@@ -0,0 +1,91 @@
+//-
+// Copyright 2017, 2018 The proptest developers
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+// Modifications Copyright Kani Contributors
+// See GitHub history for details
+
+//! Arbitrary implementations for `std::char`.
+
+use crate::std_facade::Vec;
+use core::char::*;
+use core::iter::once;
+use core::ops::Range;
+
+use crate::collection::vec;
+
+multiplex_alloc! {
+    core::char::DecodeUtf16, std::char::DecodeUtf16,
+    core::char::DecodeUtf16Error, std::char::DecodeUtf16Error,
+    core::char::decode_utf16, std::char::decode_utf16
+}
+
+const VEC_MAX: usize = ::core::u16::MAX as usize;
+
+use crate::arbitrary::*;
+use crate::strategy::statics::static_map;
+use crate::strategy::*;
+
+macro_rules! impl_wrap_char {
+    ($type: ty, $mapper: expr) => {
+        arbitrary!($type, SMapped<char, Self>;
+            static_map(any::<char>(), $mapper));
+    };
+}
+
+impl_wrap_char!(EscapeDebug, char::escape_debug);
+impl_wrap_char!(EscapeDefault, char::escape_default);
+impl_wrap_char!(EscapeUnicode, char::escape_unicode);
+#[cfg(feature = "unstable")]
+impl_wrap_char!(ToLowercase, char::to_lowercase);
+#[cfg(feature = "unstable")]
+impl_wrap_char!(ToUppercase, char::to_uppercase);
+
+#[cfg(feature = "break-dead-code")]
+arbitrary!(DecodeUtf16<<Vec<u16> as IntoIterator>::IntoIter>,
+    SMapped<Vec<u16>, Self>;
+    static_map(vec(any::<u16>(), ..VEC_MAX), decode_utf16)
+);
+
+arbitrary!(ParseCharError, IndFlatten<Mapped<bool, Just<Self>>>;
+    any::<bool>().prop_ind_flat_map(|is_two|
+        Just((if is_two { "__" } else { "" }).parse::<char>().unwrap_err()))
+);
+
+#[cfg(feature = "unstable")]
+arbitrary!(CharTryFromError; {
+    use core::convert::TryFrom;
+    char::try_from(0xD800 as u32).unwrap_err()
+});
+
+arbitrary!(DecodeUtf16Error, SFnPtrMap<Range<u16>, Self>;
+    static_map(0xD800..0xE000, |x|
+        decode_utf16(once(x)).next().unwrap().unwrap_err())
+);
+
+#[cfg(test)]
+mod test {
+    no_panic_test!(
+        escape_debug => EscapeDebug,
+        escape_default => EscapeDefault,
+        escape_unicode => EscapeUnicode,
+        parse_char_error => ParseCharError,
+        decode_utf16_error => DecodeUtf16Error
+    );
+
+    #[cfg(feature = "break-dead-code")]
+    no_panic_test!(
+        decode_utf16 => DecodeUtf16<<Vec<u16> as IntoIterator>::IntoIter>
+    );
+
+    #[cfg(feature = "unstable")]
+    no_panic_test!(
+        to_lowercase => ToLowercase,
+        to_uppercase => ToUppercase,
+        char_try_from_error => CharTryFromError
+    );
+}