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 more assembly #2016

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Add support for more assembly #2016

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b1d8cb9
Parse label-based addressing
JasonGross Mar 1, 2025
b8de985
Add rip, eip, ip registers
JasonGross Mar 1, 2025
bebe0b6
Add support for more assembly
JasonGross Mar 1, 2025
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
27 changes: 14 additions & 13 deletions src/Assembly/Equivalence.v
View file
Open in desktop
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
170 changes: 97 additions & 73 deletions src/Assembly/EquivalenceProofs.v
View file
Open in desktop

Large diffs are not rendered by default.

123 changes: 105 additions & 18 deletions src/Assembly/Parse.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,16 +80,26 @@ Definition parse_label : ParserAction string
(fun '(char, ls) => string_of_list_ascii (char :: ls))
(([a-zA-Z] || parse_any_ascii "._?$") ;;
(([a-zA-Z] || parse_any_ascii "0123456789_$#@~.?")* )).
Definition parse_non_access_size_label : ParserAction string
:= parse_lookahead_not parse_AccessSize ;;R parse_label.

Definition parse_MEM : ParserAction MEM
:= parse_map
(fun '(access_size, (br (*base reg*), sr (*scale reg, including z *), offset, base_label))
=> {| mem_bits_access_size := access_size:option AccessSize
; mem_base_reg := br:option REG
; mem_base_label := base_label
; mem_scale_reg := sr:option (Z * REG)
; mem_offset := offset:option Z |})
:= parse_option_list_map
(fun '(access_size, (constant_location_label, (br (*base reg*), sr (*scale reg, including z *), offset, base_label)))
=> match base_label, constant_location_label with
| Some _, Some _ => (* invalid? *) None
| Some _ as lbl, None
| None, Some _ as lbl
| None, None as lbl =>
Some
{| mem_bits_access_size := access_size:option AccessSize
; mem_base_reg := br:option REG
; mem_base_label := lbl
; mem_scale_reg := sr:option (Z * REG)
; mem_offset := offset:option Z |}
end)
(((strip_whitespace_after parse_AccessSize)?) ;;
(parse_non_access_size_label?) ;;
(parse_option_list_map
(fun '(offset, vars)
=> (vars <-- List.map (fun '(c, (v, e), vs) => match vs, e with [], 1%Z => Some (c, v) | _, _ => None end) vars;
Expand Down Expand Up @@ -145,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 Expand Up @@ -267,11 +278,21 @@ Global Instance show_lvl_MEM : ShowLevel MEM
then "0x08 * " ++ Decimal.show_Z (offset / 8)
else Hex.show_Z offset)
end%Z) in
"[" ++ match m.(mem_base_label) with
| None => reg_part ++ offset_part
| Some l => "((" ++ l ++ offset_part ++ "))"
end
++ "]").
match m.(mem_base_label), m.(mem_base_reg), m.(mem_offset), m.(mem_scale_reg) with
| Some lbl, Some rip, None, None => lbl ++ "[" ++ reg_part ++ offset_part ++ "]"
| Some lbl, _, _, _ => let l_offset := lbl ++ offset_part in
"[" ++
(if reg_part =? ""
then "((" ++ l_offset ++ "))"
else reg_part ++ " + " ++ l_offset)
++ "]"
| None, _, _, _ =>
"[" ++
(if reg_part =? ""
then "((" ++ offset_part ++ "))"
else reg_part ++ offset_part)
++ "]"
end).
Global Instance show_MEM : Show MEM := show_lvl_MEM.

Global Instance show_lvl_JUMP_LABEL : ShowLevel JUMP_LABEL
Expand Down Expand Up @@ -490,20 +511,86 @@ Definition find_globals (ls : Lines) : list string
end)
ls.

Fixpoint split_code_to_functions' (globals : list string) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
Definition find_labels (ls : Lines) : list string
:= Option.List.map
(fun l => match l.(rawline) with
| LABEL name => Some name
| _ => None
end)
ls.

Fixpoint split_code_to_functions' (label_is_function : string -> bool) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
:= match ls with
| [] => ([], [])
| l :: ls
=> let '(prefix, rest) := split_code_to_functions' globals ls in
=> let '(prefix, rest) := split_code_to_functions' label_is_function ls in
let default := (l :: prefix, rest) in
match l.(rawline) with
| LABEL name => if List.existsb (fun n => name =? n)%string globals
| LABEL name => if label_is_function name
then ([], (name, l::prefix) :: rest)
else default
| _ => default
end
end.

Definition split_code_to_functions (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
Definition string_matches_loose (allow_prefix : bool) (allow_suffix : bool) (longer_string shorter_string : string) : bool
:= match allow_prefix, allow_suffix with
| false, false => shorter_string =? longer_string
| true, false => String.endswith shorter_string longer_string
| false, true => String.startswith shorter_string longer_string
| true, true => String.is_substring shorter_string longer_string
end.
Definition split_code_to_listed_functions {allow_prefix allow_suffix : bool} (functions : list string) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
:= split_code_to_functions' (fun name => List.existsb (fun f => string_matches_loose allow_prefix allow_suffix f name)%string functions) ls.
Definition split_code_to_global_functions (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
:= let globals := find_globals ls in
split_code_to_functions' globals ls.
split_code_to_listed_functions (allow_prefix:=false) (allow_suffix:=false) globals ls.
Definition split_code_at_labels (ls : Lines) : Lines (* prefix *) * list (string (* label name *) * Lines)
:= let labels := find_labels ls in
split_code_to_listed_functions (allow_prefix:=false) (allow_suffix:=false) labels ls.

Fixpoint get_initial_data (ls : Lines) : list (AccessSize * list Z)
:= let get_arg_consts args :=
Option.List.lift
(List.map (fun arg => match arg with
| const c => Some c
| _ => None
end)
args) in
match ls with
| [] => []
| l :: ls
=> match l.(rawline) with
| INSTR instr =>
match accesssize_of_declaration instr.(op) with
| None => []
| Some size =>
let csts := get_arg_consts instr.(args) in
match csts with
| Some csts => (size, csts) :: get_initial_data ls
| None => []
end
end
| LABEL _
| EMPTY
| GLOBAL _
| DEFAULT_REL
=> get_initial_data ls
| SECTION _
| ALIGN _
=> []
end
end.

Definition get_labeled_data (ls : Lines) : list (string * list (AccessSize * list Z)) :=
let '(_, labeled_data) := split_code_at_labels ls in
let labeled_data := List.map (fun '(lbl, lines) => (lbl, get_initial_data lines)) labeled_data in
let labeled_data := List.filter (fun '(_, data) => match data with nil => false | _ => true end) labeled_data in
labeled_data.

Definition parse_assembly_options (ls : Lines) : assembly_program_options
:= {| default_rel := Option.is_Some (List.find (fun l => match l.(rawline) with
| DEFAULT_REL => true
| _ => false
end) ls)
|}.
12 changes: 6 additions & 6 deletions src/Assembly/Parse/TestAsm.v
View file
Open in desktop
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.*)
33 changes: 19 additions & 14 deletions src/Assembly/Symbolic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Crypto.Assembly.Parse.

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

View workflow job for this annotation

GitHub Actions / macOS 14 (arm64) 

src/Assembly/Symbolic.v

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

View workflow job for this annotation

GitHub Actions / macOS 14 (arm64) 

src/Assembly/Symbolic.v

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

View workflow job for this annotation

GitHub Actions / macOS 13 (x86_64) 

src/Assembly/Symbolic.v

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

View workflow job for this annotation

GitHub Actions / macOS 13 (x86_64) 

src/Assembly/Symbolic.v
From Coq.Program Require Import Tactics.
From Coq Require Import Derive.
From Coq Require Import List.
Expand Down Expand Up @@ -3863,8 +3863,12 @@
(List.find (fun v => option_beq N.eqb (Some i) (fst v))
(Tuple.to_list _ (Tuple.map2 (@pair _ _) st (CF, PF, AF, ZF, SF, OF)))).

Definition is_ip_register_index (ri : N) : bool :=
REG_beq (widest_register_of_index ri) rip.
Definition get_reg (st : reg_state) (ri : N) : option idx
:= Tuple.nth_default None (N.to_nat ri) st.
:= if is_ip_register_index ri
then None
else Tuple.nth_default None (N.to_nat ri) st.
Definition set_reg (st : reg_state) (ri : N) (i : idx) : reg_state
:= Tuple.from_list_default None _ (ListUtil.set_nth
(N.to_nat ri)
Expand Down Expand Up @@ -3934,15 +3938,15 @@
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 @@ -4044,11 +4048,11 @@
:= 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 @@ -4067,7 +4071,7 @@
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 @@ -4088,16 +4092,17 @@

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
Loading
Loading