Skip to content

Commit 9f80974

Browse files
JasonGrossJasonGross
committed
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
1 parent 76faf79 commit 9f80974

File tree

5 files changed

+118
-7
lines changed

5 files changed

+118
-7
lines changed

‎src/Assembly/Parse.v

+14-2
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,12 @@ Definition parse_OpCode_list : list (string * OpCode)
140140
:= Eval vm_compute in
141141
List.map
142142
(fun r => (show r, r))
143-
(list_all OpCode).
143+
(list_all OpCode)
144+
++ [(".byte", db)
145+
; (".word", dw)
146+
; (".long", dd)
147+
; (".int", dd)
148+
; (".quad", dq)].
144149

145150
Definition parse_OpCode : ParserAction OpCode
146151
:= parse_strs_case_insensitive parse_OpCode_list.
@@ -234,7 +239,14 @@ Global Instance show_lvl_MEM : ShowLevel MEM
234239
:= fun m
235240
=> (match m.(mem_bits_access_size) with
236241
| Some n
237-
=> 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 *)
242+
=> show_lvl_app (fun 'tt => if n =? 8 then "byte"
243+
else if n =? 16 then "word"
244+
else if n =? 32 then "dword"
245+
else if n =? 64 then "QWORD PTR"
246+
else if n =? 128 then "XMMWORD PTR"
247+
else if n =? 256 then "YMMWORD PTR"
248+
else if n =? 512 then "ZMMWORD PTR"
249+
else "BAD SIZE")%N (* TODO: Fix casing and stuff *)
238250
| None => show_lvl
239251
end)
240252
(fun 'tt

‎src/Assembly/Parse/Examples/fiat_25519_all_clang_19_1_0_Os.v

+1
Original file line numberDiff line numberDiff line change
@@ -896,4 +896,5 @@ Example example : list string := [
896896
"pop r14";
897897
"pop r15";
898898
"pop rbp";
899+
"ret";
899900
""].

‎src/Assembly/Parse/TestAsm.v

+5-5
Original file line numberDiff line numberDiff line change
@@ -59,10 +59,10 @@ Goal parse_correct_on_debug boringssl_nasm_full_mul_p256.example.
5959
Proof. Time native_compute. exact eq_refl. Abort.
6060
(*Redirect "log" Compute parse boringssl_nasm_full_mul_p256.example.*)
6161
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O0.example.
62-
Proof. Time native_compute. Fail exact eq_refl. Abort.
62+
Proof. Time native_compute. exact eq_refl. Abort.
6363
(* Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O0.example. *)
6464
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O1.example.
65-
Proof. Time native_compute. Fail exact eq_refl. Abort.
65+
Proof. Time native_compute. exact eq_refl. Abort.
6666
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O1.example.*)
6767
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O2.example.
6868
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.
7171
Proof. Time native_compute. Fail exact eq_refl. Abort.
7272
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O3.example.*)
7373
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_Os.example.
74-
Proof. Time native_compute. Fail exact eq_refl. Abort.
74+
Proof. Time native_compute. exact eq_refl. Abort.
7575
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_Os.example.*)
7676
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O0.example.
77-
Proof. Time native_compute. Fail exact eq_refl. Abort.
77+
Proof. Time native_compute. exact eq_refl. Abort.
7878
(*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O0.example.*)
7979
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O1.example.
80-
Proof. Time native_compute. Fail exact eq_refl. Abort.
80+
Proof. Time native_compute. exact eq_refl. Abort.
8181
(*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O1.example.*)
8282
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O2.example.
8383
Proof. Time native_compute. Fail exact eq_refl. Abort.

‎src/Assembly/Syntax.v

