Mlw: keep "execution cty" with Eexec

this allows us to infer missing post-conditions and to convert
partial applications to mappings at the same time, and saves
effort for Vc.

src/mlw/expr.ml

@@ -303,7 +303,7 @@ type expr = {
 and expr_node =
   | Evar    of pvsymbol
   | Econst  of Number.constant
-  | Eexec   of cexp
+  | Eexec   of cexp * cty
   | Eassign of assign list
   | Elet    of let_defn * expr
   | Eif     of expr * expr * expr
@@ -373,8 +373,8 @@ let find_effect pr loc e =
     if not (pr e.e_effect) then loc else
     let loc = if e.e_loc = None then loc else e.e_loc in
     let loc = match e.e_node with
-      | Eexec {c_node = Cfun d} -> find loc d
-      | _ ->                e_fold find loc e in
+      | Eexec ({c_node = Cfun d},_) -> find loc d
+      | _ ->                    e_fold find loc e in
     raise (FoundExpr (loc,e)) in
   try find loc e, e with FoundExpr (loc,e) -> loc, e
 
@@ -476,11 +476,11 @@ let rs_true  = rs_of_ls fs_bool_true
 let rs_false = rs_of_ls fs_bool_false
 
 let is_e_true e = match e.e_node with
-  | Eexec {c_node = Capp (s,[])} -> rs_equal s rs_true
+  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_true
   | _ -> false
 
 let is_e_false e = match e.e_node with
-  | Eexec {c_node = Capp (s,[])} -> rs_equal s rs_false
+  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_false
   | _ -> false
 
 let t_void = t_tuple []
@@ -503,8 +503,8 @@ let rec raw_of_expr e = copy_labels e (match e.e_node with
   | Econst n -> t_const n
   | Epure t -> t
   | Eghost e -> raw_of_expr e
-  | Eexec {c_cty = {cty_post = []}} -> raise Exit
-  | Eexec {c_cty = {cty_args = al; cty_post = q::_}} ->
+  | Eexec (_,{cty_post = []}) -> raise Exit
+  | Eexec (_,{cty_args = al; cty_post = q::_}) ->
       let v, q = open_post q in
       let rec find h = match h.t_node with
         | Tapp (ps, [{t_node = Tvar u}; t])
@@ -585,8 +585,8 @@ let rec post_of_expr res e = match e.e_node with
   | _ when ity_equal e.e_ity ity_unit -> t_true
   | Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
   | Eabsurd -> copy_labels e t_false
-  | Eexec {c_cty = c} ->
-      let conv q = open_post_with_args res c.cty_args q in
+  | Eexec (_,c) ->
+      let conv q = open_post_with res q in
       copy_labels e (t_and_l (List.map conv c.cty_post))
   | Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
       copy_labels e (t_subst_single v.pv_vs t_void (post_of_expr res e))
@@ -676,21 +676,12 @@ let e_let ld e =
 
 (* callable expressions *)
 
-let e_exec ({c_cty = cty} as c) = match cty.cty_args with
-  | _::_ as al ->
-      (* unlike for RLpv or RLls, we do not purify the signature,
-         so the regions are now frozen and we have to forbid all
-         effects, including allocation *)
-      check_effects cty; check_state cty;
-      if not (Sreg.is_empty cty.cty_effect.eff_resets) then Loc.errorm
-        "This function has side effects, it cannot be used as pure";
-      let func a ity = ity_func a.pv_ity ity in
-      let ity = List.fold_right func al cty.cty_result in
-      let ghost = List.exists (fun a -> a.pv_ghost) al in
-      let eff = eff_ghostify ghost cty.cty_effect in
-      mk_expr (Eexec c) ity MaskVisible eff
-  | [] ->
-      mk_expr (Eexec c) cty.cty_result cty.cty_mask cty.cty_effect
+let e_exec c =
+  let cty = match c with
+    | {c_node = Cfun e; c_cty = {cty_post = []} as cty} ->
+        cty_exec (cty_add_post cty (local_post_of_expr e))
+    | _ -> cty_exec c.c_cty in
+  mk_expr (Eexec (c, cty)) cty.cty_result cty.cty_mask cty.cty_effect
 
 let c_any c = mk_cexp Cany c
 
@@ -775,7 +766,7 @@ let fs_void = fs_tuple 0
 let e_void = e_app rs_void [] [] ity_unit
 
 let is_e_void e = match e.e_node with
-  | Eexec {c_node = Capp (s,[])} -> rs_equal s rs_void
+  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_void
   | _ -> false
 
 let rs_func_app = rs_of_ls fs_func_app
@@ -931,7 +922,7 @@ let cty_add_variant d varl = let add s (t,_) = t_freepvs s t in
 let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
   | Evar _ | Econst _ | Eassign _ | Eassert _ | Epure _ | Eabsurd -> e
   | Eghost e -> e_ghostify true (e_rs_subst sm e)
-  | Eexec c -> e_exec (c_rs_subst sm c)
+  | Eexec (c,_) -> e_exec (c_rs_subst sm c)
   | Elet (LDvar (v,d),e) ->
       let d = e_rs_subst sm d in
       ity_equal_check d.e_ity v.pv_ity;
@@ -1245,7 +1236,7 @@ and print_cexp exec pri fmt {c_node = n; c_cty = c} = match n with
 and print_enode pri fmt e = match e.e_node with
   | Evar v -> print_pv fmt v
   | Econst c -> print_const fmt c
-  | Eexec c -> print_cexp true pri fmt c
+  | Eexec (c,_) -> print_cexp true pri fmt c
   | Elet (LDvar (v,e1), e2)
     when v.pv_vs.vs_name.id_string = "_" && ity_equal v.pv_ity ity_unit ->
       fprintf fmt (protect_on (pri > 0) "%a;@\n%a")

src/mlw/expr.mli

@@ -117,7 +117,7 @@ type expr = private {
 and expr_node = private
   | Evar    of pvsymbol
   | Econst  of Number.constant
-  | Eexec   of cexp
+  | Eexec   of cexp * cty
   | Eassign of assign list
   | Elet    of let_defn * expr
   | Eif     of expr * expr * expr

src/mlw/ity.ml

@@ -1154,33 +1154,6 @@ let open_post_with t q = match q.t_node with
   | Teps bf -> t_open_bound_with t bf
   | _ -> invalid_arg "Ity.open_post_with"
 
-let open_post_with_args t al q =
-  if al = [] then open_post_with t q else
-  let v, h = open_post q in
-  let al = List.map (fun v -> v.pv_vs) al in
-  let res = t_func_app_l t (List.map t_var al) in
-  let rec down h s el vl = match el, vl with
-    | {t_node = Tvar u}::el, v::vl when vs_equal u v ->
-        down h s el vl
-    | el, [] ->
-        let tyl = List.map (fun v -> v.vs_ty) al in
-        let ty = Opt.map (Util.const v.vs_ty) s.ls_value in
-        t_equ t (t_app_partial s (List.rev el) tyl ty)
-    | _ -> t_subst_single v res h in
-  let rec conv h = t_label_copy h (match h.t_node with
-    | Tapp (ps, [{t_node = Tvar u}; {t_node = Tapp(s, tl)} as t])
-      when ls_equal ps ps_equ && vs_equal v u && t_v_occurs v t = 0 ->
-        down h s (List.rev tl) (List.rev al)
-    | Tbinop (Tiff, {t_node =
-        Tapp (ps, [{t_node = Tvar u}; {t_node = Tapp (fs, [])}])},
-        ({t_node = Tapp (s, tl)} as f))
-      when ls_equal ps ps_equ && vs_equal v u &&
-           ls_equal fs fs_bool_true && t_v_occurs v f = 0 ->
-        down h s (List.rev tl) (List.rev al)
-    | Tbinop (Tand, f, g) -> t_and (conv f) (conv g)
-    | _ -> t_subst_single v res h) in
-  t_forall_close_simp al [] (conv h)
-
 type cty = {
   cty_args   : pvsymbol list;
   cty_pre    : pre list;
@@ -1371,6 +1344,63 @@ let cty_tuple args =
   let frz = List.fold_right freeze_pv args isb_empty in
   cty_unsafe [] [] [post] Mexn.empty Mpv.empty eff res mask frz
 
+let cty_exec ({cty_effect = eff} as c) =
+  (* we do not purify the signature, so the regions will be frozen
+     in the resulting pvsymbol. Thus, we have to forbid all effects,
+     including allocation. TODO/FIXME: we should probably forbid
+     the rest of the signature to contain regions at all. *)
+  if eff.eff_oneway then Loc.errorm
+    "This function may not terminate, it cannot be used as pure";
+  if not (eff_pure eff && Sreg.is_empty eff.eff_resets) then Loc.errorm
+    "This function has side effects, it cannot be used as pure";
+  if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm
+    "This function is stateful, it cannot be used as pure";
+  let ity = List.fold_right (fun a ity ->
+    ity_func a.pv_ity ity) c.cty_args c.cty_result in
+  let gh = List.exists (fun a -> a.pv_ghost) c.cty_args in
+  let eff = eff_ghostify (gh || mask_ghost c.cty_mask) eff in
+  (* translate the specification *)
+  let al = List.map (fun a -> a.pv_vs) c.cty_args in
+  let pre = List.map (fun f -> t_forall_close_simp al [] f) c.cty_pre in
+  let res = create_vsymbol (id_fresh "result") (ty_of_ity ity) in
+  let res_al = t_func_app_l (t_var res) (List.map t_var al) in
+  let oldies = Mpv.fold (fun {pv_vs = o} {pv_vs = v} s ->
+    Mvs.add o (t_var v) s) c.cty_oldies Mvs.empty in
+  let conv_post q =
+    let v, h = open_post q in
+    let rec down h s el vl = match el, vl with
+      | {t_node = Tvar u}::el, v::vl when vs_equal u v ->
+          down h s el vl
+      | el, [] ->
+          let tyl = List.map (fun v -> v.vs_ty) al in
+          let ty = Opt.map (Util.const v.vs_ty) s.ls_value in
+          t_equ (t_var res) (t_app_partial s (List.rev el) tyl ty)
+      | _ -> t_subst_single v res_al h in
+    let rec conv h = t_label_copy h (match h.t_node with
+      | Tapp (ps, [{t_node = Tvar u}; {t_node = Tapp(s, tl)} as t])
+        when ls_equal ps ps_equ && vs_equal v u && t_v_occurs v t = 0 ->
+          down h s (List.rev tl) (List.rev al)
+      | Tbinop (Tiff, {t_node =
+          Tapp (ps, [{t_node = Tvar u}; {t_node = Tapp (fs, [])}])},
+          ({t_node = Tapp (s, tl)} as f))
+        when ls_equal ps ps_equ && vs_equal v u &&
+             ls_equal fs fs_bool_true && t_v_occurs v f = 0 ->
+          down h s (List.rev tl) (List.rev al)
+      | Tbinop (Tand, f, g) -> t_and (conv f) (conv g)
+      | _ -> t_subst_single v res_al h) in
+    let h = t_forall_close_simp al [] (conv (t_subst oldies h)) in
+    create_post res h in
+  let post = List.map conv_post c.cty_post in
+  (* we do not modify cty_freeze to respect the invariants of the cty type.
+     It is sound to assume that the resulting cty can be executed multiple
+     times, producing mappings with different type variables and regions.
+     Still, Expr never uses it like this: it is merely attached to Eexec
+     to provide the converted specification for VC generation. Pvsymbols
+     that carry the resulting value, however, cannot be generalized. *)
+  cty_unsafe [] pre post Mexn.empty Mpv.empty eff ity MaskVisible c.cty_freeze
+
+let cty_exec c = if c.cty_args = [] then c else cty_exec c
+
 let cty_read_pre pvs c =
   (* the external reads are already frozen and
      the arguments should stay instantiable *)

src/mlw/ity.mli

@@ -388,7 +388,6 @@ type post = term  (** postcondition: eps result . post_fmla *)
 
 val open_post : post -> vsymbol * term
 val open_post_with : term -> post -> term
-val open_post_with_args : term -> pvsymbol list -> post -> term
 
 val create_post : vsymbol -> term -> post
 
@@ -429,6 +428,11 @@ val cty_tuple : pvsymbol list -> cty
 (** [cty_tuple pvl] returns a nullary tuple-valued cty with
     an appropriate [cty_mask]. *)
 
+val cty_exec : cty -> cty
+(** [cty_exec cty] converts a cty of a partial application into
+    a cty of a fully applied application, returning a mapping.
+    The original cty must be effectless. *)
+
 val cty_ghost : cty -> bool
 (** [cty_ghost cty] returns [cty.cty_effect.eff_ghost] *)
 

src/mlw/pdecl.ml

@@ -190,7 +190,8 @@ let get_syms node pure =
     | Evar _ | Econst _ | Eabsurd -> syms
     | Eassert (_,t) | Epure t -> syms_term syms t
     | Eghost e -> syms_expr syms e
-    | Eexec c -> syms_cexp syms c
+    | Eexec (c,_) when c.c_cty.cty_args = [] -> syms_cexp syms c
+    | Eexec (c,cty) -> syms_cty (syms_cexp syms c) cty
     | Eassign al ->
         let syms_as syms (v,s,u) =
           syms_pv (syms_pv (Sid.add s.rs_name syms) u) v in

src/mlw/pmodule.ml

@@ -752,7 +752,7 @@ let clone_ppat cl sm pp mask =
 let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
   | Evar v -> e_var (sm_find_pv sm v)
   | Econst c -> e_const c
-  | Eexec c -> e_exec (clone_cexp cl sm c)
+  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
   | Eassign asl ->
       let conv (r,f,v) =
         e_var (sm_find_pv sm r), cl_find_rs cl f, e_var (sm_find_pv sm v) in

src/mlw/vc.ml

@@ -244,10 +244,6 @@ let wp_of_pre ({letrec_ps = lps} as env) loc lab = function
       wp_and p (wp_of_inv lab pl)
   | pl -> wp_of_inv lab pl
 
-let wp_of_pre env loc lab al pl =
-  let p = wp_of_pre env loc lab pl in
-  wp_forall (List.map (fun v -> v.pv_vs) al) p
-
 let wp_of_post lab ity = function
   | q::ql ->
       let v, q = open_post q in let t = t_var_or_void v in
@@ -263,10 +259,10 @@ let rec push_stop lab f = match f.t_node with
 
 let sp_of_pre lab pl = t_and_l (List.map (push_stop lab) pl)
 
-let sp_of_post lab v al ql =
+let sp_of_post lab v ql =
   let t = t_var_or_void v in
   (* remove the post-condition of () *)
-  let push q = match open_post_with_args t al q with
+  let push q = match open_post_with t q with
     | {t_node = Tapp (ps, [_; {t_ty = Some ty}])}
       when ls_equal ps ps_equ && ty_equal ty ty_unit -> t_true
     | f -> push_stop lab f in
@@ -328,8 +324,8 @@ let extract_defn v sp =
     | _ -> raise Exit in
   try Some (extract sp) with Exit -> None
 
-let wp_close lab v al ql wp =
-  let sp = sp_of_post lab v al ql in
+let wp_close lab v ql wp =
+  let sp = sp_of_post lab v ql in
   match extract_defn v sp with
   | Some (t, sp) -> wp_let v t (sp_implies sp wp)
   | None ->      wp_forall [v] (sp_implies sp wp)
@@ -644,14 +640,14 @@ let rec wp_expr env e res q xq = match e.e_node with
   | Econst c ->
       t_subst_single res (vc_label e (t_const c)) q
 
-  | Eexec {c_node = nd; c_cty = {cty_args = al} as c} ->
-      let q = wp_close expl_post res al c.cty_post q in
-      let join cq (v,q) = wp_close expl_xpost v [] cq q in
+  | Eexec (ce, c) ->
+      let q = wp_close expl_post res c.cty_post q in
+      let join cq (v,q) = wp_close expl_xpost v cq q in
       let w = wp_inter_mexn q join (cty_xpost_real c) xq in
       let w = bind_oldies c (wp_havoc env c.cty_effect w) in
-      let p = wp_of_pre env e.e_loc expl_pre al c.cty_pre in
-      let vc = match nd with
-        | Cfun e0 -> vc_fun env true c e0
+      let p = wp_of_pre env e.e_loc expl_pre c.cty_pre in
+      let vc = match ce.c_node with
+        | Cfun e -> vc_fun env true ce.c_cty e
         | Capp _ | Cpur _ | Cany -> t_true in
       vc_label e (wp_and vc (wp_and p w))
 
@@ -781,17 +777,17 @@ and sp_expr env e res xres dst = match e.e_node with
       let t = vc_label e (t_const c) in
       t_true, t_equ (t_var res) t, Mexn.empty
 
-  | Eexec {c_node = nd; c_cty = {cty_args = al} as c} ->
-      let sp_of_post lab v al ql =
-        let cq = sp_of_post lab v al ql in
+  | Eexec (ce, c) ->
+      let sp_of_post lab v ql =
+        let cq = sp_of_post lab v ql in
         let sp = sp_havoc env e.e_effect v cq dst in
         bind_oldies c sp in
-      let ne = sp_of_post expl_post res al c.cty_post in
-      let join v ql = sp_of_post expl_xpost v [] ql in
+      let ne = sp_of_post expl_post res c.cty_post in
+      let join v ql = sp_of_post expl_xpost v ql in
       let ex = inter_mexn join xres (cty_xpost_real c) in
-      let ok = wp_of_pre env e.e_loc expl_pre al c.cty_pre in
-      let vc = match nd with
-        | Cfun e0 -> vc_fun env false c e0
+      let ok = wp_of_pre env e.e_loc expl_pre c.cty_pre in
+      let vc = match ce.c_node with
+        | Cfun e -> vc_fun env false ce.c_cty e
         | Capp _ | Cpur _ | Cany -> t_true in
       out_label e (wp_and vc ok, ne, ex)