diff --git a/src/phl/README.md b/src/phl/README.md index ac483ef19..e08241aef 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -83,7 +83,7 @@ Run the test suite with `EC_RECHECK=1` to exercise every migrated checker. ## Program transformations Tactics that replace the program by an equivalent one and keep the judgement -(rndsem, rcond, swap, and later inline, …) go through **one** trusted +(rndsem, rcond, swap, inline, …) go through **one** trusted transformation rule per logic, `t__transform` (`EcTransform`; equiv: one side at a time), parameterized by an entry of a catalogue: @@ -107,7 +107,7 @@ equiv: one side at a time), parameterized by an entry of a catalogue: Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), `rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push` -(`EcTrMatchPush`) and `swap` (`EcTrSwap`). `if-push` / `match-push` push +(`EcTrMatchPush`), `swap` (`EcTrSwap`) and `inline` (`EcTrInline`). `if-push` / `match-push` push the continuation of a leading conditional / `match` into its branches: the `if` and `match` tactics are push + rule on the conditional alone (`EcIf`, `EcMatch`). diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index bce9d6b40..d529e573c 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -387,7 +387,14 @@ Current catalogue: at a resolved path to a gap `t` outside it; the independence of the exchanged statements and the absence of `raise` are checked by the entry; no obligation, same memory), used by `swap` (and `interleave`, a sequence - of swaps) in every logic. + of swaps) in every logic; +- `inline` (`EcTrInline`, inlining the calls selected by a resolved pattern + of integer offsets, possibly nested in the branches of an `if`, `while` or + `match`: arguments assigned to fresh copies of the parameters, body with + parameters and locals renamed to fresh program variables added to the + memory, result assigned (component-wise through fresh variables for a + tuple pattern without `tuple`); no obligation), used by `inline` in every + logic. The decisions of a conditional or a match are computed by `EcPlRCond`. The `if` and `match` tactics are push + rule on the conditional alone: they @@ -395,8 +402,7 @@ push the continuation into the branches (when there is one) through the transformation rule (on each side, for the two-sided equiv forms), then apply the `if` / `match` rule of their logic (`EcIf`, `EcMatch`), stated on the conditional alone. Further entries come -with the tactics that use them: inline, kill/alias/cfold/set and proc -rewrite. +with the tactics that use them: kill/alias/cfold/set and proc rewrite. Exception: the framed form of `match C k` (used when the variables of the discriminant `e` are neither read nor written by the prefix, and the diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index abf74758b..6c05f6fb9 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -5,18 +5,22 @@ open EcMaps open EcLocation open EcPath open EcAst -open EcTypes open EcModules -open EcFol -open EcEnv -open EcPV open EcCoreGoal open EcLowGoal -open EcLowPhlGoal (* -------------------------------------------------------------------- *) -type i_pat = +(* The [inline] tactic is derived: it resolves the calls to inline to a + pattern of integer offsets and applies the [inline] program + transformation ([EcTrInline]) through the transformation rule of the + goal's logic ([EcTransform]; equiv: one side at a time). The + derived tactic is the same in every logic, so this module holds it + directly (one line per logic), with the resolution and the + elaboration. *) + +(* -------------------------------------------------------------------- *) +type i_pat = EcTrInline.i_pat = | IPpat | IPif of s_pat pair | IPwhile of s_pat @@ -25,219 +29,21 @@ type i_pat = and s_pat = (int * i_pat) list (* -------------------------------------------------------------------- *) -module LowSubst = struct - let pvsubst m pv = - odfl pv (PVMap.find pv m) - - let rec esubst m e = - match e.e_node with - | Evar pv -> e_var (pvsubst m pv) e.e_ty - | _ -> EcTypes.e_map (fun ty -> ty) (esubst m) e - - let lvsubst m lv = - match lv with - | LvVar (pv, ty) -> LvVar (pvsubst m pv, ty) - | LvTuple pvs -> LvTuple (List.map (fst_map (pvsubst m)) pvs) - - let rec isubst m (i : instr) = - let esubst = esubst m in - let ssubst = ssubst m in - - match i.i_node with - | Sasgn (lv, e) -> i_asgn (lvsubst m lv, esubst e) - | Srnd (lv, e) -> i_rnd (lvsubst m lv, esubst e) - | Scall (lv, f, es) -> i_call (lv |> omap (lvsubst m), f, List.map esubst es) - | Sif (c, s1, s2) -> i_if (esubst c, ssubst s1, ssubst s2) - | Swhile (e, stmt) -> i_while (esubst e, ssubst stmt) - | Smatch (e, bs) -> i_match (esubst e, List.Smart.map (snd_map ssubst) bs) - | Sraise e -> i_raise (esubst e) - | Sabstract _ -> i - - and issubst m (is : instr list) = - List.Smart.map (isubst m) is - - and ssubst m (st : stmt) = - stmt (issubst m st.s_node) -end - -(* --------------------------------------------------------------------- *) -module LowInternal = struct - let inline ~use_tuple tc me sp s = - let hyps = FApi.tc1_hyps tc in - let env = LDecl.toenv hyps in - - let inline1 ~inloop me lv p args = - let p = EcEnv.NormMp.norm_xfun env p in - let f = EcEnv.Fun.by_xpath p env in - let fdef = - match f.f_def with - | FBdef def -> def - | _ -> begin - tc_error_lazy !!tc (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "abstract function `%a' cannot be inlined" - (EcPrinting.pp_funname ppe) p) - end - in - - (* The callee's parameters and locals become fresh variables of the - * caller. Outside of a loop, these variables are never written - * before the inlined body, and hence hold, as the callee's locals, - * an unconstrained initial value. Inside a loop body, they are - * shared by all iterations and start with the value left by the - * previous one, whereas a call starts with fresh locals. Inlining - * is then only sound if the callee never reads a local before - * writing it (parameters are written by the prelude): the inlined - * code does not depend on the initial value of these variables. *) - if inloop then begin - let uninit = get_uninit_read_of_fun f in - if not (EcSymbols.Ssym.is_empty uninit) then - tc_error_lazy !!tc (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "function `%a' cannot be inlined inside a loop: \ - it may use the uninitialized local variable(s): %a" - (EcPrinting.pp_funname ppe) p - (EcPrinting.pp_list ", " EcSymbols.pp_symbol) - (EcSymbols.Ssym.elements uninit)) - end; - let _params = - let named_arg ov = - match ov.ov_name with - | None -> assert false - | Some v -> { v_name = v; v_type = ov.ov_type } - in List.map named_arg f.f_sig.fs_anames - in - let me, anames = EcMemory.bindall_fresh f.f_sig.fs_anames me in - let me, lnames = EcMemory.bindall_fresh (List.map ovar_of_var fdef.f_locals) me in - let subst = - let for1 mx v x = - PVMap.add (pv_loc (oget v.ov_name)) (pv_loc (oget x.ov_name)) mx - in - let mx = PVMap.create env in - let mx = List.fold_left2 for1 mx f.f_sig.fs_anames anames in - let mx = List.fold_left2 for1 mx (List.map ovar_of_var fdef.f_locals) lnames in - mx - in - - let prelude = - let newpv = List.map (fun x -> pv_loc (oget x.ov_name), x.ov_type) anames in - if List.length newpv = List.length args then - List.map2 (fun npv e -> i_asgn (LvVar npv, e)) newpv args - else - match newpv with - | [x] -> [i_asgn(LvVar x, e_tuple args)] - | _ -> [i_asgn(LvTuple newpv, e_tuple args)] - in - - let body = LowSubst.ssubst subst fdef.f_body in - - let me, resasgn = - match fdef.f_ret, lv with - | None, _ -> me , [] - | Some _, None -> me, [] - | Some r, Some (LvTuple lvs) when not use_tuple -> - let r = LowSubst.esubst subst r in - let vlvs = - List.map (fun (x,ty) -> { ov_name = Some (symbol_of_pv x); ov_type = ty}) lvs in - let me, auxs = EcMemory.bindall_fresh vlvs me in - let auxs = List.map (fun v -> pv_loc (oget v.ov_name), v.ov_type) auxs in - let s1 = - let doit i auxi = i_asgn(LvVar auxi, e_proj_simpl r i (snd auxi)) in - List.mapi doit auxs in - let s2 = - List.map2 (fun lv (pv, ty) -> i_asgn(LvVar lv, e_var pv ty)) lvs auxs in - me, s1 @ s2 - - | Some r, Some lv -> - let r = LowSubst.esubst subst r in - me, [i_asgn (lv, r)] in - - me, prelude @ body.s_node @ resasgn in - - let rec inline_i ~inloop me ip i = - match ip, i.i_node with - | IPpat, Scall (lv, p, args) -> - inline1 ~inloop me lv p args - | IPif (sp1, sp2), Sif (e, s1, s2) -> - let me, s1 = inline_s ~inloop me sp1 s1.s_node in - let me, s2 = inline_s ~inloop me sp2 s2.s_node in - me, [i_if (e, stmt s1, stmt s2)] - | IPwhile sp, Swhile (e, s) -> - let me, s = inline_s ~inloop:true me sp s.s_node in - me, [i_while (e, stmt s)] - | IPmatch sps, Smatch (e, bs) -> - let me, bs = List.fold_left_map (fun me (sp, (xs, s)) -> - let me, s = inline_s ~inloop me sp s.s_node in (me, (xs, stmt s))) - me (List.combine sps bs) - in me, [i_match (e, bs)] - - | _, _ -> assert false (* FIXME error message *) - - and inline_s ~inloop me sp s = - match sp with - | [] -> me, s - | (toskip, ip)::sp -> - let r, i, s = List.pivot_at toskip s in - let me, si = inline_i ~inloop me ip i in - let me, s = inline_s ~inloop me sp s in - (me, List.rev_append r (si @ s)) - - in - - snd_map stmt (inline_s ~inloop:false me sp s.s_node) -end - -(* -------------------------------------------------------------------- *) -let t_inline_hoare_r ~use_tuple sp tc = - let hs = tc1_as_hoareS tc in - let (_,mt), stmt = LowInternal.inline ~use_tuple tc hs.hs_m sp hs.hs_s in - let concl = f_hoareS mt (hs_pr hs) stmt (hs_po hs) in - - FApi.xmutate1 tc `Inline [concl] +let tr_inline ~use_tuple sp = + EcTrInline.TrInline { tri_pat = sp; tri_use_tuple = use_tuple } -(* -------------------------------------------------------------------- *) -let t_inline_ehoare_r ~use_tuple sp tc = - let ehs = tc1_as_ehoareS tc in - let (_,mt), stmt = LowInternal.inline ~use_tuple tc ehs.ehs_m sp ehs.ehs_s in - let concl = f_eHoareS mt (ehs_pr ehs) stmt (ehs_po ehs) in +let t_inline_hoare ~use_tuple sp = + EcHoareTransform.t_hoare_transform { htr_tr = tr_inline ~use_tuple sp } - FApi.xmutate1 tc `Inline [concl] - -(* -------------------------------------------------------------------- *) -let t_inline_bdhoare_r ~use_tuple sp tc = - let bhs = tc1_as_bdhoareS tc in - let (_, mt), stmt = LowInternal.inline ~use_tuple tc bhs.bhs_m sp bhs.bhs_s in - let concl = f_bdHoareS mt (bhs_pr bhs) stmt (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in +let t_inline_ehoare ~use_tuple sp = + EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr_inline ~use_tuple sp } +let t_inline_bdhoare ~use_tuple sp = + EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr_inline ~use_tuple sp } - FApi.xmutate1 tc `Inline [concl] - -(* -------------------------------------------------------------------- *) -let t_inline_equiv_r ~use_tuple side sp tc = - let es = tc1_as_equivS tc in - let concl = - match side with - | `Left -> - let ((_,mt), stmt) = LowInternal.inline ~use_tuple tc es.es_ml sp es.es_sl in - f_equivS mt (snd es.es_mr) (es_pr es) stmt es.es_sr (es_po es) - | `Right -> - let ((_,mt), stmt) = LowInternal.inline ~use_tuple tc es.es_mr sp es.es_sr in - f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl stmt (es_po es) - in - - FApi.xmutate1 tc `Inline [concl] - -(* -------------------------------------------------------------------- *) -let t_inline_hoare ~use_tuple = - FApi.t_low1 "hoare-inline" (t_inline_hoare_r ~use_tuple) -let t_inline_ehoare ~use_tuple = - FApi.t_low1 "hoare-inline" (t_inline_ehoare_r ~use_tuple) -let t_inline_bdhoare ~use_tuple = - FApi.t_low1 "bdhoare-inline" (t_inline_bdhoare_r ~use_tuple) -let t_inline_equiv ~use_tuple = - FApi.t_low2 "equiv-inline" (t_inline_equiv_r ~use_tuple) +let t_inline_equiv ~use_tuple side sp = + EcEquivTransform.t_equiv_transform + { etr_side = side; etr_tr = tr_inline ~use_tuple sp } (* -------------------------------------------------------------------- *) module HiInternal = struct diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index 34783ccde..f3def0378 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -34,10 +34,10 @@ open EcEnv [EcTrMatchPush] (pushing the continuation of a leading conditional / [match] into its branches; the [if] and [match] tactics are push + rule on the conditional alone), [EcTrSwap] (moving a block of a possibly - nested block). Entries live in [rules/transforms/], as - [EcTr]. The framed form of [match C k] changes the precondition: - it is not a transformation, but a separate rule of each logic - ([EcRMatch]). *) + nested block) and [EcTrInline] (inlining procedure calls). Entries live + in [rules/transforms/], as [EcTr]. The framed form of [match C k] + changes the precondition: it is not a transformation, but a separate + rule of each logic ([EcRMatch]). *) (* -------------------------------------------------------------------- *) (* An entry of the catalogue, with its resolved parameters. *) diff --git a/src/phl/rules/transforms/ecTrInline.ml b/src/phl/rules/transforms/ecTrInline.ml new file mode 100644 index 000000000..4c4bd6a6f --- /dev/null +++ b/src/phl/rules/transforms/ecTrInline.ml @@ -0,0 +1,194 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcModules +open EcPV +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the [inline] transformation, resolved: the calls to + inline are selected by a pattern of integer offsets. *) +type i_pat = + | IPpat + | IPif of s_pat pair + | IPwhile of s_pat + | IPmatch of s_pat list + +and s_pat = (int * i_pat) list + +type tr_inline = { + tri_pat : s_pat; + tri_use_tuple : bool; +} + +type EcPlTransform.transform += TrInline of tr_inline + +(* -------------------------------------------------------------------- *) +(* Renaming of program variables in a statement. *) +module Subst = struct + let pvsubst m pv = + odfl pv (PVMap.find pv m) + + let rec esubst m e = + match e.e_node with + | Evar pv -> e_var (pvsubst m pv) e.e_ty + | _ -> EcTypes.e_map (fun ty -> ty) (esubst m) e + + let lvsubst m lv = + match lv with + | LvVar (pv, ty) -> LvVar (pvsubst m pv, ty) + | LvTuple pvs -> LvTuple (List.map (fst_map (pvsubst m)) pvs) + + let rec isubst m (i : instr) = + let esubst = esubst m in + let ssubst = ssubst m in + + match i.i_node with + | Sasgn (lv, e) -> i_asgn (lvsubst m lv, esubst e) + | Srnd (lv, e) -> i_rnd (lvsubst m lv, esubst e) + | Scall (lv, f, es) -> i_call (lv |> omap (lvsubst m), f, List.map esubst es) + | Sif (c, s1, s2) -> i_if (esubst c, ssubst s1, ssubst s2) + | Swhile (e, stmt) -> i_while (esubst e, ssubst stmt) + | Smatch (e, bs) -> i_match (esubst e, List.Smart.map (snd_map ssubst) bs) + | Sraise e -> i_raise (esubst e) + | Sabstract _ -> i + + and issubst m (is : instr list) = + List.Smart.map (isubst m) is + + and ssubst m (st : stmt) = + stmt (issubst m st.s_node) +end + +(* -------------------------------------------------------------------- *) +let invalid_pattern () = + raise (InvalidTransform "invalid inlining pattern") + +(* Inline the call [lv <- p(args)]: returns the extended memory and the + inlined instructions. [inloop] holds iff the call is in a loop body. *) +let inline1 ~use_tuple ~inloop env me lv p args = + let p = EcEnv.NormMp.norm_xfun env p in + let f = EcEnv.Fun.by_xpath p env in + let fdef = + match f.f_def with + | FBdef def -> def + | _ -> + let ppe = EcPrinting.PPEnv.ofenv env in + raise (InvalidTransform + (Format.asprintf "abstract function `%a' cannot be inlined" + (EcPrinting.pp_funname ppe) p)) in + + (* The callee's parameters and locals become fresh variables of the + * caller. Outside of a loop, these variables are never written + * before the inlined body, and hence hold, as the callee's locals, + * an unconstrained initial value. Inside a loop body, they are + * shared by all iterations and start with the value left by the + * previous one, whereas a call starts with fresh locals. Inlining + * is then only sound if the callee never reads a local before + * writing it (parameters are written by the prelude): the inlined + * code does not depend on the initial value of these variables. *) + if inloop then begin + let uninit = EcCoreModules.get_uninit_read_of_fun f in + if not (EcSymbols.Ssym.is_empty uninit) then + let ppe = EcPrinting.PPEnv.ofenv env in + raise (InvalidTransform + (Format.asprintf + "function `%a' cannot be inlined inside a loop: \ + it may use the uninitialized local variable(s): %a" + (EcPrinting.pp_funname ppe) p + (EcPrinting.pp_list ", " EcSymbols.pp_symbol) + (EcSymbols.Ssym.elements uninit))) + end; + + let me, anames = EcMemory.bindall_fresh f.f_sig.fs_anames me in + let me, lnames = EcMemory.bindall_fresh (List.map ovar_of_var fdef.f_locals) me in + let subst = + let for1 mx v x = + PVMap.add (pv_loc (oget v.ov_name)) (pv_loc (oget x.ov_name)) mx + in + let mx = PVMap.create env in + let mx = List.fold_left2 for1 mx f.f_sig.fs_anames anames in + let mx = List.fold_left2 for1 mx (List.map ovar_of_var fdef.f_locals) lnames in + mx + in + + let prelude = + let newpv = List.map (fun x -> pv_loc (oget x.ov_name), x.ov_type) anames in + if List.length newpv = List.length args then + List.map2 (fun npv e -> i_asgn (LvVar npv, e)) newpv args + else + match newpv with + | [x] -> [i_asgn(LvVar x, e_tuple args)] + | _ -> [i_asgn(LvTuple newpv, e_tuple args)] + in + + let body = Subst.ssubst subst fdef.f_body in + + let me, resasgn = + match fdef.f_ret, lv with + | None, _ -> me , [] + | Some _, None -> me, [] + | Some r, Some (LvTuple lvs) when not use_tuple -> + let r = Subst.esubst subst r in + let vlvs = + List.map (fun (x,ty) -> { ov_name = Some (symbol_of_pv x); ov_type = ty}) lvs in + let me, auxs = EcMemory.bindall_fresh vlvs me in + let auxs = List.map (fun v -> pv_loc (oget v.ov_name), v.ov_type) auxs in + let s1 = + let doit i auxi = i_asgn(LvVar auxi, e_proj_simpl r i (snd auxi)) in + List.mapi doit auxs in + let s2 = + List.map2 (fun lv (pv, ty) -> i_asgn(LvVar lv, e_var pv ty)) lvs auxs in + me, s1 @ s2 + + | Some r, Some lv -> + let r = Subst.esubst subst r in + me, [i_asgn (lv, r)] in + + me, prelude @ body.s_node @ resasgn + +(* -------------------------------------------------------------------- *) +(* Inline, in program order, the calls selected by the pattern. *) +let inline (p : tr_inline) (ctxt : tr_ctxt) (s : stmt) = + let use_tuple = p.tri_use_tuple in + + let rec inline_i ~inloop me ip i = + match ip, i.i_node with + | IPpat, Scall (lv, p, args) -> + inline1 ~use_tuple ~inloop ctxt.trc_env me lv p args + | IPif (sp1, sp2), Sif (e, s1, s2) -> + let me, s1 = inline_s ~inloop me sp1 s1.s_node in + let me, s2 = inline_s ~inloop me sp2 s2.s_node in + me, [i_if (e, stmt s1, stmt s2)] + | IPwhile sp, Swhile (e, s) -> + let me, s = inline_s ~inloop:true me sp s.s_node in + me, [i_while (e, stmt s)] + | IPmatch sps, Smatch (e, bs) when List.length sps = List.length bs -> + let me, bs = List.fold_left_map (fun me (sp, (xs, s)) -> + let me, s = inline_s ~inloop me sp s.s_node in (me, (xs, stmt s))) + me (List.combine sps bs) + in me, [i_match (e, bs)] + + | _, _ -> invalid_pattern () + + and inline_s ~inloop me sp s = + match sp with + | [] -> me, s + | (toskip, ip)::sp -> + let r, i, s = + try List.pivot_at toskip s + with Not_found | Invalid_argument _ -> invalid_pattern () in + let me, si = inline_i ~inloop me ip i in + let me, s = inline_s ~inloop me sp s in + (me, List.rev_append r (si @ s)) + + in + + let me, s = inline_s ~inloop:false ctxt.trc_me p.tri_pat s.s_node in + { trr_me = me; trr_s = stmt s; trr_obl = []; } + +let () = + register (function + | TrInline p -> Some (inline p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrInline.mli b/src/phl/rules/transforms/ecTrInline.mli new file mode 100644 index 000000000..468429ae1 --- /dev/null +++ b/src/phl/rules/transforms/ecTrInline.mli @@ -0,0 +1,59 @@ +(* -------------------------------------------------------------------- *) +open EcUtils + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +(* The calls to inline, as a resolved pattern over the statement: [s_pat] + is a list of [(n, ip)], [n] being the number of instructions skipped + since the previous selected one (or since the start of the block), and + [ip] what to do with the selected instruction: inline it ([IPpat], a + call), or descend into its branches ([IPif], [IPwhile], [IPmatch], one + sub-pattern per branch, in order). *) +type i_pat = + | IPpat + | IPif of s_pat pair + | IPwhile of s_pat + | IPmatch of s_pat list + +and s_pat = (int * i_pat) list + +type tr_inline = { + tri_pat : s_pat; (* the calls to inline (resolved pattern) *) + tri_use_tuple : bool; (* assign a tuple result as a whole *) +} + +(* [TrInline { tri_pat = sp; tri_use_tuple = ut }] — inlines the calls + selected by [sp], at any depth. Each selected call + [x <- f(e1, ..., en)], with [f] (normalized) defined by + [proc f(a1, ..., an) = { var l1 ... lk; b; return r }], becomes + + a1', ..., an' <- e1, ..., en; b'; x <- r' + + where [a1' ... an'], [l1' ... lk'] are fresh program variables added to + the memory (in this order), [b'] and [r'] are [b] and [r] with the + parameters and locals renamed to them, and the arguments are assigned + one by one (when there are as many as parameters), as a tuple + otherwise. The return assignment is omitted when there is no [x] or no + [r]. When [x] is a tuple pattern [(x1, ..., xm)] and [not ut], it is + instead + + t1 <- r'.`1; ...; tm <- r'.`m; x1 <- t1; ...; xm <- tm + + with [t1 ... tm] fresh program variables named after [x1 ... xm], added + to the memory after the locals. Calls are inlined in program order, so + the memory grows in that order. No obligation. + + Fails with "abstract function `f' cannot be inlined" when a selected + [f] has no concrete definition, and with "invalid inlining pattern" + when [sp] does not match the statement (a skip out of range, an + [IPpat] not on a call, a sub-pattern not on an instruction of that + kind or with the wrong number of branches). + + A selected call inside a loop body is rejected ("function `f' cannot + be inlined inside a loop") when [f] may read one of its locals before + writing it: there, the fresh variables are shared by all iterations + and hold the values left by the previous one, whereas a call starts + with fresh locals. Otherwise, every read of a fresh variable in the + inlined code follows a write in the same iteration. *) +type EcPlTransform.transform += TrInline of tr_inline diff --git a/tests/inline.ec b/tests/inline.ec new file mode 100644 index 000000000..cfd70bcf4 --- /dev/null +++ b/tests/inline.ec @@ -0,0 +1,247 @@ +(* The [inline] tactic, as the [inline] program transformation applied + through the transformation rule of each logic: every form (by name, + all, occurrences, code position, with and without [tuple]), every + logic, both equiv sides, nested positions and the error paths. The + remaining goals are admitted with [admit. qed.], so that the proof tree + (and thus the transformation nodes) is rechecked under EC_RECHECK. *) +require import AllCore Xreal. + +exception oops of int. + +(* -------------------------------------------------------------------- *) +module type T = { + proc o(x : int) : int +}. + +module N = { + var g : int + + (* parameters and locals named like the caller's variables *) + proc f(x : int, y : int) : int * int = { + var z; + z <- x + y; + g <- z; + return (z, x); + } + + (* a single parameter of tuple type *) + proc p(xy : int * int) : int = { + return xy.`1 + xy.`2; + } + + (* no return value *) + proc u(x : int) = { + g <- x; + } + + (* calls another procedure *) + proc h(x : int) : int = { + var r; + r <@ p(x, x); + return r; + } +}. + +module O = { + proc o(x : int) : int = { + return x; + } +}. + +module M (A : T) = { + (* calls at the top level, in the branches of an [if], of a [while] and + of a [match] *) + proc main(o : int option) : int = { + var x, y, z, a, b; + x <- 0; + y <- 1; + (x, y) <@ N.f(x, y); + if (x < y) { + z <@ N.p(x, y); + } else { + N.u(y); + z <@ N.h(x); + } + while (x < 10) { + (a, b) <@ N.f(x, z); + x <- x + 1; + } + match o with + | None => { z <@ N.h(z); } + | Some v => { N.u(v); z <@ A.o(v); } + end; + return x + y + z; + } + + (* a call followed by a raise *) + proc e(x : int) : int = { + x <@ N.p(x, x); + if (x < 0) { raise (oops x); } + return x; + } +}. + +(* -------------------------------------------------------------------- *) +(* hoare *) +lemma hoare_all (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline *. +admit. qed. + +lemma hoare_name (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline N.f N.u. +inline N.h. +inline N.p. +admit. qed. + +lemma hoare_minus (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline * - N.f. +inline N - N.h. +admit. qed. + +lemma hoare_tuple (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline [tuple] N.f. +admit. qed. + +lemma hoare_notuple (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline [-tuple] N.f. +admit. qed. + +lemma hoare_occs (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline (2 4) N. +inline (1) N.f. +admit. qed. + +lemma hoare_codepos (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc; inline 6#Some.1. +inline 6#None.1. +inline 5.1. +inline 4?2. +inline 4?1. +inline 4.1. +inline 3. +admit. qed. + +lemma hoare_exn : hoare [M(O).e : true ==> true | oops v => v < 0]. +proof. +proc; inline *. +admit. qed. + +lemma hoare_nothing : hoare [N.p : true ==> true]. +proof. +proc; inline *. +admit. qed. + +lemma hoare_errors (A <: T) : hoare [M(A).main : true ==> true]. +proof. +proc. +fail inline{1} *. +fail inline{1} 3. +fail inline 1. +fail inline 6#Some.2. +fail inline A.o. +admit. qed. + +(* -------------------------------------------------------------------- *) +(* ehoare: by name or all only *) +lemma ehoare_all (A <: T) : ehoare [M(A).main : (1%xr) ==> (1%xr)]. +proof. +proc; inline *. +admit. qed. + +lemma ehoare_name (A <: T) : ehoare [M(A).main : (1%xr) ==> (1%xr)]. +proof. +proc; inline [-tuple] N.f. +inline N.h N.p. +admit. qed. + +lemma ehoare_errors (A <: T) : ehoare [M(A).main : (1%xr) ==> (1%xr)]. +proof. +proc. +fail inline (1). +fail inline 3. +fail inline{1} *. +fail inline A.o. +admit. qed. + +(* -------------------------------------------------------------------- *) +(* phoare *) +lemma phoare_all (A <: T) : phoare [M(A).main : true ==> true] = 1%r. +proof. +proc; inline *. +admit. qed. + +lemma phoare_name (A <: T) : phoare [M(A).main : true ==> true] <= 1%r. +proof. +proc; inline [-tuple] N.f. +inline N.h. +admit. qed. + +lemma phoare_occs (A <: T) : phoare [M(A).main : true ==> true] >= 1%r. +proof. +proc; inline (1 3) N. +admit. qed. + +lemma phoare_codepos (A <: T) : phoare [M(A).main : true ==> true] = 1%r. +proof. +proc; inline 5.1. +inline 4?1. +inline 6#None.1. +admit. qed. + +lemma phoare_errors (A <: T) : phoare [M(A).main : true ==> true] = 1%r. +proof. +proc. +fail inline{2} *. +fail inline 2. +fail inline A.o. +admit. qed. + +(* -------------------------------------------------------------------- *) +(* equiv: both sides, one side at a time *) +lemma equiv_all (A <: T) : equiv [M(A).main ~ M(A).main : ={o} ==> true]. +proof. +proc; inline *. +admit. qed. + +lemma equiv_left (A <: T) : equiv [M(A).main ~ M(A).main : ={o} ==> true]. +proof. +proc; inline{1} *. +inline{2} [-tuple] N.f. +inline{2} N - N.f. +admit. qed. + +lemma equiv_both_name (A <: T) : equiv [M(A).main ~ M(A).main : ={o} ==> true]. +proof. +proc; inline N.f. +admit. qed. + +lemma equiv_occs (A <: T) : equiv [M(A).main ~ M(O).main : ={o} ==> true]. +proof. +proc; inline{1} (1 4) N. +inline{2} (5) N. +admit. qed. + +lemma equiv_codepos (A <: T) : equiv [M(A).main ~ M(O).main : ={o} ==> true]. +proof. +proc; inline{1} 5.1. +inline{2} 6#Some.2. +inline{2} 4?2. +inline{1} 3. +admit. qed. + +lemma equiv_errors (A <: T) : equiv [M(A).main ~ M(O).main : ={o} ==> true]. +proof. +proc. +fail inline (1). +fail inline 3. +fail inline{1} 1. +fail inline{1} 6#Some.2. +fail inline{1} A.o. +admit. qed.