Skip to content

Commit

Permalink
Add support for more assembly
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@JasonGross
JasonGross committed Mar 5, 2025
1 parent b8de985 commit bebe0b6
Show file tree
Hide file tree
Showing 8 changed files with 274 additions and 139 deletions.
27 changes: 14 additions & 13 deletions src/Assembly/Equivalence.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ From Coq Require Import ZArith.
From Coq Require Import NArith.
Require Import Crypto.Assembly.Syntax.
Require Import Crypto.Assembly.Parse.
Require Import Crypto.Assembly.Equality.
Require Import Crypto.Assembly.Symbolic.
Require Import Crypto.Util.Strings.Parse.Common.
Require Import Crypto.Util.ErrorT.
Expand Down Expand Up @@ -277,8 +278,8 @@ Definition show_annotated_Line : Show AnnotatedLine
end)%string.

Global Instance show_lines_AnnotatedLines : ShowLines AnnotatedLines
:= fun '(ls, ss)
=> let d := dag.eager.force ss.(dag_state) in
:= fun '(ls, sst)
=> let d := dag.eager.force sst.(dag_state) in
List.map (fun l => show_annotated_Line (l, d)) ls.

Fixpoint remove_common_indices {T} (eqb : T -> T -> bool) (xs ys : list T) (start_idx : nat) : list (nat * T) * list T
Expand Down Expand Up @@ -731,11 +732,11 @@ Global Instance show_lines_EquivalenceCheckingError : ShowLines EquivalenceCheck
Global Instance show_EquivalenceCheckingError : Show EquivalenceCheckingError
:= fun err => String.concat String.NewLine (show_lines err).

Definition merge_fresh_symbol {descr:description} : dag.M idx := fun d => merge_node (dag.gensym 64%N d) d.
Definition merge_fresh_symbol {descr:description} (sz : OperationSize) : dag.M idx := fun d => merge_node (dag.gensym sz d) d.
Definition merge_literal {descr:description} (l:Z) : dag.M idx := merge_node ((const l, nil)).

Definition SetRegFresh {opts : symbolic_options_computed_opt} {descr:description} (r : REG) : M idx :=
(idx <- lift_dag merge_fresh_symbol;
(idx <- lift_dag (merge_fresh_symbol (widest_reg_size_of r));
_ <- SetReg r idx;
Symbolic.ret idx).

Expand Down Expand Up @@ -812,13 +813,13 @@ Fixpoint simplify_input_type
end%error.

Definition build_inputarray {descr:description} (len : nat) : dag.M (list idx) :=
List.foldmap (fun _ => merge_fresh_symbol) (List.seq 0 len).
List.foldmap (fun _ => merge_fresh_symbol 64%N) (List.seq 0 len).

Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx + list idx))
:= match types with
| [] => dag.ret []
| None :: tys
=> (idx <- merge_fresh_symbol;
=> (idx <- merge_fresh_symbol 64%N;
rest <- build_inputs tys;
dag.ret (inl idx :: rest))
| Some len :: tys
Expand Down Expand Up @@ -858,12 +859,12 @@ Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {desc
Symbolic.ret (inl addr :: rest))
end%N%x86symex.

Fixpoint dag_gensym_n {descr:description} (n : nat) : dag.M (list symbol) :=
match n with
| O => dag.ret nil
| S n =>
(i <- merge_fresh_symbol;
rest <- dag_gensym_n n;
Fixpoint dag_gensym_ls {descr:description} (ls : list OperationSize) : dag.M (list symbol) :=
match ls with
| nil => dag.ret nil
| sz :: ls =>
(i <- merge_fresh_symbol sz;
rest <- dag_gensym_ls ls;
dag.ret (cons i rest))
end%dagM.

Expand Down Expand Up @@ -1275,7 +1276,7 @@ Definition init_symbolic_state_descr : description := Build_description "init_sy

Definition init_symbolic_state (d : dag) : symbolic_state
:= let _ := init_symbolic_state_descr in
let '(initial_reg_idxs, d) := dag_gensym_n (List.length widest_registers) d in
let '(initial_reg_idxs, d) := dag_gensym_ls (List.map reg_size widest_registers) d in
{|
dag_state := d;
symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs);
Expand Down
156 changes: 87 additions & 69 deletions src/Assembly/EquivalenceProofs.v
View file

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion src/Assembly/Parse.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,8 @@ Definition parse_OpCode_list : list (string * OpCode)
; (".word", dw)
; (".long", dd)
; (".int", dd)
; (".quad", dq)].
; (".quad", dq)
; (".octa", do)].

