diff --git a/examples/global-hybrid/GlobalHybridExamp2.ec b/examples/global-hybrid/GlobalHybridExamp2.ec index db248c762..89a74d337 100644 --- a/examples/global-hybrid/GlobalHybridExamp2.ec +++ b/examples/global-hybrid/GlobalHybridExamp2.ec @@ -416,7 +416,7 @@ rcondf{1} 1; first auto. rcondf{2} 1; first auto; smt(). rcondt{2} 1; first auto. wp; inline*. -swap{2} 2 -1; swap{2} 6 -4; swap{2} 10 -7. +swap{2} 2 -1; swap{2} 6 -4. seq 2 3 : (#pre /\ x{1} = r0{2} /\ y{1} = r1{2} /\ x0{2} = A); first auto. diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index 5f3e239dc..dc8986959 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -68,10 +68,17 @@ module type PrinterAPI = sig val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp (* ------------------------------------------------------------------ *) - val pp_codepos1 : PPEnv.t -> EcMatching.Position.codepos1 pp - val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp - - val pp_codepos : PPEnv.t -> EcMatching.Position.codepos pp + val pp_codepos1 : PPEnv.t -> EcMatching.Position.codepos1 pp + val pp_codepos_brsel : EcMatching.Position.codepos_brsel pp + val pp_codepos_step : PPEnv.t -> EcMatching.Position.codepos_step pp + val pp_codepos_path : PPEnv.t -> EcMatching.Position.codepos_path pp + val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp + + val pp_codepos : PPEnv.t -> EcMatching.Position.codepos pp + val pp_codegap1 : PPEnv.t -> EcMatching.Position.codegap1 pp + val pp_codegap : PPEnv.t -> EcMatching.Position.codegap pp + val pp_codegap1_range : PPEnv.t -> EcMatching.Position.codegap1_range pp + val pp_codegap_range : PPEnv.t -> EcMatching.Position.codegap_range pp (* ------------------------------------------------------------------ *) type vsubst = [ diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 86338c5af..e749a0f03 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -238,11 +238,15 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = try tx tc with (* PHL Specific low errors *) - | EcLowPhlGoal.InvalidSplit cpos1 -> + | EcLowPhlGoal.InvalidSplit is -> tc_error_lazy !!tc (fun fmt -> let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in Format.fprintf fmt "invalid split index: %a" - (EcPrinting.pp_codepos1 ppe) cpos1) + (fun fmt is -> match is with + | `Gap gap -> Format.fprintf fmt "%a" EcPrinting.(pp_codegap1 ppe) gap + | `Instr i -> Format.fprintf fmt "%a" EcPrinting.(pp_codepos1 ppe) i + ) is) + (* -------------------------------------------------------------------- *) and process_sub (ttenv : ttenv) tts tc = diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 07bc36471..4d2d0aaa3 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -207,11 +207,18 @@ let tc1_get_stmt side tc = tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc (* ------------------------------------------------------------------ *) -let tc1_process_codepos_range tc (side, cpr) = +let tc1_process_codepos_or_range tc (side, cpor) = let me, _ = tc1_get_stmt side tc in let env = FApi.tc1_env tc in let env = EcEnv.Memory.push_active_ss me env in - EcTyping.trans_codepos_range env cpr + EcTyping.trans_codepos_or_range env cpor + +(* ------------------------------------------------------------------ *) +let tc1_process_codegap_range tc (side, cgr) = + let me, _ = tc1_get_stmt side tc in + let env = FApi.tc1_env tc in + let env = EcEnv.Memory.push_active_ss me env in + EcTyping.trans_codegap_range env cgr (* ------------------------------------------------------------------ *) let tc1_process_codepos tc (side, cpos) = @@ -379,22 +386,37 @@ let logicS_post_read (env : env) (f : logicS) = add EcPV.PMVS.empty (es_po es).inv (* -------------------------------------------------------------------- *) -exception InvalidSplit of codepos1 +exception InvalidSplit of [ `Instr of codepos1 | `Gap of codegap1 ] + let s_split env i s = - let module Zpr = EcMatching.Zipper in - try Zpr.split_at_cpos1 env i s - with Zpr.InvalidCPos -> raise (InvalidSplit i) + let module Pos = EcMatching.Position in + try Pos.split_at_cgap1 env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) let s_split_i env i s = - let module Zpr = EcMatching.Zipper in - try Zpr.find_by_cpos1 ~rev:false env i s - with Zpr.InvalidCPos -> raise (InvalidSplit i) + let module Pos = EcMatching.Position in + try Pos.find_by_cpos1 ~rev:false env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Instr i)) let o_split ?rev env i s = - let module Zpr = EcMatching.Zipper in - try Zpr.may_split_at_cpos1 ?rev env i s - with Zpr.InvalidCPos -> raise (InvalidSplit (oget i)) + let module Pos = EcMatching.Position in + try Pos.may_split_at_cgap1 ?rev env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap(oget i))) + +(* -------------------------------------------------------------------- *) +(* Gap processing functions *) +let tc1_process_codegap1 tc (side, g) = + let me, _ = tc1_get_stmt side tc in + let env = FApi.tc1_env tc in + let env = EcEnv.Memory.push_active_ss me env in + EcTyping.trans_codegap1 env g + +let tc1_process_codegap tc (side, g) = + let me, _ = tc1_get_stmt side tc in + let env = FApi.tc1_env tc in + let env = EcEnv.Memory.push_active_ss me env in + EcTyping.trans_codegap env g (* -------------------------------------------------------------------- *) let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc = @@ -740,14 +762,14 @@ let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) = 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 Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position" + 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 Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position" + with InvalidCPos -> tc_error (fst cenv) "invalid code position" let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = let pf = FApi.tc1_penv tc in diff --git a/src/ecMatching.ml b/src/ecMatching.ml index a14e8859b..30e644878 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -28,15 +28,87 @@ module Position = struct and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ] type cp_base = [ - | `ByPos of int + | `ByPos of int (* Always <> 0 *) | `ByMatch of int option * cp_match ] - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] - type codepos1 = int * cp_base - type codepos = (codepos1 * codepos_brsel) list * codepos1 - type codepos_range = codepos * [`Base of codepos | `Offset of codepos1] - type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1] + exception InvalidCPos + + (* Code positions and code gaps: + + A block of n instructions has: + - n positions (0-indexed), each pointing AT an instruction + - n+1 gaps (0-indexed), each pointing BETWEEN instructions + + gap 0 | instr 0 | gap 1 | instr 1 | gap 2 | ... | instr n-1 | gap n + + Positions (nm_codepos1): 0-indexed, range [0, n-1] + Gaps (nm_codegap1): 0-indexed, range [0, n] + gap k = before instruction k (= after instruction k-1) + gap 0 = start of block, gap n = end of block + + Conversions: + gap_before(pos) = pos (* gap immediately before instruction pos *) + gap_after(pos) = pos + 1 (* gap immediately after instruction pos *) + instr_after(gap) = gap (* instruction immediately after gap; requires gap < n *) + instr_before(gap) = gap - 1 (* instruction immediately before gap; requires gap > 0 *) + + Ranges are pairs of gaps (g1, g2) containing instructions g1, g1+1, ..., g2-1. + User writes [a..b] (1-indexed, closed-closed), which translates to + gap pair (a-1, b) in 0-indexed representation. + + Tactics that split code take gaps (seq, wp, sp, fel, sim/eqobs). + Tactics that target instructions take positions (kill, alias, set, cfold, + proc change, fission, fusion, unroll, inline, call, cond). + Swap takes a range (gap pair) + a gap offset. + + Pre-normalization code positions (codepos1) use user syntax (1-indexed, + possibly negative, possibly match-based). Normalization resolves them + to 0-indexed nm_codepos1 values. + *) + + (* Branch selection *) + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type nm_codepos_brsel = [`Cond of bool | `Match of int] + (* Linear code position inside a block *) + type codepos1 = int * cp_base + (* Normalized code position inside a block, always > 0 *) + type nm_codepos1 = int + (* Codeposition path step *) + type codepos_step = (codepos1 * codepos_brsel) + type nm_codepos_step = (nm_codepos1 * nm_codepos_brsel) + (* Block selection by codepos + branch selection *) + type codepos_path = codepos_step list + type nm_codepos_path = nm_codepos_step list + (* Full codeposition = path to block + position in block *) + type codepos = codepos_path * codepos1 + type nm_codepos = nm_codepos_path * nm_codepos1 + (* Code position offset *) + type codeoffset1 = [`Relative of int | `Absolute of codepos1] + + (* --- Gap types --- *) + (* Normalized gap inside a block, 0-indexed, range [0, n] *) + type nm_codegap1 = int + (* Typed but unnormalized gap *) + type codegap1 = + | GapBefore of codepos1 (* gap immediately before this instruction *) + | GapAfter of codepos1 (* gap immediately after this instruction *) + (* Full gap with path *) + type codegap = codepos_path * codegap1 + (* Normalized gap with path *) + type nm_codegap = nm_codepos_path * nm_codegap1 + (* Gap-based range *) + type codegap1_range = codegap1 * codegap1 + type nm_codegap1_range = nm_codegap1 * nm_codegap1 + type codegap_range = codepos_path * codegap1_range + type nm_codegap_range = nm_codepos_path * nm_codegap1_range + (* Gap-based offset for swap *) + type codegap_offset1 = + | GapAbsolute of codegap1 + | GapRelative of int + + let cpos1 (i: int) : codepos1 = + (0, `ByPos i) let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = (o + offset, p) @@ -44,51 +116,126 @@ module Position = struct let shift ~(offset : int) ((outp, p) : codepos) : codepos = (outp, shift1 ~offset p) + let cpos1_first : codepos1 = cpos1 0 + let cpos1_last : codepos1 = cpos1 (-1) + + (* Boundary gap constructors *) + let codegap1_start : codegap1 = GapBefore cpos1_first + let codegap1_end : codegap1 = GapAfter cpos1_last + let codegap_start : codegap = ([], codegap1_start) + let codegap_end : codegap = ([], codegap1_end) + + (* Convenience constructors *) + let gap_before_pos (cp : codepos1) : codegap1 = GapBefore cp + let gap_after_pos (cp : codepos1) : codegap1 = GapAfter cp + + (* Gap -> instr *) + let instr_before_gap (cg : codegap1) : codepos1 = + match cg with + | GapAfter cp -> cp + | GapBefore cp -> shift1 ~offset:(-1) cp + + let instr_after_gap (cg : codegap1) : codepos1 = + match cg with + | GapAfter cp -> shift1 ~offset:1 cp + | GapBefore cp -> cp + + (* Position <-> Gap conversions (normalized, 0-indexed) *) + let gap_before (pos : nm_codepos1) : nm_codegap1 = pos + let gap_after (pos : nm_codepos1) : nm_codegap1 = pos + 1 + let instr_after (gap : nm_codegap1) : nm_codepos1 = gap (* requires gap < n *) + let instr_before (gap : nm_codegap1) : nm_codepos1 = gap - 1 (* requires gap > 0 *) + + (* Single-instruction range as gap pair *) + let gap_range_of_pos (pos : nm_codepos1) : nm_codegap1_range = + (gap_before pos, gap_after pos) + + let gap_range_of_cpos ((path, pos) : nm_codepos) : nm_codegap_range = + (path, gap_range_of_pos pos) + + (* Gap counting helpers *) + let gap_after_n (n : int) : codegap1 = GapAfter (0, `ByPos (n-1)) + let gap_before_n (n : int) : codegap1 = GapBefore (0, `ByPos (n-1)) + let gap_after_last_n (n : int) : codegap1 = GapAfter (0, `ByPos (-n)) + let gap_before_last_n(n : int) : codegap1 = GapBefore (0, `ByPos (-n)) + let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 = match offset with - | `ByPosition pos -> pos - | `ByOffset off -> (off + fst base, snd base) -end + | `Absolute pos -> pos + | `Relative off -> (off + fst base, snd base) -(* -------------------------------------------------------------------- *) -module Zipper = struct - open Position + let codegap1_range_of_codepos1 (cp1: codepos1) : codegap1_range = + (gap_before_pos cp1, gap_after_pos cp1) - exception InvalidCPos + let codegap_range_of_codepos ((cpath, cp1): codepos) : codegap_range = + (cpath, codegap1_range_of_codepos1 cp1) - module P = EcPath + let nm_codegap1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codegap1_range = + (gap_before cp1, gap_after cp1) - type ('a, 'state) folder = - env -> 'a -> 'state -> instr -> 'state * instr list + let nm_codegap_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codegap_range = + (cpath, nm_codegap1_range_of_nm_codepos1 cp1) - type ('a, 'state) folder_l = - env -> 'a -> 'state -> instr list -> 'state * instr list + let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = + (0, `ByPos nm) - type spath_match_ctxt = { - locals : (EcIdent.t * ty) list; - prebr : ((EcIdent.t * ty) list * stmt) list; - postbr : ((EcIdent.t * ty) list * stmt) list; - } + let cpos1_after_last : codepos1 = + (1, `ByPos (-1)) - type ipath = - | ZTop - | ZWhile of expr * spath - | ZIfThen of expr * spath * stmt - | ZIfElse of expr * stmt * spath - | ZMatch of expr * spath * spath_match_ctxt + let cpos1_to_top (cp1: codepos1) : codepos = + ([], cp1) - and spath = (instr list * instr list) * ipath + (* Top-level first instruction *) + let cpos_first : codepos = + cpos1_to_top cpos1_first - type zipper = { - z_head : instr list; (* instructions on my left (rev) *) - z_tail : instr list; (* instructions on my right (me incl.) *) - z_path : ipath; (* path (zipper) leading to me *) - z_env : env option; - } + let cpos_last : codepos = + cpos1_to_top cpos1_last - let cpos (i : int) : codepos1 = (0, `ByPos i) +(* FIXME: check if we need this + let codepos_step_of_nm_codepos_step ((cp1, brsel): nm_codepos_step) : codepos_step = + (codepos1_of_nm_codepos1 cp1, brsel) - let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; } + let codepos_path_of_nm_codepos_path (cpath: nm_codepos_path) : codepos_path = + List.map codepos_step_of_nm_codepos_step cpath + + let codepos_of_nm_codepos ((nmp, nmcp): nm_codepos) : codepos = + (codepos_path_of_nm_codepos_path nmp, codepos1_of_nm_codepos1 nmcp) +*) + + (* + Check that the ranges are valid and then: + if either is empty -> true + otherwise possibilities are: + 1. s1 <= s2 <= min(e1, e2) => false + 2. s1 <= e1 <= s2 <= e2 => true + 3. s2 <= s1 <= min(e1, e2) => false + 4. s2 <= e2 <= s1 <= e1 => true + *) + + let disjoint ((s1, e1): nm_codegap1_range) ((s2, e2): nm_codegap1_range) : bool = + if s1 > e1 || s2 > e2 then raise InvalidCPos; + (s1 = e1) || (s2 = e2) || (* Degenerate case where one of the reanges is empty *) + (max s1 s2 >= min e1 e2) (* Otherwise, intersection of (a, b) /\ (c, d) *) + (* = (max a c, min b d) *) + (* and this is empty if lower_lim >= upper_lim *) + + let nm_codepos1_in_nm_codegap1_range (cp: nm_codepos1) ((start, fin): nm_codegap1_range) : bool = + (start <= cp && cp < fin) + + module Notations = struct + let (|+>) (cp: codepos) (offset: int) = + shift ~offset cp + + let (+>) (cp1: codepos1) (offset: int) = + shift1 ~offset cp1 + + let (<+|) (cp: codepos) (i: int) = + shift ~offset:(-i) cp + + let (<+) (cp1: codepos1) (i: int) = + shift1 ~offset:(-i) cp1 + end let find_by_cp_match (env : EcEnv.env) @@ -147,144 +294,320 @@ module Zipper = struct match rev with | false -> (s1, ir, s2) - | true -> (s2, ir, s1) - - type after = [`Yes | `No | `Auto] - - let split_at_cp_base ~(after : after) (env : EcEnv.env) (cb : cp_base) (s : stmt) = - match cb with - | `ByPos i -> begin - let after = - match after with - | `Auto -> 0 <= i - | `Yes -> true - | `No -> false in - let i = if i < 0 then List.length s.s_node + i + 1 else i in - let i = i - if after then 0 else 1 in - try List.takedrop i s.s_node - with (Invalid_argument _ | Not_found) -> raise InvalidCPos - end + | true -> (List.rev s2, ir, List.rev s1) + + let exists_match (env: env) (cpm: cp_match) (s: stmt) : bool = + try + ignore (find_by_cp_match env (None, cpm) s); + true + with InvalidCPos -> false + + let find_by_nmcpos1 ?(rev = true) (nm: nm_codepos1) (s: stmt) = + let s1, i, s2 = try + List.pivot_at nm s.s_node + with (Invalid_argument _ | Not_found) -> raise InvalidCPos + in + (if rev then s1 else List.rev s1), i, s2 + + (* Throws InvalidCPos if failing — allows [0, n] where n is "after last" *) + let check_nm_cpos1 (nm: nm_codepos1) (s: stmt) : unit = + if nm < 0 || nm >= List.length s.s_node then raise InvalidCPos + (* Normalizes code position wrt stmt — input is 0-indexed *) + let normalize_cp_base ?(check = true) (env: EcEnv.env) (cb: cp_base) (s: stmt) : nm_codepos1 = + let nm = match cb with + | `ByPos i when i >= 0 -> i + | `ByPos i (* i < 0 *) -> (List.length s.s_node) + i | `ByMatch (i, cm) -> - let (s1, i, s2) = find_by_cp_match env (i, cm) s in + let (s1, _, _) = find_by_cp_match env (i, cm) s in + List.length s1 + in + if check then check_nm_cpos1 nm s; + nm + + let normalize_cpos1 ?(check = true) (env: EcEnv.env) ((off, cb): codepos1) (s: stmt) : nm_codepos1 = + let nm = off + normalize_cp_base ~check:false env cb s in + (* Make sure the position we are pointing to is valid in the context *) + (* List.length points to the position "after the last" and has + special meaning depending on the context *) + if check then check_nm_cpos1 nm s; + nm + + let find_and_normalize_cpos1 ?(rev = true) (env : EcEnv.env) (cp1 : codepos1) (s : stmt) = + let nm = normalize_cpos1 env cp1 s in + find_by_nmcpos1 ~rev nm s, nm + + let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cp1 : codepos1) (s : stmt) = + find_and_normalize_cpos1 ~rev env cp1 s |> fst + + (* Selects the index for match arm *) + let select_match_arm_idx (env:env) (e: expr) (sel: string) = + let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in + let indt = oget (EcDecl.tydecl_as_datatype indt) in + let cnames = List.fst indt.tydt_ctors in + try List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst + with Not_found -> raise InvalidCPos + + (* Get the block pointed to by brsel for a given instruction *) + let normalize_brsel (env: env) (i: instr) (br: codepos_brsel) : (env * stmt) * nm_codepos_brsel = + match i.i_node, br with + | (Sif (_, t, _), `Cond true) -> (env, t), `Cond true + | (Sif (_, _, f), `Cond false) -> (env, f), `Cond false + | (Swhile (_, s), `Cond true) -> (env, s), `Cond true + | (Smatch (e, ss), `Match ms) -> + let ix = select_match_arm_idx env e ms in + let (locals, s) = List.at ss ix in + let env = EcEnv.Var.bind_locals locals env in + begin try + (env, s), `Match ix + with Invalid_argument _ -> + raise InvalidCPos + end + | _ -> assert false - match after with - | `No -> (List.rev s1, i :: s2) - | _ -> (List.rev_append s1 [i], s2) + let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = + normalize_brsel env i br |> fst |> snd - let split_at_cpos1 ~after (env : EcEnv.env) ((ipos, cb) : codepos1) s = - let (s1, s2) = split_at_cp_base ~after env cb s in + (* Normalizes a code position step and returns the block it points to *) + let normalize_cpos_step (env: env) (s: stmt) ((cp1, brsel): codepos_step) : (env * stmt) * nm_codepos_step = + let (_, i, _), nm_cp1 = find_and_normalize_cpos1 env cp1 s in + let (env, s), nmbr = normalize_brsel env i brsel in + (env, s), (nm_cp1, nmbr) - let (s1, s2) = - match ipos with - | off when off > 0 -> - let (ss1, ss2) = - try List.takedrop off s2 - with (Invalid_argument _ | Not_found) -> raise InvalidCPos in - (s1 @ ss1, ss2) + let normalize_cpos_path (env: env) (cpath: codepos_path) (s: stmt) : (env * stmt) * nm_codepos_path = + List.fold_left_map (fun (env, s) step -> normalize_cpos_step env s step) (env, s) cpath - | off when off < 0 -> - let (ss1, ss2) = - try List.takedrop (List.length s1 + off) s1 - with (Invalid_argument _ | Not_found) -> raise InvalidCPos in - (ss1, ss2 @ s2) + let normalize_cpos (env: env) ((cpath, cp1) : codepos) (s: stmt) : (env * stmt) * nm_codepos = + let (env, s), npath = normalize_cpos_path env cpath s in + (env, s), (npath, normalize_cpos1 env cp1 s) - | _ -> (s1, s2) + 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 + | `Relative i -> + let nm = (base + i) in + check_nm_cpos1 nm s; nm - in (s1, s2) + (* --- Gap normalization and split functions --- *) - let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cpos1 : codepos1) (s : stmt) = - match split_at_cpos1 ~after:`No env cpos1 s with - | (s1, i :: s2) -> ((if rev then List.rev s1 else s1), i, s2) - | _ -> raise InvalidCPos + (* Check that a normalized gap is valid for the given statement *) + let check_nm_cgap1 (nm : nm_codegap1) (s : stmt) : unit = + if nm < 0 || nm > List.length s.s_node then raise InvalidCPos - let offset_of_position (env : EcEnv.env) (cpos : codepos1) (s : stmt) = - let (s, _) = split_at_cpos1 ~after:`No env cpos s in - 1 + List.length s + (* Normalize a codegap1 to nm_codegap1 *) + let normalize_cgap1 (env : env) (g : codegap1) (s : stmt) : nm_codegap1 = + let nm = match g with + | GapBefore cp -> normalize_cpos1 ~check:false env cp s |> gap_before + | GapAfter cp -> normalize_cpos1 ~check:false env cp s |> gap_after + in + check_nm_cgap1 nm s; nm + + (* Normalize a full codegap (with path) *) + let normalize_cgap (env : env) ((cpath, g1) : codegap) (s : stmt) : (env * stmt) * nm_codegap = + let (env, s), npath = normalize_cpos_path env cpath s in + (env, s), (npath, normalize_cgap1 env g1 s) + + (* Normalize a codegap1_range *) + let normalize_cgap1_range (env : env) ((g1, g2) : codegap1_range) (s : stmt) : nm_codegap1_range = + let nm1 = normalize_cgap1 env g1 s in + let nm2 = normalize_cgap1 env g2 s in + if nm1 > nm2 then raise InvalidCPos; + (nm1, nm2) + + (* Normalize a full codegap_range (with path) *) + let normalize_cgap_range (env : env) ((cpath, gr) : codegap_range) (s : stmt) : (env * stmt) * nm_codegap_range = + let (env, s), npath = normalize_cpos_path env cpath s in + let nmgr = normalize_cgap1_range env gr s in + (env, s), (npath, nmgr) + + (* Split at a normalized gap *) + let split_at_nmcgap1 (nm : nm_codegap1) (s : stmt) : instr list * instr list = + try List.takedrop nm s.s_node + with Invalid_argument _ -> raise InvalidCPos + + (* Split at a codegap1 *) + let split_at_cgap1 (env : env) (g : codegap1) (s : stmt) : instr list * instr list = + split_at_nmcgap1 (normalize_cgap1 env g s) s + + (* Split at a full codegap (with path) *) + let split_at_cgap (env : env) ((cpath, g1) : codegap) (s : stmt) : env * (instr list * instr list) = + let (env, s), _npath = normalize_cpos_path env cpath s in + env, split_at_cgap1 env g1 s + + (* Optional gap split *) + let may_split_at_cgap1 ?(rev = false) (env : env) (g : codegap1 option) (s : stmt) : instr list * instr list = + ofdfl + (fun () -> if rev then (s.s_node, []) else ([], s.s_node)) + (omap (fun g -> split_at_cgap1 env g s) g) + + (* Split by normalized gap range into (before, inside, after) *) + let split_by_nmcgap_range ((g1, g2) : nm_codegap1_range) (s : stmt) : instr list * instr list * instr list = + let before, rest = try List.takedrop g1 s.s_node + with Invalid_argument _ -> raise InvalidCPos in + let inside, after = try List.takedrop (g2 - g1) rest + with Invalid_argument _ -> raise InvalidCPos in + (before, inside, after) + + (* Split by a list of normalized gaps *) + let split_by_nmcgaps (gaps : nm_codegap1 list) (s : stmt) : instr list list = + let doit (prev, rest, acc) gap = + let seg, rest = try List.takedrop (gap - prev) rest + with (Invalid_argument _ | Not_found) -> raise InvalidCPos in + (gap, rest, seg :: acc) + in + let (_, last, segs) = List.fold_left doit (0, s.s_node, []) gaps in + List.rev (last :: segs) + + (* Resolve a gap offset relative to a gap range *) + let resolve_gap_offset (env : env) ((g1, g2) : nm_codegap1_range) (off : codegap_offset1) (s : stmt) : nm_codegap1 = + let nm = match off with + | GapAbsolute g -> + let nm = normalize_cgap1 env g s in + if g1 <= nm && nm <= g2 then raise InvalidCPos; nm + | GapRelative i -> + if i > 0 then g2 + i + else g1 + i + in + check_nm_cgap1 nm s; nm + + (* Semantic helpers for match-based finding *) + let find_last_match (env : env) (cm : cp_match) (s : stmt) = + find_by_cp_match env (Some (-1), cm) s + + let find_first_match (env : env) (cm : cp_match) (s : stmt) = + find_by_cp_match env (None, cm) s + + let find_nth_match (env : env) (n : int) (cm : cp_match) (s : stmt) = + find_by_cp_match env (Some n, cm) s + + (* [split_by_match env ~occ ~gap cm s] splits [s] at the gap before/after + the [occ]-th occurrence of [cm]. *) + let split_by_match (env : env) ~(occ : int) ~(gap : [`Before | `After]) (cm : cp_match) (s : stmt) = + let (s1, i, s2) = find_by_cp_match env (Some occ, cm) s in + match gap with + | `Before -> (s1, i :: s2) + | `After -> (s1 @ [i], s2) + + let gap_before_match (env : env) ~(occ : int) (cm : cp_match) (s : stmt) : nm_codegap1 = + let (s1, _, _) = find_by_cp_match env (Some occ, cm) s in + List.length s1 + + let gap_after_match (env : env) ~(occ : int) (cm : cp_match) (s : stmt) : nm_codegap1 = + let (s1, _, _) = find_by_cp_match env (Some occ, cm) s in + List.length s1 + 1 + + (* Block iteration helpers *) + let fold_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt) + (f : int -> nm_codegap1 -> nm_codegap1 -> 'a -> 'a) (init : 'a) : 'a = + let n = List.length s.s_node in + let rec aux idx g acc = + if g + block_size > n then acc + else aux (idx + 1) (g + block_size) (f idx g (g + block_size) acc) + in + aux 0 start init + + let iter_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt) + (f : int -> nm_codegap1 -> nm_codegap1 -> unit) : unit = + fold_blocks ~start ~block_size s (fun idx g1 g2 () -> f idx g1 g2) () +end + +(* -------------------------------------------------------------------- *) +module Zipper = struct + open Position + + module P = EcPath + + type ('a, 'state) folder = + env -> 'a -> 'state -> instr -> 'state * instr list + + type ('a, 'state) folder_l = + env -> 'a -> 'state -> instr list -> 'state * instr list + + type spath_match_ctxt = { + locals : (EcIdent.t * ty) list; + prebr : ((EcIdent.t * ty) list * stmt) list; + postbr : ((EcIdent.t * ty) list * stmt) list; + } + + type ipath = + | ZTop + | ZWhile of expr * spath + | ZIfThen of expr * spath * stmt + | ZIfElse of expr * stmt * spath + | ZMatch of expr * spath * spath_match_ctxt + + and spath = (instr list * instr list) * ipath + + type zipper = { + z_head : instr list; (* instructions on my left (rev) *) + z_tail : instr list; (* instructions on my right (me incl.) *) + z_path : ipath; (* path (zipper) leading to me *) + z_env : env option; + } + + let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; } - let zipper_at_nm_cpos1 + let zipper_step_into_block (env : EcEnv.env) - ((cp1, sub) : codepos1 * codepos_brsel) + ((cp1, sub) : codepos_step) (s : stmt) (zpr : ipath) - : (ipath * stmt) * (codepos1 * codepos_brsel) * env + : (ipath * stmt) * nm_codepos_step * env = + (* FIXME: unify with normalization above *) let (s1, i, s2) = find_by_cpos1 env cp1 s in - let zpr, env = + let zpr, step, env = match i.i_node, sub with | Swhile (e, sw), `Cond true -> - (ZWhile (e, ((s1, s2), zpr)), sw), env + (ZWhile (e, ((s1, s2), zpr)), sw), `Cond true, env | Sif (e, ifs1, ifs2), `Cond true -> - (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), env + (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), `Cond true, env | Sif (e, ifs1, ifs2), `Cond false -> - (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), env + (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env | Smatch (e, bs), `Match cn -> - let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in - let indt = oget (EcDecl.tydecl_as_datatype indt) in - let cnames = List.fst indt.tydt_ctors in - let ix, _ = - try List.findi (fun _ n -> EcSymbols.sym_equal cn n) cnames - with Not_found -> raise InvalidCPos - in + let ix = select_match_arm_idx env e cn 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), env + (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env | _ -> raise InvalidCPos - in zpr, ((0, `ByPos (1 + List.length s1)), sub), env + in zpr, ((List.length s1), step), env - let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) = - let ((zpr, s), env), nm = - List.fold_left_map - (fun ((zpr, s), env) nm1 -> let zpr, s, env = zipper_at_nm_cpos1 env nm1 s zpr in (zpr, env), s) - ((ZTop, s), env) nm in + let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) = + List.fold_left_map + (fun ((zpr, s), env) cps -> + let (zpr, s), step, env = zipper_step_into_block env cps s zpr in ((zpr, s), env), step) + ((ZTop, s), env) cpath - let s1, i, s2 = find_by_cpos1 env cp1 s in - let zpr = zipper ~env s1 (i :: s2) zpr in + let zipper_of_cpos_r (env : EcEnv.env) ((cpath, cp1) : codepos) (s : stmt) = + let ((zpr, s), env), nmcp = pre_zipper_of_codepos_path env cpath s in + + let nm = normalize_cpos1 env cp1 s in + let s1, s2 = split_at_nmcgap1 (gap_before nm) s in + let zpr = zipper ~env (List.rev s1) s2 zpr in - (zpr, (nm, (0, `ByPos (1 + List.length s1)))) + (zpr, ((nmcp, nm), s)) let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) = fst (zipper_of_cpos_r env cp s) - let zipper_of_cpos_range env cpr s = - let top, bot = cpr in - let zpr, (_, pos) = zipper_of_cpos_r env top s in - match bot with - | `Base cp -> begin - let zpr', (_, pos') = zipper_of_cpos_r env cp s in - (* The two positions should identify the same block *) - if zpr'.z_path <> zpr.z_path then - raise InvalidCPos; - - (* The end position should be after the start *) - match pos, pos' with - | (_, `ByPos x), (_, `ByPos y) when x <= y -> - zpr, (0, `ByPos (y - x)) - | _ -> raise InvalidCPos - end - | `Offset cp1 -> zpr, cp1 - - let zipper_and_split_of_cpos_range env cpr s = - let zpr, cp = zipper_of_cpos_range env cpr s in - match zpr.z_tail with - | [] -> raise InvalidCPos - | i :: tl -> - let s, tl = split_at_cpos1 ~after:`Auto env cp (stmt tl) in - (zpr, cp), ((i::s), tl) - - let split_at_cpos1 env cpos1 s = - split_at_cpos1 ~after:`Auto env cpos1 s - - let may_split_at_cpos1 ?(rev = false) env cpos1 s = - ofdfl - (fun () -> if rev then (s.s_node, []) else ([], s.s_node)) - (omap ((split_at_cpos1 env)^~ s) cpos1) - - let rec zip i ((hd, tl), ip) = + (* + Returns: + A zipper pointing to the start of the range + A split of the block according to the range + The normalized cpos range + *) + let zipper_and_split_of_cgap_range (env: env) (path, (start, fin) : codegap_range) (s: stmt) : zipper * _ * nm_codegap_range = + let (zpr, ((cpath, _), s)) = zipper_of_cpos_r env (path, (instr_after_gap start)) s in + let start = normalize_cgap1 env start s in + let fin = normalize_cgap1 env fin s in + let ss = split_by_nmcgap_range (start, fin) s in + (zpr, ss, (cpath, (start, fin))) + + let rec zip (i: instr option) (((hd, tl), ip): (instr list * instr list) * ipath) = let s = stmt (List.rev_append hd (List.ocons i tl)) in match ip with @@ -297,14 +620,14 @@ module Zipper = struct let zip zpr = zip None ((zpr.z_head, zpr.z_tail), zpr.z_path) - let after ~strict zpr = + let after ~strict (zpr: zipper) = let rec doit acc ip = match ip with | ZTop -> acc | ZWhile (_, ((_, is), ip)) -> doit (is :: acc) ip | ZIfThen (_, ((_, is), ip), _) -> doit (is :: acc) ip | ZIfElse (_, _, ((_, is), ip)) -> doit (is :: acc) ip - | ZMatch (_, ((_, is), ip), _) -> doit (is :: acc) ip + | ZMatch (_, ((_, is), ip), _) -> doit (is :: acc) ip in let after = @@ -315,18 +638,18 @@ module Zipper = struct in List.rev after - let fold_range env cenv cpr f state s = - let (zpr, _), (s, tl) = zipper_and_split_of_cpos_range env cpr s in + let fold_range (env: env) cenv (cpr: codegap_range) f state (s: stmt) = + let zpr, (_pre, s, tl), _nmcpr = zipper_and_split_of_cgap_range env cpr s in let env = odfl env zpr.z_env in let state', si' = f env cenv state s in state', zip { zpr with z_tail = si' @ tl } - let map_range env cpr f s = + let map_range (env: env) (cpr: codegap_range) f (s: stmt) = snd (fold_range env () cpr (fun env () _ si -> (), f env si) () s) - let fold env cenv cp f state s = + let fold (env: env) cenv ((path, cp1): codepos) f state (s: stmt) = let f env cenv state si = f env cenv state (List.hd si) in - fold_range env cenv (cp, `Offset (cpos 0)) f state s + fold_range env cenv (path, codegap1_range_of_codepos1 cp1) f state s let map env cpos f s = fst_map diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 66c6bc200..c6d9fdd36 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -21,23 +21,189 @@ module Position : sig | `Call of lvmatch ] + and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ] + exception InvalidCPos + type cp_base = [ - | `ByPos of int + | `ByPos of int (* Always <> 0 *) | `ByMatch of int option * cp_match ] - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] - type codepos1 = int * cp_base - type codepos = (codepos1 * codepos_brsel) list * codepos1 - type codepos_range = codepos * [`Base of codepos | `Offset of codepos1] - type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1] + (* Branch selection *) + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type nm_codepos_brsel = [`Cond of bool | `Match of int] + (* Linear code position inside a block *) + type codepos1 = int * cp_base + (* Normalized code position inside a block, always > 0 *) + type nm_codepos1 = int + (* Codeposition path step *) + type codepos_step = (codepos1 * codepos_brsel) + type nm_codepos_step = (int * nm_codepos_brsel) + (* Block selection by codepos + branch selection *) + type codepos_path = codepos_step list + type nm_codepos_path = nm_codepos_step list + (* Full codeposition = path to block + position in block *) + type codepos = codepos_path * codepos1 + type nm_codepos = nm_codepos_path * nm_codepos1 + (* Code position offset *) + type codeoffset1 = [`Relative of int | `Absolute of codepos1] + + (* Top-level first and last position *) + val cpos_first : codepos + val cpos_last : codepos + + (* Block-level first and last position *) + val cpos1_first : codepos1 + val cpos1_last : codepos1 + val cpos1_after_last : codepos1 + + val cpos1_to_top : codepos1 -> codepos val shift1 : offset:int -> codepos1 -> codepos1 val shift : offset:int -> codepos -> codepos val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1 + + module Notations : sig + val (|+>) : codepos -> int -> codepos + + val (+>) : codepos1 -> int -> codepos1 + + val (<+|) : codepos -> int -> codepos + + val (<+) : codepos1 -> int -> codepos1 + end + + (* Normalization functions *) + val find_by_cp_match : env -> (int option * cp_match) -> stmt -> instr list * instr * instr list + + val exists_match : env -> cp_match -> stmt -> bool + + val find_by_nmcpos1 : ?rev:bool -> nm_codepos1 -> stmt -> instr list * instr * instr list + + val check_nm_cpos1 : nm_codepos1 -> stmt -> unit + + val normalize_cp_base : ?check:bool -> env -> cp_base -> stmt -> nm_codepos1 + + val normalize_cpos1 : ?check:bool -> env -> codepos1 -> stmt -> nm_codepos1 + + val resolve_offset1_from_cpos1 : env -> nm_codepos1 -> codeoffset1 -> stmt -> nm_codepos1 + + val find_by_cpos1 : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list + + val select_match_arm_idx : env -> expr -> string -> int + + val normalize_brsel : env -> instr -> codepos_brsel -> (env * stmt) * nm_codepos_brsel + + val select_branch : env -> instr -> codepos_brsel -> stmt + + val normalize_cpos_step : env -> stmt -> codepos_step -> (env * stmt) * nm_codepos_step + + val normalize_cpos_path : env -> codepos_path -> stmt -> (env * stmt) * nm_codepos_path + + val normalize_cpos : env -> codepos -> stmt -> (env * stmt) * nm_codepos + + val cpos1 : int -> codepos1 + + (* --- Gap types --- *) + (* Normalized gap inside a block, 0-indexed, range [0, n] *) + type nm_codegap1 = int + (* Typed but unnormalized gap *) + type codegap1 = + | GapBefore of codepos1 + | GapAfter of codepos1 + (* Full gap with path *) + type codegap = codepos_path * codegap1 + (* Normalized gap with path *) + type nm_codegap = nm_codepos_path * nm_codegap1 + (* Gap-based ranges *) + type codegap1_range = codegap1 * codegap1 + type nm_codegap1_range = nm_codegap1 * nm_codegap1 + type codegap_range = codepos_path * codegap1_range + type nm_codegap_range = nm_codepos_path * nm_codegap1_range + (* Gap-based offset for swap *) + type codegap_offset1 = + | GapAbsolute of codegap1 + | GapRelative of int + + (* Boundary gap constructors *) + val codegap1_start : codegap1 + val codegap1_end : codegap1 + val codegap_start : codegap + val codegap_end : codegap + + (* Convenience constructors *) + val gap_before_pos : codepos1 -> codegap1 + val gap_after_pos : codepos1 -> codegap1 + val instr_before_gap : codegap1 -> codepos1 + val instr_after_gap : codegap1 -> codepos1 + + (* Position <-> Gap conversions (normalized, 0-indexed) *) + val gap_before : nm_codepos1 -> nm_codegap1 + val gap_after : nm_codepos1 -> nm_codegap1 + val instr_after : nm_codegap1 -> nm_codepos1 + val instr_before : nm_codegap1 -> nm_codepos1 + + (* Single-instruction range as gap pair *) + val gap_range_of_pos : nm_codepos1 -> nm_codegap1_range + val gap_range_of_cpos : nm_codepos -> nm_codegap_range + + (* Gap counting helpers *) + val gap_after_n : int -> codegap1 + val gap_before_n : int -> codegap1 + val gap_after_last_n : int -> codegap1 + val gap_before_last_n : int -> codegap1 + + (* Gap normalization *) + val check_nm_cgap1 : nm_codegap1 -> stmt -> unit + val normalize_cgap1 : env -> codegap1 -> stmt -> nm_codegap1 + val normalize_cgap : env -> codegap -> stmt -> (env * stmt) * nm_codegap + val normalize_cgap1_range : env -> codegap1_range -> stmt -> nm_codegap1_range + val normalize_cgap_range : env -> codegap_range -> stmt -> (env * stmt) * nm_codegap_range + + (* Split at gap *) + val split_at_nmcgap1 : nm_codegap1 -> stmt -> instr list * instr list + val split_at_cgap1 : env -> codegap1 -> stmt -> instr list * instr list + val split_at_cgap : env -> codegap -> stmt -> env * (instr list * instr list) + val may_split_at_cgap1 : ?rev:bool -> env -> codegap1 option -> stmt -> instr list * instr list + + (* Range operations on gaps *) + val split_by_nmcgap_range : nm_codegap1_range -> stmt -> instr list * instr list * instr list + val split_by_nmcgaps : nm_codegap1 list -> stmt -> instr list list + + (* Resolve gap offset relative to a gap range *) + val resolve_gap_offset : env -> nm_codegap1_range -> codegap_offset1 -> stmt -> nm_codegap1 + + (* Semantic helpers for match-based finding *) + val find_last_match : env -> cp_match -> stmt -> instr list * instr * instr list + val find_first_match : env -> cp_match -> stmt -> instr list * instr * instr list + val find_nth_match : env -> int -> cp_match -> stmt -> instr list * instr * instr list + + (* [split_by_match env ~occ ~gap cm s] splits [s] at the gap before/after + the [occ]-th occurrence of [cm]. *) + val split_by_match : env -> occ:int -> gap:[`Before | `After] -> cp_match -> stmt -> instr list * instr list + + val gap_before_match : env -> occ:int -> cp_match -> stmt -> nm_codegap1 + val gap_after_match : env -> occ:int -> cp_match -> stmt -> nm_codegap1 + + (* Block iteration *) + val fold_blocks : start:nm_codegap1 -> block_size:int -> stmt -> + (int -> nm_codegap1 -> nm_codegap1 -> 'a -> 'a) -> 'a -> 'a + val iter_blocks : start:nm_codegap1 -> block_size:int -> stmt -> + (int -> nm_codegap1 -> nm_codegap1 -> unit) -> unit + + (* Conversion between pos and gap for ranges *) + val codegap1_range_of_codepos1 : codepos1 -> codegap1_range + val codegap_range_of_codepos : codepos -> codegap_range + + val nm_codegap1_range_of_nm_codepos1 : nm_codepos1 -> nm_codegap1_range + val nm_codegap_range_of_nm_codepos : nm_codepos -> nm_codegap_range + + val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool + + val nm_codepos1_in_nm_codegap1_range : nm_codepos1 -> nm_codegap1_range -> bool end (* -------------------------------------------------------------------- *) @@ -66,20 +232,8 @@ module Zipper : sig z_env : env option; (* env with local vars from previous instructions *) } - exception InvalidCPos - - (* Create a codepos1 from a top-level absolute position *) - val cpos : int -> codepos1 - - (* Split a statement from a top-level position (codepos1) *) - val find_by_cpos1 : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list - val split_at_cpos1 : env -> codepos1 -> stmt -> instr list * instr list - - (* Split a statement from an optional top-level position (codepos1) *) - val may_split_at_cpos1 : ?rev:bool -> env -> codepos1 option -> stmt -> instr list * instr list - (* Find the absolute offset of a top-level position (codepos1) w.r.t. a given statement *) - val offset_of_position : env -> codepos1 -> stmt -> int +(* val offset_of_position : env -> codepos1 -> stmt -> int *) (* [zipper] soft constructor *) val zipper : ?env : env -> instr list -> instr list -> ipath -> zipper @@ -90,7 +244,7 @@ module Zipper : sig * positions only). The second variant simply throw away the second * output. *) - val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * codepos + 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] from the start of the code position @@ -98,8 +252,8 @@ module Zipper : sig * the zipper that represents the final position in the range. * Raise [InvalidCPos] if [codepos_range] is not a valid range for [stmt]. *) - val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1 - val zipper_and_split_of_cpos_range : env -> codepos_range -> stmt -> (zipper * codepos1) * (instr list * instr list) +(* val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1 *) + val zipper_and_split_of_cgap_range : env -> codegap_range -> stmt -> zipper * (instr list * instr list * instr list) * nm_codegap_range (* Zip the zipper, returning the corresponding statement *) val zip : zipper -> stmt @@ -130,8 +284,8 @@ module Zipper : sig val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt (* Variants of the above but using code position ranges *) - val fold_range : env -> 'a -> codepos_range -> ('a, 'state) folder_l -> 'state -> stmt -> 'state * stmt - val map_range : env -> codepos_range -> (env -> instr list -> instr list) -> stmt -> stmt + val fold_range : env -> 'a -> codegap_range -> ('a, 'state) folder_l -> 'state -> stmt -> 'state * stmt + val map_range : env -> codegap_range -> (env -> instr list -> instr list) -> stmt -> stmt end diff --git a/src/ecParser.mly b/src/ecParser.mly index d97f4ccb9..324477a30 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -1008,7 +1008,6 @@ pffilter: i=pfpos? COLON j=pfpos? { `Range (i, j) } | i=pfpos { `Single i }, COMMA) RBRACKET - { PFRange (flat, rg) } | LPBRACE flat=iboption(SLASH) x=ident IN h=form_h RPBRACE @@ -2554,47 +2553,105 @@ codepos1_wo_off: | k=icodepos i=option(brace(sword)) { (`ByMatch (i, k) :> pcp_base) } +(* 0-indexed variant: bare integer produces ByPos0 *) +codepos1_wo_off_0: +| i=sword + { (`ByPos0 i :> pcp_base) } + +| k=icodepos i=option(brace(sword)) + { (`ByMatch (i, k) :> pcp_base) } + codepos1: | cp=codepos1_wo_off { (0, cp) } | cp=codepos1_wo_off AMP PLUS i=word { ( i, cp) } | cp=codepos1_wo_off AMP MINUS i=word { (-i, cp) } +(* 0-indexed variant *) +codepos1_0: +| cp=codepos1_wo_off_0 { (0, cp) } + +| cp=codepos1_wo_off_0 AMP PLUS i=word { ( i, cp) } +| cp=codepos1_wo_off_0 AMP MINUS i=word { (-i, cp) } + branch_select: | SHARP s=boident DOT {`Match s} | DOT { `Cond true } | QUESTION { `Cond false } -%inline nm1_codepos: +%inline codepos_step: | i=codepos1 bs=branch_select { (i, bs) } -codepos: -| nm=rlist0(nm1_codepos, empty) i=codepos1 - { (nm, i) } - -codepos_range: -| LBRACKET cps=codepos DOTDOT cpe=codepos RBRACKET { (cps, `Base cpe) } -| LBRACKET cps=codepos MINUS cpe=codepos1 RBRACKET { (cps, `Offset cpe) } +(* Gap grammar productions *) +(* Base explicit gap — direction override only *) +codegap1: +| HAT LT i=codepos1 { GapBefore i } +| HAT GT i=codepos1 { GapAfter i } + +(* Default-before: bare integer means gap before (1-indexed) *) +codegap1_before: +| i=codepos1 { GapBefore i } +| g=codegap1 { g } + +(* FIXME: decide on semantic before merge *) +(* 0-indexed gap: GapBefore for non-negative, GapAfter for negative + (negative indexes count from the end, so "in the direction of travel" + means GapAfter — e.g. wp -1 = gap after last instruction) *) +codegap1_0before: +| i=codepos1_0 { GapBefore i } + (* { match snd i with + | `ByPos0 n when n < 0 -> GapAfter i + | _ -> GapBefore i } *) +| g=codegap1 { g } + +(* Default-after: bare integer means gap after (e.g. wp, sp) *) +codegap1_after: +| i=codepos1 { GapAfter i } +| g=codegap1 { g } + +(* Gap-based offset for swap *) +codegap_offset1: +| i=sword { PGapRelative i } +| AT g=codegap1_before { PGapAbsolute g } + +(* Optional gap positions *) +o_codegap1_before: +| UNDERSCORE { None } +| g=codegap1_before { Some g } + +(* s_codegap1 variants for doption *) +s_codegap1_0before: +| g=codegap1_0before { Single g } +| g1=codegap1_0before g2=codegap1_0before { Double (g1, g2) } + +(* FIXME: Unify with above *) +(* Shift to convert input closed range into closed-open form *) +%inline codegap1_range: +| LBRACKET cps=codepos1 DOTDOT cpe=codepos1 RBRACKET { (GapBefore cps, GapAfter cpe) } +| LBRACKET cps=codepos1 MINUS cpo=loc(sword) RBRACKET { + if (unloc cpo) > 0 then + (GapBefore cps, GapAfter (shift1 ~offset:(unloc cpo) cps)) + else + parse_error (loc cpo) (Some "cannot give negative offset for codepos range end") +} -codepos_or_range: -| cp=codepos { (cp, `Offset (0, `ByPos 0)) } -| cpr=codepos_range { cpr } +%inline codepos_path: +| path=rlist0(codepos_step, empty) { path } -codeoffset1: -| i=sword { (`ByOffset i :> pcodeoffset1) } -| AT p=codepos1 { (`ByPosition p :> pcodeoffset1) } +codepos: +| path=codepos_path i=codepos1 + { (path, i) } -o_codepos1: -| UNDERSCORE { None } -| i=codepos1 { Some i} +codegap_range: +| r=codegap1_range + { ([], r) } +| path=rlist1(codepos_step, empty) COLON r=codegap1_range + { (path, r) } -s_codepos1: -| n=codepos1 - { Single n } - -| n1=codepos1 n2=codepos1 - { Double (n1, n2) } +codepos_or_range: +| cp=codepos { Pos cp } +| cpr=codegap_range { Range cpr } semrndpos1: | b=boption(STAR) c=codepos1 @@ -2647,14 +2704,11 @@ swap_info: | s=side? p=swap_position { (s, p) } swap_position: -| offset=codeoffset1 +| offset=codegap_offset1 { { interval = None; offset; } } -| start=codepos1 offset=codeoffset1 - { { interval = Some (start, None); offset; } } - -| LBRACKET start=codepos1 DOTDOT end_=codepos1 RBRACKET offset=codeoffset1 - { { interval = Some (start, Some end_); offset; } } +| interval=codepos_or_range offset=codegap_offset1 + { { interval = Some interval; offset; } } side: | LBRACE n=word RBRACE { @@ -2851,7 +2905,7 @@ logtactic: { Pwlog (ids, b, f) } eager_tac: -| SEQ n1=codepos1 n2=codepos1 COLON s=stmt COLON p=form_or_double_form +| SEQ n1=codegap1_0before n2=codegap1_0before COLON s=stmt COLON p=form_or_double_form { Peager_seq ((n1, n2), s, p) } | IF @@ -2880,13 +2934,13 @@ form_or_double_form: | s=option(side) { `Head (s) } -| s=option(side) i1=o_codepos1 i2=o_codepos1 COLON f=sform +| s=option(side) i1=o_codegap1_before i2=o_codegap1_before COLON f=sform { `Seq (s, (i1, i2), f) } | CEQ f=sform { `Seq (None, (None, None), f) } -| s=option(side) i=codepos1? COLON LPAREN +| s=option(side) i=codegap1_before? COLON LPAREN UNDERSCORE COLON f1=form LONGARROW f2=form RPAREN { @@ -2943,13 +2997,13 @@ interleave_info: | PROC STAR { Pfun `Code } -| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info +| SEQ s=side? pos=s_codegap1_0before COLON p=form_or_double_form f=app_bd_info { Pseq (s, pos, p, f) } -| WP n=s_codepos1? +| WP n=s_codegap1_0before? { Pwp n } -| SP n=s_codepos1? +| SP n=s_codegap1_0before? { Psp n } | SKIP @@ -2996,7 +3050,7 @@ interleave_info: | RND s=side? info=rnd_info c=prefix(COLON, semrndpos)? { Prnd (s, c, info) } -| RNDSEM red=boption(STAR) s=side? c=codepos1 +| RNDSEM red=boption(STAR) s=side? c=codegap1_0before { Prndsem (red, s, c) } | INLINE s=side? u=inlineopt? o=occurences? @@ -3127,7 +3181,7 @@ interleave_info: | BYPR f1=sform f2=sform { PPr (Some (f1, f2)) } -| FEL at_pos=codepos1 cntr=sform delta=sform q=sform +| FEL at_pos=codegap1_after cntr=sform delta=sform q=sform f_event=sform some_p=fel_pred_specs inv=sform? { let info = { pfel_cntr = cntr; @@ -3253,7 +3307,7 @@ fel_pred_specs: {assoc_ps} eqobs_in_pos: -| i1=codepos1 i2=codepos1 { (i1, i2) } +| i1=codegap1_after i2=codegap1_after { (i1, i2) } eqobs_in_eqglob1: | LPAREN mp1= uoption(loc(fident)) TILD mp2= uoption(loc(fident)) COLON diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 877f37074..c3336aa19 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -49,18 +49,56 @@ type pcp_match = [ and plvmatch = [ `LvmNone | `LvmVar of pqsymbol ] -type pcp_base = [ `ByPos of int | `ByMatch of int option * pcp_match ] +(* `ByPos: 1-indexed position (standard user syntax) + `ByPos0: 0-indexed position (used by seq, rndsem, etc.) *) +type pcp_base = [ `ByPos of int | `ByPos0 of int | `ByMatch of int option * pcp_match ] +(* Code positions *) type pbranch_select = [`Cond of bool | `Match of psymbol] type pcodepos1 = int * pcp_base -type pcodepos = (pcodepos1 * pbranch_select) list * pcodepos1 -type pcodepos_range = pcodepos * [`Base of pcodepos | `Offset of pcodepos1] +type pcodepos_step = (pcodepos1 * pbranch_select) +type pcodepos_path = pcodepos_step list +type pcodepos = pcodepos_path * pcodepos1 type pdocodepos1 = pcodepos1 doption option +let shift1 ((off,base): pcodepos1) ~(offset: int) : pcodepos1 = + (off + offset, base) + +let shift ((path,cp1): pcodepos) ~(offset: int) : pcodepos = + (path, shift1 ~offset cp1) + +(* Code position offsets *) type pcodeoffset1 = [ - | `ByOffset of int - | `ByPosition of pcodepos1 + | `Relative of int + | `Absolute of pcodepos1 ] + +(* Code gap types *) +type pcodegap1 = + | GapBefore of pcodepos1 + | GapAfter of pcodepos1 + +(* Boundary gap constructors *) +let pcodegap1_start : pcodegap1 = GapBefore (0, `ByPos 1) +let pcodegap1_end : pcodegap1 = GapAfter (0, `ByPos (-1)) + +type pcodegap = pcodepos_path * pcodegap1 + +type pcodegap1_range = pcodegap1 * pcodegap1 +type pcodegap_range = pcodepos_path * pcodegap1_range + +(* Code position ranges *) +type pcodepos_or_range = + | Pos of pcodepos + | Range of pcodegap_range + +(* Gap-based offset for swap *) +type pcodegap_offset1 = + | PGapAbsolute of pcodegap1 + | PGapRelative of int + +type pdocodegap1 = pcodegap1 doption option + (* -------------------------------------------------------------------- *) type pty_r = @@ -351,7 +389,7 @@ and pstructure_item = | Pst_import of (pmsymbol located) list and pupdate_var = psymbol list * pty -and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_range located * pupdate_item) list * pexpr option) +and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_or_range located * pupdate_item) list * pexpr option) and pupdate_item = | Pup_stmt of pupdate_stmt @@ -538,8 +576,8 @@ type preduction = { (* -------------------------------------------------------------------- *) type pswap_kind = { - interval : (pcodepos1 * pcodepos1 option) option; - offset : pcodeoffset1; + interval : pcodepos_or_range option; + offset : pcodegap_offset1; } type interleave_info = oside * (int * int) * ((int * int) list) * int @@ -631,13 +669,13 @@ type fun_info = [ (* -------------------------------------------------------------------- *) type seq_info = - oside * pcodepos1 doption * pformula doption * p_seq_xt_info + oside * pcodegap1 doption * pformula doption * p_seq_xt_info (* -------------------------------------------------------------------- *) type pcond_info = [ | `Head of oside - | `Seq of oside * pcodepos1 option pair * pformula - | `SeqOne of side * pcodepos1 option * pformula * pformula + | `Seq of oside * pcodegap1 option pair * pformula + | `SeqOne of side * pcodegap1 option * pformula * pformula ] (* -------------------------------------------------------------------- *) @@ -679,7 +717,7 @@ type outline_kind = type outline_info = { outline_side: side; - outline_range: pcodepos_range; + outline_range: pcodepos_or_range; outline_kind: outline_kind; } @@ -706,7 +744,7 @@ type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm (* -------------------------------------------------------------------- *) type sim_info = { - sim_pos : pcodepos1 pair option; + sim_pos : pcodegap1 pair option; sim_hint : (pgamepath option pair * pformula) list * pformula option; sim_eqs : pformula option } @@ -742,8 +780,8 @@ type phltactic = | Prepl_stmt of trans_info | Pfun of fun_info | Pseq of seq_info - | Pwp of pdocodepos1 - | Psp of pdocodepos1 + | Pwp of pdocodegap1 + | Psp of pdocodegap1 | Pwhile of (oside * while_info) | Pasyncwhile of async_while_info | Pfission of (oside * pcodepos * (int * (int * int))) @@ -764,7 +802,7 @@ type phltactic = | Pkill of (oside * pcodepos * int option) | Pasgncase of (oside * pcodepos) | Prnd of oside * psemrndpos option * rnd_tac_info_f - | Prndsem of bool * oside * pcodepos1 + | Prndsem of bool * oside * pcodegap1 | Palias of (oside * pcodepos * osymbol_r) | Pweakmem of (oside * psymbol * fun_params) | Pset of (oside * pcodepos * bool * psymbol * pexpr) @@ -779,7 +817,7 @@ type phltactic = | Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option)) | PPr of (pformula * pformula) option | Pbyupto - | Pfel of (pcodepos1 * fel_info) + | Pfel of (pcodegap1 * fel_info) | Phoare | Pprbounded | Psim of crushmode option* sim_info @@ -790,11 +828,11 @@ type phltactic = | Prwprgm of rwprgm | Pprocrewrite of side option * pcodepos * prrewrite | Pprocrewriteat of psymbol * ppterm - | Pchangestmt of side option * pcodepos_range * pstmt + | Pchangestmt of side option * pcodepos_or_range * pstmt | Phoaresplit (* Eager *) - | Peager_seq of (pcodepos1 pair * pstmt * pformula doption) + | Peager_seq of (pcodegap1 pair * pstmt * pformula doption) | Peager_if | Peager_while of pformula | Peager_fun_def diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index dff558c4d..48dbdaeaf 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2386,8 +2386,10 @@ let pp_scvar ppe fmt vs = let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos1) = let s : string = match cp with + | `ByPos i when i >= 0 -> + string_of_int (i + 1) (* 0-indexed internal → 1-indexed display *) | `ByPos i -> - string_of_int i + string_of_int i (* negative positions displayed as-is *) | `ByMatch (i, k) -> let s = @@ -2419,22 +2421,49 @@ let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos (* -------------------------------------------------------------------- *) let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : CP.codeoffset1) = match offset with - | `ByPosition p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p - | `ByOffset o -> Format.fprintf fmt "%d" o + | `Absolute p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p + | `Relative o -> Format.fprintf fmt "%d" o + +let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) = + Format.fprintf fmt "%s" + (match br with + | `Cond true -> "." + | `Cond false -> "?" + | `Match cp -> Format.sprintf "#%s." cp) + +let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) = + Format.fprintf fmt "%a%a" (pp_codepos1 ppe) cp pp_codepos_brsel br + +let pp_codepos_path ppe = + (pp_list "" (pp_codepos_step ppe)) (* -------------------------------------------------------------------- *) -let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) = - let pp_nm (fmt : Format.formatter) ((cp, bs) : CP.codepos1 * CP.codepos_brsel) = - let bs = - match bs with - | `Cond true -> "." - | `Cond false -> "?" - | `Match cp -> Format.sprintf "#%s." cp - in - Format.fprintf fmt "%a%s" (pp_codepos1 ppe) cp bs - in +let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, cp1) : CP.codepos) = + Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codepos1 ppe) cp1 + +(* -------------------------------------------------------------------- *) +let pp_codegap1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : CP.codegap1) = + match g with + | CP.GapBefore cp -> Format.fprintf fmt "^<%a" (pp_codepos1 ppe) cp + | CP.GapAfter cp -> Format.fprintf fmt "^>%a" (pp_codepos1 ppe) cp + +let pp_codegap (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, g1) : CP.codegap) = + Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codegap1 ppe) g1 + +let symbol_and_codepos1_of_codegap1_range_edge (cg: CP.codegap1) : symbol * CP.codepos1 = + match cg with + | GapBefore cp -> "[", cp + | GapAfter cp -> "]", cp + +(* -------------------------------------------------------------------- *) +let pp_codegap1_range (ppe: PPEnv.t) (fmt: Format.formatter) ((start, fin) : CP.codegap1_range) = + let s, cps = symbol_and_codepos1_of_codegap1_range_edge start in + let e, cpe = symbol_and_codepos1_of_codegap1_range_edge fin in + Format.fprintf fmt "%s%a;%a%s" s (pp_codepos1 ppe) cps (pp_codepos1 ppe) cpe e - Format.fprintf fmt "%a%a" (pp_list "" pp_nm) nm (pp_codepos1 ppe) cp1 +(* FIXME: change when we can change the syntax *) +let pp_codegap_range (ppe: PPEnv.t) (fmt: Format.formatter) ((cpath, cp1r) : CP.codegap_range) = + Format.fprintf fmt "%a:[%a]" (pp_codepos_path ppe) cpath (pp_codegap1_range ppe) cp1r (* -------------------------------------------------------------------- *) let pp_opdecl_pr (ppe : PPEnv.t) fmt ((basename, ts, ty, op): symbol * ty_param list * ty * prbody option) = diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 266b86dc8..7b9c63956 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2283,7 +2283,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = let body = List.fold_right (fun (cpr, up) bd -> let {pl_desc = cpr; pl_loc = loc} = cpr in - let cp = trans_codepos_range env cpr in + let cp = trans_codepos_or_range env cpr in let change env si = match up with | Pup_stmt sup -> @@ -2295,7 +2295,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = try EcMatching.Zipper.map_range env cp change bd with - | EcMatching.Zipper.InvalidCPos -> + | InvalidCPos -> tyerror loc env (InvalidModUpdate MUE_InvalidCodePos); ) pupdates @@ -3732,7 +3732,9 @@ and trans_cp_match ?(memory : memory option) (env : EcEnv.env) (p : pcp_match) : (* -------------------------------------------------------------------- *) and trans_cp_base ?(memory : memory option) (env : EcEnv.env) (p : pcp_base) : cp_base = match p with + | `ByPos i when i > 0 -> `ByPos (i - 1) | `ByPos _ as p -> (p :> cp_base) + | `ByPos0 i -> `ByPos i (* already 0-indexed, no conversion *) | `ByMatch (i, p) -> `ByMatch (i, trans_cp_match ?memory env p) (* -------------------------------------------------------------------- *) @@ -3745,32 +3747,56 @@ and trans_codepos_brsel (bs : pbranch_select) : codepos_brsel = | `Cond b -> `Cond b | `Match { pl_desc = x } -> `Match x +and trans_codepos_step ?(memory: memory option) (env: EcEnv.env) ((cp1, brsel): pcodepos_step) : codepos_step = + let cp1 = trans_codepos1 ?memory env cp1 in + let brsel = trans_codepos_brsel brsel in + (cp1, brsel) + +and trans_codepos_path ?(memory: memory option) (env: EcEnv.env) (cpath: pcodepos_path) : codepos_path = + List.map (trans_codepos_step ?memory env) cpath + (* -------------------------------------------------------------------- *) -and trans_codepos ?(memory : memory option) (env : EcEnv.env) ((nm, p) : pcodepos) : codepos = - let nm = List.map (fun (cp1, bs) -> (trans_codepos1 ?memory env cp1, trans_codepos_brsel bs)) nm in +and trans_codepos ?(memory : memory option) (env : EcEnv.env) ((cpath, p) : pcodepos) : codepos = + let cpath = trans_codepos_path ?memory env cpath in let p = trans_codepos1 ?memory env p in - (nm, p) + (cpath, p) -(* -------------------------------------------------------------------- *) -and trans_codepos_range ?(memory : memory option) (env : EcEnv.env) ((cps, cpe) : pcodepos_range) : codepos_range = - let cps = trans_codepos ?memory env cps in - let cpe = - match cpe with - | `Base cp -> - `Base (trans_codepos ?memory env cp) - | `Offset cp -> - `Offset (trans_codepos1 ?memory env cp) - in - (cps, cpe) +and trans_codeoffset1 ?(memory: memory option) (env : EcEnv.env) (o : pcodeoffset1) : codeoffset1 = + match o with + | `Relative i -> `Relative i + | `Absolute p -> `Absolute (trans_codepos1 ?memory env p) + +and trans_codepos_or_range ?(memory: memory option) (env : EcEnv.env) (cpor: pcodepos_or_range) : codegap_range = + match cpor with + | Pos cp -> codegap_range_of_codepos (trans_codepos ?memory env cp) + | Range cpr -> trans_codegap_range ?memory env cpr (* -------------------------------------------------------------------- *) and trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption = DOption.map (trans_codepos1 ?memory env) p -and trans_codeoffset1 ?(memory: memory option) (env : EcEnv.env) (o : pcodeoffset1) : codeoffset1 = +(* -------------------------------------------------------------------- *) +and trans_codegap1 ?(memory : memory option) (env : EcEnv.env) (g : pcodegap1) : codegap1 = + match g with + | GapBefore cp -> GapBefore (trans_codepos1 ?memory env cp) + | GapAfter cp -> GapAfter (trans_codepos1 ?memory env cp) + +and trans_codegap ?(memory : memory option) (env : EcEnv.env) ((cpath, g1) : pcodegap) : codegap = + (trans_codepos_path ?memory env cpath, trans_codegap1 ?memory env g1) + +and trans_codegap1_range ?(memory : memory option) (env : EcEnv.env) ((g1, g2) : pcodegap1_range) : codegap1_range = + (trans_codegap1 ?memory env g1, trans_codegap1 ?memory env g2) + +and trans_codegap_range ?(memory : memory option) (env : EcEnv.env) ((cpath, gr) : pcodegap_range) : codegap_range = + (trans_codepos_path ?memory env cpath, trans_codegap1_range ?memory env gr) + +and trans_codegap_offset1 ?(memory : memory option) (env : EcEnv.env) (o : pcodegap_offset1) : codegap_offset1 = match o with - | `ByOffset i -> `ByOffset i - | `ByPosition p -> `ByPosition (trans_codepos1 ?memory env p) + | PGapRelative i -> GapRelative i + | PGapAbsolute g -> GapAbsolute (trans_codegap1 ?memory env g) + +and trans_dcodegap1 ?(memory : memory option) (env : EcEnv.env) (p : pcodegap1 doption) : codegap1 doption = + DOption.map (trans_codegap1 ?memory env) p (* -------------------------------------------------------------------- *) let get_instances (tvi, bty) env = diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 6722b92b3..936c461aa 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -239,11 +239,17 @@ type ismap = (instr list) EcMaps.Mstr.t val transstmt : ?map:ismap -> env -> EcUnify.unienv -> pstmt -> stmt (* -------------------------------------------------------------------- *) -val trans_codepos_range : ?memory:EcMemory.memory -> env -> pcodepos_range -> codepos_range +val trans_codepos_or_range : ?memory:EcMemory.memory -> env -> pcodepos_or_range -> codegap_range val trans_codepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 -> codepos1 val trans_codepos : ?memory:EcMemory.memory -> env -> pcodepos -> codepos val trans_dcodepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 doption -> codepos1 doption val trans_codeoffset1 : ?memory:EcMemory.memory -> env -> pcodeoffset1 -> codeoffset1 +val trans_codegap1 : ?memory:EcMemory.memory -> env -> pcodegap1 -> codegap1 +val trans_codegap : ?memory:EcMemory.memory -> env -> pcodegap -> codegap +val trans_codegap1_range : ?memory:EcMemory.memory -> env -> pcodegap1_range -> codegap1_range +val trans_codegap_range : ?memory:EcMemory.memory -> env -> pcodegap_range -> codegap_range +val trans_codegap_offset1 : ?memory:EcMemory.memory -> env -> pcodegap_offset1 -> codegap_offset1 +val trans_dcodegap1 : ?memory:EcMemory.memory -> env -> pcodegap1 doption -> codegap1 doption (* -------------------------------------------------------------------- *) type ptnmap = ty EcIdent.Mid.t ref diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 87a3bc727..6e4021436 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -158,16 +158,16 @@ let t_ehoare_call_core fpre fpost tc = let t_ehoare_call fpre fpost tc = - let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in + let _, _, _, _, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in + EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) wppre tc in let tcenv = FApi.t_swap_goals 0 1 tcenv in FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv let t_ehoare_call_concave f fpre fpost tc = - let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in + let _, _, _, _, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) + EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in let tcenv = FApi.t_swap_goals 0 1 tcenv in let t_call = diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index a49af0d92..1a938a6fd 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -422,9 +422,9 @@ 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 ~bdhoare:true cpos tr (t_zip cb) tc + 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 ~bdhoare:true cpos tr (t_zip cb) tc (* -------------------------------------------------------------------- *) let t_kill = FApi.t_low3 "code-tx-kill" t_kill_r diff --git a/src/phl/ecPhlCond.ml b/src/phl/ecPhlCond.ml index 69d5c4210..65af601e0 100644 --- a/src/phl/ecPhlCond.ml +++ b/src/phl/ecPhlCond.ml @@ -33,7 +33,7 @@ module LowInternal = struct let t_sub b tc = FApi.t_on1seq 0 - (EcPhlRCond.t_rcond side b (Zpr.cpos 1)) + (EcPhlRCond.t_rcond side b (EcMatching.Position.cpos1 0)) (FApi.t_seqs [t_introm; EcPhlSkip.t_skip; t_intros_i [m2;h]; t_finalize h h1 h2; t_simplify]) @@ -113,10 +113,10 @@ let rec t_equiv_cond side tc = (FApi.t_seqsub (t_equiv_cond (Some `Left)) [FApi.t_seqsub - (EcPhlRCond.Low.t_equiv_rcond `Right true (Zpr.cpos 1)) + (EcPhlRCond.Low.t_equiv_rcond `Right true (EcMatching.Position.cpos1 0)) [t_aux; t_clear hiff]; FApi.t_seqsub - (EcPhlRCond.Low.t_equiv_rcond `Right false (Zpr.cpos 1)) + (EcPhlRCond.Low.t_equiv_rcond `Right false (EcMatching.Position.cpos1 0)) [t_aux; t_clear hiff]])) tc @@ -223,7 +223,7 @@ end = struct in tc - |> EcPhlRCond.t_rcond_match side cname (Zpr.cpos 1) + |> EcPhlRCond.t_rcond_match side cname (EcMatching.Position.cpos1 0) @+ [discharge; clean] in diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index 800de9b7d..87c4809ea 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -4,7 +4,7 @@ open EcEnv open EcFol open EcLowGoal open EcLowPhlGoal -open EcMatching.Zipper +open EcMatching.Position open EcModules open EcPV open EcTypes @@ -69,8 +69,8 @@ let destruct_eager tc s = and ss = List.length s.s_node in let c, c' = (es.es_sl, es.es_sr) in - let z, c = s_split env (Zpr.cpos ss) c - and c', z' = s_split env (Zpr.cpos (List.length c'.s_node - ss)) c' in + let z, c = s_split env (gap_after_n ss) c + and c', z' = s_split env (gap_before_last_n ss) c' in let env, _, _ = FApi.tc1_eflat tc in let z_eq_s = ER.EqTest.for_stmt env (stmt z) s @@ -96,9 +96,11 @@ let destruct_on_op id_op tc = let env = FApi.tc1_env tc and es = tc1_as_equivS tc in let s = try - let s, _ = split_at_cpos1 env (-1, `ByMatch (Some (-1), id_op)) es.es_sl + let s, _ = split_by_match env ~occ:(-1) ~gap:`Before id_op es.es_sl in (* ensure the right statement also contains an [id_op]: *) - and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in + if not @@ exists_match env id_op es.es_sr then + tc_error_lazy !!tc (fun fmt -> + Format.fprintf fmt "eager: right side does not match operator"); s with InvalidCPos -> tc_error_lazy !!tc (fun fmt -> @@ -407,7 +409,7 @@ let t_eager_call = FApi.t_low2 "eager-call" t_eager_call_r let process_seq (i, j) s factor tc = let open BatTuple.Tuple2 in let indices = - mapn (tc1_process_codepos1 tc) ((Some `Left, i), (Some `Right, j)) + mapn (tc1_process_codegap1 tc) ((Some `Left, i), (Some `Right, j)) and factor = factor |> ( function Single p -> (p, p) | Double pp -> pp ) diff --git a/src/phl/ecPhlEager.mli b/src/phl/ecPhlEager.mli index 6d5c2b058..0bb47604c 100644 --- a/src/phl/ecPhlEager.mli +++ b/src/phl/ecPhlEager.mli @@ -5,7 +5,7 @@ open EcParsetree open EcCoreGoal.FApi open EcMatching.Position -val process_seq : pcodepos1 pair -> pstmt -> pformula doption -> backward +val process_seq : pcodegap1 pair -> pstmt -> pformula doption -> backward (** Tactic [eager seq] derives the following proof: {v (a) S; c₁ ~ c₁'; S : P ==> R₂ @@ -19,7 +19,7 @@ val process_seq : pcodepos1 pair -> pstmt -> pformula doption -> backward provided), as well as [S]. The predicate [={Q.1}] means equality on all free variables bound to the first memory in [Q]. *) -val t_eager_seq : codepos1 pair -> stmt -> ts_inv pair -> backward +val t_eager_seq : codegap1 pair -> stmt -> ts_inv pair -> backward (** Internal variant of [eager seq] *) val process_if : backward diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index 2cbf0416c..d7f9b0d1c 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -468,8 +468,9 @@ let process_eqobs_inS info tc = (FApi.t_try (FApi.t_seq EcPhlSkip.t_skip t_trivial)) (t_eqobs_inS sim eqo tc) | Some(p1,p2) -> - let p1 = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left , p1) in - let p2 = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Right, p2) in + (* sim positions are gaps: sim applies to instructions after the gap *) + let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in + let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in let _,sl2 = s_split env p1 es.es_sl in let _,sr2 = s_split env p2 es.es_sr in let _, eqi = diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index 90f017cbb..cef7b7999 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -8,6 +8,7 @@ open EcSubst open EcCoreGoal open EcLowGoal open EcLowPhlGoal +open EcMatching.Position module L = EcLocation module APT = EcParsetree @@ -160,19 +161,19 @@ let process_ecall oside (l, tvi, fs) tc = match kind, oside, p1 with | `Hoare n, _, Inv_ss p1 -> EcPhlSeq.t_hoare_seq - (Zpr.cpos (n-1)) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n - 1))) p1 tc | `Hoare n, _, Inv_hs p1 -> EcPhlSeq.t_hoare_seq - (Zpr.cpos (n-1)) (POE.lower p1) tc + (GapBefore (EcMatching.Position.cpos1 (n - 1))) (POE.lower p1) tc | `Equiv (n1, n2), None, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n1 - 1)), GapBefore (EcMatching.Position.cpos1 (n2 - 1))) p1 tc | `Equiv (n1, n2), Some `Left, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n1 - 1)), GapBefore (EcMatching.Position.cpos1 n2)) p1 tc | `Equiv(n1, n2), Some `Right, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc + (GapBefore (EcMatching.Position.cpos1 n1), GapBefore (EcMatching.Position.cpos1 (n2 - 1))) p1 tc | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion" in diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index b3cbef12c..dfb9d2203 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -112,6 +112,8 @@ let callable_oracles_stmt env modv = (* -------------------------------------------------------------------- *) (* FIXME: do we have to subst more? *) +(* [t_failure_event_r (gap, ...)]: splits the function body at [gap]; + FEL is applied to instructions after the gap. *) let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let env, _, concl = FApi.tc1_eflat tc in @@ -271,7 +273,7 @@ let process_fel at_pos (infos : fel_info) tc = let m = EcIdent.create "&hr" in - let at_pos = EcTyping.trans_codepos1 env at_pos in + let at_pos = EcTyping.trans_codegap1 env at_pos in let hyps = LDecl.inv_memenv1 m hyps1 in let cntr = {m;inv=TTC.pf_process_form !!tc hyps tint infos.pfel_cntr} in let hypsq = LDecl.push_active_ss (EcMemory.abstract pr.pr_mem) hyps1 in diff --git a/src/phl/ecPhlFel.mli b/src/phl/ecPhlFel.mli index e6769715a..cab7b0366 100644 --- a/src/phl/ecPhlFel.mli +++ b/src/phl/ecPhlFel.mli @@ -7,11 +7,11 @@ open EcMatching.Position (* -------------------------------------------------------------------- *) val t_failure_event : - codepos1 + codegap1 -> ss_inv -> form -> form -> ss_inv -> (xpath * ss_inv) list -> ss_inv -> backward (* -------------------------------------------------------------------- *) -val process_fel : pcodepos1 -> fel_info -> backward +val process_fel : pcodegap1 -> fel_info -> backward diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml index c5c23d645..31a2f9973 100644 --- a/src/phl/ecPhlHiAuto.ml +++ b/src/phl/ecPhlHiAuto.ml @@ -7,6 +7,7 @@ open EcModules open EcCoreGoal open EcLowGoal open EcLowPhlGoal +open EcMatching.Position (* -------------------------------------------------------------------- *) type ll_strategy = @@ -54,7 +55,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = tc |> match lls with | LL_WP -> - EcPhlWp.t_wp (Some (Single (Zpr.cpos (-1)))) + EcPhlWp.t_wp (Some (Single (GapBefore (EcMatching.Position.cpos1_last)))) | LL_RND -> let m = EcIdent.create "&hr" in @@ -69,7 +70,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = | LL_JUMP -> let m = EcIdent.create "&hr" in ( EcPhlSeq.t_bdhoare_seq - (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, + (GapBefore (EcMatching.Position.cpos1_last)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) @~ FApi.t_onalli (function @@ -87,7 +88,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = in ( EcPhlSeq.t_bdhoare_seq - (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) + (GapBefore (EcMatching.Position.cpos1_last)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) @~ FApi.t_onalli (function | 1 -> t_id @@ -142,8 +143,8 @@ let t_lossless tc = | FequivS hs -> let ml, mr = fst hs.es_ml, fst hs.es_mr in - ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ - [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ + ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Position.codegap1_start) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ + [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Position.codegap1_start) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ [ EcPhlSkip.t_skip @! t_trivial ; t_single ]; diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml index 5c0e6921d..cb1995684 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/src/phl/ecPhlHiCond.ml @@ -8,8 +8,8 @@ open EcMatching.Position (* -------------------------------------------------------------------- *) let process_cond (info : EcParsetree.pcond_info) tc = - let default_if (i : codepos1 option) s = - ofdfl (fun _ -> Zpr.cpos (tc1_pos_last_if tc s)) i in + let default_if (i : codegap1 option) s = + ofdfl (fun _ -> GapBefore (cpos1 (tc1_pos_last_if tc s))) i in match info with | `Head side -> @@ -22,8 +22,8 @@ let process_cond (info : EcParsetree.pcond_info) tc = | `Seq (side, (i1, i2), f) -> let es = tc1_as_equivS tc in let f = EcProofTyping.tc1_process_prhl_formula tc f in - let i1 = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i1)) i1 in - let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i2)) i2 in + let i1 = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i1)) i1 in + let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i2)) i2 in let n1 = default_if i1 es.es_sl in let n2 = default_if i2 es.es_sr in FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f) @@ -31,7 +31,7 @@ let process_cond (info : EcParsetree.pcond_info) tc = | `SeqOne (s, i, f1, f2) -> let es = tc1_as_equivS tc in - let i = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codepos1 tc (Some s, i1)) i in + let i = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (Some s, i1)) i in let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index 8dca495ff..6f4b8ad93 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -328,7 +328,7 @@ module HiInternal = struct match zip.Zp.z_tail with | { i_node = Scall _ } :: tl -> pat_of_spath ((zip.Zp.z_head, tl), zip.Zp.z_path) - | _ -> raise Zp.InvalidCPos + | _ -> raise EcMatching.Position.InvalidCPos end (* -------------------------------------------------------------------- *) @@ -426,7 +426,7 @@ let process_inline_codepos ~use_tuple side pos tc = | _, _ -> tc_error !!tc "invalid arguments" - with EcMatching.Zipper.InvalidCPos -> + with EcMatching.Position.InvalidCPos -> tc_error !!tc "invalid position" (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index cbe4027de..b8bf396d5 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -229,8 +229,7 @@ let process_unroll_for ~cfold side cpos tc = tc_error !!tc "cannot use deep code position"; let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in - let z, cpos = Zpr.zipper_of_cpos_r env cpos c in - let pos = 1 + List.length z.Zpr.z_head in + let z, ((_nm_path, pos), _) = Zpr.zipper_of_cpos_r env cpos c in (* Extract loop condition / body *) let t, wbody = @@ -286,23 +285,42 @@ let process_unroll_for ~cfold side cpos tc = let m = LDecl.fresh_id hyps "&m" in let x = f_pvar x tint goal_m in + (* Record the proof handle, position, and counter value for iteration [i]. + Used by [doi] below to revisit each unrolled iteration's subgoal. *) let t_set i pos z tc = hds.(i) <- Some (FApi.tc1_handle tc, pos, z); t_id tc in + (* Strengthen the goal by replacing the current precondition with [post], + closing the two side-conditions (pre ⇒ post, post ⇒ pre) via [t_trivial]. *) let t_conseq post tc = (EcPhlConseq.t_conseq (tc1_get_pre tc) post @+ [ t_trivial; t_trivial; t_id]) tc in + (* Main unrolling loop: processes the list [zs] of counter values produced + by [eval_cond]. For each value [z]: + 1. Apply [t_rcond] at position [pos] (0-indexed) to split the while into + its body (when [zs] is non-empty, i.e. guard is true) or skip it + (when [zs] is empty, i.e. guard is false). + 2. On the "guard proved" subgoal: introduce the guard hypothesis, + strengthen the pre to [x = z], and record iteration info via [t_set]. + 3. On the "rest of program" subgoal: recurse with the next counter value, + advancing [pos] by [blen] (the loop body length) since the unrolled + body instructions now precede the remaining while. + [pos] is a 0-indexed normalized position used to construct [cpos1 pos]. *) let rec t_doit i pos zs tc = match zs with | [] -> t_id tc | z :: zs -> - ((t_rcond side (zs <> []) (Zpr.cpos pos)) @+ + ((t_rcond side (zs <> []) (EcMatching.Position.cpos1 pos)) @+ [FApi.t_try (t_intro_i m) @! t_conseq (Inv_ss (map_ss_inv1 (fun x -> f_eq x (f_int z)) x)) @! t_set i pos z; t_doit (i+1) (pos + blen) zs]) tc in + (* Close a subgoal of the form hoare[... : pre ==> true] by: + 1. Weakening the postcondition to hoare-with-no-memory via [t_hoareS_conseq_nm] + 2. Closing side conditions with [t_trivial] + 3. Closing the main goal with [t_hoare_true] *) let t_conseq_nm tc = match (tc1_get_pre tc) with | Inv_ss inv -> @@ -313,17 +331,30 @@ let process_unroll_for ~cfold side cpos tc = [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc | _ -> tc_error !!tc "expecting single sided precondition" in + (* Second pass: revisit the subgoals recorded by [t_set] during [t_doit]. + For each iteration [i]: + - [pos] is the 0-indexed position of the while loop (rcond target). + - [init_pos] = pos - 1 is the counter init/increment assignment that + precedes the while; WP must consume through it to evaluate [x = z]. + - i=0: WP from [init_pos] onward, strengthen pre to true, close with + [t_hoare_true]. + - i>0: WP from [init_pos] onward, then seq-split at the previous + iteration's rcond position [pos'] with postcondition [x = z'], + applying the recorded proof handle [h'] and [t_conseq_nm]. *) let doi i tc = + let open EcMatching.Position in if Array.length hds <= i then t_id tc else - let (_h,pos,_z) = oget hds.(i) in + let (_h, pos, _z) = oget hds.(i) in + let init_pos = pos - 1 in + let wp_gap = GapBefore (cpos1 init_pos) in if i = 0 then - (EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos - 2)))) @! + (EcPhlWp.t_wp (Some (Single wp_gap)) @! t_conseq (Inv_ss {inv=f_true;m=x.m}) @! EcPhlTAuto.t_hoare_true) tc else let (h', pos', z') = oget hds.(i-1) in FApi.t_seqs [ - EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2)))); - EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ + EcPhlWp.t_wp (Some (Single wp_gap)); + EcPhlSeq.t_hoare_seq (GapBefore (cpos1 pos')) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ [t_apply_hd h'; t_conseq_nm] ] tc in @@ -331,7 +362,11 @@ let process_unroll_for ~cfold side cpos tc = let tcenv = FApi.t_onalli doi tcenv in if cfold then begin - let cpos = EcMatching.Position.shift ~offset:(-1) cpos in + (* Use normalized position: pos - 1 is the loop counter initialization + assignment that immediately precedes the while loop at pos. + We cannot reuse the original match-based cpos here because t_doit + has transformed the code, potentially invalidating the match. *) + let cpos = ([], EcMatching.Position.cpos1 (pos - 1)) in let clen = blen * (List.length zs - 1) in FApi.t_last (EcPhlCodeTx.t_cfold ~eager:false side cpos (Some clen)) tcenv diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml index 2898a138b..d0d65536b 100644 --- a/src/phl/ecPhlOutline.ml +++ b/src/phl/ecPhlOutline.ml @@ -59,7 +59,7 @@ let process_outline info tc = let ppe = EcPrinting.PPEnv.ofenv env in let range = - EcLowPhlGoal.tc1_process_codepos_range tc + EcLowPhlGoal.tc1_process_codepos_or_range tc (Some side, info.outline_range) in try diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli index d7ed5d99d..cd0031253 100644 --- a/src/phl/ecPhlOutline.mli +++ b/src/phl/ecPhlOutline.mli @@ -17,6 +17,6 @@ type outline_variant = cpr: selects the particular slice of the program to outline. variant: choose the type of outlining: procedure or statement. *) -val t_outline : side -> codepos_range -> outline_variant -> backward +val t_outline : side -> codegap_range -> outline_variant -> backward val process_outline : outline_info -> backward diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index b12461179..7a15cc611 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -237,15 +237,15 @@ let process_rewrite_at - the original program-logic goal with the selected range rewritten. *) let t_change_stmt (side : side option) - (pos : EcMatching.Position.codepos_range) + (pos : EcMatching.Position.codegap_range) (s : stmt) (tc : tcenv1) = let env = FApi.tc1_env tc in let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in - let (zpr, _), (stmt, epilog) = - EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in + let zpr, (_prelude,stmt, epilog), _nmr = + EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in (* Collect the variables that may be modified by the surrounding context, excluding the fragment being replaced. *) @@ -342,7 +342,7 @@ let t_change_stmt (* -------------------------------------------------------------------- *) let process_change_stmt (side : side option) - (pos : pcodepos_range) + (pos : pcodepos_or_range) (s : pstmt) (tc : tcenv1) = @@ -368,7 +368,7 @@ let process_change_stmt let pos = let env = EcEnv.Memory.push_active_ss me env in - EcTyping.trans_codepos_range ~memory:(fst me) env pos + EcTyping.trans_codepos_or_range ~memory:(fst me) env pos in let s = match side with diff --git a/src/phl/ecPhlRewrite.mli b/src/phl/ecPhlRewrite.mli index 100c4b6bb..bc2a23b6d 100644 --- a/src/phl/ecPhlRewrite.mli +++ b/src/phl/ecPhlRewrite.mli @@ -9,4 +9,4 @@ val process_rewrite_rw : side option -> pcodepos -> ppterm -> backward val process_rewrite_simpl : side option -> pcodepos -> backward val process_rewrite : side option -> pcodepos -> prrewrite -> backward val process_rewrite_at : psymbol -> ppterm -> backward -val process_change_stmt : side option -> pcodepos_range -> pstmt -> backward +val process_change_stmt : side option -> pcodepos_or_range -> pstmt -> backward diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 2f6008da4..268c3d731 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -598,7 +598,7 @@ let wp_equiv_rnd_r bij tc = subtc) (* -------------------------------------------------------------------- *) -let t_equiv_rnd_r side pos bij_info tc = +let t_equiv_rnd_r side (pos: (bool * codepos1) doption option) bij_info tc = match side, pos, bij_info with | Some side, None, (None, None) -> wp_equiv_disj_rnd_r side tc @@ -617,8 +617,8 @@ let t_equiv_rnd_r side pos bij_info tc = t_id tc | Some ((bl, il), (br, ir)) -> FApi.t_seq - (Core.t_equiv_rndsem_r bl `Left il) - (Core.t_equiv_rndsem_r br `Right ir) + (Core.t_equiv_rndsem_r bl `Left (gap_before_pos il)) + (Core.t_equiv_rndsem_r br `Right (gap_before_pos ir)) tc in let bij = @@ -646,7 +646,7 @@ let t_equiv_rnd ?pos side bij_info = (FApi.t_low3 "equiv-rnd" t_equiv_rnd_r) side pos bij_info (* -------------------------------------------------------------------- *) -let process_rnd side pos tac_info tc = +let process_rnd (side: side option) (pos: (bool * pcodepos1) doption option) tac_info tc = let concl = FApi.tc1_goal tc in match side, pos, tac_info with @@ -717,7 +717,7 @@ let t_equiv_rndsem = FApi.t_low3 "equiv-rndsem" Core.t_equiv_rndsem_r (* -------------------------------------------------------------------- *) let process_rndsem ~reduce side pos tc = let concl = FApi.tc1_goal tc in - let pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, pos) in + let pos = EcLowPhlGoal.tc1_process_codegap1 tc (side, pos) in match side with | None when is_hoareS concl -> diff --git a/src/phl/ecPhlRnd.mli b/src/phl/ecPhlRnd.mli index e636ac6d9..52483dd08 100644 --- a/src/phl/ecPhlRnd.mli +++ b/src/phl/ecPhlRnd.mli @@ -25,4 +25,4 @@ val t_equiv_rnd : ?pos:semrndpos -> oside -> (mkbij_t option) pair -> backward val process_rnd : oside -> psemrndpos option -> rnd_infos_t -> backward (* -------------------------------------------------------------------- *) -val process_rndsem : reduce:bool -> oside -> pcodepos1 -> backward +val process_rndsem : reduce:bool -> oside -> pcodegap1 -> backward diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml index a568172e8..9fab600d3 100644 --- a/src/phl/ecPhlRwEquiv.ml +++ b/src/phl/ecPhlRwEquiv.ml @@ -80,7 +80,7 @@ let t_rewrite_equiv side dir cp (equiv : equivF) equiv_pt rargslv tc = t_onselect p (t_seqs [ - EcPhlEqobs.process_eqobs_in none {sim_pos = some (cp, cp); sim_hint = ([], none); sim_eqs = none}; + EcPhlEqobs.process_eqobs_in none {sim_pos = some (GapAfter cp, GapAfter cp); sim_hint = ([], none); sim_eqs = none}; (match side, dir with | `Left, `LtoR -> t_id | `Left, `RtoL -> EcPhlSym.t_equiv_sym @@ -153,6 +153,7 @@ let process_rewrite_equiv info tc = (* Offload to the tactic *) try + (* FIXME: cp should be translated to codepos in process *) t_rewrite_equiv side dir cp equiv eqv_pt rargslv tc with | RwEquivError (RWE_InvalidFunction (got, wanted)) -> diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 35d47899d..0b14bf08e 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -14,6 +14,8 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) +(* [t_hoare_seq_r gap phi]: splits the statement at [gap]; the first + subgoal covers instructions before the gap, the second after. *) let t_hoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_hoareS tc in @@ -132,13 +134,13 @@ let t_equiv_seq_onesided side i pre post tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in let (ml, mr) = fst es.es_ml, fst es.es_mr in - let s, s', p', q' = + let s, _s', p', q' = match side with - | `Left -> + | `Left -> let p' = ss_inv_generalize_as_left pre ml mr in let q' = ss_inv_generalize_as_left post ml mr in es.es_sl, es.es_sr, p', q' - | `Right -> + | `Right -> let p' = ss_inv_generalize_as_right pre ml mr in let q' = ss_inv_generalize_as_right post ml mr in es.es_sr, es.es_sl, p', q' @@ -146,8 +148,8 @@ let t_equiv_seq_onesided side i pre post tc = let generalize_mod_side= sideif side generalize_mod_left generalize_mod_right in let ij = match side with - | `Left -> (i, Zpr.cpos (List.length s'. s_node)) - | `Right -> (Zpr.cpos (List.length s'. s_node), i) in + | `Left -> (i, EcMatching.Position.codegap1_end) + | `Right -> (EcMatching.Position.codegap1_end, i) in let _s1, s2 = s_split env i s in let modi = EcPV.s_write env (EcModules.stmt s2) in @@ -229,13 +231,13 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = | Single i, PSeqNone when is_hoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_hoare_seq i phi tc | Single i, PSeqNone when is_eHoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_ehoare_seq i phi tc | Single i, PSeqNone when is_equivS concl -> @@ -250,21 +252,21 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = match side with | None -> tc_error !!tc "seq onsided: side information expected" | Some side -> side in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in t_equiv_seq_onesided side i pre post tc | Single i, _ when is_bdHoareS concl -> check_side side; let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc | Double (i, j), PSeqNone when is_equivS concl -> check_side side; let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in - let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in + let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in t_equiv_seq (i, j) phi tc | Single _, PSeqNone diff --git a/src/phl/ecPhlSeq.mli b/src/phl/ecPhlSeq.mli index b5b905ad5..fd699b62e 100644 --- a/src/phl/ecPhlSeq.mli +++ b/src/phl/ecPhlSeq.mli @@ -6,11 +6,11 @@ open EcMatching.Position open EcAst (* -------------------------------------------------------------------- *) -val t_hoare_seq : codepos1 -> ss_inv -> backward -val t_ehoare_seq : codepos1 -> ss_inv -> backward -val t_bdhoare_seq : codepos1 -> ss_inv tuple6 -> backward -val t_equiv_seq : codepos1 pair -> ts_inv -> backward -val t_equiv_seq_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward +val t_hoare_seq : codegap1 -> ss_inv -> backward +val t_ehoare_seq : codegap1 -> ss_inv -> backward +val t_bdhoare_seq : codegap1 -> ss_inv tuple6 -> backward +val t_equiv_seq : codegap1 pair -> ts_inv -> backward +val t_equiv_seq_onesided : side -> codegap1 -> ss_inv -> ss_inv -> backward (* -------------------------------------------------------------------- *) val process_seq : seq_info -> backward diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index 564495bfd..3eae4f7c7 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -301,7 +301,9 @@ let t_sp_side pos tc = let t_sp = FApi.t_low1 "sp" t_sp_side (* -------------------------------------------------------------------- *) -let process_sp (cpos : pcodepos1 doption option) (tc : tcenv1) = +(* [process_sp gap]: splits the statement at [gap]; instructions after the + gap are kept, sp is applied to instructions before the gap. *) +let process_sp (cpos : pcodegap1 doption option) (tc : tcenv1) = let env = FApi.tc1_env tc in - let cpos = Option.map (EcTyping.trans_dcodepos1 env) cpos in + let cpos = Option.map (EcTyping.trans_dcodegap1 env) cpos in t_sp cpos tc diff --git a/src/phl/ecPhlSp.mli b/src/phl/ecPhlSp.mli index 2625f4030..3592d8caf 100644 --- a/src/phl/ecPhlSp.mli +++ b/src/phl/ecPhlSp.mli @@ -5,7 +5,7 @@ open EcCoreGoal.FApi open EcUtils (* -------------------------------------------------------------------- *) -val t_sp : (codepos1 doption) option -> backward +val t_sp : (codegap1 doption) option -> backward (* -------------------------------------------------------------------- *) -val process_sp : (pcodepos1 doption) option -> backward +val process_sp : (pcodegap1 doption) option -> backward diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index eacee93b2..30bdbe4c7 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -12,8 +12,8 @@ open EcLowGoal (* -------------------------------------------------------------------- *) type swap_kind = { - interval : (codepos1 * codepos1 option) option; - offset : codeoffset1; + interval : codegap_range; + offset : codegap_offset1; } (* -------------------------------------------------------------------- *) @@ -62,94 +62,38 @@ module LowInternal = struct 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 ) (env : EcEnv.env ) (info : swap_kind ) (s : stmt ) = - let len = List.length s.s_node in - - let p1, p2 (* inclusive *)= - match info.interval with - | Some (p , None ) -> p , p - | Some (p1, Some p2) -> p1, p2 - | None -> - let p = - match info.offset with - | `ByOffset offset when offset < 0 -> `ByPos (-1) - | _ -> `ByPos 1 in - let p : codepos1 = (0, p) in (p, p) - in - - let process_cpos (p : codepos1) = - try EcMatching.Zipper.offset_of_position env p s - with EcMatching.Zipper.InvalidCPos -> - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "invalid position: %a" (EcPrinting.pp_codepos1 ppe) p - ) in - - let i1 = process_cpos p1 in - let i2 = process_cpos p2 in - - if i2 < i1 then + let (env, s), (_, (start, fin)) = try + let (cpath, (start, fin)) = info.interval in + normalize_cgap_range env (cpath, (start, fin)) s + with InvalidCPos -> tc_error_lazy pf (fun fmt -> let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "invalid/empty code block: [%a..%a] (resolved as [%d..%d])" - (EcPrinting.pp_codepos1 ppe) p1 - (EcPrinting.pp_codepos1 ppe) p2 - i1 i2 - ); - - let offset = - match info.offset with - | `ByPosition p -> - let target = EcMatching.Zipper.offset_of_position env p s in - if i1 < target && target <= i2 then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "destination is inside the moved block: %a \\in ]%a..%a] (resolved as %d \\in ]%d..%d])" - (EcPrinting.pp_codeoffset1 ppe) info.offset - (EcPrinting.pp_codepos1 ppe) p1 - (EcPrinting.pp_codepos1 ppe) p2 - target i1 i2 - ); - if target <= i1 then target - i1 else target - i2 - 1 - - | `ByOffset o -> - o + Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval + ) in - let target = if 0 <= offset then i2+offset+1 else i1+offset in - - if target <= 0 then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "offset (%d) is too small by %d: start index is %a (resolved to %d)" - offset (1 + abs target) (EcPrinting.pp_codepos1 ppe) p1 i1 - ); - - if target > len+1 then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "offset (%d) is too larget by %d: end index is %a (resolved to %d)" - offset (target - len - 1) (EcPrinting.pp_codepos1 ppe) p2 i2 - ); - - let b1, b2, b3 = - if target <= i1 then target, i1, i2+1 else i1, i2+1, target in - - let hd , tl = List.takedrop (b1-1 ) s.s_node in - let s12, tl = List.takedrop (b2-b1) tl in - let s23, tl = List.takedrop (b3-b2) tl in + let target = try + resolve_gap_offset env (start, fin) info.offset s + with InvalidCPos -> + tc_error pf "invalid offset for swap" + in - check_swap pf env (stmt s12) (stmt s23); - stmt (List.flatten [hd; s23; s12; tl]) + match split_by_nmcgaps + (if target <= start + then [target; start; fin] + else [start; fin; target] + ) s + with + | [hd; s1; s2; tl] -> check_swap pf env (stmt s1) (stmt s2); + stmt (List.flatten [hd; s2; s1; tl]) + | _ -> assert false end (* -------------------------------------------------------------------- *) @@ -173,26 +117,25 @@ let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) = (process_swap1 { info with pl_desc = (Some `Right, pos)}) tc else - let env = FApi.tc1_env tc in let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in - - let process_codepos = - let env = EcEnv.Memory.push_active_ss me env in - fun p -> EcTyping.trans_codepos1 env p in - - let process_codeoffset (o : pcodeoffset1) : codeoffset1 = - match o with - | `ByOffset i -> `ByOffset i - | `ByPosition p -> `ByPosition (process_codepos p) in + let env = EcEnv.Memory.push_active_ss me (FApi.tc1_env tc) in let interval = - Option.map (fun (p1, p2) -> - let p1 = process_codepos p1 in - let p2 = Option.map process_codepos p2 in - (p1, p2) + Option.map (fun pcpor -> + EcTyping.trans_codepos_or_range ~memory:(fst me) env pcpor ) pos.interval in - let offset = process_codeoffset pos.offset in + let offset = EcTyping.trans_codegap_offset1 ~memory:(fst me) env pos.offset in + + let interval = match interval, offset with + | Some interval, _ -> interval + | None, GapRelative i -> + codegap_range_of_codepos + (if i > 0 then cpos_first else cpos_last) + | None, _ -> + tc_error (!!tc) "Cannot give a absolute offset and no range" + in + let kind : swap_kind = { interval; offset } in @@ -215,13 +158,15 @@ let process_interleave info tc = "invalide interleave range (%i + %i * %i <= %i)" pos1 k n1 pos2; + (* FIXME: should use t_swap and not process_swap; offset should use gap type *) let rec aux pos1 pos2 k tc = if k <= 0 then t_id tc else let data : pswap_kind = + (* Represent range [pos2, pos2+n2[ *) let p1 = (0, `ByPos pos2) in - let p2 = (0, `ByPos (pos2+n2-1)) in - let o = `ByOffset ((pos1+n1) - pos2) in - { interval = Some (p1, Some p2); offset = o; } in + let p2 = (0, `ByPos (pos2+n2)) in + let o = PGapRelative ((pos1+n1) - pos2) in + { interval = Some (Range ([], (GapBefore p1, GapBefore p2))); offset = o; } in FApi.t_seq (process_swap1 (mk_loc loc (side, data))) (aux (pos1+n1+n2) (pos2+n2) (k-1)) diff --git a/src/phl/ecPhlSwap.mli b/src/phl/ecPhlSwap.mli index 6b9c330d1..fc920cea7 100644 --- a/src/phl/ecPhlSwap.mli +++ b/src/phl/ecPhlSwap.mli @@ -6,8 +6,8 @@ open EcCoreGoal.FApi (* -------------------------------------------------------------------- *) type swap_kind = { - interval : (codepos1 * codepos1 option) option; - offset : codeoffset1; + interval : codegap_range; + offset : codegap_offset1; } (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 5fd61874c..75f3315c3 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -10,6 +10,7 @@ open EcParsetree open EcCoreGoal open EcLowPhlGoal open EcLowGoal +open EcMatching.Position module Sx = EcPath.Sx module TTC = EcProofTyping @@ -113,7 +114,8 @@ let t_ehoare_while inv tc = let m = EcMemory.memory hs.ehs_m in let e = ss_inv_of_expr m e in let tc = - FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in + (* FIXME: codepos should not be constructed inline *) + FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (GapBefore (0, `ByPos (List.length hs.ehs_s.s_node - 1))) inv tc) in FApi.t_sub [(EcPhlConseq.t_ehoareS_conseq inv (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not e) inv)) @+ [t_trivial; diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 535d93621..18085f706 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -1,5 +1,6 @@ (* -------------------------------------------------------------------- *) open EcUtils +open EcParsetree open EcPath open EcAst open EcModules @@ -7,6 +8,7 @@ open EcFol open EcCoreGoal open EcLowPhlGoal +open EcMatching.Position (* -------------------------------------------------------------------- *) module LowInternal = struct @@ -162,7 +164,9 @@ module TacInternal = struct if EcUtils.is_some i && not (List.is_empty rm) then tc_error !!tc "remaining %i instruction(s)" (List.length rm) - let t_hoare_wp ?(uselet=true) i tc = + (* [t_hoare_wp gap]: splits the statement at [gap]; instructions before the + gap are kept, wp is applied to instructions after the gap. *) + let t_hoare_wp ?(uselet=true) (i : codegap1 option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let hs = tc1_as_hoareS tc in @@ -177,7 +181,7 @@ module TacInternal = struct let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in FApi.xmutate1 tc `Wp [concl] - let t_ehoare_wp ?(uselet=true) i tc = + let t_ehoare_wp ?(uselet=true) (i : codegap1 option) tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in let (s_hd, s_wp) = o_split env i hs.ehs_s in @@ -189,7 +193,7 @@ module TacInternal = struct let concl = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s {m;inv=post} in FApi.xmutate1 tc `Wp [concl] - let t_bdhoare_wp ?(uselet=true) i tc = + let t_bdhoare_wp ?(uselet=true) (i : codegap1 option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let bhs = tc1_as_bdhoareS tc in @@ -204,7 +208,7 @@ module TacInternal = struct let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s {m;inv=post} bhs.bhs_cmp (bhs_bd bhs) in FApi.xmutate1 tc `Wp [concl] - let t_equiv_wp ?(uselet=true) ij tc = + let t_equiv_wp ?(uselet=true) (ij : (codegap1 * codegap1) option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let es = tc1_as_equivS tc in @@ -253,7 +257,11 @@ let t_wp_r ?(uselet=true) k g = let t_wp ?(uselet=true) = FApi.t_low1 "wp" (t_wp_r ~uselet) (* -------------------------------------------------------------------- *) -let process_wp pos tc = - let pos = - Option.map (EcTyping.trans_dcodepos1 (FApi.tc1_env tc)) pos - in t_wp pos tc +(* [process_wp gap]: splits the statement at [gap]; instructions before the + gap are kept, wp is applied to instructions after the gap. *) +let process_wp (cpos : pcodegap1 doption option) tc = + let env = (FApi.tc1_env tc) in + let cpos = + Option.map (EcTyping.trans_dcodegap1 env) cpos + in + t_wp cpos tc diff --git a/src/phl/ecPhlWp.mli b/src/phl/ecPhlWp.mli index fc8689f6d..c0017f578 100644 --- a/src/phl/ecPhlWp.mli +++ b/src/phl/ecPhlWp.mli @@ -12,6 +12,6 @@ open EcCoreGoal.FApi * soundness of the bounded hoare logic. *) -val t_wp : ?uselet:bool -> (codepos1 doption) option -> backward +val t_wp : ?uselet:bool -> (codegap1 doption) option -> backward -val process_wp : (pcodepos1 doption) option -> backward +val process_wp : (pcodegap1 doption) option -> backward diff --git a/tests/procchange.ec b/tests/procchange.ec index f656c52da..1aa18e7a6 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -150,10 +150,10 @@ theory ProcChangeInWhileEquiv. x <- x + 0 + 1; }. wp; skip. smt(). - proc change {1} [^while.1..^while.2] : { + proc change {1} ^while.:[1..2] : { x <- 2; }. wp; skip. smt(). - proc change {2} [^while.1-1] : { + proc change {2} ^while.:[1-1] : { x <- 2; }. wp; skip. smt(). abort.