Closure inference (again) (#1294)

creusot/src/backend/clone_map.rs

@@ -357,7 +357,6 @@ impl<'tcx> Dependencies<'tcx> {
         // Update the clone graph with any new entries.
         let (graph, mut bodies) = graph.update_graph(ctx);
 
-        // First we find components including weak dependencies
         for scc in petgraph::algo::tarjan_scc(&graph).into_iter() {
             if scc.iter().any(|node| node == &self_node) {
                 assert_eq!(scc.len(), 1);

creusot/src/backend/clone_map/elaborator.rs

@@ -525,7 +525,7 @@ fn fn_mut_postcond_term<'tcx>(
     );
     let res = Term::var(Symbol::intern("result"), ty_res);
     match ty_self.kind() {
-        TyKind::Closure(did, _) => Some(ctx.closure_contract(*did).postcond_mut.clone().unwrap()),
+        TyKind::Closure(did, _) => ctx.closure_contract(*did).postcond_mut.clone(),
         TyKind::Ref(_, cl, Mutability::Mut) => {
             let mut subst_postcond = subst.to_vec();
             subst_postcond[1] = GenericArg::from(*cl);
@@ -566,7 +566,7 @@ fn fn_postcond_term<'tcx>(
     );
     let res = Term::var(Symbol::intern("result"), ty_res);
     match ty_self.kind() {
-        TyKind::Closure(did, _) => Some(ctx.closure_contract(*did).postcond.clone().unwrap()),
+        TyKind::Closure(did, _) => ctx.closure_contract(*did).postcond.clone(),
         TyKind::Ref(_, cl, Mutability::Not) => {
             let mut subst_postcond = subst.to_vec();
             subst_postcond[1] = GenericArg::from(*cl);

creusot/src/backend/logic/vcgen.rs

@@ -439,6 +439,8 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             TermKind::Old { .. } => Err(VCError::OldInLemma(t.span)),
             TermKind::Closure { .. } => Err(VCError::UnimplementedClosure(t.span)),
             TermKind::Reborrow { .. } => Err(VCError::UnimplementedReborrow(t.span)),
+            TermKind::Precondition { .. } => Err(VCError::UnimplementedClosure(t.span)),
+            TermKind::Postcondition { .. } => Err(VCError::UnimplementedClosure(t.span)),
         }
     }
 

creusot/src/backend/program.rs

@@ -100,11 +100,19 @@ pub fn val<'tcx>(_: &mut Why3Generator<'tcx>, sig: Signature) -> Decl {
         vec![Defn {
             name: "return".into(),
             writes: Vec::new(),
+            attrs: vec![],
+
             params: vec![Param::Term("result".into(), sig.retty.clone().unwrap())],
             body: postcond,
         }],
     );
-    why3::declaration::Decl::Coma(Defn { name: sig.name, writes: Vec::new(), params, body })
+    why3::declaration::Decl::Coma(Defn {
+        name: sig.name,
+        writes: Vec::new(),
+        attrs: vec![],
+        params,
+        body,
+    })
 }
 
 // TODO: move to a more "central" location
@@ -156,7 +164,8 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
         })
         .collect();
 