+64
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,8 @@ Inductive OpCode :=
9393
| clc
9494
| cmovb
9595
| cmovc
96+
| cmove (* Conditional move if equal *)
97+
| cmovne (* Conditional move if not equal *)
9698
| cmovnz
9799
| cmovo
98100
| cmp
@@ -106,21 +108,51 @@ Inductive OpCode :=
106108
| je
107109
| jmp
108110
| lea
111+
| leave (* Function epilogue instruction *)
109112
| mov
113+
| movabs (* Move absolute value into register *)
114+
| movdqa (* Move aligned packed data *)
115+
| movdqu (* Move unaligned packed data *)
116+
| movq (* Move quadword *)
117+
| movd (* Move doubleword *)
118+
| movsx (* Move with sign extension *)
119+
| movups (* Move unaligned packed single-precision floating-point values *)
110120
| movzx
111121
| mul
112122
| mulx
123+
| neg (* Two's complement negation *)
124+
| nop (* No operation *)
125+
| not (* Bitwise NOT *)
113126
| or
127+
| paddq (* Add packed quadword integers *)
114128
| pop
129+
| psubq (* Subtract packed quadword integers *)
130+
| pshufd (* Shuffle packed doublewords *)
131+
| pshufw (* Shuffle packed words *)
132+
| punpcklqdq (* Unpack and interleave low quadwords *)
133+
| punpckhqdq (* Unpack and interleave high quadwords *)
134+
| pslld (* Shift packed single-precision floating-point values left *)
135+
| psrld (* Shift packed single-precision floating-point values right *)
136+
| pand (* Bitwise AND *)
137+
| pandn (* Bitwise AND NOT *)
138+
| por (* Bitwise OR *)
139+
| pxor (* Bitwise XOR *)
140+
| psrad (* Shift packed signed integers right arithmetic *)
115141
| push
116142
| rcr
117143
| ret
144+
| rol (* Rotate left *)
145+
| ror (* Rotate right *)
146+
| sal (* Shift arithmetic left (functionally equivalent to shl) *)
118147
| sar
119148
| sbb
120149
| setc
150+
| sete (* Set byte if equal *)
151+
| setne (* Set byte if not equal *)
121152
| seto
122153
| shl
123154
| shlx
155+
| shld
124156
| shr
125157
| shrx
126158
| shrd
@@ -154,6 +186,8 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
154186
| clc
155187
| cmovb
156188
| cmovc
189+
| cmove
190+
| cmovne
157191
| cmovnz
158192
| cmovo
159193
| cmp
@@ -163,21 +197,51 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
163197
| je
164198
| jmp
165199
| lea
200+
| leave
166201
| mov
202+
| movabs
203+
| movdqa
204+
| movdqu
205+
| movq
206+
| movd
207+
| movsx
208+
| movups
167209
| movzx
168210
| mul
169211
| mulx
212+
| neg
213+
| nop
214+
| not
170215
| or
216+
| paddq
171217
| pop
218+
| psubq
219+
| pshufd
220+
| pshufw
221+
| punpcklqdq
222+
| punpckhqdq
223+
| pslld
224+
| psrld
225+
| pand
226+
| pandn
227+
| por
228+
| pxor
229+
| psrad
172230
| push
173231
| rcr
174232
| ret
233+
| rol
234+
| ror
235+
| sal
175236
| sar
176237
| sbb
177238
| setc
239+
| sete
240+
| setne
178241
| seto
179242
| shl
180243
| shlx
244+
| shld
181245
| shr
182246
| shrx
183247
| shrd

‎src/Assembly/WithBedrock/Semantics.v

+34
Original file line numberDiff line numberDiff line change
@@ -415,6 +415,40 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
415415
| test, _
416416
| xor, _
417417
| xchg, _ => None
418+
(* not yet supported *)
419+
| cmove, _
420+
| cmovne, _
421+
| leave, _
422+
| movabs, _
423+
| movdqa, _
424+
| movdqu, _
425+
| movq, _
426+
| movd, _
427+
| movsx, _
428+
| movups, _
429+
| neg, _
430+
| nop, _
431+
| not, _
432+
| paddq, _
433+
| psubq, _
434+
| pshufd, _
435+
| pshufw, _
436+
| punpcklqdq, _
437+
| punpckhqdq, _
438+
| pslld, _
439+
| psrld, _
440+
| pand, _
441+
| pandn, _
442+
| por, _
443+
| pxor, _
444+
| psrad, _
445+
| rol, _
446+
| ror, _
447+
| sal, _
448+
| sete, _
449+
| setne, _
450+
| shld, _
451+
=> None
418452
end | _ => None end | _ => None end%Z%option.
419453

420454

0 commit comments

Comments
 (0)