From ef8dd1cb889b85d761d4749fe4df7c3e44f1c27c Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 7 Oct 2026 13:56:23 +0200 Subject: [PATCH] refactor(pl): looptx as program transformations PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the loop transformations (`fission`, `fusion`, `unroll`, `splitwhile`) onto the transformation rule of each logic: - rules/transforms/ecTrFission.ml, ecTrFusion.ml, ecTrUnroll.ml, ecTrSplitWhile.ml: four catalogue entries, with resolved parameters (a normalized, possibly nested, code position; the prelude length and the body offsets; the typed condition of splitwhile). Each one is a pure function of the statement that re-checks all its side conditions (a loop at the position, the prelude and the offsets, the side conditions of fission / fusion as on main: read / write independence, deterministic and loop-, call- and raise-free prelude and epilog, raise-free body parts, without calls that may raise when the judgement observes exceptions; the equality of the preludes, epilogs and conditions of fusion), raising today's messages. No obligation, the memory is unchanged. - EcMatching.Position.cpos_of_nm_cpos: the code position denoting a normalized one, so that the entries rebuild their zipper from the recorded position without any lookup. - The tactics are derived, in every logic where they exist (hoare, ehoare, phoare, equiv on either side): resolve the position, then apply `t__transform` with the entry. They are uniform across logics, so EcPhlLoopTx holds a single dispatcher on the goal kind (no per-logic module that would only hold a one-line call). The no-op `t_low*` wrappers are gone; `unroll for` stays derived (rcond, wp, seq, conseq, cfold). The interface of EcPhlLoopTx is unchanged. - `EcLowPhlGoal.t_code_transform` (and its helpers `t_fold`, `t_zip` and their types) had no user left: removed. Behaviour is preserved: on every step of the new test, the goals and the error messages printed by the reference and new builds are identical. tests/fission-fusion-soundness.ec passes unchanged. A new test, tests/looptx.ec, exercises each transformation in every logic (both equiv sides, the transformed program checked against its expected form with `sim`), at nested positions (then / else branches, match branch, loop body), `unroll for`, and every error path; it passes with the reference build too. The stdlib (128 files), the unit tests (126) and the examples (49) pass under EC_RECHECK=1 with no RecheckFailure. Each transformation checker, when deliberately broken for the loop entries only, is caught only under EC_RECHECK: on the new test, and, for equiv-transform, on the stdlib (3 files) and the examples (4); hoare-, ehoare- and bdhoare-transform are reached by the loop transformations only in the new test. --- src/ecLowPhlGoal.ml | 83 ---- src/ecMatching.ml | 9 + src/ecMatching.mli | 3 + src/phl/README.md | 6 +- src/phl/REFACTORING.md | 18 +- src/phl/ecPhlLoopTx.ml | 303 +++---------- src/phl/rules/ecPlTransform.mli | 5 +- src/phl/rules/transforms/ecTrFission.ml | 183 ++++++++ src/phl/rules/transforms/ecTrFission.mli | 65 +++ src/phl/rules/transforms/ecTrFusion.ml | 87 ++++ src/phl/rules/transforms/ecTrFusion.mli | 39 ++ src/phl/rules/transforms/ecTrSplitWhile.ml | 45 ++ src/phl/rules/transforms/ecTrSplitWhile.mli | 24 + src/phl/rules/transforms/ecTrUnroll.ml | 38 ++ src/phl/rules/transforms/ecTrUnroll.mli | 21 + tests/looptx.ec | 465 ++++++++++++++++++++ 16 files changed, 1073 insertions(+), 321 deletions(-) create mode 100644 src/phl/rules/transforms/ecTrFission.ml create mode 100644 src/phl/rules/transforms/ecTrFission.mli create mode 100644 src/phl/rules/transforms/ecTrFusion.ml create mode 100644 src/phl/rules/transforms/ecTrFusion.mli create mode 100644 src/phl/rules/transforms/ecTrSplitWhile.ml create mode 100644 src/phl/rules/transforms/ecTrSplitWhile.mli create mode 100644 src/phl/rules/transforms/ecTrUnroll.ml create mode 100644 src/phl/rules/transforms/ecTrUnroll.mli create mode 100644 tests/looptx.ec diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 42a45b169..3a94352a7 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -823,89 +823,6 @@ let abstract_info2 env fl' fr' = end; ((topl, fl, oil, sigl), (topr, fr, oir, sigr)) -(* -------------------------------------------------------------------- *) -type code_txenv = proofenv * LDecl.hyps - -type 'a code_tx = - code_txenv -> 'a -> form pair -> memenv * stmt - -> memenv * stmt * form list - -type 'a zip_t = - code_txenv -> form pair -> memenv -> Zpr.zipper - -> memenv * Zpr.zipper * form list - -let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) = - try - let env = EcEnv.LDecl.toenv (snd cenv) in - let (me, f) = Zpr.fold env cenv cpos (fun _ -> f) state s in - ((me, f, []) : memenv * _ * form list) - with InvalidCPos -> tc_error (fst cenv) "invalid code position" - -let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) = - try - let env = EcEnv.LDecl.toenv (snd cenv) in - let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in - ((me, Zpr.zip zpr, gs) : memenv * _ * form list) - with InvalidCPos -> tc_error (fst cenv) "invalid code position" - -let t_code_transform (side : oside) cpos tr tx tc = - let pf = FApi.tc1_penv tc in - - match side with - | None -> begin - let (hyps, concl) = FApi.tc1_flat tc in - - match concl.f_node with - | FhoareS hs -> - let pr, po = hs_pr hs, hs_po hs in - (* The transformations only use the postcondition for the - program variables it reads: give them the conjunction of the - main and exceptional postconditions, so that none is missed. *) - let po = f_ands (POE.fold (fun fs f -> fs @ [f]) [] po.hsi_inv) in - let (me, stmt, cs) = - tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in - let concl = - f_hoareS (snd me) pr stmt (hs_po hs) - in - FApi.xmutate1 tc (tr None) (cs @ [concl]) - - | FbdHoareS bhs -> - let pr, po = bhs_pr bhs, bhs_po bhs in - let (me, stmt, cs) = - tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in - let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc (tr None) (cs @ [concl]) - - | FeHoareS ehs -> - let pr, po = ehs_pr ehs, ehs_po ehs in - let (me, stmt, cs) = - tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in - let concl = f_eHoareS (snd me) pr stmt po in - FApi.xmutate1 tc (tr None) (cs @ [concl]) - - | _ -> - let kinds = - [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in - tc_error_noXhl ~kinds:kinds pf - end - - | Some side -> - let hyps = FApi.tc1_hyps tc in - let es = tc1_as_equivS tc in - let pre, post = es_pr es, es_po es in - let me, stmt = - match side with - | `Left -> (es.es_ml, es.es_sl) - | `Right -> (es.es_mr, es.es_sr) in - let (_, mt), stmt, cs = tx (pf, hyps) cpos (pre.inv, post.inv) (me, stmt) in - let concl = - match side with - | `Left -> f_equivS mt (snd es.es_mr) (es_pr es) stmt es.es_sr (es_po es) - | `Right -> f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl stmt (es_po es) - in - - FApi.xmutate1 tc (tr (Some side)) (cs @ [concl]) - (* -------------------------------------------------------------------- *) let get_single tc = function | Single f -> f diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 27eebe0fe..c570b7867 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -389,6 +389,15 @@ module Position = struct let (env, s), npath = normalize_cpos_path env cpath s in (env, s), (npath, normalize_cpos1 env cp1 s) + (* The code position denoting a normalized one, with absolute positions + only: resolving it again in the same statement needs no lookup and + yields the same position. *) + let cpos_of_nm_cpos ((cpath, cp1) : nm_codepos) : codepos = + let brsel : nm_codepos_brsel -> codepos_brsel = function + | `Cond b -> `Cond b + | `Match ix -> `MatchByPos ix in + (List.map (fun (i, br) -> (cpos1 i, brsel br)) cpath, cpos1 cp1) + let resolve_offset1_from_cpos1 env (base: nm_codepos1) (off: codeoffset1) (s: stmt) : nm_codepos1 = match off with | `Absolute off -> normalize_cpos1 env off s diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 45268266d..f6e4ef7df 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -110,6 +110,9 @@ module Position : sig val normalize_cpos : env -> codepos -> stmt -> (env * stmt) * nm_codepos + (* The code position denoting a normalized one (absolute positions only). *) + val cpos_of_nm_cpos : nm_codepos -> codepos + val cpos1 : int -> codepos1 (* --- Gap types --- *) diff --git a/src/phl/README.md b/src/phl/README.md index d450b99f0..e3cfce6dc 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -109,8 +109,10 @@ Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), `rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-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 +(`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`), +`simplify-if` (`EcTrSimplifyIf`), and the loop transformations `fission` +(`EcTrFission`), `fusion` (`EcTrFusion`), `unroll` (`EcTrUnroll`) and +`splitwhile` (`EcTrSplitWhile`). `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 acbe47f78..dcaeabaf5 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -420,7 +420,21 @@ Current catalogue: - `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. + assignments into a single assignment (`simplify if`); no obligation; +- `fission` (`EcTrFission`, splitting the loop at a — possibly nested — + position in two loops at two offsets of its body, its prelude of `n` + instructions duplicated; read / write independence, determinism and + `raise`-freedom side conditions; no obligation), used by `fission` in + every logic; +- `fusion` (`EcTrFusion`, the inverse: merging two consecutive loops with + equal preludes, conditions and epilogs, under the side conditions of + `fission`; no obligation), used by `fusion` in every logic; +- `unroll` (`EcTrUnroll`): `while e do c` becomes + `if e then c; while e do c`; no obligation; used by `unroll` (`unroll + for` stays derived: rcond, wp, seq, conseq, cfold); +- `splitwhile` (`EcTrSplitWhile`): `while e do c` becomes + `while (e /\ b) do c; while e do c`; no obligation; used by + `splitwhile`. 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 @@ -428,7 +442,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: the loop transformations and proc rewrite. +with the tactics that use them: proc rewrite / change. 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/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 9a880c780..ccefe86db 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -14,6 +14,7 @@ open EcLowPhlGoal open EcPhlRCond open EcLowGoal +module Pos = EcMatching.Position module Zpr = EcMatching.Zipper module TTC = EcProofTyping @@ -24,243 +25,79 @@ type unroll_t = oside * pcodepos * [`While | `For of bool] type splitwhile_t = pexpr * oside * pcodepos (* -------------------------------------------------------------------- *) -(* Side conditions of loop fission / fusion, which state: - - init; while b { c1; c2; c3 } - == init; while b { c1; c3 }; init; while b { c2; c3 } - - (1) [init] (prelude) and [c3] (epilog) are deterministic, loop-, - call- and exception-free ([check_dslc]), and [c1] / [c2] do not - raise exceptions ([check_noraise]); - (2) [b] and [c3] read nothing written by [c1] or [c2]; - (3) [c1] and [c2] commute: neither reads what the other writes, and - they write disjoint sets of variables; - (4) [c3] only writes variables that [init] writes; - (5) [init] reads nothing written by [init], [c1] or [c3], and writes - nothing written by [c1]. - - Soundness: by (1) and (2), the number of iterations and the values - taken by the variables written by [c3] are a function of the state - after [init]. Then, by (2) and (3), in the fused loop, the [c1] part - (on [wr c1]) and the [c2; c3] part (on the other variables) evolve - without any information flow between them: the fused loop has the - same distribution as the product of the two split loops. By (1), - (4) and (5), the second [init] restores the state after the first - one on all variables but [wr c1], which it leaves untouched. Since - this is an equivalence, the same conditions apply to fusion. *) -let check_independence (pf, hyps) b init c1 c2 c3 = - let env = LDecl.toenv hyps in - - (* TODO improve error message, see swap *) - let check_disjoint s1 s2 = - if not (PV.indep env s1 s2) then - tc_error pf "independence check failed" - in - - let fv_b = e_read env b in - let rd_init = is_read env init in - let wr_init = is_write env init in - let rd_c1 = is_read env c1 in - let rd_c2 = is_read env c2 in - let rd_c3 = is_read env c3 in - let wr_c1 = is_write env c1 in - let wr_c2 = is_write env c2 in - let wr_c3 = is_write env c3 in - - check_disjoint rd_c1 wr_c2; - check_disjoint rd_c2 wr_c1; - check_disjoint wr_c1 wr_c2; - List.iter (check_disjoint fv_b) [wr_c1; wr_c2]; - if not (PV.subset wr_c3 wr_init) then - tc_error pf "epilog must only write variables written by the prelude"; - List.iter (check_disjoint rd_init) [wr_init; wr_c1; wr_c3]; - check_disjoint wr_init wr_c1; - List.iter (check_disjoint rd_c3) [wr_c1; wr_c2] +(* Derived tactics. The loop transformations are entries of the + transformation catalogue, applied through the transformation rule of + the goal's logic ([t__transform]; equiv: on the given side): + + t_fission side p (n, (d1, d2)) [EcTrFission.TrFission] + t_fusion side p (n, (d1, d2)) [EcTrFusion.TrFusion] + t_unroll side p [EcTrUnroll.TrUnroll] + t_splitwhile b side p [EcTrSplitWhile.TrSplitWhile] + + Each one resolves the code position [p] in the transformed statement + (failing with "invalid code position"), then applies the rule, which + runs the entry and reports its failures. No obligation: the only + visible goal is the transformed judgement, same pre / postconditions. + They are uniform across logics, hence a single dispatcher here rather + than one module per logic that would only hold a one-line call. The + [process_*] entries type the position (and the condition of + [splitwhile]) in the memory of the transformed statement. + + [unroll for] ([process_unroll_for]) stays derived: rcond, wp, seq, + conseq and cfold. *) (* -------------------------------------------------------------------- *) -let check_dslc pf name = - let error () = - tc_error pf - "%s must be deterministic and loop/procedure-call free" name in - - let rec doit_i c = - match c.i_node with - | Sasgn _ -> - () - - | Sif (_, c1, c2) -> - List.iter doit_s [c1; c2] - - | Smatch (_, bs) -> - List.iter (doit_s -| snd) bs - - | Srnd _ | Scall _ | Swhile _ | Sraise _ | Sabstract _ -> - error () - - and doit_s c = - List.iter doit_i c.s_node - - in fun c -> List.iter doit_i c - -(* -------------------------------------------------------------------- *) -(* [c1] / [c2] must not raise: if one raises at some iteration, the - executions of the other one that precede it in the original loop are - lost (or added). A [raise] is always rejected; when the goal observes - exceptions ([exn], see [swap]), so is a call to a procedure that may - raise ([EcLowPhlGoal.s_may_raise]). Otherwise, raising is as good as - not terminating, which fission / fusion preserve. *) -let check_noraise pf ~(exn : bool) env = - let rec doit_i c = - match c.i_node with - | Sraise _ -> tc_error pf "loop body must not raise exceptions" - | _ -> EcModules.i_iter doit_i c - - in fun c -> - List.iter doit_i c; - if exn && EcLowPhlGoal.s_may_raise env (stmt c) then - tc_error pf - "loop body must not call procedures that may raise exceptions \ - when the postcondition constrains exceptions" - -(* Whether the goal observes exceptions (see [swap]). *) -let observes_exn (tc : tcenv1) = - match (FApi.tc1_goal tc).f_node with - | FhoareS hs -> hs_observes_exn (hs_po hs) - | _ -> false - -(* -------------------------------------------------------------------- *) -let fission_stmt ~exn (il, (d1, d2)) (pf, hyps) me zpr = - if d2 < d1 then - tc_error pf "%s, %s" - "in loop-fission" - "second break offset must not be lower than the first one"; - - let (hd, init, b, sw, tl) = - match zpr.Zpr.z_tail with - | { i_node = Swhile (b, sw) } :: tl -> begin - if List.length zpr.Zpr.z_head < il then - tc_error pf "while-loop is not headed by %d intructions" il; - let (init, hd) = List.takedrop il zpr.Zpr.z_head in - (hd, init, b, sw, tl) - end - | _ -> tc_error pf "code position does not lead to a while-loop" - in - - if d2 > List.length sw.s_node then - tc_error pf "in loop fission, invalid offsets range"; - - let (s1, s2, s3) = - let (s1, s2) = List.takedrop (d1 ) sw.s_node in - let (s2, s3) = List.takedrop (d2-d1) s2 in - (s1, s2, s3) - in - - check_independence (pf, hyps) b init s1 s2 s3; - check_dslc pf "prelude" init; - check_dslc pf "epilog" s3; - List.iter (check_noraise pf ~exn (LDecl.toenv hyps)) [s1; s2]; - - let wl1 = i_while (b, stmt (s1 @ s3)) in - let wl2 = i_while (b, stmt (s2 @ s3)) in - let fis = (List.rev_append init [wl1]) - @ (List.rev_append init [wl2]) in - - (me, { zpr with Zpr.z_head = hd; Zpr.z_tail = fis @ tl }, []) - -let t_fission_r side cpos infos g = - let tr = fun side -> `LoopFission (side, cpos, infos) in - let exn = observes_exn g in - let cb = fun cenv _ me zpr -> fission_stmt ~exn infos cenv me zpr in - t_code_transform side cpos tr (t_zip cb) g - -let t_fission = FApi.t_low3 "loop-fission" t_fission_r +(* Resolve [cpos] in [s] to a normalized (possibly nested) position. *) +let resolve_cpos (tc : tcenv1) (cpos : Pos.codepos) (s : stmt) = + try fst (snd (Zpr.zipper_of_cpos_r (FApi.tc1_env tc) cpos s)) + with Pos.InvalidCPos -> tc_error !!tc "invalid code position" + +(* Apply the transformation [tr at], [at] being [cpos] resolved in the + transformed statement, through the transformation rule of the goal's + logic (equiv: of [side]). *) +let t_loop_transform + side cpos (tr : Pos.nm_codepos -> EcPlTransform.transform) tc += + match side, (FApi.tc1_goal tc).f_node with + | None, FhoareS hs -> + EcHoareTransform.t_hoare_transform + { htr_tr = tr (resolve_cpos tc cpos hs.hs_s) } tc + + | None, FeHoareS hs -> + EcEHoareTransform.t_ehoare_transform + { ehtr_tr = tr (resolve_cpos tc cpos hs.ehs_s) } tc + + | None, FbdHoareS hs -> + EcBdHoareTransform.t_bdhoare_transform + { btr_tr = tr (resolve_cpos tc cpos hs.bhs_s) } tc + + | None, _ -> + tc_error_noXhl ~kinds:[`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt] !!tc + + | Some side, _ -> + let es = tc1_as_equivS tc in + let s = sideif side es.es_sl es.es_sr in + EcEquivTransform.t_equiv_transform + { etr_side = side; etr_tr = tr (resolve_cpos tc cpos s) } tc (* -------------------------------------------------------------------- *) -let fusion_stmt ~exn (il, (d1, d2)) (pf, hyps) me zpr = - let env = LDecl.toenv hyps in - - let (hd, init1, b1, sw1, tl) = - match zpr.Zpr.z_tail with - | { i_node = Swhile (b, sw) } :: tl -> begin - if List.length zpr.Zpr.z_head < il then - tc_error pf "1st while-loop is not headed by %d intruction(s)" il; - let (init, hd) = List.takedrop il zpr.Zpr.z_head in - (hd, init, b, sw, tl) - end - | _ -> tc_error pf "code position does not lead to a while-loop" - in - - let (init2, b2, sw2, tl) = - if List.length tl < il then - tc_error pf "1st first-loop is not followed by %d instruction(s)" il; - let (init2, tl) = List.takedrop il tl in - match tl with - | { i_node = Swhile (b2, sw2) } :: tl -> (List.rev init2, b2, sw2, tl) - | _ -> tc_error pf "cannot find the 2nd while-loop" - in - - if d1 > List.length sw1.s_node then - tc_error pf "in loop-fusion, body is less than %d instruction(s)" d1; - if d2 > List.length sw2.s_node then - tc_error pf "in loop-fusion, body is less than %d instruction(s)" d2; - - let (sw1, fini1) = List.takedrop d1 sw1.s_node in - let (sw2, fini2) = List.takedrop d2 sw2.s_node in - - (* FIXME: costly *) - if not (EcReduction.EqTest.for_stmt env (stmt init1) (stmt init2)) then - tc_error pf "in loop-fusion, preludes do not match"; - if not (EcReduction.EqTest.for_stmt env (stmt fini1) (stmt fini2)) then - tc_error pf "in loop-fusion, epilogs do not match"; - if not (EcReduction.EqTest.for_expr env b1 b2) then - tc_error pf "in loop-fusion, while conditions do not match"; - - check_independence (pf, hyps) b1 init1 sw1 sw2 fini1; - check_dslc pf "prelude" init1; - check_dslc pf "epilog" fini1; - List.iter (check_noraise pf ~exn (LDecl.toenv hyps)) [sw1; sw2]; - - let wl = i_while (b1, stmt (sw1 @ sw2 @ fini1)) in - let fus = List.rev_append init1 [wl] in - - (me, { zpr with Zpr.z_head = hd; Zpr.z_tail = fus @ tl; }, []) - -let t_fusion_r side cpos infos g = - let tr = fun side -> `LoopFusion (side, cpos, infos) in - let exn = observes_exn g in - let cb = fun cenv _ me zpr -> fusion_stmt ~exn infos cenv me zpr in - t_code_transform side cpos tr (t_zip cb) g - -let t_fusion = FApi.t_low3 "loop-fusion" t_fusion_r - -(* -------------------------------------------------------------------- *) -let unroll_stmt (pf, _) me i = - match i.i_node with - | Swhile (e, sw) -> (me, [i_if (e, sw, stmt []); i]) - | _ -> tc_error pf "cannot find a while loop at given position" - -let t_unroll_r side cpos g = - let tr = fun side -> `LoopUnraoll (side, cpos) in - t_code_transform side cpos tr (t_fold unroll_stmt) g - -let t_unroll = FApi.t_low2 "loop-unroll" t_unroll_r - -(* -------------------------------------------------------------------- *) -let splitwhile_stmt b (pf, _) me i = - match i.i_node with - | Swhile (e, sw) -> - let op_ty = toarrow [tbool; tbool] tbool in - let op_and = e_op EcCoreLib.CI_Bool.p_and [] op_ty in - let e = e_app op_and [e; b] tbool in - (me, [i_while (e, sw); i]) - - | _ -> tc_error pf "cannot find a while loop at given position" - -let t_splitwhile_r b side cpos g = - let tr = fun side -> `SplitWhile (b, side, cpos) in - t_code_transform side cpos tr (t_fold (splitwhile_stmt b)) g - -let t_splitwhile = FApi.t_low3 "split-while" t_splitwhile_r +let t_fission side cpos (il, (d1, d2)) = + t_loop_transform side cpos (fun at -> + EcTrFission.TrFission + { trfi_at = at; trfi_init = il; trfi_d1 = d1; trfi_d2 = d2; }) + +let t_fusion side cpos (il, (d1, d2)) = + t_loop_transform side cpos (fun at -> + EcTrFusion.TrFusion + { trfu_at = at; trfu_init = il; trfu_d1 = d1; trfu_d2 = d2; }) + +let t_unroll side cpos = + t_loop_transform side cpos (fun at -> + EcTrUnroll.TrUnroll { trun_at = at; }) + +let t_splitwhile b side cpos = + t_loop_transform side cpos (fun at -> + EcTrSplitWhile.TrSplitWhile { trsw_at = at; trsw_cond = b; }) (* -------------------------------------------------------------------- *) let process_fission (side, cpos, infos) tc = diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index a724bb3b7..58710be7a 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -36,7 +36,10 @@ open EcEnv on the conditional alone), [EcTrSwap] (moving a block of a possibly nested block), [EcTrInline] (inlining procedure calls), [EcTrKill], [EcTrAlias], [EcTrSet], [EcTrSetMatch], [EcTrCFold], [EcTrAsgnCase] - and [EcTrSimplifyIf] (the code transformations). Entries live + and [EcTrSimplifyIf] (the code transformations), [EcTrFission] / + [EcTrFusion] (splitting / merging loops), [EcTrUnroll] (unrolling the + first iteration of a loop) and [EcTrSplitWhile] (splitting a loop on an + extra condition). 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]). *) diff --git a/src/phl/rules/transforms/ecTrFission.ml b/src/phl/rules/transforms/ecTrFission.ml new file mode 100644 index 000000000..150fa60a0 --- /dev/null +++ b/src/phl/rules/transforms/ecTrFission.ml @@ -0,0 +1,183 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcModules +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [fission] transformation, resolved: the position of + the loop is a normalized (possibly nested) code position. *) +type tr_fission = { + trfi_at : EcMatching.Position.nm_codepos; + trfi_init : int; + trfi_d1 : int; + trfi_d2 : int; +} + +type EcPlTransform.transform += TrFission of tr_fission + +(* -------------------------------------------------------------------- *) +(* Side conditions of loop fission / fusion, which state: + + init; while b { c1; c2; c3 } + == init; while b { c1; c3 }; init; while b { c2; c3 } + + (1) [init] (prelude) and [c3] (epilog) are deterministic, loop-, + call- and exception-free ([check_dslc]), and [c1] / [c2] do not + raise exceptions ([check_noraise]); + (2) [b] and [c3] read nothing written by [c1] or [c2]; + (3) [c1] and [c2] commute: neither reads what the other writes, and + they write disjoint sets of variables; + (4) [c3] only writes variables that [init] writes; + (5) [init] reads nothing written by [init], [c1] or [c3], and writes + nothing written by [c1]. + + Soundness: by (1) and (2), the number of iterations and the values + taken by the variables written by [c3] are a function of the state + after [init]. Then, by (2) and (3), in the fused loop, the [c1] part + (on [wr c1]) and the [c2; c3] part (on the other variables) evolve + without any information flow between them: the fused loop has the + same distribution as the product of the two split loops. By (1), + (4) and (5), the second [init] restores the state after the first + one on all variables but [wr c1], which it leaves untouched. Since + this is an equivalence, the same conditions apply to fusion. *) +let check_independence env b init c1 c2 c3 = + (* TODO improve error message, see swap *) + let check_disjoint s1 s2 = + if not (PV.indep env s1 s2) then + raise (InvalidTransform "independence check failed") + in + + let fv_b = e_read env b in + let rd_init = is_read env init in + let wr_init = is_write env init in + let rd_c1 = is_read env c1 in + let rd_c2 = is_read env c2 in + let rd_c3 = is_read env c3 in + let wr_c1 = is_write env c1 in + let wr_c2 = is_write env c2 in + let wr_c3 = is_write env c3 in + + check_disjoint rd_c1 wr_c2; + check_disjoint rd_c2 wr_c1; + check_disjoint wr_c1 wr_c2; + List.iter (check_disjoint fv_b) [wr_c1; wr_c2]; + if not (PV.subset wr_c3 wr_init) then + raise (InvalidTransform + "epilog must only write variables written by the prelude"); + List.iter (check_disjoint rd_init) [wr_init; wr_c1; wr_c3]; + check_disjoint wr_init wr_c1; + List.iter (check_disjoint rd_c3) [wr_c1; wr_c2] + +(* -------------------------------------------------------------------- *) +let check_dslc name = + let error () = + raise (InvalidTransform + (Printf.sprintf + "%s must be deterministic and loop/procedure-call free" name)) in + + let rec doit_i c = + match c.i_node with + | Sasgn _ -> + () + + | Sif (_, c1, c2) -> + List.iter doit_s [c1; c2] + + | Smatch (_, bs) -> + List.iter (doit_s -| snd) bs + + | Srnd _ | Scall _ | Swhile _ | Sraise _ | Sabstract _ -> + error () + + and doit_s c = + List.iter doit_i c.s_node + + in fun c -> List.iter doit_i c + +(* -------------------------------------------------------------------- *) +(* [c1] / [c2] must not raise: if one raises at some iteration, the + executions of the other one that precede it in the original loop are + lost (or added). A [raise] is always rejected; when the judgement + observes exceptions ([exn], see [EcTrSwap]), so is a call to a + procedure that may raise ([EcLowPhlGoal.s_may_raise]). Otherwise, + raising is as good as not terminating, which fission / fusion + preserve. *) +let check_noraise ~(exn : bool) env = + let rec doit_i c = + match c.i_node with + | Sraise _ -> + raise (InvalidTransform "loop body must not raise exceptions") + | _ -> EcModules.i_iter doit_i c + + in fun c -> + List.iter doit_i c; + if exn && EcLowPhlGoal.s_may_raise env (stmt c) then + raise (InvalidTransform + "loop body must not call procedures that may raise \ + exceptions when the postcondition constrains exceptions") + +(* All the side conditions, on the prelude [init], the condition [b], the + two parts [c1], [c2] and the epilog [c3]. *) +let check_side_conditions ~exn env b init c1 c2 c3 = + check_independence env b init c1 c2 c3; + check_dslc "prelude" init; + check_dslc "epilog" c3; + List.iter (check_noraise ~exn env) [c1; c2] + +(* -------------------------------------------------------------------- *) +(* Split the loop at [p], headed by [n] instructions, at the offsets + [d1 <= d2] of its body. *) +let fission (p : tr_fission) (ctxt : tr_ctxt) (s : stmt) = + let il, d1, d2 = p.trfi_init, p.trfi_d1, p.trfi_d2 in + let error msg = raise (InvalidTransform msg) in + + let zpr = + let cpos = EcMatching.Position.cpos_of_nm_cpos p.trfi_at in + try Zpr.zipper_of_cpos ctxt.trc_env cpos s + with EcMatching.Position.InvalidCPos -> error "invalid code position" in + + if d2 < d1 then + error (Printf.sprintf "%s, %s" + "in loop-fission" + "second break offset must not be lower than the first one"); + + let (hd, init, b, sw, tl) = + match zpr.Zpr.z_tail with + | { i_node = Swhile (b, sw) } :: tl -> begin + if List.length zpr.Zpr.z_head < il then + error (Printf.sprintf + "while-loop is not headed by %d intructions" il); + let (init, hd) = List.takedrop il zpr.Zpr.z_head in + (hd, init, b, sw, tl) + end + | _ -> error "code position does not lead to a while-loop" + in + + if d2 > List.length sw.s_node then + error "in loop fission, invalid offsets range"; + + let (s1, s2, s3) = + let (s1, s2) = List.takedrop (d1 ) sw.s_node in + let (s2, s3) = List.takedrop (d2-d1) s2 in + (s1, s2, s3) + in + + check_side_conditions ~exn:ctxt.trc_exn ctxt.trc_env b init s1 s2 s3; + + let wl1 = i_while (b, stmt (s1 @ s3)) in + let wl2 = i_while (b, stmt (s2 @ s3)) in + let fis = (List.rev_append init [wl1]) + @ (List.rev_append init [wl2]) in + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_head = hd; Zpr.z_tail = fis @ tl }; + trr_obl = []; } + +let () = + register (function + | TrFission p -> Some (fission p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrFission.mli b/src/phl/rules/transforms/ecTrFission.mli new file mode 100644 index 000000000..cb7da8985 --- /dev/null +++ b/src/phl/rules/transforms/ecTrFission.mli @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcEnv +open EcTypes +open EcModules +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_fission = { + trfi_at : nm_codepos; (* position of the loop (resolved, maybe nested) *) + trfi_init : int; (* length n of the prelude *) + trfi_d1 : int; (* first break offset d1 in the body *) + trfi_d2 : int; (* second break offset d2 in the body *) +} + +(* [TrFission { trfi_at = p; trfi_init = n; trfi_d1 = d1; trfi_d2 = d2 }] + — splits a loop into two loops, at the (possibly nested) position [p], + the loop being preceded by a prelude [init] of [n] instructions (in the + same block), its body being cut at the offsets [d1 <= d2]: + + c = ...; init; while b do { c1; c2; c3 }; ... + ~~> + c' = ...; init; while b do { c1; c3 }; init; while b do { c2; c3 }; ... + + where [c1 = body[0..d1)], [c2 = body[d1..d2)], [c3 = body[d2..)]. Side + conditions ([check_side_conditions]): + (1) [init] and [c3] are made of assignments, conditionals and matches + only (deterministic, free of loops, calls and [raise]), and [c1], + [c2] contain no [raise] and, when the judgement observes exceptions + (the context's [trc_exn]), no call to a procedure that may raise + ([EcLowPhlGoal.s_may_raise]); + (2) [b] and [c3] read no variable written by [c1] or [c2]; + (3) [c1] reads no variable written by [c2] and conversely, and they + write disjoint sets of variables; + (4) [c3] only writes variables written by [init]; + (5) [init] reads no variable written by [init], [c1] or [c3], and + writes no variable written by [c1]. + Then the number of iterations and what [c3] writes only depend on the + state after [init], the [c1] part and the [c2; c3] part of the fused + loop exchange no information, and the second [init] restores the state + after the first one but on what [c1] writes, which it does not touch. + No obligation, the memory is unchanged. + + Fails, in this order, with "invalid code position" (when [p] is not a + position of [c]), "in loop-fission, second break offset must not be + lower than the first one", "code position does not lead to a + while-loop", "while-loop is not headed by intructions", "in loop + fission, invalid offsets range", "independence check failed" / "epilog + must only write variables written by the prelude", "prelude must be + deterministic and loop/procedure-call free", "epilog must be ...", + "loop body must not raise exceptions", "loop body must not call + procedures that may raise exceptions when the postcondition constrains + exceptions". *) +type EcPlTransform.transform += TrFission of tr_fission + +(* -------------------------------------------------------------------- *) +(* The side conditions of the loop fission, shared with the loop fusion + ([EcTrFusion]); they raise [EcPlTransform.InvalidTransform]. *) + +(* [check_side_conditions ~exn env b init c1 c2 c3]: the conditions + (1)-(5) above, [exn] telling whether the judgement observes + exceptions. *) +val check_side_conditions : + exn:bool -> env -> expr -> instr list -> instr list -> instr list -> instr list -> unit diff --git a/src/phl/rules/transforms/ecTrFusion.ml b/src/phl/rules/transforms/ecTrFusion.ml new file mode 100644 index 000000000..24673d58e --- /dev/null +++ b/src/phl/rules/transforms/ecTrFusion.ml @@ -0,0 +1,87 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [fusion] transformation, resolved: the position of + the first loop is a normalized (possibly nested) code position. *) +type tr_fusion = { + trfu_at : EcMatching.Position.nm_codepos; + trfu_init : int; + trfu_d1 : int; + trfu_d2 : int; +} + +type EcPlTransform.transform += TrFusion of tr_fusion + +(* -------------------------------------------------------------------- *) +(* Merge the loop at [p] with the next one, both headed by the same [n] + instructions, their bodies ending with the same epilog after [d1] and + [d2] instructions. *) +let fusion (p : tr_fusion) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + let il, d1, d2 = p.trfu_init, p.trfu_d1, p.trfu_d2 in + let error msg = raise (InvalidTransform msg) in + + let zpr = + let cpos = EcMatching.Position.cpos_of_nm_cpos p.trfu_at in + try Zpr.zipper_of_cpos env cpos s + with EcMatching.Position.InvalidCPos -> error "invalid code position" in + + let (hd, init1, b1, sw1, tl) = + match zpr.Zpr.z_tail with + | { i_node = Swhile (b, sw) } :: tl -> begin + if List.length zpr.Zpr.z_head < il then + error (Printf.sprintf + "1st while-loop is not headed by %d intruction(s)" il); + let (init, hd) = List.takedrop il zpr.Zpr.z_head in + (hd, init, b, sw, tl) + end + | _ -> error "code position does not lead to a while-loop" + in + + let (init2, b2, sw2, tl) = + if List.length tl < il then + error (Printf.sprintf + "1st first-loop is not followed by %d instruction(s)" il); + let (init2, tl) = List.takedrop il tl in + match tl with + | { i_node = Swhile (b2, sw2) } :: tl -> (List.rev init2, b2, sw2, tl) + | _ -> error "cannot find the 2nd while-loop" + in + + if d1 > List.length sw1.s_node then + error (Printf.sprintf + "in loop-fusion, body is less than %d instruction(s)" d1); + if d2 > List.length sw2.s_node then + error (Printf.sprintf + "in loop-fusion, body is less than %d instruction(s)" d2); + + let (sw1, fini1) = List.takedrop d1 sw1.s_node in + let (sw2, fini2) = List.takedrop d2 sw2.s_node in + + (* FIXME: costly *) + if not (EcReduction.EqTest.for_stmt env (stmt init1) (stmt init2)) then + error "in loop-fusion, preludes do not match"; + if not (EcReduction.EqTest.for_stmt env (stmt fini1) (stmt fini2)) then + error "in loop-fusion, epilogs do not match"; + if not (EcReduction.EqTest.for_expr env b1 b2) then + error "in loop-fusion, while conditions do not match"; + + EcTrFission.check_side_conditions ~exn:ctxt.trc_exn env b1 init1 sw1 sw2 fini1; + + let wl = i_while (b1, stmt (sw1 @ sw2 @ fini1)) in + let fus = List.rev_append init1 [wl] in + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_head = hd; Zpr.z_tail = fus @ tl; }; + trr_obl = []; } + +let () = + register (function + | TrFusion p -> Some (fusion p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrFusion.mli b/src/phl/rules/transforms/ecTrFusion.mli new file mode 100644 index 000000000..4b28fae2e --- /dev/null +++ b/src/phl/rules/transforms/ecTrFusion.mli @@ -0,0 +1,39 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_fusion = { + trfu_at : nm_codepos; (* position of the 1st loop (resolved, + maybe nested) *) + trfu_init : int; (* length n of the preludes *) + trfu_d1 : int; (* length d1 of the 1st body, epilog excluded *) + trfu_d2 : int; (* length d2 of the 2nd body, epilog excluded *) +} + +(* [TrFusion { trfu_at = p; trfu_init = n; trfu_d1 = d1; trfu_d2 = d2 }] + — merges two loops with the same condition, prelude and epilog, the + first one at the (possibly nested) position [p], both preceded by a + prelude of [n] instructions (in the same block): + + c = ...; init; while b do { c1; c3 }; init'; while b' do { c2; c3' }; ... + ~~> + c' = ...; init; while b do { c1; c2; c3 }; ... + + where [c1] (resp. [c2]) is made of the first [d1] (resp. [d2]) + instructions of its body, and [init] and [init'] (resp. [c3] and [c3'], + [b] and [b']) are equal (up to [EcReduction.EqTest]). Side conditions: + those of the fission, of which this is the inverse + ([EcTrFission.check_side_conditions ~exn b init c1 c2 c3]). No obligation, + the memory is unchanged. + + Fails, in this order, with "invalid code position" (when [p] is not a + position of [c]), "code position does not lead to a while-loop", "1st + while-loop is not headed by intruction(s)", "1st first-loop is not + followed by instruction(s)", "cannot find the 2nd while-loop", "in + loop-fusion, body is less than instruction(s)" (then ), "in + loop-fusion, preludes do not match", "in loop-fusion, epilogs do not + match", "in loop-fusion, while conditions do not match", then the + failures of the fission's side conditions. *) +type EcPlTransform.transform += TrFusion of tr_fusion diff --git a/src/phl/rules/transforms/ecTrSplitWhile.ml b/src/phl/rules/transforms/ecTrSplitWhile.ml new file mode 100644 index 000000000..7f4554db0 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSplitWhile.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcAst +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [splitwhile] transformation, resolved: the position + of the loop is a normalized (possibly nested) code position, the + additional condition a typed expression. *) +type tr_splitwhile = { + trsw_at : EcMatching.Position.nm_codepos; + trsw_cond : expr; +} + +type EcPlTransform.transform += TrSplitWhile of tr_splitwhile + +(* -------------------------------------------------------------------- *) +(* Precede the loop at [p] by the same loop, also guarded by [b]. *) +let splitwhile (p : tr_splitwhile) (ctxt : tr_ctxt) (s : stmt) = + let split1 (i : instr) = + match i.i_node with + | Swhile (e, sw) -> + let op_ty = toarrow [tbool; tbool] tbool in + let op_and = e_op EcCoreLib.CI_Bool.p_and [] op_ty in + let e = e_app op_and [e; p.trsw_cond] tbool in + ((), [i_while (e, sw); i]) + + | _ -> + raise (InvalidTransform "cannot find a while loop at given position") in + + let (), s = + let cpos = EcMatching.Position.cpos_of_nm_cpos p.trsw_at in + try Zpr.map ctxt.trc_env cpos split1 s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + { trr_me = ctxt.trc_me; trr_s = s; trr_obl = []; } + +let () = + register (function + | TrSplitWhile p -> Some (splitwhile p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrSplitWhile.mli b/src/phl/rules/transforms/ecTrSplitWhile.mli new file mode 100644 index 000000000..8b2fa1c26 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSplitWhile.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_splitwhile = { + trsw_at : nm_codepos; (* position of the loop (resolved, maybe nested) *) + trsw_cond : expr; (* the additional condition b (typed, bool) *) +} + +(* [TrSplitWhile { trsw_at = p; trsw_cond = b }] — splits the loop at the + (possibly nested) position [p] into the iterations where [b] also + holds, then the remaining ones: + + c = ...; while e do c1; ... ~~> c' = ...; while (e /\ b) do c1; + while e do c1; ... + + No obligation, the memory is unchanged. Fails with "invalid code + position" when [p] is not an instruction of [c], and with "cannot find + a while loop at given position" when that instruction is not a + [while]. *) +type EcPlTransform.transform += TrSplitWhile of tr_splitwhile diff --git a/src/phl/rules/transforms/ecTrUnroll.ml b/src/phl/rules/transforms/ecTrUnroll.ml new file mode 100644 index 000000000..4a8e38daf --- /dev/null +++ b/src/phl/rules/transforms/ecTrUnroll.ml @@ -0,0 +1,38 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the [unroll] transformation, resolved: the position of + the loop is a normalized (possibly nested) code position. *) +type tr_unroll = { + trun_at : EcMatching.Position.nm_codepos; +} + +type EcPlTransform.transform += TrUnroll of tr_unroll + +(* -------------------------------------------------------------------- *) +(* Replace the loop at [p] by its first iteration, guarded by the loop + condition, followed by the loop itself. *) +let unroll (p : tr_unroll) (ctxt : tr_ctxt) (s : stmt) = + let unroll1 (i : instr) = + match i.i_node with + | Swhile (e, sw) -> ((), [i_if (e, sw, stmt []); i]) + | _ -> + raise (InvalidTransform "cannot find a while loop at given position") in + + let (), s = + let cpos = EcMatching.Position.cpos_of_nm_cpos p.trun_at in + try Zpr.map ctxt.trc_env cpos unroll1 s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + { trr_me = ctxt.trc_me; trr_s = s; trr_obl = []; } + +let () = + register (function + | TrUnroll p -> Some (unroll p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrUnroll.mli b/src/phl/rules/transforms/ecTrUnroll.mli new file mode 100644 index 000000000..15da605b7 --- /dev/null +++ b/src/phl/rules/transforms/ecTrUnroll.mli @@ -0,0 +1,21 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_unroll = { + trun_at : nm_codepos; (* position of the loop (resolved, maybe nested) *) +} + +(* [TrUnroll { trun_at = p }] — unrolls the first iteration of the loop + at the (possibly nested) position [p]: + + c = ...; while e do c1; ... ~~> c' = ...; if e then c1; + while e do c1; ... + + No obligation, the memory is unchanged. Fails with "invalid code + position" when [p] is not an instruction of [c], and with "cannot find + a while loop at given position" when that instruction is not a + [while]. *) +type EcPlTransform.transform += TrUnroll of tr_unroll diff --git a/tests/looptx.ec b/tests/looptx.ec new file mode 100644 index 000000000..1d886e5e0 --- /dev/null +++ b/tests/looptx.ec @@ -0,0 +1,465 @@ +require import AllCore Xreal. + +(* Loop transformations (fission, fusion, unroll, splitwhile) in every + logic: each one replaces the program by an equivalent one. The equiv + lemmas check the transformed program against its expected form with + [sim]. *) + +exception e1. + +module M = { + var x, y : int + var b : bool + var o : int option + + proc f() = { + var i; + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + + (* [f] after [fission 2 @ 1, 2]. *) + proc f_fis() = { + var i; + i <- 0; + while (i < 10) { + x <- x + 1; + i <- i + 1; + } + i <- 0; + while (i < 10) { + y <- y + 2; + i <- i + 1; + } + } + + (* [f] after [unroll 2]. *) + proc f_unroll() = { + var i; + i <- 0; + if (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + + (* [f] after [splitwhile 2 : (i < 5)]. *) + proc f_split() = { + var i; + i <- 0; + while (i < 10 /\ i < 5) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + + (* The loop of [f] under a conditional (both branches), a match and a + loop. *) + proc g() = { + var i, j; + if (b) { + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } else { + x <- 0; + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + match o with + | None => { } + | Some v => { + i <- v; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + end; + j <- 0; + while (j < 2) { + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + j <- j + 1; + } + } + + (* [g] after fission in the then branch, unroll in the else branch, + splitwhile in the match branch and fission then fusion in the + loop. *) + proc g_r() = { + var i, j; + if (b) { + i <- 0; + while (i < 10) { + x <- x + 1; + i <- i + 1; + } + i <- 0; + while (i < 10) { + y <- y + 2; + i <- i + 1; + } + } else { + x <- 0; + i <- 0; + if (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + match o with + | None => { } + | Some v => { + i <- v; + while (i < 10 /\ x < 3) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + } + end; + j <- 0; + while (j < 2) { + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + 2; + i <- i + 1; + } + j <- j + 1; + } + } + + (* Error paths. *) + proc h() = { + var i; + x <- 0; + i <- 0; + while (i < 10) { + x <- x + 1; + y <- y + x; + i <- i + 1; + b <$ {0,1}; + } + i <- 0; + while (i < 10) { + y <- y + 1; + i <- i + 1; + b <$ {0,1}; + } + i <- 0; + while (i < 11) { + y <- y + 1; + i <- i + 2; + } + } + + proc k() = { + var i; + i <- 0; + while (i < 10) { + x <- x + 1; + i <- i + 1; + } + i <- 1; + while (i < 10) { + y <- y + 1; + i <- i + 1; + } + } + + (* For [unroll for]. *) + proc u() = { + var i; + i <- 0; + while (i < 3) { + x <- x + i; + i <- i + 1; + } + } +}. + +(* -------------------------------------------------------------------- *) +(* equiv, both sides: the transformed program is the expected one. *) + +lemma equiv_fission_left : equiv [M.f ~ M.f_fis : ={glob M} ==> ={glob M}]. +proof. proc; fission{1} 2 @ 1, 2; sim. qed. + +lemma equiv_fission_right : equiv [M.f_fis ~ M.f : ={glob M} ==> ={glob M}]. +proof. proc; fission{2} 2!1 @ 1, 2; sim. qed. + +lemma equiv_fusion_left : equiv [M.f_fis ~ M.f : ={glob M} ==> ={glob M}]. +proof. proc; fusion{1} 2 @ 1, 1; sim. qed. + +lemma equiv_fusion_right : equiv [M.f ~ M.f_fis : ={glob M} ==> ={glob M}]. +proof. proc; fusion{2} 2!1 @ 1, 1; sim. qed. + +lemma equiv_unroll : equiv [M.f ~ M.f_unroll : ={glob M} ==> ={glob M}]. +proof. proc; unroll{1} 2; sim. qed. + +lemma equiv_unroll_right : equiv [M.f_unroll ~ M.f : ={glob M} ==> ={glob M}]. +proof. proc; unroll{2} ^while; sim. qed. + +lemma equiv_splitwhile : equiv [M.f ~ M.f_split : ={glob M} ==> ={glob M}]. +proof. proc; splitwhile{1} 2 : (i < 5); sim. qed. + +lemma equiv_splitwhile_right : equiv [M.f_split ~ M.f : ={glob M} ==> ={glob M}]. +proof. proc; splitwhile{2} -1 : (i < 5); sim. qed. + +(* Nested positions: then / else branches, match branch, loop body. *) +lemma equiv_nested : equiv [M.g ~ M.g_r : ={glob M} ==> ={glob M}]. +proof. +proc. +fission{1} 1.2 @ 1, 2. +unroll{1} 1?3. +splitwhile{1} 2#Some.2 : (M.x < 3). +fission{1} 4.2 @ 2, 2. +fusion{1} 4.2 @ 2, 0. +sim. +qed. + +lemma equiv_nested_right : equiv [M.g_r ~ M.g : ={glob M} ==> ={glob M}]. +proof. +proc. +fission{2} 1.2 @ 1, 2. +unroll{2} 1?3. +splitwhile{2} 2#Some.2 : (M.x < 3). +sim. +qed. + +(* -------------------------------------------------------------------- *) +(* hoare (exceptional postconditions kept), ehoare, phoare. *) + +lemma hoare_looptx : hoare [M.f : true ==> M.x = 0 | e1 => M.y = 0]. +proof. +proc. +fission 2 @ 1, 2. +fusion 2 @ 1, 1. +unroll 2. +splitwhile 3 : (i < 5). +abort. + +lemma hoare_looptx_nested : hoare [M.g : true ==> true]. +proof. +proc. +fission 1.2 @ 1, 2. +fusion 1.2 @ 1, 1. +unroll 1?3. +splitwhile 2#Some.2 : (M.x < 3). +fission 4.2 @ 2, 2. +by trivial. +qed. + +lemma ehoare_looptx : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +fission 2 @ 1, 2. +fusion 2 @ 1, 1. +unroll 2. +splitwhile 3 : (i < 5). +abort. + +lemma ehoare_looptx_nested : ehoare [M.g : 1%xr ==> 1%xr]. +proof. +proc. +fission 1.2 @ 1, 2. +unroll 1?3. +splitwhile 2#Some.2 : (M.x < 3). +fission 4.2 @ 2, 2. +abort. + +lemma phoare_looptx : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +fission 2 @ 1, 2. +fusion 2 @ 1, 1. +unroll 2. +splitwhile 3 : (i < 5). +abort. + +lemma phoare_looptx_nested : phoare [M.g : true ==> M.x = 0] <= 1%r. +proof. +proc. +fission 1.2 @ 1, 2. +unroll 1?3. +splitwhile 2#Some.2 : (M.x < 3). +fission 4.2 @ 2, 2. +abort. + +(* Closed proofs, so that the proof-nodes are checked (EC_RECHECK). *) +lemma ehoare_looptx_closed : ehoare [M.g : 1%xr ==> 0%xr]. +proof. +proc. +fission 1.2 @ 1, 2. +fusion 1.2 @ 1, 1. +unroll 1?3. +splitwhile 2#Some.2 : (M.x < 3). +by trivial. +qed. + +lemma phoare_looptx_closed : phoare [M.g : false ==> true] = 1%r. +proof. +proc. +fission 1.2 @ 1, 2. +fusion 1.2 @ 1, 1. +unroll 1?3. +splitwhile 2#Some.2 : (M.x < 3). +by exfalso. +qed. + +(* unroll for: derived (rcond, wp, seq, conseq, cfold). *) +lemma hoare_unroll_for : hoare [M.u : M.x = 0 ==> M.x = 3]. +proof. +proc. +unroll for 2. +by auto. +qed. + +lemma equiv_unroll_for : equiv [M.u ~ M.u : ={M.x} ==> ={M.x}]. +proof. +proc. +unroll for{1} 2. +unroll for*{2} 2. +by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Error paths. *) + +lemma hoare_fission_errors : hoare [M.h : true ==> true]. +proof. +proc. +fail fission 3 @ 2, 1. (* second offset lower than the first *) +fail fission 2 @ 1, 2. (* not a loop *) +fail fission 10 @ 1, 2. (* invalid code position *) +fail fission 10 @ 2, 1. (* invalid code position, before the offsets *) +fail fission 3!3 @ 1, 2. (* not headed by 3 instructions *) +fail fission 3 @ 1, 5. (* invalid offsets range *) +fail fission 3!1 @ 1, 2. (* independence: c2 reads x, written by c1 *) +fail fission 3!1 @ 2, 3. (* independence: b reads i, written by c2 *) +fail fission 3!0 @ 2, 2. (* independence: c3 writes i, read by b, not + written by the (empty) prelude *) +fail fission 3 @ 2, 2. (* epilog samples *) +fail fission 5!1 @ 0, 1. (* epilog samples (2nd loop) *) +fail fission {1} 3 @ 1, 2. (* side on a hoare goal *) +abort. + +lemma hoare_fusion_errors : hoare [M.h : true ==> true]. +proof. +proc. +fail fusion 2 @ 1, 1. (* not a loop *) +fail fusion 10 @ 1, 1. (* invalid code position *) +fail fusion 3!3 @ 1, 1. (* 1st loop not headed by 3 instructions *) +fail fusion 7!3 @ 1, 1. (* 1st loop not followed by 3 instructions *) +fail fusion 5!2 @ 1, 1. (* no 2nd loop *) +fail fusion 3 @ 5, 1. (* 1st body too short *) +fail fusion 3 @ 1, 5. (* 2nd body too short *) +fail fusion 3 @ 1, 1. (* epilogs do not match *) +fail fusion 5 @ 2, 2. (* epilogs do not match *) +fail fusion 5 @ 3, 2. (* conditions do not match *) +fail fusion 3 @ 2, 1. (* independence: c1 reads y, written by c2 *) +fail fusion 3 @ 3, 2. (* independence *) +fail fusion {2} 3 @ 1, 1. (* side on a hoare goal *) +abort. + +lemma hoare_fusion_errors2 : hoare [M.k : true ==> true]. +proof. +proc. +fail fusion 2 @ 1, 1. (* preludes do not match *) +fail fusion 2!2 @ 1, 1. (* not headed by 2 instructions *) +abort. + +lemma ehoare_errors : ehoare [M.h : 1%xr ==> 1%xr]. +proof. +proc. +fail fission 3 @ 2, 1. (* second offset lower than the first *) +fail fusion 2 @ 1, 1. (* not a loop *) +fail unroll 1. (* not a loop *) +fail splitwhile 10 : true. (* invalid code position *) +abort. + +lemma phoare_errors : phoare [M.h : true ==> true] = 1%r. +proof. +proc. +fail fission 3 @ 1, 5. (* invalid offsets range *) +fail fusion 5 @ 1, 1. (* epilogs do not match *) +fail fusion 3 @ 2, 1. (* independence *) +fail unroll 9. (* invalid code position *) +fail splitwhile 1 : true. (* not a loop *) +fail unroll {1} 3. (* side on a phoare goal *) +abort. + +lemma loop_errors : hoare [M.g : true ==> true]. +proof. +proc. +fail unroll 1. (* not a loop *) +fail unroll 6. (* invalid code position *) +fail unroll 5. (* after the last instruction *) +fail unroll 1.1. (* not a loop, nested *) +fail unroll 1.4. (* invalid code position, nested *) +fail unroll 2#None.1. (* invalid code position, empty branch *) +fail unroll 3.1. (* no such branch *) +fail splitwhile 1 : true. (* not a loop *) +fail splitwhile 5 : true. (* invalid code position *) +fail splitwhile 1.2 : 1. (* not a boolean *) +fail fission 1.1 @ 1, 2. (* not a loop, nested *) +fail fission 1.3 @ 1, 2. (* after the last instruction, nested *) +fail fission 5 @ 1, 2. (* after the last instruction *) +fail fusion 4.2 @ 1, 1. (* no 2nd loop *) +abort. + +lemma equiv_errors : equiv [M.h ~ M.h : true ==> true]. +proof. +proc. +fail unroll 3. (* no side on an equiv goal *) +fail fission 3 @ 1, 2. (* no side on an equiv goal *) +fail fission{1} 3 @ 2, 1. (* second offset lower than the first *) +fail fission{2} 3 @ 2, 2. (* epilog samples *) +fail fusion{1} 3 @ 1, 1. (* epilogs do not match *) +fail fusion{2} 5 @ 3, 2. (* conditions do not match *) +fail fusion{2} 10 @ 1, 1. (* invalid code position *) +fail unroll{1} 1. (* not a loop *) +fail unroll{2} 10. (* invalid code position *) +fail splitwhile{1} 2 : true. (* not a loop *) +fail splitwhile{2} 10 : true. (* invalid code position *) +abort.