Add check to prevent swapping of exception raises

Author: lyonel2017

src/ecCoreModules.ml

@@ -161,6 +161,26 @@ let is_while  = _is_of_get get_while
 let is_match  = _is_of_get get_match
 let is_raise  = _is_of_get get_raise
 
+(* -------------------------------------------------------------------- *)
+let i_iter (f : instr -> unit) =
+  let rec i_iter (i : instr) =
+    match i.i_node with
+    | Sasgn _ | Srnd _ | Scall _ | Sraise _ | Sabstract _ -> ()
+
+    | Sif (_, s1, s2) ->
+      List.iter fs [s1; s2] 
+
+    | Swhile (_, s) ->
+      fs s
+
+    | Smatch (_, bs) ->
+      List.iter (fun (_, s) -> fs s) bs
+
+  and fs (s : stmt) =
+    List.iter f s.s_node
+
+  in fun (i : instr) -> i_iter i
+
 (* -------------------------------------------------------------------- *)
 module Uninit = struct    (* FIXME: generalize this for use in ecPV *)
   let e_pv e =

src/ecCoreModules.mli

@@ -76,6 +76,9 @@ val is_while  : instr -> bool
 val is_match  : instr -> bool
 val is_raise  : instr -> bool
 
+(* -------------------------------------------------------------------- *)
+val i_iter : (instr -> unit) -> instr -> unit
+
 (* -------------------------------------------------------------------- *)
 val get_uninit_read : stmt -> Sx.t
 

src/phl/ecPhlSwap.ml

@@ -19,6 +19,23 @@ type swap_kind = {
 (* -------------------------------------------------------------------- *)
 module LowInternal = struct
   let check_swap (pf : proofenv) (env : EcEnv.env) (s1 : stmt) (s2 : stmt) =
+    let is_contains_raise =
+      let exception HasRaise in
+
+      let rec i_contains_raise (i : instr) =
+        match i.i_node with
+        | Sraise _ -> raise HasRaise
+        | _ -> EcModules.i_iter i_contains_raise i in
+
+      fun (s : stmt) ->
+        try
+          List.iter i_contains_raise s.s_node;
+          false
+        with HasRaise -> true in
+
+    if List.exists is_contains_raise [s1; s2] then
+      tc_error pf "cannot swap blocks that contain exceptions";
+
     let m1,m2 = s_write env s1, s_write env s2 in
     let r1,r2 = s_read  env s1, s_read  env s2 in
     (* FIXME: this is not sufficient *)

tests/exception/exception_swap.ec

@@ -0,0 +1,32 @@
+require import AllCore.
+
+exception exn1.
+
+module M = {
+  var w : int
+  var x : int
+  var y : int
+  var z : int
+
+  proc f() : unit = {
+  w <- 42;
+  x <- 42;
+  raise exn1;
+  y <- 42;
+  z <- 42;
+  }
+}.
+
+lemma f_correct :
+  hoare[M.f : true ==> false | exn1 => M.x = 42 /\ M.w = 42].
+proof. proc. wp. skip. smt(). qed.
+
+lemma f_wrong :
+  hoare[M.f : M.x = 0 ==> false | exn1 => M.x = 0].
+proof. proc.
+  swap 1 1.
+  swap 4 1.
+  fail swap 1 2.
+  fail swap 1 3.
+  fail swap 3 1.
+abort.