From aa119aaadc66c1fab772acdfc489f234c356c042 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@mpi-sp.org>
Date: Fri, 11 Sep 2026 14:44:03 +0200
Subject: [PATCH] Fix swap when exception are in call

---
 src/phl/ecPhlSwap.ml              | 41 ++++++++++++-------------------
 tests/exception/exception_swap.ec |  6 ++---
 2 files changed, 19 insertions(+), 28 deletions(-)

diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml
index 821391bc4..887927aed 100644
--- a/src/phl/ecPhlSwap.ml
+++ b/src/phl/ecPhlSwap.ml
@@ -18,24 +18,15 @@ 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 check_swap tc (env : EcEnv.env) (s1 : stmt) (s2 : stmt) =
+
+    let concl = FApi.tc1_goal tc in
+    match concl.f_node with
+    | FhoareS h ->
+      if not (POE.is_empty (hs_po h).hsi_inv) then
+        tc_error !!tc "Swaping blocks with exceptions not allowed"
+    | _  ->  ()
+                   ;
     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 *)
@@ -44,7 +35,7 @@ module LowInternal = struct
     let m1r2 = PV.interdep env m1 r2 in
 
     let error mode d =
-      tc_error_lazy pf (fun fmt ->
+      tc_error_lazy !!tc (fun fmt ->
         Format.fprintf fmt
           "the two statements are not independent, %t"
           (fun fmt ->
@@ -64,7 +55,7 @@ module LowInternal = struct
 
 
   let swap_stmt
-    (pf   : proofenv   )
+    tc
     (env  : EcEnv.env  )
     (info : swap_kind  )
     (s    : stmt       )
@@ -72,7 +63,7 @@ module LowInternal = struct
     let zpr, _, (_, (start, fin)) = try
       EcMatching.Zipper.zipper_and_split_of_cgap_range env info.interval s
     with InvalidCPos ->
-      tc_error_lazy pf (fun fmt ->
+      tc_error_lazy !!tc (fun fmt ->
         let ppe = EcPrinting.PPEnv.ofenv env in
         Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval
       )
@@ -84,7 +75,7 @@ module LowInternal = struct
     let target = try
       resolve_gap_offset env (start, fin) info.offset s
     with InvalidCPos ->
-      tc_error pf "invalid offset for swap"
+      tc_error !!tc "invalid offset for swap"
     in
 
     match split_by_nmcgaps
@@ -92,8 +83,8 @@ module LowInternal = struct
       then [target; start; fin]
       else [start; fin; target]
       ) s
-    with 
-    | [hd; s1; s2; tl] -> check_swap pf env (stmt s1) (stmt s2);
+    with
+    | [hd; s1; s2; tl] -> check_swap tc env (stmt s1) (stmt s2);
       EcMatching.Zipper.zip
         { zpr with z_head = []; z_tail = List.flatten [hd; s2; s1; tl] }
     | _ -> assert false
@@ -103,7 +94,7 @@ end
 let t_swap_r (side : oside) (info : swap_kind) (tc : tcenv1) =
   let env = FApi.tc1_env tc in
   let _, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
-  let stmt = LowInternal.swap_stmt !!tc env info stmt in
+  let stmt = LowInternal.swap_stmt tc env info stmt in
   FApi.xmutate1 tc `Swap [EcLowPhlGoal.hl_set_stmt side (FApi.tc1_goal tc) stmt]
 
 (* -------------------------------------------------------------------- *)
diff --git a/tests/exception/exception_swap.ec b/tests/exception/exception_swap.ec
index 7d1a06f5e..f008793a1 100644
--- a/tests/exception/exception_swap.ec
+++ b/tests/exception/exception_swap.ec
@@ -19,13 +19,13 @@ module M = {
 
 lemma f_correct :
   hoare[M.f : true ==> false | exn1 => M.x = 42 /\ M.w = 42].
-proof. proc. wp. skip. smt(). qed.
+proof. proc. wp. skip. move => //.  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 1.
+  fail swap 4 1.
   fail swap 1 2.
   fail swap 1 3.
   fail swap 3 1.