From ee89281d322a8f785e730d4b270a9bae5321e6b8 Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Mon, 4 Aug 2025 09:15:13 +0200 Subject: [PATCH] Add exception declaration, raise, and update logic --- examples/exception.ec | 102 ++++++++ src/ecAst.ml | 101 +++++--- src/ecAst.mli | 22 +- src/ecCallbyValue.ml | 16 +- src/ecCommands.ml | 44 ++-- src/ecCoreFol.ml | 59 +++-- src/ecCoreFol.mli | 5 +- src/ecCoreModules.ml | 17 +- src/ecCoreModules.mli | 8 +- src/ecCorePrinting.ml | 31 +-- src/ecCoreSubst.ml | 19 +- src/ecDecl.ml | 14 ++ src/ecDecl.mli | 8 + src/ecEnv.ml | 66 ++++- src/ecEnv.mli | 12 +- src/ecLexer.mll | 3 +- src/ecLowPhlGoal.ml | 50 ++-- src/ecMatching.ml | 31 ++- src/ecPV.ml | 11 +- src/ecParser.mly | 63 ++++- src/ecParsetree.ml | 24 +- src/ecPath.ml | 10 +- src/ecPath.mli | 1 + src/ecPrinting.ml | 99 +++++--- src/ecProcSem.ml | 2 +- src/ecReduction.ml | 18 +- src/ecScope.ml | 42 +++- src/ecScope.mli | 5 + src/ecSection.ml | 55 ++++- src/ecSubst.ml | 36 ++- src/ecThCloning.ml | 4 +- src/ecTheory.ml | 1 + src/ecTheory.mli | 1 + src/ecTheoryReplay.ml | 13 +- src/ecTyping.ml | 84 ++++++- src/ecTyping.mli | 5 + src/ecUnifyProc.ml | 21 +- src/ecUserMessages.ml | 5 +- src/phl/ecPhlApp.ml | 21 +- src/phl/ecPhlCall.ml | 147 ++++++++--- src/phl/ecPhlCall.mli | 2 +- src/phl/ecPhlCase.ml | 13 +- src/phl/ecPhlCodeTx.ml | 8 +- src/phl/ecPhlConseq.ml | 513 +++++++++++++++++++++++++++------------ src/phl/ecPhlConseq.mli | 12 +- src/phl/ecPhlCoreView.ml | 4 +- src/phl/ecPhlEager.ml | 20 +- src/phl/ecPhlEqobs.ml | 20 +- src/phl/ecPhlExists.ml | 20 +- src/phl/ecPhlFel.ml | 8 +- src/phl/ecPhlFun.ml | 17 +- src/phl/ecPhlInline.ml | 4 +- src/phl/ecPhlLoopTx.ml | 14 +- src/phl/ecPhlRCond.ml | 24 +- src/phl/ecPhlRnd.ml | 24 +- src/phl/ecPhlRwPrgm.ml | 4 +- src/phl/ecPhlSp.ml | 9 +- src/phl/ecPhlUpto.ml | 5 +- src/phl/ecPhlWhile.ml | 37 ++- src/phl/ecPhlWp.ml | 37 +-- 60 files changed, 1518 insertions(+), 553 deletions(-) create mode 100644 examples/exception.ec diff --git a/examples/exception.ec b/examples/exception.ec new file mode 100644 index 0000000000..44276a1861 --- /dev/null +++ b/examples/exception.ec @@ -0,0 +1,102 @@ +require import AllCore. + +exception assume. +exception assert. + +module M' ={ + proc truc (x:int) : int = { + if (x = 3) { + raise assume; + } + if (x=3) { + raise assert; + } + return x; + } +}. + +op p7: bool. +op p1: bool. +op p2: bool. +op p3: bool. + +lemma assume_assert : +hoare [M'.truc : p7 ==> p3 | assume:p1 |assert: p2 ]. + proof. +admitted. + +op p8: bool. +op q1: bool. +op q2: bool. +op q3: bool. + +lemma assert_assume : +hoare [M'.truc : p8 ==> q3 | assume:q1 |assert: q2 ]. + proof. +admitted. + +op p4: bool. +op p5: bool. +op p6: bool. +op p9: bool. +lemma assert_assume' : +hoare [M'.truc : p9 ==> p4 | assume:p6 |assert: p5 ]. + proof. + conseq (assume_assert) (assert_assume). + + admit. + + admit. + + admit. + + admit. + qed. + +exception e1. +exception e2. +exception e3. + +module M ={ + proc f1 (x:int) : int = { + if (x = 3) { + raise e1; + } else { + x <- 5; + } + return x; + } + + proc f2 (x:int) : int = { + if (x = 3) { + x <- x; + x <@ f1(x); + } else { + x <@ f1(x); + } + return x; + } +}. + + +(* Multiple time post for the same exception *) + +lemma l_f1 (_x: int): +hoare [M.f1 : _x = x ==> (4 < res) | e1:_x = 3 | e2:false ]. + proof. + proc. + conseq (: _ ==> x = 5 | e1: p1 | e2: p2 ). + + auto. + + auto. admit. + + admit. + + admit. + qed. + +lemma l_f2 (_x: int): +hoare [M.f2 : p9 ==> p4 | e1: p2 | e2:p1 | e3: p6 ]. + proof. + proc. + if. + + call (: p5 ==> p3 | e1 : p9 | e2: p7). + proc. + wp. + admit. + + admit. + + call (l_f1 _x);auto. admit. + qed. diff --git a/src/ecAst.ml b/src/ecAst.ml index aa9b6011ac..4079c371dc 100644 --- a/src/ecAst.ml +++ b/src/ecAst.ml @@ -115,7 +115,7 @@ and instr_node = | Sif of expr * stmt * stmt | Swhile of expr * stmt | Smatch of expr * ((EcIdent.t * ty) list * stmt) list - | Sassert of expr + | Sraise of EcPath.path * expr list | Sabstract of EcIdent.t and stmt = { @@ -234,19 +234,23 @@ and equivS = { es_sr : stmt; es_po : form; } +and post = (EcPath.path * form) list + and sHoareF = { hf_m : memory; hf_pr : form; hf_f : EcPath.xpath; hf_po : form; + hf_poe : post } and sHoareS = { - hs_m : memenv; - hs_pr : form; - hs_s : stmt; - hs_po : form; } - + hs_m : memenv; + hs_pr : form; + hs_s : stmt; + hs_po : form; + hs_poe : post +} and eHoareF = { ehf_m : memory; @@ -292,7 +296,7 @@ and pr = { pr_event : ss_inv; } -let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv = +let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv = let m' = match m with | Some m -> m | None -> (List.hd invs).m in @@ -318,7 +322,7 @@ let map_ss_inv_destr2 (fn: form -> form * form) (inv: ss_inv): ss_inv * ss_inv = let inv1, inv2 = fn inv.inv in let m = inv.m in (* Everything should be boolean *) - assert (inv1.f_ty = inv2.f_ty && inv1.f_ty = inv.inv.f_ty); + assert (inv1.f_ty = inv2.f_ty && inv1.f_ty = inv.inv.f_ty); {m;inv=inv1}, {m;inv=inv2} let map_ss_inv_destr3 (fn: form -> form * form * form) (inv: ss_inv): ss_inv * ss_inv * ss_inv = @@ -335,11 +339,11 @@ type ts_inv = { } let map_ts_inv ?ml ?mr (fn: form list -> form) (invs: ts_inv list): ts_inv = - let ml' = match ml with - | Some m -> m + let ml' = match ml with + | Some m -> m | None -> (List.hd invs).ml in - let mr' = match mr with - | Some m -> m + let mr' = match mr with + | Some m -> m | None -> (List.hd invs).mr in let inv = fn (List.map (fun {inv;ml;mr} -> assert (ml = ml' && mr = mr'); inv) invs) in { ml = ml'; mr = mr'; inv = inv } @@ -432,7 +436,7 @@ let ts_inv_lower_left2 (fn: ss_inv -> ss_inv -> form) (inv1: ts_inv) inv2 = assert (inv1.mr = inv2.mr); let inv' = fn {m=inv1.ml; inv=inv1.inv} {m=inv2.ml; inv=inv2.inv} in { m = inv1.mr; inv = inv' } - + let ts_inv_lower_left3 (fn: ss_inv -> ss_inv -> ss_inv -> form) (inv1: ts_inv) (inv2: ts_inv) (inv3: ts_inv): ss_inv = assert (inv1.mr = inv2.mr && inv2.mr = inv3.mr); @@ -512,11 +516,11 @@ let map_inv (fn: form list -> form) (inv: inv list): inv = assert (List.length inv > 0); match List.hd inv with | Inv_ss ss' -> - Inv_ss (map_ss_inv fn (List.map (function + Inv_ss (map_ss_inv fn (List.map (function Inv_ss ss -> assert (ss.m = ss'.m); ss | _ -> failwith "expected all invariants to have same kind") inv)) | Inv_ts ts' -> - Inv_ts (map_ts_inv fn (List.map (function + Inv_ts (map_ts_inv fn (List.map (function Inv_ts ts -> assert (ts.ml = ts'.ml && ts.mr = ts'.mr); ts | _ -> failwith "expected all invariants to have same kind") inv)) @@ -535,7 +539,7 @@ let map_inv2 (fn: form -> form -> form) (inv1: inv) (inv2: inv): inv = Inv_ts (map_ts_inv2 fn ts1 ts2) | _ -> failwith "incompatible invariants for map_inv2" - + let map_inv3 (fn: form -> form -> form -> form) (inv1: inv) (inv2: inv) (inv3: inv): inv = match inv1, inv2, inv3 with @@ -559,11 +563,13 @@ let ef_po ef = {ml=ef.ef_ml; mr=ef.ef_mr; inv=ef.ef_po} let es_pr es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_pr} let es_po es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_po} -let hf_pr hf = {m=hf.hf_m; inv=hf.hf_pr} -let hf_po hf = {m=hf.hf_m; inv=hf.hf_po} +let hf_pr hf = {m=hf.hf_m; inv=hf.hf_pr} +let hf_po hf = {m=hf.hf_m; inv=hf.hf_po} +let hf_poe hf = List.map (fun (e,f) -> e,{m=hf.hf_m; inv=f}) hf.hf_poe let hs_pr hs = {m=fst hs.hs_m; inv=hs.hs_pr} let hs_po hs = {m=fst hs.hs_m; inv=hs.hs_po} +let hs_poe hs = List.map (fun (e,f) -> e,{m=fst hs.hs_m; inv=f}) hs.hs_poe let ehf_pr ehf = {m=ehf.ehf_m; inv=ehf.ehf_pr} let ehf_po ehf = {m=ehf.ehf_m; inv=ehf.ehf_po} @@ -916,14 +922,26 @@ let b_hash (bs : bindings) = Why3.Hashcons.combine_list b1_hash 0 bs (*-------------------------------------------------------------------- *) + +let post_equal (e1, f1) (e2,f2) = + EcPath.p_equal e1 e2 && + f_equal f1 f2 + +let posts_equal posts1 posts2 = + List.equal post_equal posts1 posts2 + +(*-------------------------------------------------------------------- *) + let hf_equal hf1 hf2 = f_equal hf1.hf_pr hf2.hf_pr + && posts_equal hf1.hf_poe hf2.hf_poe && f_equal hf1.hf_po hf2.hf_po && EcPath.x_equal hf1.hf_f hf2.hf_f && mem_equal hf1.hf_m hf2.hf_m let hs_equal hs1 hs2 = f_equal hs1.hs_pr hs2.hs_pr + && posts_equal hs1.hs_poe hs2.hs_poe && f_equal hs1.hs_po hs2.hs_po && s_equal hs1.hs_s hs2.hs_s && me_equal hs1.hs_m hs2.hs_m @@ -989,14 +1007,28 @@ let pr_equal pr1 pr2 = && f_equal pr1.pr_args pr2.pr_args && mem_equal pr1.pr_event.m pr2.pr_event.m +(*-------------------------------------------------------------------- *) + +let post_hash (e, f) = +Why3.Hashcons.combine + (EcPath.p_hash e) + (f_hash f) + +let posts_hash posts = + Why3.Hashcons.combine_list post_hash 0 posts + (* -------------------------------------------------------------------- *) let hf_hash hf = Why3.Hashcons.combine3 - (f_hash hf.hf_pr) (f_hash hf.hf_po) (EcPath.x_hash hf.hf_f) (mem_hash hf.hf_m) + (f_hash hf.hf_pr) + (Why3.Hashcons.combine (f_hash hf.hf_po) (posts_hash hf.hf_poe)) + (EcPath.x_hash hf.hf_f) + (mem_hash hf.hf_m) let hs_hash hs = Why3.Hashcons.combine3 - (f_hash hs.hs_pr) (f_hash hs.hs_po) + (f_hash hs.hs_pr) + (Why3.Hashcons.combine (f_hash hs.hs_po) (posts_hash hs.hs_poe)) (s_hash hs.hs_s) (me_hash hs.hs_m) @@ -1025,7 +1057,7 @@ let bhs_hash bhs = [bhs.bhs_pr;bhs.bhs_po;bhs.bhs_bd] let ef_hash ef = - Why3.Hashcons.combine_list f_hash + Why3.Hashcons.combine_list f_hash (Why3.Hashcons.combine3 (EcPath.x_hash ef.ef_fl) (EcPath.x_hash ef.ef_fr) (mem_hash ef.ef_ml) (mem_hash ef.ef_mr)) [ef.ef_pr;ef.ef_po] @@ -1344,6 +1376,11 @@ module Hsform = Why3.Hashcons.Make (struct let fv_mlr ml mr = Sid.add ml (Sid.singleton mr) + let posts_fv init posts = + List.fold + (fun acc (_,f) -> fv_union (f_fv f) acc) + init posts + let fv_node f = let union ex nodes = List.fold_left (fun s a -> fv_union s (ex a)) Mid.empty nodes @@ -1371,11 +1408,13 @@ module Hsform = Why3.Hashcons.Make (struct fv_union (f_fv f1) fv2 | FhoareF hf -> - let fv = fv_union (f_fv hf.hf_pr) (f_fv hf.hf_po) in + let fv = f_fv hf.hf_po in + let fv = fv_union (f_fv hf.hf_pr) (posts_fv fv hf.hf_poe) in EcPath.x_fv (Mid.remove hf.hf_m fv) hf.hf_f | FhoareS hs -> - let fv = fv_union (f_fv hs.hs_pr) (f_fv hs.hs_po) in + let fv = f_fv hs.hs_po in + let fv = fv_union (f_fv hs.hs_pr) (posts_fv fv hs.hs_poe) in fv_union (s_fv hs.hs_s) (Mid.remove (fst hs.hs_m) fv) | FeHoareF hf -> @@ -1470,8 +1509,9 @@ module Hinstr = Why3.Hashcons.Make (struct in List.all2 forbs bs1 bs2 && s_equal s1 s2 in e_equal e1 e2 && List.all2 forb b1 b2 - | Sassert e1, Sassert e2 -> - (e_equal e1 e2) + | Sraise (e1, es1), Sraise (e2, es2) -> + (EcPath.p_equal e1 e2) + && (List.all2 e_equal es1 es2) | Sabstract id1, Sabstract id2 -> EcIdent.id_equal id1 id2 @@ -1509,7 +1549,10 @@ module Hinstr = Why3.Hashcons.Make (struct in Why3.Hashcons.combine_list forbs (s_hash s) bds in Why3.Hashcons.combine_list forb (e_hash e) b - | Sassert e -> e_hash e + | Sraise (e, tys) -> + Why3.Hashcons.combine_list e_hash + (EcPath.p_hash e) + tys | Sabstract id -> EcIdent.id_hash id @@ -1543,8 +1586,10 @@ module Hinstr = Why3.Hashcons.Make (struct (fun s b -> EcIdent.fv_union s (forb b)) (e_fv e) b - | Sassert e -> - e_fv e + | Sraise (_, args) -> + List.fold_left + (fun s a -> EcIdent.fv_union s (e_fv a)) + Mid.empty args | Sabstract id -> EcIdent.fv_singleton id diff --git a/src/ecAst.mli b/src/ecAst.mli index 6da2cff790..13b507c0ed 100644 --- a/src/ecAst.mli +++ b/src/ecAst.mli @@ -111,7 +111,7 @@ and instr_node = | Sif of expr * stmt * stmt | Swhile of expr * stmt | Smatch of expr * ((EcIdent.t * ty) list * stmt) list - | Sassert of expr + | Sraise of EcPath.path * expr list | Sabstract of EcIdent.t and stmt = private { @@ -201,7 +201,7 @@ and f_node = | Fpr of pr (* hr *) -(* We use the alert system for privacy because we want to +(* We use the alert system for privacy because we want to permit access in *some* instances, and the other fields are fine *) (* This is to ensure that memory bindings are carried along with the invariants *) and eagerF = { @@ -239,13 +239,17 @@ and equivS = { [@alert priv_pl "Use the accessor function `es_po` instead of the field"] } +and post = (EcPath.path * form) list + and sHoareF = { hf_m : memory; hf_pr : form; [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"] hf_f : EcPath.xpath; hf_po : form; - [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"] + [@alert priv_pl "Use the accessor function `hf_po` instead of the field"] + hf_poe : post; + [@alert priv_pl "Use the accessor function `hf_poe` instead of the field"] } and sHoareS = { @@ -255,6 +259,8 @@ and sHoareS = { hs_s : stmt; hs_po : form; [@alert priv_pl "Use the accessor function `hs_po` instead of the field"] + hs_poe : post; + [@alert priv_pl "Use the accessor function `hs_poe` instead of the field"] } @@ -336,13 +342,13 @@ val map_ts_inv3 : (form -> form -> form -> form) -> ts_inv -> ts_inv -> ts_inv - val map_ts_inv_left : (ss_inv list -> ss_inv) -> ts_inv list -> ts_inv val map_ts_inv_left1 : (ss_inv -> ss_inv) -> ts_inv -> ts_inv val map_ts_inv_left2 : (ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv -val map_ts_inv_left3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> +val map_ts_inv_left3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv -> ts_inv val map_ts_inv_right : (ss_inv list -> ss_inv) -> ts_inv list -> ts_inv val map_ts_inv_right1 : (ss_inv -> ss_inv) -> ts_inv -> ts_inv val map_ts_inv_right2 : (ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv -val map_ts_inv_right3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> +val map_ts_inv_right3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv -> ts_inv val map_ts_inv_destr2 : (form -> form * form) -> ts_inv -> ts_inv * ts_inv @@ -351,13 +357,13 @@ val map_ts_inv_destr3 : (form -> form * form * form) -> ts_inv -> ts_inv * ts_in val ts_inv_lower_left : (ss_inv list -> form) -> ts_inv list -> ss_inv val ts_inv_lower_left1 : (ss_inv -> form) -> ts_inv -> ss_inv val ts_inv_lower_left2 : (ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ss_inv -val ts_inv_lower_left3 : (ss_inv -> ss_inv -> ss_inv -> form) -> +val ts_inv_lower_left3 : (ss_inv -> ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ts_inv -> ss_inv val ts_inv_lower_right : (ss_inv list -> form) -> ts_inv list -> ss_inv val ts_inv_lower_right1 : (ss_inv -> form) -> ts_inv -> ss_inv val ts_inv_lower_right2 : (ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ss_inv -val ts_inv_lower_right3 : (ss_inv -> ss_inv -> ss_inv -> form) -> +val ts_inv_lower_right3 : (ss_inv -> ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ts_inv -> ss_inv (* -------------------------------------------------------------------- *) @@ -390,8 +396,10 @@ val es_pr : equivS -> ts_inv val es_po : equivS -> ts_inv val hf_pr : sHoareF -> ss_inv val hf_po : sHoareF -> ss_inv +val hf_poe : sHoareF -> (EcPath.path * ss_inv) list val hs_pr : sHoareS -> ss_inv val hs_po : sHoareS -> ss_inv +val hs_poe : sHoareS -> (EcPath.path * ss_inv) list val ehf_pr : eHoareF -> ss_inv val ehf_po : eHoareF -> ss_inv val ehs_pr : eHoareS -> ss_inv diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml index f65c8f25e6..a65e4a0288 100644 --- a/src/ecCallbyValue.ml +++ b/src/ecCallbyValue.ml @@ -223,7 +223,7 @@ and try_reduce_record_projection try if not ( - st.st_ri.iota + st.st_ri.iota && EcEnv.Op.is_projection st.st_env p && not (Args.isempty args) ) then raise Bailout; @@ -485,7 +485,12 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form = let hf_po = norm st s (hf_po hf).inv in let hf_f = norm_xfun st s hf.hf_f in let (m,_) = norm_me s (abstract hf.hf_m) in - f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po} + let hf_poe = + List.map + (fun (e,(f:ss_inv)) -> e, {m;inv=norm st s f.inv}) + (hf_poe hf) + in + f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po} hf_poe | FhoareS hs -> assert (Args.isempty args); @@ -495,7 +500,12 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form = let hs_s = norm_stmt s hs.hs_s in let hs_m = norm_me s hs.hs_m in let m = fst hs_m in - f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po} + let hs_poe = + List.map + (fun (e,(f:ss_inv)) -> e, {m;inv=norm st s f.inv}) + (hs_poe hs) + in + f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po} hs_poe | FeHoareF hf -> assert (Args.isempty args); diff --git a/src/ecCommands.ml b/src/ecCommands.ml index f2da6001d7..147c083777 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -262,17 +262,17 @@ module HiPrinting = struct let pr_axioms (fmt : Format.formatter) (env : EcEnv.env) = let ax = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env in let ppe0 = EcPrinting.PPEnv.ofenv env in - EcPrinting.pp_by_theory ppe0 (EcPrinting.pp_axiom) fmt ax + EcPrinting.pp_by_theory ppe0 (EcPrinting.pp_axiom) fmt ax let pr_hint_solve (fmt : Format.formatter) (env : EcEnv.env) = let hint_solve = EcEnv.Auto.all env in let hint_solve = List.map (fun (p, mode) -> let ax = EcEnv.Ax.by_path p env in (p, (ax, mode)) - ) hint_solve in - + ) hint_solve in + let ppe = EcPrinting.PPEnv.ofenv env in - + let pp_hint_solve ppe fmt = (fun (p, (ax, mode)) -> let mode = match mode with @@ -281,8 +281,8 @@ module HiPrinting = struct Format.fprintf fmt "%a %s" (EcPrinting.pp_axiom ppe) (p, ax) mode ) in - - EcPrinting.pp_by_theory ppe pp_hint_solve fmt hint_solve + + EcPrinting.pp_by_theory ppe pp_hint_solve fmt hint_solve (* ------------------------------------------------------------------ *) let pr_hint_rewrite (fmt : Format.formatter) (env : EcEnv.env) = @@ -302,13 +302,13 @@ module HiPrinting = struct if List.is_empty elems then Format.fprintf fmt "%s (empty)@." (EcPath.basename p) else - Format.fprintf fmt "@[%s = @\n%a@]@\n" (EcPath.basename p) - (EcPrinting.pp_list "@\n" (fun fmt p -> + Format.fprintf fmt "@[%s = @\n%a@]@\n" (EcPath.basename p) + (EcPrinting.pp_list "@\n" (fun fmt p -> Format.fprintf fmt "%a" pp_path p)) (EcPath.Sp.ntr_elements sp) ) in - + EcPrinting.pp_by_theory ppe pp_hint_rewrite fmt hint_rewrite (* ------------------------------------------------------------------ *) @@ -317,17 +317,17 @@ module HiPrinting = struct let (hint_simplify: (EcEnv.Reduction.topsym * rule list) list) = EcEnv.Reduction.all env in - let hint_simplify = List.filter_map (fun (ts, rl) -> + let hint_simplify = List.filter_map (fun (ts, rl) -> match ts with - | `Path p -> Some (p, rl) + | `Path p -> Some (p, rl) | _ -> None - ) hint_simplify + ) hint_simplify in - + let ppe = EcPrinting.PPEnv.ofenv env in - + let pp_hint_simplify ppe fmt = (fun (p, (rls : rule list)) -> - Format.fprintf fmt "@[%s:@\n%a@]" (EcPath.basename p) + Format.fprintf fmt "@[%s:@\n%a@]" (EcPath.basename p) (EcPrinting.pp_list "@\n" (fun fmt rl -> begin match rl.rl_cond with | [] -> Format.fprintf fmt "Conditions: None@\n" @@ -340,7 +340,7 @@ module HiPrinting = struct rls ) in - + EcPrinting.pp_by_theory ppe pp_hint_simplify fmt hint_simplify end @@ -454,6 +454,15 @@ and process_operator (scope : EcScope.scope) (pop : poperator located) = List.iter (fun s -> EcScope.notify scope `Info "added axiom: `%s'" s) axs; scope +(* -------------------------------------------------------------------- *) +and process_exception (scope : EcScope.scope) (ed : pexception_decl located) = + EcScope.check_state `InTop "exception" scope; + let e, scope = EcScope.Except.add scope ed in + let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in + EcScope.notify scope `Info "added exception %s %a" + (unloc ed.pl_desc.pe_name) (EcPrinting.pp_added_except ppe) e; + scope + (* -------------------------------------------------------------------- *) and process_procop (scope : EcScope.scope) (pop : pprocop located) = EcScope.check_state `InTop "operator" scope; @@ -557,7 +566,7 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) = try_finally (fun () -> let commands = EcIo.parseall (EcIo.from_file filename) in let commands = - List.fold_left + List.fold_left (fun scope g -> process_internal subld scope g.gl_action) iscope commands in commands) @@ -761,6 +770,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g = | Gmodule m -> `Fct (fun scope -> process_module scope m) | Ginterface i -> `Fct (fun scope -> process_interface scope i) | Goperator o -> `Fct (fun scope -> process_operator scope (mk_loc loc o)) + | Gexception e -> `Fct (fun scope -> process_exception scope (mk_loc loc e)) | Gprocop o -> `Fct (fun scope -> process_procop scope (mk_loc loc o)) | Gpredicate p -> `Fct (fun scope -> process_predicate scope (mk_loc loc p)) | Gnotation n -> `Fct (fun scope -> process_notation scope (mk_loc loc n)) diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 03dd1f64ec..6c595b8e10 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -269,14 +269,29 @@ let f_eqs fs1 fs2 = let f_hoareS_r hs = mk_form (FhoareS hs) tbool let f_hoareF_r hf = mk_form (FhoareF hf) tbool -let f_hoareS hs_mt hs_pr hs_s hs_po = +let f_hoareS hs_mt hs_pr hs_s hs_po hs_poe = assert (hs_pr.m = hs_po.m); - f_hoareS_r { hs_m=(hs_pr.m, hs_mt); hs_pr=hs_pr.inv; hs_s; - hs_po=hs_po.inv; } [@alert "-priv_pl"] - -let f_hoareF pr hf_f po = + List.iter (fun (_,f) -> assert (hs_pr.m = f.m)) hs_poe; + let hs_poe = List.map (fun (e,(f:ss_inv)) -> (e, f.inv)) hs_poe in + f_hoareS_r + { hs_m=(hs_pr.m, hs_mt); + hs_pr=hs_pr.inv; + hs_s; + hs_po=hs_po.inv; + hs_poe=hs_poe + } [@alert "-priv_pl"] + +let f_hoareF pr hf_f po poe = assert (pr.m = po.m); - f_hoareF_r { hf_m=pr.m; hf_pr=pr.inv; hf_f; hf_po=po.inv; } [@alert "-priv_pl"] + List.iter (fun (_,f) -> assert (pr.m = f.m)) poe; + let hf_poe = List.map (fun (e,(f:ss_inv)) -> (e, f.inv)) poe in + f_hoareF_r + { hf_m=pr.m; + hf_pr=pr.inv; + hf_f; + hf_po=po.inv; + hf_poe=hf_poe + } [@alert "-priv_pl"] (* -------------------------------------------------------------------- *) let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool @@ -284,7 +299,7 @@ let f_eHoareF_r hf = mk_form (FeHoareF hf) tbool let f_eHoareS ehs_mt ehs_pr ehs_s ehs_po = assert (ehs_pr.m = ehs_po.m); - f_eHoareS_r { ehs_m=(ehs_pr.m, ehs_mt); ehs_pr=ehs_pr.inv; ehs_s; + f_eHoareS_r { ehs_m=(ehs_pr.m, ehs_mt); ehs_pr=ehs_pr.inv; ehs_s; ehs_po=ehs_po.inv; } [@alert "-priv_pl"] let f_eHoareF ehf_pr ehf_f ehf_po = @@ -304,7 +319,7 @@ let f_bdHoareF_r bhf = mk_form (FbdHoareF bhf) tbool let f_bdHoareS bhs_mt bhs_pr bhs_s bhs_po bhs_cmp bhs_bd = assert (bhs_pr.m = bhs_po.m && bhs_bd.m = bhs_po.m); - f_bdHoareS_r { bhs_m=(bhs_pr.m,bhs_mt); bhs_pr=bhs_pr.inv; bhs_s; + f_bdHoareS_r { bhs_m=(bhs_pr.m,bhs_mt); bhs_pr=bhs_pr.inv; bhs_s; bhs_po=bhs_po.inv; bhs_cmp; bhs_bd=bhs_bd.inv; } [@alert "-priv_pl"] let f_bdHoareF bhf_pr bhf_f bhf_po bhf_cmp bhf_bd = @@ -476,12 +491,22 @@ let f_map gt g fp = | FhoareF hf -> let pr' = map_ss_inv1 g (hf_pr hf) in let po' = map_ss_inv1 g (hf_po hf) in - f_hoareF pr' hf.hf_f po' + let poe' = + List.map + (fun (e,f) -> e, map_ss_inv1 g f) + (hf_poe hf) + in + f_hoareF pr' hf.hf_f po' poe' | FhoareS hs -> let pr' = map_ss_inv1 g (hs_pr hs) in let po' = map_ss_inv1 g (hs_po hs) in - f_hoareS (snd hs.hs_m) pr' hs.hs_s po' + let poe' = + List.map + (fun (e,f) -> e, map_ss_inv1 g f) + (hs_poe hs) + in + f_hoareS (snd hs.hs_m) pr' hs.hs_s po' poe' | FeHoareF hf -> let pr' = map_ss_inv1 g (ehf_pr hf) in @@ -648,8 +673,8 @@ let decompose_exists ?(bound : int option) (f : form) = decompose_binder ?bound ~quantif:Lexists f let decompose_lambda ?(bound : int option) (f : form) = - decompose_binder ?bound ~quantif:Llambda f - + decompose_binder ?bound ~quantif:Llambda f + (* -------------------------------------------------------------------- *) let destr_binder ?(bound : int option) ~quantif:quantif (f : form) = let bds, f = decompose_binder ?bound ~quantif f in @@ -660,10 +685,10 @@ let destr_binder ?(bound : int option) ~quantif:quantif (f : form) = let destr_forall ?(bound : int option) (f : form) = destr_binder ?bound ~quantif:Lforall f - + let destr_exists ?(bound : int option) (f : form) = destr_binder ?bound ~quantif:Lexists f - + let destr_lambda ?(bound : int option) (f : form) = destr_binder ?bound ~quantif:Llambda f @@ -678,10 +703,10 @@ let destr_forall1 (f : form) = let destr_exists1 (f : form) = destr_binder1 ~quantif:Lexists f - + let destr_lambda1 (f : form) = destr_binder1 ~quantif:Llambda f - + (* -------------------------------------------------------------------- *) let destr_let f = match f.f_node with @@ -828,7 +853,7 @@ let destr_imp = destr_app2 ~name:"imp" is_op_imp let destr_iff = destr_app2 ~name:"iff" is_op_iff let destr_eq = destr_app2 ~name:"eq" is_op_eq -let destr_and_ts_inv inv = +let destr_and_ts_inv inv = let c1 = map_ts_inv1 (fun po -> fst (destr_and po)) inv in let c2 = map_ts_inv1 (fun po -> snd (destr_and po)) inv in (c1, c2) diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index 0977a33a50..da930607fb 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -108,8 +108,9 @@ val f_lambda : bindings -> form -> form val f_forall_mems : (EcIdent.t * memtype) list -> form -> form -val f_hoareF : ss_inv -> xpath -> ss_inv -> form -val f_hoareS : memtype -> ss_inv -> stmt -> ss_inv -> form +val f_hoareF : ss_inv -> xpath -> ss_inv -> (EcPath.path * ss_inv) list -> form +val f_hoareS : + memtype -> ss_inv -> stmt -> ss_inv -> (EcPath.path * ss_inv) list -> form val f_eHoareF : ss_inv -> xpath -> ss_inv -> form val f_eHoareS : memtype -> ss_inv -> EcCoreModules.stmt -> ss_inv -> form diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml index 6f96118abe..71718a1750 100644 --- a/src/ecCoreModules.ml +++ b/src/ecCoreModules.ml @@ -93,7 +93,7 @@ let i_call (lv, m, tys) = mk_instr (Scall (lv, m, tys)) let i_if (c, s1, s2) = mk_instr (Sif (c, s1, s2)) let i_while (c, s) = mk_instr (Swhile (c, s)) let i_match (e, b) = mk_instr (Smatch (e, b)) -let i_assert e = mk_instr (Sassert e) +let i_raise (e,es) = mk_instr (Sraise (e,es)) let i_abstract id = mk_instr (Sabstract id) let s_seq s1 s2 = stmt (s1.s_node @ s2.s_node) @@ -105,7 +105,7 @@ let s_call arg = stmt [i_call arg] let s_if arg = stmt [i_if arg] let s_while arg = stmt [i_while arg] let s_match arg = stmt [i_match arg] -let s_assert arg = stmt [i_assert arg] +let s_raise arg = stmt [i_raise arg] let s_abstract arg = stmt [i_abstract arg] (* -------------------------------------------------------------------- *) @@ -133,8 +133,8 @@ let get_match = function | { i_node = Smatch (e, b) } -> Some (e, b) | _ -> None -let get_assert = function - | { i_node = Sassert e } -> Some e +let get_raise = function + | { i_node = Sraise(e,es) } -> Some (e,es) | _ -> raise Not_found (* -------------------------------------------------------------------- *) @@ -147,7 +147,7 @@ let destr_call = _destr_of_get get_call let destr_if = _destr_of_get get_if let destr_while = _destr_of_get get_while let destr_match = _destr_of_get get_match -let destr_assert = _destr_of_get get_assert +let destr_raise = _destr_of_get get_raise (* -------------------------------------------------------------------- *) let _is_of_get (get : instr -> 'a option) (i : instr) = @@ -159,7 +159,7 @@ let is_call = _is_of_get get_call let is_if = _is_of_get get_if let is_while = _is_of_get get_while let is_match = _is_of_get get_match -let is_assert = _is_of_get get_assert +let is_raise = _is_of_get get_raise (* -------------------------------------------------------------------- *) module Uninit = struct (* FIXME: generalize this for use in ecPV *) @@ -223,8 +223,9 @@ and i_get_uninit_read (w : Ssym.t) (i : instr) = let ws, rs = List.split wrs in (Ssym.union w (Ssym.big_inter ws), Ssym.big_union (r :: rs)) - | Sassert e -> - (w, Ssym.diff (Uninit.e_pv e) w) + | Sraise (_, args) -> + let r1 = Ssym.diff (Ssym.big_union (List.map (Uninit.e_pv) args)) w in + (w, r1) | Sabstract (_ : EcIdent.t) -> (w, Ssym.empty) diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli index 1b84c0df22..5227b4dcc1 100644 --- a/src/ecCoreModules.mli +++ b/src/ecCoreModules.mli @@ -42,7 +42,7 @@ val i_call : lvalue option * xpath * expr list -> instr val i_if : expr * stmt * stmt -> instr val i_while : expr * stmt -> instr val i_match : expr * ((EcIdent.t * ty) list * stmt) list -> instr -val i_assert : expr -> instr +val i_raise : EcPath.path * expr list -> instr val i_abstract : EcIdent.t -> instr val s_asgn : lvalue * expr -> stmt @@ -51,7 +51,7 @@ val s_call : lvalue option * xpath * expr list -> stmt val s_if : expr * stmt * stmt -> stmt val s_while : expr * stmt -> stmt val s_match : expr * ((EcIdent.t * ty) list * stmt) list -> stmt -val s_assert : expr -> stmt +val s_raise : EcPath.path * expr list -> stmt val s_abstract : EcIdent.t -> stmt val s_seq : stmt -> stmt -> stmt val s_empty : stmt @@ -66,7 +66,7 @@ val destr_call : instr -> lvalue option * xpath * expr list val destr_if : instr -> expr * stmt * stmt val destr_while : instr -> expr * stmt val destr_match : instr -> expr * ((EcIdent.t * ty) list * stmt) list -val destr_assert : instr -> expr +val destr_raise : instr -> EcPath.path * expr list val is_asgn : instr -> bool val is_rnd : instr -> bool @@ -74,7 +74,7 @@ val is_call : instr -> bool val is_if : instr -> bool val is_while : instr -> bool val is_match : instr -> bool -val is_assert : instr -> bool +val is_raise : instr -> bool (* -------------------------------------------------------------------- *) val get_uninit_read : stmt -> Sx.t diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index d906a61e3c..2ba5b69b55 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -61,7 +61,7 @@ module type PrinterAPI = sig val pp_tyvar : PPEnv.t -> ident pp val pp_tyunivar : PPEnv.t -> EcUid.uid pp val pp_path : path pp - + (* ------------------------------------------------------------------ *) val shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path -> qsymbol * qsymbol option @@ -79,21 +79,22 @@ module type PrinterAPI = sig | `Glob of EcIdent.t * EcMemory.memory | `PVar of EcTypes.prog_var * EcMemory.memory ] - + val pp_vsubst : PPEnv.t -> vsubst pp (* ------------------------------------------------------------------ *) - val pp_typedecl : PPEnv.t -> (path * tydecl ) pp - val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator ) pp - val pp_added_op : PPEnv.t -> operator pp - val pp_axiom : ?long:bool -> PPEnv.t -> (path * axiom ) pp - val pp_theory : PPEnv.t -> (path * ctheory ) pp - val pp_modtype1 : PPEnv.t -> (module_type ) pp - val pp_modtype : PPEnv.t -> (module_type ) pp - val pp_modexp : PPEnv.t -> (mpath * module_expr ) pp - val pp_moditem : PPEnv.t -> (mpath * module_item ) pp - val pp_modsig : ?long:bool -> PPEnv.t -> (path * module_sig) pp - val pp_modsig_smpl : PPEnv.t -> (path * module_smpl_sig ) pp + val pp_typedecl : PPEnv.t -> (path * tydecl ) pp + val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator ) pp + val pp_added_op : PPEnv.t -> operator pp + val pp_added_except : PPEnv.t -> excep pp + val pp_axiom : ?long:bool -> PPEnv.t -> (path * axiom ) pp + val pp_theory : PPEnv.t -> (path * ctheory ) pp + val pp_modtype1 : PPEnv.t -> (module_type ) pp + val pp_modtype : PPEnv.t -> (module_type ) pp + val pp_modexp : PPEnv.t -> (mpath * module_expr ) pp + val pp_moditem : PPEnv.t -> (mpath * module_item ) pp + val pp_modsig : ?long:bool -> PPEnv.t -> (path * module_sig) pp + val pp_modsig_smpl : PPEnv.t -> (path * module_smpl_sig ) pp (* ------------------------------------------------------------------ *) val pp_hoareS : PPEnv.t -> ?prpo:prpo_display -> sHoareS pp @@ -113,10 +114,10 @@ module type PrinterAPI = sig val pp_goal : PPEnv.t -> prpo_display -> ppgoal pp (* ------------------------------------------------------------------ *) - val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp + val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp (* ------------------------------------------------------------------ *) - val pp_rule_pattern : PPEnv.t -> EcTheory.rule_pattern pp + val pp_rule_pattern : PPEnv.t -> EcTheory.rule_pattern pp (* ------------------------------------------------------------------ *) module ObjectInfo : sig diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index c39a87a278..e34f377022 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -332,8 +332,9 @@ let rec s_subst_top (s : f_subst) : stmt -> stmt = i_match (e_subst e, List.Smart.map forb b) - | Sassert e -> - i_assert (e_subst e) + | Sraise (e,es) -> + let es' = List.Smart.map e_subst es in + i_raise (e, es') | Sabstract _ -> i @@ -455,14 +456,24 @@ module Fsubst = struct let (s, m) = add_m_binding s hf.hf_m in let hf_pr = f_subst ~tx s (hf_pr hf).inv in let hf_po = f_subst ~tx s (hf_po hf).inv in - f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po} + let hf_poe = + List.map + (fun (e,(f:ss_inv)) -> e,{m;inv=f_subst ~tx s f.inv}) + (hf_poe hf) + in + f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po} hf_poe | FhoareS hs -> let hs_s = s_subst s hs.hs_s in let s, (m, mt) = add_me_binding s hs.hs_m in let hs_pr = f_subst ~tx s (hs_pr hs).inv in let hs_po = f_subst ~tx s (hs_po hs).inv in - f_hoareS mt {m;inv=hs_pr} hs_s {m;inv=hs_po} + let hs_poe = + List.map + (fun (e,(f:ss_inv)) -> e,{m;inv=f_subst ~tx s f.inv}) + (hs_poe hs) + in + f_hoareS mt {m;inv=hs_pr} hs_s {m;inv=hs_po} hs_poe | FeHoareF hf -> let hf_f = x_subst s hf.ehf_f in diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 5636641acc..5610d0c242 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -152,6 +152,13 @@ type axiom = { let is_axiom (x : axiom_kind) = match x with `Axiom _ -> true | _ -> false let is_lemma (x : axiom_kind) = match x with `Lemma -> true | _ -> false +(* -------------------------------------------------------------------- *) + +type excep = { + e_typargs : ty_params; + e_loca : locality; + } + (* -------------------------------------------------------------------- *) let op_ty op = op.op_ty @@ -217,6 +224,13 @@ let mk_op ?clinline ?unfold ~opaque tparams ty body lc = let kind = OB_oper body in gen_op ?clinline ?unfold ~opaque tparams ty kind lc +let gen_excep tparams lc = { + e_typargs = tparams; + e_loca = lc; +} + +let mk_except tparams lc = gen_excep tparams lc + let mk_abbrev ?(ponly = false) tparams xs (codom, body) lc = let kind = { ont_args = xs; diff --git a/src/ecDecl.mli b/src/ecDecl.mli index 7864a0e0de..e4c5322a06 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -161,6 +161,14 @@ val axiomatized_op : -> locality -> axiom +(* -------------------------------------------------------------------- *) +type excep = { + e_typargs : ty_params; + e_loca : locality; +} + +val mk_except : ty_params -> locality -> excep + (* -------------------------------------------------------------------- *) type typeclass = { tc_prt : EcPath.path option; diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a4a5c8a7ca..104ac75eff 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -87,6 +87,7 @@ type mc = { mc_modsigs : (ipath * top_module_sig) MMsym.t; mc_tydecls : (ipath * EcDecl.tydecl) MMsym.t; mc_operators : (ipath * EcDecl.operator) MMsym.t; + mc_except : (ipath * EcDecl.excep) MMsym.t; mc_axioms : (ipath * EcDecl.axiom) MMsym.t; mc_theories : (ipath * ctheory) MMsym.t; mc_typeclasses: (ipath * typeclass) MMsym.t; @@ -277,6 +278,7 @@ let empty_mc params = { mc_modsigs = MMsym.empty; mc_tydecls = MMsym.empty; mc_operators = MMsym.empty; + mc_except = MMsym.empty; mc_axioms = MMsym.empty; mc_theories = MMsym.empty; mc_variables = MMsym.empty; @@ -515,6 +517,7 @@ module MC = struct let _downpath_for_tydecl = _downpath_for_th let _downpath_for_modsig = _downpath_for_th let _downpath_for_operator = _downpath_for_th + let _downpath_for_except = _downpath_for_th let _downpath_for_axiom = _downpath_for_th let _downpath_for_typeclass = _downpath_for_th let _downpath_for_rwbase = _downpath_for_th @@ -711,6 +714,20 @@ module MC = struct let import_axiom p ax env = import (_up_axiom true) (IPPath p) ax env + (* -------------------------------------------------------------------- *) + let lookup_except qnx env = + match lookup (fun mc -> mc.mc_except) qnx env with + | None -> lookup_error (`QSymbol qnx) + | Some (p, (args, obj)) -> (_downpath_for_except env p args, obj) + + let _up_except candup mc x obj = + if not candup && MMsym.last x mc.mc_except <> None then + raise (DuplicatedBinding x); + { mc with mc_except = MMsym.add x obj mc.mc_except } + + let import_except p e env = + import (_up_except true) (IPPath p) e env + (* -------------------------------------------------------------------- *) let lookup_operator qnx env = match lookup (fun mc -> mc.mc_operators) qnx env with @@ -1086,6 +1103,9 @@ module MC = struct | Th_operator (xop, op) -> (add2mc _up_operator xop op mc, None) + | Th_exception (xop, e) -> + (add2mc _up_except xop e mc, None) + | Th_axiom (xax, ax) -> (add2mc _up_axiom xax ax mc, None) @@ -1185,6 +1205,9 @@ module MC = struct and bind_axiom x ax env = bind _up_axiom x ax env + and bind_except x e env = + bind _up_except x e env + and bind_operator x op env = bind _up_operator x op env @@ -1478,7 +1501,7 @@ module BaseRw = struct env_item = mkitem ~import (Th_addrw (p, l, lc)) :: env.env_item; } let all env = - List.filter_map (fun (ip, sp) -> + List.filter_map (fun (ip, sp) -> match ip with | IPPath p -> Some (p, sp) | _ -> None) @@ @@ -1534,10 +1557,10 @@ module Reduction = struct |> odfl [] (* FIXME: handle other cases, right now only used for print hint *) - let all (env : env) = - List.map (fun (ts, mr) -> + let all (env : env) = + List.map (fun (ts, mr) -> (ts, Lazy.force mr.ri_list)) - (Mrd.bindings env.env_redbase) + (Mrd.bindings env.env_redbase) end (* -------------------------------------------------------------------- *) @@ -1586,7 +1609,7 @@ module Auto = struct let getall (bases : symbol list) (env : env) : atbase0 list = let dbs = List.map (fun base -> get_core ~base env) bases in - let dbs = + let dbs = List.fold_left (fun db mi -> Mint.union (fun _ sp1 sp2 -> Some (sp1 @ sp2)) db mi) Mint.empty dbs @@ -2780,6 +2803,36 @@ module Op = struct gen_all (fun mc -> mc.mc_operators) MC.lookup_operators ?check ?name env end +(* -------------------------------------------------------------------- *) +module Except = struct + type t = excep + + let by_path_opt (p : EcPath.path) (env : env) = + omap + check_not_suspended + (MC.by_path (fun mc -> mc.mc_except) (IPPath p) env) + + let by_path (p : EcPath.path) (env : env) = + match by_path_opt p env with + | None -> lookup_error (`Path p) + | Some obj -> obj + + let add (p : EcPath.path) (env : env) = + let obj = by_path p env in + MC.import_except p obj env + + let lookup qname (env : env) = + MC.lookup_except qname env + + let lookup_opt name env = + try_lf (fun () -> lookup name env) + + let bind ?(import = true) name e env = + let env = MC.bind_except name e env in + { env with env_item = mkitem ~import (Th_exception (name, e)) :: env.env_item } + +end + (* -------------------------------------------------------------------- *) module Ax = struct type t = axiom @@ -3086,6 +3139,9 @@ module Theory = struct | Th_operator (x, op) -> MC.import_operator (xpath x) op env + | Th_exception (x, e) -> + MC.import_except (xpath x) e env + | Th_axiom (x, ax) -> MC.import_axiom (xpath x) ax env diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 5a1d5bf602..ba081d0899 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -151,6 +151,16 @@ module Var : sig val bindall_pvglob : (EcSymbols.symbol * EcTypes.ty) list -> env -> env end +(* -------------------------------------------------------------------- *) +module Except : sig + type t = excep + val by_path : path -> env -> t + val by_path_opt : path -> env -> t option + val add : path -> env -> env + val lookup : qsymbol -> env -> path * t + val lookup_opt : qsymbol -> env -> (path * t) option + val bind : ?import:bool -> symbol -> t -> env -> env +end (* -------------------------------------------------------------------- *) module Ax : sig @@ -404,7 +414,7 @@ module BaseRw : sig val add : ?import:bool -> symbol -> is_local -> env -> env val addto : ?import:bool -> path -> path list -> is_local -> env -> env - val all : env -> (path * Sp.t) list + val all : env -> (path * Sp.t) list end (* -------------------------------------------------------------------- *) diff --git a/src/ecLexer.mll b/src/ecLexer.mll index a1b90c7c8c..da7f09cf64 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -53,7 +53,7 @@ "match" , MATCH ; (* KW: prog *) "for" , FOR ; (* KW: prog *) "while" , WHILE ; (* KW: prog *) - "assert" , ASSERT ; (* KW: prog *) + "raise" , RAISE ; (* KW: prog *) "return" , RETURN ; (* KW: prog *) "res" , RES ; (* KW: prog *) "equiv" , EQUIV ; (* KW: prog *) @@ -190,6 +190,7 @@ "of" , OF ; (* KW: global *) "const" , CONST ; (* KW: global *) "op" , OP ; (* KW: global *) + "exception" , EXCEP ; (* KW: global *) "pred" , PRED ; (* KW: global *) "inductive" , INDUCTIVE ; (* KW: global *) "notation" , NOTATION ; (* KW: global *) diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 4bec3d0ca2..3b0daba20c 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -96,7 +96,7 @@ let pf_first_call pe st = pf_first_gen "call" destr_call pe st let pf_first_if pe st = pf_first_gen "if" destr_if pe st let pf_first_match pe st = pf_first_gen "match" destr_match pe st let pf_first_while pe st = pf_first_gen "while" destr_while pe st -let pf_first_assert pe st = pf_first_gen "assert" destr_assert pe st +let pf_first_raise pe st = pf_first_gen "raise" destr_raise pe st (* -------------------------------------------------------------------- *) let pf_last_asgn pe st = pf_last_gen "asgn" destr_asgn pe st @@ -105,7 +105,7 @@ let pf_last_call pe st = pf_last_gen "call" destr_call pe st let pf_last_if pe st = pf_last_gen "if" destr_if pe st let pf_last_match pe st = pf_last_gen "match" destr_match pe st let pf_last_while pe st = pf_last_gen "while" destr_while pe st -let pf_last_assert pe st = pf_last_gen "assert" destr_assert pe st +let pf_last_raise pe st = pf_last_gen "raise" destr_raise pe st (* -------------------------------------------------------------------- *) let tc1_first_asgn tc st = pf_first_asgn !!tc st @@ -114,7 +114,7 @@ let tc1_first_call tc st = pf_first_call !!tc st let tc1_first_if tc st = pf_first_if !!tc st let tc1_first_match tc st = pf_first_match !!tc st let tc1_first_while tc st = pf_first_while !!tc st -let tc1_first_assert tc st = pf_first_assert !!tc st +let tc1_first_raise tc st = pf_first_raise !!tc st (* -------------------------------------------------------------------- *) let tc1_last_asgn tc st = pf_last_asgn !!tc st @@ -123,7 +123,7 @@ let tc1_last_call tc st = pf_last_call !!tc st let tc1_last_if tc st = pf_last_if !!tc st let tc1_last_match tc st = pf_last_match !!tc st let tc1_last_while tc st = pf_last_while !!tc st -let tc1_last_assert tc st = pf_last_assert !!tc st +let tc1_last_raise tc st = pf_last_raise !!tc st (* -------------------------------------------------------------------- *) (* TODO: use in change pos *) @@ -139,7 +139,7 @@ let pf_pos_last_call pe s = pf_pos_last_gen "call" is_call pe s let pf_pos_last_if pe s = pf_pos_last_gen "if" is_if pe s let pf_pos_last_match pe s = pf_pos_last_gen "match" is_match pe s let pf_pos_last_while pe s = pf_pos_last_gen "while" is_while pe s -let pf_pos_last_assert pe s = pf_pos_last_gen "assert" is_assert pe s +let pf_pos_last_raise pe s = pf_pos_last_gen "raise" is_raise pe s let tc1_pos_last_asgn tc s = pf_pos_last_asgn !!tc s @@ -148,7 +148,7 @@ let tc1_pos_last_call tc s = pf_pos_last_call !!tc s let tc1_pos_last_if tc s = pf_pos_last_if !!tc s let tc1_pos_last_match tc s = pf_pos_last_match !!tc s let tc1_pos_last_while tc s = pf_pos_last_while !!tc s -let tc1_pos_last_assert tc s = pf_pos_last_assert !!tc s +let tc1_pos_last_raise tc s = pf_pos_last_raise !!tc s (* -------------------------------------------------------------------- *) let pf_as_hoareF pe c = as_phl (`Hoare `Pred) (fun () -> destr_hoareF c) pe @@ -209,7 +209,7 @@ let tc1_get_stmt side tc = (* -------------------------------------------------------------------- *) let hl_set_stmt (side : side option) (f : form) (s : stmt) = match side, f.f_node with - | None , FhoareS hs -> f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) + | None , FhoareS hs -> f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) (hs_poe hs) | None , FeHoareS hs -> f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs) | None , FbdHoareS hs -> f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs) | Some `Left , FequivS es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es) @@ -253,31 +253,43 @@ let tc1_get_post tc = | None -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc | Some f -> f +(* -------------------------------------------------------------------- *) +let get_poste f = + match f.f_node with + | FhoareF hf -> Some (hf_poe hf) + | FhoareS hs -> Some (hs_poe hs) + | _ -> None + +let tc1_get_poste tc = + match get_poste (FApi.tc1_goal tc) with + | None -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc + | Some f -> f + (* -------------------------------------------------------------------- *) let set_pre ~pre f = match f.f_node, pre with - | FhoareF hf, Inv_ss pre -> + | FhoareF hf, Inv_ss pre -> let pre = ss_inv_rebind pre hf.hf_m in - f_hoareF pre hf.hf_f (hf_po hf) - | FhoareS hs, Inv_ss pre -> + f_hoareF pre hf.hf_f (hf_po hf) (hf_poe hf) + | FhoareS hs, Inv_ss pre -> let pre = ss_inv_rebind pre (fst hs.hs_m) in - f_hoareS (snd hs.hs_m) pre hs.hs_s (hs_po hs) - | FeHoareF hf, Inv_ss pre -> + f_hoareS (snd hs.hs_m) pre hs.hs_s (hs_po hs) (hs_poe hs) + | FeHoareF hf, Inv_ss pre -> let pre = ss_inv_rebind pre hf.ehf_m in f_eHoareF pre hf.ehf_f (ehf_po hf) - | FeHoareS hs, Inv_ss pre -> + | FeHoareS hs, Inv_ss pre -> let pre = ss_inv_rebind pre (fst hs.ehs_m) in f_eHoareS (snd hs.ehs_m) pre hs.ehs_s (ehs_po hs) | FbdHoareF hf, Inv_ss pre -> let pre = ss_inv_rebind pre hf.bhf_m in f_bdHoareF pre hf.bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf) - | FbdHoareS hs, Inv_ss pre -> + | FbdHoareS hs, Inv_ss pre -> let pre = ss_inv_rebind pre (fst hs.bhs_m) in f_bdHoareS (snd hs.bhs_m) pre hs.bhs_s (bhs_po hs) hs.bhs_cmp (bhs_bd hs) - | FequivF ef, Inv_ts pre -> + | FequivF ef, Inv_ts pre -> let pre = ts_inv_rebind pre ef.ef_ml ef.ef_mr in f_equivF pre ef.ef_fl ef.ef_fr (ef_po ef) - | FequivS es, Inv_ts pre -> + | FequivS es, Inv_ts pre -> let pre = ts_inv_rebind pre (fst es.es_ml) (fst es.es_mr) in f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr (es_po es) | _ -> assert false @@ -665,14 +677,16 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = let pr, po = hs_pr hs, hs_po hs in let (me, stmt, cs) = tx (pf, hyps) cpos (pr.inv, po.inv) (hs.hs_m, hs.hs_s) in - let concl = f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs) in + let concl = + f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs) (hs_poe hs) + in FApi.xmutate1 tc (tr None) (cs @ [concl]) | FbdHoareS bhs when bdhoare -> 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) + let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in FApi.xmutate1 tc (tr None) (cs @ [concl]) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 76f7aee485..5f3449a93f 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -685,9 +685,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then failure (); let subst = - if id_equal hf1.hf_m hf2.hf_m then + if id_equal hf1.hf_m hf2.hf_m then subst - else + else Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs)); let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in @@ -701,9 +701,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if hf1.bhf_cmp <> hf2.bhf_cmp then failure (); let subst = - if id_equal hf1.bhf_m hf2.bhf_m then + if id_equal hf1.bhf_m hf2.bhf_m then subst - else + else Fsubst.f_bind_mem subst hf1.bhf_m hf2.bhf_m in assert (not (Mid.mem hf1.bhf_m mxs) && not (Mid.mem hf2.bhf_m mxs)); let mxs = Mid.add hf1.bhf_m hf2.bhf_m mxs in @@ -718,16 +718,16 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if not (EcReduction.EqTest.for_xp env hf1.ef_fr hf2.ef_fr) then failure(); let subst = - if id_equal hf1.ef_ml hf2.ef_ml then + if id_equal hf1.ef_ml hf2.ef_ml then subst - else + else Fsubst.f_bind_mem subst hf1.ef_ml hf2.ef_ml in assert (not (Mid.mem hf1.ef_ml mxs) && not (Mid.mem hf2.ef_ml mxs)); let mxs = Mid.add hf1.ef_ml hf2.ef_ml mxs in let subst = - if id_equal hf1.ef_mr hf2.ef_mr then + if id_equal hf1.ef_mr hf2.ef_mr then subst - else + else Fsubst.f_bind_mem subst hf1.ef_mr hf2.ef_mr in assert (not (Mid.mem hf1.ef_mr mxs) && not (Mid.mem hf2.ef_mr mxs)); let mxs = Mid.add hf1.ef_mr hf2.ef_mr mxs in @@ -743,9 +743,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = doit env (subst, mxs) pr1.pr_args pr2.pr_args; let ev1, ev2 = pr1.pr_event, pr2.pr_event in let subst = - if id_equal ev1.m ev2.m then + if id_equal ev1.m ev2.m then subst - else + else Fsubst.f_bind_mem subst ev1.m ev2.m in assert (not (Mid.mem ev1.m mxs) && not (Mid.mem ev2.m mxs)); let mxs = Mid.add ev1.m ev2.m mxs in @@ -1169,9 +1169,16 @@ module FPosition = struct f_pr pr.pr_mem pr.pr_fun args' {m;inv=event'} | FhoareF hf -> - let (hf_pr, hf_po) = as_seq2 (doit p [(hf_pr hf).inv; (hf_po hf).inv]) in + let (hf_pr, hf_po) = + as_seq2 (doit p [(hf_pr hf).inv; (hf_po hf).inv]) + in let m = hf.hf_m in - f_hoareF {m;inv=hf_pr} hf.hf_f {m;inv=hf_po} + let hf_poe = + List.map + (fun (e,(f:ss_inv)) -> e,{m;inv=as_seq1 (doit p [f.inv])}) + (hf_poe hf) + in + f_hoareF {m;inv=hf_pr} hf.hf_f {m;inv=hf_po} hf_poe | FeHoareF hf -> let (ehf_pr, ehf_po) = diff --git a/src/ecPV.ml b/src/ecPV.ml index 6d5c5bd5e1..0aa9b0305c 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -129,7 +129,7 @@ module Mpv = struct | Sif (c, s1, s2) -> i_if (esubst c, ssubst s1, ssubst s2) | Swhile (e, stmt) -> i_while (esubst e, ssubst stmt) | Smatch (e, b) -> i_match (esubst e, List.Smart.map (snd_map ssubst) b) - | Sassert e -> i_assert (esubst e) + | Sraise (e,es) -> i_raise (e, List.map esubst es) | Sabstract _ -> i and issubst env (s : esubst) (is : instr list) = @@ -513,7 +513,7 @@ and i_write_r ?(except=Sx.empty) env w i = match i.i_node with | Sasgn (lp, _) -> lp_write_r env w lp | Srnd (lp, _) -> lp_write_r env w lp - | Sassert _ -> w + | Sraise _ -> w | Scall(lp,f,_) -> if Sx.mem f except then w else @@ -571,7 +571,8 @@ and i_read_r env r i = match i.i_node with | Sasgn (_lp, e) -> e_read_r env r e | Srnd (_lp, e) -> e_read_r env r e - | Sassert e -> e_read_r env r e + | Sraise (_e, es) -> + List.fold_left (e_read_r env) r es | Scall (_lp, f, es) -> let r = List.fold_left (e_read_r env) r es in @@ -1054,7 +1055,9 @@ and i_eqobs_in_refl env i eqo = let eqs = List.fold_left PV.union PV.empty eqs in add_eqs_refl env eqs e - | Sassert e -> add_eqs_refl env eqo e + | Sraise (_,es) -> + List.fold_left (add_eqs_refl env) eqo es + | Sabstract _ -> assert false and eqobs_inF_refl env f' eqo = diff --git a/src/ecParser.mly b/src/ecParser.mly index bb42556954..30467a788c 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -384,7 +384,7 @@ %token AMP %token APPLY %token AS -%token ASSERT +%token RAISE %token ASSUMPTION %token ASYNC %token AT @@ -442,6 +442,7 @@ %token EQUIV %token ETA %token EXACT +%token EXCEP %token EXFALSO %token EXIST %token EXIT @@ -1222,9 +1223,14 @@ hoare_bd_cmp : | EQ { EcAst.FHeq } | GE { EcAst.FHge } +epost(P): x=lident COLON post=form_r(P) + { let loc = EcLocation.make $startpos $endpos in + (EcLocation.mk_loc loc ([], x),post)} + hoare_body(P): mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW post=form_r(P) - { PFhoareF (m, pre, mp, post) } + epost=splist(epost(P), PIPE) + { PFhoareF (m, pre, mp, post, epost) } ehoare_body(P): mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW @@ -1345,8 +1351,9 @@ base_instr: | f=loc(fident) LPAREN es=loc(plist0(expr, COMMA)) RPAREN { PScall (None, f, es) } -| ASSERT LPAREN c=expr RPAREN - { PSassert c } + | RAISE x=lident + {let loc = EcLocation.make $startpos $endpos in + PSraise (EcLocation.mk_loc loc ([], x), EcLocation.mk_loc loc []) } instr: | bi=base_instr SEMICOLON @@ -1753,6 +1760,7 @@ tyci_ax: | PROOF x=ident BY tg=tactic_core { (x, tg) } + (* -------------------------------------------------------------------- *) (* Operator definitions *) @@ -1859,6 +1867,14 @@ procop: | locality=locality PROC OP x=ident EQ f=loc(fident) { { ppo_name = x; ppo_target = f; ppo_locality = locality; } } +(* -------------------------------------------------------------------- *) +(* Exceptions *) +excep: +| locality=locality EXCEP x=oident + { { pe_name = x; + pe_typargs = None; + pe_locality = locality; } } + (* -------------------------------------------------------------------- *) (* Predicate definitions *) predicate: @@ -2508,17 +2524,36 @@ conseq: | UNDERSCORE LONGARROW f2=form { None, Some f2 } | f1=form LONGARROW f2=form { Some f1, Some f2 } +epost_xt: +| x=lident COLON f=form +{ let loc = EcLocation.make $startpos $endpos in + (EcLocation.mk_loc loc ([], x), f)} + +epostl: +| PIPE p=epost_xt { [ p ] } +| PIPE p=epost_xt a=epostl { p :: a } + +conseq_epost: +| empty { None } +| c=epostl { Some c } + conseq_xt: -| c=conseq { c, None } -| c=conseq COLON cmp=hoare_bd_cmp? bd=sform { c, Some (CQI_bd (cmp, bd)) } -| UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform { (None, None), Some (CQI_bd (cmp, bd)) } +| c=conseq d=conseq_epost + { (fst c, snd c, d), None } +| c=conseq COLON cmp=hoare_bd_cmp? bd=sform + { (fst c, snd c, None), Some (CQI_bd (cmp, bd)) } +| UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform + { (None, None, None), Some (CQI_bd (cmp, bd)) } +call_epost: +| empty { [] } +| c=epostl { c } call_info: -| f1=form LONGARROW f2=form { CI_spec (f1, f2) } -| f=form { CI_inv f } -| bad=form COMMA p=form { CI_upto (bad,p,None) } -| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) } +| f1=form LONGARROW f2=form poe=call_epost { CI_spec (f1, f2, poe) } +| f=form poe=call_epost { CI_inv (f, poe) } +| bad=form COMMA p=form { CI_upto (bad,p,None) } +| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) } tac_dir: | BACKS { Backs } @@ -3847,6 +3882,7 @@ global_action: | typeclass { Gtypeclass $1 } | tycinstance { Gtycinstance $1 } | operator { Goperator $1 } +| excep { Gexception $1 } | procop { Gprocop $1 } | predicate { Gpredicate $1 } | notation { Gnotation $1 } @@ -3935,6 +3971,11 @@ iplist1_r(X, S): %inline empty: | /**/ { () } +(* -------------------------------------------------------------------- *) +%inline splist(X, S): +| /* empty */ { [] } +| S xs=iplist1_r(X, S) { xs } + (* -------------------------------------------------------------------- *) __rlist1(X, S): (* left-recursive *) | x=X { [x] } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 8e900919b9..686335d927 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -160,7 +160,7 @@ and pinstr_r = | PSif of pscond * pscond list * pstmt | PSwhile of pscond | PSmatch of pexpr * psmatch - | PSassert of pexpr + | PSraise of pgamepath * (pexpr list) located and psmatch = [ | `Full of (ppattern * pstmt) list @@ -201,8 +201,7 @@ and pformula_r = | PFeqf of pformula list | PFlsless of pgamepath | PFscope of pqsymbol * pformula - - | PFhoareF of psymbol option * pformula * pgamepath * pformula + | PFhoareF of psymbol option * pformula * pgamepath * pformula * (pgamepath * pformula) list | PFehoareF of psymbol option * pformula * pgamepath * pformula | PFequivF of psymbol option * psymbol option * pformula * (pgamepath * pgamepath) * pformula | PFeagerF of psymbol option * psymbol option * pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula @@ -429,6 +428,12 @@ and pprocop = { ppo_locality : locality; } +type pexception_decl = { + pe_name : psymbol; + pe_typargs : (psymbol * pqsymbol list) list option; + pe_locality : locality; + } + type ppred_def = | PPabstr of pty list | PPconcr of ptybindings * pformula @@ -531,9 +536,11 @@ type pipattern = and pspattern = unit +type pfel_spec_preds = (pgamepath * pformula) list + type call_info = - | CI_spec of (pformula * pformula) - | CI_inv of pformula + | CI_spec of (pformula * pformula * pfel_spec_preds) + | CI_inv of (pformula * pfel_spec_preds) | CI_upto of (pformula * pformula * pformula option) type p_app_xt_info = @@ -554,8 +561,6 @@ type psemrndpos = (bool * pcodepos1) doption type tac_dir = Backs | Fwds -type pfel_spec_preds = (pgamepath * pformula) list - (* -------------------------------------------------------------------- *) type pim_repeat_kind = | IM_R_Repeat of int option pair @@ -685,7 +690,9 @@ type deno_ppterm = (pformula option pair) gppterm type conseq_info = | CQI_bd of phoarecmp option * pformula -type conseq_ppterm = ((pformula option pair) * (conseq_info) option) gppterm +type conseq_contra = pformula option * pformula option * pfel_spec_preds option + +type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm (* -------------------------------------------------------------------- *) type sim_info = { @@ -1273,6 +1280,7 @@ type global_action = | Gmodule of pmodule_def_or_decl | Ginterface of pinterface | Goperator of poperator + | Gexception of pexception_decl | Gprocop of pprocop | Gpredicate of ppredicate | Gnotation of pnotation diff --git a/src/ecPath.ml b/src/ecPath.ml index 0cb0edf4da..878c030379 100644 --- a/src/ecPath.ml +++ b/src/ecPath.ml @@ -59,6 +59,14 @@ let rec p_ntr_compare (p1 : path) (p2 : path) = | n -> n end +let rec p_ntr_equal (p1 : path) (p2 : path) = + match p1.p_node, p2.p_node with + | Psymbol x1, Psymbol x2 -> + String.equal x1 x2 + | Pqname (p1, x1), Pqname (p2, x2) -> + p_ntr_equal p1 p2 && String.equal x1 x2 + | _, _ -> false + (* -------------------------------------------------------------------- *) module Mp = Path.M module Hp = Path.H @@ -268,7 +276,7 @@ let is_abstract (mp : mpath) = let is_concrete (mp : mpath) = match mp.m_top with `Concrete _ -> true | _ -> false - + let m_functor mp = let top = match mp.m_top with diff --git a/src/ecPath.mli b/src/ecPath.mli index ef2d2e8c0f..1555e9d1a8 100644 --- a/src/ecPath.mli +++ b/src/ecPath.mli @@ -22,6 +22,7 @@ val poappend : path -> path option -> path val p_equal : path -> path -> bool val p_compare : path -> path -> int +val p_ntr_equal : path -> path -> bool val p_ntr_compare : path -> path -> int val p_hash : path -> int diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index fd8171647b..f60f85e816 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1545,9 +1545,8 @@ and pp_instr_for_form (ppe : PPEnv.t) fmt i = (pp_funname ppe) xp (pp_list ",@ " (pp_expr ppe)) args - | Sassert e -> - Format.fprintf fmt "assert %a;" - (pp_expr ppe) e + | Sraise _ -> + Format.fprintf fmt "raise TODO;" | Swhile (e, _) -> Format.fprintf fmt "while (%a) {...}" @@ -1810,6 +1809,14 @@ and try_pp_notations let f = f_app f eargs f.f_ty in pp_form_core_r ppe outer fmt f; true +and ppepoe ppepr fmt l = + let aux fmt (e, f) = + Format.fprintf fmt " %a: %a" pp_path e (pp_form ppepr) f + in + match l with + | [] -> Format.fprintf fmt "" + | _ -> Format.fprintf fmt "| %a" (pp_list "|" aux) l + and pp_form_core_r (ppe : PPEnv.t) (outer : opprec * iassoc) @@ -1941,21 +1948,25 @@ and pp_form_core_r let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in - Format.fprintf fmt "hoare[@[@ %a %a:@ @[%a ==>@ %a@]@]]" + let hf_poe = List.map (fun (e,(f:ss_inv)) -> e,f.inv) (hf_poe hf) in + Format.fprintf fmt "hoare[@[@ %a %a:@ @[%a ==>@ %a@ %a]@]]" (pp_funname ppe) hf.hf_f (pp_pl_mem_binding pm ppe) hf.hf_m (pp_form ppepr) (hf_pr hf).inv (pp_form ppepo) (hf_po hf).inv + (ppepoe ppepo) hf_poe | FhoareS hs -> let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in + let hs_poe = List.map (fun (e,(f:ss_inv)) -> e,f.inv) (hs_poe hs) in let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in - Format.fprintf fmt "hoare[@[@ %a %a:@ @[%a ==>@ %a@]@]]" + Format.fprintf fmt "hoare[@[@ %a %a:@ @[%a ==>@ %a@ %a]@]]" (pp_stmt_for_form ppe) hs.hs_s (pp_pl_mem_binding pm ppe) (fst hs.hs_m) (pp_form ppe) (hs_pr hs).inv (pp_form ppe) (hs_po hs).inv - + (ppepoe ppe) hs_poe + | FeHoareF hf -> let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_m hf.ehf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in @@ -2591,6 +2602,12 @@ let pp_added_op (ppe : PPEnv.t) fmt op = | ts -> Format.fprintf fmt "@[%a :@ %a.@]" (pp_tyvarannot ppe) ts (pp_type ppe) op.op_ty +(* -------------------------------------------------------------------- *) +let pp_added_except (ppe : PPEnv.t) fmt e = + let ppe = PPEnv.add_locals ppe (List.map fst e.e_typargs) in + match e.e_typargs with + | [] -> Format.fprintf fmt ": @[@]" + | ts -> Format.fprintf fmt "@[%a@]" (pp_tyvarannot ppe) ts (* -------------------------------------------------------------------- *) let pp_opname (ppe : PPEnv.t) fmt (p : EcPath.path) = @@ -2648,7 +2665,7 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) = (* -------------------------------------------------------------------- *) type ppnode1 = [ | `Asgn of (EcModules.lvalue * EcTypes.expr) - | `Assert of (EcTypes.expr) + | `Raise of (EcPath.path * EcTypes.expr list) | `Call of (EcModules.lvalue option * P.xpath * EcTypes.expr list) | `Rnd of (EcModules.lvalue * EcTypes.expr) | `Abstract of EcIdent.t @@ -2671,7 +2688,7 @@ let at (ppe : PPEnv.t) n i = | Sasgn (lv, e) , 0 -> Some (`Asgn (lv, e) , `P, []) | Srnd (lv, e) , 0 -> Some (`Rnd (lv, e) , `P, []) | Scall (lv, f, es), 0 -> Some (`Call (lv, f, es), `P, []) - | Sassert e , 0 -> Some (`Assert e , `P, []) + | Sraise (e,es) , 0 -> Some (`Raise (e,es) , `P, []) | Sabstract id , 0 -> Some (`Abstract id , `P, []) | Swhile (e, s), 0 -> Some (`While e, `P, s.s_node) @@ -2759,8 +2776,8 @@ let pp_i_asgn (ppe : PPEnv.t) fmt (lv, e) = Format.fprintf fmt "%a <-@ %a" (pp_lvalue ppe) lv (pp_expr ppe) e -let pp_i_assert (ppe : PPEnv.t) fmt e = - Format.fprintf fmt "assert (%a)" (pp_expr ppe) e +let pp_i_raise (_ppe : PPEnv.t) fmt ((e,_es):EcPath.path * expr list) = + Format.fprintf fmt "raise %a" pp_path e let pp_i_call (ppe : PPEnv.t) fmt (lv, xp, args) = match lv with @@ -2807,7 +2824,7 @@ let pp_i_abstract (_ppe : PPEnv.t) fmt id = let c_ppnode1 ~width ppe (pp1 : ppnode1) = match pp1 with | `Asgn x -> c_split ~width (pp_i_asgn ppe) x - | `Assert x -> c_split ~width (pp_i_assert ppe) x + | `Raise x -> c_split ~width (pp_i_raise ppe) x | `Call x -> c_split ~width (pp_i_call ppe) x | `Rnd x -> c_split ~width (pp_i_rnd ppe) x | `Abstract x -> c_split ~width (pp_i_abstract ppe) x @@ -2977,6 +2994,14 @@ let pp_post (ppe : PPEnv.t) ?prpo fmt post = (omap (fun x -> x.prpo_po) prpo |> odfl false) fmt post None +(* -------------------------------------------------------------------- *) +let pp_poe (ppe : PPEnv.t) ?prpo (fmt: Format.formatter) poe = + List.iter (fun ((e:EcPath.path),f) -> + pp_prpo ppe (EcPath.basename e) + (omap (fun x -> x.prpo_po) prpo |> odfl false) + fmt f None + ) poe + (* -------------------------------------------------------------------- *) let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf = let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in @@ -2986,23 +3011,41 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf = Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv; let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in Format.fprintf fmt " %a %a@\n%!" (pp_funname ppe) hf.hf_f (pp_pl_mem_binding pm ppe) hf.hf_m; - Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (hf_po hf).inv + Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (hf_po hf).inv; + let hf_poe = List.map (fun (e,(f:ss_inv)) -> e,f.inv) (hf_poe hf) in + Format.fprintf fmt "@\n%a%!" (pp_poe ppepo ?prpo) hf_poe (* -------------------------------------------------------------------- *) let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs = let ppef = PPEnv.push_mem ppe ~active:true hs.hs_m in let ppnode = collect2_s ppef hs.hs_s.s_node [] in - let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode - in - Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m) - (pp_memtype ppe) (snd hs.hs_m); - Format.fprintf fmt "@\n%!"; - Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (hs_pr hs).inv; - Format.fprintf fmt "@\n%!"; - Format.fprintf fmt "%a" (pp_node `Left) ppnode; - Format.fprintf fmt "@\n%!"; - Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) (hs_po hs).inv +(* <<<<<<< HEAD *) +(* let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode *) +(* in *) +(* Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m) *) +(* (pp_memtype ppe) (snd hs.hs_m); *) +(* Format.fprintf fmt "@\n%!"; *) +(* Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (hs_pr hs).inv; *) +(* Format.fprintf fmt "@\n%!"; *) +(* Format.fprintf fmt "%a" (pp_node `Left) ppnode; *) +(* Format.fprintf fmt "@\n%!"; *) +(* Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) (hs_po hs).inv *) + (* ======= *) + + let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in + + Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m) + (pp_memtype ppe) (snd hs.hs_m); + Format.fprintf fmt "@\n%!"; + Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (hs_pr hs).inv; + Format.fprintf fmt "@\n%!"; + Format.fprintf fmt "%a" (pp_node `Left) ppnode; + Format.fprintf fmt "@\n%!"; + Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) (hs_po hs).inv; + Format.fprintf fmt "@\n%!"; + let hs_poe = List.map (fun (e,(f:ss_inv)) -> e,f.inv) (hs_poe hs) in + Format.fprintf fmt "%a%!" (pp_poe ppef ?prpo) hs_poe (* -------------------------------------------------------------------- *) let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf = @@ -3022,7 +3065,7 @@ let pp_eHoareS (ppe : PPEnv.t) ?prpo fmt hs = let ppnode = collect2_s ppef hs.ehs_s.s_node [] in let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in - Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.ehs_m) + Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.ehs_m) (pp_memtype ppe) (snd hs.ehs_m); Format.fprintf fmt "@\n%!"; Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (ehs_pr hs).inv; @@ -3395,9 +3438,8 @@ let rec pp_instr_r (ppe : PPEnv.t) fmt i = (pp_funname ppe) xp (pp_list ",@ " (pp_expr ppe)) args - | Sassert e -> - Format.fprintf fmt "@[assert %a@];" - (pp_expr ppe) e + | Sraise _ -> + Format.fprintf fmt "@[assert TODO@];" | Swhile (e, s) -> Format.fprintf fmt "@[while (@[%a@])%a@]" @@ -3441,7 +3483,7 @@ and pp_block ppe fmt s = | [] -> Format.fprintf fmt "{}" - | [ { i_node = (Sasgn _ | Srnd _ | Scall _ | Sassert _ | Sabstract _) } as i ] -> + | [ { i_node = (Sasgn _ | Srnd _ | Scall _ | Sraise _ | Sabstract _) } as i ] -> Format.fprintf fmt "@;<1 2>%a" (pp_instr ppe) i | _ -> @@ -3558,6 +3600,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = | EcTheory.Th_operator (id, op) -> pp_opdecl ppe fmt (EcPath.pqname p id, op) + | EcTheory.Th_exception (_id, _e) -> + Format.fprintf fmt "exception ." + | EcTheory.Th_axiom (id, ax) -> pp_axiom ppe fmt (EcPath.pqname p id, ax) diff --git a/src/ecProcSem.ml b/src/ecProcSem.ml index 26df3e6228..2fb1af20f5 100644 --- a/src/ecProcSem.ml +++ b/src/ecProcSem.ml @@ -191,7 +191,7 @@ let rec translate_i (env : senv) (cont : senv -> mode * expr) (i : instr) = | Swhile _ | Smatch _ - | Sassert _ + | Sraise _ | Sabstract _ | Scall _ -> raise SemNotSupported; diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 1dce11fabf..6a4d524f80 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -243,8 +243,8 @@ end) = struct with E.NotConv -> false end - | Sassert a1, Sassert a2 -> - for_expr env alpha ~norm a1 a2 + | Sraise (_,es1), Sraise (_,es2) -> + List.all2 (for_expr env alpha ~norm) es1 es2 | Sabstract id1, Sabstract id2 -> EcIdent.id_equal id1 id2 @@ -1258,23 +1258,23 @@ let rec simplify ri env f = match f.f_node with | FhoareF hf when ri.ri.modpath -> let hf_f = EcEnv.NormMp.norm_xfun env hf.hf_f in - f_map (fun ty -> ty) (simplify ri env) - (f_hoareF (hf_pr hf) hf_f (hf_po hf)) + f_map (fun ty -> ty) (simplify ri env) + (f_hoareF (hf_pr hf) hf_f (hf_po hf) (hf_poe hf)) | FeHoareF hf when ri.ri.modpath -> let ehf_f = EcEnv.NormMp.norm_xfun env hf.ehf_f in - f_map (fun ty -> ty) (simplify ri env) + f_map (fun ty -> ty) (simplify ri env) (f_eHoareF (ehf_pr hf) ehf_f (ehf_po hf)) | FbdHoareF hf when ri.ri.modpath -> let bhf_f = EcEnv.NormMp.norm_xfun env hf.bhf_f in - f_map (fun ty -> ty) (simplify ri env) + f_map (fun ty -> ty) (simplify ri env) (f_bdHoareF (bhf_pr hf) bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf)) | FequivF ef when ri.ri.modpath -> let ef_fl = EcEnv.NormMp.norm_xfun env ef.ef_fl in let ef_fr = EcEnv.NormMp.norm_xfun env ef.ef_fr in - f_map (fun ty -> ty) (simplify ri env) + f_map (fun ty -> ty) (simplify ri env) (f_equivF (ef_pr ef) ef_fl ef_fr (ef_po ef)) | FeagerF eg when ri.ri.modpath -> @@ -1362,10 +1362,10 @@ let zpop ri side f hd = | Zproj i, [f1] -> f_proj f1 i hd.se_ty | Zhl {f_node = FhoareF hf}, [pr;po] -> let m = hf.hf_m in - f_hoareF {m;inv=pr} hf.hf_f {m;inv=po} + f_hoareF {m;inv=pr} hf.hf_f {m;inv=po} (hf_poe hf) | Zhl {f_node = FhoareS hs}, [pr;po] -> let m = fst hs.hs_m in - f_hoareS (snd hs.hs_m) {m;inv=pr} hs.hs_s {m;inv=po} + f_hoareS (snd hs.hs_m) {m;inv=pr} hs.hs_s {m;inv=po} (hs_poe hs) | Zhl {f_node = FeHoareF hf}, [pr;po] -> let m = hf.ehf_m in f_eHoareF {m;inv=pr} hf.ehf_f {m;inv=po} diff --git a/src/ecScope.ml b/src/ecScope.ml index bce77e0abe..aa2020ff92 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1317,7 +1317,7 @@ module Op = struct tyop, List.rev !axs, scope - + (*-------------------------------------------------------------------------*) let add_opsem (scope : scope) (op : pprocop located) = let module Sem = EcProcSem in @@ -1429,7 +1429,9 @@ module Op = struct (f_app (f_op oppath [] opdecl.op_ty) (List.map (fun (x, ty) -> f_local x ty) locs) - sig_.fs_ret))}) + sig_.fs_ret))} + [] + ) in let prax = EcDecl.{ @@ -1449,6 +1451,28 @@ module Op = struct scope end +(* -------------------------------------------------------------------- *) +module Except = struct + module TT = EcTyping + + let bind ?(import = true) (scope : scope) ((x, e) : _ * excep) = + assert (scope.sc_pr_uc = None); + let item = EcTheory.mkitem ~import (EcTheory.Th_exception (x, e)) in + { scope with sc_env = EcSection.add_item item scope.sc_env; } + + let add (scope : scope) (pe : pexception_decl located) = + assert (scope.sc_pr_uc = None); + let pe = pe.pl_desc and loc = pe.pl_loc in + let eenv = env scope in + let ue = TT.transtyvars eenv (loc, pe.pe_typargs) in + let lc = pe.pe_locality in + let tparams = EcUnify.UniEnv.tparams ue in + let e = EcDecl.mk_except tparams lc in + let scope = bind scope (unloc pe.pe_name, e) in + e, scope + +end + (* -------------------------------------------------------------------- *) module Pred = struct module TT = EcTyping @@ -1840,7 +1864,7 @@ module Cloning = struct | Some pt -> let t = { pt_core = pt; pt_intros = []; } in let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in - let t = { pt_core = t; pt_intros = []; } in + let t = { pt_core = t; pt_intros = []; } in let (x, ax) = axc.C.axc_axiom in let pucflags = { puc_smt = true; puc_local = false; } in @@ -1897,7 +1921,7 @@ module Cloning = struct | `Include -> scope) scope in - + if is_none thcl.pthc_local && oth.cth_loca = `Local then notify scope `Info "Theory `%s` has inherited `local` visibility. \ @@ -1986,14 +2010,14 @@ module Ty = struct let carrier = let ue = EcUnify.UniEnv.create None in transty tp_tydecl env ue subtype.pst_carrier in - + let pred = let x = EcIdent.create (fst subtype.pst_pred).pl_desc in let env = EcEnv.Var.bind_local x carrier env in let ue = EcUnify.UniEnv.create None in let pred = EcTyping.trans_prop env ue (snd subtype.pst_pred) in if not (EcUnify.UniEnv.closed ue) then - hierror ~loc:(snd subtype.pst_pred).pl_loc + hierror ~loc:(snd subtype.pst_pred).pl_loc "the predicate contains free type variables"; let uidmap = EcUnify.UniEnv.close ue in let fs = Tuni.subst uidmap in @@ -2015,12 +2039,12 @@ module Ty = struct ev_bynames = Msym.empty; ev_global = [ (None, Some [`Include, "prove"]) ] } } in - + let cname = Option.map unloc subtype.pst_cname in let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in - + let renames = match subtype.pst_rename with | None -> [] @@ -2043,7 +2067,7 @@ module Ty = struct ) in let proofs = Cloning.replay_proofs scope `Check proofs in - + Ax.add_defer scope proofs (* ------------------------------------------------------------------ *) diff --git a/src/ecScope.mli b/src/ecScope.mli index bc3c2812d1..8709187cfc 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -98,6 +98,11 @@ module Op : sig val add_opsem : scope -> pprocop located -> scope end +(* -------------------------------------------------------------------- *) +module Except : sig + val add : scope -> pexception_decl located -> EcDecl.excep * scope +end + (* -------------------------------------------------------------------- *) module Pred : sig val add : scope -> ppredicate located -> EcDecl.operator * scope diff --git a/src/ecSection.ml b/src/ecSection.ml index cdd5b1cb27..932fb9b0ef 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -18,6 +18,7 @@ type cbarg = [ | `Type of path | `Op of path | `Ax of path + | `Ex of path | `Module of mpath | `ModuleType of path | `Typeclass of path @@ -39,6 +40,7 @@ let pp_cbarg env fmt (who : cbarg) = | `Type p -> Format.fprintf fmt "type %a" (EcPrinting.pp_tyname ppe) p | `Op p -> Format.fprintf fmt "operator %a" (EcPrinting.pp_opname ppe) p | `Ax p -> Format.fprintf fmt "lemma/axiom %a" (EcPrinting.pp_axname ppe) p + | `Ex _p -> Format.fprintf fmt "TODO" | `Module mp -> let ppe = match mp.m_top with @@ -157,8 +159,8 @@ let rec on_instr (cb : cb) (i : instr)= on_lv cb lv; on_expr cb e - | Sassert e -> - on_expr cb e + | Sraise (_,es) -> + List.iter (on_expr cb) es | Scall (lv, f, args) -> lv |> oiter (on_lv cb); @@ -425,6 +427,10 @@ let on_axiom (cb : cb) (ax : axiom) = on_typarams cb ax.ax_tparams; on_form cb ax.ax_spec +(* -------------------------------------------------------------------- *) +let on_except (cb : cb) (e : excep) = + on_typarams cb e.e_typargs + (* -------------------------------------------------------------------- *) let on_modsig (cb:cb) (ms:module_sig) = List.iter (fun (_,mt) -> on_modty cb mt) ms.mis_params; @@ -507,6 +513,7 @@ let locality (env : EcEnv.env) (who : cbarg) = | `Type p -> (EcEnv. Ty.by_path p env).tyd_loca | `Op p -> (EcEnv. Op.by_path p env).op_loca | `Ax p -> (EcEnv. Ax.by_path p env).ax_loca + | `Ex _p -> assert false | `Typeclass p -> ((EcEnv.TypeClass.by_path p env).tc_loca :> locality) | `Module mp -> begin match EcEnv.Mod.by_mpath_opt mp env with @@ -1043,6 +1050,7 @@ let rec set_lc_item lc_override item = match item.ti_item with | Th_type (s,ty) -> Th_type (s, { ty with tyd_loca = set_lc lc_override ty.tyd_loca }) | Th_operator (s,op) -> Th_operator (s, { op with op_loca = set_lc lc_override op.op_loca }) + | Th_exception (s,e) -> Th_exception (s, { e with e_loca = set_lc lc_override e.e_loca }) | Th_axiom (s,ax) -> Th_axiom (s, { ax with ax_loca = set_lc lc_override ax.ax_loca }) | Th_modtype (s,ms) -> Th_modtype (s, { ms with tms_loca = set_lc lc_override ms.tms_loca }) | Th_module me -> Th_module { me with tme_loca = set_lc lc_override me.tme_loca } @@ -1102,6 +1110,7 @@ type can_depend = { d_ty : locality list; d_op : locality list; d_ax : locality list; + d_ex : locality list; d_sc : locality list; d_mod : locality list; d_modty : locality list; @@ -1112,6 +1121,7 @@ let cd_glob = { d_ty = [`Global]; d_op = [`Global]; d_ax = [`Global]; + d_ex = [`Global]; d_sc = [`Global]; d_mod = [`Global]; d_modty = [`Global]; @@ -1122,6 +1132,7 @@ let can_depend (cd : can_depend) = function | `Type _ -> cd.d_ty | `Op _ -> cd.d_op | `Ax _ -> cd.d_ax + | `Ex _ -> cd.d_ex | `Sc _ -> cd.d_sc | `Module _ -> cd.d_mod | `ModuleType _ -> cd.d_modty @@ -1154,6 +1165,7 @@ let check_tyd scenv prefix name tyd = d_ty = [`Declare; `Global]; d_op = [`Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Global]; d_modty = []; @@ -1200,6 +1212,7 @@ let check_op scenv prefix name op = d_ty = [`Declare; `Global]; d_op = [`Declare; `Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Declare; `Global]; d_modty = []; @@ -1212,6 +1225,7 @@ let check_op scenv prefix name op = d_ty = [`Declare; `Global]; d_op = [`Declare; `Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Global]; d_modty = []; @@ -1231,6 +1245,7 @@ let check_ax (scenv : scenv) (prefix : path) (name : symbol) (ax : axiom) = d_ty = [`Declare; `Global]; d_op = [`Declare; `Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Declare; `Global]; d_modty = [`Global]; @@ -1261,6 +1276,33 @@ let check_ax (scenv : scenv) (prefix : path) (name : symbol) (ax : axiom) = doit ax end +let check_except (scenv : scenv) (prefix : path) (name : symbol) (e : excep) = + let path = EcPath.pqname prefix name in + let from = e.e_loca, `Ex path in + let cd = { + d_ty = [`Declare; `Global]; + d_op = [`Declare; `Global]; + d_ax = []; + d_ex = []; + d_sc = []; + d_mod = [`Declare; `Global]; + d_modty = [`Global]; + d_tc = [`Global]; + } in + let doit = on_except (cb scenv from cd) in + + match e.e_loca with + | `Local -> + check_section scenv from + + | `Declare -> + check_section scenv from; + check_polymorph scenv from e.e_typargs; + doit e + + | `Global -> + if scenv.sc_insec then doit e + let check_modtype scenv prefix name ms = let path = pqname prefix name in let from = ((ms.tms_loca :> locality), `ModuleType path) in @@ -1283,6 +1325,7 @@ let check_module scenv prefix tme = { d_ty = [`Global]; d_op = [`Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Global]; (* FIXME section: add local *) d_modty = [`Global]; @@ -1344,6 +1387,7 @@ let add_item_ ?(override_locality=None) (item : theory_item) (scenv:scenv) = | Th_type (s,tyd) -> EcEnv.Ty.bind ~import s tyd env | Th_operator (s,op) -> EcEnv.Op.bind ~import s op env | Th_axiom (s, ax) -> EcEnv.Ax.bind ~import s ax env + | Th_exception (s,e) -> EcEnv.Except.bind ~import s e env | Th_modtype (s, ms) -> EcEnv.ModTy.bind ~import s ms env | Th_module me -> EcEnv.Mod.bind ~import me.tme_expr.me_name me env | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind ~import s tc env @@ -1372,6 +1416,7 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i match th_item.ti_item with | Th_type tydecl -> generalize_tydecl to_gen prefix tydecl | Th_operator opdecl -> generalize_opdecl to_gen prefix opdecl + | Th_exception _ -> assert false | Th_axiom ax -> generalize_axiom to_gen prefix ax | Th_modtype ms -> generalize_modtype to_gen ms | Th_module me -> generalize_module to_gen prefix me @@ -1443,7 +1488,7 @@ let genenv_of_scenv (scenv : scenv) : to_gen = ; tg_params = [] ; tg_binds = [] ; tg_subst = EcSubst.empty - ; tg_clear = empty_locals } + ; tg_clear = empty_locals } let generalize_lc_items scenv = let togen = @@ -1452,7 +1497,7 @@ let generalize_lc_items scenv = (EcEnv.root scenv.sc_env) (List.rev scenv.sc_items) in togen.tg_env - + (* -----------------------------------------------------------*) let import p scenv = { scenv with sc_env = EcEnv.Theory.import p scenv.sc_env } @@ -1476,6 +1521,7 @@ let check_item scenv item = match item.ti_item with | Th_type (s,tyd) -> check_tyd scenv prefix s tyd | Th_operator (s,op) -> check_op scenv prefix s op + | Th_exception (s,e) -> check_except scenv prefix s e | Th_axiom (s, ax) -> check_ax scenv prefix s ax | Th_modtype (s, ms) -> check_modtype scenv prefix s ms | Th_module me -> check_module scenv prefix me @@ -1521,6 +1567,7 @@ let add_decl_mod id mt scenv = d_ty = [`Global]; d_op = [`Global]; d_ax = []; + d_ex = []; d_sc = []; d_mod = [`Declare; `Global]; d_modty = [`Global]; diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 45bdb2f747..ab36f59c17 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -426,8 +426,9 @@ and subst_instr (s : subst) (i : instr) : instr = i_match (e, bs) - | Sassert e -> - i_assert (subst_expr s e) + | Sraise (e,es) -> + let es' = List.map (subst_expr s) es in + i_raise (e,es') | Sabstract _ -> i @@ -534,14 +535,24 @@ let rec subst_form (s : subst) (f : form) = let s = add_memory s hf.hf_m hf.hf_m in let hf_pr = map_ss_inv1 (subst_form s) (hf_pr hf) in let hf_po = map_ss_inv1 (subst_form s) (hf_po hf) in - f_hoareF hf_pr hf_f hf_po + let hf_poe = + List.map + (fun (e,f) -> e, map_ss_inv1 (subst_form s) f) + (hf_poe hf) + in + f_hoareF hf_pr hf_f hf_po hf_poe | FhoareS hs -> let hs_s = subst_stmt s hs.hs_s in let s, (_,mt) = subst_memtype s hs.hs_m in let hs_pr = map_ss_inv1 (subst_form s) (hs_pr hs) in let hs_po = map_ss_inv1 (subst_form s) (hs_po hs) in - f_hoareS mt hs_pr hs_s hs_po + let hs_poe = + List.map + (fun (e,f) -> e, map_ss_inv1 (subst_form s) f) + (hs_poe hs) + in + f_hoareS mt hs_pr hs_s hs_po hs_poe | FbdHoareF bhf -> let bhf_f = subst_xpath s bhf.bhf_f in @@ -952,6 +963,14 @@ let subst_op (s : subst) (op : operator) = op_clinline = op.op_clinline; op_unfold = op.op_unfold ; } +(* -------------------------------------------------------------------- *) +let subst_excep (s : subst) (e : excep) = + let _, tparams = fresh_tparams s e.e_typargs in + + { e_typargs = tparams ; + e_loca = e.e_loca ; + } + (* -------------------------------------------------------------------- *) let subst_ax (s : subst) (ax : axiom) = let s, tparams = fresh_tparams s ax.ax_tparams in @@ -1024,6 +1043,9 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = | Th_operator (x, op) -> Th_operator (x, subst_op s op) + | Th_exception (e, es) -> + Th_exception (e, subst_excep s es) + | Th_axiom (x, ax) -> Th_axiom (x, subst_ax s ax) @@ -1165,14 +1187,14 @@ let ts_inv_rebind ({inv;ml;mr}: ts_inv) (ml': memory) (mr': memory) : ts_inv = | true, true -> { inv; ml; mr } | false, true -> assert (mr <> ml'); ts_inv_rebind_left {inv;ml;mr} ml' | true, false -> assert (ml <> mr'); ts_inv_rebind_right {inv;ml;mr} mr' - | false, false -> begin + | false, false -> begin let s = add_memory empty ml ml' in let s = add_memory s mr mr' in let inv = subst_form s inv in { inv; ml = ml'; mr = mr' } end -let f_forall_mems_ts_inv menvl menvr inv = +let f_forall_mems_ts_inv menvl menvr inv = f_forall_mems [menvl; menvr] (ts_inv_rebind inv (fst menvl) (fst menvr)).inv let ss_inv_forall_ml_ts_inv menvl inv = @@ -1181,4 +1203,4 @@ let ss_inv_forall_ml_ts_inv menvl inv = let ss_inv_forall_mr_ts_inv menvr inv = let inv' = f_forall_mems [menvr] (ts_inv_rebind_right inv (fst menvr)).inv in - { inv=inv'; m=inv.ml } \ No newline at end of file + { inv=inv'; m=inv.ml } diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index a2f24e593a..b344535b1f 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -304,7 +304,7 @@ end = struct (fun evc -> if Msym.mem x evc.evc_ops then clone_error oc.oc_env (CE_DupOverride (OVK_Operator, name)); - { evc with evc_ops = + { evc with evc_ops = Msym.add x (mk_loc lc opd :> xop_override located) evc.evc_ops }) nm evc @@ -437,6 +437,8 @@ end = struct let ovrd = (ovrd, mode) in nt_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd + | Th_exception _ -> (proofs, evc) + | Th_axiom (x, _) -> let axd = loced (thd @ prefix, x) in let name = (loced (xdth @ prefix, x)) in diff --git a/src/ecTheory.ml b/src/ecTheory.ml index ffe226d060..4f5c4f7984 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -21,6 +21,7 @@ and theory_item = { and theory_item_r = | Th_type of (symbol * tydecl) | Th_operator of (symbol * operator) + | Th_exception of (symbol * excep) | Th_axiom of (symbol * axiom) | Th_modtype of (symbol * top_module_sig) | Th_module of top_module_expr diff --git a/src/ecTheory.mli b/src/ecTheory.mli index f246ee3f40..2b8551ed40 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -17,6 +17,7 @@ and theory_item = { and theory_item_r = | Th_type of (symbol * tydecl) | Th_operator of (symbol * operator) + | Th_exception of (symbol * excep) | Th_axiom of (symbol * axiom) | Th_modtype of (symbol * top_module_sig) | Th_module of top_module_expr diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 0eff5cf66d..8542c11f2c 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -594,7 +594,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = ~opaque:optransparent ~clinline:(opmode <> `Alias) [] body.f_ty (Some (OP_Plain body)) refop.op_loca in (newop, body) - + in match opmode with | `Alias -> @@ -785,6 +785,14 @@ and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oont) = (subst, ops, proofs, scope) end + +(* -------------------------------------------------------------------- *) +and replay_excep + (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, excep) += + let scope = ove.ovre_hooks.hadd_item scope ~import (Th_exception (name, excep)) in + (subst, ops, proofs, scope) + (* -------------------------------------------------------------------- *) and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) = let scenv = ove.ovre_hooks.henv scope in @@ -1100,6 +1108,9 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) = | Th_operator (x, ({ op_kind = OB_nott _} as oont)) -> replay_ntd ove (subst, ops, proofs, scope) (import, x, oont) + | Th_exception (x, e) -> + replay_excep ove (subst, ops, proofs, scope) (import, x, e) + | Th_axiom (x, ax) -> replay_axd ove (subst, ops, proofs, scope) (import, x, ax) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 75f594a105..e9daa90ac1 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -153,6 +153,7 @@ type tyerror = | UnknownModName of qsymbol | UnknownTyModName of qsymbol | UnknownFunName of qsymbol +| UnknownExceptionName of qsymbol | UnknownModVar of qsymbol | UnknownMemName of symbol | InvalidFunAppl of funapp_error @@ -283,8 +284,8 @@ let (_i_inuse, s_inuse, se_inuse) = let map = List.fold_left (fun map -> s_inuse map |- snd) map bs in map - | Sassert e -> - se_inuse map e + | Sraise (_,args) -> + List.fold_left se_inuse map args | Sabstract _ -> assert false (* FIXME *) @@ -1466,6 +1467,13 @@ let trans_gamepath (env : EcEnv.env) gp = tyerror gp.pl_loc env (UnknownFunName (modsymb, funsymb)); EcPath.xpath mpath funsymb +let except_genpath env name = + let modsymb = List.map (unloc -| fst) (fst (unloc name)) + and symb = unloc (snd (unloc name)) in + match EcEnv.Except.lookup_opt (modsymb, symb) env with + | None -> tyerror name.pl_loc env (UnknownExceptionName (modsymb, symb)) + | Some (p,_) -> symb, p + (* -------------------------------------------------------------------- *) let trans_oracle (env : EcEnv.env) (m,f) = let msymbol = mk_loc (loc m) [m,None] in @@ -1606,7 +1614,7 @@ let form_of_opselect in (op, args) - in + in f_app op args codom (* -------------------------------------------------------------------- *) @@ -1683,6 +1691,10 @@ let f_or_mod_ident_loc : f_or_mod_ident -> EcLocation.t = function | FM_FunOrVar x -> loc x | FM_Mod x -> loc x +(* -------------------------------------------------------------------- *) +let check_unique_epost epost = + List.is_unique ~eq:(fun (e1,_) (e2,_) -> EcPath.p_ntr_equal e1 e2) epost + (* -------------------------------------------------------------------- *) let trans_restr_mem env (r_mem : pmod_restr_mem) = @@ -2749,10 +2761,43 @@ and transinstr [ i_match (e, branches) ] end - | PSassert pe -> - let e, ety = transexp env `InProc ue pe in - unify_or_fail env ue pe.pl_loc ~expct:tbool ety; - [ i_assert e ] + | PSraise (name, args) -> + let _,path = except_genpath env name in + let esig = (EcEnv.Except.by_path path env).e_typargs in + let aux (_,s) = + match Sp.elements s with + | [recp] -> recp + | _ -> assert false + in + let paths = List.map aux esig in + let indty = + List.map (fun path -> + oget (EcEnv.Ty.by_path_opt path env) + ) paths + in + let ind = + List.map (fun typdecl -> + let x = oget (EcDecl.tydecl_as_datatype typdecl) in + match x.tydt_ctors with + | [(_,t)] -> t + | _ -> assert false + ) indty + in + let typs = List.flatten ind in + + let args = unloc args in + let loc = name.pl_loc in + let args = + if List.length args <> List.length typs then + tyerror loc env (InvalidFunAppl FAE_WrongArgCount); + List.map2 + (fun a ty -> + let loc = a.pl_loc in + let a, aty = transexp env `InProc ue a in + unify_or_fail env ue loc ~expct:ty aty; a) args typs + in + + [i_raise (path, args)] (* -------------------------------------------------------------------- *) and trans_pv env { pl_desc = x; pl_loc = loc } = @@ -3195,7 +3240,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = @ List.map (fun (xp, ty) -> f_pvar (EcTypes.pv_glob xp) ty mem) pv in map_ss_inv f_tuple res in - + let ml, mr = oget (EcEnv.Memory.get_active_ts env) in let x1 = ss_inv_generalize_right (create ml) mr in let x2 = ss_inv_generalize_left (create mr) ml in @@ -3442,7 +3487,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = unify_or_fail env ue event.pl_loc ~expct:tbool event'.inv.f_ty; f_pr memid fpath (f_tuple args) event' - | PFhoareF (m, pre, gp, post) -> + | PFhoareF (m, pre, gp, post, eposts) -> if mode <> `Form then tyerror f.pl_loc env (NotAnExpression `Logic); let fpath = trans_gamepath env gp in @@ -3451,9 +3496,24 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let penv, qenv = EcEnv.Fun.hoareF m fpath env in let pre' = transf penv pre in let post' = transf qenv post in - unify_or_fail penv ue pre.pl_loc ~expct:tbool pre' .f_ty; - unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty; - f_hoareF {m;inv=pre'} fpath {m;inv=post'} + let epost' = + List.map + (fun (e,f) -> + let _,p = except_genpath env e in + p,transf penv f) + eposts + in + + unify_or_fail penv ue pre.pl_loc ~expct:tbool pre'.f_ty; + unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty; + List.iter + (fun (_,f) -> unify_or_fail qenv ue post.pl_loc ~expct:tbool f.f_ty) + epost'; + + if check_unique_epost epost' then + let epost' = List.map (fun (e,f) -> e,{m;inv=f}) epost' in + f_hoareF {m;inv=pre'} fpath {m;inv=post'} epost' + else assert false | PFehoareF (m, pre, gp, post) -> if mode <> `Form then diff --git a/src/ecTyping.mli b/src/ecTyping.mli index bf2da3aa21..994275d645 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -145,6 +145,7 @@ type tyerror = | UnknownModName of qsymbol | UnknownTyModName of qsymbol | UnknownFunName of qsymbol +| UnknownExceptionName of qsymbol | UnknownModVar of qsymbol | UnknownMemName of symbol | InvalidFunAppl of funapp_error @@ -253,6 +254,9 @@ val trans_pattern : env -> ptnmap -> EcUnify.unienv -> pformula -> EcFol.form val trans_memtype : env -> EcUnify.unienv -> pmemtype -> EcMemory.memtype +(* -------------------------------------------------------------------- *) +val check_unique_epost: (EcPath.path * 'a) list -> bool + (* -------------------------------------------------------------------- *) val trans_restr_for_modty : env -> module_type -> pmod_restr option -> mty_mr @@ -264,6 +268,7 @@ val transmod : attop:bool -> env -> pmodule_def -> module_expr val trans_topmsymbol : env -> pmsymbol located -> mpath val trans_msymbol : env -> pmsymbol located -> mpath * module_smpl_sig val trans_gamepath : env -> pgamepath -> xpath +val except_genpath : env -> pgamepath -> symbol * path val trans_oracle : env -> psymbol * psymbol -> xpath val trans_restr_mem : env -> pmod_restr_mem -> mod_restr diff --git a/src/ecUnifyProc.ml b/src/ecUnifyProc.ml index e7ef218a70..f6284c88d6 100644 --- a/src/ecUnifyProc.ml +++ b/src/ecUnifyProc.ml @@ -170,8 +170,24 @@ let rec unify_instrs env umap i1 i2 = unify_stmts env umap b1 b2 ) umap bs1 bs2 - | Sassert e1, Sassert e2 -> - unify_exprs env umap e1 e2 + | Sraise (_,args1), Sraise (_,args2) -> + let args1, args2 = + match args1, args2 with + | _, _ when List.length args1 = List.length args2 -> args1, args2 + | [al], _ -> begin + match al.e_node with + | Etuple args1 -> args1, args2 + | _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2))) + end + | _, [ar] -> begin + match ar.e_node with + | Etuple args2 -> args1, args2 + | _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2))) + end + | _, _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2))) + in + + List.fold_left (fun umap (e1, e2) -> unify_exprs env umap e1 e2) umap (List.combine args1 args2) | Sabstract x1, Sabstract x2 when EcIdent.id_equal x1 x2 -> umap @@ -245,4 +261,3 @@ let unify_func env mode fname s = lv_of_list pvs in s_call (alias, fname, args) - diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index 9c947c1b6c..985616507c 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -423,7 +423,10 @@ end = struct msg "unknown type name: %a" pp_qsymbol name | UnknownFunName name -> - msg "unknown procedure: %a" pp_qsymbol name + msg "unknown procedure: %a" pp_qsymbol name + + | UnknownExceptionName name -> + msg "unknown exception: %a" pp_qsymbol name | UnknownModVar x -> msg "unknown module-level variable: %a" pp_qsymbol x diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlApp.ml index d632864299..8ca5665410 100644 --- a/src/phl/ecPhlApp.ml +++ b/src/phl/ecPhlApp.ml @@ -19,8 +19,8 @@ let t_hoare_app_r i phi tc = let hs = tc1_as_hoareS tc in let phi = ss_inv_rebind phi (fst hs.hs_m) in let s1, s2 = s_split env i hs.hs_s in - let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) phi in - let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in + let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) phi (hs_poe hs) in + let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) (hs_poe hs) in FApi.xmutate1 tc `HlApp [a; b] let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r @@ -51,7 +51,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc = let s1, s2 = stmt s1, stmt s2 in let nR = map_ss_inv1 f_not pR in let mt = snd bhs.bhs_m in - let cond_phi = f_hoareS mt (bhs_pr bhs) s1 phi in + let cond_phi = f_hoareS mt (bhs_pr bhs) s1 phi [] in let condf1 = f_bdHoareS mt (bhs_pr bhs) s1 pR bhs.bhs_cmp f1 in let condg1 = f_bdHoareS mt (bhs_pr bhs) s1 nR bhs.bhs_cmp g1 in let condf2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi pR) s2 (bhs_po bhs) bhs.bhs_cmp f2 in @@ -67,11 +67,11 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc = let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in let condnm = - let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2) + let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2) (map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in f_forall [(ir1, GTty treal); (ir2, GTty treal)] - (f_hoareS (snd bhs.bhs_m) (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 eqs) in + (f_hoareS (snd bhs.bhs_m) (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 eqs []) in let conds = [EcSubst.f_forall_mems_ss_inv bhs.bhs_m condbd; condnm] in let conds = if f_equal g1.inv f_r0 @@ -95,7 +95,12 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc = let t_bdhoare_app_r i info tc = let tactic tc = let hs = tc1_as_hoareS tc in - let tt1 = EcPhlConseq.t_hoareS_conseq_nm (hs_pr hs) {m=(fst hs.hs_m);inv=f_true} in + let tt1 = + EcPhlConseq.t_hoareS_conseq_nm + (hs_pr hs) + {m=(fst hs.hs_m);inv=f_true} + (hs_poe hs) + in let tt2 = EcPhlAuto.t_pl_trivial in FApi.t_seqs [tt1; tt2; t_fail] tc in @@ -124,11 +129,11 @@ let t_equiv_app_onesided side i pre post tc = let (ml, mr) = fst es.es_ml, fst es.es_mr in let s, s', p', q' = match side with - | `Left -> + | `Left -> let p' = ss_inv_generalize_right (EcSubst.ss_inv_rebind pre ml) mr in let q' = ss_inv_generalize_right (EcSubst.ss_inv_rebind post ml) mr in es.es_sl, es.es_sr, p', q' - | `Right -> + | `Right -> let p' = ss_inv_generalize_left (EcSubst.ss_inv_rebind pre mr) ml in let q' = ss_inv_generalize_left (EcSubst.ss_inv_rebind post mr) ml in es.es_sr, es.es_sl, p', q' diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 298e0588d6..9cf3f383d8 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -59,14 +59,25 @@ let wp2_call map_ts_inv2 f_anda_simpl (map_ts_inv1 (PVM.subst env spre) fpre) post (* -------------------------------------------------------------------- *) -let t_hoare_call fpre fpost tc = +let find_poe epost e = + snd (List.find (fun (e',_) -> EcPath.p_ntr_equal e e') epost) + +let call_conde env spre poe1 poe2 = + List.map + (fun (e1,p1) -> + let p2 = find_poe poe2 e1 in + let aux = map_ss_inv1 (PVM.subst env spre) in + map_ss_inv2 f_imp_simpl (aux p1) (aux p2)) + poe1 + +let t_hoare_call fpre fpost fepost tc = let env = FApi.tc1_env tc in let hs = tc1_as_hoareS tc in let (lp,f,args),s = tc1_last_call tc hs.hs_s in let m = EcMemory.memory hs.hs_m in let fsig = (Fun.by_xpath f env).f_sig in (* The function satisfies the specification *) - let f_concl = f_hoareF fpre f fpost in + let f_concl = f_hoareF fpre f fpost fepost in (* substitute memories *) let fpre = (ss_inv_rebind fpre m) in let fpost = (ss_inv_rebind fpost m) in @@ -81,11 +92,13 @@ let t_hoare_call fpre fpost tc = let post = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) post in let spre = subst_args_call env m (e_tuple args) PVM.empty in let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in - let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in - + let poe = List.map (fun (e,f) -> e, map_ss_inv1 (PVM.subst env spre) f) (hs_poe hs) in + let fepost = List.map (fun (e,f) -> e,ss_inv_rebind f m) fepost in + let poe = call_conde env spre fepost poe in + let post = List.fold (map_ss_inv2 f_anda_simpl) post poe in + let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post (hs_poe hs)in FApi.xmutate1 tc `HlCall [f_concl; concl] - (* -------------------------------------------------------------------- *) let ehoare_call_pre_post fpre fpost tc = let (env, hyps, _) = FApi.tc1_eflat tc in @@ -152,7 +165,7 @@ let t_ehoare_call fpre fpost tc = let t_ehoare_call_concave f fpre fpost tc = let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) + EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) (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 = @@ -219,11 +232,11 @@ let t_bdhoare_call fpre fpost opt_bd tc = let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in (* most of the above code is duplicated from t_hoare_call *) - let concl = + let concl = let _,mt = bhs.bhs_m in match bhs.bhs_cmp, opt_bd with | FHle, None -> - f_hoareS mt bhs_pr s post + f_hoareS mt bhs_pr s post [] | FHeq, Some bd -> f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd) | FHeq, None -> @@ -332,7 +345,7 @@ let t_call side ax tc = let (_, f, _), _ = tc1_last_call tc hs.hs_s in if not (EcEnv.NormMp.x_equal env hf.hf_f f) then call_error env tc hf.hf_f f; - t_hoare_call (hf_pr hf) (hf_po hf) tc + t_hoare_call (hf_pr hf) (hf_po hf) (hf_poe hf) tc | FeHoareF hf, FeHoareS hs -> let (_, f, _), _ = tc1_last_call tc hs.ehs_s in @@ -410,17 +423,9 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr = f_equivF pre fl fr post let process_call side info tc = - let process_spec tc side pre post = + let process_spec_2 tc side pre post = let (hyps, concl) = FApi.tc1_flat tc in match concl.f_node, side with - | FhoareS hs, None -> - let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let m = (EcIdent.create "&hr") in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in - f_hoareF {m;inv=pre} f {m;inv=post} - | FbdHoareS bhs, None -> let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in let m = (EcIdent.create "&hr") in @@ -435,7 +440,7 @@ let process_call side info tc = let m = (EcIdent.create "&hr") in let penv, qenv = LDecl.hoareF m f hyps in let pre = TTC.pf_process_form !!tc penv txreal pre in - let post = TTC.pf_process_form !!tc qenv txreal post in + let post = TTC.pf_process_form !!tc qenv txreal post in f_eHoareF {m;inv=pre} f {m;inv=post} | FbdHoareS _, Some _ @@ -448,7 +453,7 @@ let process_call side info tc = let (ml, mr) = (EcIdent.create "&1", EcIdent.create "&2") in let penv, qenv = LDecl.equivF ml mr fl fr hyps in let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in + let post = TTC.pf_process_form !!tc qenv tbool post in f_equivF {ml;mr;inv=pre} fl fr {ml;mr;inv=post} | FequivS es, Some side -> @@ -462,21 +467,37 @@ let process_call side info tc = | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in - let process_inv tc side inv = + let process_spec_1 tc side pre post poe = + let (hyps, concl) = FApi.tc1_flat tc in + match concl.f_node, side with + | FhoareS hs, None -> + let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in + let m = (EcIdent.create "&hr") in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = TTC.pf_process_form !!tc penv tbool pre in + let post = TTC.pf_process_form !!tc qenv tbool post in + let env = LDecl.toenv hyps in + let poe = + List.map + (fun (e,f) -> + let _,e = EcTyping.except_genpath env e in + let f = TTC.pf_process_form !!tc penv tbool f in + e,{m;inv=f}) + poe + in + if EcTyping.check_unique_epost poe then + f_hoareF {m;inv=pre} f {m;inv=post} poe + else assert false + + | _ -> tc_error !!tc "the conclusion is not a hoare" in + + + let process_inv_1 tc side inv = if not (is_none side) then tc_error !!tc "cannot specify side for call with invariants"; let hyps, concl = FApi.tc1_flat tc in match concl.f_node with - | FhoareS hs -> - let m = fst hs.hs_m in - let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let me = EcMemory.abstract m in - let hyps = LDecl.push_active_ss me hyps in - let inv = TTC.pf_process_form !!tc hyps tbool inv in - let inv = {m; inv} in - (f_hoareF inv f inv, Inv_ss inv) - | FeHoareS hs -> let m = fst hs.ehs_m in let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in @@ -509,6 +530,35 @@ let process_call side info tc = | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in + let process_inv_2 tc side inv poe = + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + + let hyps, concl = FApi.tc1_flat tc in + match concl.f_node with + | FhoareS hs -> + let m = fst hs.hs_m in + let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in + let me = EcMemory.abstract m in + let hyps = LDecl.push_active_ss me hyps in + let inv = TTC.pf_process_form !!tc hyps tbool inv in + let inv = {m; inv} in + let env = LDecl.toenv hyps in + let poe = + List.map + (fun (e,f) -> + let _,e = EcTyping.except_genpath env e in + let f = TTC.pf_process_form !!tc hyps tbool f in + e,{m;inv=f}) + poe + in + if EcTyping.check_unique_epost poe then + (f_hoareF inv f inv poe, Inv_ss inv) + else assert false + + | _ -> tc_error !!tc "the conclusion is not a hoare" in + + let process_upto tc side info = if not (is_none side) then tc_error !!tc "cannot specify side for call with invariants"; @@ -541,13 +591,32 @@ let process_call side info tc = let process_cut tc info = match info with - | CI_spec (pre, post) -> - process_spec tc side pre post - | CI_inv inv -> - let f, inv = process_inv tc side inv in - subtactic := (fun tc -> - FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc)); - f + | CI_spec (pre, post, poe) -> + begin + let _, concl = FApi.tc1_flat tc in + match concl.f_node with + | FhoareS _ -> + process_spec_1 tc side pre post poe + | _ -> + process_spec_2 tc side pre post + end + + | CI_inv (inv, poe) -> + begin + let _, concl = FApi.tc1_flat tc in + match concl.f_node with + | FhoareS _ -> + let f, inv = process_inv_2 tc side inv poe in + subtactic := (fun tc -> + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc)); + f + + | _ -> + let f, inv = process_inv_1 tc side inv in + subtactic := (fun tc -> + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc)); + f + end | CI_upto info -> let bad, p, q, form = process_upto tc side info in @@ -614,13 +683,13 @@ let process_call_concave (fc, info) tc = let process_cut tc info = match info with - | CI_spec (pre, post) -> + | CI_spec (pre, post, []) -> let ty,fmake = process_spec tc in let _, pre = TTC.tc1_process_Xhl_form tc ty pre in let _, post = TTC.tc1_process_Xhl_form tc ty post in fmake pre post - | CI_inv inv -> + | CI_inv (inv, []) -> let ty, fmake = process_inv tc in let _, inv = TTC.tc1_process_Xhl_form tc ty inv in subtactic := (fun tc -> diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli index 79da81f636..f1df7d867f 100644 --- a/src/phl/ecPhlCall.mli +++ b/src/phl/ecPhlCall.mli @@ -13,7 +13,7 @@ val wp2_call : -> ts_inv -> EcEnv.LDecl.hyps -> ts_inv -val t_hoare_call : ss_inv -> ss_inv -> backward +val t_hoare_call : ss_inv -> ss_inv -> (EcPath.path * ss_inv) list -> backward val t_bdhoare_call : ss_inv -> ss_inv -> ss_inv option -> backward val t_equiv_call : ts_inv -> ts_inv -> backward val t_equiv_call1 : side -> ss_inv -> ss_inv -> backward diff --git a/src/phl/ecPhlCase.ml b/src/phl/ecPhlCase.ml index 069c05035d..d1ac72eab9 100644 --- a/src/phl/ecPhlCase.ml +++ b/src/phl/ecPhlCase.ml @@ -9,8 +9,17 @@ let t_hoare_case_r ?(simplify = true) f tc = let fand = if simplify then f_and_simpl else f_and in let hs = tc1_as_hoareS tc in let mt = snd hs.hs_m in - let concl1 = f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs) in - let concl2 = f_hoareS mt (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f)) hs.hs_s (hs_po hs) in + let concl1 = + f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs) (hs_poe hs) + in + let concl2 = + f_hoareS + mt + (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f)) + hs.hs_s + (hs_po hs) + (hs_poe hs) + in FApi.xmutate1 tc (`HlCase f) [concl1; concl2] (* --------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 0cc9e48b4f..c47c809c66 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -236,11 +236,11 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) ( | e, _ -> [e] in let lv = lv_to_ty_list lv in - + let tosubst, asgn2 = List.partition (fun ((pv, _), e) -> Mpv.mem env pv subst0 && is_const_expression e ) (List.combine lv es) in - + let subst = List.fold_left (fun subst ((pv, _), e) -> Mpv.add env pv e subst) @@ -368,7 +368,7 @@ let process_set_match (side, cpos, id, pattern) tc = t_set_match side cpos (EcLocation.unloc id) (ue, EcMatching.MEV.of_idents (Mid.keys !ptnmap) `Form, pattern) tc - + (* -------------------------------------------------------------------- *) let process_weakmem (side, id, params) tc = let open EcLocation in @@ -397,7 +397,7 @@ let process_weakmem (side, id, params) tc = match f.f_node with | FhoareS hs -> let _, mt = bind hs.hs_m in - f_hoareS mt (hs_pr hs) hs.hs_s (hs_po hs) + f_hoareS mt (hs_pr hs) hs.hs_s (hs_po hs) (hs_poe hs) | FeHoareS hs -> let _, mt = bind hs.ehs_m in diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 90a07c86ff..b70d84d902 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -39,11 +39,11 @@ let bd_goal_r fcmp fbd cmp bd = | FHle, (FHle | FHeq) -> Some (map_ss_inv2 f_real_le bd fbd) | FHge, (FHge | FHeq) -> Some (map_ss_inv2 f_real_le fbd bd) | FHeq, FHeq -> Some (map_ss_inv2 f_eq bd fbd) - | FHeq, FHge -> Some (map_ss_inv2 f_and - (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd) + | FHeq, FHge -> Some (map_ss_inv2 f_and + (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd) (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) bd)) - | FHeq, FHle -> Some (map_ss_inv2 f_and - (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd) + | FHeq, FHle -> Some (map_ss_inv2 f_and + (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd) (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) bd)) | _ , _ -> None @@ -58,28 +58,58 @@ let bd_goal tc fcmp fbd cmp bd = | Some fp -> fp (* -------------------------------------------------------------------- *) -let t_hoareF_conseq pre post tc = + +let find_poe epost e = + snd (List.find (fun (e',_) -> EcPath.p_ntr_equal e e') epost) + +let conseq_conde_ss poe1 poe2 = + assert (List.length poe1 = List.length poe2); + List.map + (fun (e1,p1) -> map_ss_inv2 f_imp (find_poe poe2 e1) p1) + poe1 + +let conseq_conde_conj_ss poe1 poe2 = + assert (List.length poe1 = List.length poe2); + List.map + (fun (e1,p1) -> e1,map_ss_inv2 f_and (find_poe poe2 e1) p1) + poe1 + +let check_eq_poe tc hyps poe1 poe2 = + assert (List.length poe1 = List.length poe2); + List.iter + (fun (e,f) -> + if not (ss_inv_alpha_eq hyps (find_poe poe2 e) f) + then tc_error !!tc "invalid exception post-condition") + poe1 + +let t_hoareF_conseq pre post epost tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in let pre = ss_inv_rebind pre hf.hf_m in let post = ss_inv_rebind post hf.hf_m in + let epost = List.map (fun (e,f) -> e,ss_inv_rebind f hf.hf_m) epost in let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f env in let cond1, cond2 = conseq_cond_ss (hf_pr hf) (hf_po hf) pre post in let concl1 = f_forall_mems_ss_inv mpr cond1 in let concl2 = f_forall_mems_ss_inv mpo cond2 in - let concl3 = f_hoareF pre hf.hf_f post in - FApi.xmutate1 tc `Conseq [concl1; concl2; concl3] + let cond2e = conseq_conde_ss (hf_poe hf) epost in + let concl2e = List.map (f_forall_mems_ss_inv mpo) cond2e in + let concl3 = f_hoareF pre hf.hf_f post epost in + FApi.xmutate1 tc `Conseq ([concl1; concl2; concl3] @ concl2e) (* -------------------------------------------------------------------- *) -let t_hoareS_conseq pre post tc = +let t_hoareS_conseq pre post epost tc = let hs = tc1_as_hoareS tc in let pre = ss_inv_rebind pre (fst hs.hs_m) in let post = ss_inv_rebind post (fst hs.hs_m) in + let epost = List.map (fun (e,f) -> e,ss_inv_rebind f (fst hs.hs_m)) epost in let cond1, cond2 = conseq_cond_ss (hs_pr hs) (hs_po hs) pre post in let concl1 = f_forall_mems_ss_inv hs.hs_m cond1 in let concl2 = f_forall_mems_ss_inv hs.hs_m cond2 in - let concl3 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in - FApi.xmutate1 tc `HlConseq [concl1; concl2; concl3] + let cond2e = conseq_conde_ss (hs_poe hs) epost in + let concl2e = List.map (f_forall_mems_ss_inv hs.hs_m) cond2e in + let concl3 = f_hoareS (snd hs.hs_m) pre hs.hs_s post epost in + FApi.xmutate1 tc `HlConseq ([concl1; concl2; concl3] @ concl2e) (* -------------------------------------------------------------------- *) let t_ehoareF_conseq pre post tc = @@ -205,8 +235,8 @@ let t_equivS_conseq pre post tc = (* -------------------------------------------------------------------- *) let t_conseq pre post tc = match (FApi.tc1_goal tc).f_node, pre, post with - | FhoareF _, Inv_ss pre, Inv_ss post -> t_hoareF_conseq pre post tc - | FhoareS _, Inv_ss pre, Inv_ss post -> t_hoareS_conseq pre post tc + | FhoareF _, Inv_ss pre, Inv_ss post -> t_hoareF_conseq pre post [] tc + | FhoareS _, Inv_ss pre, Inv_ss post -> t_hoareS_conseq pre post [] tc | FbdHoareF _, Inv_ss pre, Inv_ss post -> t_bdHoareF_conseq pre post tc | FbdHoareS _, Inv_ss pre, Inv_ss post -> t_bdHoareS_conseq pre post tc | FeHoareF _ , Inv_ss pre, Inv_ss post -> t_ehoareF_conseq pre post tc @@ -316,12 +346,19 @@ let cond_hoareF_notmod ?(mk_other=false) tc (cond: ss_inv) = else [] in cond, bmem, bother -let t_hoareF_notmod (post: ss_inv) tc = +let t_hoareF_notmod (post: ss_inv) epost tc = let hf = tc1_as_hoareF tc in let post = ss_inv_rebind post hf.hf_m in + let epost = List.map (fun (e,f) -> e,ss_inv_rebind f hf.hf_m) epost in let cond1, _, _ = cond_hoareF_notmod tc (map_ss_inv2 f_imp post (hf_po hf)) in - let cond2 = f_hoareF (hf_pr hf) hf.hf_f post in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] + let econd1 = List.map (fun (e1,p1) -> + let f = map_ss_inv2 f_imp (find_poe epost e1) p1 in + let cond1 , _, _ = cond_hoareF_notmod tc f in + cond1 + ) (hf_poe hf) + in + let cond2 = f_hoareF (hf_pr hf) hf.hf_f post epost in + FApi.xmutate1 tc `HlNotmod ([cond1; cond2] @econd1) (* -------------------------------------------------------------------- *) let cond_hoareS_notmod ?(mk_other=false) tc cond = @@ -339,12 +376,19 @@ let cond_hoareS_notmod ?(mk_other=false) tc cond = else [] in cond, bmem, bother -let t_hoareS_notmod post tc = +let t_hoareS_notmod post epost tc = let hs = tc1_as_hoareS tc in let post = ss_inv_rebind post (fst hs.hs_m) in + let epost = List.map (fun (e,f) -> e,ss_inv_rebind f (fst hs.hs_m)) epost in let cond1, _, _ = cond_hoareS_notmod tc (map_ss_inv2 f_imp post (hs_po hs)) in - let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s post in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] + let econd1 = List.map (fun (e1,p1) -> + let f = map_ss_inv2 f_imp (find_poe epost e1) p1 in + let cond1 , _, _ = cond_hoareS_notmod tc f in + cond1 + ) (hs_poe hs) + in + let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s post epost in + FApi.xmutate1 tc `HlNotmod ([cond1; cond2] @ econd1) (* -------------------------------------------------------------------- *) let cond_bdHoareF_notmod ?(mk_other=false) tc (cond: ss_inv) = @@ -417,15 +461,6 @@ let gen_conseq_nm tnm tc pre post = FApi.t_swap_goals 0 1 gs ) -let gen_conseq_nm_ss tnm tc (pre: ss_inv) (post: ss_inv) = - FApi.t_internal ~info:"generic-conseq-nm" (fun g -> - let gs = - (tnm post @+ - [ t_id; - tc pre post @+ [t_id; t_trivial; t_id] ]) g in - FApi.t_swap_goals 0 1 gs - ) - let gen_conseq_nm_ts tnm tc (pre: ts_inv) (post: ts_inv) = FApi.t_internal ~info:"generic-conseq-nm" (fun g -> let gs = @@ -435,12 +470,23 @@ let gen_conseq_nm_ts tnm tc (pre: ts_inv) (post: ts_inv) = FApi.t_swap_goals 0 1 gs ) -let t_hoareF_conseq_nm = gen_conseq_nm_ss t_hoareF_notmod t_hoareF_conseq -let t_hoareS_conseq_nm = gen_conseq_nm t_hoareS_notmod t_hoareS_conseq +let gen_conseq_nm_e tnm tc pre post epost = + let t_trivials = List.map (fun _ -> fun a -> t_trivial a) epost in + let t_ids = List.map (fun _ -> t_id) epost in + FApi.t_internal ~info:"generic-conseq-nm" (fun g -> + let back = tc pre post epost @+ ([t_id; t_trivial; t_id] @ t_trivials) in + let gs = + (tnm post epost @+ ([t_id] @ [back] @ t_ids)) g + in + FApi.t_swap_goals 0 1 gs + ) + +let t_hoareF_conseq_nm = gen_conseq_nm_e t_hoareF_notmod t_hoareF_conseq +let t_hoareS_conseq_nm = gen_conseq_nm_e t_hoareS_notmod t_hoareS_conseq let t_equivF_conseq_nm = gen_conseq_nm_ts t_equivF_notmod t_equivF_conseq -let t_equivS_conseq_nm = gen_conseq_nm t_equivS_notmod t_equivS_conseq -let t_bdHoareF_conseq_nm = gen_conseq_nm t_bdHoareF_notmod t_bdHoareF_conseq -let t_bdHoareS_conseq_nm = gen_conseq_nm t_bdHoareS_notmod t_bdHoareS_conseq +let t_equivS_conseq_nm = gen_conseq_nm t_equivS_notmod t_equivS_conseq +let t_bdHoareF_conseq_nm = gen_conseq_nm t_bdHoareF_notmod t_bdHoareF_conseq +let t_bdHoareS_conseq_nm = gen_conseq_nm t_bdHoareS_notmod t_bdHoareS_conseq (* -------------------------------------------------------------------- *) (* concavity (jenhsen) : E(f g2) <= f (E g2) @@ -614,7 +660,7 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc let pre = map_ss_inv1 (fun gpre -> pre |> omap (TTC.pf_process_form !!tc penv txreal) |> odfl gpre) gpre in let post = map_ss_inv1 (fun gpost -> post |> omap (TTC.pf_process_form !!tc qenv txreal) |> odfl gpost) gpost in - + fmake pre post in @@ -660,31 +706,35 @@ let t_hoareF_conseq_bdhoare tc = FApi.xmutate1 tc `HlConseqBd [concl1] (* -------------------------------------------------------------------- *) -let t_hoareS_conseq_conj pre post pre' post' tc = +let t_hoareS_conseq_conj pre post epost pre' post' epost' tc = let (_, hyps, _) = FApi.tc1_eflat tc in let hs = tc1_as_hoareS tc in let pre'' = map_ss_inv2 f_and pre' pre in let post'' = map_ss_inv2 f_and post' post in - if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'') - then tc_error !!tc "invalid pre-condition"; - if not (ss_inv_alpha_eq hyps (hs_po hs) post'') - then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in - let concl2 = f_hoareS (snd hs.hs_m) pre' hs.hs_s post' in + let poste'' = conseq_conde_conj_ss epost' epost in + if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'') + then tc_error !!tc "invalid pre-condition"; + if not (ss_inv_alpha_eq hyps (hs_po hs) post'') + then tc_error !!tc "invalid post-condition"; + check_eq_poe tc hyps (hs_poe hs) poste''; + let concl1 = f_hoareS (snd hs.hs_m) pre hs.hs_s post epost in + let concl2 = f_hoareS (snd hs.hs_m) pre' hs.hs_s post' epost' in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] (* -------------------------------------------------------------------- *) -let t_hoareF_conseq_conj pre post pre' post' tc = +let t_hoareF_conseq_conj pre post epost pre' post' epost' tc = let (_, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_hoareF tc in let pre'' = map_ss_inv2 f_and pre' pre in let post'' = map_ss_inv2 f_and post' post in - if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'') + let poste'' = conseq_conde_conj_ss epost' epost in + if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'') then tc_error !!tc "invalid pre-condition"; if not (ss_inv_alpha_eq hyps (hf_po hf) post'') then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF pre hf.hf_f post in - let concl2 = f_hoareF pre' hf.hf_f post' in + check_eq_poe tc hyps (hf_poe hf) poste''; + let concl1 = f_hoareF pre hf.hf_f post epost in + let concl2 = f_hoareF pre' hf.hf_f post' epost' in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] (* -------------------------------------------------------------------- *) @@ -695,8 +745,8 @@ let t_bdHoareS_conseq_conj ~add post post' tc = let posth = if add then post' else map_ss_inv2 f_and post' post in if not (ss_inv_alpha_eq hyps (bhs_po hs) postc) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post in - let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth + let concl1 = f_hoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post [] in + let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth hs.bhs_cmp (bhs_bd hs) in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] @@ -710,7 +760,7 @@ let t_bdHoareF_conseq_conj ~add post post' tc = let posth = if add then post' else map_ss_inv2 f_and post' post in if not (ss_inv_alpha_eq hyps (bhf_po hs) postc) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF (bhf_pr hs) hs.bhf_f post in + let concl1 = f_hoareF (bhf_pr hs) hs.bhf_f post [] in let concl2 = f_bdHoareF (bhf_pr hs) hs.bhf_f posth hs.bhf_cmp (bhf_bd hs) in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] @@ -727,8 +777,8 @@ let t_equivS_conseq_conj pre1 post1 pre2 post2 pre' post' tc = tc_error !!tc "invalid pre-condition"; if not (ts_inv_alpha_eq hyps (es_po es) (map_ts_inv f_ands [post';post1';post2'])) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareS mtl pre1 es.es_sl post1 in - let concl2 = f_hoareS mtr pre2 es.es_sr post2 in + let concl1 = f_hoareS mtl pre1 es.es_sl post1 [] in + let concl2 = f_hoareS mtr pre2 es.es_sr post2 [] in let concl3 = f_equivS mtl mtr pre' es.es_sl es.es_sr post' in FApi.xmutate1 tc `HlConseqConj [concl1; concl2; concl3] @@ -743,12 +793,12 @@ let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc = let post2' = ss_inv_generalize_left (ss_inv_rebind post2 mr) ml in let pre'' = map_ts_inv f_ands [pre'; pre1'; pre2'] in let post'' = map_ts_inv f_ands [post'; post1'; post2'] in - if not (ts_inv_alpha_eq hyps (ef_pr ef) pre'') + if not (ts_inv_alpha_eq hyps (ef_pr ef) pre'') then tc_error !!tc "invalid pre-condition"; if not (ts_inv_alpha_eq hyps (ef_po ef) post'') then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF pre1 ef.ef_fl post1 in - let concl2 = f_hoareF pre2 ef.ef_fr post2 in + let concl1 = f_hoareF pre1 ef.ef_fl post1 [] in + let concl2 = f_hoareF pre2 ef.ef_fr post2 [] in let concl3 = f_equivF pre' ef.ef_fl ef.ef_fr post' in FApi.xmutate1 tc `HlConseqConj [concl1; concl2; concl3] @@ -763,7 +813,7 @@ let t_equivS_conseq_bd side pr po tc = let pos = ss_inv_generalize_right (ss_inv_rebind po ml) mr in let prs = ss_inv_generalize_right (ss_inv_rebind pr ml) mr in es.es_ml, es.es_sl, es.es_sr, prs, pos - | `Right -> + | `Right -> let pos = ss_inv_generalize_left (ss_inv_rebind po mr) ml in let prs = ss_inv_generalize_left (ss_inv_rebind pr mr) ml in es.es_mr, es.es_sr, es.es_sl, prs, pos @@ -814,8 +864,9 @@ let transitivity_side_cond hyps prml poml pomr p q p2 q2 p1 q1 = let t_hoareF_conseq_equiv f2 p q p2 q2 tc = let env, hyps, _ = FApi.tc1_eflat tc in let hf1 = tc1_as_hoareF tc in + assert (hf_poe hf1 = []); let ef = f_equivF p hf1.hf_f f2 q in - let hf2 = f_hoareF p2 f2 q2 in + let hf2 = f_hoareF p2 f2 q2 [] in let (prml, _prmr), (poml, pomr) = Fun.equivF_memenv p.ml p.mr hf1.hf_f f2 env in let (cond1, cond2) = transitivity_side_cond hyps prml poml pomr p q p2 q2 (hf_pr hf1) (hf_po hf1) in @@ -897,7 +948,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* hoareS / hoareS / ⊥ / ⊥ *) | FhoareS _, Some ((_, {f_node = FhoareS hs}) as nf1), None, None -> let tac = if notmod then t_hoareS_conseq_nm else t_hoareS_conseq in - t_on1 2 (t_apply_r nf1) (tac (hs_pr hs) (hs_po hs) tc) + t_on1 2 (t_apply_r nf1) (tac (hs_pr hs) (hs_po hs) (hs_poe hs) tc) (* ------------------------------------------------------------------ *) (* hoareS / hoareS / hoareS / ⊥ *) @@ -909,11 +960,18 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = let hs2 = pf_as_hoareS !!tc f2 in let tac = if notmod then t_hoareS_conseq_nm else t_hoareS_conseq in + let epost = conseq_conde_conj_ss (hs_poe hs) (hs_poe hs2) in + t_on1seq 2 - (tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2)) - (map_ss_inv2 f_and (hs_po hs) (hs_po hs2))) + (tac + (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2)) + (map_ss_inv2 f_and (hs_po hs) (hs_po hs2)) + epost + ) (FApi.t_seqsub - (t_hoareS_conseq_conj (hs_pr hs2) (hs_po hs2) (hs_pr hs) (hs_po hs)) + (t_hoareS_conseq_conj + (hs_pr hs2) (hs_po hs2) (hs_poe hs2) + (hs_pr hs) (hs_po hs) (hs_poe hs)) [t_apply_r nf2; t_apply_r nf1]) tc @@ -935,7 +993,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* hoareF / hoareF / ⊥ / ⊥ *) | FhoareF _, Some ((_, {f_node = FhoareF hs}) as nf1), None, None -> let tac = if notmod then t_hoareF_conseq_nm else t_hoareF_conseq in - t_on1 2 (t_apply_r nf1) (tac (hf_pr hs) (hf_po hs) tc) + t_on1 2 (t_apply_r nf1) (tac (hf_pr hs) (hf_po hs) (hf_poe hs) tc) (* ------------------------------------------------------------------ *) (* hoareF / hoareF / hoareF / ⊥ *) @@ -946,20 +1004,26 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = -> let hs2 = pf_as_hoareF !!tc f2 in let tac = if notmod then t_hoareF_conseq_nm else t_hoareF_conseq in - let pr1, po1 = hf_pr hf, hf_po hf in + let pr1, po1, poe1 = hf_pr hf, hf_po hf, hf_poe hf in let pr2 = ss_inv_rebind (hf_pr hs2) hf.hf_m in let po2 = ss_inv_rebind (hf_po hs2) hf.hf_m in + let poe2 = List.map (fun (e,f) -> e,ss_inv_rebind f hf.hf_m) (hf_poe hs2) in + let epost = conseq_conde_conj_ss (hf_poe hf) poe2 in + (* check that the pre- and post-conditions are well formed *) t_on1seq 2 - ((tac (map_ss_inv2 f_and pr1 pr2) - (map_ss_inv2 f_and po1 po2))) + ((tac + (map_ss_inv2 f_and pr1 pr2) + (map_ss_inv2 f_and po1 po2) + epost + )) (FApi.t_seqsub - (t_hoareF_conseq_conj pr2 po2 pr1 po1) + (t_hoareF_conseq_conj pr2 po2 poe2 pr1 po1 poe1) [t_apply_r nf2; t_apply_r nf1]) tc (* ------------------------------------------------------------------ *) - (* hoareF / bdhoareF / ⊥ / ⊥ *) + (* hoareF / bdhoareF / ⊥ / ⊥ *) | FhoareF _, Some ((_, {f_node = FbdHoareF hs}) as nf1), None, None -> let tac = if notmod then t_bdHoareF_conseq_nm else t_bdHoareF_conseq in @@ -981,19 +1045,19 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = [t_id; t_id; t_apply_r nef; t_apply_r nf2] tc (* ------------------------------------------------------------------ *) - (* ehoareS / ehoareS / ⊥ / ⊥ *) + (* ehoareS / ehoareS / ⊥ / ⊥ *) | FeHoareS _, Some ((_, {f_node = FeHoareS hs}) as nf1), None, None -> let tac = if notmod then t_ehoareS_conseq_nm else t_ehoareS_conseq in FApi.t_last (t_apply_r nf1) (tac (ehs_pr hs) (ehs_po hs) tc) (* ------------------------------------------------------------------ *) - (* ehoareF / ehoareF / ⊥ / ⊥ *) + (* ehoareF / ehoareF / ⊥ / ⊥ *) | FeHoareF _, Some ((_, {f_node = FeHoareF hf}) as nf1), None, None -> let tac = if notmod then t_ehoareF_conseq_nm else t_ehoareF_conseq in FApi.t_last (t_apply_r nf1) (tac (ehf_pr hf) (ehf_po hf) tc) (* ------------------------------------------------------------------ *) - (* ehoareF / equivF / ehoareF *) + (* ehoareF / equivF / ehoareF *) | FeHoareF _, Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ -> let hf2 = pf_as_ehoareF !!tc f2 in @@ -1034,8 +1098,8 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = let tc = ( t_cut concl1 @+ [ t_id; (* subgoal 1 : pre *) t_intro_i hi @! - t_cut (f_hoareS (snd hs2.hs_m) pre hs2.hs_s (hs_po hs2)) @+ [ - t_hoareS_conseq (hs_pr hs2) (hs_po hs2) @+ + t_cut (f_hoareS (snd hs2.hs_m) pre hs2.hs_s (hs_po hs2) []) @+ [ + t_hoareS_conseq (hs_pr hs2) (hs_po hs2) [] @+ [ EcLowGoal.t_trivial; t_mytrivial; t_clear hi (* subgoal 2 : hs2 *)]; @@ -1043,7 +1107,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (t_bdHoareS_conseq_bd hs.bhs_cmp (bhs_bd hs) @+ [ t_id; (* subgoal 3 : bound *) t_bdHoareS_conseq_conj ~add:false (hs_po hs2) post1 @+ [ - t_hoareS_conseq pre (hs_po hs2) @+ [ + t_hoareS_conseq pre (hs_po hs2) [] @+ [ t_intros_i [m;h0] @! t_cutdef (ptlocal ~args:[pamemory m; palocal h0] hi) mpre @! EcLowGoal.t_trivial; @@ -1089,7 +1153,6 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = Some ((_, f2) as nf2), None -> - let hs2 = pf_as_hoareF !!tc f2 in let tac = if notmod then t_bdHoareF_conseq_nm else t_bdHoareF_conseq in let m,hi,hh, h0 = @@ -1107,8 +1170,8 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = let tc = ( t_cut concl1 @+ [ t_id; (* subgoal 1 : pre *) t_intro_i hi @! - t_cut (f_hoareF pre hs2.hf_f (hf_po hs2)) @+ [ - t_hoareF_conseq (hf_pr hs2) (hf_po hs2) @+ + t_cut (f_hoareF pre hs2.hf_f (hf_po hs2) []) @+ [ + t_hoareF_conseq (hf_pr hs2) (hf_po hs2) [] @+ [ EcLowGoal.t_trivial; t_mytrivial; t_clear hi (* subgoal 2 : hs2 *)]; @@ -1116,7 +1179,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (t_bdHoareF_conseq_bd hs.bhf_cmp (bhf_bd hs) @+ [ t_id; (* subgoal 3 : bound *) t_bdHoareF_conseq_conj ~add:false (hf_po hs2) post1 @+ [ - t_hoareF_conseq pre (hf_po hs2) @+ [ + t_hoareF_conseq pre (hf_po hs2) [] @+ [ t_intros_i [m;h0] @! t_cutdef (ptlocal ~args:[pamemory m; palocal h0] hi) mpre @! EcLowGoal.t_trivial; @@ -1151,7 +1214,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ -> let hf2 = pf_as_bdhoareF !!tc f2 in FApi.t_seqsub - (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef) + (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef) (bhf_pr hf2) (bhf_po hf2)) [t_id; t_id; t_apply_r nef; t_apply_r nf2] tc @@ -1214,14 +1277,14 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* equivS / ? / ? / ⊥ *) | FequivS es, Some _, Some _, None -> let m = EcIdent.create "&hr" in - let f3 = f_hoareS (snd es.es_mr) {m;inv=f_true} es.es_sr {m;inv=f_true} in + let f3 = f_hoareS (snd es.es_mr) {m;inv=f_true} es.es_sr {m;inv=f_true} [] in t_hi_conseq notmod f1 f2 (Some (None, f3)) tc (* ------------------------------------------------------------------ *) (* equivS / ? / ⊥ / ? *) | FequivS es, Some _, None, Some _ -> let m = EcIdent.create "&hr" in - let f2 = f_hoareS (snd es.es_ml) {m;inv=f_true} es.es_sl {m;inv=f_true} in + let f2 = f_hoareS (snd es.es_ml) {m;inv=f_true} es.es_sl {m;inv=f_true} [] in t_hi_conseq notmod f1 (Some (None, f2)) f3 tc (* ------------------------------------------------------------------ *) @@ -1295,14 +1358,14 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* equivF / ? / ? / ⊥ *) | FequivF ef, Some _, Some _, None -> let m = EcIdent.create "&hr" in - let f3 = f_hoareF {m;inv=f_true} ef.ef_fr {m;inv=f_true} in + let f3 = f_hoareF {m;inv=f_true} ef.ef_fr {m;inv=f_true} [] in t_hi_conseq notmod f1 f2 (Some (None, f3)) tc (* ------------------------------------------------------------------ *) (* equivF / ? / ⊥ / ? *) | FequivF ef, Some _, None, Some _ -> let m = EcIdent.create "&hr" in - let f2 = f_hoareF {m;inv=f_true} ef.ef_fl {m;inv=f_true} in + let f2 = f_hoareF {m;inv=f_true} ef.ef_fl {m;inv=f_true} [] in t_hi_conseq notmod f1 (Some (None, f2)) f3 tc | _ -> @@ -1334,38 +1397,15 @@ type processed_conseq_info = let process_info pe hyps m = function | CQI_bd (cmp, bd) -> PCI_bd (cmp, {m; inv=TTC.pf_process_form pe hyps treal bd}) -let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc = +let process_conseq_2 notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc = let hyps, concl = FApi.tc1_flat tc in let ensure_none o = if not (is_none o) then tc_error !!tc "cannot give a bound here" in - let process_cut1 ((pre, post), bd) = + let process_cut1 ((pre, post, poe), bd) = let penv, qenv, gpre, gpost, ty, fmake = match concl.f_node with - | FhoareS hs -> - let env = LDecl.push_active_ss hs.hs_m hyps in - - let fmake pre post c_or_bd = - match c_or_bd with - | None -> - f_hoareS(snd hs.hs_m) pre hs.hs_s post - | Some (PCI_bd (cmp, bd)) -> - f_bdHoareS (snd hs.hs_m) pre hs.hs_s post (oget cmp) bd - in (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), tbool, lift_ss_inv2 fmake) - - | FhoareF hf -> - let penv, qenv = LDecl.hoareF hf.hf_m hf.hf_f hyps in - - let fmake pre post c_or_bd = - match c_or_bd with - | None -> - f_hoareF pre hf.hf_f post - | Some (PCI_bd (cmp, bd)) -> - f_bdHoareF pre hf.hf_f post (oget cmp) bd - - in (penv, qenv, Inv_ss (hf_pr hf), Inv_ss (hf_po hf), tbool, lift_ss_inv2 fmake) - | FeHoareS hs -> let env = LDecl.push_active_ss hs.ehs_m hyps in let fmake pre post bd = @@ -1424,54 +1464,37 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | _ -> tc_error !!tc "conseq: not a phl/prhl judgement" in - let pre = pre |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in - let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in + match poe with + | Some _ -> assert false + | None -> + let pre = pre |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in + let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in + + let (pre, post, bd) = match gpre, gpost with + | Inv_ss gpre, Inv_ss gpost -> + let bd = bd |> omap (process_info !!tc penv gpre.m) in + (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, bd) + | Inv_ts gpre, Inv_ts gpost -> + ensure_none bd; + (Inv_ts {inv=pre;ml=gpre.ml;mr=gpost.mr}, + Inv_ts {inv=post;ml=gpost.ml;mr=gpost.mr}, + None) + | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" in - let (pre, post, bd) = match gpre, gpost with - | Inv_ss gpre, Inv_ss gpost -> - let bd = bd |> omap (process_info !!tc penv gpre.m) in - (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, bd) - | Inv_ts gpre, Inv_ts gpost -> - ensure_none bd; - (Inv_ts {inv=pre;ml=gpre.ml;mr=gpost.mr}, - Inv_ts {inv=post;ml=gpost.ml;mr=gpost.mr}, - None) - | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" in + fmake pre post bd - fmake pre post bd in - let process_cut2 side f1 ((pre, post), c_or_bd) = + let process_cut2 side f1 ((pre, post, poe), c_or_bd) = let penv, qenv, gpre, gpost, ty, fmake = match concl.f_node with - | FhoareS hs -> - let env = LDecl.push_active_ss hs.hs_m hyps in - let fmake pre post c_or_bd = - ensure_none c_or_bd; - f_hoareS (snd hs.hs_m) pre hs.hs_s post - in (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), tbool, lift_ss_inv2 fmake) - - | FhoareF hf -> - let m = hf.hf_m in - let f, pr, po = match f1 with - | None -> hf.hf_f, hf_pr hf, hf_po hf - | Some f1 -> match (snd f1).f_node with - | FequivF ef when side = `Left -> - ef.ef_fr, {m; inv=f_true}, {m; inv=f_true} - | _ -> hf.hf_f, hf_pr hf, hf_po hf - in - let penv, qenv = LDecl.hoareF m f hyps in - let fmake pre post c_or_bd = - ensure_none c_or_bd; f_hoareF pre f post in - (penv, qenv, Inv_ss pr, Inv_ss po, tbool, lift_ss_inv2 fmake) - | FeHoareF hf -> let f, pr, po, m = match f1 with | None -> hf.ehf_f, ehf_pr hf, ehf_po hf, hf.ehf_m | Some f1 -> match (snd f1).f_node with | FequivF ef when side = `Left -> let f_xreal_1 = f_r2xr f_r1 in - ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1}, + ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1}, {m=ef.ef_mr; inv=f_xreal_1}, ef.ef_mr | _ -> hf.ehf_f, ehf_pr hf, ehf_po hf, hf.ehf_m in @@ -1484,20 +1507,20 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) let env = LDecl.push_active_ss bhs.bhs_m hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; - f_hoareS (snd bhs.bhs_m) pre bhs.bhs_s post + f_hoareS (snd bhs.bhs_m) pre bhs.bhs_s post [] in (env, env, Inv_ss (bhs_pr bhs), Inv_ss (bhs_po bhs), tbool, lift_ss_inv2 fmake) | FbdHoareF bhf -> let f, pr, po, m = match f1 with | None -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m | Some f1 -> match (snd f1).f_node with - | FequivF ef when side = `Left -> ef.ef_fr, + | FequivF ef when side = `Left -> ef.ef_fr, {m=ef.ef_mr;inv=f_true}, {m=ef.ef_mr;inv=f_true}, ef.ef_mr | _ -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m in let penv, qenv = LDecl.hoareF m f hyps in let fmake pre post c_or_bd = - ensure_none c_or_bd; f_hoareF pre f post in + ensure_none c_or_bd; f_hoareF pre f post [] in (penv, qenv, Inv_ss pr, Inv_ss po, tbool, lift_ss_inv2 fmake) | FequivF ef -> @@ -1506,7 +1529,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) let penv, qenv = LDecl.hoareF m f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; - f_hoareF pre f post in + f_hoareF pre f post [] in let f_true = {m; inv=f_true} in (penv, qenv, Inv_ss f_true, Inv_ss f_true, tbool, lift_ss_inv2 fmake) @@ -1526,7 +1549,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) f_bdHoareS (snd m) pre f post cmp bd | _, None -> - f_hoareS (snd m) pre f post + f_hoareS (snd m) pre f post [] | _, Some (PCI_bd (cmp,bd)) -> let cmp = odfl FHeq cmp in @@ -1537,21 +1560,197 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | _ -> tc_error !!tc "conseq: not a phl/prhl judgement" in + match poe with + | Some _ -> assert false + | None -> + let pre = pre |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in + let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in + + let (pre, post, c_or_bd) = match gpre, gpost with + | Inv_ss gpre, Inv_ss gpost -> + let bd = c_or_bd |> omap (process_info !!tc penv gpre.m) in + (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, bd) + | Inv_ts gpre, Inv_ts gpost -> + ensure_none c_or_bd; + (Inv_ts {inv=pre;ml=gpre.ml;mr=gpost.mr}, + Inv_ts {inv=post;ml=gpost.ml;mr=gpost.mr}, + None) + | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" + in + fmake pre post c_or_bd + in + + if List.for_all is_none [info1; info2; info3] + then t_id tc + else + let f1 = info1 |> omap (PT.tc1_process_full_closed_pterm_cut + ~prcut:(process_cut1) tc) in + let f2 = info2 |> omap (PT.tc1_process_full_closed_pterm_cut + ~prcut:(process_cut2 `Left f1) tc) in + let f3 = info3 |> omap (PT.tc1_process_full_closed_pterm_cut + ~prcut:(process_cut2 `Right f1) tc) in + + let ofalse = omap (fun (x, y) -> (Some x, y)) in + + t_hi_conseq notmod (f1 |> ofalse) (f2 |> ofalse) (f3 |> ofalse) tc + +let process_conseq_1 notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc = + let hyps, concl = FApi.tc1_flat tc in + + let env = LDecl.toenv hyps in + + let ensure_none o = + if not (is_none o) then tc_error !!tc "cannot give a bound here" in + + let process_conseq_e tc penv ty = + let aux (e,f) = + let _,e = EcTyping.except_genpath env e in + let f = TTC.pf_process_form !!tc penv ty f in + e,f + in + List.map aux + in + + let process_cut1 ((pre, post, poe), c_or_bd) = + let penv, qenv, gpre, gpost, gpoe, ty, fmake = + match concl.f_node with + | FhoareS hs -> + let env = LDecl.push_active_ss hs.hs_m hyps in + + let fmake pre post poe c_or_bd = + match c_or_bd with + | None -> + f_hoareS(snd hs.hs_m) pre hs.hs_s post poe + | Some (PCI_bd (cmp, bd)) -> + f_bdHoareS (snd hs.hs_m) pre hs.hs_s post (oget cmp) bd + in + (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), (hs_poe hs), tbool, lift_ss_inv2 fmake) + + | FhoareF hf -> + let penv, qenv = LDecl.hoareF hf.hf_m hf.hf_f hyps in + + let fmake pre post poe c_or_bd = + match c_or_bd with + | None -> + f_hoareF pre hf.hf_f post poe + | Some (PCI_bd (cmp, bd)) -> + f_bdHoareF pre hf.hf_f post (oget cmp) bd + in + (penv, qenv, Inv_ss (hf_pr hf), Inv_ss (hf_po hf), (hf_poe hf), tbool, lift_ss_inv2 fmake) + + | _ -> tc_error !!tc "conseq: not a phl/prhl judgement" + in + let pre = pre |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in - let (pre, post, c_or_bd) = match gpre, gpost with - | Inv_ss gpre, Inv_ss gpost -> + let poe = omap (process_conseq_e tc penv ty) poe in + let poe = match poe with + None -> gpoe + | Some poe -> + begin + if not (EcTyping.check_unique_epost poe) then assert false; + List.map + (fun (e,f) -> e,{inv=f;m=(find_poe gpoe e).m}) + poe + end + in + + let (pre, post, poe, c_or_bd) = match gpre, gpost with + | Inv_ss gpre, Inv_ss gpost -> let bd = c_or_bd |> omap (process_info !!tc penv gpre.m) in - (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, bd) - | Inv_ts gpre, Inv_ts gpost -> + (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, poe, bd) + | Inv_ts gpre, Inv_ts gpost -> ensure_none c_or_bd; (Inv_ts {inv=pre;ml=gpre.ml;mr=gpost.mr}, Inv_ts {inv=post;ml=gpost.ml;mr=gpost.mr}, + poe, None) - | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" in + | _ -> + tc_error + !!tc + "conseq: pre, post and exception post must be of the same kind" + in + fmake pre post poe c_or_bd + + in + + let process_cut2 side f1 ((pre, post, poe), c_or_bd) = + let penv, qenv, gpre, gpost, gpoe, ty, fmake = + match concl.f_node with + (* | FhoareS hs -> *) + (* let env = LDecl.push_active hs.hs_m hyps in *) + (* let fmake pre post poe c_or_bd = *) + (* ensure_none c_or_bd; *) + (* f_hoareS_r { hs with hs_pr = pre; hs_po = post; hs_poe = poe } *) + (* in (env, env, hs.hs_pr, hs.hs_po, hs.hs_poe, tbool, fmake) *) + + (* | FhoareF hf -> *) + (* let f, pr, po, poe = match f1 with *) + (* | None -> hf.hf_f, hf.hf_pr, hf.hf_po, hf.hf_poe *) + (* | Some f1 -> match (snd f1).f_node with *) + (* | FequivF ef when side = `Left -> ef.ef_fr, f_true, f_true, [] *) + (* | _ -> hf.hf_f, hf.hf_pr, hf.hf_po, hf.hf_poe *) + (* in *) + (* let penv, qenv = LDecl.hoareF f hyps in *) + (* let fmake pre post poe c_or_bd = *) + (* ensure_none c_or_bd; f_hoareF pre f post poe in *) + (* (penv, qenv, pr, po, poe, tbool, fmake) *) + | FhoareS hs -> + let env = LDecl.push_active_ss hs.hs_m hyps in + let fmake pre post poe c_or_bd = + ensure_none c_or_bd; + f_hoareS (snd hs.hs_m) pre hs.hs_s post poe + in + (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), (hs_poe hs), tbool, lift_ss_inv2 fmake) + + | FhoareF hf -> + let m = hf.hf_m in + let f, pr, po, poe = match f1 with + | None -> hf.hf_f, hf_pr hf, hf_po hf, hf_poe hf + | Some f1 -> + match (snd f1).f_node with + | FequivF ef when side = `Left -> + ef.ef_fr, {m; inv=f_true}, {m; inv=f_true}, [] + | _ -> hf.hf_f, hf_pr hf, hf_po hf, hf_poe hf + in + let penv, qenv = LDecl.hoareF m f hyps in + let fmake pre post poe c_or_bd = + ensure_none c_or_bd; f_hoareF pre f post poe + in + (penv, qenv, Inv_ss pr, Inv_ss po, poe, tbool, lift_ss_inv2 fmake) - fmake pre post c_or_bd + | _ -> tc_error !!tc "conseq: not a phl/prhl judgement" + in + + let pre = pre |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in + let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in + + let poe = omap (process_conseq_e tc penv ty) poe in + let poe = match poe with + None -> gpoe + | Some poe -> + begin + if not (EcTyping.check_unique_epost poe) then assert false; + List.map + (fun (e,f) -> e,{inv=f;m=(find_poe gpoe e).m}) + poe + end + in + + let (pre, post, poe, c_or_bd) = match gpre, gpost with + | Inv_ss gpre, Inv_ss gpost -> + let bd = c_or_bd |> omap (process_info !!tc penv gpre.m) in + (Inv_ss {inv=pre;m=gpre.m}, Inv_ss {inv=post;m=gpost.m}, poe, bd) + | Inv_ts gpre, Inv_ts gpost -> + ensure_none c_or_bd; + (Inv_ts {inv=pre;ml=gpre.ml;mr=gpost.mr}, + Inv_ts {inv=post;ml=gpost.ml;mr=gpost.mr}, + poe, + None) + | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" + in + fmake pre post poe c_or_bd in @@ -1569,9 +1768,16 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) t_hi_conseq notmod (f1 |> ofalse) (f2 |> ofalse) (f3 |> ofalse) tc +let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc = + let _, concl = FApi.tc1_flat tc in + + match concl.f_node with + | FhoareS _ | FhoareF _ -> process_conseq_1 notmod (info1, info2, info3) tc + | _ -> process_conseq_2 notmod (info1, info2, info3) tc + (* -------------------------------------------------------------------- *) let process_bd_equiv side (pr, po) tc = - let info = FPCut ((Some pr, Some po), None) in + let info = FPCut ((Some pr, Some po, None), None) in let info = Some { fp_mode = `Implicit; fp_head = info; fp_args = []; } in let info2, info3 = sideif side (info, None) (None, info) in process_conseq true (None, info2, info3) tc @@ -1601,6 +1807,9 @@ let process_conseq_opt cqopt infos tc = let t_conseqauto ?(delta = true) ?tsolve tc = let (hyps, concl), mk_other = FApi.tc1_flat tc, true in + let t_hoareF_notmod f = t_hoareF_notmod f [] in + let t_hoareS_notmod f = t_hoareS_notmod f [] in + let todo = match concl.f_node with | FhoareF hf -> Some (lift_ss_inv t_hoareF_notmod, cond_hoareF_notmod ~mk_other tc (hf_po hf)) diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli index 18c2c22e47..49425a7fee 100644 --- a/src/phl/ecPhlConseq.mli +++ b/src/phl/ecPhlConseq.mli @@ -11,8 +11,10 @@ open EcAst val t_equivF_conseq : ts_inv -> ts_inv -> FApi.backward val t_equivS_conseq : ts_inv -> ts_inv -> FApi.backward val t_eagerF_conseq : ts_inv -> ts_inv -> FApi.backward -val t_hoareF_conseq : ss_inv -> ss_inv -> FApi.backward -val t_hoareS_conseq : ss_inv -> ss_inv -> FApi.backward +val t_hoareF_conseq : + ss_inv -> ss_inv -> (EcPath.path * ss_inv) list -> FApi.backward +val t_hoareS_conseq : + ss_inv -> ss_inv -> (EcPath.path * ss_inv) list -> FApi.backward val t_bdHoareF_conseq : ss_inv -> ss_inv -> FApi.backward val t_bdHoareS_conseq : ss_inv -> ss_inv -> FApi.backward @@ -24,8 +26,10 @@ val t_bdHoareF_conseq_bd : hoarecmp -> ss_inv -> FApi.backward (* -------------------------------------------------------------------- *) val t_equivF_conseq_nm : ts_inv -> ts_inv -> FApi.backward val t_equivS_conseq_nm : ts_inv -> ts_inv -> FApi.backward -val t_hoareF_conseq_nm : ss_inv -> ss_inv -> FApi.backward -val t_hoareS_conseq_nm : ss_inv -> ss_inv -> FApi.backward +val t_hoareF_conseq_nm : + ss_inv -> ss_inv -> (EcPath.path * ss_inv) list -> FApi.backward +val t_hoareS_conseq_nm : + ss_inv -> ss_inv -> (EcPath.path * ss_inv) list -> FApi.backward val t_bdHoareF_conseq_nm : ss_inv -> ss_inv -> FApi.backward val t_bdHoareS_conseq_nm : ss_inv -> ss_inv -> FApi.backward (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlCoreView.ml b/src/phl/ecPhlCoreView.ml index 5ae5735177..da4623e54d 100644 --- a/src/phl/ecPhlCoreView.ml +++ b/src/phl/ecPhlCoreView.ml @@ -10,7 +10,7 @@ let t_hoare_of_bdhoareS_r tc = let bhs = tc1_as_bdhoareS tc in if not (bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0) then tc_error !!tc "%s" "bound must be equal to 0%r"; - let concl = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s (map_ss_inv1 f_not (bhs_po bhs)) in + let concl = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s (map_ss_inv1 f_not (bhs_po bhs)) [] in FApi.xmutate1 tc `ViewBdHoare [concl] (* -------------------------------------------------------------------- *) @@ -19,7 +19,7 @@ let t_hoare_of_bdhoareF_r tc = if not (bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0) then tc_error !!tc "%s" "bound must be equal to 0%r"; let post = map_ss_inv1 f_not (bhf_po bhf) in - let concl = f_hoareF (bhf_pr bhf) bhf.bhf_f post in + let concl = f_hoareF (bhf_pr bhf) bhf.bhf_f post [] in FApi.xmutate1 tc `ViewBdHoare [concl] (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index a99092c829..795563fce2 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -140,10 +140,10 @@ let t_eager_if_r tc = let fe = ss_inv_generalize_right (ss_inv_of_expr ml e) mr in let eqb = map_ts_inv2 f_eq fe {ml;mr;inv=f_local b tbool} in - EcSubst.f_forall_mems_ss_inv es.es_mr + EcSubst.f_forall_mems_ss_inv es.es_mr (map_ss_inv1 (f_forall [(b, GTty tbool)]) - (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd es.es_ml) pr s po) (map_ts_inv2 f_and (es_pr es) eqb) eqb)) in + (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd es.es_ml) pr s po []) (map_ts_inv2 f_and (es_pr es) eqb) eqb)) in let cT = let pre = map_ts_inv2 f_and (es_pr es) (map_ts_inv2 f_eq fel {ml;mr;inv=f_true}) in @@ -196,7 +196,7 @@ let t_eager_while_r h tc = and bT = f_equivS (snd eC.es_ml) (snd eC.es_mr) (map_ts_inv2 f_and_simpl eqI e1) (stmt (s.s_node@c.s_node)) (stmt (c'.s_node@s'.s_node)) eqI - + and cT = f_equivS (snd eC.es_mr) (snd eC.es_mr) eqI2 c' c' eqI2 in @@ -467,13 +467,17 @@ let eager pf env s s' inv eqIs eqXs c c' eqO = (* (h) is assumed *) (fhyps, eqi) - | Sassert el, Sassert er -> - check_args [el]; + | Sraise (_,argsl), Sraise (_,argsr) -> + check_args argsl; let eqnm = Mpv2.split_nmod env modi modi' eqo in let eqm = Mpv2.split_mod env modi modi' eqo in if not (Mpv2.subset eqm eqXs) then raise EqObsInError; - let eqi = Mpv2.union eqIs eqnm in - (fhyps, Mpv2.add_eqs env el er eqi) + let eqi = + List.fold_left2 + (fun eqs e1 e2 -> Mpv2.add_eqs env e1 e2 eqs) + eqnm argsl argsr + in + (fhyps,eqi) | Sabstract _, Sabstract _ -> assert false (* FIXME *) @@ -605,7 +609,7 @@ let process_fun_abs info eqI tc = let process_call info tc = let process_cut info = match info with - | EcParsetree.CI_spec (fpre, fpost) -> + | EcParsetree.CI_spec (fpre, fpost, []) -> let env, hyps, _ = FApi.tc1_eflat tc in let es = tc1_as_equivS tc in diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index 6fc4497fda..84e367fa94 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -277,7 +277,25 @@ and i_eqobs_in il ir sim local (eqo:Mpv2.t) = let eqs = List.fold_left2 doit Mpv2.empty bsl bsr in !rsim, add_eqs !rsim local eqs el er - | Sassert el, Sassert er -> sim, add_eqs sim local eqo el er + | Sraise (_,argsl), Sraise (_,argsr) -> + let argsl, argsr = + match argsl, argsr with + | _, _ when List.length argsl = List.length argsr -> argsl, argsr + | [al], _ -> begin + match al.e_node with + | Etuple argsl -> argsl, argsr + | _ -> raise EqObsInError + end + | _, [ar] -> begin + match ar.e_node with + | Etuple argsr -> argsl, argsr + | _ -> raise EqObsInError + end + | _ -> raise EqObsInError + in + let eqi = List.fold_left2 (add_eqs sim local) eqo argsl argsr in + sim, eqi + | _, _ -> raise EqObsInError and s_eqobs_in_full sl sr sim local eqo = diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index b0f5b508f9..f25797be37 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -20,14 +20,14 @@ let get_to_gens fs = let id = match f with | Inv_ss f -> begin match f.inv.f_node with - | Fpvar (pv, m) -> + | Fpvar (pv, m) -> id_of_pv pv m - | _ -> EcIdent.create "f" + | _ -> EcIdent.create "f" end | Inv_ts f -> begin match f.inv.f_node with - | Fpvar (pv, m) -> + | Fpvar (pv, m) -> id_of_pv ~mc:(f.ml, f.mr) pv m - | _ -> EcIdent.create "f" + | _ -> EcIdent.create "f" end in id, f in List.map do_id fs @@ -58,7 +58,7 @@ let t_hr_exists_intro_r fs tc = let pre = if is_ehoare then map_inv2 f_interp_ehoare_form (map_inv1 (f_exists bd) (map_inv f_ands eqs)) pre1 - else + else map_inv1 (f_exists bd) (map_inv2 f_and (map_inv f_ands eqs) pre1) in let h = LDecl.fresh_id hyps "h" in @@ -105,15 +105,15 @@ let process_exists_intro ~(elim : bool) fs tc = let (hyps, concl) = FApi.tc1_flat tc in let penv, f_tr = match concl.f_node with - | FhoareF {hf_f=f;hf_m=m} | FeHoareF {ehf_f=f; ehf_m=m} - | FbdHoareF {bhf_f=f; bhf_m=m} -> + | FhoareF {hf_f=f;hf_m=m} | FeHoareF {ehf_f=f; ehf_m=m} + | FbdHoareF {bhf_f=f; bhf_m=m} -> fst (LDecl.hoareF m f hyps), Inv_ss {m; inv = f_true} | FhoareS {hs_m=(m,_) as me} | FeHoareS {ehs_m=(m,_) as me} - | FbdHoareS {bhs_m=(m,_) as me} -> + | FbdHoareS {bhs_m=(m,_) as me} -> LDecl.push_active_ss me hyps, Inv_ss {m; inv = f_true} - | FequivF ef -> fst (LDecl.equivF ef.ef_ml ef.ef_mr ef.ef_fl ef.ef_fr hyps), + | FequivF ef -> fst (LDecl.equivF ef.ef_ml ef.ef_mr ef.ef_fl ef.ef_fr hyps), Inv_ts {ml=ef.ef_ml; mr=ef.ef_mr; inv=f_true} - | FequivS es -> LDecl.push_all [es.es_ml; es.es_mr] hyps, + | FequivS es -> LDecl.push_all [es.es_ml; es.es_mr] hyps, Inv_ts {ml=(fst es.es_ml); mr=(fst es.es_mr); inv=f_true} | _ -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc in diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 8d4e44c347..c5e6585814 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -103,7 +103,7 @@ and callable_oracles_i env modv os i = | Smatch (_, b) -> callable_oracles_sx env modv os (List.map snd b) | Sif (_, s1, s2) -> callable_oracles_sx env modv os [s1; s2] - | Sasgn _ | Srnd _ | Sassert _ -> os + | Sasgn _ | Srnd _ | Sraise _ -> os | Sabstract _ -> assert false (* FIXME *) @@ -189,7 +189,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let p = map_ss_inv2 f_and (map_ss_inv1 f_not f_event) (map_ss_inv2 f_eq cntr {m=cntr.m;inv=f_i0}) in let p = map_ss_inv2 f_and_simpl p inv in let p = EcSubst.ss_inv_rebind p pre.m in - f_hoareS (snd memenv) pre (stmt s_hd) p + f_hoareS (snd memenv) pre (stmt s_hd) p [] in let oracle_goal o = @@ -220,7 +220,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let pre = map_ss_inv2 f_and_simpl pre inv in let post = map_ss_inv2 f_int_lt old_cntr cntr in let post = map_ss_inv2 f_and_simpl post inv in - f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF pre o post) + f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF pre o post []) in let cntr_stable_goal = let old_cntr = {m=cntr.m;inv=old_cntr} in @@ -234,7 +234,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let post = map_ss_inv2 f_and_simpl post inv in f_forall_simpl [old_b_id,GTty tbool; old_cntr_id,GTty tint] - (f_hoareF pre o post) + (f_hoareF pre o post []) in [not_F_to_F_goal;cntr_decr_goal;cntr_stable_goal] in diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 004e191cea..55ee4ff75f 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -81,7 +81,16 @@ let t_hoareF_fun_def_r tc = let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (hf_po hf) in let pre = map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) (hf_pr hf) in - let concl' = f_hoareS (snd memenv) pre fdef.f_body post in + let epost = + List.map + (fun (e,f) -> + let f = + map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) f + in + e,f) + (hf_poe hf) + in + let concl' = f_hoareS (snd memenv) pre fdef.f_body post epost in FApi.xmutate1 tc `FunDef [concl'] (* ------------------------------------------------------------------ *) @@ -160,7 +169,7 @@ module FunAbsLow = struct let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in let fv = PV.fv env inv.m inv.inv in PV.check_depend env fv top; - let ospec o = f_hoareF inv o inv in + let ospec o = f_hoareF inv o inv [] in let sg = List.map ospec (OI.allowed oi) in (inv, inv, sg) @@ -248,7 +257,7 @@ let t_hoareF_abs_r inv tc = let pre, post, sg = FunAbsLow.hoareF_abs_spec !!tc env hf.hf_f inv in let tactic tc = FApi.xmutate1 tc `FunAbs sg in - FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre post tc) + FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre post (hf_poe hf) tc) let t_ehoareF_abs_r inv tc = let env = FApi.tc1_env tc in @@ -426,7 +435,7 @@ let t_fun_to_code_hoare_r tc = let spo = ToCodeLow.add_var env pv_res m r m PVM.empty in let pre = PVM.subst env spr (hf_pr hf).inv in let post = PVM.subst env spo (hf_po hf).inv in - let concl = f_hoareS mt {m;inv=pre} st {m;inv=post} in + let concl = f_hoareS mt {m;inv=pre} st {m;inv=post} (hf_poe hf) in FApi.xmutate1 tc `FunToCode [concl] (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index bdf1a7ef64..3e668c099b 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -50,7 +50,7 @@ module LowSubst = struct | Sif (c, s1, s2) -> i_if (esubst c, ssubst s1, ssubst s2) | Swhile (e, stmt) -> i_while (esubst e, ssubst stmt) | Smatch (e, bs) -> i_match (esubst e, List.Smart.map (snd_map ssubst) bs) - | Sassert e -> i_assert (esubst e) + | Sraise (e,es) -> i_raise (e, List.map esubst es) | Sabstract _ -> i and issubst m (is : instr list) = @@ -171,7 +171,7 @@ end let t_inline_hoare_r ~use_tuple sp tc = let hs = tc1_as_hoareS tc in let (_,mt), stmt = LowInternal.inline ~use_tuple tc hs.hs_m sp hs.hs_s in - let concl = f_hoareS mt (hs_pr hs) stmt (hs_po hs) in + let concl = f_hoareS mt (hs_pr hs) stmt (hs_po hs) (hs_poe hs) in FApi.xmutate1 tc `Inline [concl] diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index bef1209842..1ba8a4ab90 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -67,7 +67,7 @@ let check_dslc pf = | Smatch (_, bs) -> List.iter (doit_s |- snd) bs - | Srnd _ | Scall _ | Swhile _ | Sassert _ | Sabstract _ -> + | Srnd _ | Scall _ | Swhile _ | Sraise _ | Sabstract _ -> error () and doit_s c = @@ -305,9 +305,13 @@ let process_unroll_for side cpos tc = let t_conseq_nm tc = match (tc1_get_pre tc) with - | Inv_ss inv -> - (EcPhlConseq.t_hoareS_conseq_nm inv {m=inv.m;inv=f_true} @+ - [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc + | Inv_ss inv -> + (EcPhlConseq.t_hoareS_conseq_nm + inv + {m=inv.m;inv=f_true} + (tc1_get_poste tc) + @+ + [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc | _ -> tc_error !!tc "expecting single sided precondition" in let doi i tc = @@ -339,4 +343,4 @@ let process_unroll (side, cpos, for_) tc = else begin let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in t_unroll side cpos tc - end \ No newline at end of file + end diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml index 20bd429ad6..ed02a5672d 100644 --- a/src/phl/ecPhlRCond.ml +++ b/src/phl/ecPhlRCond.ml @@ -37,8 +37,8 @@ module Low = struct let hs = tc1_as_hoareS tc in let m = EcMemory.memory hs.hs_m in let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.hs_s in - let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd e in - let concl2 = f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) in + let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd e (hs_poe hs) in + let concl2 = f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) (hs_poe hs) in FApi.xmutate1 tc `RCond [concl1; concl2] (* ------------------------------------------------------------------ *) @@ -53,7 +53,7 @@ module Low = struct | _ -> tc_error !!tc "the pre should have the form \"_ `|` _\"" in let pre = map_ss_inv1 pre (ehs_pr hs) in - let concl1 = f_hoareS (snd hs.ehs_m) pre hd e in + let concl1 = f_hoareS (snd hs.ehs_m) pre hd e [] in let concl2 = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs) in FApi.xmutate1 tc `RCond [concl1; concl2] @@ -63,7 +63,7 @@ module Low = struct let bhs = tc1_as_bdhoareS tc in let m = EcMemory.memory bhs.bhs_m in let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos bhs.bhs_s in - let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd e in + let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd e [] in let concl2 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in FApi.xmutate1 tc `RCond [concl1; concl2] @@ -79,13 +79,13 @@ module Low = struct let ss_inv_generalize_other = sideif side ss_inv_generalize_right ss_inv_generalize_left in let hd,_,e,s = gen_rcond (!!tc, env) b (fst m) at_pos s in let e = ss_inv_generalize_other e (fst mo) in - let concl1 = + let concl1 = EcSubst.f_forall_mems_ss_inv (EcIdent.create "&m", snd mo) (ts_inv_lower_side2 (fun pr po -> let mhs = EcIdent.create "&hr" in let pr = ss_inv_rebind pr mhs in let po = ss_inv_rebind po mhs in - f_hoareS (snd m) pr hd po) (es_pr es) e) in + f_hoareS (snd m) pr hd po []) (es_pr es) e) in let sl,sr = match side with `Left -> s, es.es_sr | `Right -> es.es_sl, s in let concl2 = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr (es_po es) in FApi.xmutate1 tc `RCond [concl1; concl2] @@ -222,8 +222,8 @@ module LowMatch = struct let pr = ofold (map_ss_inv2 f_and) (hs_pr hs) epr in - let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd po1 in - let concl2 = f_hoareS (snd me) pr full (hs_po hs) in + let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd po1 (hs_poe hs) in + let concl2 = f_hoareS (snd me) pr full (hs_po hs) (hs_poe hs) in FApi.xmutate1 tc `RCondMatch [concl1; concl2] @@ -248,7 +248,7 @@ module LowMatch = struct let pr = ofold (map_ss_inv2 f_and) (bhs_pr bhs) epr in - let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd po1 in + let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd po1 [] in let concl2 = f_bdHoareS (snd me) pr full (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in FApi.xmutate1 tc `RCondMatch [concl1; concl2] @@ -266,18 +266,18 @@ module LowMatch = struct let (epr, hd, po1), (me, full) = gen_rcond_full (!!tc, FApi.tc1_env tc) c m at_pos s in - let ss_inv_generalize_other inv = sideif side + let ss_inv_generalize_other inv = sideif side (ss_inv_generalize_right inv mr) (ss_inv_generalize_left inv ml) in let epr = omap (fun epr -> ss_inv_generalize_other (ss_inv_rebind epr (fst m))) epr in - + let ts_inv_lower_side1 = sideif side ts_inv_lower_left1 ts_inv_lower_right1 in let concl1 = f_forall_mems_ss_inv mo - (ts_inv_lower_side1 (fun pr -> f_hoareS (snd m) pr hd po1) (es_pr es)) in + (ts_inv_lower_side1 (fun pr -> f_hoareS (snd m) pr hd po1 []) (es_pr es)) in let (ml, mr), (sl, sr) = match side with diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 5ed923c2b3..bfa73fb990 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -37,7 +37,7 @@ module Core = struct let post = subst_form_lv env lv x (hs_po hs) in let post = map_ss_inv2 f_imp (map_ss_inv2 f_in_supp x distr) post in let post = map_ss_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in - let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in + let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post (hs_poe hs) in FApi.xmutate1 tc `Rnd [concl] (* -------------------------------------------------------------------- *) @@ -51,7 +51,7 @@ module Core = struct let m = fst hs.ehs_m in let distr = EcFol.ss_inv_of_expr m distr in let post = subst_form_lv env lv {m;inv=x} (ehs_po hs) in - let post = map_ss_inv2 (f_Ep ty_distr) distr + let post = map_ss_inv2 (f_Ep ty_distr) distr (map_ss_inv1 (f_lambda [(x_id,GTty ty_distr)]) post) in let concl = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s post in FApi.xmutate1 tc `Rnd [concl] @@ -211,7 +211,7 @@ module Core = struct | PNoRndParams, FHle -> if is_post_indep then (* event is true *) - let concl = f_bdHoareS (snd bhs.bhs_m) + let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in [concl] else @@ -219,7 +219,7 @@ module Core = struct let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let concl = f_hoareS (snd bhs.bhs_m) pre s post in + let concl = f_hoareS (snd bhs.bhs_m) pre s post [] in let concl = f_forall_simpl binders concl in [concl] | PNoRndParams, _ -> @@ -244,7 +244,7 @@ module Core = struct let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let concl = f_hoareS (snd bhs.bhs_m) pre s post in + let concl = f_hoareS (snd bhs.bhs_m) pre s post [] in let concl = f_forall_simpl binders concl in [concl] | PSingleRndParam event, _ -> @@ -273,7 +273,7 @@ module Core = struct let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in f_forall_mems_ss_inv bhs.bhs_m (map_ss_inv2 f_imp (map_ss_inv1 f_not phi) post) in let sgoal5 = - let f_inbound x = + let f_inbound x = let f_r1, f_r0 = {m;inv=f_r1}, {m;inv=f_r0} in map_ss_inv2 f_anda (map_ss_inv2 f_real_le f_r0 x) (map_ss_inv2 f_real_le x f_r1) in map_ss_inv f_ands (List.map f_inbound [d1; d2; d3; d4]) @@ -405,7 +405,9 @@ module Core = struct Some (PV.fv (FApi.tc1_env tc) (fst hs.hs_m) (hs_po hs).inv) else None in let (_, mt), s2 = semrnd tc hs.hs_m fv s2 in - let concl = f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs) in + let concl = + f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs) (hs_poe hs) + in FApi.xmutate1 tc (`RndSem pos) [concl] (* -------------------------------------------------------------------- *) @@ -525,11 +527,11 @@ let wp_equiv_rnd_r bij tc = let po = match hdc2, hdc3 with | None , None -> None - | Some _, Some _ -> + | Some _, Some _ -> Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4))) - | Some _, None -> + | Some _, None -> Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind (map_ts_inv2 f_anda c3 c4)))) - | None , Some _ -> + | None , Some _ -> Some (map_ts_inv f_andas [c1; c2; map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4)]) in @@ -690,7 +692,7 @@ let process_rnd side pos tac_info tc = Double ((b1, p1), (b2, p2)) ) in - + t_equiv_rnd side ?pos bij_info tc | _ -> tc_error !!tc "invalid arguments" diff --git a/src/phl/ecPhlRwPrgm.ml b/src/phl/ecPhlRwPrgm.ml index c249539240..05bbff64df 100644 --- a/src/phl/ecPhlRwPrgm.ml +++ b/src/phl/ecPhlRwPrgm.ml @@ -23,10 +23,10 @@ let process_idassign ((cpos, pv) : idassign_t) (tc : tcenv1) = let s = Zpr.zipper_of_cpos env cpos hs.hs_s in let s = { s with z_tail = sasgn :: s.z_tail } in { hs with hs_s = Zpr.zip s } in - FApi.xmutate1 tc `IdAssign [EcFol.f_hoareS (snd hs.hs_m) (hs_pr hs) (hs.hs_s) (hs_po hs)] + FApi.xmutate1 tc `IdAssign [EcFol.f_hoareS (snd hs.hs_m) (hs_pr hs) (hs.hs_s) (hs_po hs) []] (* -------------------------------------------------------------------- *) let process_rw_prgm (mode : rwprgm) (tc : tcenv1) = - match mode with + match mode with | `IdAssign (cpos, pv) -> process_idassign (cpos, pv) tc diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index ec3b2eb361..ee1a7d9537 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -246,7 +246,14 @@ let t_sp_side pos tc = let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 (hs_pr hs).inv in check_sp_progress pos stmt1; let m = fst hs.hs_m in - let subgoal = f_hoareS (snd hs.hs_m) {m;inv=hs_pr} (stmt (stmt1@stmt2)) (hs_po hs) in + let subgoal = + f_hoareS + (snd hs.hs_m) + {m;inv=hs_pr} + (stmt (stmt1@stmt2)) + (hs_po hs) + (hs_poe hs) + in FApi.xmutate1 tc `Sp [subgoal] diff --git a/src/phl/ecPhlUpto.ml b/src/phl/ecPhlUpto.ml index 7dc597b9ea..93478af3cd 100644 --- a/src/phl/ecPhlUpto.ml +++ b/src/phl/ecPhlUpto.ml @@ -62,7 +62,7 @@ let rec check_bad_true env bad s = | Smatch(_,bs) -> let check_branch (_, s) = check_bad_true env bad s.s_node in List.iter (check_branch) bs - | Sassert _ -> () + | Sraise _ -> assert false | Sabstract _ -> () end; check_bad_true env bad c @@ -142,8 +142,7 @@ and i_upto env alpha bad i1 i2 = with E.NotConv -> false end - | Sassert a1, Sassert a2 -> - EqTest.for_expr env ~alpha a1 a2 + | Sraise (_e1,_es1), Sraise (_e2,_es2) -> assert false | Sabstract id1, Sabstract id2 -> EcIdent.id_equal id1 id2 diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index c54b43ea49..507b49f99f 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -42,8 +42,7 @@ let while_info env e s = let f = EcEnv.NormMp.norm_xfun env f in (w, r, Sx.add f c) - | Sassert e -> - (w, e_read_r env r e, c) + | Sraise _ -> assert false | Sabstract id -> let add_pv x (pv,ty) = PV.add env pv ty x in @@ -71,14 +70,14 @@ let t_hoare_while_r inv tc = (* the body preserves the invariant *) let b_pre = map_ss_inv2 f_and_simpl inv e in let b_post = inv in - let b_concl = f_hoareS mt b_pre c b_post in + let b_concl = f_hoareS mt b_pre c b_post (hs_poe hs) in (* the wp of the while *) let f_imps_simpl' f = f_imps_simpl (List.tl f) (List.hd f) in let post = map_ss_inv f_imps_simpl' [hs_po hs;map_ss_inv1 f_not_simpl e; inv] in let modi = s_write env c in let post = generalize_mod_ss_inv env modi post in let post = map_ss_inv2 f_and_simpl inv post in - let concl = f_hoareS mt (hs_pr hs) s post in + let concl = f_hoareS mt (hs_pr hs) s post (hs_poe hs) in FApi.xmutate1 tc `While [b_concl; concl] @@ -94,7 +93,7 @@ let t_ehoare_while_core tc = check_single_stmt tc s; let (m, mt) = hs.ehs_m in let e = ss_inv_of_expr m e in - if not (EcReduction.ss_inv_alpha_eq hyps (ehs_po hs) + if not (EcReduction.ss_inv_alpha_eq hyps (ehs_po hs) (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not e) (ehs_pr hs))) then tc_error !!tc "ehoare while rule: wrong post-condition"; (* the body preserves the invariant *) @@ -136,7 +135,7 @@ let t_bdhoare_while_r inv vrnt tc = (* the wp of the while *) let f_imps_simpl' f = f_imps_simpl (List.tl f) (List.hd f) in let post = map_ss_inv f_imps_simpl' [bhs_po bhs; map_ss_inv1 f_not_simpl e; inv] in - let term_condition = map_ss_inv f_imps_simpl' + let term_condition = map_ss_inv f_imps_simpl' [map_ss_inv1 f_not_simpl e; inv;map_ss_inv2 f_int_le vrnt {m;inv=f_i0}] in let post = map_ss_inv2 f_and term_condition post in let modi = s_write env c in @@ -187,7 +186,7 @@ let t_bdhoare_while_rev_r inv tc = (map_ss_inv2 f_eq bound {m;inv=f_r1}) in let term_post = generalize_mod_ss_inv env modi term_post in let term_post = map_ss_inv2 f_and inv term_post in - f_hoareS mt b_pre rem_s term_post + f_hoareS mt b_pre rem_s term_post [] in FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)] @@ -252,14 +251,14 @@ let t_bdhoare_while_rev_geq_r inv vrnt k (eps: ss_inv) tc = let vrnt_eq_k = map_ss_inv2 f_eq vrnt k in let vrnt_lt_k = map_ss_inv2 f_int_lt vrnt k in f_and - (EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_imp inv + (EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_imp inv (map_ss_inv2 f_real_lt {m;inv=f_r0} eps))) (f_forall_simpl [(k_id,GTty tint)] (f_bdHoareS - mt - (map_ss_inv f_ands [inv;lp_guard;vrnt_eq_k]) + mt + (map_ss_inv f_ands [inv;lp_guard;vrnt_eq_k]) lp_body - vrnt_lt_k + vrnt_lt_k FHge eps)) in @@ -297,7 +296,7 @@ let t_bdhoare_while_rev_geq_r inv vrnt k (eps: ss_inv) tc = let t_equiv_while_disj_r side vrnt inv tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in - let ss_inv_generalize_other f = + let ss_inv_generalize_other f = match side with | `Left -> ss_inv_generalize_right f (fst es.es_mr) | `Right -> ss_inv_generalize_left f (fst es.es_ml) in @@ -321,7 +320,7 @@ let t_equiv_while_disj_r side vrnt inv tc = let b_pre = map_ts_inv2 f_and_simpl (map_ts_inv2 f_and_simpl inv e) vrnt_eq_k in let b_post = map_ts_inv2 f_and_simpl inv vrnt_lt_k in - let b_concl = ts_inv_lower_side2 (fun pr po -> + let b_concl = ts_inv_lower_side2 (fun pr po -> let m = EcIdent.create "&hr" in let pr = EcSubst.ss_inv_rebind pr m in let po = EcSubst.ss_inv_rebind po m in @@ -332,7 +331,7 @@ let t_equiv_while_disj_r side vrnt inv tc = (* 2. WP of the while *) let f_imps_simpl' fl = f_imps_simpl (List.tl fl) (List.hd fl) in let post = map_ts_inv f_imps_simpl' [es_po es; map_ts_inv1 f_not_simpl e; inv] in - let term_condition = map_ts_inv + let term_condition = map_ts_inv f_imps_simpl' [map_ts_inv1 f_not_simpl e; inv;map_ts_inv2 f_int_le vrnt {ml;mr;inv=f_i0}] in let post = map_ts_inv2 f_and term_condition post in let modi = s_write env c in @@ -488,7 +487,7 @@ let t_equiv_ll_while_disj_r side inv tc = let post = map_ts_inv2 f_and_simpl inv post in let concl = let sl, sr = sideif side (s, es.es_sr) (es.es_sl, s) in - f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr post + f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr post in FApi.xmutate1 tc `While [b_concl; ll; concl] @@ -513,7 +512,7 @@ let t_equiv_while_r inv tc = (* 2. WP of the while *) let f_imps_simpl' f = f_imps_simpl (List.tl f) (List.hd f) in - let post = map_ts_inv f_imps_simpl' [es_po es; + let post = map_ts_inv f_imps_simpl' [es_po es; map_ts_inv1 f_not_simpl el; map_ts_inv1 f_not_simpl er; inv] in let modil = s_write env cl in let modir = s_write env cr in @@ -633,7 +632,7 @@ let process_async_while (winfos : EP.async_while_info) tc = let cond1 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr (map_ts_inv f_imps' [map_ts_inv f_ands [fe1; fe2; map_ts_inv f_app' [ft1; f1]; - map_ts_inv f_app' [ft2; f2]]; + map_ts_inv f_app' [ft2; f2]]; inv; fe; p0]) in let cond2 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr @@ -662,13 +661,13 @@ let process_async_while (winfos : EP.async_while_info) tc = let el = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in let pre = map_ts_inv f_ands [inv; el ; map_ts_inv1 f_not p0; p1] in EcSubst.f_forall_mems_ss_inv evs.es_mr - (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd evs.es_ml) pr cl po) pre inv) + (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd evs.es_ml) pr cl po []) pre inv) and hr2 = let er = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in let pre = map_ts_inv f_ands [inv; er; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1] in EcSubst.f_forall_mems_ss_inv evs.es_ml - (ts_inv_lower_right2 (fun pr po -> f_hoareS (snd evs.es_mr) pr cr po) pre inv) + (ts_inv_lower_right2 (fun pr po -> f_hoareS (snd evs.es_mr) pr cr po []) pre inv) in (hr1, hr2) in diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 49a8d6d131..f7ae9a70b6 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -11,32 +11,35 @@ open EcLowPhlGoal module LowInternal = struct exception No_wp + let find_poe epost e = + snd (List.find (fun (e',_) -> EcPath.p_ntr_equal e e') epost) + let wp_asgn_aux c_pre memenv lv e (lets, f) = let m = EcMemory.memory memenv in let let1 = lv_subst ?c_pre m lv (ss_inv_of_expr m e).inv in (let1::lets, f) let rec wp_stmt ?mc - onesided c_pre env memenv (stmt: EcModules.instr list) letsf + onesided c_pre env memenv (stmt: EcModules.instr list) letsf epost = match stmt with | [] -> (stmt, letsf) | i :: stmt' -> try - let letsf = wp_instr ?mc onesided c_pre env memenv i letsf in - wp_stmt ?mc onesided c_pre env memenv stmt' letsf + let letsf = wp_instr ?mc onesided c_pre env memenv i letsf epost in + wp_stmt ?mc onesided c_pre env memenv stmt' letsf epost with No_wp -> (stmt, letsf) - and wp_instr ?mc onesided c_pre env memenv i letsf = + and wp_instr ?mc onesided c_pre env memenv i letsf epost = match i.i_node with | Sasgn (lv,e) -> wp_asgn_aux c_pre memenv lv e letsf | Sif (e,s1,s2) -> let (r1,letsf1) = - wp_stmt ?mc onesided c_pre env memenv (List.rev s1.s_node) letsf in + wp_stmt ?mc onesided c_pre env memenv (List.rev s1.s_node) letsf epost in let (r2,letsf2) = - wp_stmt ?mc onesided c_pre env memenv (List.rev s2.s_node) letsf in + wp_stmt ?mc onesided c_pre env memenv (List.rev s2.s_node) letsf epost in if List.is_empty r1 && List.is_empty r2 then begin let post1 = mk_let_of_lv_substs ?mc:mc env letsf1 in let post2 = mk_let_of_lv_substs ?mc:mc env letsf2 in @@ -49,7 +52,7 @@ module LowInternal = struct | Smatch (e, bs) -> begin let wps = let do1 (_, s) = - wp_stmt ?mc onesided c_pre env memenv (List.rev s.s_node) letsf in + wp_stmt ?mc onesided c_pre env memenv (List.rev s.s_node) letsf epost in List.map do1 bs in @@ -70,10 +73,7 @@ module LowInternal = struct ([],post) end - | Sassert e when onesided -> - let phi = ss_inv_of_expr (EcMemory.memory memenv) e in - let lets, f = letsf in - (lets, EcFol.f_and_simpl phi.inv f) + | Sraise (e,_) when onesided -> ([], find_poe epost e) | _ -> raise No_wp @@ -120,10 +120,10 @@ module LowInternal = struct end -let wp ?mc ?(uselet=true) ?(onesided=false) ?c_pre env m s post = +let wp ?mc ?(uselet=true) ?(onesided=false) ?c_pre env m s post epost = let (r, letsf) = LowInternal.wp_stmt ?mc - onesided c_pre env m (List.rev s.s_node) ([], post) + onesided c_pre env m (List.rev s.s_node) ([], post) epost in let pre = mk_let_of_lv_substs ?mc ~uselet env letsf in List.rev r, pre @@ -144,12 +144,13 @@ module TacInternal = struct let hs = tc1_as_hoareS tc in let (s_hd, s_wp) = o_split env i hs.hs_s in let s_wp = EcModules.stmt s_wp in + let poe = List.map (fun (e,(f:ss_inv)) -> e,f.inv) (hs_poe hs) in let s_wp, post = - wp ~uselet ~onesided:true env hs.hs_m s_wp (hs_po hs).inv in + wp ~uselet ~onesided:true env hs.hs_m s_wp (hs_po hs).inv poe in check_wp_progress tc i hs.hs_s s_wp; let s = EcModules.stmt (s_hd @ s_wp) in let m = fst hs.hs_m in - let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s {m;inv=post} in + let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s {m;inv=post} (hs_poe hs) in FApi.xmutate1 tc `Wp [concl] let t_ehoare_wp ?(uselet=true) i tc = @@ -169,7 +170,7 @@ module TacInternal = struct let bhs = tc1_as_bdhoareS tc in let (s_hd, s_wp) = o_split env i bhs.bhs_s in let s_wp = EcModules.stmt s_wp in - let s_wp,post = wp ~uselet env bhs.bhs_m s_wp (bhs_po bhs).inv in + let s_wp,post = wp ~uselet env bhs.bhs_m s_wp (bhs_po bhs).inv [] in check_wp_progress tc i bhs.bhs_s s_wp; let s = EcModules.stmt (s_hd @ s_wp) in let m = fst bhs.bhs_m in @@ -186,8 +187,8 @@ module TacInternal = struct let meml, s_wpl = es.es_ml, EcModules.stmt s_wpl in let memr, s_wpr = es.es_mr, EcModules.stmt s_wpr in let post = es_po es in - let s_wpl, post = wp ~mc:(ml,mr) ~uselet env meml s_wpl post.inv in - let s_wpr, post = wp ~mc:(ml,mr) ~uselet env memr s_wpr post in + let s_wpl, post = wp ~mc:(ml,mr) ~uselet env meml s_wpl post.inv [] in + let s_wpr, post = wp ~mc:(ml,mr) ~uselet env memr s_wpr post [] in check_wp_progress tc i es.es_sl s_wpl; check_wp_progress tc j es.es_sr s_wpr; let sl = EcModules.stmt (s_hdl @ s_wpl) in