Add support for more assembly #2016
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
force-pushed
the
more-asm
branch
3 times, most recently
from
3601761 to
e6c475f
Compare
JasonGross
commented
Mar 1, 2025
src/Assembly/Syntax.v
Outdated
Comment on lines
18
to
49
| Inductive REG := | ||
| | rax | rcx | rdx | rbx | rsp | rbp | rsi | rdi | r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | ||
| | eax | ecx | edx | ebx | esp | ebp | esi | edi | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | ||
| | ax | cx | dx | bx | sp | bp | si | di | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ||
| (* XMM/YMM/ZMM registers *) | ||
| | zmm0 | zmm1 | zmm2 | zmm3 | zmm4 | zmm5 | zmm6 | zmm7 | zmm8 | zmm9 | zmm10 | zmm11 | zmm12 | zmm13 | zmm14 | zmm15 | zmm16 | zmm17 | zmm18 | zmm19 | zmm20 | zmm21 | zmm22 | zmm23 | zmm24 | zmm25 | zmm26 | zmm27 | zmm28 | zmm29 | zmm30 | zmm31 | ||
| | ymm0 | ymm1 | ymm2 | ymm3 | ymm4 | ymm5 | ymm6 | ymm7 | ymm8 | ymm9 | ymm10 | ymm11 | ymm12 | ymm13 | ymm14 | ymm15 | ||
| | xmm0 | xmm1 | xmm2 | xmm3 | xmm4 | xmm5 | xmm6 | xmm7 | xmm8 | xmm9 | xmm10 | xmm11 | xmm12 | xmm13 | xmm14 | xmm15 | ||
| (* Segment registers *) | ||
| | cs | ds | es | fs | gs | ss | ||
| (* Control registers *) | ||
| | cr0 | cr1 | cr2 | cr3 | cr4 | cr8 | cr9 | cr10 | cr11 | cr12 | cr13 | cr14 | cr15 | ||
| | msw | ||
| | mxcsr | ||
| (* Debug registers *) | ||
| | dr0 | dr1 | dr2 | dr3 | dr4 | dr5 | dr6 | dr7 | dr8 | dr9 | dr10 | dr11 | dr12 | dr13 | dr14 | dr15 | ||
| (* General purpose registers (64/32/16/8 bit) *) | ||
| | rax | rcx | rdx | rbx | rsp | rbp | rsi | rdi | r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | rip | ||
| | eax | ecx | edx | ebx | esp | ebp | esi | edi | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip | ||
| | ax | cx | dx | bx | sp | bp | si | di | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip | ||
| | ah | al | ch | cl | dh | dl | bh | bl | spl | bpl | sil | dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b | ||
| (* MMX registers *) | ||
| | mm0 | mm1 | mm2 | mm3 | mm4 | mm5 | mm6 | mm7 | ||
| (* Special registers *) | ||
| (*| st0 | st1 | st2 | st3 | st4 | st5 | st6 | st7 (* FPU stack registers *)*) | ||
| | k0 | k1 | k2 | k3 | k4 | k5 | k6 | k7 (* AVX-512 mask registers *) | ||
| | gdtr | idtr | ldtr | tr | ||
| | cw | sw | tw | fp_cs | fp_opc | fp_ds | ||
| (* Flags registers *) | ||
| | rflags | ||
| | eflags | ||
| | flags | ||
| . |
There was a problem hiding this comment.
@andres-erbsen Do you have any objection to extending the registers like this?
JasonGross
commented
Mar 1, 2025
src/Assembly/Syntax.v
Outdated
Comment on lines
116
to
190
| | movups (* Move unaligned packed single-precision floating-point values *) | ||
| | movzx | ||
| | mul | ||
| | mulx | ||
| | neg (* Two's complement negation *) | ||
| | nop (* No operation *) | ||
| | not (* Bitwise NOT *) | ||
| | or | ||
| | paddq (* Add packed quadword integers *) | ||
| | pop | ||
| | psubq (* Subtract packed quadword integers *) | ||
| | pshufd (* Shuffle packed doublewords *) | ||
| | pshufw (* Shuffle packed words *) | ||
| | punpcklqdq (* Unpack and interleave low quadwords *) | ||
| | punpckhqdq (* Unpack and interleave high quadwords *) | ||
| | pslld (* Shift packed single-precision floating-point values left *) | ||
| | psrld (* Shift packed single-precision floating-point values right *) | ||
| | pand (* Bitwise AND *) | ||
| | pandn (* Bitwise AND NOT *) | ||
| | por (* Bitwise OR *) | ||
| | pxor (* Bitwise XOR *) | ||
| | psrad (* Shift packed signed integers right arithmetic *) | ||
| | push | ||
| | rcr | ||
| | ret | ||
| | sar | ||
| | sbb | ||
| | rol (* Rotate left *) | ||
| | ror (* Rotate right *) | ||
| | sal (* Shift arithmetic left (functionally equivalent to shl) *) | ||
| | sar (* Shift arithmetic right *) | ||
| | sbb (* Subtract with borrow *) | ||
| | setc | ||
| | sete (* Set byte if equal *) | ||
| | setne (* Set byte if not equal *) | ||
| | seto | ||
| | shl | ||
| | shlx | ||
| | shld | ||
| | shr | ||
| | shrx | ||
| | shrd |
There was a problem hiding this comment.
@andres-erbsen Do you have any opinion on / objection to extending the list of opcodes?
JasonGross
force-pushed
the
more-asm
branch
7 times, most recently
from
dc4ae5d to
a92462b
Compare
I want to be able to handle the output of gcc/clang on our C code. Right now, I have added support for parsing the assembly output. Equivalence checking is still to come.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I want to be able to handle the output of gcc/clang on our C code.
Right now, I have added support for parsing the assembly output. Equivalence checking is still to come.