Add support for parsing more assembly (#2027)

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
mit-plv · Mar 5, 2025 · bfc6118 · bfc6118
1 parent 76faf79
commit bfc6118
Show file tree

Hide file tree

Showing 5 changed files with 118 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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.