-    let sig = if body_id.promoted.is_none() {
+    // Remove the invariant from the contract here??
+    let mut sig = if body_id.promoted.is_none() {
         signature_of(ctx, names, name, body_id.def_id())
     } else {
         let ret = ret.unwrap();
@@ -173,16 +182,31 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
 
     let mut postcond = Expr::Symbol("return".into()).app(vec![Arg::Term(Exp::var("result"))]);
 
-    if body_id.promoted.is_none() && !is_ghost_closure(ctx.tcx, body_id.def_id()) {
-        postcond = Expr::BlackBox(Box::new(postcond));
-    }
+    let inferred_closure_spec = ctx.is_closure_like(body_id.def_id())
+        && !ctx.sig(body_id.def_id()).contract.has_user_contract;
+
+    // We remove the barrier around the definition in the following edge cases:
+    let open_body = false
+        // a closure with no contract
+        || inferred_closure_spec
+        // a promoted item
+        || body_id.promoted.is_some()
+        // a ghost closure
+        || is_ghost_closure(ctx.tcx, body_id.def_id());
+
     let ensures = sig.contract.ensures.into_iter().map(Condition::labelled_exp);
-    postcond = ensures.rfold(postcond, |acc, cond| Expr::Assert(Box::new(cond), Box::new(acc)));
 
-    if body_id.promoted.is_none() && !is_ghost_closure(ctx.tcx, body_id.def_id()) {
+    if !open_body {
+        postcond = Expr::BlackBox(Box::new(postcond));
+        postcond = ensures.rfold(postcond, |acc, cond| Expr::Assert(Box::new(cond), Box::new(acc)));
+
         body = Expr::BlackBox(Box::new(body))
     };
 
+    if inferred_closure_spec {
+        sig.attrs.push(Attribute::Attr("coma:extspec".into()));
+    }
+
     body = Expr::Let(Box::new(body), vars);
 
     body = Expr::Defn(
@@ -191,14 +215,16 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
         vec![Defn {
             name: "return".into(),
             writes: Vec::new(),
+            attrs: vec![],
             params: vec![Param::Term("result".into(), sig.retty.clone().unwrap())],
             body: postcond,
         }],
     );
 
     let requires = sig.contract.requires.into_iter().map(Condition::labelled_exp);
-    body = requires.rfold(body, |acc, req| Expr::Assert(Box::new(req), Box::new(acc)));
-
+    if !open_body {
+        body = requires.rfold(body, |acc, req| Expr::Assert(Box::new(req), Box::new(acc)));
+    }
     let params = sig
         .args
         .into_iter()
@@ -210,7 +236,7 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
             vec![Param::Term("ret".into(), sig.retty.unwrap())],
         )])
         .collect();
-    coma::Defn { name: sig.name, writes: Vec::new(), params, body }
+    coma::Defn { name: sig.name, writes: Vec::new(), attrs: sig.attrs, params, body }
 }
 
 fn component_to_defn<'tcx, N: Namer<'tcx>>(
@@ -682,7 +708,7 @@ fn mk_adt_switch<'tcx, N: Namer<'tcx>>(
             );
             let name = format!("br{}", ix.as_usize()).into();
 
-            coma::Defn { name, body, params, writes: Vec::new() }
+            coma::Defn { name, body, params, writes: Vec::new(), attrs: vec![] }
         })
         .collect();
     assert!(brch.next().is_none());
@@ -774,6 +800,7 @@ where
             vec![Defn {
                 name: "any_".into(),
                 writes: vec![],
+                attrs: vec![],
                 params: vec![Param::Term(id, ty)],
                 body: Expr::BlackBox(Box::new(tail)),
             }],

creusot/src/backend/term.rs

@@ -220,6 +220,19 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 // Discard cond, use unit
                 Exp::Tuple(vec![])
             }
+            TermKind::Precondition { item, args, params } => {
+                let params: Vec<_> = params.iter().map(|p| self.lower_term(p)).collect();
+                let mut sym = self.names.value(*item, args);
+                sym.name = format!("{}'pre", &*sym.name).into();
+
+                Exp::qvar(sym).app(params)
+            }
+            TermKind::Postcondition { item, args, params } => {
+                let params: Vec<_> = params.iter().map(|p| self.lower_term(p)).collect();
+                let mut sym = self.names.value(*item, args);
+                sym.name = format!("{}'post'return'", &*sym.name).into();
+                Exp::qvar(sym).app(params)
+            }
         }
     }
 

creusot/src/backend/ty.rs

@@ -266,6 +266,7 @@ pub(crate) fn eliminator<'tcx, N: Namer<'tcx>>(
     let good_branch: coma::Defn = coma::Defn {
         name: format!("good").into(),
         writes: vec![],
+        attrs: vec![],
         params: field_args.clone(),
         body: Expr::Assert(
             Box::new(cons_test.clone().eq(Exp::var("input"))),
@@ -294,6 +295,7 @@ pub(crate) fn eliminator<'tcx, N: Namer<'tcx>>(
             name: format!("bad").into(),
             writes: vec![],
             params: vec![],
+            attrs: vec![],
             body: Expr::Assert(Box::new(negative_assertion), Box::new(fail)),
         })
     } else {
@@ -310,6 +312,7 @@ pub(crate) fn eliminator<'tcx, N: Namer<'tcx>>(
         writes: vec![],
         params: vec![input, ret_cont],
         body: Expr::Defn(Box::new(Expr::Any), false, branches),
+        attrs: vec![],
     })
 }