Add exception declaration, raise, and update logic

Author: lyonel2017

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.

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 = {
@@ -230,18 +230,22 @@ and equivS = {
   es_sr  : stmt;
   es_po  : form; }
 
+and post = (EcPath.path * form) list
+
 and sHoareF = {
   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_pr  : form;
@@ -615,13 +619,25 @@ 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
 
 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
@@ -680,14 +696,27 @@ let pr_equal pr1 pr2 =
   && f_equal          pr1.pr_event pr2.pr_event
   && f_equal          pr1.pr_args pr2.pr_args
 
+(*-------------------------------------------------------------------- *)
+
+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.combine2
-    (f_hash hf.hf_pr) (f_hash hf.hf_po) (EcPath.x_hash hf.hf_f)
+    (f_hash hf.hf_pr)
+    (Why3.Hashcons.combine (f_hash hf.hf_po) (posts_hash hf.hf_poe))
+    (EcPath.x_hash hf.hf_f)
 
 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)
 
@@ -1036,6 +1065,11 @@ module Hsform = Why3.Hashcons.Make (struct
 
   let fv_mlr = Sid.add mleft (Sid.singleton mright)
 
+  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
@@ -1063,11 +1097,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 mhr 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 ->
@@ -1162,8 +1198,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
 
@@ -1201,7 +1238,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
 
@@ -1235,8 +1275,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

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 {
@@ -225,17 +225,22 @@ and equivS = {
   es_sr  : stmt;
   es_po  : form; }
 
+and post = (EcPath.path * form) list
+
 and sHoareF = {
   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 = {

src/ecCallbyValue.ml

@@ -222,7 +222,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;
@@ -483,7 +483,8 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let hf_pr = norm st s hf.hf_pr in
     let hf_po = norm st s hf.hf_po in
     let hf_f  = norm_xfun st s hf.hf_f in
-    f_hoareF_r { hf_pr; hf_f; hf_po }
+    let hf_poe  = List.map (fun (e,f) -> e, norm st s f) hf.hf_poe in
+    f_hoareF_r { hf_pr; hf_f; hf_po; hf_poe}
 
   | FhoareS hs ->
     assert (Args.isempty args);
@@ -492,7 +493,8 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let hs_po = norm st s hs.hs_po in
     let hs_s  = norm_stmt s hs.hs_s in
     let hs_m  = norm_me s hs.hs_m in
-    f_hoareS_r { hs_pr; hs_po; hs_s; hs_m }
+    let hs_poe  = List.map (fun (e,f) -> e, norm st s f) hs.hs_poe in
+    f_hoareS_r { hs_pr; hs_po; hs_s; hs_m; hs_poe}
 
   | FeHoareF hf ->
     assert (Args.isempty args);