From 195b4b75e821acaada87ad67480aeb7bd114222d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 7 Oct 2026 14:00:08 +0200 Subject: [PATCH] refactor(pl): codetx as program transformations PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `codetx` tactic class (kill, alias, set, set-match, cfold, `case <-` and `simplify if`) onto the transformation rule of each logic: - rules/transforms/ecTr{Kill,Alias,Set,SetMatch,CFold,AsgnCase, SimplifyIf}.ml: seven catalogue entries, with resolved parameters (normalized, possibly nested, code positions; typed expressions; the matched subterm and its occurrences for set-match). Each entry re-checks its side conditions (kill: the killed code writes nothing read by the code that may run after it, loops included, as computed by `EcPV.zpr_pv`, or by the postcondition; set-match: the selected occurrences are alpha-equivalent to the named subterm; the tuple split: the assigned variables are not read by the expression; ...) with today's messages, so the checker re-validates them. - rules/ecPlTransform.ml: a new obligation kind, `OLossless ks` (the statement `ks` is lossless), stated by each of the four transformation rules as phoare [ks : true ==> true] = 1 in the memory of the transformed program: the premise `kill` has always stated. - kill reads the postcondition through the context of the rule, which for hoare includes the exceptional postconditions (as on main since the corresponding fix). - EcMatching.Zipper.zipper_of_nm_cpos: the zipper at a normalized code position, without environment. - EcPhlCodeTx is reduced to derived tactics and a logic-agnostic dispatcher onto the transformation rule of the goal's logic; its interface is unchanged, the no-op FApi.t_low* wrappers are dropped, and it no longer uses EcLowPhlGoal.t_code_transform (still used by EcPhlLoopTx). weakmem changes the memory type of the goal: it is not a program transformation and is left unchanged. Behaviour is otherwise preserved: on the new test, the goals after every step and the error messages of every failing invocation are identical to those of the unmodified build. Anomalies (assertion failures) raised by `case <-` on ill-formed input are kept, their reported source location aside. A new test, tests/codetx.ec, exercises every entry in every logic (hoare, ehoare, phoare, both equiv sides), at top-level and nested positions, the error paths, and the kill of a variable read by an exceptional postcondition (rejected); tests/kill-exn.ec and tests/kill-loop.ec pass unchanged. The stdlib, the unit tests and the examples pass under EC_RECHECK=1 with no RecheckFailure. The transformation checkers, when deliberately broken on the entries of this class, are caught only under EC_RECHECK: on the new test, on the stdlib (bdhoare-transform 1, equiv-transform 2), the other unit tests (hoare-transform 2) and the examples (hoare-transform 1, bdhoare-transform 1); ehoare-transform only by the new test. --- src/ecMatching.ml | 27 + src/ecMatching.mli | 8 + src/phl/README.md | 9 +- src/phl/REFACTORING.md | 54 +- src/phl/ecPhlCodeTx.ml | 616 ++++--------------- src/phl/rules/bdhoare/ecBdHoareTransform.ml | 5 +- src/phl/rules/bdhoare/ecBdHoareTransform.mli | 4 +- src/phl/rules/ecPlTransform.ml | 1 + src/phl/rules/ecPlTransform.mli | 10 +- src/phl/rules/ehoare/ecEHoareTransform.ml | 5 +- src/phl/rules/ehoare/ecEHoareTransform.mli | 4 +- src/phl/rules/equiv/ecEquivTransform.ml | 5 +- src/phl/rules/equiv/ecEquivTransform.mli | 4 +- src/phl/rules/hoare/ecHoareTransform.ml | 5 +- src/phl/rules/hoare/ecHoareTransform.mli | 4 +- src/phl/rules/transforms/ecTrAlias.ml | 72 +++ src/phl/rules/transforms/ecTrAlias.mli | 26 + src/phl/rules/transforms/ecTrAsgnCase.ml | 79 +++ src/phl/rules/transforms/ecTrAsgnCase.mli | 25 + src/phl/rules/transforms/ecTrCFold.ml | 258 ++++++++ src/phl/rules/transforms/ecTrCFold.mli | 40 ++ src/phl/rules/transforms/ecTrKill.ml | 90 +++ src/phl/rules/transforms/ecTrKill.mli | 31 + src/phl/rules/transforms/ecTrSet.ml | 44 ++ src/phl/rules/transforms/ecTrSet.mli | 24 + src/phl/rules/transforms/ecTrSetMatch.ml | 83 +++ src/phl/rules/transforms/ecTrSetMatch.mli | 34 + src/phl/rules/transforms/ecTrSimplifyIf.ml | 116 ++++ src/phl/rules/transforms/ecTrSimplifyIf.mli | 26 + tests/codetx.ec | 436 +++++++++++++ 30 files changed, 1626 insertions(+), 519 deletions(-) create mode 100644 src/phl/rules/transforms/ecTrAlias.ml create mode 100644 src/phl/rules/transforms/ecTrAlias.mli create mode 100644 src/phl/rules/transforms/ecTrAsgnCase.ml create mode 100644 src/phl/rules/transforms/ecTrAsgnCase.mli create mode 100644 src/phl/rules/transforms/ecTrCFold.ml create mode 100644 src/phl/rules/transforms/ecTrCFold.mli create mode 100644 src/phl/rules/transforms/ecTrKill.ml create mode 100644 src/phl/rules/transforms/ecTrKill.mli create mode 100644 src/phl/rules/transforms/ecTrSet.ml create mode 100644 src/phl/rules/transforms/ecTrSet.mli create mode 100644 src/phl/rules/transforms/ecTrSetMatch.ml create mode 100644 src/phl/rules/transforms/ecTrSetMatch.mli create mode 100644 src/phl/rules/transforms/ecTrSimplifyIf.ml create mode 100644 src/phl/rules/transforms/ecTrSimplifyIf.mli create mode 100644 tests/codetx.ec diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 8590bff8c..27eebe0fe 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -650,6 +650,33 @@ module Zipper = struct let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) = fst (zipper_of_cpos_r env cp s) + let zipper_of_nm_cpos ((cpath, cp1) : nm_codepos) (s : stmt) = + let step (zpr, s) ((k, br) : nm_codepos_step) = + let (s1, i, s2) = find_by_nmcpos1 k s in + match i.i_node, br with + | Swhile (e, sw), `Cond true -> + (ZWhile (e, ((s1, s2), zpr)), sw) + + | Sif (e, ifs1, ifs2), `Cond true -> + (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1) + + | Sif (e, ifs1, ifs2), `Cond false -> + (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2) + + | Smatch (e, bs), `Match ix -> + let prebr, (locals, body), postbr = + try List.pivot_at ix bs + with Invalid_argument _ | Not_found -> raise InvalidCPos in + (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body) + + | _ -> raise InvalidCPos + in + + let zpr, s = List.fold_left step (ZTop, s) cpath in + check_nm_cgap1 cp1 s; + let s1, s2 = split_at_nmcgap1 cp1 s in + zipper (List.rev s1) s2 zpr + let zipper_of_cgap (env : EcEnv.env) (cp : codegap) (s : stmt) = fst (zipper_of_cgap_r env cp s) diff --git a/src/ecMatching.mli b/src/ecMatching.mli index e45e50c72..45268266d 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -270,6 +270,14 @@ module Zipper : sig *) val zipper_of_nm_cgap : env -> nm_codegap -> stmt -> zipper + (* Return the zipper for the stmt [stmt] at the normalized code position + * [nm_codepos] (as returned by [zipper_of_cpos_r]): the cursor is before + * the designated instruction, or at the end of its block. Needs no + * environment ([z_env] is unset). Raise [InvalidCPos] if [nm_codepos] is + * not valid for [stmt]. + *) + val zipper_of_nm_cpos : nm_codepos -> stmt -> zipper + (* Return the zipper for the stmt [stmt] from the start of the code position * range [codepos_range]. It also returns a code position relative to * the zipper that represents the final position in the range. diff --git a/src/phl/README.md b/src/phl/README.md index e08241aef..d450b99f0 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -99,15 +99,18 @@ equiv: one side at a time), parameterized by an entry of a catalogue: function, which may extend the memory with fresh program variables. - The obligations are abstract (a small closed set: so far, "every terminating run of the prefix `hd` from the precondition satisfies - `cond`"); each logic's rule states them as its own premises (see its - `.mli`). + `cond`" and "the statement `ks` is lossless"); each logic's rule states + them as its own premises (see its `.mli`). - The node records the transformation and its parameters; the checker ("-transform") re-runs it on the goal's program and compares the subgoals up to conversion (programs up to alpha-equivalence). Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), `rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push` -(`EcTrMatchPush`), `swap` (`EcTrSwap`) and `inline` (`EcTrInline`). `if-push` / `match-push` push +(`EcTrMatchPush`), `swap` (`EcTrSwap`), `inline` (`EcTrInline`), `kill` +(`EcTrKill`), `alias` (`EcTrAlias`), `set` (`EcTrSet`), `set-match` +(`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`) and +`simplify-if` (`EcTrSimplifyIf`). `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 d529e573c..acbe47f78 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -342,18 +342,24 @@ parameterized by an entry of a **catalogue** of transformations: Entries live in `rules/transforms/`, one module `EcTr` each. - **The obligations** are **abstract** and form a small closed set; each logic's rule states them as premises of its own (first, in order, then the - transformed judgement — same pre/post, possibly extended memory). The only - kind so far is `OPrefixPost (hd, cond)`: every terminating run of the prefix - `hd` from the precondition ends in a state satisfying `cond`. Per logic: - - hoare: `hoare [hd : P ==> cond | E]` (the goal's exceptional - postconditions kept); - - ehoare: `hoare [hd : P_bool ==> cond]`, the precondition having the form - ``P_bool `|` f``; - - bdhoare: `hoare [hd : P ==> cond]`; - - equiv (transformation of side `i`): `forall &j, hoare [hd : P ==> cond]`, - the relation read on side `i` with the other memory quantified. - - These are the premises `rcondt` / `rcondf` have always stated. + transformed judgement — same pre/post, possibly extended memory). The + kinds so far: + - `OPrefixPost (hd, cond)`: every terminating run of the prefix `hd` from + the precondition ends in a state satisfying `cond`. Per logic: + - hoare: `hoare [hd : P ==> cond | E]` (the goal's exceptional + postconditions kept); + - ehoare: `hoare [hd : P_bool ==> cond]`, the precondition having the + form ``P_bool `|` f``; + - bdhoare: `hoare [hd : P ==> cond]`; + - equiv (transformation of side `i`): `forall &j, hoare [hd : P ==> + cond]`, the relation read on side `i` with the other memory + quantified. + + These are the premises `rcondt` / `rcondf` have always stated. + - `OLossless ks`: the statement `ks` terminates with probability 1 from + every state; in every logic `phoare [ks : true ==> true] = 1`, in the + memory of the transformed program (the premise `kill` has always + stated). - **The rules** `t__transform` (`rules//EcTransform`; equiv: one side at a time, the other program and memory unchanged) record `(transformation, resolved parameters)` (and the side) in their node. The @@ -394,7 +400,27 @@ Current catalogue: 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. + logic; +- `kill` (`EcTrKill`): removes the `n` instructions `ks` at a (possibly + nested) position, provided that what they write is read neither by the + code that may run after them (in their block and the enclosing ones, and + the guard and whole body of each enclosing loop) nor by the postcondition + (for hoare, including the exceptional ones); obligation `OLossless ks`; +- `alias` (`EcTrAlias`): `lv <- e` / `lv <$ d` / `lv <@ f(a)` becomes + `x' <- e; lv <- x'` (resp. `<$`, `<@`), `x'` a fresh program variable; + no obligation; +- `set` (`EcTrSet`): inserts `x' <- e` at a position, `x'` fresh; no + obligation; +- `set-match` (`EcTrSetMatch`): names the subterm `t` matched in the + expression of an instruction, `x' <- t; i(e[occ := x'])`, the selected + occurrences being alpha-equivalent to `t`; no obligation; +- `cfold` (`EcTrCFold`): propagates an assignment to local variables into + the following instructions as long as valid (eager or not), and + materializes it afterwards; no obligation; +- `asgn-case` (`EcTrAsgnCase`): splits a tuple assignment into one + assignment per variable (`case <-`); no obligation; +- `simplify-if` (`EcTrSimplifyIf`): turns a conditional whose branches are + assignments into a single assignment (`simplify if`); no obligation. 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 @@ -402,7 +428,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: kill/alias/cfold/set and proc rewrite. +with the tactics that use them: the loop transformations 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/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index bba5829c4..da84ea3ed 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -1,9 +1,7 @@ (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree -open EcSymbols open EcAst -open EcTypes open EcModules open EcFol open EcEnv @@ -16,406 +14,127 @@ open EcLowPhlGoal module Mid = EcIdent.Mid module Zpr = EcMatching.Zipper module TTC = EcProofTyping -module Map = Batteries.Map (* -------------------------------------------------------------------- *) -let t_kill_r side cpos olen tc = - let env = FApi.tc1_env tc in - - let kill_stmt (pf, _) (_, po) me zpr = - let (ks, tl) = - match olen with - | None -> (zpr.Zpr.z_tail, []) - | Some len -> - if List.length zpr.Zpr.z_tail < len then - tc_error pf - "cannot find %d consecutive instructions at given position" - len; - List.takedrop len zpr.Zpr.z_tail - in - - (* [ks] is replaced by [skip]. This is sound if [ks] is lossless - (side goal below) and if the variables it writes ([ks_wr]) are - read neither by the postcondition nor by any code that may run - after [ks]: then both programs end in states that agree outside - of [ks_wr]. The code that may run after [ks] is, for each - enclosing block, the code that follows the block's cursor, and, - for each enclosing while loop, the loop guard and the whole loop - body (with [ks] removed): the next iterations run them again, - including the part of the body before [ks]. This is what - [EcPV.zpr_pv `Read `After] computes. *) - let ks_wr = is_write env ks in - let po_rd = PV.fv env (fst me) po in - let af_rd = - EcPV.zpr_pv `Read `After env PV.empty - ((zpr.Zpr.z_head, tl), zpr.Zpr.z_path) in - - let pp_of_name = - let ppe = EcPrinting.PPEnv.ofenv env in - fun fmt x -> - match x with - | `Global p -> EcPrinting.pp_topmod ppe fmt p - | `PV p -> EcPrinting.pp_pv ppe fmt p - in - - begin - match PV.pick (PV.interdep env ks_wr af_rd) with - | None -> () - | Some x -> - tc_error !!tc - "code writes variables (%a) used by the code that may run after it" - pp_of_name x - end; - - begin - match PV.pick (PV.interdep env ks_wr po_rd) with - | None -> () - | Some x -> - tc_error !!tc - "code writes variables (%a) used by the post-condition" - pp_of_name x - end; - let (m, mt) = me in - let kslconcl = EcFol.f_bdHoareS mt {m;inv=f_true} (stmt ks) {m;inv=f_true} FHeq {m;inv=f_r1} in - (me, { zpr with Zpr.z_tail = tl; }, [kslconcl]) - in +(* The code transformations (kill, alias, set, set-match, cfold, the split + of a tuple assignment and simplify-if) are derived, uniformly in every + logic: they resolve their code position (and their other arguments), + check what they always checked (keeping their error messages), and + apply a program transformation of the catalogue ([EcTrKill], + [EcTrAlias], [EcTrSet], [EcTrSetMatch], [EcTrCFold], [EcTrAsgnCase], + [EcTrSimplifyIf]) through the transformation rule of the logic of the + goal ([EcTransform]; for equiv, on the given side). The visible + goals are those of that rule: the obligations of the transformation + (only [kill] has one: [phoare [ks : true ==> true] = 1] for the killed + statement [ks]), then the transformed judgement. As the derived tactics + only differ by the transformation they apply, they share the + logic-agnostic dispatcher [t_transform] below, and no per-logic module. + + [weakmem] is not a program transformation (it changes the memory type + of the goal and adds an implication): it is not migrated. *) - let tr = fun side -> `Kill (side, cpos, olen) in - t_code_transform side cpos tr (t_zip kill_stmt) tc +(* -------------------------------------------------------------------- *) +(* The memory and statement transformed: the program of the goal (hoare, + ehoare, bdhoare) or of the given side (equiv). *) +let tx_stmt (side : oside) (tc : tcenv1) = + match side, (FApi.tc1_goal tc).f_node with + | None, FhoareS hs -> (hs.hs_m, hs.hs_s) + | None, FeHoareS hs -> (hs.ehs_m, hs.ehs_s) + | None, FbdHoareS hs -> (hs.bhs_m, hs.bhs_s) + | None, _ -> + tc_error_noXhl ~kinds:[`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt] !!tc + | Some side, _ -> + let es = tc1_as_equivS tc in + sideif side (es.es_ml, es.es_sl) (es.es_mr, es.es_sr) + +(* Apply the transformation [tr] through the transformation rule of the + logic of the goal (on the given side for equiv). *) +let t_transform (side : oside) (tr : EcPlTransform.transform) (tc : tcenv1) = + match side, (FApi.tc1_goal tc).f_node with + | None, FhoareS _ -> + EcHoareTransform.t_hoare_transform { htr_tr = tr } tc + | None, FeHoareS _ -> + EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr } tc + | None, FbdHoareS _ -> + EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr } tc + | None, _ -> + tc_error_noXhl ~kinds:[`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt] !!tc + | Some side, _ -> + EcEquivTransform.t_equiv_transform { etr_side = side; etr_tr = tr } tc + +(* Resolve a code position of [s] (failing with "invalid code position"). *) +let resolve_cpos (tc : tcenv1) (cpos : Position.codepos) (s : stmt) = + try fst (snd (Zpr.zipper_of_cpos_r (FApi.tc1_env tc) cpos s)) + with Position.InvalidCPos -> tc_error !!tc "invalid code position" (* -------------------------------------------------------------------- *) -let alias_stmt env id (pf, _) me i = - let dopv ty = - let id = odfl "x" (omap EcLocation.unloc id) in - let id = { ov_name = Some id; ov_type = ty; } in - let (me, id) = EcMemory.bind_fresh id me in - (* oget cannot fail — Some in, Some out *) - let pv = pv_loc (oget id.ov_name) in - me, pv in - - match i.i_node with - | Sasgn(lv,e) -> - let ty = e.e_ty in - let (me, pv) = dopv ty in - (me, [i_asgn (LvVar (pv, ty), e); i_asgn (lv, e_var pv ty)]) - | Srnd (lv, e) -> - let ty = proj_distr_ty env e.e_ty in - let (me, pv) = dopv ty in - (me, [i_rnd (LvVar (pv, ty), e); i_asgn (lv, e_var pv ty)]) - | Scall (Some lv, f, args) -> - let ty = (EcEnv.Fun.by_xpath f env).f_sig.fs_ret in - let (me, pv) = dopv ty in - (me, [i_call (Some (LvVar (pv, ty)), f ,args); i_asgn (lv, e_var pv ty)]) - | _ -> - tc_error pf "cannot create an alias for that kind of instruction" - -let t_alias_r side cpos id g = - let env = FApi.tc1_env g in - let tr = fun side -> `Alias (side, cpos) in - t_code_transform side cpos tr (t_fold (alias_stmt env id)) g +let t_kill (side : oside) (cpos : Position.codepos) (olen : int option) tc = + let _, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + t_transform side (EcTrKill.TrKill { trk_at = at; trk_len = olen }) tc (* -------------------------------------------------------------------- *) -let set_stmt (fresh, id) e = - let get_i me = - let id = EcLocation.unloc id in - let v = { ov_name = Some id; ov_type = e.e_ty } in - let (me, id) = EcMemory.bind_fresh v me in - (* oget cannot fail — Some in, Some out *) - let pv = pv_loc (oget id.ov_name) in - - (me, i_asgn (LvVar (pv, e.e_ty), e)) - in +let t_alias (side : oside) (cpos : Position.codepos) (id : psymbol option) tc = + let _, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + let name = odfl "x" (omap EcLocation.unloc id) in + t_transform side (EcTrAlias.TrAlias { tral_at = at; tral_name = name }) tc - let get_i = - if fresh then get_i - else - let res = ref None in - fun me -> - if !res = None then res := Some (get_i me); - oget !res in - fun _ _ me z -> - let me,i = get_i me in - (me, {z with Zpr.z_tail = i::z.Zpr.z_tail},[]) - -let t_set_r side cpos (fresh, id) e tc = - let tr = fun side -> `Set (side, cpos) in - t_code_transform side cpos tr (t_zip (set_stmt (fresh, id) e)) tc +(* -------------------------------------------------------------------- *) +(* The [fresh] flag has no effect: the variable is always fresh. *) +let t_set (side : oside) (cpos : Position.codepos) ((_fresh, id) : bool * psymbol) e tc = + let _, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + t_transform side + (EcTrSet.TrSet { trs_at = at; trs_name = EcLocation.unloc id; trs_e = e }) + tc (* -------------------------------------------------------------------- *) -let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) = - fun (pe, hyps) _ me z -> - let i, is = List.destruct z.Zpr.z_tail in - let e, mk = - let e, kind, mk = - get_expression_of_instruction i |> ofdfl (fun () -> - tc_error pe "targetted instruction should contain an expression" - ) in - - match kind with - | `Sasgn | `Srnd | `Sif | `Smatch -> (e, mk) - | `Swhile -> tc_error pe "while loops not supported" - in +(* Find the subterm matched by the pattern in the expression of the + instruction at the position, and its occurrences. *) +let t_set_match (side : oside) (cpos : Position.codepos) (id : EcSymbols.symbol) ((ue, mev, ptn) : _ * _ * form) tc = + let pe = !!tc in + let hyps = FApi.tc1_hyps tc in + let me, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + let zpr = Zpr.zipper_of_nm_cpos at s in + + let i, _ = List.destruct zpr.Zpr.z_tail in + let e = + let e, kind, _ = + get_expression_of_instruction i |> ofdfl (fun () -> + tc_error pe "targetted instruction should contain an expression" + ) in + + match kind with + | `Sasgn | `Srnd | `Sif | `Smatch -> e + | `Swhile -> tc_error pe "while loops not supported" + in + let subf, occ = try let ptev = EcProofTerm.ptenv pe hyps (ue, mev) in let e = ss_inv_of_expr (fst me) e in let subf, occmode = EcProofTerm.pf_find_occurence_lazy ptev ~ptn e.inv in - let subf = {m=e.m; inv= subf} in + let subf = { m = e.m; inv = subf } in assert (EcProofTerm.can_concretize ptev); - let cpos = + let occ = EcMatching.FPosition.select_form ~xconv:`AlphaEq ~keyed:occmode.k_keyed hyps None subf.inv e.inv in - let v = { ov_name = Some id; ov_type = subf.inv.f_ty } in - let (me, id) = EcMemory.bind_fresh v me in - let pv = pv_loc (oget id.ov_name) in - let e = map_ss_inv2 (fun pv -> EcMatching.FPosition.map cpos (fun _ -> pv)) (f_pvar pv (subf.inv.f_ty) (fst me)) e in - - let i1 = i_asgn (LvVar (pv, subf.inv.f_ty), expr_of_ss_inv subf) in - let i2 = mk (expr_of_ss_inv e) in - - (me, { z with z_tail = i1 :: i2 :: is }, []) + (subf, occ) with EcProofTerm.FindOccFailure _ -> tc_error pe "cannot find an occurrence of the pattern" - -let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc = - let tr = fun side -> `SetMatch (side, cpos) in - t_code_transform side cpos tr - (t_zip (set_match_stmt id pattern)) tc - -(* -------------------------------------------------------------------- *) -(* - Works on a block starting at an assignment to local variables. - - It initializes: - - propagate: a substitution mapping the assigned variables to their values - - preserve : for each propagated variable, the variables that must keep their - current value for that propagated expression to remain valid - - It then scans subsequent instructions from left to right. - - For assignments: - - if the assigned variable is preserved, stop in non-eager mode; in eager - mode, substitute in the right-hand side and promote that variable to the - propagated substitution - - if the assigned variable is already propagated, update its propagated value - and recompute its preservation set - - otherwise, substitute propagated values in the right-hand side and keep the - assignment - - For calls, loops, conditionals, matches, and random samplings: - - continue only if none of the currently propagated or preserved variables is - written by the instruction; in that case, substitute propagated values in - the instruction - - otherwise, stop - - For abstract instructions without calls: - - continue only if they neither read nor write propagated or preserved - variables - - otherwise, stop - - When the scan stops, the remaining propagated substitution is materialized as - assignments appended after the transformed prefix. -*) - -let cfold_stmt - ?(simplify : bool = true) - ?(eager : bool = true) - ((pf, hyps) : proofenv * LDecl.hyps) - (me : memenv) - (olen : int option) - (zpr : Zpr.zipper) -= - let env = LDecl.toenv hyps in - - let e_simplify (e : expr) = - let e = form_of_expr ~m:(fst me) e in - let e = EcReduction.simplify EcReduction.nodelta hyps e in - expr_of_ss_inv { m = fst me; inv = e } in - - let i_simplify (i : instr) = - i_map_expr e_simplify i in - - let e_simplify, i_simplify = - if simplify - then (e_simplify, i_simplify) - else (identity, identity) in - - (* - Process one instruction under the current propagated substitution and - preservation map. - - - `Continue ((subst, preserve), is)` means that propagation may proceed, - with updated state and replacement instructions `is` - - `Interrupt` means that propagation stops before this instruction - - In eager mode, assigning to a preserved variable does not stop the scan: - the assigned expression is first substituted, then that variable is - promoted into the propagated substitution. - *) - let for_instruction (subst, preserve: (expr, unit) Mpv.t * (PV.t Mnpv.t)) (i : instr) = - let esubst subst e = - EcPV.Mpv.esubst env subst e |> e_simplify - in - let isubst subst i = - EcPV.Mpv.isubst env subst i |> i_simplify - in - let is_preserved preserve pv = - Mnpv.exists (fun _ preserve -> EcPV.PV.mem_pv env pv preserve) preserve - in - let is_propagated subst pv = - Mnpv.contains (Mpv.pvs subst) pv - in - let propagated_pvs subst = - (Mpv.pvs subst) |> Mnpv.bindings |> List.fst - in - (* Update preserve vars on assignment to given PV *) - (* Do not include any propagated vars, since these *) - (* are automatically preserved by construction *) - let update_preserved preserve subst pv e = - let rd = EcPV.e_read env e in - let rd = List.fold_left (fun rd pv -> - EcPV.PV.remove env pv rd - ) rd (propagated_pvs subst) - in - Mnpv.add pv rd preserve - in - let promote_preserved_to_propagated subst preserve pv (e:expr) = - let preserve = Mnpv.map (fun preserve -> - PV.remove env pv preserve - ) preserve - in - let subst = Mpv.add env pv e subst in - (subst, preserve) - in - - match i.i_node with - | Sasgn (lv, e) -> - let asgns = explode_assgn lv e in - let exception Abort in - begin try - let (subst, preserve), asgns = List.fold_left_map (fun (subst, preserve) ((pv, t), e) -> - (* 1. When hitting an assignment to a preserved var *) - if is_preserved preserve pv then - if eager (* 1.1 Promote to propagated on eager *) - then - let e = esubst subst e in - promote_preserved_to_propagated subst preserve pv e, None - else raise Abort (* 1.2 Fail on non-eager *) - else - (* 2. When not preserved and not propagated, do nothing *) - if not (is_propagated subst pv) then - (subst, preserve), Some ((pv, t), esubst subst e) - (* 3. When propagated, propagate *) - else - let e = esubst subst e in - let preserve = update_preserved preserve subst pv e in - let subst = Mpv.add env pv e subst in - (subst, preserve), None - ) (subst, preserve) asgns - in - let asgns = List.filter_map identity asgns in - `Continue ((subst, preserve), Option.to_list (i_asgn_of_pve asgns)) - with Abort -> `Interrupt - end - - | Srnd _ - | Scall _ - | Swhile _ - | Sif _ - | Smatch _ -> - let wr = EcPV.i_write env i in - let spvs = Mnpv.keys (Mpv.pvs subst) in - let ppvs = Mnpv.keys preserve in - if - let check = List.for_all (fun pv -> - not @@ EcPV.PV.mem_pv env pv wr) in - check spvs && check ppvs - then - `Continue ((subst, preserve), [isubst subst i]) - else - `Interrupt - - | Sraise _ -> `Interrupt - - | Sabstract id -> - let aus = EcEnv.AbsStmt.byid id env in - begin match aus with - | { aus_calls = []; aus_reads; aus_writes } -> - if List.for_all (fun (pv, _) -> - not ((is_propagated subst pv) || (is_preserved preserve pv)) - ) (aus_reads @ aus_writes) then - `Continue ((subst, preserve), [i]) - else - `Interrupt - | _ -> `Interrupt - end in - let body, epilog = - match olen with - | None -> - (zpr.z_tail, []) - | Some olen -> - if List.length zpr.z_tail < olen+1 then - tc_error pf "expecting at least %d instructions" olen; - List.takedrop (olen+1) zpr.z_tail in - - let _lv, (subst, _preserve), body, rem = - match body with - | { i_node = Sasgn (lv, e) } :: is -> - let asgns = explode_assgn lv e in - let lv = List.fst asgns in - - if not (List.for_all (is_loc -| fst) lv) then - tc_error pf "left-values must be made of local variables only"; - - (* Variables in the domain of substs - are variables to be propagated *) - let subst = - List.fold_left - (fun subst ((pv, _), e) -> Mpv.add env pv e subst) - Mpv.empty asgns in - - let preserve = - List.fold_left - (fun preserve ((pv, _), e) -> - Mnpv.add - pv - EcPV.(PV.remove env pv (e_read env e)) - preserve) - Mnpv.empty - asgns - in - - let (subst, preserve), is, rem = - List.fold_left_map_while for_instruction (subst, preserve) is in - - lv, (subst, preserve), List.flatten is, rem - - | _ -> - tc_error pf "cannot find a left-value assignment at given position" - in - - let asgns = Mnpv.bindings (Mpv.pvs subst) in - - let lv, es = List.map (fun (pv, e) -> - (pv, e_ty e), e) asgns |> List.split - in - - let asgn = - lv_of_list lv - |> Option.map (fun lv -> i_asgn (lv, e_tuple es)) - |> Option.to_list in - - let zpr = - { zpr with Zpr.z_tail = body @ asgn @ rem @ epilog } in - - (me, zpr, []) + t_transform side + (EcTrSetMatch.TrSetMatch + { trsm_at = at; trsm_name = id; trsm_sub = subf; trsm_occ = occ; }) + tc (* -------------------------------------------------------------------- *) let t_cfold @@ -425,15 +144,11 @@ let t_cfold (olen : int option) (tc : tcenv1) = - let tr = fun side -> `Fold (side, cpos, olen) in - let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in - t_code_transform side cpos tr (t_zip cb) tc - -(* -------------------------------------------------------------------- *) -let t_kill = FApi.t_low3 "code-tx-kill" t_kill_r -let t_alias = FApi.t_low3 "code-tx-alias" t_alias_r -let t_set = FApi.t_low4 "code-tx-set" t_set_r -let t_set_match = FApi.t_low4 "code-tx-set-match" t_set_match_r + let _, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + t_transform side + (EcTrCFold.TrCFold { trcf_at = at; trcf_len = olen; trcf_eager = eager; }) + tc (* -------------------------------------------------------------------- *) let process_cfold (info : pcfold) tc = @@ -521,44 +236,13 @@ let process_weakmem (side, id, params) tc = FApi.xmutate1 tc `WeakenMem [concl] (* -------------------------------------------------------------------- *) +(* [case <- p]: split the tuple assignment at [p]. The checks done before + the transformation (and their failures, assertion failures and an + uncaught [InvalidCPos] included) are those of the tactic before its + migration. *) let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) = let (env, _, concl) = FApi.tc1_eflat tc in - let change (i : instr) = - if not (is_asgn i) then - tc_error !!tc "the code position should target an assignment"; - - let lv, e = destr_asgn i in - - let pvl = - match lv with - | LvVar _ -> PV.empty - | LvTuple lvs -> - let lvs = List.tl (List.rev lvs) in - let lvs = Option.get (lv_of_list lvs) in - EcPV.lp_write env lvs in - - let pve = EcPV.e_read env e in - let lv = lv_to_list lv in - - if not (EcPV.PV.indep env pvl pve) then - assert false; - - let e = - match lv, e.e_node with - | [_], _ -> [e] - | _ , Etuple es -> es - | _ ,_ -> - let tys = - match (EcEnv.Ty.hnorm e.e_ty env).ty_node with - | Ttuple tys -> tys | _ -> assert false in - List.mapi (fun i ty -> e_proj e i ty) tys in - - let s = List.map2 (fun pv e -> i_asgn (LvVar (pv, e.e_ty), e)) lv e in - - ([], s) - in - let kinds = [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] in if not (EcLowPhlGoal.is_program_logic concl kinds) then @@ -566,88 +250,36 @@ let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) = let _, s = EcLowPhlGoal.tc1_get_stmt side tc in let pos = EcLowPhlGoal.tc1_process_codepos tc (side, pos) in - let goals, s = EcMatching.Zipper.map env pos change s in - let concl = EcLowPhlGoal.hl_set_stmt side concl s in + let zpr, (at, _) = Zpr.zipper_of_cpos_r env pos s in - FApi.xmutate1 tc `ProcCase (goals @ [concl]) + let i = + match zpr.Zpr.z_tail with + | i :: _ -> i + | [] -> raise Position.InvalidCPos in -(* -------------------------------------------------------------------- *) -let transform_if pf (env : EcEnv.env) (e : expr) (s1 : stmt) (s2 : stmt) = - let mod1 = s_write env s1 in - let mod2 = s_write env s2 in - let modv, modg = PV.elements (PV.union mod1 mod2) in + if not (is_asgn i) then + tc_error !!tc "the code position should target an assignment"; - if not (List.is_empty modg) then - tc_error pf "the branches modify global variables"; + let lv, e = destr_asgn i in - if List.is_empty modv then [] else - - let upd (m : (expr, unit) Mpv.t) (x : prog_var) (e : expr) = - Mpv.add env x e (Mpv.remove env x m) - in - - let init = - List.fold_left - (fun m (x, ty) -> Mpv.add env x (e_var x ty) m) - Mpv.empty modv - in - - let transform_v m (x, ty) = - let x' = EcIdent.create (symbol_of_pv x) in - upd m x (e_local x' ty), (x', ty) in - - let transform_lv m lv = + let pvl = match lv with - | LvVar (x, ty) -> - let m, (x', ty) = transform_v m (x, ty) in - m, LSymbol (x', ty) - | LvTuple xs -> - let m, xs' = List.map_fold transform_v m xs in - m, LTuple xs' in - - let transform_i m i = - let lv, e = destr_asgn i in - let e = Mpv.esubst env m e in - let m, lp = transform_lv m lv in - m, (lp, e) in + | LvVar _ -> PV.empty + | LvTuple lvs -> + let lvs = List.tl (List.rev lvs) in + let lvs = Option.get (lv_of_list lvs) in + EcPV.lp_write env lvs in - let transform_s (s : stmt) = - List.map_fold transform_i init s.s_node in - - let m1, bd1 = transform_s s1 in - let m2, bd2 = transform_s s2 in - - let es = - let e_if (x, ty) = - let ex = e_var x ty in - e_if e (Mpv.esubst env m1 ex) (Mpv.esubst env m2 ex) in - e_tuple (List.map e_if modv) in - - let add_binding bd es = - List.fold_right (fun (lp, e) es -> e_let lp e es) bd es in - - let es = add_binding bd1 (add_binding bd2 es) in - [i_asgn (oget (lv_of_list modv), es)] + if not (EcPV.PV.indep env pvl (EcPV.e_read env e)) then + assert false; -(* -------------------------------------------------------------------- *) -let transform_if_stmt env (pf, _) me i = - match i.i_node with - | Sif (e, s1, s2) -> - if not (List.for_all is_asgn s1.s_node) then - tc_error pf "the then branch contains intruction that are not assignments"; - if not (List.for_all is_asgn s2.s_node) then - tc_error pf "the else branch contains intruction that are not assignments"; - (me, transform_if pf env e s1 s2) - | _ -> - tc_error pf "the given position does not correspond to an if instruction" + t_transform side (EcTrAsgnCase.TrAsgnCase { trac_at = at }) tc (* -------------------------------------------------------------------- *) -let t_transform_if_r side cpos g = - let env = FApi.tc1_env g in - let tr = fun side -> `TransformIf (side, cpos) in - t_code_transform side cpos tr (t_fold (transform_if_stmt env)) g - -let t_transform_if = FApi.t_low2 "code-tx-transform_if" t_transform_if_r +let t_transform_if (side : oside) (cpos : Position.codepos) (tc : tcenv1) = + let _, s = tx_stmt side tc in + let at = resolve_cpos tc cpos s in + t_transform side (EcTrSimplifyIf.TrSimplifyIf { trsi_at = at }) tc (* -------------------------------------------------------------------- *) let t_transform_if_rec1 side g = diff --git a/src/phl/rules/bdhoare/ecBdHoareTransform.ml b/src/phl/rules/bdhoare/ecBdHoareTransform.ml index daa1763de..d6e1cdecc 100644 --- a/src/phl/rules/bdhoare/ecBdHoareTransform.ml +++ b/src/phl/rules/bdhoare/ecBdHoareTransform.ml @@ -38,7 +38,10 @@ let bdhoare_transform_subgoals let obligation = function | OPrefixPost { opp_prefix = hd; opp_cond = cond } -> let cond = { (ss_inv_rebind cond m) with m } in - f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd (POE.lift cond) in + f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd (POE.lift cond) + | OLossless ks -> + f_bdHoareS (snd bhs.bhs_m) + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in List.map obligation r.trr_obl @ [f_bdHoareS (snd r.trr_me) (bhs_pr bhs) r.trr_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs)] diff --git a/src/phl/rules/bdhoare/ecBdHoareTransform.mli b/src/phl/rules/bdhoare/ecBdHoareTransform.mli index c15c3b512..d3755035a 100644 --- a/src/phl/rules/bdhoare/ecBdHoareTransform.mli +++ b/src/phl/rules/bdhoare/ecBdHoareTransform.mli @@ -20,7 +20,9 @@ type bdhoare_transform = { where [c'] may live in an extended memory (fresh program variables), and the entry is given the program variables read by [Q]. Each obligation becomes a premise (first, in order): - - [OPrefixPost (hd, cond)]: hoare [hd : P ==> cond]. + - [OPrefixPost (hd, cond)]: hoare [hd : P ==> cond]; + - [OLossless ks]: phoare [ks : true ==> true] = 1 + (in the memory of [c]). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [RBdHoareTransform { btr_tr = t }]. Checker: "bdhoare-transform" diff --git a/src/phl/rules/ecPlTransform.ml b/src/phl/rules/ecPlTransform.ml index 730b750da..6b869555e 100644 --- a/src/phl/rules/ecPlTransform.ml +++ b/src/phl/rules/ecPlTransform.ml @@ -11,6 +11,7 @@ type transform = .. type obligation = | OPrefixPost of prefix_post + | OLossless of stmt and prefix_post = { opp_prefix : stmt; diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index f3def0378..a724bb3b7 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -34,7 +34,9 @@ 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) and [EcTrInline] (inlining procedure calls). Entries live + nested block), [EcTrInline] (inlining procedure calls), [EcTrKill], + [EcTrAlias], [EcTrSet], [EcTrSetMatch], [EcTrCFold], [EcTrAsgnCase] + and [EcTrSimplifyIf] (the code transformations). 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]). *) @@ -48,10 +50,14 @@ type transform = .. extended one of [c']). *) type obligation = | OPrefixPost of prefix_post + | OLossless of stmt (* [OPrefixPost { opp_prefix = hd; opp_cond = cond }]: every terminating run of [hd] (a prefix of [c]) from the precondition ends in a state - satisfying [cond]. *) + satisfying [cond]. + + [OLossless ks]: the statement [ks] (a fragment of [c], over its memory) + terminates with probability 1 from every state. *) and prefix_post = { opp_prefix : stmt; (* the prefix [hd] *) opp_cond : ss_inv; (* [cond] *) diff --git a/src/phl/rules/ehoare/ecEHoareTransform.ml b/src/phl/rules/ehoare/ecEHoareTransform.ml index a1974e9b6..390e6ba59 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.ml +++ b/src/phl/rules/ehoare/ecEHoareTransform.ml @@ -45,7 +45,10 @@ let ehoare_transform_subgoals let obligation = function | OPrefixPost { opp_prefix = hd; opp_cond = cond } -> let cond = { (ss_inv_rebind cond m) with m } in - f_hoareS (snd hs.ehs_m) (pre ()) hd (POE.lift cond) in + f_hoareS (snd hs.ehs_m) (pre ()) hd (POE.lift cond) + | OLossless ks -> + f_bdHoareS (snd hs.ehs_m) + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in List.map obligation r.trr_obl @ [f_eHoareS (snd r.trr_me) (ehs_pr hs) r.trr_s (ehs_po hs)] diff --git a/src/phl/rules/ehoare/ecEHoareTransform.mli b/src/phl/rules/ehoare/ecEHoareTransform.mli index a249d8409..2f07babce 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.mli +++ b/src/phl/rules/ehoare/ecEHoareTransform.mli @@ -21,7 +21,9 @@ type ehoare_transform = { obligation becomes a premise (first, in order): - [OPrefixPost (hd, cond)]: hoare [hd : P_bool ==> cond] where [P] is [P_bool `|` f] (otherwise fails with "the pre should - have the form \"_ `|` _\""). + have the form \"_ `|` _\""); + - [OLossless ks]: phoare [ks : true ==> true] = 1 + (in the memory of [c]). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [REHoareTransform { ehtr_tr = t }]. Checker: "ehoare-transform" diff --git a/src/phl/rules/equiv/ecEquivTransform.ml b/src/phl/rules/equiv/ecEquivTransform.ml index b23c0db71..bcb5b6c05 100644 --- a/src/phl/rules/equiv/ecEquivTransform.ml +++ b/src/phl/rules/equiv/ecEquivTransform.ml @@ -56,7 +56,10 @@ let equiv_transform_subgoals let mhs = EcIdent.create "&hr" in let pr = ss_inv_rebind pr mhs in let po = ss_inv_rebind po mhs in - f_hoareS (snd me) pr hd (POE.lift po)) (es_pr es) cond) in + f_hoareS (snd me) pr hd (POE.lift po)) (es_pr es) cond) + | OLossless ks -> + f_bdHoareS (snd me) + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in let concl = match side with | `Left -> diff --git a/src/phl/rules/equiv/ecEquivTransform.mli b/src/phl/rules/equiv/ecEquivTransform.mli index ecf9f8f33..04e485869 100644 --- a/src/phl/rules/equiv/ecEquivTransform.mli +++ b/src/phl/rules/equiv/ecEquivTransform.mli @@ -26,7 +26,9 @@ type equiv_transform = { - [OPrefixPost (hd, cond)]: forall &2, hoare [hd : P ==> cond] ([P] read as an assertion on [&1], the other memory [&2] being - universally quantified). + universally quantified); + - [OLossless ks]: phoare [ks : true ==> true] = 1 + (in the memory [&1] of [c], the other memory not involved). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [REquivTransform { etr_side; etr_tr = t }]. Checker: diff --git a/src/phl/rules/hoare/ecHoareTransform.ml b/src/phl/rules/hoare/ecHoareTransform.ml index 2e11e6608..8d8f6e091 100644 --- a/src/phl/rules/hoare/ecHoareTransform.ml +++ b/src/phl/rules/hoare/ecHoareTransform.ml @@ -39,7 +39,10 @@ let hoare_transform_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_trans let obligation = function | OPrefixPost { opp_prefix = hd; opp_cond = cond } -> let cond = { (ss_inv_rebind cond m) with m } in - f_hoareS (snd hs.hs_m) (hs_pr hs) hd (update_hs_ss cond po) in + f_hoareS (snd hs.hs_m) (hs_pr hs) hd (update_hs_ss cond po) + | OLossless ks -> + f_bdHoareS (snd hs.hs_m) + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in List.map obligation r.trr_obl @ [f_hoareS (snd r.trr_me) (hs_pr hs) r.trr_s po] diff --git a/src/phl/rules/hoare/ecHoareTransform.mli b/src/phl/rules/hoare/ecHoareTransform.mli index 6c0281284..876a7a4af 100644 --- a/src/phl/rules/hoare/ecHoareTransform.mli +++ b/src/phl/rules/hoare/ecHoareTransform.mli @@ -20,7 +20,9 @@ type hoare_transform = { and the entry is given the program variables read by [Q | E]. Each obligation becomes a premise (first, in order): - [OPrefixPost (hd, cond)]: hoare [hd : P ==> cond | E] - (the exceptional postconditions [E] of the goal are kept). + (the exceptional postconditions [E] of the goal are kept); + - [OLossless ks]: phoare [ks : true ==> true] = 1 + (in the memory of [c]). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [RHoareTransform { htr_tr = t }]. Checker: "hoare-transform" (it diff --git a/src/phl/rules/transforms/ecTrAlias.ml b/src/phl/rules/transforms/ecTrAlias.ml new file mode 100644 index 000000000..e8010c9bf --- /dev/null +++ b/src/phl/rules/transforms/ecTrAlias.ml @@ -0,0 +1,72 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcTypes +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [alias] transformation, resolved: the position is a + normalized (possibly nested) code position. *) +type tr_alias = { + tral_at : EcMatching.Position.nm_codepos; + tral_name : symbol; +} + +type EcPlTransform.transform += TrAlias of tr_alias + +(* -------------------------------------------------------------------- *) +(* Store the value computed by the instruction at the position in a fresh + program variable, then assign it to the original left-value. *) +let alias (p : tr_alias) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + + let zpr = + try Zpr.zipper_of_nm_cpos p.tral_at s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let i, tl = + match zpr.Zpr.z_tail with + | i :: tl -> (i, tl) + | [] -> raise (InvalidTransform "invalid code position") in + + let dopv ty = + let id = { ov_name = Some p.tral_name; ov_type = ty; } in + let (me, id) = EcMemory.bind_fresh id ctxt.trc_me in + (* oget cannot fail — Some in, Some out *) + let pv = pv_loc (EcUtils.oget id.ov_name) in + me, pv in + + let me, is = + match i.i_node with + | Sasgn (lv, e) -> + let ty = e.e_ty in + let (me, pv) = dopv ty in + (me, [i_asgn (LvVar (pv, ty), e); i_asgn (lv, e_var pv ty)]) + + | Srnd (lv, e) -> + let ty = EcFol.proj_distr_ty env e.e_ty in + let (me, pv) = dopv ty in + (me, [i_rnd (LvVar (pv, ty), e); i_asgn (lv, e_var pv ty)]) + + | Scall (Some lv, f, args) -> + let ty = (EcEnv.Fun.by_xpath f env).f_sig.fs_ret in + let (me, pv) = dopv ty in + (me, [i_call (Some (LvVar (pv, ty)), f, args); i_asgn (lv, e_var pv ty)]) + + | _ -> + raise (InvalidTransform + "cannot create an alias for that kind of instruction") + in + + { trr_me = me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = is @ tl; }; + trr_obl = []; } + +let () = + register (function + | TrAlias p -> Some (alias p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrAlias.mli b/src/phl/rules/transforms/ecTrAlias.mli new file mode 100644 index 000000000..94dddce25 --- /dev/null +++ b/src/phl/rules/transforms/ecTrAlias.mli @@ -0,0 +1,26 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_alias = { + tral_at : nm_codepos; (* position of the instruction (resolved, + possibly nested) *) + tral_name : symbol; (* name of the alias *) +} + +(* [TrAlias { tral_at = p; tral_name = x }] — names the value computed by + the instruction at position [p] (an assignment, a sampling or a call + with a left-value), through a fresh program variable [x'] (named after + [x], added to the memory): + + c = C[lv <- e] ~~> c' = C[x' <- e; lv <- x'] + c = C[lv <$ d] ~~> c' = C[x' <$ d; lv <- x'] + c = C[lv <@ f(args)] ~~> c' = C[x' <@ f(args); lv <- x'] + + No obligation. Fails with "invalid code position" when [p] is not the + position of an instruction of [c], and "cannot create an alias for that + kind of instruction" otherwise. *) +type EcPlTransform.transform += TrAlias of tr_alias diff --git a/src/phl/rules/transforms/ecTrAsgnCase.ml b/src/phl/rules/transforms/ecTrAsgnCase.ml new file mode 100644 index 000000000..2a06e6d35 --- /dev/null +++ b/src/phl/rules/transforms/ecTrAsgnCase.ml @@ -0,0 +1,79 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcTypes +open EcModules +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [asgn-case] transformation, resolved: the position is + a normalized (possibly nested) code position. *) +type tr_asgn_case = { + trac_at : EcMatching.Position.nm_codepos; +} + +type EcPlTransform.transform += TrAsgnCase of tr_asgn_case + +(* -------------------------------------------------------------------- *) +(* Split the assignment into one assignment per assigned variable, in + order: the variables assigned before the last one must not be read by + the assigned expression. *) +let asgn_case (p : tr_asgn_case) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + + let zpr = + try Zpr.zipper_of_nm_cpos p.trac_at s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let i, tl = + match zpr.Zpr.z_tail with + | i :: tl -> (i, tl) + | [] -> raise (InvalidTransform "invalid code position") in + + if not (is_asgn i) then + raise (InvalidTransform "the code position should target an assignment"); + + let lv, e = destr_asgn i in + + let pvl = + match lv with + | LvVar _ -> PV.empty + | LvTuple lvs -> + let lvs = List.tl (List.rev lvs) in + let lvs = Option.get (lv_of_list lvs) in + EcPV.lp_write env lvs in + + let pve = EcPV.e_read env e in + let lv = lv_to_list lv in + + if not (EcPV.PV.indep env pvl pve) then + raise (InvalidTransform + "the assigned variables are read by the assigned expression"); + + let e = + match lv, e.e_node with + | [_], _ -> [e] + | _ , Etuple es -> es + | _ ,_ -> + let tys = + match (EcEnv.Ty.hnorm e.e_ty env).ty_node with + | Ttuple tys -> tys + | _ -> raise (InvalidTransform "the assigned expression is not a tuple") in + List.mapi (fun i ty -> e_proj e i ty) tys in + + if List.length lv <> List.length e then + raise (InvalidTransform "the assigned expression is not a tuple"); + + let is = List.map2 (fun pv e -> i_asgn (LvVar (pv, e.e_ty), e)) lv e in + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = is @ tl; }; + trr_obl = []; } + +let () = + register (function + | TrAsgnCase p -> Some (asgn_case p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrAsgnCase.mli b/src/phl/rules/transforms/ecTrAsgnCase.mli new file mode 100644 index 000000000..b3d159313 --- /dev/null +++ b/src/phl/rules/transforms/ecTrAsgnCase.mli @@ -0,0 +1,25 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_asgn_case = { + trac_at : nm_codepos; (* position of the assignment (resolved, + possibly nested) *) +} + +(* [TrAsgnCase { trac_at = p }] — splits the (tuple) assignment at + position [p] into one assignment per variable: + + c = C[(x_1, ..., x_n) <- e] ~~> c' = C[x_1 <- e_1; ...; x_n <- e_n] + + where [e_i] is the [i]-th component of [e] when [e] is a syntactic + tuple, its [i]-th projection otherwise (the assignment is unchanged + when it assigns a single variable). Side condition: [x_1 ... x_(n-1)] + are not read by [e]. No obligation. Same memory. Fails with "invalid + code position" when [p] is not the position of an instruction of [c], + "the code position should target an assignment" when it is not an + assignment, and "the assigned variables are read by the assigned + expression" when the side condition does not hold. *) +type EcPlTransform.transform += TrAsgnCase of tr_asgn_case diff --git a/src/phl/rules/transforms/ecTrCFold.ml b/src/phl/rules/transforms/ecTrCFold.ml new file mode 100644 index 000000000..96587a418 --- /dev/null +++ b/src/phl/rules/transforms/ecTrCFold.ml @@ -0,0 +1,258 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcModules +open EcFol +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [cfold] transformation, resolved: the position is a + normalized (possibly nested) code position. *) +type tr_cfold = { + trcf_at : EcMatching.Position.nm_codepos; + trcf_len : int option; + trcf_eager : bool; +} + +type EcPlTransform.transform += TrCFold of tr_cfold + +(* -------------------------------------------------------------------- *) +let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidTransform msg)) fmt + +(* -------------------------------------------------------------------- *) +(* Constant folding (see the [.mli]). The scan works on a block starting + at an assignment to local variables. + + It initializes: + - propagate: a substitution mapping the assigned variables to their values + - preserve : for each propagated variable, the variables that must keep their + current value for that propagated expression to remain valid + + It then scans subsequent instructions from left to right. + + For assignments: + - if the assigned variable is preserved, stop in non-eager mode; in eager + mode, substitute in the right-hand side and promote that variable to the + propagated substitution + - if the assigned variable is already propagated, update its propagated value + and recompute its preservation set + - otherwise, substitute propagated values in the right-hand side and keep the + assignment + + For calls, loops, conditionals, matches, and random samplings: + - continue only if none of the currently propagated or preserved variables is + written by the instruction; in that case, substitute propagated values in + the instruction + - otherwise, stop + + For abstract instructions without calls: + - continue only if they neither read nor write propagated or preserved + variables + - otherwise, stop + + When the scan stops, the remaining propagated substitution is materialized as + assignments appended after the transformed prefix. + + The values are simplified without delta (the local definitions of the + goal are not unfolded): the entry simplifies under its environment only. +*) +let cfold (p : tr_cfold) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + let me = ctxt.trc_me in + let eager = p.trcf_eager in + let hyps = EcEnv.LDecl.init env [] in + + let zpr = + try Zpr.zipper_of_nm_cpos p.trcf_at s + with EcMatching.Position.InvalidCPos -> invalid "invalid code position" in + + let e_simplify (e : expr) = + let e = form_of_expr ~m:(fst me) e in + let e = EcReduction.simplify EcReduction.nodelta hyps e in + expr_of_ss_inv { m = fst me; inv = e } in + + let i_simplify (i : instr) = + i_map_expr e_simplify i in + + (* + Process one instruction under the current propagated substitution and + preservation map. + + - `Continue ((subst, preserve), is)` means that propagation may proceed, + with updated state and replacement instructions `is` + - `Interrupt` means that propagation stops before this instruction + + In eager mode, assigning to a preserved variable does not stop the scan: + the assigned expression is first substituted, then that variable is + promoted into the propagated substitution. + *) + let for_instruction (subst, preserve: (expr, unit) Mpv.t * (PV.t Mnpv.t)) (i : instr) = + let esubst subst e = + EcPV.Mpv.esubst env subst e |> e_simplify + in + let isubst subst i = + EcPV.Mpv.isubst env subst i |> i_simplify + in + let is_preserved preserve pv = + Mnpv.exists (fun _ preserve -> EcPV.PV.mem_pv env pv preserve) preserve + in + let is_propagated subst pv = + Mnpv.contains (Mpv.pvs subst) pv + in + let propagated_pvs subst = + (Mpv.pvs subst) |> Mnpv.bindings |> List.fst + in + (* Update preserve vars on assignment to given PV *) + (* Do not include any propagated vars, since these *) + (* are automatically preserved by construction *) + let update_preserved preserve subst pv e = + let rd = EcPV.e_read env e in + let rd = List.fold_left (fun rd pv -> + EcPV.PV.remove env pv rd + ) rd (propagated_pvs subst) + in + Mnpv.add pv rd preserve + in + let promote_preserved_to_propagated subst preserve pv (e:expr) = + let preserve = Mnpv.map (fun preserve -> + PV.remove env pv preserve + ) preserve + in + let subst = Mpv.add env pv e subst in + (subst, preserve) + in + + match i.i_node with + | Sasgn (lv, e) -> + let asgns = explode_assgn lv e in + let exception Abort in + begin try + let (subst, preserve), asgns = List.fold_left_map (fun (subst, preserve) ((pv, t), e) -> + (* 1. When hitting an assignment to a preserved var *) + if is_preserved preserve pv then + if eager (* 1.1 Promote to propagated on eager *) + then + let e = esubst subst e in + promote_preserved_to_propagated subst preserve pv e, None + else raise Abort (* 1.2 Fail on non-eager *) + else + (* 2. When not preserved and not propagated, do nothing *) + if not (is_propagated subst pv) then + (subst, preserve), Some ((pv, t), esubst subst e) + (* 3. When propagated, propagate *) + else + let e = esubst subst e in + let preserve = update_preserved preserve subst pv e in + let subst = Mpv.add env pv e subst in + (subst, preserve), None + ) (subst, preserve) asgns + in + let asgns = List.filter_map identity asgns in + `Continue ((subst, preserve), Option.to_list (i_asgn_of_pve asgns)) + with Abort -> `Interrupt + end + + | Srnd _ + | Scall _ + | Swhile _ + | Sif _ + | Smatch _ -> + let wr = EcPV.i_write env i in + let spvs = Mnpv.keys (Mpv.pvs subst) in + let ppvs = Mnpv.keys preserve in + if + let check = List.for_all (fun pv -> + not @@ EcPV.PV.mem_pv env pv wr) in + check spvs && check ppvs + then + `Continue ((subst, preserve), [isubst subst i]) + else + `Interrupt + + | Sraise _ -> `Interrupt + + | Sabstract id -> + let aus = EcEnv.AbsStmt.byid id env in + begin match aus with + | { aus_calls = []; aus_reads; aus_writes } -> + if List.for_all (fun (pv, _) -> + not ((is_propagated subst pv) || (is_preserved preserve pv)) + ) (aus_reads @ aus_writes) then + `Continue ((subst, preserve), [i]) + else + `Interrupt + | _ -> `Interrupt + end + in + + let body, epilog = + match p.trcf_len with + | None -> + (zpr.Zpr.z_tail, []) + | Some olen -> + if List.length zpr.Zpr.z_tail < olen+1 then + invalid "expecting at least %d instructions" olen; + List.takedrop (olen+1) zpr.Zpr.z_tail in + + let _lv, (subst, _preserve), body, rem = + match body with + | { i_node = Sasgn (lv, e) } :: is -> + let asgns = explode_assgn lv e in + let lv = List.fst asgns in + + if not (List.for_all (is_loc -| fst) lv) then + invalid "left-values must be made of local variables only"; + + (* Variables in the domain of substs + are variables to be propagated *) + let subst = + List.fold_left + (fun subst ((pv, _), e) -> Mpv.add env pv e subst) + Mpv.empty asgns in + + let preserve = + List.fold_left + (fun preserve ((pv, _), e) -> + Mnpv.add + pv + EcPV.(PV.remove env pv (e_read env e)) + preserve) + Mnpv.empty + asgns + in + + let (subst, preserve), is, rem = + List.fold_left_map_while for_instruction (subst, preserve) is in + + lv, (subst, preserve), List.flatten is, rem + + | _ -> + invalid "cannot find a left-value assignment at given position" + in + + let asgns = Mnpv.bindings (Mpv.pvs subst) in + + let lv, es = List.map (fun (pv, e) -> + (pv, e_ty e), e) asgns |> List.split + in + + let asgn = + lv_of_list lv + |> Option.map (fun lv -> i_asgn (lv, e_tuple es)) + |> Option.to_list in + + let zpr = + { zpr with Zpr.z_tail = body @ asgn @ rem @ epilog } in + + { trr_me = me; + trr_s = Zpr.zip zpr; + trr_obl = []; } + +let () = + register (function + | TrCFold p -> Some (cfold p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrCFold.mli b/src/phl/rules/transforms/ecTrCFold.mli new file mode 100644 index 000000000..751f3e5d9 --- /dev/null +++ b/src/phl/rules/transforms/ecTrCFold.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_cfold = { + trcf_at : nm_codepos; (* position of the assignment (resolved, + possibly nested) *) + trcf_len : int option; (* number n of instructions to scan after it; + [None]: up to the end of its block *) + trcf_eager : bool; (* eager propagation *) +} + +(* [TrCFold { trcf_at = p; trcf_len = n; trcf_eager = eager }] — + constant folding: propagates the assignment [xs <- es] to local + variables at position [p] into the (at most [n]) instructions that + follow it in its block, as long as this is valid, and materializes the + propagated values afterwards: + + c = C[xs <- es; c1; c2; c3] ~~> c' = C[c1'; ys <- fs; c2; c3] + + where [c1] is the longest prefix of the scanned instructions [c1; c2] + through which the propagation proceeds, [c1'] is [c1] with the + propagated values substituted (and simplified, without delta), [ys] the + variables still propagated at the end of [c1] and [fs] their values, and + [c3] the instructions not scanned. An assignment to a variable read by a + propagated value stops the propagation, unless [eager], in which case + that variable is propagated too; calls, loops, conditionals, matches and + samplings stop it when they write a propagated variable or a variable + read by a propagated value; abstract statements when they read or write + one of them, or make calls; [raise] always stops it. + + No obligation. Same memory. Fails with "invalid code position" when [p] + is not a position of [c], "expecting at least n instructions" when the + block has fewer than [n + 1] instructions from [p], "cannot find a + left-value assignment at given position" when the instruction at [p] is + not an assignment, and "left-values must be made of local variables + only" when it assigns a global. *) +type EcPlTransform.transform += TrCFold of tr_cfold diff --git a/src/phl/rules/transforms/ecTrKill.ml b/src/phl/rules/transforms/ecTrKill.ml new file mode 100644 index 000000000..71fdf8aee --- /dev/null +++ b/src/phl/rules/transforms/ecTrKill.ml @@ -0,0 +1,90 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcModules +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [kill] transformation, resolved: the position is a + normalized (possibly nested) code position. *) +type tr_kill = { + trk_at : EcMatching.Position.nm_codepos; + trk_len : int option; +} + +type EcPlTransform.transform += TrKill of tr_kill + +(* -------------------------------------------------------------------- *) +let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidTransform msg)) fmt + +(* -------------------------------------------------------------------- *) +(* Remove the killed instructions [ks], provided that what they write is + read neither by the code that may run after them nor by the + postcondition; [ks] must be lossless. *) +let kill (p : tr_kill) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + + let zpr = + try Zpr.zipper_of_nm_cpos p.trk_at s + with EcMatching.Position.InvalidCPos -> invalid "invalid code position" in + + let (ks, tl) = + match p.trk_len with + | None -> (zpr.Zpr.z_tail, []) + | Some len -> + if List.length zpr.Zpr.z_tail < len then + invalid "cannot find %d consecutive instructions at given position" len; + List.takedrop len zpr.Zpr.z_tail + in + + let ks_wr = is_write env ks in + + let pp_of_name = + let ppe = EcPrinting.PPEnv.ofenv env in + fun fmt x -> + match x with + | `Global p -> EcPrinting.pp_topmod ppe fmt p + | `PV p -> EcPrinting.pp_pv ppe fmt p + in + + (* [ks] is replaced by [skip]. This is sound if [ks] is lossless + (obligation) and if the variables it writes ([ks_wr]) are read + neither by the postcondition nor by any code that may run after + [ks]: then both programs end in states that agree outside of + [ks_wr]. The code that may run after [ks] is, for each enclosing + block, the code that follows the block's cursor, and, for each + enclosing while loop, the loop guard and the whole loop body (with + [ks] removed): the next iterations run them again, including the + part of the body before [ks]. This is what + [EcPV.zpr_pv `Read `After] computes. *) + let af_rd = + zpr_pv `Read `After env PV.empty ((zpr.Zpr.z_head, tl), zpr.Zpr.z_path) in + + begin + match PV.pick (PV.interdep env ks_wr af_rd) with + | None -> () + | Some x -> + invalid + "code writes variables (%a) used by the code that may run after it" + pp_of_name x + end; + + begin + match PV.pick (PV.interdep env ks_wr (Lazy.force ctxt.trc_post)) with + | None -> () + | Some x -> + invalid + "code writes variables (%a) used by the post-condition" + pp_of_name x + end; + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = tl; }; + trr_obl = [OLossless (stmt ks)]; } + +let () = + register (function + | TrKill p -> Some (kill p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrKill.mli b/src/phl/rules/transforms/ecTrKill.mli new file mode 100644 index 000000000..783912361 --- /dev/null +++ b/src/phl/rules/transforms/ecTrKill.mli @@ -0,0 +1,31 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_kill = { + trk_at : nm_codepos; (* position of the first killed instruction + (resolved, possibly nested) *) + trk_len : int option; (* number n of killed instructions; [None]: up + to the end of their block *) +} + +(* [TrKill { trk_at = p; trk_len = n }] — removes the [n] instructions + [ks] at position [p] (in the block of [p], possibly nested): + + c = C[ks; tl] ~~> c' = C[tl] + + provided that no variable written by [ks] is read by the code that may + run after it ([tl], the instructions following each enclosing + instruction, and, for each enclosing while loop, its guard and its + whole body, as the next iterations run them again: [EcPV.zpr_pv `Read + `After]), nor by the postcondition (the context's [trc_post], for + hoare including the exceptional postconditions). One obligation: + [OLossless ks], in the memory of [c]. Same memory. Fails with "invalid + code position" when [p] is not a position of [c], "cannot find n + consecutive instructions at given position" when the block has fewer + than [n] instructions from [p], and "code writes variables (x) used by + the code that may run after it / the post-condition" when the + independence condition does not hold. *) +type EcPlTransform.transform += TrKill of tr_kill diff --git a/src/phl/rules/transforms/ecTrSet.ml b/src/phl/rules/transforms/ecTrSet.ml new file mode 100644 index 000000000..9d40bc69f --- /dev/null +++ b/src/phl/rules/transforms/ecTrSet.ml @@ -0,0 +1,44 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcTypes +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [set] transformation, resolved: the position is a + normalized (possibly nested) code position, the value a typed + expression. *) +type tr_set = { + trs_at : EcMatching.Position.nm_codepos; + trs_name : symbol; + trs_e : expr; +} + +type EcPlTransform.transform += TrSet of tr_set + +(* -------------------------------------------------------------------- *) +(* Insert the assignment of the value to a fresh program variable. *) +let set (p : tr_set) (ctxt : tr_ctxt) (s : stmt) = + let zpr = + try Zpr.zipper_of_nm_cpos p.trs_at s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let e = p.trs_e in + let v = { ov_name = Some p.trs_name; ov_type = e.e_ty } in + let (me, id) = EcMemory.bind_fresh v ctxt.trc_me in + (* oget cannot fail — Some in, Some out *) + let pv = pv_loc (EcUtils.oget id.ov_name) in + let i = i_asgn (LvVar (pv, e.e_ty), e) in + + { trr_me = me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = i :: zpr.Zpr.z_tail; }; + trr_obl = []; } + +let () = + register (function + | TrSet p -> Some (set p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrSet.mli b/src/phl/rules/transforms/ecTrSet.mli new file mode 100644 index 000000000..4e31886fb --- /dev/null +++ b/src/phl/rules/transforms/ecTrSet.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcTypes +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_set = { + trs_at : nm_codepos; (* insertion position (resolved, possibly + nested; may be the end of its block) *) + trs_name : symbol; (* name of the new variable *) + trs_e : expr; (* its value, typed in the memory of [c] *) +} + +(* [TrSet { trs_at = p; trs_name = x; trs_e = e }] — inserts, at position + [p], the assignment of [e] to a fresh program variable [x'] (named + after [x], added to the memory): + + c = C[tl] ~~> c' = C[x' <- e; tl] + + No obligation. Fails with "invalid code position" when [p] is not a + position of [c]. *) +type EcPlTransform.transform += TrSet of tr_set diff --git a/src/phl/rules/transforms/ecTrSetMatch.ml b/src/phl/rules/transforms/ecTrSetMatch.ml new file mode 100644 index 000000000..f58453e07 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSetMatch.ml @@ -0,0 +1,83 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcSymbols +open EcAst +open EcTypes +open EcModules +open EcFol +open EcMatching +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [set-match] transformation, resolved: the position is + a normalized (possibly nested) code position, the pattern has been + matched and its occurrences selected. *) +type tr_set_match = { + trsm_at : Position.nm_codepos; + trsm_name : symbol; + trsm_sub : ss_inv; + trsm_occ : ptnpos; +} + +type EcPlTransform.transform += TrSetMatch of tr_set_match + +(* -------------------------------------------------------------------- *) +(* Assign the subterm to a fresh program variable just before the + instruction, and replace its selected occurrences by that variable. *) +let set_match (p : tr_set_match) (ctxt : tr_ctxt) (s : stmt) = + let zpr = + try Zpr.zipper_of_nm_cpos p.trsm_at s + with Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let i, is = + match zpr.Zpr.z_tail with + | i :: is -> (i, is) + | [] -> raise (InvalidTransform "invalid code position") in + + let e, mk = + let e, kind, mk = + get_expression_of_instruction i |> ofdfl (fun () -> + raise (InvalidTransform + "targetted instruction should contain an expression")) in + + match kind with + | `Sasgn | `Srnd | `Sif | `Smatch -> (e, mk) + | `Swhile -> raise (InvalidTransform "while loops not supported") + in + + let m = fst ctxt.trc_me in + let hyps = EcEnv.LDecl.init ctxt.trc_env [] in + let e = ss_inv_of_expr m e in + let subf = EcSubst.ss_inv_rebind p.trsm_sub m in + + let v = { ov_name = Some p.trsm_name; ov_type = subf.inv.f_ty } in + let (me, id) = EcMemory.bind_fresh v ctxt.trc_me in + let pv = pv_loc (oget id.ov_name) in + + let occurrence pv t = + if not (EcReduction.is_alpha_eq hyps subf.inv t) then + raise (InvalidTransform "cannot find an occurrence of the pattern"); + pv in + + let e = + try + map_ss_inv2 + (fun pv -> FPosition.map p.trsm_occ (occurrence pv)) + (f_pvar pv subf.inv.f_ty m) e + with InvalidPosition -> + raise (InvalidTransform "cannot find an occurrence of the pattern") in + + let i1 = i_asgn (LvVar (pv, subf.inv.f_ty), expr_of_ss_inv subf) in + let i2 = mk (expr_of_ss_inv e) in + + { trr_me = me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = i1 :: i2 :: is; }; + trr_obl = []; } + +let () = + register (function + | TrSetMatch p -> Some (set_match p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrSetMatch.mli b/src/phl/rules/transforms/ecTrSetMatch.mli new file mode 100644 index 000000000..422b65cb3 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSetMatch.mli @@ -0,0 +1,34 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcMatching +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_set_match = { + trsm_at : nm_codepos; (* position of the instruction (resolved, + possibly nested) *) + trsm_name : symbol; (* name of the new variable *) + trsm_sub : ss_inv; (* the named subterm [t] (read in the memory + of [c]) *) + trsm_occ : ptnpos; (* its occurrences in the expression of the + instruction *) +} + +(* [TrSetMatch { trsm_at = p; trsm_name = x; trsm_sub = t; trsm_occ = o }] + — names the subterm [t] of the expression [e] of the instruction [i] at + position [p] (an assignment, a sampling, a conditional or a match), + through a fresh program variable [x'] (named after [x], added to the + memory): + + c = C[i(e)] ~~> c' = C[x' <- t; i(e[o := x'])] + + where every occurrence selected by [o] in [e] must be alpha-equivalent + to [t]. No obligation. Fails with "invalid code position" when [p] is + not the position of an instruction of [c], "targetted instruction + should contain an expression" or "while loops not supported" when [i] + is not of the expected kind, and "cannot find an occurrence of the + pattern" when [o] does not select occurrences of [t] in [e]. *) +type EcPlTransform.transform += TrSetMatch of tr_set_match diff --git a/src/phl/rules/transforms/ecTrSimplifyIf.ml b/src/phl/rules/transforms/ecTrSimplifyIf.ml new file mode 100644 index 000000000..e0de36b4b --- /dev/null +++ b/src/phl/rules/transforms/ecTrSimplifyIf.ml @@ -0,0 +1,116 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcModules +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [simplify-if] transformation, resolved: the position + is a normalized (possibly nested) code position. *) +type tr_simplify_if = { + trsi_at : EcMatching.Position.nm_codepos; +} + +type EcPlTransform.transform += TrSimplifyIf of tr_simplify_if + +(* -------------------------------------------------------------------- *) +(* The single assignment computing the final values of the variables + written by the branches [s1] / [s2] (assignments only) of + [if e then s1 else s2]; no instruction when they write nothing. *) +let simplify_if (env : EcEnv.env) (e : expr) (s1 : stmt) (s2 : stmt) = + let mod1 = s_write env s1 in + let mod2 = s_write env s2 in + let modv, modg = PV.elements (PV.union mod1 mod2) in + + if not (List.is_empty modg) then + raise (InvalidTransform "the branches modify global variables"); + + if List.is_empty modv then [] else + + let upd (m : (expr, unit) Mpv.t) (x : prog_var) (e : expr) = + Mpv.add env x e (Mpv.remove env x m) + in + + let init = + List.fold_left + (fun m (x, ty) -> Mpv.add env x (e_var x ty) m) + Mpv.empty modv + in + + let transform_v m (x, ty) = + let x' = EcIdent.create (symbol_of_pv x) in + upd m x (e_local x' ty), (x', ty) in + + let transform_lv m lv = + match lv with + | LvVar (x, ty) -> + let m, (x', ty) = transform_v m (x, ty) in + m, LSymbol (x', ty) + | LvTuple xs -> + let m, xs' = List.map_fold transform_v m xs in + m, LTuple xs' in + + let transform_i m i = + let lv, e = destr_asgn i in + let e = Mpv.esubst env m e in + let m, lp = transform_lv m lv in + m, (lp, e) in + + let transform_s (s : stmt) = + List.map_fold transform_i init s.s_node in + + let m1, bd1 = transform_s s1 in + let m2, bd2 = transform_s s2 in + + let es = + let e_if (x, ty) = + let ex = e_var x ty in + e_if e (Mpv.esubst env m1 ex) (Mpv.esubst env m2 ex) in + e_tuple (List.map e_if modv) in + + let add_binding bd es = + List.fold_right (fun (lp, e) es -> e_let lp e es) bd es in + + let es = add_binding bd1 (add_binding bd2 es) in + [i_asgn (oget (lv_of_list modv), es)] + +(* -------------------------------------------------------------------- *) +(* Replace the conditional at the position by a single assignment. *) +let simplify_if_tr (p : tr_simplify_if) (ctxt : tr_ctxt) (s : stmt) = + let zpr = + try Zpr.zipper_of_nm_cpos p.trsi_at s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let i, tl = + match zpr.Zpr.z_tail with + | i :: tl -> (i, tl) + | [] -> raise (InvalidTransform "invalid code position") in + + let is = + match i.i_node with + | Sif (e, s1, s2) -> + if not (List.for_all is_asgn s1.s_node) then + raise (InvalidTransform + "the then branch contains intruction that are not assignments"); + if not (List.for_all is_asgn s2.s_node) then + raise (InvalidTransform + "the else branch contains intruction that are not assignments"); + simplify_if ctxt.trc_env e s1 s2 + | _ -> + raise (InvalidTransform + "the given position does not correspond to an if instruction") + in + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = is @ tl; }; + trr_obl = []; } + +let () = + register (function + | TrSimplifyIf p -> Some (simplify_if_tr p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrSimplifyIf.mli b/src/phl/rules/transforms/ecTrSimplifyIf.mli new file mode 100644 index 000000000..522ba3af8 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSimplifyIf.mli @@ -0,0 +1,26 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_simplify_if = { + trsi_at : nm_codepos; (* position of the conditional (resolved, + possibly nested) *) +} + +(* [TrSimplifyIf { trsi_at = p }] — turns the conditional at position [p], + whose branches are sequences of assignments, into a single assignment: + + c = C[if e then c1 else c2] ~~> c' = C[xs <- es] + + where [xs] are the (local) variables written by [c1] or [c2] and [es] + computes their final values: [c1] and [c2] are read as nested [let]s + (on fresh local binders) over [if e then xs1 else xs2], [xsi] being the + values of [xs] at the end of [ci]. When [xs] is empty, the conditional + is removed. No obligation. Same memory. Fails with "invalid code + position" when [p] is not the position of an instruction of [c], "the + given position does not correspond to an if instruction", "the then + (resp. else) branch contains intruction that are not assignments", and + "the branches modify global variables". *) +type EcPlTransform.transform += TrSimplifyIf of tr_simplify_if diff --git a/tests/codetx.ec b/tests/codetx.ec new file mode 100644 index 000000000..9dc54597b --- /dev/null +++ b/tests/codetx.ec @@ -0,0 +1,436 @@ +(* The code transformations as program transformations: kill, alias, set + (`alias p x = e`), set-match (`alias x := pat @ p`), cfold, the split of + a tuple assignment (`case <-`) and `simplify if`, in every logic (hoare, + ehoare, phoare, equiv on both sides), at top-level and nested + positions, and their error paths. Each tactic is a separate sentence, + so that the goals it leaves can be compared across builds. *) +require import AllCore Distr DBool Xreal. + +op d : int distr. +axiom d_ll : is_lossless d. + +type t = [A | B of int]. + +exception oops. + +module N = { + proc h(a : int) : int = { + return a + 1; + } +}. + +module M = { + var g : int + + (* straight-line code, a conditional and a match, a loop *) + proc f(a : int, b : bool, o : t) : int = { + var x, y, z : int; + var p : int * int; + x <- a; + y <- x + 1; + z <$ d; + if (b) { + z <- y + 1; + y <- z + y; + } else { + z <- 0; + } + match o with + | A => { x <- 2; } + | B v => { x <- v + y; z <- 3; } + end; + p <- (x, y); + (x, y) <- (y, x); + while (x < 10) { + x <- x + 1; + y <- y + x; + } + z <@ N.h(x); + return x + y; + } + + (* for kill: dead code, at top-level and nested *) + proc k(a : int, b : bool) : int = { + var x, y, z, w : int; + x <- a; + y <- x + 1; + z <- 2; + if (b) { + w <- 3; + z <- w; + } else { + w <- 4; + } + x <- x + 1; + return x; + } + + (* for kill: live code *) + proc k2(a : int, b : bool) : int = { + var x, w : int; + x <- a; + if (b) { + w <- 3; + } else { + w <- 4; + } + x <- x + w; + return x; + } + + (* for kill, with an exceptional postcondition *) + proc ke(a : int) : int = { + var x : int; + x <- a; + g <- 1; + if (x < 0) { raise oops; } + return x; + } + + (* for simplify if: two conditionals over assignments, a nested one *) + proc s(a : int, b : bool) : int = { + var x, y : int; + x <- a; + if (b) { x <- x + 1; y <- x; } else { y <- 2; } + if (x < y) { (x, y) <- (y, x); } + while (0 < x) { + if (b) { x <- x - 1; } else { x <- x - 2; } + } + if (b) { g <- 1; } + if (b) { x <$ d; } + if (!b) { x <- 0; } else { x <$ d; } + return x + y; + } + + (* for case <-: tuple assignments *) + proc c(a : int) : int = { + var x, y : int; + var p : int * int; + p <- (a, a + 1); + (x, y) <- p; + (x, y) <- (y, a); + if (0 < x) { (x, y) <- (y + 1, a); } + return x + y; + } +}. + +(* ==================================================================== *) +(* kill *) + +lemma hoare_kill : hoare [M.k : true ==> res = 0]. +proof. +proc. +kill 2. +by auto. +kill 3.1 ! *. +by auto. +kill 2 ! 2. +by auto. +admit. +qed. + +lemma ehoare_kill : ehoare [M.k : 1%xr ==> 1%xr]. +proof. +proc. +kill 3. +by auto. +kill 3?1. +by auto. +admit. +qed. + +lemma phoare_kill : phoare [M.k : true ==> res = 0] = 1%r. +proof. +proc. +kill 2 ! 2. +by auto. +kill 2.2. +by auto. +admit. +qed. + +lemma equiv_kill : equiv [M.k ~ M.k : ={a, b} ==> ={res}]. +proof. +proc. +kill {1} 2. +by auto. +kill {2} 4.1 ! 2. +by auto. +kill {2} 2. +by auto. +admit. +qed. + +(* The variables read by the exceptional postconditions count: [g] + cannot be killed when one of them reads it. (Accepted by the builds + that only look at the main postcondition.) *) +lemma hoare_kill_exn : hoare [M.ke : true ==> true | oops => true]. +proof. +proc. +kill 2. +by auto. +by auto. +qed. + +lemma hoare_kill_exn_rejected : hoare [M.ke : true ==> true | oops => M.g = 1]. +proof. +proc. +fail kill 2. +by auto. +qed. + +lemma kill_errors : hoare [M.k2 : true ==> res = 0]. +proof. +proc. +fail kill 1. (* written variable read by the current block *) +fail kill 2.1. (* written variable read by a parent block *) +fail kill 3. (* written variable read by the post-condition *) +fail kill 2 ! 3. (* not enough instructions *) +fail kill 10. (* invalid code position *) +fail kill 2?3. (* invalid code position, nested *) +fail kill {1} 2. (* side on a hoare goal *) +abort. + +lemma kill_errors_equiv : equiv [M.k2 ~ M.k2 : ={a, b} ==> ={res}]. +proof. +proc. +fail kill 2. (* no side on an equiv goal *) +fail kill {1} 1. (* written variable read by the current block *) +fail kill {2} 10. (* invalid code position *) +abort. + +(* ==================================================================== *) +(* alias (assignment, sampling, call) and set *) + +lemma hoare_alias : hoare [M.f : true ==> true]. +proof. +proc. +alias 9. +alias 4.1 with u. +alias 3 with r. +alias 1. +alias 7#B.1 w = y. +alias 6?1 t = 0. +alias 13 e = x + y. +admit. +qed. + +lemma ehoare_alias : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +alias 3. +alias 1 t = a. +admit. +qed. + +lemma phoare_alias : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +alias 1 with r. +alias 9.1. +alias 1 t = a. +admit. +qed. + +lemma equiv_alias : equiv [M.f ~ M.f : ={a, b, o} ==> true]. +proof. +proc. +alias {1} 3. +alias {2} 4.1 with u. +alias {2} 9 t = x + 1. +alias {1} 9 t = x + 1. +admit. +qed. + +lemma alias_errors : hoare [M.f : true ==> true]. +proof. +proc. +fail alias 4. (* not an assignment, sampling or call *) +fail alias 20. (* invalid code position *) +fail alias 4?2. (* invalid code position, nested *) +fail alias 20 t = x. (* invalid code position (set) *) +fail alias {1} 1. (* side on a hoare goal *) +abort. + +(* ==================================================================== *) +(* set-match *) + +lemma hoare_set_match : hoare [M.f : true ==> true]. +proof. +proc. +alias c := (x + _) @ 2. +alias e := (_ + 1) @ 5.1. +alias f := b @ 5. +alias h := (o) @ 7. +admit. +qed. + +lemma ehoare_set_match : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +alias c := (_ + 1) @ 2. +admit. +qed. + +lemma phoare_set_match : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +alias c := (x, y) @ 6. +admit. +qed. + +lemma equiv_set_match : equiv [M.f ~ M.f : ={a, b, o} ==> true]. +proof. +proc. +alias {1} c := (x + _) @ 2. +alias {2} c := (_ + y) @ 4.2. +admit. +qed. + +lemma set_match_errors : hoare [M.f : true ==> true]. +proof. +proc. +fail alias c := (x * _) @ 2. (* no occurrence *) +fail alias c := (_ < 10) @ 8. (* while loop *) +fail alias c := a @ 9. (* no expression *) +fail alias c := a @ 20. (* invalid code position *) +abort. + +(* ==================================================================== *) +(* cfold *) + +lemma hoare_cfold : hoare [M.f : true ==> true]. +proof. +proc. +cfold 1. +cfold 3.1 1. +admit. +qed. + +lemma hoare_cfold_eager : hoare [M.f : true ==> true]. +proof. +proc. +cfold* 1. +admit. +qed. + +lemma ehoare_cfold : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +cfold 1 1. +admit. +qed. + +lemma phoare_cfold : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +cfold 1. +admit. +qed. + +lemma equiv_cfold : equiv [M.f ~ M.f : ={a, b, o} ==> true]. +proof. +proc. +cfold {1} 1. +cfold* {2} 2. +admit. +qed. + +lemma cfold_errors : hoare [M.f : true ==> true]. +proof. +proc. +fail cfold 3. (* not an assignment *) +fail cfold 1 20. (* not enough instructions *) +fail cfold 20. (* invalid code position *) +abort. + +(* ==================================================================== *) +(* case <- (split of a tuple assignment) *) + +lemma hoare_asgn_case : hoare [M.c : true ==> true]. +proof. +proc. +case <- 2. +case <- 4. +case <- 6.1. +case <- 1. +admit. +qed. + +lemma ehoare_asgn_case : ehoare [M.c : 1%xr ==> 1%xr]. +proof. +proc. +case <- 3. +admit. +qed. + +lemma phoare_asgn_case : phoare [M.c : true ==> true] = 1%r. +proof. +proc. +case <- 4.1. +admit. +qed. + +lemma equiv_asgn_case : equiv [M.c ~ M.c : ={a} ==> true]. +proof. +proc. +case <- {1} 2. +case <- {2} 3. +admit. +qed. + +lemma asgn_case_errors : hoare [M.c : true ==> true]. +proof. +proc. +fail case <- 4. (* not an assignment *) +abort. + +(* ==================================================================== *) +(* simplify if *) + +lemma hoare_simplify_if : hoare [M.s : true ==> true]. +proof. +proc. +simplify if 2. +simplify if 4.1. +simplify if 5. +admit. +qed. + +lemma hoare_simplify_if_all : hoare [M.s : true ==> true]. +proof. +proc. +simplify if. +admit. +qed. + +lemma ehoare_simplify_if : ehoare [M.s : 1%xr ==> 1%xr]. +proof. +proc. +simplify if 3. +admit. +qed. + +lemma phoare_simplify_if : phoare [M.s : true ==> true] = 1%r. +proof. +proc. +simplify if. +admit. +qed. + +lemma equiv_simplify_if : equiv [M.s ~ M.s : ={a, b} ==> true]. +proof. +proc. +simplify if {1} 2. +simplify if {2}. +admit. +qed. + +lemma simplify_if_errors : hoare [M.s : true ==> true]. +proof. +proc. +fail simplify if 1. (* not a conditional *) +fail simplify if 6. (* then branch: not only assignments *) +fail simplify if 7. (* else branch: not only assignments *) +fail simplify if 20. (* invalid code position *) +abort.