From 137ba8cc9c8c91170db71a2585997ea2e1ce7403 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 13 Apr 2026 22:13:57 +0200 Subject: [PATCH] feat(phl): add `simplify if` tactic Merges conditional branches that share common code. Also extends `t_code_transform` to eHoare and adds `MatchByPos` branch selection. --- doc/tactics/simplify-if.rst | 142 ++++++++++++++++++++++++++++++++ examples/tactics/simplify_if.ec | 51 ++++++++++++ src/ecHiTacticals.ml | 1 + src/ecLowPhlGoal.ml | 21 +++-- src/ecMatching.ml | 50 ++++++++--- src/ecMatching.mli | 4 +- src/ecParser.mly | 3 + src/ecParsetree.ml | 1 + src/ecPrinting.ml | 3 +- src/phl/ecPhlCodeTx.ml | 113 +++++++++++++++++++++++-- src/phl/ecPhlCodeTx.mli | 2 +- src/phl/ecPhlLoopTx.ml | 8 +- 12 files changed, 369 insertions(+), 30 deletions(-) create mode 100644 doc/tactics/simplify-if.rst create mode 100644 examples/tactics/simplify_if.ec diff --git a/doc/tactics/simplify-if.rst b/doc/tactics/simplify-if.rst new file mode 100644 index 0000000000..9bc9896e77 --- /dev/null +++ b/doc/tactics/simplify-if.rst @@ -0,0 +1,142 @@ +======================================================================== +Tactic: ``simplify if`` +======================================================================== + +The ``simplify if`` transformation performs an if-conversion on program +statements, i.e., it rewrites ``if`` statements into conditional +expressions. This transformation preserves the program semantics. + +This conversion helps prevent the weakest precondition from growing +exponentially with the number of ``if`` statements. + +To illustrate this issue, consider the following example, which shows +how the weakest precondition can grow exponentially: + +.. ecproof:: + :title: Weakest precondition grows exponentially. + + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (*$*) time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *) + skip. + move => />. + smt(). + qed. + +Since the tactic preserves semantics, it can be applied to all program +logics. + +.. admonition:: Syntax + + ``simplify if side? codepos?`` + +The ``side`` argument is required when the goal is an ``equiv`` +judgment; it specifies on which side the transformation should be +applied. The ``codepos`` argument allows you to indicate which ``if`` +statement the transformation should target. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Variant: Transform at a given code position +------------------------------------------------------------------------ + +The tactic applies only if the branches of the selected ``if`` statement +consist solely of assignments. + +.. ecproof:: + :title: Hoare logic example selecting where to apply the transformation. + + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (* You can select a particular occurence of if using codepos *) + (*$*) simplify if ^if. (* Apply the transformation on the first if *) + simplify if ^if{2}. (* Apply the transformation on the second if *) + simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *) + time wp. + skip. + move => />. + smt(). + qed. + +------------------------------------------------------------------------ +Variant: Transform as much as possible +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``simplify if`` + +This variant attempts to find a position where the transformation can +be applied and applies it. The process is repeated until no applicable +position remains. + +.. ecproof:: + :title: Hoare logic example. + + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (*$*)simplify if. (* if instruction are transformed into single assignment *) + time wp. (* The size of the wp is now linear in the number of instruction *) + skip. + move => />. + smt(). + qed. diff --git a/examples/tactics/simplify_if.ec b/examples/tactics/simplify_if.ec new file mode 100644 index 0000000000..dbd011352f --- /dev/null +++ b/examples/tactics/simplify_if.ec @@ -0,0 +1,51 @@ +require import AllCore. + +module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } +}. + +hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *) + skip. + move => />. + smt(). +qed. + +hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + simplify if. (* if instruction are transformed into single assignment *) + time wp. (* The size of the wp is now linear in the number of instruction *) + skip. + move => />. + smt(). +qed. + +hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + (* You can select a particular occurence of if using codepos *) + simplify if ^if. (* Apply the transformation on the first if *) + simplify if ^if{2}. (* Apply the transformation on the second if *) + simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *) + time wp. + skip. + move => />. + smt(). +qed. diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 7c6da7e2e1..2a97475335 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pinterleave info -> EcPhlSwap.process_interleave info | Pcfold info -> EcPhlCodeTx.process_cfold info | Pkill info -> EcPhlCodeTx.process_kill info + | PsimplifyIf info -> EcPhlCodeTx.process_transform_if info | Pasgncase info -> EcPhlCodeTx.process_case info | Palias info -> EcPhlCodeTx.process_alias info | Pset info -> EcPhlCodeTx.process_set info diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 63da6bf64e..416bb15627 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -789,7 +789,7 @@ let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) ((me, Zpr.zip zpr, gs) : memenv * _ * form list) with InvalidCPos -> tc_error (fst cenv) "invalid code position" -let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = +let t_code_transform (side : oside) cpos tr tx tc = let pf = FApi.tc1_penv tc in match side with @@ -799,27 +799,32 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = match concl.f_node with | FhoareS hs -> let pr, po = hs_pr hs, hs_po hs in + (* FIXME: This is very suspicious why only main is provided ? *) let po = po.hsi_inv.main in let (me, stmt, cs) = tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in let concl = - f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs) + f_hoareS (snd me) pr stmt (hs_po hs) in FApi.xmutate1 tc (tr None) (cs @ [concl]) - | FbdHoareS bhs when bdhoare -> + | FbdHoareS bhs -> let pr, po = bhs_pr bhs, bhs_po bhs in let (me, stmt, cs) = tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in - let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs) - bhs.bhs_cmp (bhs_bd bhs) in + let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in + FApi.xmutate1 tc (tr None) (cs @ [concl]) + + | FeHoareS ehs -> + let pr, po = ehs_pr ehs, ehs_po ehs in + let (me, stmt, cs) = + tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in + let concl = f_eHoareS (snd me) pr stmt po in FApi.xmutate1 tc (tr None) (cs @ [concl]) | _ -> let kinds = - (if bdhoare then [`PHoare `Stmt] else []) - @ [`Hoare `Stmt] in - + [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in tc_error_noXhl ~kinds:kinds pf end diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 23d1acf0b2..29a4617cb0 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -68,7 +68,7 @@ module Position = struct *) (* Branch selection *) - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int] type nm_codepos_brsel = [`Cond of bool | `Match of int] (* Linear code position inside a block *) @@ -354,21 +354,23 @@ module Position = struct try List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst with Not_found -> raise InvalidCPos + let select_match_arm on_error env e (br:codepos_brsel) = + match br with + | `Match ms -> select_match_arm_idx env e ms + | `MatchByPos ix -> ix + | _ -> on_error () + (* 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 + | (Smatch (e, ss), _) -> + let ix = select_match_arm (fun _ -> assert false) env e br 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 + (env, s), `Match ix | _ -> assert false let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = @@ -515,6 +517,34 @@ module Position = struct 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) () + + let find_first_matching_instr (test : instr -> bool) (s : stmt) = + let exception Found of codepos in + + let rec find_pos rpath n (s : instr list) = + match s with + | [] -> () + | i :: s -> + if test i then raise (Found (List.rev rpath, cpos1 n)); + find_pos_sub rpath n i; + find_pos rpath (n + 1) s + + and find_pos_sub rpath n i = + match i.i_node with + | Sif (_, s1, s2) -> + find_pos ((cpos1 n, `Cond true ) :: rpath) 0 s1.s_node; + find_pos ((cpos1 n, `Cond false) :: rpath) 0 s2.s_node + | Swhile (_, s) -> + find_pos ((cpos1 n, `Cond true) :: rpath) 0 s.s_node + | Smatch (_, bs) -> + List.iteri (fun i (_, s) -> + find_pos ((cpos1 n, `MatchByPos i) :: rpath) 0 s.s_node + ) bs + | _ -> () + in + + try find_pos [] 0 s.s_node; None + with Found r -> Some r end (* -------------------------------------------------------------------- *) @@ -572,8 +602,8 @@ module Zipper = struct | Sif (e, ifs1, ifs2), `Cond false -> (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env - | Smatch (e, bs), `Match cn -> - let ix = select_match_arm_idx env e cn in + | Smatch (e, bs), _ -> + let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in let prebr, (locals, body), postbr = List.pivot_at ix bs in let env = EcEnv.Var.bind_locals locals env in (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env diff --git a/src/ecMatching.mli b/src/ecMatching.mli index d8a917ea2f..d13622e4d7 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -31,7 +31,7 @@ module Position : sig ] (* Branch selection *) - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int] type nm_codepos_brsel = [`Cond of bool | `Match of int] (* Linear code position inside a block *) @@ -218,6 +218,8 @@ module Position : sig val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool val nm_codepos1_in_nm_codegap1_range : nm_codepos1 -> nm_codegap1_range -> bool + + val find_first_matching_instr : (instr -> bool) -> stmt -> codepos option end (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index cb470f5162..7a044d45a1 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3119,6 +3119,9 @@ direction: | ALIAS s=side? x=lident CEQ p=sform_h AT o=codepos { Psetmatch (s, o, x, p) } +| SIMPLIFY IF s=side? o=codepos? + { PsimplifyIf (s, o) } + | WEAKMEM s=side? h=loc(ipcore_name) p=param_decl { Pweakmem(s, h, p) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 2068c5d05e..24d42a6672 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -802,6 +802,7 @@ type phltactic = | Poutline of outline_info | Pinterleave of interleave_info located | Pkill of (oside * pcodepos * int option) + | PsimplifyIf of (oside * pcodepos option) | Pasgncase of (oside * pcodepos) | Prnd of oside * psemrndpos option * rnd_tac_info_f | Prndsem of bool * oside * pcodegap1 diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index cbe75ad3f2..b5f4e20300 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2470,7 +2470,8 @@ let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) = (match br with | `Cond true -> "." | `Cond false -> "?" - | `Match cp -> Format.sprintf "#%s." cp) + | `Match cp -> Format.sprintf "#%s." cp + | `MatchByPos ix -> Format.sprintf "#%i" ix) 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 diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 5d49a34fc2..5f11d199c4 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -78,7 +78,7 @@ let t_kill_r side cpos olen tc = in let tr = fun side -> `Kill (side, cpos, olen) in - t_code_transform side ~bdhoare:true cpos tr (t_zip kill_stmt) tc + t_code_transform side cpos tr (t_zip kill_stmt) tc (* -------------------------------------------------------------------- *) let alias_stmt env id (pf, _) me i = @@ -109,7 +109,7 @@ let alias_stmt env id (pf, _) me i = let t_alias_r side cpos id g = let env = FApi.tc1_env g in let tr = fun side -> `Alias (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold (alias_stmt env id)) g + t_code_transform side cpos tr (t_fold (alias_stmt env id)) g (* -------------------------------------------------------------------- *) let set_stmt (fresh, id) e = @@ -136,7 +136,7 @@ let set_stmt (fresh, id) e = let t_set_r side cpos (fresh, id) e tc = let tr = fun side -> `Set (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_zip (set_stmt (fresh, id) e)) tc + t_code_transform side cpos tr (t_zip (set_stmt (fresh, id) e)) tc (* -------------------------------------------------------------------- *) let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) = @@ -181,7 +181,7 @@ let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) = let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc = let tr = fun side -> `SetMatch (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr + t_code_transform side cpos tr (t_zip (set_match_stmt id pattern)) tc (* -------------------------------------------------------------------- *) @@ -424,7 +424,7 @@ let t_cfold = 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 + t_code_transform side cpos tr (t_zip cb) tc (* -------------------------------------------------------------------- *) let t_kill = FApi.t_low3 "code-tx-kill" t_kill_r @@ -556,3 +556,106 @@ let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) = let concl = EcLowPhlGoal.hl_set_stmt side concl s in FApi.xmutate1 tc `ProcCase (goals @ [concl]) + +(* -------------------------------------------------------------------- *) +let transform_if pf (env : EcEnv.env) (e : expr) (s1 : stmt) (s2 : stmt) = + let mod1 = s_write env s1 in + let mod2 = s_write env s2 in + let modv, modg = PV.elements (PV.union mod1 mod2) in + + if not (List.is_empty modg) then + tc_error pf "the branches modify global variables"; + + if List.is_empty modv then [] else + + let upd (m : (expr, unit) Mpv.t) (x : prog_var) (e : expr) = + Mpv.add env x e (Mpv.remove env x m) + in + + let init = + List.fold_left + (fun m (x, ty) -> Mpv.add env x (e_var x ty) m) + Mpv.empty modv + in + + let transform_v m (x, ty) = + let x' = EcIdent.create (symbol_of_pv x) in + upd m x (e_local x' ty), (x', ty) in + + let transform_lv m lv = + match lv with + | LvVar (x, ty) -> + let m, (x', ty) = transform_v m (x, ty) in + m, LSymbol (x', ty) + | LvTuple xs -> + let m, xs' = List.map_fold transform_v m xs in + m, LTuple xs' in + + let transform_i m i = + let lv, e = destr_asgn i in + let e = Mpv.esubst env m e in + let m, lp = transform_lv m lv in + m, (lp, e) in + + let transform_s (s : stmt) = + List.map_fold transform_i init s.s_node in + + let m1, bd1 = transform_s s1 in + let m2, bd2 = transform_s s2 in + + let es = + let e_if (x, ty) = + let ex = e_var x ty in + e_if e (Mpv.esubst env m1 ex) (Mpv.esubst env m2 ex) in + e_tuple (List.map e_if modv) in + + let add_binding bd es = + List.fold_right (fun (lp, e) es -> e_let lp e es) bd es in + + let es = add_binding bd1 (add_binding bd2 es) in + [i_asgn (oget (lv_of_list modv), es)] + +(* -------------------------------------------------------------------- *) +let transform_if_stmt env (pf, _) me i = + match i.i_node with + | Sif (e, s1, s2) -> + if not (List.for_all is_asgn s1.s_node) then + tc_error pf "the then branch contains intruction that are not assignments"; + if not (List.for_all is_asgn s2.s_node) then + tc_error pf "the else branch contains intruction that are not assignments"; + (me, transform_if pf env e s1 s2) + | _ -> + tc_error pf "the given position does not correspond to an if instruction" + +(* -------------------------------------------------------------------- *) +let t_transform_if_r side cpos g = + let env = FApi.tc1_env g in + let tr = fun side -> `TransformIf (side, cpos) in + t_code_transform side cpos tr (t_fold (transform_if_stmt env)) g + +let t_transform_if = FApi.t_low2 "code-tx-transform_if" t_transform_if_r + +(* -------------------------------------------------------------------- *) +let t_transform_if_rec1 side g = + let (_, s) = tc1_get_stmt side g in + let test i = + match i.i_node with + | Sif (_, s1, s2) -> + List.for_all is_asgn s1.s_node && List.for_all is_asgn s2.s_node + | _ -> false + in + match Position.find_first_matching_instr test s with + | Some cpos -> t_transform_if side cpos g + | None -> tc_error (!!g) "no more transformation" + +let t_transform_if_rec side g = + FApi.t_repeat (t_transform_if_rec1 side) g + +(* -------------------------------------------------------------------- *) +let process_transform_if (side, cpos) tc = + match cpos with + | None -> + t_transform_if_rec side tc + | Some cpos -> + let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in + t_transform_if side cpos tc diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli index 468b4b0562..3bbd6e1cf8 100644 --- a/src/phl/ecPhlCodeTx.mli +++ b/src/phl/ecPhlCodeTx.mli @@ -21,6 +21,6 @@ val process_set : oside * pcodepos * bool * psymbol * pexpr -> backward val process_set_match : oside * pcodepos * psymbol * pformula -> backward val process_cfold : pcfold -> backward val process_case : oside * pcodepos -> backward - +val process_transform_if : oside * pcodepos option -> backward (* -------------------------------------------------------------------- *) val process_weakmem : (oside * psymbol * fun_params) -> backward diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 71f33072dc..a1727ff94a 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -115,7 +115,7 @@ let fission_stmt (il, (d1, d2)) (pf, hyps) me zpr = let t_fission_r side cpos infos g = let tr = fun side -> `LoopFission (side, cpos, infos) in let cb = fun cenv _ me zpr -> fission_stmt infos cenv me zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g + t_code_transform side cpos tr (t_zip cb) g let t_fission = FApi.t_low3 "loop-fission" t_fission_r @@ -170,7 +170,7 @@ let fusion_stmt (il, (d1, d2)) (pf, hyps) me zpr = let t_fusion_r side cpos infos g = let tr = fun side -> `LoopFusion (side, cpos, infos) in let cb = fun cenv _ me zpr -> fusion_stmt infos cenv me zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g + t_code_transform side cpos tr (t_zip cb) g let t_fusion = FApi.t_low3 "loop-fusion" t_fusion_r @@ -182,7 +182,7 @@ let unroll_stmt (pf, _) me i = let t_unroll_r side cpos g = let tr = fun side -> `LoopUnraoll (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold unroll_stmt) g + t_code_transform side cpos tr (t_fold unroll_stmt) g let t_unroll = FApi.t_low2 "loop-unroll" t_unroll_r @@ -199,7 +199,7 @@ let splitwhile_stmt b (pf, _) me i = let t_splitwhile_r b side cpos g = let tr = fun side -> `SplitWhile (b, side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold (splitwhile_stmt b)) g + t_code_transform side cpos tr (t_fold (splitwhile_stmt b)) g let t_splitwhile = FApi.t_low3 "split-while" t_splitwhile_r