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

Jump to bottom

Fix semantics of SHLD_16, SHRD_16, and VPSxLV #520

Merged
merged 2 commits into from
Jul 17, 2023
Merged

Fix semantics of SHLD_16, SHRD_16, and VPSxLV #520

merged 2 commits into from
Jul 17, 2023

Commits on Jul 13, 2023

  1. Fix semantics of SHLD_16 and SHRD_16 

    When the (masked) shift amount is larger than the operand size, the
result is undefined. This is soundly approximated in the semantics by
throwing a type error.

Note that it is not necessary to fix the EasyCrypt model: it is meant to
be correct for safe executions only.
    @vbgl
    vbgl committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    bb02c6d View commit details
    Browse the repository at this point in the history

  2. Relax size constraints of VPSxLV instructions 

    These instructions are available for vector elements of size 16-bit.
    @vbgl
    vbgl committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    66f95ba View commit details
    Browse the repository at this point in the history