Add --asm-node-reveal-depth (#2055)

Author: JasonGross

src/Assembly/Symbolic.v

@@ -404,6 +404,8 @@ Module Export Options.
   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.
+  (** How deep should we reveal nodes? *)
+  Class node_reveal_depth_opt := node_reveal_depth : nat.
   Definition default_rewriting_passes
              {rewriting_pipeline : rewriting_pipeline_opt}
              {rewriting_pass_filter : rewriting_pass_filter_opt}
@@ -414,19 +416,24 @@ Module Export Options.
     { asm_rewriting_pipeline : rewriting_pipeline_opt
     ; asm_rewriting_pass_filter : rewriting_pass_filter_opt
     ; asm_debug_symex_asm_first : debug_symex_asm_first_opt
+    ; asm_node_reveal_depth : node_reveal_depth_opt
     }.
 
+  Definition default_node_reveal_depth := 3%nat.
+
   (* 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
+    ; asm_node_reveal_depth_computed : node_reveal_depth_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
+       ; asm_node_reveal_depth := default_node_reveal_depth
        |}.
 End Options.
 Module Export Hints.
@@ -439,6 +446,8 @@ Module Export Hints.
          asm_rewriting_passes
          asm_debug_symex_asm_first
          asm_debug_symex_asm_first_computed
+         asm_node_reveal_depth
+         asm_node_reveal_depth_computed
   .
   #[global]
    Hint Cut [
@@ -448,6 +457,8 @@ Module Export Hints.
         | asm_rewriting_passes
         | asm_debug_symex_asm_first
         | asm_debug_symex_asm_first_computed
+        | asm_node_reveal_depth
+        | asm_node_reveal_depth_computed
         ) ( _ * )
         (Build_symbolic_options_opt
         | Build_symbolic_options_computed_opt
@@ -3808,7 +3819,7 @@ Qed.
 End Rewrite.
 
 Definition simplify {opts : symbolic_options_computed_opt} (dag : dag) (e : node idx) :=
-  Rewrite.expr dag (reveal_node_at_least dag 3 e).
+  Rewrite.expr dag (reveal_node_at_least dag node_reveal_depth e).
 
 Lemma eval_simplify {opts : symbolic_options_computed_opt} G d n v : gensym_dag_ok G d -> eval_node G d n v -> eval G d (simplify d n) v.
 Proof using Type. eauto using Rewrite.eval_expr, eval_node_reveal_node_at_least. Qed.

src/CLI.v

@@ -519,6 +519,10 @@ Module ForExtraction.
          Arg.Custom (parse_string_and parse_callee_saved_registers) "REG",
          ["Either '" ++ show System_V_AMD64 ++ "' (indicating " ++ String.concat "," (List.map show system_v_amd64_assembly_callee_saved_registers) ++ "), '" ++ show Microsoft_x64 ++ "' (indicating " ++ String.concat "," (List.map show microsoft_x64_assembly_callee_saved_registers) ++ "), or a comma-separated list of registers which are callee-saved / non-volatile.  Only relevant when --hints-file is specified."
           ; "Defaults to " ++ show default_assembly_callee_saved_registers ++ "."]).
+  Definition asm_node_reveal_depth_spec : named_argT
+    := ([Arg.long_key "asm-node-reveal-depth"],
+        Arg.Custom (parse_string_and parse_nat) "ℕ",
+        ["The depth of nodes to reveal in the assembly equivalence checker.  Only relevant when --hints-file is specified.  In most situations, this should not have to be changed.  Defaults to " ++ show default_node_reveal_depth ++ "."]).
   Definition asm_stack_size_spec : named_argT
     := ([Arg.long_key "asm-stack-size"],
         Arg.Custom (parse_string_and parse_N) "ℕ",
@@ -734,6 +738,7 @@ Module ForExtraction.
         ; asm_error_on_unique_names_mismatch_spec
         ; asm_rewriting_pipeline_spec
         ; asm_rewriting_passes_spec
+        ; asm_node_reveal_depth_spec
         ; asm_debug_symex_asm_first_spec
         ; doc_text_before_function_name_spec
         ; doc_text_before_type_name_spec
@@ -793,6 +798,7 @@ Module ForExtraction.
              , asm_error_on_unique_names_mismatchv
              , asm_rewriting_pipelinev
              , asm_rewriting_passesv
+             , asm_node_reveal_depthv
              , asm_debug_symex_asm_firstv
              , doc_text_before_function_namev
              , doc_text_before_type_namev
@@ -806,6 +812,7 @@ Module ForExtraction.
        let to_bool ls := (0 <? List.length ls)%nat in
        let to_string_list ls := List.map (@snd _ _) ls in
        let to_N_list ls := List.map (@snd _ _) (List.map (@snd _ _) ls) in
+       let to_nat_list ls := List.map (@snd _ _) (List.map (@snd _ _) ls) in
        let to_Z_flat_list ls := List.flat_map (@snd _ _) (List.map (@snd _ _) ls) in
        let to_reg_list ls := match List.map (@snd _ _) (List.map (@snd _ _) ls) with
                              | nil => None
@@ -820,6 +827,8 @@ Module ForExtraction.
        let to_assembly_callee_saved_registers_default ls default := Option.value (to_assembly_callee_saved_registers_opt ls) default in
        let to_N_opt ls := choose_one_of_many (to_N_list ls) in
        let to_N_default ls default := Option.value (to_N_opt ls) default in
+       let to_nat_opt ls := choose_one_of_many (to_nat_list ls) in
+       let to_nat_default ls default := Option.value (to_nat_opt ls) default in
        let to_string_opt ls := choose_one_of_many (to_string_list ls) in
        let to_string_default ls default := Option.value (to_string_opt ls) default in
        let to_capitalization_data_opt ls := choose_one_of_many (List.map (fun '(_, (_, v)) => v) ls) in
@@ -882,6 +891,7 @@ Module ForExtraction.
                       {| 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
+                      ; asm_node_reveal_depth := to_nat_default asm_node_reveal_depthv default_node_reveal_depth
                       |}
                     |}
                   ; ignore_unique_asm_names := negb (to_bool asm_error_on_unique_names_mismatchv)