Rename compilation flags "checkmach" to "zero-alloc-checker"

backend/asmgen.ml

@@ -277,7 +277,7 @@ let compile_fundecl ~ppf_dump ~funcnames fd_cmm =
   ++ Profile.record ~accumulate:true "polling"
        (Polling.instrument_fundecl ~future_funcnames:funcnames)
   ++ Compiler_hooks.execute_and_pipe Compiler_hooks.Mach_polling
-  ++ Profile.record ~accumulate:true "checkmach"
+  ++ Profile.record ~accumulate:true "zero_alloc_checker"
        (Zero_alloc_checker.fundecl ~future_funcnames:funcnames ppf_dump)
   ++ (fun fd ->
       match !Flambda_backend_flags.cfg_cse_optimize with

backend/zero_alloc_checker.ml

@@ -126,7 +126,7 @@ end = struct
 
   let join t1 t2 =
     let res = union t1 t2 in
-    match !Flambda_backend_flags.checkmach_details_cutoff with
+    match !Flambda_backend_flags.zero_alloc_checker_details_cutoff with
     | Keep_all -> res
     | No_details ->
       if not (is_empty res)
@@ -1629,7 +1629,7 @@ end = struct
       List.concat [f div "diverge"; f nor ""; f exn "exceptional return"]
     in
     let details =
-      match !Flambda_backend_flags.checkmach_details_cutoff with
+      match !Flambda_backend_flags.zero_alloc_checker_details_cutoff with
       | No_details ->
         (* do not print witnesses. *)
         []
@@ -1883,7 +1883,7 @@ end = struct
     }
 
   let should_keep_witnesses keep =
-    match !Flambda_backend_flags.checkmach_details_cutoff with
+    match !Flambda_backend_flags.zero_alloc_checker_details_cutoff with
     | Keep_all -> true
     | No_details -> false
     | At_most _ -> keep
@@ -1895,7 +1895,7 @@ end = struct
   let analysis_name = "zero_alloc"
 
   let report' ppf v ~current_fun_name ~msg ~desc dbg =
-    if !Flambda_backend_flags.dump_checkmach
+    if !Flambda_backend_flags.dump_zero_alloc_checker
     then
       Format.fprintf ppf "*** check %s %s in %s: %s with %a (%a)\n"
         analysis_name msg current_fun_name desc
@@ -1908,13 +1908,13 @@ end = struct
   let is_future_funcname t callee = String.Set.mem callee t.future_funcnames
 
   let report_unit_info ppf unit_info ~msg =
-    if !Flambda_backend_flags.dump_checkmach
+    if !Flambda_backend_flags.dump_zero_alloc_checker
     then
       let msg = Printf.sprintf "%s %s:" analysis_name msg in
       Unit_info.iter unit_info ~f:(Func_info.print ~witnesses:true ppf ~msg)
 
   let report_func_info ~msg ppf func_info =
-    if !Flambda_backend_flags.dump_checkmach
+    if !Flambda_backend_flags.dump_zero_alloc_checker
     then
       let msg = Printf.sprintf "%s %s:" analysis_name msg in
       Func_info.print ~witnesses:true ppf ~msg func_info
@@ -1977,7 +1977,7 @@ end = struct
     in
     if is_future_funcname t callee
     then
-      if !Flambda_backend_flags.disable_precise_checkmach
+      if !Flambda_backend_flags.disable_precise_zero_alloc_checker
       then
         (* Conservatively return Top. Won't be able to prove any recursive
            functions as non-allocating. *)
@@ -2385,7 +2385,7 @@ end = struct
         report_unit_info ppf unit_info ~msg:"after record"
       in
       let really_check () =
-        if !Flambda_backend_flags.disable_checkmach
+        if !Flambda_backend_flags.disable_zero_alloc_checker
         then
           (* Do not analyze the body of the function, conservatively assume that
              the summary is top. *)