Definition parse_OpCode : ParserAction OpCode
:= parse_strs_case_insensitive parse_OpCode_list.
Expand Down
12 changes: 6 additions & 6 deletions src/Assembly/Parse/TestAsm.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,13 +65,13 @@ Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O1.example.
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.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O2.example.*)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O3.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_O3.example.*)
Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_Os.example.
Proof. Time native_compute. 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. exact eq_refl. Abort.
Expand All @@ -80,11 +80,11 @@ Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O1.example.
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.
Proof. Time native_compute. exact eq_refl. Abort.
(*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O2.example.*)
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O3.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_O3.example.*)
Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_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_clang_19_1_0_Os.example.*)
27 changes: 14 additions & 13 deletions src/Assembly/Symbolic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3938,15 +3938,15 @@ Global Instance ShowLines_symbolic_state : ShowLines symbolic_state :=
fun X : symbolic_state =>
match X with
| {|
dag_state := ds;
dag_state := dagst;
symbolic_reg_state := rs;
symbolic_flag_state := fs;
symbolic_flag_state := flst;
symbolic_mem_state := ms
|} =>
["(*symbolic_state*) {|";
" dag_state :="] ++ show_lines ds ++ [";";
" dag_state :="] ++ show_lines dagst ++ [";";
(" symbolic_reg_state := " ++ show rs ++ ";")%string;
(" symbolic_flag_state := " ++ show fs ++";")%string;
(" symbolic_flag_state := " ++ show flst ++";")%string;
" symbolic_mem_state :="] ++show_lines ms ++ [";";
"|}"]
end%list%string.
Expand Down Expand Up @@ -4048,11 +4048,11 @@ Definition error_get_reg_of_reg_index ri : symbolic_state -> error
:= error.get_reg (let r := widest_register_of_index ri in
if (reg_index r =? ri)%N
then inr r
else inl ri).
else inl (N.to_nat ri)).

Check failure on line 4051 in src/Assembly/Symbolic.v

View workflow job for this annotation

GitHub Actions / macOS 14 (arm64) 


In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").

Check failure on line 4051 in src/Assembly/Symbolic.v

View workflow job for this annotation

GitHub Actions / debian-sid 


In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").

Check failure on line 4051 in src/Assembly/Symbolic.v

View workflow job for this annotation

GitHub Actions / macOS 13 (x86_64) 


In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").

Check failure on line 4051 in src/Assembly/Symbolic.v

View workflow job for this annotation

GitHub Actions / archlinux 


In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").

Check failure on line 4051 in src/Assembly/Symbolic.v

View workflow job for this annotation

GitHub Actions / alpine-edge 


In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").

Definition GetFlag f : M idx :=
some_or (fun s => get_flag s f) (error.get_flag f).
Definition GetReg64 ri : M idx :=
Definition GetRegFull ri : M idx :=
some_or (fun st => get_reg st ri) (error_get_reg_of_reg_index ri).
Definition Load64 (a : idx) : M idx := some_or (load a) (error.load a).
Definition Remove64 (a : idx) : M idx
Expand All @@ -4071,7 +4071,7 @@ Definition PreserveFlag {T} (f : FLAG) (k : M T) : M T :=
x <- k;
_ <- (fun s => Success (tt, update_flag_with s (fun s => set_flag_internal s f vf)));
ret x.
Definition SetReg64 rn i : M unit :=
Definition SetRegFull rn i : M unit :=
fun s => Success (tt, update_reg_with s (fun s => set_reg s rn i)).
Definition Store64 (a v : idx) : M unit :=
ms <- some_or (store a v) (error.store a v);
Expand All @@ -4092,16 +4092,17 @@ Definition RevealConst (i : idx) : M Z :=

Definition GetReg {opts : symbolic_options_computed_opt} {descr:description} r : M idx :=
let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg r in
v <- GetReg64 rn;
v <- GetRegFull rn;
App ((slice lo sz), [v]).
Definition SetReg {opts : symbolic_options_computed_opt} {descr:description} r (v : idx) : M unit :=
let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg r in
if N.eqb sz 64
then v <- App (slice 0 64, [v]);
SetReg64 rn v (* works even if old value is unspecified *)
else old <- GetReg64 rn;
let widest_size := reg_size (widest_register_of_index rn) in
if (sz =? widest_size)%N
then v <- App (slice 0 widest_size, [v]);
SetRegFull rn v (* works even if old value is unspecified *)
else old <- GetRegFull rn;
v <- App ((set_slice lo sz), [old; v]);
SetReg64 rn v.
SetRegFull rn v.

Class AddressSize := address_size : OperationSize.
Definition Address {opts : symbolic_options_computed_opt} {descr:description} {sa : AddressSize} (a : MEM) : M idx :=
Expand Down
81 changes: 80 additions & 1 deletion src/Assembly/Syntax.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,34 @@ Local Set Implicit Arguments.
Local Set Primitive Projections.

Inductive REG :=
(* 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 *)
.

Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable.
Expand All @@ -35,7 +59,7 @@ Definition REG_eq_dec : forall x y : REG, {x = y} + {x <> y} := eq_dec_of_listab
Definition CONST := Z.
Coercion CONST_of_Z (x : Z) : CONST := x.

