Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix a bug on the handling of #VPEXTR_8 and #VPEXTR_16 #394

Merged
merged 3 commits into from
Mar 22, 2023
Merged

fix a bug on the handling of #VPEXTR_8 and #VPEXTR_16 #394

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1c6f00e
fix a bug on the handling of #VPEXTR_8 and #VPEXTR_16
jba-uminho Mar 19, 2023
a57a29d
fix semantics of VPEXTR and VPINSR
jba-uminho Mar 21, 2023
dc57075
add CHANGELOG entry
jba-uminho Mar 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix semantics of VPEXTR and VPINSR
  • Loading branch information
@jba-uminho
jba-uminho committed Mar 21, 2023
commit a57a29d94298c40d14ddf131333079b027c8f1df
2 changes: 2 additions & 0 deletions proofs/compiler/x86_instr_decl.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -716,10 +716,12 @@ Definition x86_VPMULHRS ve sz v1 v2 :=
(* ---------------------------------------------------------------- *)
Definition x86_VPEXTR (ve: wsize) (v: u128) (i: u8) : ex_tpl (w_ty ve) :=
Let _ := check_size_8_64 ve in
let i := wand i (x86_nelem_mask ve U128) in
ok (nth (0%R: word ve) (split_vec ve v) (Z.to_nat (wunsigned i))).

(* ---------------------------------------------------------------- *)
Definition x86_VPINSR (ve: velem) (v1: u128) (v2: word ve) (i: u8) : ex_tpl (w_ty U128) :=
let i := wand i (x86_nelem_mask ve U128) in
ok (wpinsr v1 v2 i).

Arguments x86_VPINSR : clear implicits.
Expand Down
3 changes: 3 additions & 0 deletions proofs/lang/word.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -428,6 +428,9 @@ Definition x86_shift_mask (s:wsize) : u8 :=
| U256 => wrepr U8 255
end%Z.

Definition x86_nelem_mask (sze szc:wsize) : u8 :=
wrepr U8 (2 ^ (wsize_log2 szc - wsize_log2 sze) - 1).

Definition wbit_n sz (w:word sz) (n:nat) : bool :=
wbit (wunsigned w) n.

Expand Down