backend/zero_alloc_checker.mli

@@ -87,7 +87,8 @@ end
       at any time, but the complete information is only available after a call to
       [record_unit_info].  To get all witnesses for all functions, and not only for
       functions annotated with [@zero_alloc], set
-      [Flambda_backend_flags.checkmach_details_cutoff] to a negative value before calls to
+      [Flambda_backend_flags.zero_alloc_checker_details_cutoff]
+      to a negative value before calls to
       [fundecl].  Used by compiler_hooks. *)
 type iter_witnesses = (string -> Witnesses.components -> unit) -> unit
 

driver/flambda_backend_args.ml

@@ -107,38 +107,37 @@ let mk_zero_alloc_check f =
   " Check that annotated functions do not allocate \
    and do not have indirect calls. "^Zero_alloc_annotations.doc
 
-let mk_dcheckmach f =
-  "-dcheckmach", Arg.Unit f, " (undocumented)"
+let mk_dzero_alloc f =
+  "-dzero-alloc", Arg.Unit f, " (undocumented)"
 
-let mk_disable_checkmach f =
-  "-disable-checkmach", Arg.Unit f,
+let mk_disable_zero_alloc_checker f =
+  "-disable-zero-alloc-checker", Arg.Unit f,
   " Conservatively assume that all functions may allocate, without checking. \
     Disables computation of zero_alloc function summaries, \
     unlike \"-zero-alloc-check none\" which disables checking of zero_alloc annotations)"
 
-let mk_disable_precise_checkmach f =
-  "-disable-precise-checkmach", Arg.Unit f,
+let mk_disable_precise_zero_alloc_checker f =
+  "-disable-precise-zero-alloc-checker", Arg.Unit f,
   " Conservatively assume that all forward calls and mutually recursive functions may \
     allocate. Disables fixed point computation of summaries for these functions. \
     Intended as a temporary workaround when precise analysis is too expensive."
 
-let mk_checkmach_details_cutoff f =
-  "-checkmach-details-cutoff", Arg.Int f,
+let mk_zero_alloc_checker_details_cutoff f =
+  "-zero-alloc-checker-details-cutoff", Arg.Int f,
   Printf.sprintf " Do not show more than this number of error locations \
                   in each function that fails the check \
                   (default %d, negative to show all)"
