Extract impl block functions (#47)

* Refactor to use own function item type.
* Add simple spec for impl blocks.
* Extract functions in local impl block as well.
* Adapt insertion sort to implementations.
* Extract specs for impl functions.
* Generate sibling specs with macros.
* Allow multiple specs of the same type and deal with all function names.
* Cache spec type on fn item.
* Move make_and to stainless data.
* Reconsider nested specs and add them to passing examples.

demo/examples/insertion_sort.rs

@@ -6,92 +6,98 @@ use stainless::*;
 ///
 /// [1]: https://github.com/epfl-lara/stainless/blob/master/frontends/benchmarks/verification/valid/InsertionSort.scala
 
-pub enum List {
-  Nil,
-  Cons(i32, Box<List>),
+pub enum Option<T> {
+  None,
+  Some(T),
 }
 
-pub enum IntOption {
-  None,
-  Some(i32),
+pub enum List<T> {
+  Nil,
+  Cons(T, Box<List<T>>),
 }
 
-#[measure(l)]
-pub fn size(l: List) -> u32 {
-  match l {
-    List::Nil => 0,
-    List::Cons(_, tail) => 1 + size(*tail),
+impl<T> List<T> {
+  #[measure(self)]
+  pub fn size(&self) -> u32 {
+    match self {
+      List::Nil => 0,
+      List::Cons(_, tail) => 1 + tail.size(),
+    }
   }
-}
 
-#[measure(l)]
-pub fn is_sorted(l: List) -> bool {
-  match l {
-    List::Nil => true,
-    List::Cons(x, tail) => match *tail {
-      List::Nil => true,
-      List::Cons(y, ys) => x <= y && is_sorted(List::Cons(y, ys)),
-    },
+  #[measure(self)]
+  pub fn contents(&self) -> Set<T> {
+    match self {
+      List::Nil => Set::empty(),
+      List::Cons(head, tail) => tail.contents().union(&Set::singleton(head)),
+    }
   }
 }
 
-#[measure(l)]
-pub fn min(l: List) -> IntOption {
-  match l {
-    List::Nil => IntOption::None,
-    List::Cons(x, xs) => match min(*xs) {
-      IntOption::None => IntOption::Some(x),
-      IntOption::Some(y) => {
-        if x < y {
-          IntOption::Some(x)
-        } else {
-          IntOption::Some(y)
-        }
-      }
-    },
+impl List<i32> {
+  #[measure(self)]
+  pub fn is_sorted(&self) -> bool {
+    match self {
+      List::Nil => true,
+      List::Cons(x, tail) => match &**tail {
+        List::Nil => true,
+
+        // FIXME: We *have* to deref the two integers here, because otherwise
+        //   their type is &i32 which we can't extract to primitive '<=' for the
+        //   moment.
+        List::Cons(y, ..) => *x <= *y && tail.is_sorted(),
+      },
+    }
   }
-}
 
-#[measure(l)]
-pub fn contents(l: List) -> Set<i32> {
-  match l {
-    List::Nil => Set::empty(),
-    List::Cons(head, tail) => contents(*tail).union(Set::singleton(head)),
+  #[measure(self)]
+  pub fn min(&self) -> Option<i32> {
+    match self {
+      List::Nil => Option::None,
+      List::Cons(x, xs) => match xs.min() {
+        Option::None => Option::Some(*x),
+        Option::Some(y) => {
+          if *x < y {
+            Option::Some(*x)
+          } else {
+            Option::Some(y)
+          }
+        }
+      },
+    }
   }
-}
 
-/// Inserting element 'e' into a sorted list 'l' produces a sorted list with
-/// the expected content and size
-#[pre(is_sorted(l))]
-#[measure(l)]
-#[post(size(ret) == size(l) + 1)]
-#[post(is_sorted(ret))]
-#[post(contents(ret).is_subset_of(contents(l).add(e)))]
-#[post(contents(l).add(e).is_subset_of(contents(ret)))]
-pub fn sorted_insert(e: i32, l: List) -> List {
-  match l {
-    List::Nil => List::Cons(e, Box::new(List::Nil)),
-    List::Cons(x, xs) => {
-      if x <= e {
-        List::Cons(x, Box::new(sorted_insert(e, *xs)))
-      } else {
-        List::Cons(e, Box::new(List::Cons(x, xs)))
-      }
+  /// Inserting element 'e' into a sorted list 'l' produces a sorted list with
+  /// the expected content and size
+  #[pre(self.is_sorted())]
+  #[measure(self)]
+  #[post(
+    ret.size() == self.size() + 1 &&
+    ret.is_sorted() &&
+    ret.contents().is_subset_of(&self.contents().add(&e)) &&
+    self.contents().add(&e).is_subset_of(&ret.contents())
+  )]
+  pub fn sorted_insert(self, e: i32) -> List<i32> {
+    match self {
+      List::Cons(head, tail) if head <= e => List::Cons(head, Box::new(tail.sorted_insert(e))),
+      _ => List::Cons(e, Box::new(self)),
     }
   }
-}
 
-/// Insertion sort yields a sorted list of same size and content as the input
-/// list
-#[measure(l)]
-#[post(size(ret) == size(l))]
-#[post(is_sorted(ret))]
-#[post(contents(ret).is_subset_of(contents(l)))]
-#[post(contents(l).is_subset_of(contents(ret)))]
-pub fn sort(l: List) -> List {
-  match l {
-    List::Nil => l,
-    List::Cons(x, xs) => sorted_insert(x, sort(*xs)),
+  /// Insertion sort yields a sorted list of same size and content as the input
+  /// list
+  #[measure(self)]
+  #[post(
+    ret.size() == self.size() &&
+    ret.is_sorted() &&
+    ret.contents().is_subset_of(&self.contents()) &&
+    self.contents().is_subset_of(&ret.contents())
+  )]
+  pub fn sort(self) -> List<i32> {
+    match self {
+      List::Nil => self,
+      List::Cons(x, xs) => xs.sort().sorted_insert(x),
+    }
   }
 }
 
@@ -111,5 +117,5 @@ pub fn main() {
     )),
   );
 
-  assert!(is_sorted(sort(list)))
+  assert!(list.sort().is_sorted())
 }

demo/examples/nested_spec.rs

@@ -0,0 +1,16 @@
+extern crate stainless;
+use stainless::*;
+
+pub fn is_cool() -> bool {
+  #[pre(x > 0 && x < 100 && y > 0 && y < 100)]
+  #[post(ret > 0)]
+  fn inner_fn(x: i32, y: i32) -> i32 {
+    x * y
+  }
+
+  inner_fn(2, 3) == 123
+}
+
+pub fn main() {
+  is_cool();
+}

libstainless/lib.rs

@@ -15,26 +15,26 @@ impl<T> Set<T> {
 
   // TODO: Only take 'self' as a reference and also take the other parameters
   //   only by reference.
-  pub fn singleton(_t: T) -> Self {
+  pub fn singleton(_t: &T) -> Self {
     unimplemented!()
   }
-  pub fn add(self, _t: T) -> Set<T> {
+  pub fn add(&self, _t: &T) -> Set<T> {
     unimplemented!()
   }
-  pub fn contains(self, _t: T) -> bool {
+  pub fn contains(&self, _t: &T) -> bool {
     unimplemented!()
   }
 
-  pub fn union(self, _other: Set<T>) -> Set<T> {
+  pub fn union(&self, _other: &Set<T>) -> Set<T> {
     unimplemented!()
   }
-  pub fn intersection(self, _other: Set<T>) -> Set<T> {
+  pub fn intersection(&self, _other: &Set<T>) -> Set<T> {
     unimplemented!()
   }
-  pub fn difference(self, _other: Set<T>) -> Set<T> {
+  pub fn difference(&self, _other: &Set<T>) -> Set<T> {
     unimplemented!()
   }
-  pub fn is_subset_of(self, _other: Set<T>) -> bool {
+  pub fn is_subset_of(&self, _other: &Set<T>) -> bool {
     unimplemented!()
   }
 }

libstainless_macros/implementation.rs

@@ -1,12 +1,11 @@
 use proc_macro2::{Ident, Span, TokenStream};
 use quote::{format_ident, quote, ToTokens};
-use syn::{parse_quote, Attribute, Expr, Item, ItemFn, Result, ReturnType, Stmt, Type};
+use syn::{parse_quote, Attribute, Expr, FnArg, Item, ItemFn, Result, ReturnType, Stmt, Type};
 
 use std::convert::TryFrom;
 use std::iter;
 
 /// Specs (pre-, postconditions, ...)
-
 #[derive(Debug, PartialEq, Eq)]
 pub enum SpecType {
   Pre,
@@ -58,30 +57,30 @@ struct Spec {
 
 /// Parse the decorated function and all specs
 fn try_parse(
-  first_typ: SpecType,
+  first_spec_type: SpecType,
   first_attr_args: TokenStream,
   item: TokenStream,
 ) -> Result<(ItemFn, Vec<Spec>)> {
   let item_fn: ItemFn = parse_quote!(#item);
-  let first_cond: Expr = parse_quote!(#first_attr_args);
+  let first_args: Expr = parse_quote!(#first_attr_args);
 
-  let pre_specs = item_fn.attrs.iter().filter_map(|attr: &Attribute| {
-    if let Ok(typ) = SpecType::try_from(attr) {
-      Some((typ, attr.parse_args()))
-    } else {
-      None
-    }
+  // Filter out & parse all the remaining specs
+  let specs = item_fn.attrs.iter().filter_map(|attr: &Attribute| {
+    SpecType::try_from(attr)
+      .ok()
+      .map(|typ| (typ, attr.parse_args()))
   });
-  let pre_specs: Vec<(SpecType, Result<Expr>)> = iter::once((first_typ, Ok(first_cond)))
-    .chain(pre_specs)
+  // Add the first spec to the head of the list
+  let specs: Vec<(SpecType, Result<Expr>)> = iter::once((first_spec_type, Ok(first_args)))
+    .chain(specs)
     .collect();
 
-  for (_, cond) in &pre_specs {
-    if let Err(err) = cond {
-      return Err(err.clone());
-    }
+  // Check whether any parsing has caused errors and failed if so.
+  if let Some((_, Err(err))) = specs.iter().find(|(_, cond)| cond.is_err()) {
+    return Err(err.clone());
   }
-  let specs: Vec<Spec> = pre_specs
+
+  let specs: Vec<Spec> = specs
     .into_iter()
     .map(|(typ, cond)| Spec {
       typ,
@@ -92,16 +91,20 @@ fn try_parse(
   Ok((item_fn, specs))
 }
 
-fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> ItemFn {
+fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> Vec<ItemFn> {
   let fn_generics = &item_fn.sig.generics;
   let fn_arg_tys = &item_fn.sig.inputs;
   let fn_return_ty: Type = match &item_fn.sig.output {
     ReturnType::Type(_, ty) => *ty.clone(),
     ReturnType::Default => parse_quote! { () },
   };
+  let fn_name = &item_fn.sig.ident.to_string();
+
+  let make_spec_fn = |(index, spec): (usize, Spec)| -> ItemFn {
+    // The spec identifier is of the form __{type}_{index}_{?name}
+    // For sibling specs, the name of the spec'ed function has to be given.
+    let spec_ident = format_ident!("__{}_{}_{}", spec.typ.name(), index + 1, fn_name);
 
-  let make_spec_fn = |(index, spec): (usize, Spec)| -> Stmt {
-    let fn_ident = format_ident!("__{}{}", spec.typ.name(), index + 1);
     let ret_param: TokenStream = match spec.typ {
       SpecType::Post => quote! { , ret: #fn_return_ty },
       _ => quote! {},
@@ -113,53 +116,63 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> ItemFn {
       _ => (parse_quote!(bool), parse_quote! { #expr }),
     };
 
-    let spec_fn: ItemFn = parse_quote! {
+    parse_quote! {
       #[doc(hidden)]
       #[allow(unused_variables)]
-      fn #fn_ident#fn_generics(#fn_arg_tys#ret_param) -> #return_type {
+      fn #spec_ident#fn_generics(#fn_arg_tys#ret_param) -> #return_type {
         #body
       }
-    };
-    Stmt::Item(Item::Fn(spec_fn))
+    }
   };
-  let (pre_specs, other): (Vec<Spec>, Vec<Spec>) = specs
-    .into_iter()
-    .partition(|spec| spec.typ == SpecType::Pre);
 
-  let (post_specs, measure_specs): (Vec<Spec>, Vec<Spec>) = other
-    .into_iter()
-    .partition(|spec| spec.typ == SpecType::Post);
+  let specs = specs.into_iter().enumerate().map(make_spec_fn);
 
-  let pre_spec_fns = pre_specs.into_iter().enumerate().map(make_spec_fn);
-  let post_spec_fns = post_specs.into_iter().enumerate().map(make_spec_fn);
-  let measure_spec_fns = measure_specs.into_iter().enumerate().map(make_spec_fn);
+  let has_self_param = item_fn
+    .sig
+    .inputs
+    .first()
+    .map(|first_input| match first_input {
+      FnArg::Receiver(_) => true,
+      _ => false,
+    })
+    .unwrap_or(false);
 
-  #[allow(clippy::reversed_empty_ranges)]
-  {
-    item_fn.block.stmts.splice(0..0, measure_spec_fns);
-    item_fn.block.stmts.splice(0..0, post_spec_fns);
-    item_fn.block.stmts.splice(0..0, pre_spec_fns);
+  // If the function has the 'self' param, then the specs must be siblings
+  if has_self_param {
+    specs.chain(iter::once(item_fn.clone())).collect()
+  }
+  // otherwise the specs can be nested
+  else {
+    #[allow(clippy::reversed_empty_ranges)]
+    {
+      item_fn
+        .block
+        .stmts
+        .splice(0..0, specs.map(|s| Stmt::Item(Item::Fn(s))));
+    }
+    vec![item_fn]
   }
-
-  item_fn
 }
 
 /// Extract all the specs from a given function and insert spec functions
 pub fn extract_specs_and_expand(
-  first_typ: SpecType,
+  first_spec_type: SpecType,
   first_attr_args: TokenStream,
   item: TokenStream,
 ) -> TokenStream {
-  match try_parse(first_typ, first_attr_args, item) {
+  match try_parse(first_spec_type, first_attr_args, item) {
     Ok((mut item_fn, specs)) => {
       // Remove all remaining spec attributes
       item_fn
         .attrs
         .retain(|attr| SpecType::try_from(attr).is_err());
 
       // Build the spec function and insert it into the original function
-      let item_fn = generate_fn_with_spec(item_fn, specs);
-      item_fn.to_token_stream()
+
+      generate_fn_with_spec(item_fn, specs)
+        .into_iter()
+        .map(|fn_item| fn_item.to_token_stream())
+        .collect()
     }
     Err(err) => err.to_compile_error(),
   }