Add support for 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.

src/Assembly/Equivalence.v

@@ -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.
@@ -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
@@ -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).
 
@@ -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
@@ -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.
 
@@ -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);

src/Assembly/Parse.v

@@ -79,16 +79,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;
@@ -144,7 +154,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.
@@ -266,11 +277,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
@@ -489,20 +510,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)
+     |}.

src/Assembly/Parse/TestAsm.v

@@ -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.
@@ -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.*)

src/Assembly/Symbolic.v

@@ -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.
@@ -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)).
 
 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
@@ -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);
@@ -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 :=