-    (match Flambda_backend_flags.default_checkmach_details_cutoff with
+    (match Flambda_backend_flags.default_zero_alloc_checker_details_cutoff with
      | Keep_all -> (-1)
      | No_details -> 0
      | At_most n -> n)
 
-
-let mk_checkmach_join f =
-  "-checkmach-join", Arg.Int f,
+let mk_zero_alloc_checker_join f =
+  "-zero-alloc-checker-join", Arg.Int f,
   Printf.sprintf " How many abstract paths before losing precision \
                   (default %d, negative to fail instead of widening, \
                   0 to keep all)"
-    (match Flambda_backend_flags.default_checkmach_join with
+    (match Flambda_backend_flags.default_zero_alloc_checker_join with
      | Keep_all -> 0
      | Widen n -> n
      | Error n -> -n)
@@ -672,11 +671,11 @@ module type Flambda_backend_options = sig
 
   val heap_reduction_threshold : int -> unit
   val zero_alloc_check : string -> unit
-  val dcheckmach : unit -> unit
-  val disable_checkmach : unit -> unit
-  val disable_precise_checkmach : unit -> unit
-  val checkmach_details_cutoff : int -> unit
-  val checkmach_join : int -> unit
+  val dzero_alloc : unit -> unit
+  val disable_zero_alloc : unit -> unit
+  val disable_precise_zero_alloc : unit -> unit
+  val zero_alloc_details_cutoff : int -> unit
+  val zero_alloc_join : int -> unit
 
   val function_layout : string -> unit
   val disable_poll_insertion : unit -> unit
@@ -791,11 +790,12 @@ struct
 
     mk_heap_reduction_threshold F.heap_reduction_threshold;
     mk_zero_alloc_check F.zero_alloc_check;
-    mk_dcheckmach F.dcheckmach;
-    mk_disable_checkmach F.disable_checkmach;
-    mk_disable_precise_checkmach F.disable_precise_checkmach;
-    mk_checkmach_details_cutoff F.checkmach_details_cutoff;
-    mk_checkmach_join F.checkmach_join;
+
+    mk_dzero_alloc F.dzero_alloc;
+    mk_disable_zero_alloc_checker F.disable_zero_alloc_checker;
+    mk_disable_precise_zero_alloc_checker F.disable_precise_zero_alloc_checker;
+    mk_zero_alloc_checker_details_cutoff F.zero_alloc_checker_details_cutoff;
+    mk_zero_alloc_checker_join F.zero_alloc_checker_join;
 
     mk_function_layout F.function_layout;
     mk_disable_poll_insertion F.disable_poll_insertion;
@@ -958,16 +958,16 @@ module Flambda_backend_options_impl = struct
     | Some a ->
       Clflags.zero_alloc_check := a
 
-  let dcheckmach = set' Flambda_backend_flags.dump_checkmach
-  let disable_checkmach = set' Flambda_backend_flags.disable_checkmach
-  let disable_precise_checkmach = set' Flambda_backend_flags.disable_precise_checkmach
-  let checkmach_details_cutoff n =
-    let c : Flambda_backend_flags.checkmach_details_cutoff =
+  let dzero_alloc_checker = set' Flambda_backend_flags.dump_zero_alloc_checker
+  let disable_zero_alloc_checker = set' Flambda_backend_flags.disable_zero_alloc_checker
+  let disable_precise_zero_alloc_checker = set' Flambda_backend_flags.disable_precise_zero_alloc_checker
+  let zero_alloc_checker_details_cutoff n =
+    let c : Flambda_backend_flags.zero_alloc_checker_details_cutoff =
       if n < 0 then Keep_all
       else if n = 0 then No_details
       else At_most n
     in
-    Flambda_backend_flags.checkmach_details_cutoff := c
+    Flambda_backend_flags.zero_alloc_checker_details_cutoff := c
 
   let checkmach_join n =
     let c : Flambda_backend_flags.checkmach_join =
@@ -1256,13 +1256,13 @@ module Extra_params = struct
          raise
            (Arg.Bad
               (Printf.sprintf "Unexpected value %s for %s" v name)))
-    | "dump-checkmach" -> set' Flambda_backend_flags.dump_checkmach
-    | "disable-checkmach" -> set' Flambda_backend_flags.disable_checkmach
-    | "disable-precise-checkmach" -> set' Flambda_backend_flags.disable_precise_checkmach
-    | "checkmach-details-cutoff" ->
+    | "dump-zero-alloc-checker" -> set' Flambda_backend_flags.dump_zero_alloc_checker
+    | "disable-zero-alloc-checker" -> set' Flambda_backend_flags.disable_zero_alloc_checker
+    | "disable-precise-zero-alloc-checker" -> set' Flambda_backend_flags.disable_precise_zero_alloc_checker
+    | "zero-alloc-checker-details-cutoff" ->
       begin match Compenv.check_int ppf name v with
       | Some i ->
-        Flambda_backend_options_impl.checkmach_details_cutoff i
+        Flambda_backend_options_impl.zero_alloc_checker_details_cutoff i
       | None -> ()
       end;
       true

driver/flambda_backend_args.mli

@@ -51,11 +51,12 @@ module type Flambda_backend_options = sig
 
   val heap_reduction_threshold : int -> unit
   val zero_alloc_check : string -> unit
-  val dcheckmach : unit -> unit
-  val disable_checkmach : unit -> unit
-  val disable_precise_checkmach : unit -> unit
-  val checkmach_details_cutoff : int -> unit
-  val checkmach_join : int -> unit
+
+  val dzero_alloc : unit -> unit
+  val disable_zero_alloc_checker : unit -> unit
+  val disable_precise_zero_alloc_checker : unit -> unit
+  val zero_alloc_checker_details_cutoff : int -> unit
+  val zero_alloc_checker_join : int -> unit
 
   val function_layout : string -> unit
   val disable_poll_insertion : unit -> unit

driver/flambda_backend_flags.ml

@@ -34,18 +34,19 @@ let dasm_comments = ref false (* -dasm-comments *)
 
 let default_heap_reduction_threshold = 500_000_000 / (Sys.word_size / 8)
 let heap_reduction_threshold = ref default_heap_reduction_threshold (* -heap-reduction-threshold *)
-let dump_checkmach = ref false          (* -dcheckmach *)
-let disable_checkmach = ref false       (* -disable-checkmach *)
-let disable_precise_checkmach = ref false  (* -disable-precise-checkmach *)
+let dump_zero_alloc_checker = ref false          (* -dzero-alloc-checker *)
+let disable_zero_alloc_checker = ref false       (* -disable-zero-alloc-checker *)
+let disable_precise_zero_alloc_checker = ref false  (* -disable-precise-zero_alloc_checker *)
 
-type checkmach_details_cutoff =
+type zero_alloc_checker_details_cutoff =
   | Keep_all
   | At_most of int
   | No_details
 
-let default_checkmach_details_cutoff = At_most 20
-let checkmach_details_cutoff = ref default_checkmach_details_cutoff
-                                       (* -checkmach-details-cutoff n *)
+let default_zero_alloc_checker_details_cutoff = At_most 20
+let zero_alloc_checker_details_cutoff = ref default_zero_alloc_checker_details_cutoff
+                                       (* -zero-alloc-checker-details-cutoff n *)
+
 type checkmach_join =
   | Keep_all
   | Widen of int  (* n > 0 *)
@@ -54,6 +55,7 @@ type checkmach_join =
 let default_checkmach_join = Widen 100
 let checkmach_join = ref default_checkmach_join
                               (* -checkmach-precise-join-threshold n *)
+
 module Function_layout = struct
   type t =
     | Topological

driver/flambda_backend_flags.mli

@@ -35,19 +35,19 @@ val dasm_comments : bool ref
 
 val default_heap_reduction_threshold : int
 val heap_reduction_threshold : int ref
-val dump_checkmach : bool ref
-val disable_checkmach : bool ref
-val disable_precise_checkmach : bool ref
+val dump_zero_alloc_checker : bool ref
+val disable_zero_alloc_checker : bool ref
+val disable_precise_zero_alloc_checker : bool ref
 val davail : bool ref
 val dranges : bool ref
 
-type checkmach_details_cutoff =
+type zero_alloc_checker_details_cutoff =
   | Keep_all
   | At_most of int  (* n > 0 *)
   | No_details
 
-val checkmach_details_cutoff : checkmach_details_cutoff ref
-val default_checkmach_details_cutoff : checkmach_details_cutoff
+val zero_alloc_checker_details_cutoff : zero_alloc_checker_details_cutoff ref
+val default_zero_alloc_checker_details_cutoff : zero_alloc_checker_details_cutoff
 
 type checkmach_join =
   | Keep_all

tests/backend/checkmach/fail25.ml

@@ -1,4 +1,4 @@
-(* all functions fail the check when -disable-checkmach is passed. *)
+(* all functions fail the check when -disable-zero-zero-alloc-checker is passed. *)
 module Sexp = struct
   type t =
     | Atom of string
@@ -18,7 +18,7 @@ let raise_s sexp = raise (Exn sexp)
  *       "Unknown" (unknown_index : int) (name : string)]
  * ;; *)
 
