From 81b6c4558ae19537c2a0ff7707d4782232df4d12 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 30 Oct 2024 11:14:56 +0100 Subject: [PATCH] fix "unroll for" failure (InvalidCPos) Keep a resolved version of the position so that it can be safely reused later. --- src/ecCorePrinting.ml | 2 ++ src/ecMatching.ml | 43 ++++++++++++++++++++++++++---------------- src/ecMatching.mli | 7 ++++++- src/ecPrinting.ml | 13 +++++++++++-- src/phl/ecPhlLoopTx.ml | 7 +++++-- 5 files changed, 51 insertions(+), 21 deletions(-) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index 299b7aa6e..a8187a70e 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -66,6 +66,8 @@ module type PrinterAPI = sig 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_typedecl : PPEnv.t -> (path * tydecl ) pp val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator ) pp diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 85ce3270c..867cf67ad 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -30,8 +30,8 @@ module Position = struct | `ByMatch of int option * cp_match ] - type codepos1 = int * cp_base - type codepos = (codepos1 * int) list * codepos1 + type codepos1 = int * cp_base + type codepos = (codepos1 * int) list * codepos1 type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1] let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = @@ -176,30 +176,41 @@ module Zipper = struct let (s, _) = split_at_cpos1 ~after:`No env cpos s in 1 + List.length s - let zipper_at_nm_cpos1 (env : EcEnv.env) ((cp1, sub) : codepos1 * int) s zpr = + let zipper_at_nm_cpos1 + (env : EcEnv.env) + ((cp1, sub) : codepos1 * int) + (s : stmt) + (zpr : ipath) + : (ipath * stmt) * (codepos1 * int) + = let (s1, i, s2) = find_by_cpos1 env cp1 s in + let zpr = + match i.i_node, sub with + | Swhile (e, sw), 0 -> + (ZWhile (e, ((s1, s2), zpr)), sw) - match i.i_node, sub with - | Swhile (e, sw), 0 -> - (ZWhile (e, ((s1, s2), zpr)), sw) - - | Sif (e, ifs1, ifs2), 0 -> - (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1) + | Sif (e, ifs1, ifs2), 0 -> + (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1) - | Sif (e, ifs1, ifs2), 1 -> - (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2) + | Sif (e, ifs1, ifs2), 1 -> + (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2) - | _ -> raise InvalidCPos + | _ -> raise InvalidCPos + in zpr, ((0, `ByPos (1 + List.length s1)), sub) - let zipper_of_cpos (env : EcEnv.env) ((nm, cp1) : codepos) s = - let zpr, s = - List.fold_left + let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) = + let (zpr, s), nm = + List.fold_left_map (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 env nm1 s zpr) (ZTop, s) nm in let s1, i, s2 = find_by_cpos1 env cp1 s in + let zpr = zipper s1 (i :: s2) zpr in + + (zpr, (nm, (0, `ByPos (1 + List.length s1)))) - zipper s1 (i :: s2) zpr + let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) = + fst (zipper_of_cpos_r env cp s) let split_at_cpos1 env cpos1 s = split_at_cpos1 ~after:`Auto env cpos1 s diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 651fb934e..c792f6ef7 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -73,7 +73,12 @@ module Zipper : sig val zipper : instr list -> instr list -> ipath -> zipper (* Return the zipper for the stmt [stmt] at code position [codepos]. - * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. *) + * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. It also + * returns a input code-position, but fully resolved (i.e. with absolute + * 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 : env -> codepos -> stmt -> zipper (* Zip the zipper, returning the corresponding statement *) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 88c8b23c4..4f51dc7a1 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -12,6 +12,7 @@ module P = EcPath module EP = EcParser module BI = EcBigInt module EI = EcInductive +module CP = EcMatching.Position module Ssym = EcSymbols.Ssym module Msym = EcSymbols.Msym @@ -2112,7 +2113,7 @@ let pp_scvar ppe fmt vs = pp_list "@ " pp_grp fmt vs (* -------------------------------------------------------------------- *) -let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : EcMatching.Position.codepos1) = +let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos1) = let s : string = match cp with | `ByPos i -> @@ -2141,11 +2142,19 @@ let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : EcMatching Format.fprintf fmt "%s%s%d" s (if off < 0 then "-" else "+") (abs off) (* -------------------------------------------------------------------- *) -let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : EcMatching.Position.codeoffset1) = +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 +(* -------------------------------------------------------------------- *) +let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) = + let pp_nm (fmt : Format.formatter) ((cp, i) : CP.codepos1 * int) = + Format.eprintf "%a%s" (pp_codepos1 ppe) cp (if i = 0 then "." else "?") + in + + Format.eprintf "%a%a" (pp_list "" pp_nm) nm (pp_codepos1 ppe) cp1 + (* -------------------------------------------------------------------- *) let pp_opdecl_pr (ppe : PPEnv.t) fmt (basename, ts, ty, op) = let ppe = PPEnv.add_locals ppe (List.map fst ts) in diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index f617b172c..973fe8a14 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -224,8 +224,12 @@ let process_unroll_for side cpos tc = let env = FApi.tc1_env tc in let hyps = FApi.tc1_hyps tc in let _, c = EcLowPhlGoal.tc1_get_stmt side tc in + + if not (List.is_empty (fst cpos)) then + tc_error !!tc "cannot use deep code position"; + let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in - let z = Zpr.zipper_of_cpos env cpos c in + let z, cpos = Zpr.zipper_of_cpos_r env cpos c in let pos = 1 + List.length z.Zpr.z_head in (* Extract loop condition / body *) @@ -323,7 +327,6 @@ let process_unroll_for side cpos tc = let cpos = EcMatching.Position.shift ~offset:(-1) cpos in let clen = blen * (List.length zs - 1) in - Format.eprintf "[W]%d %d@." blen (List.length zs); FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv (* -------------------------------------------------------------------- *)