diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index bf5dc1f3fc..f3f65f3170 100644 --- a/src/Assembly/Equivalence.v +++ b/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,6 +151,8 @@ 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 @@ -147,6 +160,8 @@ Definition default_assembly_conventions : assembly_conventions_opt ; 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. diff --git a/src/CLI.v b/src/CLI.v index e8300fec1a..58fff1c8ce 100644 --- a/src/CLI.v +++ b/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 diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 684331b62a..3f1cb07682 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/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,