From 47cdf1e52f02cd1f5d28ac9ec83dd894a4e732e3 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Fri, 22 Sep 2023 11:56:38 +0200
Subject: [PATCH] x86 lowering: use XOR instead of MOV 0 in division
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

There seem to be no good reason not to use “xor edx, edx” to set the
highest word to zero. The encoding is shorter and flags are obliterated
by the following DIV instruction.
---
 CHANGELOG.md                         | 3 +++
 proofs/compiler/x86_lowering.v       | 2 +-
 proofs/compiler/x86_lowering_proof.v | 4 ++--
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 526efdbc8..0ccadb7b0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -56,6 +56,9 @@
   ([PR #531](https://github.com/jasmin-lang/jasmin/pull/531);
   fixes [#525](https://github.com/jasmin-lang/jasmin/issues/525)).
 
+- Unsigned division on x86 emits a xor instead of “mov 0“
+  ([PR #582](https://github.com/jasmin-lang/jasmin/pull/582)).
+
 # Jasmin 2023.06.1 — 2023-07-31
 
 ## New features
diff --git a/proofs/compiler/x86_lowering.v b/proofs/compiler/x86_lowering.v
index bcf5c9694..baf9382d2 100644
--- a/proofs/compiler/x86_lowering.v
+++ b/proofs/compiler/x86_lowering.v
@@ -504,7 +504,7 @@ Definition lower_cassgn (ii:instr_info) (x: lval) (tg: assgn_tag) (ty: stype) (e
     let i1 :=
       match s with
       | Signed => Copn [:: Lvar c ] tg (Ox86 (CQO sz)) [:: a]
-      | Unsigned => Copn [:: Lvar c ] tg (Ox86 (MOV sz)) [:: Papp1 (Oword_of_int sz) (Pconst 0)]
+      | Unsigned => Copn [:: f ; f ; f ; f ; f ; Lvar c ] tg (Oasm (ExtOp (Oset0 sz))) [::]
       end in
 
     [::MkI ii i1; MkI ii (Copn lv tg op [::Plvar c; a; b]) ]
diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86_lowering_proof.v
index 691ed90ff..a0971b437 100644
--- a/proofs/compiler/x86_lowering_proof.v
+++ b/proofs/compiler/x86_lowering_proof.v
@@ -1406,8 +1406,8 @@ Section PROOF.
               /check_size_16_64 hle1 hle2 /= write_var_eq_type //.
         + by rewrite get_var_eq //= cmp_le_refl orbT.
         + by split => //; apply vmap_eq_except_set; apply multiplicand_in_fv.
-        + by apply: EmkI;  apply: Eopn; rewrite /sem_sopn /exec_sopn /sopn_sem /= truncate_word_u /=
-               /x86_MOV /check_size_8_64 hle2 /= write_var_eq_type.
+        + by apply: EmkI; apply: Eopn; rewrite /sem_sopn /exec_sopn /sopn_sem /=
+                                         /Oset0_instr hle2 /= write_var_eq_type.
         + by rewrite /= get_var_eq /= cmp_le_refl orbT ?wrepr0.
         split => //.
         by apply vmap_eq_except_set; apply multiplicand_in_fv.