Allow fuzzy matching of assembly labels (#2032)

It can be disabled with `--asm-label-exact-match`

src/Assembly/Equivalence.v

@@ -29,6 +29,17 @@ Import ListNotations.
 Local Open Scope string_scope.
 Local Open Scope list_scope.
 
+
+(** Permit labels to have arbitrary suffixes *)
+Class assembly_labels_fuzzy_suffixes_opt := assembly_labels_fuzzy_suffixes : bool.
+#[global]
+Typeclasses Opaque assembly_labels_fuzzy_suffixes_opt.
+Definition default_assembly_labels_fuzzy_suffixes : assembly_labels_fuzzy_suffixes_opt := true.
+(** Permit labels to have arbitrary prefixes *)
+Class assembly_labels_fuzzy_prefixes_opt := assembly_labels_fuzzy_prefixes : bool.
+#[global]
+Typeclasses Opaque assembly_labels_fuzzy_prefixes_opt.
+Definition default_assembly_labels_fuzzy_prefixes : assembly_labels_fuzzy_prefixes_opt := true.
 (** List of registers used for outputs/inputs *)
 Class assembly_calling_registers_opt := assembly_calling_registers' : option (list REG).
 #[global]
@@ -140,13 +151,17 @@ Class assembly_conventions_opt :=
   ; #[global] assembly_output_first_ :: assembly_output_first_opt
   ; #[global] assembly_argument_registers_left_to_right_ :: assembly_argument_registers_left_to_right_opt
   ; #[global] assembly_callee_saved_registers_ :: assembly_callee_saved_registers_opt
+  ; #[global] assembly_labels_fuzzy_suffixes_ :: assembly_labels_fuzzy_suffixes_opt
+  ; #[global] assembly_labels_fuzzy_prefixes_ :: assembly_labels_fuzzy_prefixes_opt
   }.
 Definition default_assembly_conventions : assembly_conventions_opt
   := {| assembly_calling_registers_ := None
      ; assembly_stack_size_ := None
      ; assembly_output_first_ := true
      ; assembly_argument_registers_left_to_right_ := true
      ; assembly_callee_saved_registers_ := default_assembly_callee_saved_registers
+     ; assembly_labels_fuzzy_suffixes_ := default_assembly_labels_fuzzy_suffixes
+     ; assembly_labels_fuzzy_prefixes_ := default_assembly_labels_fuzzy_prefixes
      |}.
 
 Module Export Options.

src/CLI.v

@@ -505,6 +505,10 @@ Module ForExtraction.
     := ([Arg.long_key "output-asm"],
         Arg.String,
         ["The name of the file to write generated assembly to.  Use - for stdout.  (default: -)"]).
+  Definition asm_label_exact_match_spec : named_argT
+    := ([Arg.long_key "asm-label-exact-match"],
+        Arg.Unit,
+        ["Assembly labels must exactly match the requested function names, rather than permitting arbitrary prefixes and suffixes.  Only relevant when --hints-file is specified."]).
   Definition asm_reg_spec : named_argT
     := ([Arg.long_key "asm-reg"],
         Arg.Custom (parse_string_and parse_list_REG) "REG",
@@ -716,6 +720,7 @@ Module ForExtraction.
         ; hint_file_spec
         ; output_file_spec
         ; asm_output_spec
+        ; asm_label_exact_match_spec
         ; asm_reg_spec
         ; asm_callee_saved_registers_spec
         ; asm_stack_size_spec
@@ -773,6 +778,7 @@ Module ForExtraction.
              , hint_file_namesv
              , output_file_namev
              , asm_output_file_namev
+             , asm_label_exact_matchv
              , asm_regv
              , asm_callee_saved_registersv
              , asm_stack_sizev
@@ -863,6 +869,8 @@ Module ForExtraction.
                       ; assembly_stack_size_ := to_N_opt asm_stack_sizev
                       ; assembly_output_first_ := negb (to_bool asm_input_firstv)
                       ; assembly_argument_registers_left_to_right_ := negb (to_bool asm_reg_rtlv)
+                      ; assembly_labels_fuzzy_suffixes_ := negb (to_bool asm_label_exact_matchv)
+                      ; assembly_labels_fuzzy_prefixes_ := negb (to_bool asm_label_exact_matchv)
                       |}
                     ; symbolic_options_ :=
                       {| asm_rewriting_pipeline := to_rewriting_pipeline_list asm_rewriting_pipelinev

src/PushButtonSynthesis/Primitives.v

@@ -1322,17 +1322,18 @@ Section __.
                     end)
                 assembly_data in
          (* combine normal data with corresponding assembly data *)
-         let ls := List.map (fun '(n1, normal_data)
-                             => ((n1, normal_data), List.find (fun '(n2, _) => n1 =? n2)%string assembly_data))
+         let cmp longer_string shorter_string := Assembly.Parse.string_matches_loose assembly_labels_fuzzy_prefixes assembly_labels_fuzzy_suffixes longer_string shorter_string in
+         let ls := List.map (fun '(n, normal_data)
+                             => ((n, normal_data), List.find (fun '(n_asm, _) => cmp n_asm n) assembly_data))
                             normal_data in
          (* split out the normal data that has assembly data from the normal data that doesn't *)
          let '(lsAB, lsB) := List.partition (fun '(_, o) => match o with Some _ => true | None => false end) ls in
          (* get the assembly functions that have no corresponding normal function *)
-         let lsA := List.filter (fun '(n1, _) => negb (List.existsb (fun '(n2, _) => (n1 =? n2)%string) normal_data)) assembly_data in
+         let lsA := List.filter (fun '(n_asm, _) => negb (List.existsb (fun '(n, _) => cmp n_asm n) normal_data)) assembly_data in
          (* flatten out assembly functions and move the file names first *)
-         let lsA := List.flat_map (fun '(function_name, ls) => List.map (fun '(file_name, v) => (file_name, (function_name, v))) ls) lsA in
+         let lsA := List.flat_map (fun '(function_name_asm, ls) => List.map (fun '(file_name, v) => (file_name, (function_name_asm, v))) ls) lsA in
          (* group by files for assembly data *)
-         let lsA := List.groupAllBy (fun '(n1, _) '(n2, _) => (n1 =? n2)%string) lsA in
+         let lsA := List.groupAllBy (fun '(n1_asm, _) '(n2_asm, _) => (n1_asm =? n2_asm)%string) lsA in
          let lsA
            := Option.List.map
                 (fun ls
@@ -1344,7 +1345,7 @@ Section __.
          (Option.List.map
             (fun '((n, normal_data), assembly_data)
              => match assembly_data with
-                | Some (_n (* should be equal to n *), assembly_data) => Some (n, (assembly_data, normal_data))
+                | Some (_n_asm, assembly_data) => Some (n, (assembly_data, normal_data))
                 | None => (* should not happen *) None
                 end)
             lsAB,