-(* pass the check when -disable-precise-checkmach is passed, because
+(* pass the check when -disable-precise-zero-alloc-checker is passed, because
    conservative summary of ppx_sexp_message is on used on a path to
    raise_s. *)
 let raise_invalid_index_FAIL ~unknown_index ~name =
@@ -41,7 +41,7 @@ let[@zero_alloc] rec g x =
     try g x with _ -> ()
   else raise (Failure x)
 
-(* Functions below fail the check when -disable-precise-checkmach is passed. *)
+(* Functions below fail the check when -disable-precise-zero-alloc-checker is passed. *)
 let[@zero_alloc] rec foo n =
   bar (n-1)
 and[@zero_alloc] bar n =
@@ -53,7 +53,7 @@ let[@zero_alloc] rec f1 x =
 and[@zero_alloc] f2 x =
   f1 (x + 1)
 
-(* Fail the check when -disable-precise-checkmach is passed and -function-layout source *)
+(* Fail the check when -disable-precise-zero-alloc-checker is passed and -function-layout source *)
 let[@zero_alloc] outer x =
   let[@zero_alloc][@inline never][@local never] inner x =
     if x > Sys.opaque_identity 10

tests/backend/checkmach/gen/gen_dune.ml

@@ -17,7 +17,7 @@ let () =
  (alias   runtest)
  ${enabled_if}
  (deps ${deps})
- (action (run %{bin:ocamlopt.opt} %{deps} -g -c ${extra_flags} -dcse -dcheckmach -dump-into-file -O3 -warn-error +a)))
+ (action (run %{bin:ocamlopt.opt} %{deps} -g -c ${extra_flags} -dcse -dzero-alloc-checker -dump-into-file -O3 -warn-error +a)))
 |};
     Buffer.output_buffer Out_channel.stdout buf
   in
@@ -75,7 +75,7 @@ let () =
     (pipe-outputs
     (with-accepted-exit-codes ${exit_code}
      (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c
-          ${extra_flags} -checkmach-details-cutoff ${cutoff} -O3))
+          ${extra_flags} -zero-alloc-checker-details-cutoff ${cutoff} -O3))
     (run "./${filter}")
    ))))
 
@@ -148,10 +148,10 @@ let () =
   print_test_expected_output ~cutoff:default_cutoff ~extra_dep:None ~exit_code:2 "fail24";
   print_test ~extra_flags:"-zero-alloc-check default -function-layout topological"  "test_raise_message.ml";
   print_test_expected_output ~cutoff:default_cutoff
-    ~extra_flags:"-zero-alloc-check default -disable-precise-checkmach -function-layout source"
+    ~extra_flags:"-zero-alloc-check default -disable-precise-zero-alloc-checker -function-layout source"
     ~extra_dep:None ~exit_code:2 "fail25";
   print_test_expected_output ~cutoff:default_cutoff
-    ~extra_flags:"-zero-alloc-check default -disable-checkmach -function-layout source"
+    ~extra_flags:"-zero-alloc-check default -disable-zero-alloc-checker -function-layout source"
     ~extra_dep:None ~exit_code:2 "fail26";
   print_test_expected_output ~cutoff:default_cutoff
     ~extra_flags:"-zero-alloc-check default"

tools/gen_compiler_libs_installation.ml

@@ -19,7 +19,7 @@ let () =
       | "relocation_table", (".cmt" | ".cmi" | ".cmti" | ".cmx")
       | "symbol_entry", (".cmt" | ".cmi" | ".cmti" | ".cmx") ->
         None
-      | "checkmach", ".mli" -> Some "mach_checks"
+      | "zero_alloc_checker", ".mli" -> Some "mach_checks"
       | "cSE", (".cmi" | ".cmt" | ".cmx") -> Some "CSE"
       | "cSEgen", (".cmi" | ".cmt" | ".cmti" | ".cmx") -> Some "CSEgen"
       | _, _ -> Some prefix