Skip to content

Emit vmovdqa instructions on x86 - #1424

Draft
vbgl wants to merge 1 commit into
mainfrom
vmovdqa
Draft

Emit vmovdqa instructions on x86#1424
vbgl wants to merge 1 commit into
mainfrom
vmovdqa

Conversation

@vbgl

@vbgl vbgl commented Mar 27, 2026

Copy link
Copy Markdown
Member

Description

The compiler emits VMOVDQA instructions instead of VMOVDQU when the underlying memory access is known to be aligned.

Checklist

  • Add a changelog entry in changes if the PR is a user-visible change

Comment thread proofs/compiler/x86_lowering.v
Comment thread proofs/lang/fexpr.v
@vbgl

vbgl commented Mar 30, 2026

Copy link
Copy Markdown
Member Author

I’ve doubts regarding this PR: I think that we are too optimistic about the alignment of arrays that are arguments to export functions.

@eponier

eponier commented Mar 30, 2026

Copy link
Copy Markdown
Contributor

Hm, the compiler should report the expected alignment for the arguments. You think users don't care and don't check that they align their arguments properly, or that it is anyway difficult to ensure for the users (a bit like when we align the stack of export functions ourselves instead of asking the external world to call the export function with the right alignment)?

@vbgl

vbgl commented Mar 31, 2026

Copy link
Copy Markdown
Member Author

I think that even if user care, it is difficult to achieve the desired alignment constraint (from the Jasmin side). For instance, the copy primitive will use aligned array accesses. Here is a typical snippet:

export
fn in_place_computation(reg ptr u8[192] state) -> reg ptr u8[192] {
  reg u256[6] w;

  w = #copy_256(state);
  w = do_stuff(w);
  state = #copy_256(w);
  return state;
}

If such a case, if we want to relax the alignment constraint, we have to give up on the copy operator and write the loops manually.

@vbgl
vbgl force-pushed the vmovdqa branch 2 times, most recently from a67cb36 to c565742 Compare April 13, 2026 16:09
@vbgl
vbgl marked this pull request as draft April 14, 2026 09:21
@vbgl
vbgl marked this pull request as draft April 14, 2026 09:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants