Merge pull request #951 from creusot-rs/demote-calll

Demote `Expr::Call` to `Statement::Call`

creusot/src/backend/optimization.rs

@@ -94,6 +94,10 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
             }
             Statement::AssumeBorrowInv(p) => self.read_place(p),
             Statement::AssertTyInv(p) => self.read_place(p),
+            Statement::Call(dest, _, _, args, _) => {
+                self.write_place(dest);
+                args.iter().for_each(|a| self.visit_expr(a));
+            }
         }
     }
 
@@ -110,17 +114,22 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
 
     // fn visit_term(&mut self, t: &Term<'tcx>) {}
 
+    fn visit_operand(&mut self, op: &Operand<'tcx>) {
+        match op {
+            Operand::Move(p) => self.read_place(p),
+            Operand::Copy(p) => self.read_place(p),
+        }
+    }
+
     fn visit_expr(&mut self, e: &Expr<'tcx>) {
         match &e.kind {
-            ExprKind::Move(p) => self.read_place(p),
-            ExprKind::Copy(p) => self.read_place(p),
+            ExprKind::Operand(op) => self.visit_operand(op),
             ExprKind::BinOp(_, l, r) => {
                 self.visit_expr(l);
                 self.visit_expr(r)
             }
             ExprKind::UnaryOp(_, e) => self.visit_expr(e),
             ExprKind::Constructor(_, _, es) => es.iter().for_each(|e| self.visit_expr(e)),
-            ExprKind::Call(_, _, es) => es.iter().for_each(|e| self.visit_expr(e)),
             ExprKind::Constant(t) => self.visit_term(t),
             ExprKind::Cast(e, _, _) => self.visit_expr(e),
             ExprKind::Tuple(es) => es.iter().for_each(|e| self.visit_expr(e)),
@@ -220,11 +229,11 @@ impl<'tcx> SimplePropagator<'tcx> {
             match s {
                 Statement::Assignment(l, RValue::Expr(r), _)
                     // we do not propagate calls to avoid moving them after the resolve of their arguments
-                    if self.should_propagate(l.local) && !self.usage[&l.local].used_in_pure_ctx && !r.is_call() => {
+                    if self.should_propagate(l.local) && !self.usage[&l.local].used_in_pure_ctx => {
                       self.prop.insert(l.local, r);
                       self.dead.insert(l.local);
                     }
-                Statement::Assignment(ref l, RValue::Expr(ref r), _) if self.should_erase(l.local)  && !r.is_call() && r.is_pure() => {
+                Statement::Assignment(ref l, RValue::Expr(ref r), _) if self.should_erase(l.local) && r.is_pure() => {
                       self.dead.insert(l.local);
                 }
                 Statement::Resolve(_,_, ref p) => {
@@ -255,6 +264,7 @@ impl<'tcx> SimplePropagator<'tcx> {
               }
             }
             Statement::Assertion { cond, msg: _ } => self.visit_term(cond),
+            Statement::Call(_, _, _, args, _) => args.iter_mut().for_each(|a| self.visit_expr(a)),
             Statement::AssumeBorrowInv(_) => {},
             Statement::AssertTyInv( _) => {},
         }
@@ -272,7 +282,7 @@ impl<'tcx> SimplePropagator<'tcx> {
 
     fn visit_expr(&mut self, e: &mut Expr<'tcx>) {
         match &mut e.kind {
-            ExprKind::Move(p) | ExprKind::Copy(p) => {
+            ExprKind::Operand(Operand::Move(p) | Operand::Copy(p)) => {
               if let Some(l) = p.as_symbol() && let Some(v) = self.prop.remove(&l) {
                 *e = v;
               }
@@ -283,7 +293,6 @@ impl<'tcx> SimplePropagator<'tcx> {
             }
             ExprKind::UnaryOp(_, e) => self.visit_expr(e),
             ExprKind::Constructor(_, _, es) => es.iter_mut().for_each(|e| self.visit_expr(e)),
-            ExprKind::Call(_, _, es) => es.iter_mut().for_each(|e| self.visit_expr(e)),
             ExprKind::Constant(t) => self.visit_term(t),
             ExprKind::Cast(e, _, _) => self.visit_expr(e),
             ExprKind::Tuple(es) => es.iter_mut().for_each(|e| self.visit_expr(e)),

creusot/src/backend/program.rs

@@ -7,11 +7,12 @@ use super::{
 };
 use crate::{
     backend::{
-        closure_generic_decls, optimization, place,
-        place::translate_rplace,
+        closure_generic_decls, optimization,
+        place::{self, translate_rplace},
         ty::{self, translate_closure_ty, translate_ty},
     },
     ctx::{BodyId, CloneMap, TranslationCtx},
+    fmir::Operand,
     translation::{
         binop_to_binop,
         fmir::{
@@ -25,7 +26,7 @@ use crate::{
 use rustc_hir::{def_id::DefId, Unsafety};
 use rustc_middle::{
     mir::{BasicBlock, BinOp, ProjectionElem},
-    ty::TyKind,
+    ty::{GenericArgsRef, TyKind},
 };
 use rustc_span::{Span, DUMMY_SP};
 use rustc_type_ir::{IntTy, UintTy};
@@ -301,11 +302,11 @@ impl<'tcx> Expr<'tcx> {
         locals: &LocalDecls<'tcx>,
     ) -> Exp {
         let e = match self.kind {
-            ExprKind::Move(pl) => {
+            ExprKind::Operand(Operand::Move(pl)) => {
                 // TODO invalidate original place
                 pl.as_rplace(ctx, names, locals)
             }
-            ExprKind::Copy(pl) => pl.as_rplace(ctx, names, locals),
+            ExprKind::Operand(Operand::Copy(pl)) => pl.as_rplace(ctx, names, locals),
             ExprKind::BinOp(BinOp::BitAnd, l, r) if l.ty.is_bool() => {
                 l.to_why(ctx, names, locals).lazy_and(r.to_why(ctx, names, locals))
             }
@@ -338,36 +339,6 @@ impl<'tcx> Expr<'tcx> {
                 let ctor = names.constructor(id, subst);
                 Exp::Constructor { ctor, args }
             }
-            ExprKind::Call(id, subst, args) => {
-                let mut args: Vec<_> =
-                    args.into_iter().map(|a| a.to_why(ctx, names, locals)).collect();
-                let fname = names.value(id, subst);
-
-                let exp = if ctx.is_closure(id) {
-                    assert!(args.len() == 2, "closures should only have two arguments (env, args)");
-
-                    let real_sig =
-                        ctx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);
-                    let closure_arg_count = real_sig.inputs().skip_binder().len();
-                    let names = ('a'..).take(closure_arg_count);
-
-                    let mut closure_args = vec![args.remove(0)];
-
-                    closure_args
-                        .extend(names.clone().map(|nm| Exp::impure_var(nm.to_string().into())));
-
-                    Exp::Let {
-                        pattern: Pattern::TupleP(
-                            names.map(|nm| Pattern::VarP(nm.to_string().into())).collect(),
-                        ),
-                        arg: Box::new(args.remove(0)),
-                        body: Box::new(Exp::impure_qvar(fname).app(closure_args)),
-                    }
-                } else {
-                    Exp::impure_qvar(fname).app(args)
-                };
-                exp
-            }
             ExprKind::Constant(c) => lower_impure(ctx, names, &c),
             ExprKind::Tuple(f) => {
                 Exp::Tuple(f.into_iter().map(|f| f.to_why(ctx, names, locals)).collect())
@@ -455,15 +426,14 @@ impl<'tcx> Expr<'tcx> {
 
     fn invalidated_places(&self, places: &mut Vec<(fmir::Place<'tcx>, Span)>) {
         match &self.kind {
-            ExprKind::Move(p) => places.push((p.clone(), self.span)),
-            ExprKind::Copy(_) => {}
+            ExprKind::Operand(Operand::Move(p)) => places.push((p.clone(), self.span)),
+            ExprKind::Operand(_) => {}
             ExprKind::BinOp(_, l, r) => {
                 l.invalidated_places(places);
                 r.invalidated_places(places)
             }
             ExprKind::UnaryOp(_, e) => e.invalidated_places(places),
             ExprKind::Constructor(_, _, es) => es.iter().for_each(|e| e.invalidated_places(places)),
-            ExprKind::Call(_, _, es) => es.iter().for_each(|e| e.invalidated_places(places)),
             ExprKind::Constant(_) => {}
             ExprKind::Cast(e, _, _) => e.invalidated_places(places),
             ExprKind::Tuple(es) => es.iter().for_each(|e| e.invalidated_places(places)),
@@ -729,18 +699,24 @@ impl<'tcx> Statement<'tcx> {
                 let rhs = rhs.to_why(ctx, names, locals);
                 let mut exps =
                     vec![place::create_assign_inner(ctx, names, locals, &lhs, rhs, span)];
-                for (pl, pl_span) in invalid {
-                    let ty = pl.ty(ctx.tcx, locals);
-                    let ty = translate_ty(ctx, names, pl_span.substitute_dummy(span), ty);
-                    exps.push(place::create_assign_inner(
-                        ctx,
-                        names,
-                        locals,
-                        &pl,
-                        Exp::Any(ty),
-                        pl_span,
-                    ));
+                invalidate_places(ctx, names, locals, span, invalid, &mut exps);
+
+                exps
+            }
+            Statement::Call(dest, fun_id, subst, args, span) => {
+                let mut invalid = Vec::new();
+                args.iter().for_each(|a| a.invalidated_places(&mut invalid));
+
+                let mut exp = func_call_to_why3(ctx, names, locals, fun_id, subst, args);
+
+                if let Some(attr) = ctx.span_attr(span) {
+                    exp = Exp::Attr(attr, Box::new(exp));
                 }
+
+                let mut exps =
+                    vec![place::create_assign_inner(ctx, names, locals, &dest, exp, span)];
+                invalidate_places(ctx, names, locals, span, invalid, &mut exps);
+
                 exps
             }
             Statement::Resolve(id, subst, pl) => {
@@ -779,6 +755,56 @@ impl<'tcx> Statement<'tcx> {
     }
 }
 
+fn invalidate_places<'tcx>(
+    ctx: &mut Why3Generator<'tcx>,
+    names: &mut CloneMap<'tcx>,
+    locals: &LocalDecls<'tcx>,
+    span: Span,
+    invalid: Vec<(Place<'tcx>, Span)>,
+    out: &mut Vec<mlcfg::Statement>,
+) {
+    for (pl, pl_span) in invalid {
+        let ty = pl.ty(ctx.tcx, locals);
+        let ty = translate_ty(ctx, names, pl_span.substitute_dummy(span), ty);
+        out.push(place::create_assign_inner(ctx, names, locals, &pl, Exp::Any(ty), pl_span));
+    }
+}
+
+fn func_call_to_why3<'tcx>(
+    ctx: &mut Why3Generator<'tcx>,
+    names: &mut CloneMap<'tcx>,
+    locals: &LocalDecls<'tcx>,
+    id: DefId,
+    subst: GenericArgsRef<'tcx>,
+    args: Vec<Expr<'tcx>>,
+) -> Exp {
+    let mut args: Vec<_> = args.into_iter().map(|a| a.to_why(ctx, names, locals)).collect();
+    let fname = names.value(id, subst);
+
+    let exp = if ctx.is_closure(id) {
+        assert!(args.len() == 2, "closures should only have two arguments (env, args)");
+
+        let real_sig = ctx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);
+        let closure_arg_count = real_sig.inputs().skip_binder().len();
+        let names = ('a'..).take(closure_arg_count);
+
+        let mut closure_args = vec![args.remove(0)];
+
+        closure_args.extend(names.clone().map(|nm| Exp::impure_var(nm.to_string().into())));
+
+        Exp::Let {
+            pattern: Pattern::TupleP(
+                names.map(|nm| Pattern::VarP(nm.to_string().into())).collect(),
+            ),
+            arg: Box::new(args.remove(0)),
+            body: Box::new(Exp::impure_qvar(fname).app(closure_args)),
+        }
+    } else {
+        Exp::impure_qvar(fname).app(args)
+    };
+    exp
+}
+
 pub(crate) fn int_to_prelude(ity: IntTy) -> PreludeModule {
     match ity {
         IntTy::Isize => PreludeModule::Isize,

creusot/src/translation.rs

@@ -100,7 +100,7 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box<dyn Error>>
                 let outputs = why3.output_filenames(());
                 let crate_name = why3.crate_name(LOCAL_CRATE);
 
-                let libname = format!("{}-{}.mlcfg", crate_name.as_str(), why3.crate_types()[0]);
+                let libname = format!("{}-{}.coma", crate_name.as_str(), why3.crate_types()[0]);
 
                 let directory = if why3.opts.in_cargo {
                     let mut dir = outputs.out_directory.clone();

creusot/src/translation/fmir.rs

@@ -42,7 +42,9 @@ pub enum Statement<'tcx> {
     Resolve(DefId, GenericArgsRef<'tcx>, Place<'tcx>),
     Assertion { cond: Term<'tcx>, msg: String },
     AssumeBorrowInv(Place<'tcx>),
+    // Todo: fold into `Assertion`
     AssertTyInv(Place<'tcx>),
+    Call(Place<'tcx>, DefId, GenericArgsRef<'tcx>, Vec<Expr<'tcx>>, Span),
 }
 
 // Re-organize this completely
@@ -68,16 +70,18 @@ pub struct Expr<'tcx> {
 }
 
 #[derive(Clone, Debug)]
-pub enum ExprKind<'tcx> {
-    // Extract this into a standalone `Operand` type
+pub enum Operand<'tcx> {
     Move(Place<'tcx>),
     Copy(Place<'tcx>),
+}
+
+#[derive(Clone, Debug)]
+pub enum ExprKind<'tcx> {
+    Operand(Operand<'tcx>),
     // Revisit whether this is a good idea to allow general expression trees.
     BinOp(BinOp, Box<Expr<'tcx>>, Box<Expr<'tcx>>),
     UnaryOp(UnOp, Box<Expr<'tcx>>),
     Constructor(DefId, GenericArgsRef<'tcx>, Vec<Expr<'tcx>>),
-    // Should this be a statement?
-    Call(DefId, GenericArgsRef<'tcx>, Vec<Expr<'tcx>>),
     Constant(Term<'tcx>),
     Cast(Box<Expr<'tcx>>, Ty<'tcx>, Ty<'tcx>),
     Tuple(Vec<Expr<'tcx>>),
@@ -89,12 +93,10 @@ pub enum ExprKind<'tcx> {
 impl<'tcx> Expr<'tcx> {
     pub fn is_call(&self) -> bool {
         match &self.kind {
-            ExprKind::Move(_) => false,
-            ExprKind::Copy(_) => false,
+            ExprKind::Operand(_) => false,
             ExprKind::BinOp(_, _, _) => false,
             ExprKind::UnaryOp(_, _) => false,
             ExprKind::Constructor(_, _, _) => false,
-            ExprKind::Call(_, _, _) => true,
             ExprKind::Constant(_) => false,
             ExprKind::Cast(_, _, _) => false,
             ExprKind::Tuple(_) => false,
@@ -106,8 +108,7 @@ impl<'tcx> Expr<'tcx> {
 
     pub fn is_pure(&self) -> bool {
         match &self.kind {
-            ExprKind::Move(_) => true,
-            ExprKind::Copy(_) => true,
+            ExprKind::Operand(_) => true,
             ExprKind::BinOp(
                 BinOp::Add | BinOp::Mul | BinOp::Rem | BinOp::Div | BinOp::Sub,
                 _,
@@ -117,7 +118,6 @@ impl<'tcx> Expr<'tcx> {
             ExprKind::UnaryOp(UnOp::Neg, _) => false,
             ExprKind::UnaryOp(_, _) => true,
             ExprKind::Constructor(_, _, es) => es.iter().all(|e| e.is_pure()),
-            ExprKind::Call(_, _, es) => es.iter().all(|e| e.is_pure()),
             ExprKind::Constant(_) => true,
             ExprKind::Cast(_, _, _) => false,
             ExprKind::Tuple(es) => es.iter().all(|e| e.is_pure()),

creusot/src/translation/function.rs

@@ -348,8 +348,8 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     // Useful helper to translate an operand
     pub(crate) fn translate_operand(&mut self, operand: &Operand<'tcx>) -> Expr<'tcx> {
         let kind = match operand {
-            Operand::Copy(pl) => ExprKind::Copy(self.translate_place(*pl)),
-            Operand::Move(pl) => ExprKind::Move(self.translate_place(*pl)),
+            Operand::Copy(pl) => ExprKind::Operand(fmir::Operand::Copy(self.translate_place(*pl))),
+            Operand::Move(pl) => ExprKind::Operand(fmir::Operand::Move(self.translate_place(*pl))),
             Operand::Constant(c) => {
                 return crate::constant::from_mir_constant(self.param_env(), self.ctx, c)
             }

creusot/src/translation/function/statement.rs

@@ -1,6 +1,7 @@
 use super::BodyTranslator;
 use crate::{
     analysis::NotFinalPlaces,
+    fmir::Operand,
     translation::{
         fmir::{self, Expr, ExprKind, RValue},
         specification::inv_subst,
@@ -90,7 +91,8 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                         return;
                     }
 
-                    ExprKind::Copy(self.translate_place(self.compute_ref_place(*pl, loc)))
+                    let op = Operand::Copy(self.translate_place(self.compute_ref_place(*pl, loc)));
+                    ExprKind::Operand(op)
                 }
                 Mut { .. } => {
                     if self.erased_locals.contains(pl.local) {
@@ -158,7 +160,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             }
             Rvalue::Len(pl) => {
                 let e = Expr {
-                    kind: ExprKind::Copy(self.translate_place(*pl)),
+                    kind: ExprKind::Operand(Operand::Copy(self.translate_place(*pl))),
                     ty: pl.ty(self.body, self.tcx).ty,
                     span: DUMMY_SP,
                 };