Merge pull request #999 from arnaudgolfouse/detect-recursion

Detect recursion

creusot-contracts-dummy/src/lib.rs

@@ -33,6 +33,16 @@ pub fn snapshot(_: TS1) -> TS1 {
         .into()
 }
 
+#[proc_macro_attribute]
+pub fn terminates(_: TS1, _: TS1) -> TS1 {
+    TS1::new()
+}
+
+#[proc_macro_attribute]
+pub fn pure(_: TS1, _: TS1) -> TS1 {
+    TS1::new()
+}
+
 #[proc_macro_attribute]
 pub fn logic(_: TS1, _: TS1) -> TS1 {
     TS1::new()

creusot-contracts-proc/src/lib.rs

@@ -410,6 +410,21 @@ pub fn snapshot(assertion: TS1) -> TS1 {
     })
 }
 
+#[proc_macro_attribute]
+pub fn terminates(_: TS1, tokens: TS1) -> TS1 {
+    let mut result = TS1::from(quote! { #[creusot::clause::terminates] });
+    result.extend(tokens);
+    result
+}
+
+#[proc_macro_attribute]
+pub fn pure(_: TS1, tokens: TS1) -> TS1 {
+    let mut result =
+        TS1::from(quote! { #[creusot::clause::no_panic] #[creusot::clause::terminates] });
+    result.extend(tokens);
+    result
+}
+
 struct LogicItem {
     vis: Visibility,
     defaultness: Option<Token![default]>,
@@ -478,6 +493,7 @@ fn logic_sig(sig: TraitItemSignature, prophetic: Option<TokenStream>) -> TS1 {
     let span = sig.span();
 
     TS1::from(quote_spanned! {span =>
+        #[::creusot_contracts::pure]
         #[creusot::decl::logic]
         #prophetic
         #sig
@@ -495,6 +511,7 @@ fn logic_item(log: LogicItem, prophetic: Option<TokenStream>) -> TS1 {
     let req_body = pretyping::encode_block(&term.stmts).unwrap();
 
     TS1::from(quote_spanned! {span =>
+        #[::creusot_contracts::pure]
         #[creusot::decl::logic]
         #prophetic
         #(#attrs)*
@@ -557,7 +574,8 @@ pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 {
 
 fn predicate_sig(sig: TraitItemSignature, prophetic: Option<TokenStream>) -> TS1 {
     let span = sig.span();
-    TS1::from(quote_spanned! {span=>
+    TS1::from(quote_spanned! {span =>
+        #[::creusot_contracts::pure]
         #[creusot::decl::predicate]
         #prophetic
         #sig
@@ -574,7 +592,8 @@ fn predicate_item(log: LogicItem, prophetic: Option<TokenStream>) -> TS1 {
 
     let req_body = pretyping::encode_block(&term.stmts).unwrap();
 
-    TS1::from(quote_spanned! {span=>
+    TS1::from(quote_spanned! {span =>
+        #[::creusot_contracts::pure]
         #[creusot::decl::predicate]
         #prophetic
         #(#attrs)*

creusot-contracts/src/lib.rs

@@ -27,6 +27,39 @@ mod macros {
 
     pub use base_macros::snapshot;
 
+    /// Indicate that the function terminates: fullfilling the `requires` clauses
+    /// ensures that this function will not loop indefinitively.
+    pub use base_macros::terminates;
+
+    /// Indicate that the function is pure: fullfilling the `requires` clauses ensures
+    /// that this function will terminate, and will not panic.
+    ///
+    /// # No panics ?
+    ///
+    /// "But I though Creusot was supposed to check the absence of panics ?"
+    ///
+    /// That's true, but with a caveat: some functions of the standart library are
+    /// allowed to panic in specific cases. The main example is `Vec::push`: we want its
+    /// specification to be
+    /// ```ignore
+    /// #[ensures((^self)@ == self@.push(v))]
+    /// fn push(&mut self, v: T) { /* ... */ }
+    /// ```
+    ///
+    /// But the length of a vector [cannot overflow `isize::MAX`](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.push). This is a very annoying condition to require, so we don't.
+    /// In exchange, this means `Vec::push` might panic in some cases, even though your
+    /// code passed Creusot's verification.
+    ///
+    /// # Non-pure std function
+    ///
+    /// Here are some examples of functions in `std` that are not marked as terminates
+    /// but not pure (this list might not be exhaustive):
+    /// - `Vec::push`, `Vec::insert`, `Vec::reserve`, `Vec::with_capacity`
+    /// - `str::to_string`
+    /// - `<&[T]>::into_vec`
+    /// - `Deque::push_front`, `Deque::push_back`, `Deque::with_capacity`
+    pub use base_macros::pure;
+
     /// A loop invariant
     /// The first argument should be a name for the invariant
     /// The second argument is the Pearlite expression for the loop invariant

creusot-contracts/src/std/boxed.rs

@@ -25,15 +25,18 @@ extern_spec! {
     mod std {
         mod boxed {
             impl<T> Box<T> {
+                #[pure]
                 #[ensures(*result == val)]
                 fn new(val: T) -> Self;
             }
 
             impl<T, A: Allocator> Box<T, A> {
+                #[pure]
                 #[ensures(**self == *result)]
                 #[ensures(*^self == ^result)]
                 fn as_mut(&mut self) -> &mut T;
 
+                #[pure]
                 #[ensures(**self == *result)]
                 fn as_ref(&self) -> &T;
             }

creusot-contracts/src/std/deque.rs

@@ -54,23 +54,29 @@ extern_spec! {
     mod std {
         mod collections {
             impl<T> VecDeque<T> {
+                #[pure]
                 #[ensures(result@.len() == 0)]
                 fn new() -> Self;
 
+                #[terminates] // can OOM
                 #[ensures(result@.len() == 0)]
                 fn with_capacity(capacity: usize) -> Self;
             }
 
             impl<T, A: Allocator> VecDeque<T, A> {
+                #[pure]
                 #[ensures(result@ == self@.len())]
                 fn len(&self) -> usize;
 
+                #[pure]
                 #[ensures(result == (self@.len() == 0))]
                 fn is_empty(&self) -> bool;
 
+                #[pure]
                 #[ensures((^self)@.len() == 0)]
                 fn clear(&mut self);
 
+                #[pure]
                 #[ensures(match result {
                     Some(t) =>
                         (^self)@ == self@.subsequence(1, self@.len()) &&
@@ -79,6 +85,7 @@ extern_spec! {
                 })]
                 fn pop_front(&mut self) -> Option<T>;
 
+                #[pure]
                 #[ensures(match result {
                     Some(t) =>
                         (^self)@ == self@.subsequence(0, self@.len() - 1) &&
@@ -87,10 +94,12 @@ extern_spec! {
                 })]
                 fn pop_back(&mut self) -> Option<T>;
 
+                #[terminates] // can OOM
                 #[ensures((^self)@.len() == self@.len() + 1)]
                 #[ensures((^self)@ == Seq::singleton(value).concat(self@))]
                 fn push_front(&mut self, value: T);
 
+                #[terminates] // can OOM
                 #[ensures((^self)@ == self@.push(value))]
                 fn push_back(&mut self, value: T);
             }

creusot-contracts/src/std/iter.rs

@@ -98,28 +98,34 @@ extern_spec! {
                 })]
                 fn next(&mut self) -> Option<Self::Item>;
 
+                #[pure]
                 #[ensures(result.iter() == self && result.n() == n@)]
                 fn skip(self, n: usize) -> Skip<Self>;
 
+                #[pure]
                 #[ensures(result.iter() == self && result.n() == n@)]
                 fn take(self, n: usize) -> Take<Self>;
 
+                #[pure]
                 #[ensures(result.iter() == self)]
                 fn cloned<'a, T>(self) -> Cloned<Self>
                     where T : 'a + Clone,
                         Self: Sized + Iterator<Item = &'a T>;
 
+                #[pure]
                 #[ensures(result.iter() == self)]
                 fn copied<'a, T>(self) -> Copied<Self>
                     where T : 'a + Copy,
                         Self: Sized + Iterator<Item = &'a T>;
 
+                #[pure]
                 #[ensures(result.iter() == self && result.n() == 0)]
                 fn enumerate(self) -> Enumerate<Self>;
 
                 #[ensures(result@ == Some(self))]
                 fn fuse(self) -> Fuse<Self>;
 
+                #[pure]
                 #[requires(other.into_iter_pre())]
                 #[ensures(result.itera() == self)]
                 #[ensures(other.into_iter_post(result.iterb()))]
@@ -154,11 +160,14 @@ extern_spec! {
                     where T: IntoIterator<Item = A>, T::IntoIter: Iterator;
             }
 
+            #[pure]
             fn empty<T>() -> Empty<T>;
 
+            #[pure]
             #[ensures(result@ == Some(value))]
             fn once<T>(value: T) -> Once<T>;
 
+            #[pure]
             #[ensures(result@ == elt)]
             fn repeat<T: Clone>(elt: T) -> Repeat<T>;
         }

creusot-contracts/src/std/iter/empty.rs

@@ -25,3 +25,15 @@ impl<T> Iterator for Empty<T> {
     #[ensures(a.produces(ab.concat(bc), c))]
     fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
 }
+
+extern_spec! {
+    mod std {
+        mod iter {
+            impl<T> Iterator for Empty<T> {
+                #[pure]
+                #[ensures(result == None && self.completed())]
+                fn next(&mut self) -> Option<T>;
+            }
+        }
+    }
+}

creusot-contracts/src/std/iter/once.rs

@@ -39,3 +39,18 @@ impl<T> Iterator for Once<T> {
     #[ensures(a.produces(ab.concat(bc), c))]
     fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
 }
+
+extern_spec! {
+    mod std {
+        mod iter {
+            impl<T> Iterator for Once<T> {
+                #[pure]
+                #[ensures(match result {
+                    None => self.completed(),
+                    Some(v) => (*self).produces(Seq::singleton(v), ^self)
+                })]
+                fn next(&mut self) -> Option<T>;
+            }
+        }
+    }
+}

creusot-contracts/src/std/mem.rs

@@ -4,10 +4,12 @@ pub use ::std::mem::*;
 extern_spec! {
     mod std {
         mod mem {
+            #[pure]
             #[ensures(^dest == src)]
             #[ensures(result == *dest)]
             fn replace<T>(dest: &mut T, src: T) -> T;
 
+            #[pure]
             #[ensures(^x == *y)]
             #[ensures(^y == *x)]
             fn swap<T>(x: &mut T, y: &mut T);

creusot-contracts/src/std/num.rs

@@ -62,13 +62,15 @@ macro_rules! spec_type {
         extern_spec! {
             impl $type {
                 #[allow(dead_code)]
+                #[pure]
                 // Returns `None` iff the divisor is zero or the division overflows
                 #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
                 // Else, returns the result of the division
                 #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
                 fn checked_div(self, rhs: $type) -> Option<$type>;
 
                 #[allow(dead_code)]
+                #[pure]
                 // Panics if the divisor is zero
                 #[requires(rhs@ != 0)]
                 // Returns `self` if the division overflows
@@ -78,6 +80,7 @@ macro_rules! spec_type {
                 fn wrapping_div(self, rhs: $type) -> $type;
 
                 #[allow(dead_code)]
+                #[pure]
                 // Panics if the divisor is zero
                 #[requires(rhs@ != 0)]
                 // Returns `$type::MIN` if the division overflows
@@ -87,6 +90,7 @@ macro_rules! spec_type {
                 fn saturating_div(self, rhs: $type) -> $type;
 
                 #[allow(dead_code)]
+                #[pure]
                 // Panics if the divisor is zero
                 #[requires(rhs@ != 0)]
                 // Returns `self` if the division overflows
@@ -119,6 +123,7 @@ macro_rules! spec_op_common {
                 // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
                 // `$type`
                 #[allow(dead_code)]
+                #[pure]
                 // Returns `None` iff the result is out of range
                 #[ensures(
                     (result == None)
@@ -130,6 +135,7 @@ macro_rules! spec_op_common {
 
                 // Wrapping: performs the operation on `Int` and converts back to `$type`
                 #[allow(dead_code)]
+                #[pure]
                 // Returns result converted to `$type`
                 #[ensures(
                     result@ == (self@ $op rhs@).rem_euclid(2.pow($type::BITS@)) + $type::MIN@
@@ -157,6 +163,7 @@ macro_rules! spec_op_common {
                 // Saturating: performs the operation on `Int` and clamps the result between
                 // `$type::MIN` and `$type::MAX`
                 #[allow(dead_code)]
+                #[pure]
                 // Returns the result if it is in range
                 #[ensures(
                     (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
@@ -170,6 +177,7 @@ macro_rules! spec_op_common {
                 // Overflowing: performs the operation on `Int` and converts back to `$type`, and
                 // indicates whether an overflow occurred
                 #[allow(dead_code)]
+                #[pure]
                 // Returns result converted to `$type`
                 #[ensures(
                     result.0@ == (self@ $op rhs@).rem_euclid(2.pow($type::BITS@)) + $type::MIN@
@@ -209,12 +217,14 @@ macro_rules! spec_abs_diff {
         extern_spec! {
             impl $unsigned {
                 #[allow(dead_code)]
+                #[pure]
                 #[ensures(result@ == self@.abs_diff(other@))]
                 fn abs_diff(self, other: $unsigned) -> $unsigned;
             }
 
             impl $signed {
                 #[allow(dead_code)]
+                #[pure]
                 #[ensures(result@ == self@.abs_diff(other@))]
                 fn abs_diff(self, other: $signed) -> $unsigned;
             }