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.

Author: JasonGross

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

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,13 +436,17 @@ 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 [
       ( _ * )
         (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

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)