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

Add support for parsing more assembly #2027

Merged
merged 1 commit into from
Mar 5, 2025
Merged

Add support for parsing more assembly #2027

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions src/Assembly/Parse.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,12 @@ Definition parse_OpCode_list : list (string * OpCode)
:= Eval vm_compute in
List.map
(fun r => (show r, r))
(list_all OpCode).
(list_all OpCode)
++ [(".byte", db)
; (".word", dw)
; (".long", dd)
; (".int", dd)
; (".quad", dq)].

Definition parse_OpCode : ParserAction OpCode
:= parse_strs_case_insensitive parse_OpCode_list.
Expand Down Expand Up @@ -234,7 +239,14 @@ Global Instance show_lvl_MEM : ShowLevel MEM
:= fun m
=> (match m.(mem_bits_access_size) with
| Some n
=> show_lvl_app (fun 'tt => if n =? 8 then "byte" else if n =? 64 then "QWORD PTR" else "BAD SIZE")%N (* TODO: Fix casing and stuff *)
=> show_lvl_app (fun 'tt => if n =? 8 then "byte"
else if n =? 16 then "word"
else if n =? 32 then "dword"
else if n =? 64 then "QWORD PTR"
else if n =? 128 then "XMMWORD PTR"
else if n =? 256 then "YMMWORD PTR"
else if n =? 512 then "ZMMWORD PTR"
else "BAD SIZE")%N (* TODO: Fix casing and stuff *)
| None => show_lvl
end)
(fun 'tt
Expand Down
1 change: 1 addition & 0 deletions src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -896,4 +896,5 @@ Example example : list string := [
"pop r14";
"pop r15";
"pop rbp";
"ret";
""].
10 changes: 5 additions & 5 deletions src/Assembly/Parse/TestAsm.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,10 +59,10 @@ Goal parse_correct_on_debug boringssl_nasm_full_mul_p256.example.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse boringssl_nasm_full_mul_p256.example.*)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O0.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Proof. Time native_compute. exact eq_refl. Abort.
(* Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O0.example. *)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O1.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O1.example.*)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O2.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Expand All @@ -71,13 +71,13 @@ Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O3.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O3.example.*)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_Os.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_Os.example.*)
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O0.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O0.example.*)
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O1.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O1.example.*)
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O2.example.
Proof. Time native_compute. Fail exact eq_refl. Abort.
Expand Down
64 changes: 64 additions & 0 deletions src/Assembly/Syntax.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,8 @@ Inductive OpCode :=
| clc
| cmovb
| cmovc
| cmove (* Conditional move if equal *)
| cmovne (* Conditional move if not equal *)
| cmovnz
| cmovo
| cmp
Expand All @@ -106,21 +108,51 @@ Inductive OpCode :=
| je
| jmp
| lea
| leave (* Function epilogue instruction *)
| mov
| movabs (* Move absolute value into register *)
| movdqa (* Move aligned packed data *)
| movdqu (* Move unaligned packed data *)
| movq (* Move quadword *)
| movd (* Move doubleword *)
| movsx (* Move with sign extension *)
| 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
| rol (* Rotate left *)
| ror (* Rotate right *)
| sal (* Shift arithmetic left (functionally equivalent to shl) *)
| sar
| sbb
| setc
| sete (* Set byte if equal *)
| setne (* Set byte if not equal *)
| seto
| shl
| shlx
| shld
| shr
| shrx
| shrd
Expand Down Expand Up @@ -154,6 +186,8 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
| clc
| cmovb
| cmovc
| cmove
| cmovne
| cmovnz
| cmovo
| cmp
Expand All @@ -163,21 +197,51 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
| je
| jmp
| lea
| leave
| mov
| movabs
| movdqa
| movdqu
| movq
| movd
| movsx
| movups
| movzx
| mul
| mulx
| neg
| nop
| not
| or
| paddq
| pop
| psubq
| pshufd
| pshufw
| punpcklqdq
| punpckhqdq
| pslld
| psrld
| pand
| pandn
| por
| pxor
| psrad
| push
| rcr
| ret
| rol
| ror
| sal
| sar
| sbb
| setc
| sete
| setne
| seto
| shl
| shlx
| shld
| shr
| shrx
| shrd
Expand Down
34 changes: 34 additions & 0 deletions src/Assembly/WithBedrock/Semantics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,6 +415,40 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
| test, _
| xor, _
| xchg, _ => None
(* not yet supported *)
| cmove, _
| cmovne, _
| leave, _
| movabs, _
| movdqa, _
| movdqu, _
| movq, _
| movd, _
| movsx, _
| movups, _
| neg, _
| nop, _
| not, _
| paddq, _
| psubq, _
| pshufd, _
| pshufw, _
| punpcklqdq, _
| punpckhqdq, _
| pslld, _
| psrld, _
| pand, _
| pandn, _
| por, _
| pxor, _
| psrad, _
| rol, _
| ror, _
| sal, _
| sete, _
| setne, _
| shld, _
=> None
end | _ => None end | _ => None end%Z%option.


Expand Down
Loading