FIX LZCNT semantics to handle the size parameter

jasmin-lang · Jul 12, 2023 · 3faab79 · 3faab79
1 parent 4fae756
commit 3faab79
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -23,6 +23,10 @@
 
 ## Bug fixes
 
+- Handle the size parameter in LZCNT semantic
+  ([PR #516](https://github.com/jasmin-lang/jasmin/pull/516);
+  fixes [#515](https://github.com/jasmin-lang/jasmin/issues/515)).
+
 - Type-checking rejects wrongly casted primitive operators
   ([PR #489](https://github.com/jasmin-lang/jasmin/pull/488);
   fixes [#69](https://github.com/jasmin-lang/jasmin/issues/69)).

diff --git a/proofs/compiler/x86_instr_decl.v b/proofs/compiler/x86_instr_decl.v
@@ -500,15 +500,15 @@ Definition x86_DEC sz (w: word sz) : ex_tpl (b4w_ty sz) :=
     (wsigned w - 1)%Z).
 
 
-Fixpoint leading_zero_aux (n: Z) (k : nat) :=
-  if (n <? 2^(64 - k))%Z then k 
+Fixpoint leading_zero_aux (n: Z) (k : nat) (sz : nat) :=
+  if (n <? 2^(sz - k))%Z then k 
   else match k with 
   | 0 => 0
-  | S k' => leading_zero_aux n k'
+  | S k' => leading_zero_aux n k' sz
   end.
 
 Definition leading_zero sz (w: word sz) : word sz := 
-  wrepr sz (leading_zero_aux (wunsigned w) sz).
+  wrepr sz (leading_zero_aux (wunsigned w) sz sz).
 
 Definition x86_LZCNT sz (w: word sz) : ex_tpl (b5w_ty sz) := 
    Let _ := check_size_16_64 sz in