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

Add support for translation of AVX2 code #1000

Open
wants to merge 27 commits into
base: cryptoline
Choose a base branch
from
Open

Add support for translation of AVX2 code #1000

wants to merge 27 commits into from

Conversation

MQuaresma
Copy link
Collaborator

This pull request adds support for translating (annotated) AVX2 code to Cryptoline which includes:

  • reasoning about vector registers as lists of scalar values using the UnPack abstract predficate
  • support for translating several AVX2 instructions (signed and unsigned)
  • simplification of CFG to remove redundant casting operations
  • support for lists of lvals in Cryptoline translation

Support for the following AVX2 instructions was added:

  • VPMULL, VPMULH, VPSRA, VPBROADCAST, VPADD, VPSUB

@MQuaresma MQuaresma requested a review from lyonel2017 December 30, 2024 19:05
MQuaresma added 26 commits January 9, 2025 16:19
@MQuaresma
WIP: vector unfolding in predicates
01b88b4
@MQuaresma
Add UnPack predicate to CAS
781ef3a
@MQuaresma
Fix CFG simplification
785ad71
@MQuaresma
Fix unused lval search
138269c
@MQuaresma
Fix naming overload in unfold_vectors
d8650ee
@MQuaresma
Refactor CFG simplification to ignore output vars when checking for u…
5f41b02 
…nused lvals
@MQuaresma
Fix vector unfolding in post conditions to use correct ghost
473834c
@MQuaresma
Simplify CFG simplification
e2af4ea
@MQuaresma
Add support for lists as lvals
e211ec6
@MQuaresma
Add unsafe versions of VPADD and VPSUB, add translation for VPSRA
c5baf9d
@MQuaresma
Fix infinite recursion bug in equality check of types due to incomple…
4875ad0 
…te pattern matching
@MQuaresma
Support for VPBROADCAST, (WIP) support for VPSRA
209ea1b
@MQuaresma
Support for ssplit/split and improved CFG simplification when using c…
ee76221 
…asts
@MQuaresma
Unfold vector ghosts in predicates of called functions
b800d4e
@MQuaresma
(WIP) Add signed translations for VPSRA/VPMULH/VPMULL/VPSUB; CFG simp…
2be9290 
…lification for split/mul operations
@MQuaresma
Add eqsmod abstract range predicate
4324352
@MQuaresma
Fix translation of VPSRA and add vector variant of sra in cryptoline
0b781d7
@MQuaresma
Fix translation of vector instructions
9176f3f
@MQuaresma
Add signed versions of AVX2 instructions and fix previous translations
185e79e
@MQuaresma
Add formals from function calls to formals list
3ad0755
@MQuaresma
Merge with upstream/cryptoline branch
0ceb012
@MQuaresma
Return lvals as formals
5737388
@MQuaresma
Fix translation of VPBROADCAST
7340fa9
@MQuaresma
Use UID to find unfolded vector formals instead of flag when dealing …
cdd0c5e 
…with output variables
@MQuaresma
Return lists of lvals to formals
81dce95
@MQuaresma
Set return variables in CFG simplifcation based on post condition
0665cf8
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lyonel2017 lyonel2017 Awaiting requested review from lyonel2017

Assignees
No one assigned
Labels
cryptoline
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@MQuaresma @eponier