From 9f80974c902c5a083cefb42fe3f63cf1166f2348 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Mar 2025 01:38:51 -0800 Subject: [PATCH] Add support for parsing more assembly 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. Also still to come is parsing data declarations --- src/Assembly/Parse.v | 16 ++++- .../Examples/fiat_25519_all_clang_19_1_0_Os.v | 1 + src/Assembly/Parse/TestAsm.v | 10 +-- src/Assembly/Syntax.v | 64 +++++++++++++++++++ src/Assembly/WithBedrock/Semantics.v | 34 ++++++++++ 5 files changed, 118 insertions(+), 7 deletions(-) diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v index 486c886602..4bf046fd20 100644 --- a/src/Assembly/Parse.v +++ b/src/Assembly/Parse.v @@ -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. @@ -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 diff --git a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v index 770d195a6e..dcf2a38203 100644 --- a/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v +++ b/src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v @@ -896,4 +896,5 @@ Example example : list string := [ "pop r14"; "pop r15"; "pop rbp"; +"ret"; ""]. diff --git a/src/Assembly/Parse/TestAsm.v b/src/Assembly/Parse/TestAsm.v index 89e193b1b4..86dcddbdb9 100644 --- a/src/Assembly/Parse/TestAsm.v +++ b/src/Assembly/Parse/TestAsm.v @@ -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. @@ -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. diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v index 29638b22a2..73dc6d3afc 100644 --- a/src/Assembly/Syntax.v +++ b/src/Assembly/Syntax.v @@ -93,6 +93,8 @@ Inductive OpCode := | clc | cmovb | cmovc +| cmove (* Conditional move if equal *) +| cmovne (* Conditional move if not equal *) | cmovnz | cmovo | cmp @@ -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 @@ -154,6 +186,8 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize := | clc | cmovb | cmovc + | cmove + | cmovne | cmovnz | cmovo | cmp @@ -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 diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v index 695e4aa6c2..23cd75aa9d 100644 --- a/src/Assembly/WithBedrock/Semantics.v +++ b/src/Assembly/WithBedrock/Semantics.v @@ -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.