Emit vmovdqa instructions on x86

changes/03-other/1424-vmovdqa.md

@@ -0,0 +1,3 @@
+- Emit `vmovdqa` instructions on x86 for memory accesses introduced by the
+  compiler
+  ([PR 1424](https://github.com/jasmin-lang/jasmin/pull/1424)).

proofs/compiler/x86_extra.v

@@ -18,6 +18,8 @@ Require Import
 Require Export arch_extra.
 Import sopn.
 
+Notation VMOVDQ al := (if al is Aligned then VMOVDQA else VMOVDQU).
+
 Module E.
 
 Definition pass_name := "asmgen"%string.

proofs/compiler/x86_lowering.v

@@ -226,6 +226,17 @@ Definition check_signed_range (m: option wsize) sz' (n: Z) : bool :=
       if h <=? z then z <? -h else false)%Z
   else false.
 
+Definition classify_pget ty e x (al: aligned) sz v : lower_cassgn_t :=
+    if (sz ≤ U64)%CMP
+    then LowerMov (if is_var_in_memory v then is_lval_in_memory x else false)
+    else if ty is aword szo
+    then if (U128 ≤ szo)%CMP then
+           let al := min_aligned al (aligned_of_lval x) in
+           LowerCopn (Ox86 (VMOVDQ al szo)) [:: e ]
+    else if (U32 ≤ szo)%CMP then LowerCopn (Ox86 (MOVV szo)) [:: e ]
+    else LowerAssgn
+    else LowerAssgn.
+
 (* x =(ty) e *)
 Definition lower_cassgn_classify ty e x : lower_cassgn_t :=
   let chk (b: bool) r := if b then r else LowerAssgn in
@@ -234,19 +245,13 @@ Definition lower_cassgn_classify ty e x : lower_cassgn_t :=
   let k16 sz := kb ((U16 ≤ sz) && (sz ≤ U64))%CMP sz in
   let k32 sz := kb ((U32 ≤ sz) && (sz ≤ U64))%CMP sz in
   match e with
-  | Pget _ _ sz {| gv := v |} _
+  | Pget al _ sz {| gv := v |} _ => classify_pget ty e x al sz v
   | Pvar {| gv := ({| v_var := {| vtype := aword sz |} |} as v) |} =>
-    if (sz ≤ U64)%CMP
-    then LowerMov (if is_var_in_memory v then is_lval_in_memory x else false)
-    else if ty is aword szo
-    then if (U128 ≤ szo)%CMP then LowerCopn (Ox86 (VMOVDQU szo)) [:: e ]
-    else if (U32 ≤ szo)%CMP then LowerCopn (Ox86 (MOVV szo)) [:: e ]
-    else LowerAssgn
-    else LowerAssgn
-  | Pload _ sz _ =>
+      classify_pget ty e x Aligned sz v
+  | Pload al sz _ =>
       if (sz ≤ U64)%CMP
       then LowerMov (is_lval_in_memory x)
-      else kb true sz (LowerCopn (Ox86 (VMOVDQU sz)) [:: e ])
+      else kb true sz (LowerCopn (Ox86 (VMOVDQ al sz)) [:: e ])
 
   | Papp1 (Oword_of_int sz) (Pconst z) =>
       if ty is aword sz' then

proofs/compiler/x86_lowering_proof.v

@@ -501,6 +501,14 @@ Section PROOF.
     lia.
   Qed.
 
+  Lemma sopn_sem_VMOVDQ al sz :
+    sopn_sem (Ox86 (VMOVDQ al sz)) =
+      assert (U128 ≤ sz)%CMP ErrType >> ok (sopn_sem_ (Ox86 (VMOVDQ al sz))).
+  Proof. by case: al; rewrite /sopn_sem /= /size_128_256 wsize_ge_U256 andbT. Qed.
+
+  Lemma nle_u64_u128_le sz : (U128 ≤ sz)%CMP = ~~ (sz ≤ U64)%CMP.
+  Proof. by case: sz. Qed.
+
   Lemma lower_cassgn_classifyP e l s s' v ty v' (Hs: sem_pexpr true gd s e = ok v)
       (Hv': truncate_val (eval_atype ty) v = ok v')
       (Hw: write_lval true gd l v' s = ok s'):
@@ -572,15 +580,16 @@ Section PROOF.
       case: (write_lval_undef Hw hty) => w ? {hty}; subst v'.
       case/truncate_valI: Hv' => s'' [] w'' [] hty ok_w ?; subst.
       case: Hs => ?; subst s''.
+      rewrite /classify_pget.
       case: ifP.
       * move => h; eexists; first reflexivity.
         split; first exact: (cmp_le_trans hle (cmp_le_trans Hs' h)).
         by eexists _, _; split; last reflexivity.
       move => hsz_le_64.
       case: ty hty => //= _ [->].
       case: ifP => h128_le_sz''.
-      * rewrite /= ok_v /exec_sopn /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
-        by rewrite ok_w /x86_VMOVDQ /size_128_256 h128_le_sz'' wsize_ge_U256.
+      * rewrite /= ok_v /exec_sopn sopn_sem_VMOVDQ h128_le_sz'' /=.
+        by case: aligned_of_lval; rewrite /sopn_sem_ /= /semi_to_atype computational_eq_refl ok_w.
       case: ifP => // hsz''.
       rewrite /= ok_v /exec_sopn /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
       rewrite /x86_MOVX /size_32_64 hsz'' ok_w.
@@ -589,6 +598,7 @@ Section PROOF.
     + rewrite /=; apply: rbindP => - [] // len a /= ok_a; t_xrbindP => i j ok_j ok_i w ok_w ?; subst v.
       case: x ok_a => x xs ok_a.
       case/truncate_valE: Hv' => sz' [] w' [] hty ok_w' ?; subst v'.
+      rewrite /classify_pget.
       case: ifP => hsz.
       * rewrite hty.
         eexists; first reflexivity.
@@ -597,8 +607,9 @@ Section PROOF.
         by eauto.
       case: ty hty => //= _ [->].
       case: ifP => h128_le_sz'.
-      * rewrite /= ok_a ok_j /= ok_i /= ok_w /exec_sopn /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
-        by rewrite /x86_VMOVDQ /size_128_256 h128_le_sz' ok_w' wsize_ge_U256.
+      * rewrite /= ok_a ok_j /= ok_i /= ok_w /exec_sopn sopn_sem_VMOVDQ h128_le_sz' /=.
+        case: min_aligned;
+        by rewrite /sopn_sem_ /= /semi_to_atype computational_eq_refl ok_w'.
       case: ifP => // hsz''.
       rewrite /= ok_a ok_j /= ok_i /= ok_w /exec_sopn /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
       rewrite /x86_MOVX /size_32_64 hsz'' ok_w'.
@@ -613,11 +624,9 @@ Section PROOF.
         by eauto.
       case hc: convertible => //.
       move: hty; rewrite -(convertible_eval_atype hc) => -[?]; subst sz'.
-      rewrite /= he /= hz /= hload /exec_sopn /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
-      rewrite /x86_VMOVDQ truncate_word_u /=.
-      set b := (X in assert X).
-      suff -> : b; first by rewrite zero_extend_u.
-      by subst b; move: hsz; clear; case: sz.
+      rewrite /= he /= hz /= hload /exec_sopn sopn_sem_VMOVDQ nle_u64_u128_le hsz /=.
+      case: al {hload};
+      by rewrite /sopn_sem_ /= /semi_to_atype computational_eq_refl truncate_word_u zero_extend_u.
     + case: o => //.
       (* Oword_of_int *)
       - move => sz; case: e => // z [?]; subst v.

proofs/compiler/x86_params.v

@@ -81,11 +81,10 @@ Definition x86_free_stack_frame (rspi: var_i) (tmp: option var_i) (sz: Z) :=
   let p := Fapp2 (Oadd (Op_w Uptr)) (Fvar rspi) (fconst Uptr sz) in
   [:: ([:: LLvar rspi ], Ox86 (LEA Uptr), [:: Rexpr p ])].
 
-(* TODO: consider using VMOVDQA when the address is known to be aligned *)
 Definition x86_lassign (x: lexpr) (ws: wsize) (e: rexpr) :=
   let op := if (ws <= U64)%CMP
             then MOV ws
-            else VMOVDQU ws
+            else VMOVDQ (aligned_of_lexpr x) ws
   in ([:: x ], Ox86 op, [:: e ]).
 
 Definition x86_set_up_sp_register

proofs/compiler/x86_params_proof.v

@@ -208,9 +208,10 @@ Lemma x86_lassign_correct s x ws e (w : word ws) s':
 Proof.
   move=> /=; t_xrbindP => v -> /= hv hwr.
   rewrite /exec_sopn /=.
-  case: ifP => /= h; rewrite hv /= /sopn_sem /sopn_sem_ /= /semi_to_atype computational_eq_refl.
-  + by rewrite /x86_MOV /= /size_8_64 h /= hwr.
-  by rewrite /x86_VMOVDQ (wsize_nle_u64_size_128_256 h) /= hwr.
+  case: ifP => /= h.
+  2: rewrite sopn_sem_VMOVDQ nle_u64_u128_le h /=; case: aligned_of_lexpr.
+  1: rewrite /sopn_sem /sopn_sem_ /= /size_8_64 h.
+  all: by rewrite /= hv /= /sopn_sem_ /= /semi_to_atype computational_eq_refl /= hwr.
 Qed.
 
 Lemma x86_lmove_correct : lmove_correct x86_liparams.

proofs/lang/expr.v

@@ -321,6 +321,15 @@ Coercion Lvar : var_i >-> lval.
 
 Notation lvals := (seq lval).
 
+Definition aligned_of_lval (x: lval) : aligned :=
+  match x with
+  | Lnone _ _
+  | Lvar _ => Aligned
+  | Lmem al _ _ _
+  | Laset al _ _ _ _ => al
+  | Lasub _ _ _ _ _ => Unaligned (* dummy value *)
+  end.
+
 Definition get_pvar (e: pexpr) : exec var :=
   if e is Pvar {| gv := x ; gs := Slocal |} then ok (v_var x) else type_error.
 

proofs/lang/fexpr.v

@@ -33,6 +33,9 @@ Variant lexpr :=
 Notation rexprs := (seq rexpr).
 Notation lexprs := (seq lexpr).
 
+Definition aligned_of_lexpr (x: lexpr) : aligned :=
+  if x is Store al _ _ then al else Aligned.
+
 (* -------------------------------------------------------------------------- *)
 Fixpoint fexpr_of_pexpr (e: pexpr) : option fexpr :=
   match e with

proofs/lang/memory_model.v

@@ -162,6 +162,9 @@ HB.instance Definition _ := hasDecEq.Build aligned aligned_eqb_OK.
 Definition aligned_le (x y: aligned) : bool :=
   (x == Unaligned) || (y == Aligned).
 
+Definition min_aligned (a b: aligned) : aligned :=
+  if a is Aligned then b else a.
+
 (* -------------------------------------------------------------------- *)
 Module Export CoreMem.
 Section CoreMem.