sessions

creusot/src/backend/program.rs

@@ -1,5 +1,7 @@
 use super::{
-    clone_map::PreludeModule, dependency::ExtendedId, place::rplace_to_expr, signature::signature_of, term::lower_pure, CloneSummary, GraphDepth, Namer, TransId, Why3Generator
+    clone_map::PreludeModule, dependency::ExtendedId, place::rplace_to_expr,
+    signature::signature_of, term::lower_pure, CloneSummary, GraphDepth, Namer, TransId,
+    Why3Generator,
 };
 use crate::{
     backend::{
@@ -19,7 +21,7 @@ use crate::{
 };
 use itertools::Itertools;
 use rustc_ast::token::TokenKind::Interpolated;
-use rustc_hir::def_id::DefId;
+use rustc_hir::{def_id::DefId, Unsafety};
 use rustc_middle::{
     mir::{self, BasicBlock, BinOp, ProjectionElem, UnOp, START_BLOCK},
     ty::{AdtDef, GenericArgsRef, Ty, TyKind},
@@ -1176,20 +1178,71 @@ fn func_call_to_why3<'tcx>(
     locals: &LocalDecls<'tcx>,
     id: DefId,
     subst: GenericArgsRef<'tcx>,
-    args: Vec<Operand<'tcx>>,
+    mut args: Vec<Operand<'tcx>>,
     istmts: &mut Vec<IntermediateStmt>,
 ) -> (coma::Expr, Vec<coma::Arg>) {
-    let args: Vec<_> = args
-        .into_iter()
-        .map(|a| a.to_why(ctx, names, locals, istmts))
-        .map(|a| coma::Arg::Term(a))
-        .collect();
+    // TODO(xavier): Perform this simplification earlier
+    // Eliminate "rust-call" ABI
+    let args: Vec<_> = if ctx.is_closure_or_coroutine(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 Operand::Move(pl) = args.remove(1) else { panic!() };
+        let mut args = vec![coma::Arg::Term(args.remove(0).to_why(ctx,names,locals, istmts))];
+        for (ix, inp) in real_sig.inputs().skip_binder().iter().enumerate() {
+            let mut arg = pl.clone();
+            arg.projection.push(ProjectionElem::Field(ix.into(), *inp));
+            args.push(coma::Arg::Term(Operand::Move(arg).to_why(ctx, names, locals, istmts)));
+        }
+        args
+    } else {
+        args.into_iter()
+            .map(|a| a.to_why(ctx, names, locals, istmts))
+            .map(|a| coma::Arg::Term(a))
+            .collect()
+    };
 
     let fname = names.value(id, subst);
 
     (coma::Expr::Symbol(fname), args)
 }
 
+// fn func_call_to_why3<'tcx>(
+//     ctx: &mut Why3Generator<'tcx>,
+//     names: &mut Dependencies<'tcx>,
+//     locals: &LocalDecls<'tcx>,
+//     id: DefId,
+//     subst: GenericArgsRef<'tcx>,
+//     args: Vec<Operand<'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_or_coroutine(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::var(nm.to_string())));
+
+//         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::qvar(fname).app(closure_args)),
+//         }
+//     } else {
+//         Exp::qvar(fname).app(args)
+//     };
+//     exp
+// }
+
 pub(crate) fn binop_to_binop<'tcx, N: Namer<'tcx>>(names: &mut N, ty: Ty, op: mir::BinOp) -> QName {
     let prelude: PreludeModule = match ty.kind() {
         TyKind::Int(ity) => int_to_prelude(*ity),

creusot/tests/should_succeed/bug/206/why3session.xml

@@ -3,17 +3,12 @@
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
-<file format="coma">
+<file format="coma" proved="true">
 <path name=".."/><path name="206.coma"/>
 <theory name="C206_U2_Impl" proved="true">
  <goal name="vc_u2" proved="true">
  <proof prover="0"><result status="valid" time="0.006573" steps="0"/></proof>
  </goal>
 </theory>
-<theory name="C206_Ex">
- <goal name="ex&#39;vc" expl="VC for ex">
- <proof prover="0"><result status="valid" time="0.006735" steps="2"/></proof>
- </goal>
-</theory>
 </file>
 </why3session>

creusot/tests/should_succeed/bug/594.coma

@@ -140,14 +140,18 @@ module C594_TestClosure
        [ &_5 <- (([#"../594.rs" 20 19 20 20] (4 : int32)), _6) ] 
       (any
       [ any_ (_any:(int32, int32))-> (!  [ &_6 <- _any ] 
-        closure0'0 {cl1} {_5} (fun (_ret':int32) ->  [ &_a <- _ret' ] bb1)) ]
+        closure0'0
+          {cl1}
+          {let (l0', _) = _5 in l0'}
+          {let (_, l0') = _5 in l0'}
+          (fun (_ret':int32) ->  [ &_a <- _ret' ] bb1)) ]
       )
     | bb1 = -{resolve'0 cl1}-
        [ &_10 <- (([#"../594.rs" 21 20 21 21] (0 : int32)), ([#"../594.rs" 21 23 21 24] (4 : int32))) ] 
        [ &_9 <- (_10) ] 
       (any
       [ any_ (_any:(int32, int32))-> (!  [ &_10 <- _any ] 
-        closure1'0 {cl2} {_9} (fun (_ret':int32) ->  [ &_b <- _ret' ] bb2)) ]
+        closure1'0 {cl2} {let (l0') = _9 in l0'} (fun (_ret':int32) ->  [ &_b <- _ret' ] bb2)) ]
       )
     | bb2 = -{resolve'1 cl2}-
        [ &_0 <- [#"../594.rs" 15 22 22 1] () ] 

creusot/tests/should_succeed/bug/594/why3session.xml

@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"https://www.why3.org/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
+<file format="coma" proved="true">
+<path name=".."/><path name="594.coma"/>
+<theory name="C594_TestProgram" proved="true">
+ <goal name="vc_test_program" proved="true">
+ <proof prover="0"><result status="valid" time="0.009576" steps="4"/></proof>
+ </goal>
+</theory>
+<theory name="C594_TestClosure_Closure1" proved="true">
+ <goal name="vc_c594_testclosure_closure1" proved="true">
+ <proof prover="0"><result status="valid" time="0.009378" steps="4"/></proof>
+ </goal>
+</theory>
+<theory name="C594_TestClosure_Closure0" proved="true">
+ <goal name="vc_c594_testclosure_closure0" proved="true">
+ <proof prover="0"><result status="valid" time="0.008510" steps="4"/></proof>
+ </goal>
+</theory>
+<theory name="C594_Impl0_TestMethod" proved="true">
+ <goal name="vc_test_method" proved="true">
+ <proof prover="0"><result status="valid" time="0.007230" steps="4"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>