From eafb105d8010f6973364330c0c990bc781618cba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Mar 2025 14:34:35 -0800 Subject: [PATCH] Add `--debug-asm-symex-first` This flag results in running symex on the asm side first, resulting in easier debugging when there is an error in symbolically executing the assembly at all. --- src/Assembly/Equivalence.v | 63 ++++++++++++++++++++++++++++---------- src/Assembly/Symbolic.v | 9 ++++++ src/CLI.v | 7 +++++ 3 files changed, 63 insertions(+), 16 deletions(-) diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index f3f65f3170..2006770e83 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -1452,30 +1452,61 @@ Section check_equivalence. Local Notation map_err_None v := (ErrorT.map_error (fun e => (None, e)) v). Local Notation map_err_Some label v := (ErrorT.map_error (fun e => (Some label, e)) v). - Definition check_equivalence : ErrorT (option (string (* fname *) * Lines (* asm lines *)) * EquivalenceCheckingError) unit := + Definition map_symex_asm (inputs : list (idx + list idx)) (output_types : type_spec) (d : dag) + : ErrorT + (option (string (* fname *) * Lines (* asm lines *)) * EquivalenceCheckingError) + (list ((string (* fname *) * Lines (* asm lines *)) * (list (idx + list idx) * symbolic_state))) := let reg_available := assembly_calling_registers (* registers available for calling conventions *) in + (ls <-- (List.map + (fun '((fname, asm) as label) + => (asm <- map_err_Some label (strip_ret asm); + let stack_size : nat := N.to_nat (assembly_stack_size asm) in + symevaled_asm <- map_err_Some label (symex_asm_func (dereference_output_scalars:=false) d assembly_callee_saved_registers output_types stack_size inputs reg_available asm); + Success (label, symevaled_asm))) + asm); + Success ls)%error. + + Definition check_equivalence : ErrorT (option (string (* fname *) * Lines (* asm lines *)) * EquivalenceCheckingError) unit := let d := dag.empty in input_types <- map_err_None (simplify_input_type t arg_bounds); output_types <- map_err_None (simplify_base_type (type.final_codomain t) out_bounds); - let '(inputs, d) := build_inputs (descr:=Build_description "build_inputs" true ) input_types d in + let '(inputs, d) := build_inputs (descr:=Build_description "build_inputs" true) input_types d in - PHOAS_output <- map_err_None (symex_PHOAS expr inputs d); - let '(PHOAS_output, d) := PHOAS_output in + ls <- ( + if negb debug_symex_asm_first then ( + PHOAS_output <- map_err_None (symex_PHOAS expr inputs d); + let '(PHOAS_output, d) := PHOAS_output in - let first_new_idx_after_all_old_idxs : option idx := Some (dag.size d) in + let first_new_idx_after_all_old_idxs : option idx := Some (dag.size d) in - _ <-- (List.map - (fun '((fname, asm) as label) - => (asm <- map_err_Some label (strip_ret asm); - let stack_size : nat := N.to_nat (assembly_stack_size asm) in - symevaled_asm <- map_err_Some label (symex_asm_func (dereference_output_scalars:=false) d assembly_callee_saved_registers output_types stack_size inputs reg_available asm); - let '(asm_output, s) := symevaled_asm in + asm_output <- map_symex_asm inputs output_types d; + + let ls := List.map (fun '(lbl, (asm_output, s)) => (lbl, asm_output, PHOAS_output, s, first_new_idx_after_all_old_idxs)) asm_output in + Success ls + ) else ( (* debug version, do asm first *) + asm_output <- map_symex_asm inputs output_types d; + + ls <-- (List.map (fun '(lbl, (asm_output, s)) => + let d := s.(dag_state) in + let first_new_idx_after_all_old_idxs : option idx := Some (dag.size d) in + + PHOAS_output <- map_err_None (symex_PHOAS expr inputs d); + let '(PHOAS_output, d) := PHOAS_output in + + let s := {| dag_state := d; symbolic_reg_state := s.(symbolic_reg_state); symbolic_flag_state := s.(symbolic_flag_state); symbolic_mem_state := s.(symbolic_mem_state) |} in + + Success (lbl, asm_output, PHOAS_output, s, first_new_idx_after_all_old_idxs)) + asm_output); + Success ls + )); + + _ <-- List.map (fun '(lbl, asm_output, PHOAS_output, s, first_new_idx_after_all_old_idxs) => + if list_beq _ (sum_beq _ _ N.eqb (list_beq _ N.eqb)) asm_output PHOAS_output + then Success tt + else Error (Some lbl, Unable_to_unify asm_output PHOAS_output first_new_idx_after_all_old_idxs s)) + ls; + Success tt. - if list_beq _ (sum_beq _ _ N.eqb (list_beq _ N.eqb)) asm_output PHOAS_output - then Success tt - else Error (Some label, Unable_to_unify asm_output PHOAS_output first_new_idx_after_all_old_idxs s))) - asm); - Success tt. (** We don't actually generate assembly, we just check equivalence and pass assembly through unchanged *) Definition generate_assembly_of_hinted_expr : ErrorT (option (string (* fname *) * Lines (* asm lines *)) * EquivalenceCheckingError) (list (string * Lines)) diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v index 5849e9547a..fd6d6cdca3 100644 --- a/src/Assembly/Symbolic.v +++ b/src/Assembly/Symbolic.v @@ -401,6 +401,8 @@ Module Export Options. than every time, because it is (currently) quadratic to compute in the number of passes *) Class rewriting_passes_opt := rewriting_passes : list rewrite_pass. + (** Should we symex the assembly first, even though this may be more inefficient? *) + Class debug_symex_asm_first_opt := debug_symex_asm_first : bool. Definition default_rewriting_passes {rewriting_pipeline : rewriting_pipeline_opt} {rewriting_pass_filter : rewriting_pass_filter_opt} @@ -410,17 +412,20 @@ Module Export Options. Class symbolic_options_opt := { asm_rewriting_pipeline : rewriting_pipeline_opt ; asm_rewriting_pass_filter : rewriting_pass_filter_opt + ; asm_debug_symex_asm_first : debug_symex_asm_first_opt }. (* This holds the list of computed options, which are passed around between methods *) Class symbolic_options_computed_opt := { asm_rewriting_passes : rewriting_passes_opt + ; asm_debug_symex_asm_first_computed : debug_symex_asm_first_opt }. (* N.B. The default rewriting pass filter should not be changed here, but instead changed in CLI.v where it is derived from a default string *) Definition default_symbolic_options : symbolic_options_opt := {| asm_rewriting_pipeline := default_rewrite_pass_order ; asm_rewriting_pass_filter := fun _ => true + ; asm_debug_symex_asm_first := false |}. End Options. Module Export Hints. @@ -431,6 +436,8 @@ Module Export Hints. asm_rewriting_pipeline asm_rewriting_pass_filter asm_rewriting_passes + asm_debug_symex_asm_first + asm_debug_symex_asm_first_computed . #[global] Hint Cut [ @@ -438,6 +445,8 @@ Module Export Hints. (asm_rewriting_pipeline | asm_rewriting_pass_filter | asm_rewriting_passes + | asm_debug_symex_asm_first + | asm_debug_symex_asm_first_computed ) ( _ * ) (Build_symbolic_options_opt | Build_symbolic_options_computed_opt diff --git a/src/CLI.v b/src/CLI.v index 58fff1c8ce..06f74cf12a 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -547,6 +547,10 @@ Module ForExtraction. := ([Arg.long_key "asm-rewriting-passes"], Arg.String, ["A comma-separated list of rewriting passes to enable. Prefix with - to disable a pass. This list only impacts passes listed in --asm-rewriting-pipeline. Default : " ++ (if default_asm_rewriting_passes =? "" then "(none)" else default_asm_rewriting_passes)]%string ++ describe_flag_options "rewriting pass" "Enable all rewriting passes" special_asm_rewriting_pass_flags known_asm_rewriting_pass_flags_with_spec)%list. + Definition asm_debug_symex_asm_first_spec : named_argT + := ([Arg.long_key "debug-asm-symex-first"], + Arg.Unit, + ["Debug option: If true, the assembly equivalence checker will symex the assembly first, even though this may be more inefficient. This may be useful for having a more concise description of errors in assembly symbolic execution."]). Definition doc_text_before_function_name_spec : named_argT := ([Arg.long_key "doc-text-before-function-name"], Arg.String, @@ -730,6 +734,7 @@ Module ForExtraction. ; asm_error_on_unique_names_mismatch_spec ; asm_rewriting_pipeline_spec ; asm_rewriting_passes_spec + ; asm_debug_symex_asm_first_spec ; doc_text_before_function_name_spec ; doc_text_before_type_name_spec ; doc_newline_before_package_declaration_spec @@ -788,6 +793,7 @@ Module ForExtraction. , asm_error_on_unique_names_mismatchv , asm_rewriting_pipelinev , asm_rewriting_passesv + , asm_debug_symex_asm_firstv , doc_text_before_function_namev , doc_text_before_type_namev , doc_newline_before_package_declarationv @@ -875,6 +881,7 @@ Module ForExtraction. ; symbolic_options_ := {| asm_rewriting_pipeline := to_rewriting_pipeline_list asm_rewriting_pipelinev ; asm_rewriting_pass_filter := fun p => asm_rewriting_pass_filterv (show_rewrite_pass p) + ; asm_debug_symex_asm_first := to_bool asm_debug_symex_asm_firstv |} |} ; ignore_unique_asm_names := negb (to_bool asm_error_on_unique_names_mismatchv)