Refactor verification-annotations

Added a prelude to verification-annotations to make it easier to import.

Added verifier module, that re-exports klee/seahorn, and moved shared code
from those modules to verifier.

Reimplemented verifier_nondet_bytes (not using klee_make_symbolic anymore).

Added a string module to propverify with strategies for generating an arbitrary
string with `n` bytes (doesn't work very well), and ascii string with `n`
bytes (works quite well with Klee).

Added demo/simple/string to test the new string module.

demos/bottlenecks/merging/src/main.rs

@@ -17,7 +17,7 @@
 /// Indicating that the original version suffers from a path explosion and generates
 /// more tests, executes more instructions and explores more paths than the merged version.
 
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn main() {
     println!("Hello, world!");
@@ -40,7 +40,7 @@ fn test_original() {
 
     // Set each element of array to a symbolic value
     for i in &mut a {
-        *i = verifier::AbstractValue::abstract_value();
+        *i = u32::abstract_value();
     }
 
     // A loop containing two branches - this will cause a performance problem
@@ -69,7 +69,7 @@ fn test_merged() {
 
     // Set each element of array to a symbolic value
     for i in 0..a.len() {
-        a[i] = verifier::AbstractValue::abstract_value();
+        a[i] = u32::abstract_value();
     }
 
     // A loop containing two branches - this will cause a performance problem

demos/bottlenecks/regex/src/main.rs

@@ -16,7 +16,7 @@
 ///    strings very short to keep execution time reasonable.
 
 use regex::Regex;
-use verification_annotations as verifier;
+use verification_annotations::verifier;
 
 fn main() {
     println!("Hello, world!");

demos/simple/annotations/src/main.rs

@@ -1,10 +1,10 @@
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 #[cfg_attr(feature="verifier-crux", crux_test)]
 #[cfg_attr(not(feature="verifier-crux"), test)]
 fn t1() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     if verifier::is_replay() {

demos/simple/klee/src/main.rs

@@ -1,8 +1,8 @@
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn main() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     if verifier::is_replay() {

demos/simple/seahorn/src/main.rs

@@ -1,9 +1,8 @@
-
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn main() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     let r = a*b;

demos/simple/string/Cargo.toml

@@ -0,0 +1,22 @@
+[package]
+name = "string"
+version = "0.1.0"
+authors = ["Shaked Flur <[email protected]>"]
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+regex = "1"
+
+[target.'cfg(verify)'.dependencies]
+propverify = { path="/home/rust-verification-tools/propverify" }
+verification-annotations = { path = "/home/rust-verification-tools/verification-annotations" }
+
+[target.'cfg(not(verify))'.dependencies]
+proptest = { version = "*" }
+
+[features]
+verifier-klee = ["propverify/verifier-klee", "verification-annotations/verifier-klee"]
+verifier-crux = ["propverify/verifier-crux"]
+verifier-seahorn = ["propverify/verifier-seahorn"]

demos/simple/string/src/main.rs

@@ -0,0 +1,38 @@
+#[cfg(not(verify))]
+use proptest::prelude::*;
+#[cfg(verify)]
+use propverify::prelude::*;
+
+use regex::Regex;
+
+proptest! {
+    #[test]
+    // Construct an arbitrary (utf8) string from 3 bytes.
+    // Klee can only handle a small number of bytes in this case.
+    fn string(s in prop::string::arbitrary(3)) {
+        let re = Regex::new(r"^a").unwrap();
+        prop_assume!(re.is_match(&s));
+        prop_assert!(s.starts_with('a'));
+    }
+}
+
+proptest! {
+    #[test]
+    // Construct a (utf8) string from 100 bytes, restricted to ascii chars.
+    // Klee can handle much more bytes this way.
+    fn ascii_string(s in prop::string::arbitrary_ascii(100)) {
+        let re = Regex::new(r"^a").unwrap();
+        prop_assume!(re.is_match(&s));
+        prop_assert!(s.starts_with('a'));
+    }
+}
+
+proptest! {
+    #[test]
+    #[should_panic]
+    fn string_add(s1 in prop::string::arbitrary_ascii(200), s2 in prop::string::arbitrary_ascii(200)) {
+        let s = s1 + &s2;
+        let s: String = s.chars().rev().collect();
+        prop_assert!(s.len() == 200);
+    }
+}

docs/_posts/2020-09-01-using-klee.md

@@ -46,11 +46,11 @@ This code is in [demos/simple/klee/src/main.rs] and the shell commands in this
 file are in [demos/simple/klee/verify.sh].
 
 ``` rust
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn main() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     if verifier::is_replay() {

docs/_posts/2020-09-02-using-annotations.md

@@ -112,7 +112,7 @@ values of `a` are not legal. For example, you might create a unicode character
 like this:
 
 ```
-let a : u32 = verifier::AbstractValue::abstract_value();
+let a = u32::abstract_value();
 let b = match std::char::from_u32(a) {
     Some(r) => r,
     None => verifier::reject(),
@@ -146,11 +146,11 @@ This code is in [demos/simple/annotations/src/main.rs] and the shell commands in
 file are in [demos/simple/annotations/verify.sh].
 
 ```
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn t1() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     #[cfg(not(crux))]
@@ -291,13 +291,13 @@ As a first variation, let's restore the original error and add a call to
 `expect`:
 
 ```
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 #[test]
 fn main() {
     verifier::expect(Some("assertion failed"));
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     if verifier::is_replay() {
@@ -332,13 +332,13 @@ For example, we might allow larger values for `a` and `b` or we might
 just delete the assumptions.
 
 ```
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 #[test]
 fn t1() {
     // verifier::expect(Some("overflow"));
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000000);
     verifier::assume(1 <= b && b <= 1000000);
     if verifier::is_replay() {

docs/_posts/2021-04-01-using-seahorn.md

@@ -39,11 +39,11 @@ This code is in [demos/simple/seahorn/src/main.rs] and the shell commands in thi
 file are in [demos/simple/seahorn/verify.sh].
 
 ``` rust
-use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 fn main() {
-    let a : u32 = verifier::AbstractValue::abstract_value();
-    let b : u32 = verifier::AbstractValue::abstract_value();
+    let a = u32::abstract_value();
+    let b = u32::abstract_value();
     verifier::assume(1 <= a && a <= 1000);
     verifier::assume(1 <= b && b <= 1000);
     let r = a*b;

propverify/src/lib.rs

@@ -51,9 +51,12 @@ pub mod prelude {
             pub use crate::strategy::{u128, u16, u32, u64, u8, usize};
             #[cfg(feature = "float")] pub use crate::strategy::{f32, f64};
         }
+
+        pub use crate::strategy::string;
     }
 
-    pub use crate::strategy::verifier;
+    pub use verification_annotations;
+    pub use verification_annotations::verifier;
 
     pub use verifier::assert as prop_assert;
     pub use verifier::assert_eq as prop_assert_eq;

propverify/src/strategy.rs

@@ -7,7 +7,7 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-pub use verification_annotations as verifier;
+use verification_annotations::prelude::*;
 
 use std::boxed::Box;
 use std::marker::PhantomData;
@@ -339,10 +339,7 @@ pub mod char {
         type Value = char;
         fn value(&self) -> Self::Value {
             let c : u32 = verifier::AbstractValue::abstract_value();
-            match std::char::from_u32(c) {
-                Some(r) => r,
-                None => verifier::reject(),
-            }
+            std::char::from_u32(c).unwrap_or_reject()
         }
     }
     impl Arbitrary for char {
@@ -489,10 +486,7 @@ impl<S: Strategy, F: Fn(S::Value) -> Option<T>, T: std::fmt::Debug> Strategy for
     type Value = T;
     fn value(&self) -> Self::Value {
         let val = self.source.value();
-        match (self.fun)(val) {
-            Some(r) => r,
-            None => verifier::reject(),
-        }
+        (self.fun)(val).unwrap_or_reject()
     }
 }
 
@@ -841,6 +835,47 @@ pub fn vec<S: Strategy>(element: S, size: usize) -> VecStrategy<S> {
     VecStrategy { element, size }
 }
 
+pub mod string {
+    use super::*;
+
+    #[derive(Clone, Copy, Debug)]
+    pub struct Any(usize);
+    // pub const ANY: Any = Any();
+    impl Strategy for Any {
+        type Value = String;
+        fn value(&self) -> Self::Value {
+            let length = self.0;
+            let bytes = verifier::verifier_nondet_bytes(length);
+            String::from_utf8(bytes).unwrap_or_reject()
+        }
+    }
+    // impl Arbitrary for String {
+    //     type Strategy = Any;
+    //     fn arbitrary() -> Self::Strategy { ANY }
+    // }
+    pub fn arbitrary(length: usize) -> Any {
+        Any(length)
+    }
+
+    #[derive(Clone, Copy, Debug)]
+    pub struct AnyAscii(usize);
+    impl Strategy for AnyAscii {
+        type Value = String;
+        fn value(&self) -> Self::Value {
+            let length = self.0;
+            let bytes = verifier::verifier_nondet_bytes(length);
+            for i in 0..length {
+                verifier::assume(bytes[i] != 0u8);
+                verifier::assume(bytes[i].is_ascii());
+            }
+            String::from_utf8(bytes).unwrap_or_reject()
+        }
+    }
+    pub fn arbitrary_ascii(length: usize) -> AnyAscii {
+        AnyAscii(length)
+    }
+}
+
 #[derive(Clone, Copy, Debug)]
 pub struct VecDequeStrategy<S: Strategy> {
     element: S,

scripts/regression-test

@@ -1,19 +1,22 @@
 #! /usr/bin/env bash
 
 set -e
+set -x
 
-readonly FLAGS="--backend=klee --verbose --clean"
 (cd demos/simple/annotations; ./verify.sh)
 (cd demos/simple/klee; ./verify.sh)
 (cd demos/simple/seahorn; ./verify.sh)
 (cd demos/simple/errors; ./verify.sh)
+
+readonly FLAGS="--backend=klee --verbose --clean"
 cargo-verify ${FLAGS} --tests --manifest-path=verification-annotations/Cargo.toml
 cargo-verify ${FLAGS} --tests --manifest-path=compatibility-test/Cargo.toml
 cargo-verify ${FLAGS} --tests --manifest-path=demos/bottlenecks/bornholt2018-1/Cargo.toml
 cargo-verify ${FLAGS} --tests --manifest-path=demos/simple/ffi/Cargo.toml
 cargo-verify ${FLAGS} -v -v -v --manifest-path=demos/simple/argv/Cargo.toml -- foo foo
 cargo verify ${FLAGS} --tests --manifest-path=demos/bottlenecks/merging/Cargo.toml --backend-flags=--use-merge
 cargo verify ${FLAGS} --tests --manifest-path=demos/bottlenecks/regex/Cargo.toml
+cargo-verify ${FLAGS} --tests --manifest-path=demos/simple/string/Cargo.toml
 
 # Test the --backend-flags and --replace-backend-flags options.
 # Note the use of handlebars and passing args to main (foo foo).