Mutability translation with mutable cells

demo/examples/blocks.rs

@@ -1,15 +1,26 @@
 extern crate stainless;
+use stainless::*;
 
 fn foo(_n: i32) -> () {}
 
 pub fn bar(x: i32) -> i32 {
   foo(x);
-  let y = x * 2;
+  let y = x / 2;
   foo(y);
+
   if y <= 0 {
     1
-  } else {
+  } else if x > 10 {
     bar(x - 1) * x
+  } else {
+    y
+  }
+}
+
+#[pre(y != 123)]
+pub fn sole_if(y: i32) {
+  if y == 123 {
+    panic!()
   }
 }
 

demo/examples/external_fn.rs

@@ -3,7 +3,6 @@ use stainless::*;
 
 struct State(i32);
 
-#[var(0)]
 struct Printer(i32);
 
 #[pure(state)]
@@ -18,6 +17,6 @@ fn work(state: State, printer: Printer) -> i32 {
   do_sideeffectful_stuff(state, printer)
 }
 
-fn main() -> () {
+pub fn main() -> () {
   work(State(123), Printer(999));
 }

demo/examples/fact.rs

@@ -1,7 +1,7 @@
 extern crate stainless;
 use stainless::*;
 
-#[pre(x >= 0)]
+#[pre(x >= 0 && x < 10)]
 #[post(ret >= 0)]
 pub fn fact(x: i32) -> i32 {
   if x <= 0 {

demo/examples/generic_id.rs

@@ -1,9 +1,9 @@
 extern crate stainless;
 
-pub fn id<T>(x: T) -> T {
+fn id<T>(x: T) -> T {
   x
 }
 
-fn main() -> () {
+pub fn main() -> () {
   id(0);
 }

demo/examples/insertion_sort.rs

@@ -6,11 +6,6 @@ use stainless::*;
 ///
 /// [1]: https://github.com/epfl-lara/stainless/blob/master/frontends/benchmarks/verification/valid/InsertionSort.scala
 
-pub enum Option<T> {
-  None,
-  Some(T),
-}
-
 pub enum List<T> {
   Nil,
   Cons(T, Box<List<T>>),
@@ -53,11 +48,11 @@ impl List<i32> {
   #[measure(self)]
   pub fn min(&self) -> Option<i32> {
     match self {
-      List::Nil => Option::None,
+      List::Nil => None,
       List::Cons(x, xs) => match xs.min() {
-        Option::None => Option::Some(*x),
-        Option::Some(y) if *x < y => Option::Some(*x),
-        Option::Some(y) => Option::Some(y),
+        None => Some(*x),
+        Some(y) if *x < y => Some(*x),
+        Some(y) => Some(y),
       },
     }
   }

demo/examples/mut_local_fields.rs

@@ -1,27 +1,30 @@
 #![allow(dead_code, unused_assignments)]
 
 extern crate stainless;
-use stainless::*;
 
-#[var(field)]
 struct S {
   field: i32,
 }
 
-#[pure]
 fn set_field(mut s: S) -> S {
   s.field = 456;
   s
 }
 
 struct Outer(S);
 
-#[pure]
 fn set_inner_field(mut o: Outer) -> Outer {
   o.0.field = 101112;
   o
 }
 
+struct Gen<T>(T);
+
+fn set_gen_field(mut g: Gen<S>) -> Gen<S> {
+  g = Gen(S { field: 161718 });
+  g
+}
+
 // As control, the same for a primitive type
 fn set_int(mut s: i32) -> i32 {
   s = 1000;
@@ -42,6 +45,11 @@ pub fn main() {
   let o = set_inner_field(o);
   assert!(o.0.field == 101112);
 
+  let s = S { field: 123 };
+  let g = Gen(s);
+  let g = set_gen_field(g);
+  assert!(g.0.field == 161718);
+
   let i = set_int(12);
   assert!(i == 1000);
 }

demo/examples/thesis_example.rs

@@ -0,0 +1,65 @@
+extern crate stainless;
+use stainless::*;
+
+trait Id {
+  /// Calculate ID for this object.
+  fn id(&self) -> isize;
+
+  #[law]
+  fn law_positive(&self) -> bool {
+    self.id() > 0
+  }
+}
+
+impl Id for String {
+  fn id(&self) -> isize {
+    123456
+  }
+}
+
+struct Container<K, V> {
+  pair: Option<(K, V)>,
+}
+
+impl<K, V> Container<K, V> {
+  #[post(ret.is_empty())]
+  pub fn new() -> Self {
+    Container { pair: None }
+  }
+
+  pub fn is_empty(&self) -> bool {
+    matches!(self.pair, None)
+  }
+
+  #[post(!self.is_empty())]
+  pub fn insert(&mut self, k: K, v: V) {
+    self.pair = Some((k, v))
+  }
+}
+
+impl<K: Id, V> Container<K, V> {
+  #[post((self.is_empty()).implies(matches!(ret, None)))]
+  pub fn get_mut_by_id(&mut self, id: isize) -> Option<&mut V> {
+    match &mut self.pair {
+      Some((k, v)) if k.id() == id => Some(v),
+      _ => None,
+    }
+  }
+}
+
+pub fn main() {
+  let mut cont = Container::new();
+  let id = 123456;
+  let key = "foo".to_string();
+
+  assert!(cont.is_empty());
+  assert!(matches!(cont.get_mut_by_id(id), None));
+
+  cont.insert(key.clone(), 0);
+  match cont.get_mut_by_id(id) {
+    Some(v) => *v = 1000,
+    _ => panic!("no value"),
+  };
+
+  assert!(matches!(cont, Container { pair: Some((k, 1000))} if k == key))
+}

demo/examples/tuples.rs

@@ -20,4 +20,25 @@ pub fn swap(t: (i32, i32)) -> (i32, i32) {
   (t.1, t.0)
 }
 
-fn main() -> () {}
+pub fn main() {
+  #[allow(unused_variables)]
+  let unit_tuple = ();
+
+  let unary_tuple = (123,);
+  assert!(unary_tuple.0 == 123);
+
+  let huge_tuple = (
+    0, "hello", 2, "world", -4, "!", 6, "how", 8, "are", 10, "you", 12, "?",
+  );
+
+  assert!(
+    huge_tuple.0
+      + huge_tuple.2
+      + huge_tuple.4
+      + huge_tuple.6
+      + huge_tuple.8
+      + huge_tuple.10
+      + huge_tuple.12
+      == 34
+  )
+}

demo/examples/type_class_specs.rs

@@ -1,3 +1,5 @@
+#![allow(unused_variables)]
+
 extern crate stainless;
 use stainless::*;
 

libstainless/src/lib.rs

@@ -7,6 +7,10 @@ pub use set::*;
 mod map;
 pub use map::*;
 
+pub fn old<T>(t: T) -> T {
+  t
+}
+
 pub trait Implies {
   fn implies(self, b: Self) -> bool;
 }

libstainless/src/map.rs

@@ -36,13 +36,13 @@ where
     self.map.contains_key(key)
   }
 
-  pub fn insert(&self, key: K, val: V) -> Self {
+  pub fn insert(self, key: K, val: V) -> Self {
     Self {
       map: self.map.update(key, val),
     }
   }
 
-  pub fn remove(&self, key: &K) -> Self {
+  pub fn remove(self, key: &K) -> Self {
     Self {
       map: self.map.without(key),
     }

libstainless_macros/src/implementation.rs

@@ -220,27 +220,19 @@ fn replace_param(args: &Punctuated<FnArg, Token![,]>) -> Punctuated<FnArg, Token
   let fn_arg_tys: Vec<_> = args.iter().cloned().collect();
   (match &fn_arg_tys[..] {
     [FnArg::Receiver(Receiver {
-      mutability: None,
+      mutability,
       reference,
       ..
     }), args @ ..] => {
-      let new_self: FnArg = if reference.is_some() {
-        parse_quote! { _self: &Self }
-      } else {
-        parse_quote! { _self: Self }
+      let new_self: FnArg = match (mutability, reference) {
+        (None, None) => parse_quote! { _self: Self },
+        (None, Some(_)) => parse_quote! { _self: &Self },
+        (Some(_), None) => parse_quote! { mut _self: Self },
+        (Some(_), Some(_)) => parse_quote! { _self: &mut Self },
       };
       [&[new_self], args].concat()
     }
 
-    [FnArg::Receiver(Receiver {
-      mutability: Some(_),
-      reference: None,
-      ..
-    }), args @ ..] => {
-      let new_self: FnArg = parse_quote! { mut _self: Self };
-      [&[new_self], args].concat()
-    }
-
     args => args.to_vec(),
   })
   .into_iter()

libstainless_macros/src/lib.rs

@@ -38,4 +38,4 @@ macro_rules! define_flags {
   }
 }
 
-define_flags!(external, pure, mutable, var, law);
+define_flags!(external, pure, law);

stainless_data/src/ast.rs

@@ -162,6 +162,12 @@ impl ValDef<'_> {
   }
 }
 
+impl TypeParameter<'_> {
+  pub fn is_mutable(&self) -> bool {
+    self.flags.iter().any(|f| matches!(f, Flag::IsMutable(_)))
+  }
+}
+
 // Additional helpers that mirror those in Inox
 
 pub fn Int32Literal(value: Int) -> BVLiteral {