x86: Add support for VMOVDQA instruction

[dsprenkels]

On avx and avx2, the vmovdqa instruction performs aligned moves from/to memory.
Where vmovdqu will always copy data, no matter the alignment of the address. vmovdqa requires the address to be aligned corresponding to the size of the register where the data is being copied to/from. I.e., for an ymm register, the address needs to be aligned to 32 bytes. If the address is not aligned, this will trigger a general protection fault.

Review suggestions:

• This patch adds support for an instruction that is meant to crash under certain circumstances. Should this be modeled by proofs? (I.e., should EC proofs also prove that the code will never crash, or do they assume that the code will never crash?)

Cc @vbgl

[bgregoir]

Thank for this contribution.
Actually, all memory access already check the alignment.
So it would be great to use this instruction in the generated code.
For the safety checker, yes it should be patched to ensure this. I hope this can be done in a generic way.

[dsprenkels]

I tried but not could not find exactly where the alignment information is analyzed in the jasmin compiler. I can only find info on the alignment of the stack. Do you have any pointers?

[eponier]

In memory_model.v, writeV states that a write succeeds if the memory location is validw and validwP states that this implies that the memory address is aligned.

[dsprenkels]

Would this imply that all memory accesses are always correctly aligned (because that is not true)? Or otherwise, how do we query that from the OCaml side?

---

My current train of thought:

jasminc will happily compile the following code:

export
fn test_vmovdqa(reg u64 p) {
        reg u256 r;

        r = (u256)[p + 16 * 0];
        (u256)[p + 16 * 1] = r;
}

which would result in the following assembly:

        .intel_syntax noprefix
        .text
        .p2align        5
        .globl  _test_vmovdqa
        .globl  test_vmovdqa
_test_vmovdqa:
test_vmovdqa:
        vmovdqu ymm0, ymmword ptr[rdi]
        vmovdqu ymmword ptr[rdi + 16], ymm0
        ret 

Which (after assembly) will crash with a general protection fault when it is run.

So, even though regular array indexing is aligned, not all memory-accesses are guaranteed to be aligned. In the linearization step, we have to figure out whether the assignment that is being linearized is aligned or not. However, I can not figure out how to determine if the alignment is known from an lval, wsize, or pexpr.

It's probably because I don't really have any experience with OCaml/Coq though ^^'

[vbgl]

Asking the safety checker might give you some insight:

Analyzing function test_vmovdqa

*** Possible Safety Violation(s):
"huhu.jazz", line 6 (8-31): aligned pointer p + ((64u) (16 * 1)) u256

[vbgl]

I’ve just try to always emit VMOVDQA instructions instead of VMOVDQU, to see in case it is faster.

I got a nice crash (SIGSEGV) there: https://github.com/formosa-crypto/libjade/blob/c5b9629c3fe6d92db8df12bf0e95d5edd76b0830/src/crypto_kem/kyber/kyber768/amd64/avx2/gen_matrix.jinc#L456, translated to: vmovdqa %xmm5,(%r11,%rdx,2)

where r11 = 0x7ffff78a9920 and rdx = 0xf.

[vbgl]

I think that this PR should be merged: it is a nice addition that let the Jasmin programmers use VMOVDQA explicitly (in place of a plain assignment) when they believe this is good.

There is further work to do in order to allow the compiler to emit this instruction:

• distinguish memory accesses introduced by the compiler that are proved to be aligned from the ones written by the programmer that target the external memory and are (currently) assumed to be aligned
• relax the memory model to allow unaligned accesses and drop the assumption that accesses targeting the external memory are aligned

CI: https://gitlab.com/jasmin-lang/jasmin/-/pipelines/768753230