Distinguish between "light" and "heavy" flambda2 invariants (#3205)

* Distinguish between "light" and "heavy" flambda2 invariants

Light invariants can be checked in the CI, while heavy invariants are
intended for local debugging. More precisely:

 - Light invariants must be fast to check and have low complexity. A guideline
   is that it is acceptable to call `find` or `mem` functions, but they should
   not use any kind of iterations iterations (`iter`, `fold`, `exists`, etc.).
   It must be viable to enable light invariants in regular user workflows
   without significantly impacting the performance of the compiler.

   Light invariants are enabled by the pre-existing `-dflambda-invariants`
   compiler flag, which is also enabled with `--enable-flambda-invariants`
   configure flag.

   To determine in code whether light invariants should be checked, call the
   function `Flambda_features.check_light_invariants ()`.

   Light invariants are checked on CI jobs, which should prevent drifts between
   the expressed invariants and the actual invariants.

 - Heavy invariants are allowed to be (almost) unbounded in complexity. They
   are not intended to be enabled during regular workflows, but rather to be
   used to help identify the source of a bug once it has been identified that
   one exists. It is fine if enabling heavy invariants drastically slow down
   the compiler on some inputs.

   Heavy invariants are enabled by a new `-dflambda-heavy-invariants`
   compiler flag. This flag implies `-dflambda-invariants`, so light invariants
   are always checked when heavy invariants are checked.

   To determine in code whether heavy invariants should be checked, call the
   function `Flambda_features.check_invariants ()`.

   Heavy invariants are *not* checked on CI jobs at the moment. They currently
   include invariants that are known to be broken and should be investigated
   before being moved to the light invariants.

The name of the compiler flags (invariants/heavy invariants) and feature checks
(light invariants/invariants) is chosen to reflect that users should usually
enable light checks only, but calling `check_light_invariants ()` is a reminder
to make sure the invariant does not do any expensive computation.

A few invariants related to the typing env and aliases that currently hold and
perform no iterations are moved to the set of light invariants. The goal is
that invariants are slowly moved from the heavy set to the light set over time
when it seems useful.

* Support OCAMLPARAM=flambda-invariants=heavy

Author: bclement-ocp

.github/workflows/build.yml

@@ -55,7 +55,7 @@ jobs:
             ocamlparam: '_,O3=1'
 
           - name: flambda2_o3_advanced_meet_frame_pointers_runtime5_polling
-            config: --enable-middle-end=flambda2 --enable-frame-pointers --enable-runtime5 --enable-poll-insertion
+            config: --enable-middle-end=flambda2 --enable-frame-pointers --enable-runtime5 --enable-poll-insertion --enable-flambda-invariants
             os: ubuntu-latest
             build_ocamlparam: ''
             ocamlparam: '_,O3=1,flambda2-meet-algorithm=advanced,flambda2-expert-cont-lifting-budget=200'
@@ -68,7 +68,7 @@ jobs:
             ocamlparam: '_,O3=1,flambda2-meet-algorithm=advanced,flambda2-expert-cont-lifting-budget=200'
 
           - name: flambda2_frame_pointers_oclassic_polling
-            config: --enable-middle-end=flambda2 --enable-frame-pointers --enable-poll-insertion
+            config: --enable-middle-end=flambda2 --enable-frame-pointers --enable-poll-insertion --enable-flambda-invariants
             os: ubuntu-latest
             build_ocamlparam: ''
             ocamlparam: '_,Oclassic=1'

driver/compenv.ml

@@ -188,6 +188,21 @@ let set_compiler_pass ppf ~name v flag ~filter =
           "Please specify at most one %s <pass>." name
       end
 
+let decode_flambda_invariants ppf v ~name =
+  match v with
+  | "0" -> Some No_checks
+  | "1" -> Some Light_checks
+  | "heavy" -> Some Heavy_checks
+  | _ ->
+    Printf.ksprintf (print_error ppf)
+      "bad value %s for %s" v name;
+    None
+
+let set_flambda_invariants ppf ~name v flag =
+  match decode_flambda_invariants ppf v ~name with
+  | None -> ()
+  | Some checks -> flag := checks
+
 (* 'can-discard=' specifies which arguments can be discarded without warning
    because they are not understood by some versions of OCaml. *)
 let can_discard = ref []
@@ -353,7 +368,7 @@ let read_one_param ppf position name v =
   | "flambda-verbose" ->
       set "flambda-verbose" [ dump_flambda_verbose ] v
   | "flambda-invariants" ->
-      set "flambda-invariants" [ flambda_invariant_checks ] v
+    set_flambda_invariants ppf ~name v flambda_invariant_checks
   | "cmm-invariants" ->
       set "cmm-invariants" [ cmm_invariants ] v
   | "linscan" ->

driver/main_args.ml

@@ -809,6 +809,10 @@ let mk_dflambda_invariants f =
   "-dflambda-invariants", Arg.Unit f, " Check Flambda (1 and 2) invariants"
 ;;
 
+let mk_dflambda_heavy_invariants f =
+  "-dflambda-heavy-invariants", Arg.Unit f, " Check Flambda 2 heavy invariants"
+;;
+
 let mk_dflambda_no_invariants f =
   "-dflambda-no-invariants", Arg.Unit f, " Do not check Flambda (1 and 2) \
       invariants"
@@ -1132,6 +1136,7 @@ module type Optcommon_options = sig
   val _dflambda : unit -> unit
   val _drawflambda : unit -> unit
   val _dflambda_invariants : unit -> unit
+  val _dflambda_heavy_invariants : unit -> unit
   val _dflambda_no_invariants : unit -> unit
   val _dflambda_let : int -> unit
   val _dflambda_verbose : unit -> unit
@@ -1573,6 +1578,7 @@ struct
     mk_dflambda F._dflambda;
     mk_drawflambda F._drawflambda;
     mk_dflambda_invariants F._dflambda_invariants;
+    mk_dflambda_heavy_invariants F._dflambda_heavy_invariants;
     mk_dflambda_no_invariants F._dflambda_no_invariants;
     mk_dflambda_let F._dflambda_let;
     mk_dflambda_verbose F._dflambda_verbose;
@@ -1937,9 +1943,13 @@ module Default = struct
     let _dcombine = set dump_combine
     let _dcse = set dump_cse
     let _dflambda = set dump_flambda
-    let _dflambda_invariants = set flambda_invariant_checks
+    let _dflambda_heavy_invariants () =
+      flambda_invariant_checks := Heavy_checks
+    let _dflambda_invariants () =
+      flambda_invariant_checks := Light_checks
     let _dflambda_let stamp = dump_flambda_let := (Some stamp)
-    let _dflambda_no_invariants = clear flambda_invariant_checks
+    let _dflambda_no_invariants () =
+      flambda_invariant_checks := No_checks
     let _dflambda_verbose () =
       set dump_flambda (); set dump_flambda_verbose ()
     let _dinterval = set dump_interval

driver/main_args.mli

@@ -225,6 +225,7 @@ module type Optcommon_options = sig
   val _dflambda : unit -> unit
   val _drawflambda : unit -> unit
   val _dflambda_invariants : unit -> unit
+  val _dflambda_heavy_invariants : unit -> unit
   val _dflambda_no_invariants : unit -> unit
   val _dflambda_let : int -> unit
   val _dflambda_verbose : unit -> unit

middle_end/flambda2/types/env/aliases.ml

@@ -152,7 +152,7 @@ end = struct
         (function
           | None -> Some (Name.Map.singleton elt coercion_to_canonical)
           | Some elts ->
-            if Flambda_features.check_invariants ()
+            if Flambda_features.check_light_invariants ()
             then assert (not (Name.Map.mem elt elts));
             Some (Name.Map.add elt coercion_to_canonical elts))
         t.aliases
@@ -646,7 +646,7 @@ let add_alias_between_canonical_elements ~binding_time_resolver
     let aliases_of_to_be_demoted =
       get_aliases_of_canonical_element t ~canonical_element:to_be_demoted
     in
-    if Flambda_features.check_invariants ()
+    if Flambda_features.check_light_invariants ()
     then
       Simple.pattern_match canonical_element
         ~const:(fun _ -> ())
@@ -808,7 +808,7 @@ let add ~binding_time_resolver ~binding_times_and_modes t
       (Simple.coercion element2_with_coercion)
       ~then_:(Coercion.inverse (Simple.coercion element1_with_coercion))
   in
-  if Flambda_features.check_invariants ()
+  if Flambda_features.check_light_invariants ()
   then (
     if Simple.equal canonical_element1 canonical_element2
     then

middle_end/flambda2/types/env/typing_env.ml

@@ -708,7 +708,7 @@ let add_definition t (name : Bound_name.t) kind =
 
 let invariant_for_alias (t : t) name ty =
   (* Check that no canonical element gets an [Equals] type *)
-  if Flambda_features.check_invariants () || true
+  if Flambda_features.check_light_invariants ()
   then
     match TG.get_alias_exn ty with
     | exception Not_found -> ()
@@ -798,7 +798,7 @@ let rec add_equation0 (t : t) name ty =
   with_current_level t ~current_level
 
 and add_equation1 ~raise_on_bottom t name ty ~(meet_type : meet_type) =
-  (if Flambda_features.check_invariants ()
+  (if Flambda_features.check_light_invariants ()
   then
     let existing_ty = find t name None in
     if not (K.equal (TG.kind existing_ty) (TG.kind ty))
@@ -807,7 +807,7 @@ and add_equation1 ~raise_on_bottom t name ty ~(meet_type : meet_type) =
         "Cannot add equation %a = %a@ given existing binding %a = %a@ whose \
          type is of a different kind:@ %a"
         Name.print name TG.print ty Name.print name TG.print existing_ty print t);
-  (if Flambda_features.check_invariants ()
+  (if Flambda_features.check_light_invariants ()
   then
     match TG.get_alias_exn ty with
     | exception Not_found -> ()

middle_end/flambda2/ui/flambda_features.ml

@@ -99,7 +99,15 @@ let unicode () =
   !Flambda_backend_flags.Flambda2.unicode
   |> with_default ~f:(fun d -> d.unicode)
 
-let check_invariants () = !Clflags.flambda_invariant_checks
+let check_invariants () =
+  match !Clflags.flambda_invariant_checks with
+  | No_checks | Light_checks -> false
+  | Heavy_checks -> true
+
+let check_light_invariants () =
+  match !Clflags.flambda_invariant_checks with
+  | No_checks -> false
+  | Light_checks | Heavy_checks -> true
 
 type dump_target = Flambda_backend_flags.Flambda2.Dump.target =
   | Nowhere

middle_end/flambda2/ui/flambda_features.mli

@@ -60,8 +60,11 @@ val colour : unit -> Misc.Color.setting option
 
 val unicode : unit -> bool
 
+(** Check all invariants (light and heavy). *)
 val check_invariants : unit -> bool
 
+val check_light_invariants : unit -> bool
+
 type dump_target = Flambda_backend_flags.Flambda2.Dump.target =
   | Nowhere
   | Main_dump_stream

utils/clflags.ml

@@ -54,6 +54,7 @@ end
 
 type profile_column = [ `Time | `Alloc | `Top_heap | `Abs_top_heap | `Counters ]
 type profile_granularity_level = File_level | Function_level | Block_level
+type flambda_invariant_checks = No_checks | Light_checks | Heavy_checks
 
 let compile_only = ref false            (* -c *)
 and output_name = ref (None : string option) (* -o *)
@@ -183,7 +184,8 @@ let cmm_invariants =
   ref Config.with_cmm_invariants        (* -dcmm-invariants *)
 
 let flambda_invariant_checks =
-  ref Config.with_flambda_invariants    (* -flambda-(no-)invariants *)
+  let v = if Config.with_flambda_invariants then Light_checks else No_checks in
+  ref v (* -flambda-(no-)invariants *)
 
 let dont_write_files = ref false        (* set to true under ocamldoc *)
 

utils/clflags.mli

@@ -61,6 +61,7 @@ end
 
 type profile_column = [ `Time | `Alloc | `Top_heap | `Abs_top_heap | `Counters ]
 type profile_granularity_level = File_level | Function_level | Block_level
+type flambda_invariant_checks = No_checks | Light_checks | Heavy_checks
 
 val objfiles : string list ref
 val ccobjs : string list ref
@@ -207,7 +208,7 @@ val profile_columns : profile_column list ref
 val profile_granularity : profile_granularity_level ref
 val all_profile_granularity_levels : string list
 val set_profile_granularity : string -> unit
-val flambda_invariant_checks : bool ref
+val flambda_invariant_checks : flambda_invariant_checks ref
 val unbox_closures : bool ref
 val unbox_closures_factor : int ref
 val default_unbox_closures_factor : int