Make-reference-arguments also applies to #swap

Fixes #815

CHANGELOG.md

@@ -33,7 +33,8 @@
   See `compiler/tests/success/common/swap.jazz` and
       `compiler/tests/success/common/swap_word.jazz` for usage.
   ([PR #691](https://github.com/jasmin-lang/jasmin/pull/691),
-   [PR #816](https://github.com/jasmin-lang/jasmin/pull/816)).
+   [PR #816](https://github.com/jasmin-lang/jasmin/pull/816),
+   [PR #818](https://github.com/jasmin-lang/jasmin/pull/818)).
 
 - Support Selective Speculative Load Hardening.
   We now support operators SLH operators as in [Typing High-Speed Cryptography

compiler/tests/success/common/bug_815.jazz

@@ -0,0 +1,9 @@
+export
+fn snd(reg u32 x y) -> reg u32 {
+  stack u32[1] a b;
+  a[0] = x;
+  b[0] = y;
+  a, b = #swap(a, b);
+  x = a[0];
+  return x;
+}

proofs/compiler/makeReferenceArguments.v

@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import ssreflect ssrfun ssrbool.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
 From Coq Require Import ZArith Uint63.
 Require Import gen_map expr compiler_util.
 
@@ -134,10 +134,22 @@ Definition get_syscall_sig o :=
   (map (fun ty => (is_sarr ty, "__p__"%string, ty)) s.(scs_tin),
    map (fun ty => (is_sarr ty, "__p__"%string, ty)) s.(scs_tout)).
 
+Definition is_swap_op (op: sopn) : option stype :=
+  if op is Opseudo_op (pseudo_operator.Oswap (sarr _ as ty)) then Some ty else None.
+
 Fixpoint update_i (X:Sv.t) (i:instr) : cexec cmd :=
   let (ii,ir) := i in
   match ir with
-  | Cassgn _ _ _ _ |  Copn _ _ _ _  => ok [::i]
+  | Copn xs tg op es =>
+      if is_swap_op op is Some ty then
+        let sig := (true, "__swap__"%string, ty) in
+        let sig := [:: sig; sig ] in
+        Let: (prologue, es) := make_prologue ii X 0 sig es in
+        Let: (xs, epilogue) := make_epilogue ii X sig xs in
+        let tg := if [&& size prologue == 2 & size epilogue == 2] then AT_inline else tg in
+        ok (prologue ++ MkI ii (Copn xs tg (Opseudo_op (pseudo_operator.Oswap ty)) es) :: epilogue)
+      else ok [:: i ]
+  | Cassgn _ _ _ _ => ok [:: i ]
   | Cif b c1 c2 =>
     Let c1 := update_c (update_i X) c1 in
     Let c2 := update_c (update_i X) c2 in

proofs/compiler/makeReferenceArguments_proof.v

@@ -337,9 +337,115 @@ Context
     by apply/sem_seq1/EmkI/(Eassgn _ _ he htr); rewrite -eq_globs.
   Qed.
 
+  Lemma is_reg_ptr_expr_ty b ii ctr x ty lv y:
+     is_reg_ptr_expr fresh_id b ii ctr x ty lv = Some y -> vtype y = ty.
+  Proof. by case: lv => //= [? | _ _ _ ? _]; case: ifP => // _ [<-]. Qed.
+
+  Lemma make_prologueP X ii s:
+     forall xfty ctr args Y pl args',
+       make_prologue fresh_id ii Y ctr xfty args = ok (pl, args') ->
+       Sv.Subset X Y ->
+       Sv.Subset (read_es args) X ->
+     forall vargs vs vm1,
+       sem_pexprs true (p_globs p) s args = ok vargs ->
+       mapM2 ErrType truncate_val (map snd xfty) vargs = ok vs ->
+       evm s =[X] vm1 ->
+     exists vm2 vargs', [/\
+      sem p' ev (with_vm s vm1) pl (with_vm s vm2),
+      sem_pexprs true (p_globs p') (with_vm s vm2) args' = ok vargs',
+      mapM2 ErrType truncate_val (map snd xfty) vargs' = ok vs &
+      vm1 =[Y] vm2].
+  Proof.
+    elim.
+    + move=> ctr [] //= Y _ _ [<- <-] _ _ _ _ vm1 [<-] [<-] _.
+      exists vm1, [::]; split => //; constructor.
+    move=> [[b x] ty] xfty ih ctr [] //= a args Y _pl _args'; rewrite read_es_cons.
+    move=> hisr hXY hX _vargs _vs vm1; t_xrbindP => va hva vargs hvargs <- {_vargs}.
+    t_xrbindP => v hv vs hvs <- {_vs} heqvm.
+    have [haX hasX]: Sv.Subset (read_e a) X /\ Sv.Subset (read_es args) X by split; SvD.fsetdec.
+    case E: is_reg_ptr_expr hisr => [y | ]; t_xrbindP; last first.
+    + move=> [c args'] hmk [<- <-] {_pl _args'}.
+      have [vm2 [vargs' [h1 h2 h3 h4]]]:= ih _ _ _ _ _ hmk hXY hasX _ _ vm1 hvargs hvs heqvm.
+      exists vm2, [:: va & vargs']; split => //=; last by rewrite hv h3.
+      rewrite -(eq_on_sem_pexpr _ _ (s:= s)) //=; last first.
+      + by apply (eq_onT (vm2:= vm1));[apply: eq_onI heqvm => //| apply: eq_onI h4; SvD.fsetdec ].
+      by rewrite h2 -(make_referenceprog_globs Hp) hva.
+    move=> /Sv_memP hnin [c args'] hmk [<- <-]{_pl _args'}.
+    have ? := is_reg_ptr_expr_ty E; subst ty.
+
+    pose vm1' := vm1.[y <- v].
+    have [|| vm2 [vargs' [h1 h2 h3 h4]]]:= ih _ _ _ _ _ hmk _ hasX _ _ vm1' hvargs hvs.
+    + by SvD.fsetdec.
+    + by apply: (eq_onT heqvm)=> z hz; rewrite /vm1' Vm.setP_neq //; apply/eqP => h;apply hnin; SvD.fsetdec.
+    exists vm2, [:: v & vargs']; split => //; first last.
+    + apply (eq_onT (vm2:= vm1')); last by apply: eq_onI h4; SvD.fsetdec.
+      by move=> z hz; rewrite /vm1' Vm.setP_neq //; apply/eqP => h;apply hnin; SvD.fsetdec.
+    + by rewrite (truncate_val_idem hv) h3.
+    + rewrite /= /get_gvar /= /get_var -(h4 y); last by SvD.fsetdec.
+      rewrite /vm1' Vm.setP_eq /= vm_truncate_val_eq; last by apply: truncate_val_has_type hv.
+      by rewrite (truncate_val_defined hv) /= h2.
+    apply: Eseq h1; apply/EmkI; econstructor; eauto.
+    + rewrite -hva -(make_referenceprog_globs Hp); apply eq_on_sem_pexpr => //.
+      by rewrite evm_with_vm; apply/eq_onS/eq_onI/heqvm.
+    rewrite /write_lval; apply/write_var_eq_type.
+    + by apply: truncate_val_has_type hv.
+    by apply: truncate_val_DB hv.
+  Qed.
+
+  Lemma make_epilogueP X ii s1 s2 xfty lv lv' ep vres vs vm1 :
+    make_epilogue fresh_id ii X xfty lv = ok (lv', ep) ->
+    Sv.Subset (Sv.union (read_rvs lv) (vrvs lv)) X ->
+    write_lvals true (p_globs p) s1 lv vs = ok s2 ->
+    mapM2 ErrType truncate_val (map snd xfty) vres = ok vs ->
+    evm s1 =[X] vm1 ->
+    exists vm2 s2', [/\
+      write_lvals true (p_globs p') (with_vm s1 vm1) lv' vs = ok s2',
+      sem p' ev s2' ep (with_vm s2 vm2) &
+      evm s2 =[X] vm2].
+  Proof.
+    move=> eqE hsub hw htr heqon; move: eqE; rewrite /make_epilogue.
+    t_xrbindP => pinstrs Hpseudo Hswap.
+    have [vm2 Hsem_pis eq_s2_vm2]:= make_pseudo_codeP Hpseudo htr hsub hw heqon.
+    have [sy [vmy] [Hwrite_lvals Hsem /= eq_vm2_vmy]]:= swapableP Hswap Hsem_pis.
+    exists vmy, sy ; split => //.
+    by apply/(eq_onT eq_s2_vm2)/vm_eq_eq_on.
+  Qed.
+
+  Opaque make_prologue.
+
   Local Lemma Hopn : sem_Ind_opn p Pi_r.
   Proof.
-    move=> s1 s2 t o xs es He ii X c' [<-].
+    move=> s1 s2 t o xs es He ii X c' /=.
+    case hop: is_swap_op => [ ty | ].
+    {
+      case: o He hop => // - [] // [] // len He /Some_inj <-{ty}.
+      t_xrbindP => - [] prologue es' ok_prologue.
+      t_xrbindP => - [] epilogue xs' ok_epilogue.
+      move => /ok_inj <- {c'}.
+      rewrite /write_I /write_I_rec /read_I /read_I_rec read_esE vrvs_recE => hsub vm hvm.
+      move: He; rewrite /sem_sopn /=; t_xrbindP => rs vs ok_vs ok_rs ok_xs.
+      have X_es : Sv.Subset (read_es es) X by clear - hsub; SvD.fsetdec.
+      case: vs ok_rs ok_vs => // a'' vs.
+      rewrite /exec_sopn /=; t_xrbindP => - [] /= a b a' /to_arrI -> {a''}.
+      case: vs => //; t_xrbindP => _ [] // b' /to_arrI -> [] ???; subst a' b' rs => ok_vs.
+      have := make_prologueP ok_prologue _ X_es ok_vs (vs := [:: Varr b; Varr a]) _ hvm.
+      case; first by clear; SvD.fsetdec.
+      - by rewrite /= /truncate_val /= !WArray.castK.
+      move => vm' [] vs' [] sem_pl ok_vs' {} ok_vs hvm'.
+      have X_xs : Sv.Subset (Sv.union (read_rvs xs) (vrvs xs)) X by clear -hsub; SvD.fsetdec.
+      have := make_epilogueP ok_epilogue X_xs ok_xs (vres := [:: Varr a; Varr b]) _ (eq_onT hvm hvm').
+      case; first by rewrite /= /truncate_val /= !WArray.castK.
+      move => vm2 [] s2' [] ok_s2' sem_el hvm2.
+      exists vm2; first by [].
+      apply: (sem_app sem_pl); apply: (Eseq _ sem_el); apply: EmkI.
+      case: vs' ok_vs ok_vs' => // - [] // ? ? vs' /=; t_xrbindP => ? /truncate_valE[] [] ???; subst.
+      case: vs' => // - [] // ? a' vs'; t_xrbindP => ? /truncate_valE[] [] ???; subst.
+      case: vs' => // /ok_inj <- <- /Varr_inj1 ?; subst => ? ok_vs'.
+      have ? : a' = a by apply: Varr_inj1; congruence.
+      subst a'.
+      by constructor; rewrite /sem_sopn ok_vs' /exec_sopn /= !WArray.castK /=.
+    }
+    move => /ok_inj <- {c'}.
     rewrite read_Ii read_i_opn /write_I /write_I_rec vrvs_recE => hsub vm1 hvm1.
     move: He; rewrite eq_globs /sem_sopn Let_Let.
     t_xrbindP => vs Hsem_pexprs res Hexec_sopn hw.
@@ -460,80 +566,6 @@ Context
     by apply: (eq_onI _ eq_s1_vm1); SvD.fsetdec.
   Qed.
 
-  Lemma is_reg_ptr_expr_ty b ii ctr x ty lv y:
-     is_reg_ptr_expr fresh_id b ii ctr x ty lv = Some y -> vtype y = ty.
-  Proof. by case: lv => //= [? | _ _ _ ? _]; case: ifP => // _ [<-]. Qed.
-
-  Lemma make_prologueP X ii s:
-     forall xfty ctr args Y pl args',
-       make_prologue fresh_id ii Y ctr xfty args = ok (pl, args') ->
-       Sv.Subset X Y ->
-       Sv.Subset (read_es args) X ->
-     forall vargs vs vm1,
-       sem_pexprs true (p_globs p) s args = ok vargs ->
-       mapM2 ErrType truncate_val (map snd xfty) vargs = ok vs ->
-       evm s =[X] vm1 ->
-     exists vm2 vargs', [/\
-      sem p' ev (with_vm s vm1) pl (with_vm s vm2),
-      sem_pexprs true (p_globs p') (with_vm s vm2) args' = ok vargs',
-      mapM2 ErrType truncate_val (map snd xfty) vargs' = ok vs &
-      vm1 =[Y] vm2].
-  Proof.
-    elim.
-    + move=> ctr [] //= Y _ _ [<- <-] _ _ _ _ vm1 [<-] [<-] _.
-      exists vm1, [::]; split => //; constructor.
-    move=> [[b x] ty] xfty ih ctr [] //= a args Y _pl _args'; rewrite read_es_cons.
-    move=> hisr hXY hX _vargs _vs vm1; t_xrbindP => va hva vargs hvargs <- {_vargs}.
-    t_xrbindP => v hv vs hvs <- {_vs} heqvm.
-    have [haX hasX]: Sv.Subset (read_e a) X /\ Sv.Subset (read_es args) X by split; SvD.fsetdec.
-    case E: is_reg_ptr_expr hisr => [y | ]; t_xrbindP; last first.
-    + move=> [c args'] hmk [<- <-] {_pl _args'}.
-      have [vm2 [vargs' [h1 h2 h3 h4]]]:= ih _ _ _ _ _ hmk hXY hasX _ _ vm1 hvargs hvs heqvm.
-      exists vm2, [:: va & vargs']; split => //=; last by rewrite hv h3.
-      rewrite -(eq_on_sem_pexpr _ _ (s:= s)) //=; last first.
-      + by apply (eq_onT (vm2:= vm1));[apply: eq_onI heqvm => //| apply: eq_onI h4; SvD.fsetdec ].
-      by rewrite h2 -(make_referenceprog_globs Hp) hva.
-    move=> /Sv_memP hnin [c args'] hmk [<- <-]{_pl _args'}.
-    have ? := is_reg_ptr_expr_ty E; subst ty.
-
-    pose vm1' := vm1.[y <- v].
-    have [|| vm2 [vargs' [h1 h2 h3 h4]]]:= ih _ _ _ _ _ hmk _ hasX _ _ vm1' hvargs hvs.
-    + by SvD.fsetdec.
-    + by apply: (eq_onT heqvm)=> z hz; rewrite /vm1' Vm.setP_neq //; apply/eqP => h;apply hnin; SvD.fsetdec.
-    exists vm2, [:: v & vargs']; split => //; first last.
-    + apply (eq_onT (vm2:= vm1')); last by apply: eq_onI h4; SvD.fsetdec.
-      by move=> z hz; rewrite /vm1' Vm.setP_neq //; apply/eqP => h;apply hnin; SvD.fsetdec.
-    + by rewrite (truncate_val_idem hv) h3.
-    + rewrite /= /get_gvar /= /get_var -(h4 y); last by SvD.fsetdec.
-      rewrite /vm1' Vm.setP_eq /= vm_truncate_val_eq; last by apply: truncate_val_has_type hv.
-      by rewrite (truncate_val_defined hv) /= h2.
-    apply: Eseq h1; apply/EmkI; econstructor; eauto.
-    + rewrite -hva -(make_referenceprog_globs Hp); apply eq_on_sem_pexpr => //.
-      by rewrite evm_with_vm; apply/eq_onS/eq_onI/heqvm.
-    rewrite /write_lval; apply/write_var_eq_type.
-    + by apply: truncate_val_has_type hv.
-    by apply: truncate_val_DB hv.
-  Qed.
-
-  Lemma make_epilogueP X ii s1 s2 xfty lv lv' ep vres vs vm1 :
-    make_epilogue fresh_id ii X xfty lv = ok (lv', ep) ->
-    Sv.Subset (Sv.union (read_rvs lv) (vrvs lv)) X ->
-    write_lvals true (p_globs p) s1 lv vs = ok s2 ->
-    mapM2 ErrType truncate_val (map snd xfty) vres = ok vs ->
-    evm s1 =[X] vm1 ->
-    exists vm2 s2', [/\
-      write_lvals true (p_globs p') (with_vm s1 vm1) lv' vs = ok s2',
-      sem p' ev s2' ep (with_vm s2 vm2) &
-      evm s2 =[X] vm2].
-  Proof.
-    move=> eqE hsub hw htr heqon; move: eqE; rewrite /make_epilogue.
-    t_xrbindP => pinstrs Hpseudo Hswap.
-    have [vm2 Hsem_pis eq_s2_vm2]:= make_pseudo_codeP Hpseudo htr hsub hw heqon.
-    have [sy [vmy] [Hwrite_lvals Hsem /= eq_vm2_vmy]]:= swapableP Hswap Hsem_pis.
-    exists vmy, sy ; split => //.
-    by apply/(eq_onT eq_s2_vm2)/vm_eq_eq_on.
-  Qed.
-
   Local Lemma Hcall : sem_Ind_call p ev Pi_r Pfun.
   Proof.
     move=> s1 scs m s2 lv fn args vargs aout eval_args h1 h2 h3.