Fixes regarding the swap pseudo-operator

CHANGELOG.md

@@ -32,7 +32,8 @@
   On arm-m4, this is compiled using 3 xor instructions.
   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 #691](https://github.com/jasmin-lang/jasmin/pull/691),
+   [PR #816](https://github.com/jasmin-lang/jasmin/pull/816)).
 
 - Support Selective Speculative Load Hardening.
   We now support operators SLH operators as in [Typing High-Speed Cryptography

compiler/safety/success/swap.jazz

@@ -0,0 +1,17 @@
+export
+fn swapw(reg u64 x y) -> reg u64, reg u64 {
+  x = x;
+  y = y;
+  x, y = #swap(x, y);
+  return x, y;
+}
+
+export
+fn swapa(reg u64 x) -> reg u64 {
+  stack u64[1] a b;
+  a[0] = x;
+  b[0] = x;
+  a, b = #swap(a, b);
+  x = a[0];
+  return x;
+}

compiler/safetylib/safetyInterpreter.ml

@@ -1167,6 +1167,10 @@ end = struct
 
     | Sopn.Opseudo_op (Oaddcarry ws) -> mk_addcarry ws es
 
+    | Sopn.Opseudo_op (Oswap ty) ->
+       let x, y = as_seq2 es in
+       [ Some y; Some x]
+
     | Sopn.Oasm (Arch_extra.ExtOp X86_extra.Ox86MOVZX32) ->
       let e = as_seq1 es in
       (* Cast [e], seen as an U32, to an integer, and then back to an U64. *)

compiler/src/pretyping.ml

@@ -1776,6 +1776,13 @@ let rec tt_instr arch_info (env : 'asm Env.env) ((annot,pi) : S.pinstr) : 'asm E
         | _ ->
           rs_tyerror ~loc:(L.loc pi)
             (string_error "a pair of destination is expected for swap") in
+      let () = match ty with
+        | Arr _ -> ()
+        | Bty (U ws) when ws <= U64 -> ()
+        | Bty ty ->
+           rs_tyerror ~loc:(L.loc pi)
+             (string_error "the swap primitive is not available at type %a" PrintCommon.pp_btype ty)
+      in
       let es = tt_exprs_cast arch_info.pd env (L.loc pi) args [ty; ty] in
       let p = Sopn.Opseudo_op (Oswap Type.Coq_sbool) in  (* The type is fixed latter *)
       env, [mk_i (P.Copn(lvs, AT_keep, p, es))]

compiler/tests/fail/x86-64/swap128.jazz

@@ -0,0 +1,5 @@
+export
+fn main(reg u128 x y) -> reg u128, reg u128 {
+  y, x = #swap(x, y);
+  return y, x;
+}

compiler/tests/fail/x86-64/swap_bool.jazz

@@ -0,0 +1,9 @@
+export
+fn main(reg u8 a) -> reg u8 {
+  reg bool b c;
+  b = a != 0;
+  c = a <s 0;
+  b, c = #swap(b, c);
+  a = a if b;
+  return a;
+}

compiler/tests/fail/x86-64/swap_int.jazz

@@ -0,0 +1,9 @@
+export
+fn main(reg u8 a) -> reg u8 {
+  inline int i j;
+  i = 0;
+  j = 1;
+  i, j = #swap(i, j);
+  a = a if i < j;
+  return a;
+}