diff --git a/src/ecMatching.ml b/src/ecMatching.ml index c12e64a3f..8590bff8c 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -583,33 +583,51 @@ module Zipper = struct let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; } - let zipper_step_into_block + (* Step into the block selected by a normalized step: nothing is + resolved. *) + let zipper_step_into_nm_block (env : EcEnv.env) - ((cp1, sub) : codepos_step) + ((cp1, sub) : nm_codepos_step) (s : stmt) (zpr : ipath) - : (ipath * stmt) * nm_codepos_step * env + : (ipath * stmt) * env = - let (s1, i, s2) = find_by_cpos1 env cp1 s in - let zpr, step, env = - match i.i_node, sub with - | Swhile (e, sw), `Cond true -> - (ZWhile (e, ((s1, s2), zpr)), sw), `Cond true, env + let (s1, i, s2) = find_by_nmcpos1 cp1 s in + match i.i_node, sub with + | Swhile (e, sw), `Cond true -> + (ZWhile (e, ((s1, s2), zpr)), sw), env - | Sif (e, ifs1, ifs2), `Cond true -> - (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), `Cond true, env + | Sif (e, ifs1, ifs2), `Cond true -> + (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), env - | Sif (e, ifs1, ifs2), `Cond false -> - (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env + | Sif (e, ifs1, ifs2), `Cond false -> + (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), env - | Smatch (e, bs), _ -> - let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in - let prebr, (locals, body), postbr = List.pivot_at ix bs in - let env = EcEnv.Var.bind_locals locals env in - (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env + | Smatch (e, bs), `Match ix -> + let prebr, (locals, body), postbr = + try List.pivot_at ix bs + with (Invalid_argument _ | Not_found) -> raise InvalidCPos in + let env = EcEnv.Var.bind_locals locals env in + (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), env - | _ -> raise InvalidCPos - in zpr, ((List.length s1), step), env + | _ -> raise InvalidCPos + + let zipper_step_into_block + (env : EcEnv.env) + ((cp1, sub) : codepos_step) + (s : stmt) + (zpr : ipath) + : (ipath * stmt) * nm_codepos_step * env + = + let (_, i, _), cp1 = find_and_normalize_cpos1 env cp1 s in + let sub = + match i.i_node, sub with + | Smatch (e, _), _ -> + `Match (select_match_arm (fun () -> raise InvalidCPos) env e sub) + | _, `Cond b -> `Cond b + | _ -> raise InvalidCPos in + let zs, env = zipper_step_into_nm_block env (cp1, sub) s zpr in + zs, (cp1, sub), env let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) = List.fold_left_map @@ -634,6 +652,17 @@ module Zipper = struct let zipper_of_cgap (env : EcEnv.env) (cp : codegap) (s : stmt) = fst (zipper_of_cgap_r env cp s) + + (* Normalized counterpart of [zipper_of_cgap]: nothing is resolved. *) + let zipper_of_nm_cgap (env : EcEnv.env) ((cpath, nm) : nm_codegap) (s : stmt) = + let (zpr, s), env = + List.fold_left + (fun ((zpr, s), env) step -> zipper_step_into_nm_block env step s zpr) + ((ZTop, s), env) cpath in + check_nm_cgap1 nm s; + let s1, s2 = split_at_nmcgap1 nm s in + zipper ~env (List.rev s1) s2 zpr + (* * Returns: * - A zipper pointing to the start of the range diff --git a/src/ecMatching.mli b/src/ecMatching.mli index a0d9e2598..e45e50c72 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -263,6 +263,13 @@ module Zipper : sig val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * (nm_codepos * stmt) val zipper_of_cpos : env -> codepos -> stmt -> zipper + (* Return the zipper for the stmt [stmt] at the normalized code gap + * [nm_codegap], the environment binding the locals of the enclosing + * [match] arms. Pure: nothing is resolved. Raise [InvalidCPos] if + * [nm_codegap] is not valid for [stmt]. + *) + val zipper_of_nm_cgap : env -> nm_codegap -> 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 388f1f969..ac483ef19 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -83,7 +83,7 @@ Run the test suite with `EC_RECHECK=1` to exercise every migrated checker. ## Program transformations Tactics that replace the program by an equivalent one and keep the judgement -(rndsem, rcond, and later inline, swap, …) go through **one** trusted +(rndsem, rcond, swap, and later inline, …) go through **one** trusted transformation rule per logic, `t__transform` (`EcTransform`; equiv: one side at a time), parameterized by an entry of a catalogue: @@ -106,10 +106,11 @@ equiv: one side at a time), parameterized by an entry of a catalogue: subgoals up to conversion (programs up to alpha-equivalence). Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), -`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`) and `match-push` -(`EcTrMatchPush`), the last two pushing the continuation of a leading -conditional / `match` into its branches. The `if` and `match` tactics are -push + rule on the conditional alone (`EcIf`, `EcMatch`). +`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push` +(`EcTrMatchPush`) and `swap` (`EcTrSwap`). `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`). Further entries come with the tactics that use them. The framed form of `match C k` changes the precondition: it stays a separate trusted rule of each logic, `t__rmatch_framed` (`EcRMatch`). See diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index fa49d6764..bce9d6b40 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -382,7 +382,12 @@ Current catalogue: the single instruction `match e with C xs => { b; c } ...`; no obligation. The pattern variables are local identifiers bound in the branch only: the binders of a branch are renamed apart when they occur - free in `c`, so that `c` is not captured. + free in `c`, so that `c` is not captured; +- `swap` (`EcTrSwap`, moving the block `[s..f)` of the possibly nested block + at a resolved path to a gap `t` outside it; the independence of the + exchanged statements and the absence of `raise` are checked by the entry; + no obligation, same memory), used by `swap` (and `interleave`, a sequence + of swaps) in every logic. 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 @@ -390,8 +395,8 @@ 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: swap, inline, kill/alias/cfold/set and -proc rewrite. +with the tactics that use them: inline, kill/alias/cfold/set and proc +rewrite. Exception: the framed form of `match C k` (used when the variables of the discriminant `e` are neither read nor written by the prefix, and the diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index 81f38fcad..0f729fb94 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -4,8 +4,6 @@ open EcParsetree open EcLocation open EcAst open EcModules -open EcFol -open EcPV open EcMatching.Position open EcCoreGoal open EcLowGoal @@ -17,133 +15,60 @@ type swap_kind = { } (* -------------------------------------------------------------------- *) -module LowInternal = struct - (* [exn] holds when the goal observes exceptions (a hoare goal whose - postcondition constrains some exception, see - [EcLowPhlGoal.hs_observes_exn]). Swapping two independent blocks - preserves the final state of the runs that terminate normally, but - not the state in which an exception is raised: if one of the blocks - raises, the other one has run (or not) before. Hence: - - blocks that contain a [raise] are never swapped; - - when the goal observes exceptions, blocks that may raise (through - a procedure call, see [EcLowPhlGoal.s_may_raise]) are not swapped - either. Otherwise, raising is as good as not terminating, which - the swap preserves. *) - let check_swap - (pf : proofenv) ~(exn : bool) (env : EcEnv.env) (s1 : stmt) (s2 : stmt) - = - let is_contains_raise = - let exception HasRaise in - - let rec i_contains_raise (i : instr) = - match i.i_node with - | Sraise _ -> raise HasRaise - | _ -> EcModules.i_iter i_contains_raise i in - - fun (s : stmt) -> - try - List.iter i_contains_raise s.s_node; - false - with HasRaise -> true in - - if List.exists is_contains_raise [s1; s2] then - tc_error pf "cannot swap blocks that contain exceptions"; - - if exn && List.exists (EcLowPhlGoal.s_may_raise env) [s1; s2] then - tc_error pf - "cannot swap blocks that may raise an exception \ - (through a procedure call) when the postcondition \ - constrains exceptions"; - - let m1,m2 = s_write env s1, s_write env s2 in - let r1,r2 = s_read env s1, s_read env s2 in - (* FIXME: this is not sufficient *) - let m2r1 = PV.interdep env m2 r1 in - let m1m2 = PV.interdep env m1 m2 in - let m1r2 = PV.interdep env m1 r2 in - - let error mode d = - tc_error_lazy pf (fun fmt -> - Format.fprintf fmt - "the two statements are not independent, %t" - (fun fmt -> - let (s1, s2) = - match mode with - | `RW -> "reads" , "written" - | `WR -> "writes", "read" - | `WW -> "writes", "written" - in - Format.fprintf fmt - "the first statement %s %a which is %s by the second" - s1 (PV.pp env) d s2)) - in - if not (PV.is_empty m2r1) then error `RW m2r1; - if not (PV.is_empty m1m2) then error `WW m1m2; - if not (PV.is_empty m1r2) then error `WR m1r2 - - - let swap_stmt - (pf : proofenv ) - ~(exn : bool ) - (env : EcEnv.env ) - (info : swap_kind ) - (s : stmt ) - = - let zpr, _, (_, (start, fin)) = try - EcMatching.Zipper.zipper_and_split_of_cgap_range env info.interval s - with InvalidCPos -> - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval - ) - in - - let env = odfl env zpr.z_env in - let s = stmt (List.rev_append zpr.z_head zpr.z_tail) in - - let target = try - resolve_gap_offset env (start, fin) info.offset s - with InvalidCPos -> - tc_error pf "invalid offset for swap" - in - - match split_by_nmcgaps - (if target <= start - then [target; start; fin] - else [start; fin; target] - ) s - with - | [hd; s1; s2; tl] -> check_swap pf ~exn env (stmt s1) (stmt s2); - EcMatching.Zipper.zip - { zpr with z_head = []; z_tail = List.flatten [hd; s2; s1; tl] } - | _ -> assert false -end - -(* -------------------------------------------------------------------- *) -let t_swap_r (side : oside) (info : swap_kind) (tc : tcenv1) = - let env = FApi.tc1_env tc in - let _, stmt = EcLowPhlGoal.tc1_get_stmt side tc in - let exn = - match (FApi.tc1_goal tc).f_node with - | FhoareS hs -> EcLowPhlGoal.hs_observes_exn (hs_po hs) - | _ -> false in - let stmt = LowInternal.swap_stmt !!tc ~exn env info stmt in - FApi.xmutate1 tc `Swap [EcLowPhlGoal.hl_set_stmt side (FApi.tc1_goal tc) stmt] +(* [swap] is derived in every logic: the positions are resolved here + (failing as before the migration when they are invalid), then the + [swap] program transformation ([EcTrSwap], which checks the + independence of the exchanged statements) is applied through the + transformation rule of the logic. The derived tactic is the same in + every logic, hence a single dispatcher on the goal kind. *) +let resolve_swap (pf : proofenv) (env : EcEnv.env) (info : swap_kind) (s : stmt) = + let zpr, _, (path, (start, fin)) = try + EcMatching.Zipper.zipper_and_split_of_cgap_range env info.interval s + with InvalidCPos -> + tc_error_lazy pf (fun fmt -> + let ppe = EcPrinting.PPEnv.ofenv env in + Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval + ) + in + + let env = odfl env zpr.z_env in + let s = stmt (List.rev_append zpr.z_head zpr.z_tail) in + + let target = try + resolve_gap_offset env (start, fin) info.offset s + with InvalidCPos -> + tc_error pf "invalid offset for swap" + in + + EcTrSwap.TrSwap { trsw_range = (path, (start, fin)); trsw_target = target; } (* -------------------------------------------------------------------- *) -let t_swap = FApi.t_low2 "swap" t_swap_r +let t_swap (side : oside) (info : swap_kind) (tc : tcenv1) = + let _, s = EcLowPhlGoal.tc1_get_stmt side tc in + let tr = resolve_swap !!tc (FApi.tc1_env tc) info s in + 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 + | Some side, FequivS _ -> + EcEquivTransform.t_equiv_transform { etr_side = side; etr_tr = tr } tc + | _ -> assert false (* -------------------------------------------------------------------- *) let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) = let side, pos = info.pl_desc in let concl = FApi.tc1_goal tc in - if is_equivS concl && Option.is_none side then + match side, concl.f_node with + | None, FequivS _ -> FApi.t_seq (process_swap1 { info with pl_desc = (Some `Left , pos)}) (process_swap1 { info with pl_desc = (Some `Right, pos)}) tc - else + | _ -> let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in let env = EcEnv.Memory.push_active_ss me (FApi.tc1_env tc) in diff --git a/src/phl/rules/bdhoare/ecBdHoareTransform.ml b/src/phl/rules/bdhoare/ecBdHoareTransform.ml index 70a24b68c..daa1763de 100644 --- a/src/phl/rules/bdhoare/ecBdHoareTransform.ml +++ b/src/phl/rules/bdhoare/ecBdHoareTransform.ml @@ -32,6 +32,7 @@ let bdhoare_transform_subgoals trc_env = env; trc_me = bhs.bhs_m; trc_post = lazy (EcPV.PV.fv env m (bhs_po bhs).inv); + trc_exn = false; } in let r = apply ctxt n.btr_tr bhs.bhs_s in let obligation = function diff --git a/src/phl/rules/ecPlTransform.ml b/src/phl/rules/ecPlTransform.ml index 97245cce9..730b750da 100644 --- a/src/phl/rules/ecPlTransform.ml +++ b/src/phl/rules/ecPlTransform.ml @@ -21,6 +21,7 @@ type tr_ctxt = { trc_env : env; trc_me : memenv; trc_post : EcPV.PV.t Lazy.t; + trc_exn : bool; } type tr_result = { diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index ed52d2b69..34783ccde 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -33,7 +33,8 @@ open EcEnv (deciding a [match], its unframed form), [EcTrIfPush] and [EcTrMatchPush] (pushing the continuation of a leading conditional / [match] into its branches; the [if] and [match] tactics are push + rule - on the conditional alone). Entries live in [rules/transforms/], as + on the conditional alone), [EcTrSwap] (moving a block of a possibly + nested block). Entries live in [rules/transforms/], as [EcTr]. The framed form of [match C k] changes the precondition: it is not a transformation, but a separate rule of each logic ([EcRMatch]). *) @@ -65,6 +66,12 @@ type tr_ctxt = { trc_post : EcPV.PV.t Lazy.t; (* program variables of [trc_me] read by the postcondition (for hoare, including the exceptional ones) *) + trc_exn : bool; (* the judgement observes exceptions: + a hoare postcondition constraining + some exception + ([EcLowPhlGoal.hs_observes_exn]); + otherwise, raising is as good as + not terminating *) } (* The result of an entry: the (possibly extended) memory, the diff --git a/src/phl/rules/ehoare/ecEHoareTransform.ml b/src/phl/rules/ehoare/ecEHoareTransform.ml index 2eb92eba4..a1974e9b6 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.ml +++ b/src/phl/rules/ehoare/ecEHoareTransform.ml @@ -33,6 +33,7 @@ let ehoare_transform_subgoals trc_env = env; trc_me = hs.ehs_m; trc_post = lazy (EcPV.PV.fv env m (ehs_po hs).inv); + trc_exn = false; } in let r = apply ctxt n.ehtr_tr hs.ehs_s in let pre () = diff --git a/src/phl/rules/equiv/ecEquivTransform.ml b/src/phl/rules/equiv/ecEquivTransform.ml index aa2b6e26b..b23c0db71 100644 --- a/src/phl/rules/equiv/ecEquivTransform.ml +++ b/src/phl/rules/equiv/ecEquivTransform.ml @@ -40,6 +40,7 @@ let equiv_transform_subgoals trc_env = env; trc_me = me; trc_post = lazy (EcPV.PV.fv env m (es_po es).inv); + trc_exn = false; } in let r = apply ctxt n.etr_tr s in let ts_inv_lower_side2 = diff --git a/src/phl/rules/hoare/ecHoareTransform.ml b/src/phl/rules/hoare/ecHoareTransform.ml index 294f724f9..2e11e6608 100644 --- a/src/phl/rules/hoare/ecHoareTransform.ml +++ b/src/phl/rules/hoare/ecHoareTransform.ml @@ -33,6 +33,7 @@ let hoare_transform_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_trans trc_post = lazy (POE.fold (fun fv f -> EcPV.PV.union fv (EcPV.PV.fv env m f)) EcPV.PV.empty po.hsi_inv); + trc_exn = hs_observes_exn po; } in let r = apply ctxt n.htr_tr hs.hs_s in let obligation = function diff --git a/src/phl/rules/transforms/ecTrSwap.ml b/src/phl/rules/transforms/ecTrSwap.ml new file mode 100644 index 000000000..f22da128a --- /dev/null +++ b/src/phl/rules/transforms/ecTrSwap.ml @@ -0,0 +1,108 @@ +(* -------------------------------------------------------------------- *) +open EcModules +open EcPV +open EcMatching.Position +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the [swap] transformation, resolved: the block to move is + an integer gap range of the (possibly nested) block at a normalized + path, and its destination an integer gap of that block. *) +type tr_swap = { + trsw_range : nm_codegap_range; + trsw_target : nm_codegap1; +} + +type EcPlTransform.transform += TrSwap of tr_swap + +(* -------------------------------------------------------------------- *) +(* The two adjacent statements [s1; s2] can be exchanged: neither raises, + and neither reads nor writes what the other writes. Swapping two + independent blocks preserves the final state of the runs that + terminate normally, but not the state in which an exception is + raised: if one of the blocks raises, the other one has run (or not) + before. Hence blocks that contain a [raise] are never swapped, and, + when the judgement observes exceptions ([exn]), neither are blocks + that may raise (through a procedure call, + [EcLowPhlGoal.s_may_raise]). Otherwise, raising is as good as not + terminating, which the swap preserves. *) +let check_swap ~(exn : bool) (env : EcEnv.env) (s1 : stmt) (s2 : stmt) = + let is_contains_raise = + let exception HasRaise in + + let rec i_contains_raise (i : instr) = + match i.i_node with + | Sraise _ -> raise HasRaise + | _ -> EcModules.i_iter i_contains_raise i in + + fun (s : stmt) -> + try + List.iter i_contains_raise s.s_node; + false + with HasRaise -> true in + + if List.exists is_contains_raise [s1; s2] then + raise (InvalidTransform "cannot swap blocks that contain exceptions"); + + if exn && List.exists (EcLowPhlGoal.s_may_raise env) [s1; s2] then + raise (InvalidTransform + "cannot swap blocks that may raise an exception \ + (through a procedure call) when the postcondition \ + constrains exceptions"); + + let m1,m2 = s_write env s1, s_write env s2 in + let r1,r2 = s_read env s1, s_read env s2 in + (* FIXME: this is not sufficient *) + let m2r1 = PV.interdep env m2 r1 in + let m1m2 = PV.interdep env m1 m2 in + let m1r2 = PV.interdep env m1 r2 in + + let error mode d = + let (s1, s2) = + match mode with + | `RW -> "reads" , "written" + | `WR -> "writes", "read" + | `WW -> "writes", "written" + in + raise (InvalidTransform (Format.asprintf + "the two statements are not independent, %t" + (fun fmt -> + Format.fprintf fmt + "the first statement %s %a which is %s by the second" + s1 (PV.pp env) d s2))) + in + if not (PV.is_empty m2r1) then error `RW m2r1; + if not (PV.is_empty m1m2) then error `WW m1m2; + if not (PV.is_empty m1r2) then error `WR m1r2 + +(* -------------------------------------------------------------------- *) +(* Move the block [c[start..fin)] of the block at [path] to the gap + [target] of that block, outside of the moved block, checking that it is + independent of the instructions it is exchanged with. *) +let swap (p : tr_swap) (ctxt : tr_ctxt) (s : stmt) = + let (path, (start, fin)), target = p.trsw_range, p.trsw_target in + let zpr = + try EcMatching.Zipper.zipper_of_nm_cgap ctxt.trc_env (path, start) s + with InvalidCPos -> raise (InvalidTransform "invalid range for swap") in + let env = EcUtils.odfl ctxt.trc_env zpr.z_env in + let s = stmt (List.rev_append zpr.z_head zpr.z_tail) in + + let gaps = + if not (start <= fin && fin <= List.length s.s_node) + then raise (InvalidTransform "invalid range for swap") + else if 0 <= target && target <= start then [target; start; fin] + else if fin <= target && target <= List.length s.s_node then [start; fin; target] + else raise (InvalidTransform "invalid offset for swap") in + + match split_by_nmcgaps gaps s with + | [hd; s1; s2; tl] -> + check_swap ~exn:ctxt.trc_exn env (stmt s1) (stmt s2); + let s = EcMatching.Zipper.zip + { zpr with z_head = []; z_tail = List.flatten [hd; s2; s1; tl] } in + { trr_me = ctxt.trc_me; trr_s = s; trr_obl = []; } + | _ -> assert false + +let () = + register (function + | TrSwap p -> Some (swap p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrSwap.mli b/src/phl/rules/transforms/ecTrSwap.mli new file mode 100644 index 000000000..29cc8bde0 --- /dev/null +++ b/src/phl/rules/transforms/ecTrSwap.mli @@ -0,0 +1,35 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_swap = { + trsw_range : nm_codegap_range; (* block [p : [s..f)] to move (resolved) *) + trsw_target : nm_codegap1; (* its destination gap t (resolved) *) +} + +(* [TrSwap { trsw_range = (p, (s, f)); trsw_target = t }] — moves the + block [b = d[s..f)] of the block [d] at the (possibly nested) path [p] + of [c] (the body of a [while], a branch of an [if] or of a [match]) to + the gap [t] of [d], outside of [b] ([t <= s] or [f <= t]); the rest of + [c] is unchanged: + + d = hd; d1; b; tl ~~> d' = hd; b; d1; tl (t <= s, d1 = d[t..s)) + d = hd; b; d2; tl ~~> d' = hd; d2; b; tl (f <= t, d2 = d[f..t)) + + Side conditions: neither [b] nor [d1] / [d2] contains a [raise] + (otherwise fails with "cannot swap blocks that contain exceptions"); + when the judgement observes exceptions (the context's [trc_exn]), + neither may raise through a procedure call + ([EcLowPhlGoal.s_may_raise]; otherwise fails with "cannot swap blocks + that may raise an exception (through a procedure call) when the + postcondition constrains exceptions"); and the two exchanged statements are independent: the first one reads + nothing the second one writes, they write nothing in common, and the + first one writes nothing the second one reads (checked in this order, + failing with "the two statements are not independent, the first + statement reads / writes X which is written / read by the second"). + Fails with "invalid range for swap" / "invalid offset for swap" when + the positions are not valid for [c]. No obligation, the memory is + unchanged. *) +type EcPlTransform.transform += TrSwap of tr_swap diff --git a/tests/swap.ec b/tests/swap.ec new file mode 100644 index 000000000..7ebcbf13f --- /dev/null +++ b/tests/swap.ec @@ -0,0 +1,382 @@ +(* The `swap` program transformation, through the transformation rule of + each logic: hoare (with exceptional postconditions), ehoare, phoare and + equiv (each side, and both sides at once), at the top level and in + nested blocks (branches of an `if`, body of a `while`, arm of a + `match`), with relative and absolute offsets, the derived `interleave`, + and the error paths. Each tactic is a separate sentence, so that the + goals it leaves can be compared across builds. *) +require import AllCore Xreal. + +exception e. + +module M = { + var x, y, z, w : int + + proc f() : unit = { + x <- 1; + y <- 2; + z <- 3; + w <- 4; + } + + proc c(b : bool) : unit = { + if (b) { + x <- 1; + y <- 2; + z <- 3; + } else { + y <- 5; + x <- 6; + } + w <- 0; + } + + proc l() : unit = { + x <- 0; + while (x < 10) { + y <- 1; + z <- 2; + x <- x + 1; + } + } + + proc n(b : bool) : unit = { + if (b) { + while (x < 10) { + y <- 1; + z <- 2; + x <- x + 1; + } + } + } + + proc m(o : int option) : unit = { + match o with + | None => { x <- 0; y <- 1; } + | Some v => { x <- v; y <- v + 1; z <- 2; } + end; + } + + proc d() : unit = { + x <- 1; + y <- x; + x <- 2; + z <- 3; + } + + proc nd(o : int option) : unit = { + match o with + | None => { x <- 0; } + | Some v => { x <- v; y <- x; } + end; + while (x < 3) { + x <- x + 1; + y <- x; + } + } + + proc r() : unit = { + x <- 1; + raise e; + y <- 2; + } +}. + +module N = { + proc f() : unit = { + M.w <- 4; + M.z <- 3; + M.y <- 2; + M.x <- 1; + } + + proc c(b : bool) : unit = { + if (b) { + M.z <- 3; + M.y <- 2; + M.x <- 1; + } else { + M.x <- 6; + M.y <- 5; + } + M.w <- 0; + } +}. + +(* -------------------------------------------------------------------- *) +(* hoare *) +lemma h_top : hoare [M.f : true ==> M.x = 1 /\ M.y = 2 /\ M.z = 3 /\ M.w = 4]. +proof. +proc. +swap 1 1. +swap 4 -2. +swap [1..2] 2. +swap [3..4] -2. +swap 1 @3. +swap 2. +swap -1. +auto. +qed. + +lemma h_exc : + hoare [M.f : true ==> M.x = 1 /\ M.y = 2 | e => M.w = 4]. +proof. +proc. +swap 1 3. +swap [1..2] 1. +auto. +qed. + +lemma h_if : hoare [M.c : true ==> M.w = 0]. +proof. +proc. +swap 1.:[1..1] 1. +swap 1.3 -2. +swap 1?1 1. +swap 1.:[2..3] -1. +auto. +qed. + +lemma h_while : hoare [M.l : true ==> 10 <= M.x]. +proof. +proc. +swap 2.:[1..1] 1. +swap 2.3 -2. +while (true). +- by auto. +by auto => /#. +qed. + +lemma h_nested : hoare [M.n : true ==> true]. +proof. +proc. +swap 1.1.1 1. +swap 1.1.:[2..3] -1. +swap 1.1.3 @1. +by auto; while (true); auto. +qed. + +lemma h_match : hoare [M.m : true ==> true]. +proof. +proc. +swap 1#Some.1 1. +swap 1#Some.:[2..3] -1. +swap 1#None.1 1. +by auto. +qed. + +lemma h_errors : hoare [M.d : true ==> true]. +proof. +proc. +(* not independent: reads / writes / writes what the other writes / reads *) +fail swap 2 1. +fail swap 1 2. +fail swap 1 1. +fail swap 2 -1. +fail swap 3 -1. +(* invalid ranges and offsets *) +fail swap [3..1] 1. +fail swap [1..5] 1. +fail swap 5 1. +fail swap 1 5. +fail swap 4 -4. +fail swap [1..2] @2. +fail swap [1..2] @9. +fail swap @2. +fail swap 1.1 1. +fail swap 1?:[1..1] 1. +(* sided swap on a non-equiv goal *) +fail swap{1} 1 1. +fail swap{2} 1 1. +swap 4 -1. +abort. + +lemma h_nested_errors : hoare [M.nd : true ==> true]. +proof. +proc. +fail swap 1#Some.1 1. +fail swap 1#Some.2 -1. +fail swap 2.2 -1. +fail swap 2.:[1..2] 1. +fail swap 2?1 1. +fail swap 1#None.1 1. +abort. + +lemma h_raise : hoare [M.r : true ==> true | e => true]. +proof. +proc. +fail swap 1 1. +fail swap 2 1. +fail swap 3 -1. +fail swap [1..2] 1. +abort. + +(* -------------------------------------------------------------------- *) +(* ehoare *) +lemma eh_top : ehoare [M.f : 1%xr ==> (M.x = 1 /\ M.w = 4)%xr]. +proof. +proc. +swap 1 1. +swap [3..4] -2. +fail swap{1} 1 1. +auto. +qed. + +lemma eh_nested : ehoare [M.c : 1%xr ==> (M.w = 0)%xr]. +proof. +proc. +swap 1.1 1. +swap 1?:[1..1] 1. +fail swap 1.1 @4. +auto. +qed. + +lemma eh_errors : ehoare [M.d : 1%xr ==> 1%xr]. +proof. +proc. +fail swap 1 1. +fail swap 2 -1. +fail swap [1..3] 2. +abort. + +(* -------------------------------------------------------------------- *) +(* phoare *) +lemma ph_top : phoare [M.f : true ==> M.x = 1 /\ M.w = 4] = 1%r. +proof. +proc. +swap 1 1. +swap [3..4] -2. +fail swap{2} 1 1. +auto. +qed. + +lemma ph_le : phoare [M.c : true ==> M.w = 0] <= 1%r. +proof. +proc. +swap 1.:[1..2] 1. +swap 1?1 1. +auto. +qed. + +lemma ph_ge : phoare [M.l : true ==> true] >= 0%r. +proof. +proc. +swap 2.1 1. +auto. +qed. + +lemma ph_errors : phoare [M.d : true ==> true] = 1%r. +proof. +proc. +fail swap 1 1. +fail swap 2 -1. +fail swap 1.1 1. +abort. + +(* -------------------------------------------------------------------- *) +(* equiv *) +lemma e_sides : equiv [M.f ~ N.f : true ==> ={M.x, M.y, M.z, M.w}]. +proof. +proc. +swap{1} 1 3. +swap{2} 4 -3. +swap{1} [1..2] 2. +swap{2} [3..4] -2. +swap{1} 1 @4. +swap{2} -1. +auto. +qed. + +lemma e_both : equiv [M.f ~ M.f : true ==> ={M.x, M.y, M.z, M.w}]. +proof. +proc. +swap 1 1. +swap [2..3] 1. +swap 4 -3. +sim. +qed. + +lemma e_nested : equiv [M.c ~ N.c : ={b} ==> ={M.x, M.y, M.w}]. +proof. +proc. +swap{1} 1.:[1..2] 1. +swap{1} 1.1 1. +swap{2} 1?1 1. +swap{1} 1?1 1. +swap{2} 1.1 1. +swap{2} 1.3 -1. +by auto => /#. +qed. + +lemma e_loop : equiv [M.l ~ M.l : ={M.y, M.z} ==> ={M.x, M.y, M.z}]. +proof. +proc. +swap{1} 2.1 1. +swap{2} 2.2 -1. +sim. +qed. + +lemma e_loop_nested : equiv [M.n ~ M.n : ={b, M.x, M.y, M.z} ==> ={M.x, M.y, M.z}]. +proof. +proc. +swap{1} 1.1.1 1. +swap{2} 1.1.:[2..2] -1. +sim. +qed. + +lemma e_match : equiv [M.m ~ M.m : ={o, M.z} ==> ={M.x, M.y, M.z}]. +proof. +proc. +swap{1} 1#Some.1 1. +swap{2} 1#Some.:[2..2] -1. +swap 1#None.1 1. +sim. +qed. + +lemma e_errors : equiv [M.d ~ M.r : true ==> true]. +proof. +proc. +fail swap{1} 1 1. +fail swap{1} 2 -1. +fail swap{1} [1..5] 1. +fail swap{1} 1 @1. +fail swap{2} 1 1. +fail swap{2} 3 -1. +fail swap{2} 1.1 1. +fail swap 1 1. +abort. + +(* -------------------------------------------------------------------- *) +(* interleave (derived: a sequence of swaps) *) +module I = { + var a, b, c, d : int + + proc f() : unit = { + a <- 1; + b <- 2; + c <- 3; + d <- 4; + } + + proc g() : unit = { + a <- 1; + c <- 3; + b <- 2; + d <- 4; + } +}. + +lemma h_interleave : hoare [I.f : true ==> I.a = 1 /\ I.d = 4]. +proof. +proc. +interleave [1:1] [3:1] 2. +auto. +qed. + +lemma e_interleave : equiv [I.f ~ I.g : true ==> ={I.a, I.b, I.c, I.d}]. +proof. +proc. +interleave{1} [1:1] [3:1] 2. +fail interleave{2} [3:1] [1:1] 1. +sim. +qed.