Inductive AccessSize := byte | word | dword | qword.
Inductive AccessSize := byte | word | dword | qword | tbyte | xmmword | ymmword | zmmword.

Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Expand All @@ -51,6 +75,10 @@ Coercion bits_of_AccessSize (x : AccessSize) : N
| word => 16
| dword => 32
| qword => 64
| tbyte => 80
| xmmword => 128
| ymmword => 256
| zmmword => 512
end.

Record MEM := { mem_bits_access_size : option AccessSize ; mem_base_reg : option REG ; mem_scale_reg : option (Z * REG) ; mem_base_label : option string ; mem_offset : option Z }.
Expand Down Expand Up @@ -102,6 +130,10 @@ Inductive OpCode :=
| dw
| dd
| dq
| dt
| do
| dy
| dz
| dec
| imul
| inc
Expand Down Expand Up @@ -176,6 +208,10 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
| dd => Some dword
| dq => Some qword
| dw => Some word
| dt => Some tbyte
| do => Some xmmword
| dy => Some ymmword
| dz => Some zmmword
| adc
| adcx
| add
Expand Down Expand Up @@ -276,14 +312,38 @@ Definition Lines := list Line.

Definition reg_size (r : REG) : N :=
match r with
|(xmm0 | xmm1 | xmm2 | xmm3 | xmm4 | xmm5 | xmm6 | xmm7 | xmm8 | xmm9 | xmm10 | xmm11 | xmm12 | xmm13 | xmm14 | xmm15)
=> 128
|(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)
=> 512
|(ymm0 | ymm1 | ymm2 | ymm3 | ymm4 | ymm5 | ymm6 | ymm7 | ymm8 | ymm9 | ymm10 | ymm11 | ymm12 | ymm13 | ymm14 | ymm15)
=> 256
|( rax | rcx | rdx | rbx | rsp | rbp | rsi | rdi | r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | rip)
=> 64
|( eax | ecx | edx | ebx | esp | ebp | esi | edi | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip)
=> 32
|( ax | cx | dx | bx | sp | bp | si | di | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip)
=> 16
|(cs | ds | es | fs | gs | ss)
=> 16
|(ah | al | ch | cl | dh | dl | bh | bl | spl | bpl | sil | dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b)
=> 8
|(cr0 | cr1 | cr2 | cr3 | cr4 | cr8 | cr9 | cr10 | cr11 | cr12 | cr13 | cr14 | cr15)
=> 64
|(dr0 | dr1 | dr2 | dr3 | dr4 | dr5 | dr6 | dr7 | dr8 | dr9 | dr10 | dr11 | dr12 | dr13 | dr14 | dr15)
=> 64
|(mm0 | mm1 | mm2 | mm3 | mm4 | mm5 | mm6 | mm7)
=> 64
|(st0 | st1 | st2 | st3 | st4 | st5 | st6 | st7)
=> 80
|(k0 | k1 | k2 | k3 | k4 | k5 | k6 | k7)
=> 64
|(gdtr | idtr | ldtr | tr)
=> 16
|(cw | sw | tw | fp_cs | fp_opc | fp_ds)
=> 16
| msw => 16
| mxcsr => 32
end.

Definition standalone_operand_size (x : ARG) : option N :=
Expand Down Expand Up @@ -355,6 +415,25 @@ Definition widest_register_of (r : REG) : REG :=
| (r14b | r14w | r14d | r14) => r14
| (r15b | r15w | r15d | r15) => r15
| (ip | eip | rip) => rip
(* | (flags | eflags | rflags) => rflags *)
| (xmm0 | ymm0 | zmm0) => zmm0
| (xmm1 | ymm1 | zmm1) => zmm1
| (xmm2 | ymm2 | zmm2) => zmm2
| (xmm3 | ymm3 | zmm3) => zmm3
| (xmm4 | ymm4 | zmm4) => zmm4
| (xmm5 | ymm5 | zmm5) => zmm5
| (xmm6 | ymm6 | zmm6) => zmm6
| (xmm7 | ymm7 | zmm7) => zmm7
| (xmm8 | ymm8 | zmm8) => zmm8
| (xmm9 | ymm9 | zmm9) => zmm9
| (xmm10 | ymm10 | zmm10) => zmm10
| (xmm11 | ymm11 | zmm11) => zmm11
| (xmm12 | ymm12 | zmm12) => zmm12
| (xmm13 | ymm13 | zmm13) => zmm13
| (xmm14 | ymm14 | zmm14) => zmm14
| (xmm15 | ymm15 | zmm15) => zmm15
| (msw | cr0) => cr0
| _ => r
end.

Definition widest_registers := Eval lazy in List.filter (fun x => REG_beq x (widest_register_of x)) (list_all REG).
Expand Down
Loading

0 comments on commit bebe0b6

Please sign in to comment.