Static check for noalloc: attributes

backend/checkmach.ml

@@ -80,10 +80,10 @@ module type Spec = sig
   (** returns true when the check passes. *)
   val check_specific : Arch.specific_operation -> bool
 
-  val annotation : Cmm.codegen_option
+  val annotation : Cmm.property
 end
-(* CR gyorsh: Annotations are not yet implemented. We may also want annotations
-   on call sites, not only on functions. *)
+(* CR-someday gyorsh: We may also want annotations on call sites, not only on
+   functions. *)
 
 (** Check one function. *)
 module Analysis (S : Spec) : sig
@@ -267,7 +267,7 @@ end = struct
   let report t ~msg ~desc dbg =
     if !Flambda_backend_flags.dump_checkmach
     then
-      Format.fprintf t.ppf "*** check %s %s in %s: %s at %a\n" S.name msg
+      Format.fprintf t.ppf "*** check %s %s in %s: %s %a\n" S.name msg
         t.fun_name desc Debuginfo.print_compact dbg
 
   exception Bail
@@ -391,20 +391,25 @@ end = struct
           let fun_name = f.fun_name in
           let t = { ppf; fun_name; unresolved_dependencies = false } in
           Unit_info.in_current_unit unit_info fun_name;
-          (try
-             let _ = check_instr_exn t f.fun_body false in
-             if (not t.unresolved_dependencies)
-                && not (Unit_info.is_fail unit_info t.fun_name)
-             then (
-               report t ~msg:"passed" ~desc:"" f.fun_dbg;
-               Unit_info.add_value t.ppf unit_info fun_name Pass)
-           with Bail -> debug t Fail);
-          if List.mem S.annotation f.fun_codegen_options
-          then Unit_info.annotated unit_info fun_name)
+          if List.mem (Cmm.Assume S.annotation) f.fun_codegen_options
+          then (
+            report t ~msg:"assumed" ~desc:"fundecl" f.fun_dbg;
+            Unit_info.add_value t.ppf unit_info fun_name Pass)
+          else (
+            (try
+               let _ = check_instr_exn t f.fun_body false in
+               if (not t.unresolved_dependencies)
+                  && not (Unit_info.is_fail unit_info t.fun_name)
+               then (
+                 report t ~msg:"passed" ~desc:"fundecl" f.fun_dbg;
+                 Unit_info.add_value t.ppf unit_info fun_name Pass)
+             with Bail -> debug t Fail);
+            if List.mem (Cmm.Assert S.annotation) f.fun_codegen_options
+            then Unit_info.annotated unit_info fun_name))
 end
 
 module Spec_alloc : Spec = struct
-  let name = "alloc"
+  let name = "noalloc"
 
   let enabled () = !Flambda_backend_flags.alloc_check
 
@@ -419,7 +424,7 @@ module Spec_alloc : Spec = struct
 
   let check_specific s = not (Arch.operation_allocates s)
 
-  let annotation = Cmm.Noalloc_check
+  let annotation = Cmm.Noalloc
 end
 
 (***************************************************************************
@@ -448,7 +453,7 @@ let record_unit_info ppf_dump =
 
 let report_error ppf = function
   | Annotation { fun_name; check } ->
-    Format.fprintf ppf "Annotation check for %s on function %s failed" check
+    Format.fprintf ppf "Annotation check for %s failed on function %s" check
       fun_name
 
 let () =

backend/cmm.ml

@@ -244,11 +244,15 @@ type expression =
   | Cregion of expression
   | Ctail of expression
 
+type property =
+  | Noalloc
+
 type codegen_option =
   | Reduce_code_size
   | No_CSE
   | Use_linscan_regalloc
-  | Noalloc_check
+  | Assert of property
+  | Assume of property
 
 type fundecl =
   { fun_name: string;

backend/cmm.mli

@@ -253,11 +253,15 @@ type expression =
   | Cregion of expression
   | Ctail of expression
 
+type property =
+  | Noalloc
+
 type codegen_option =
   | Reduce_code_size
   | No_CSE
   | Use_linscan_regalloc
-  | Noalloc_check
+  | Assert of property
+  | Assume of property
 
 type fundecl =
   { fun_name: string;

backend/cmm_helpers.ml

@@ -4169,3 +4169,11 @@ let cmm_arith_size (e : Cmm.expression) =
   | Cifthenelse _ | Cswitch _ | Ccatch _ | Cexit _ | Ctrywith _ | Cregion _
   | Ctail _ ->
     None
+
+let transl_property : Lambda.property -> Cmm.property = function
+  | Noalloc -> Noalloc
+
+let transl_attrib : Lambda.check_attribute -> Cmm.codegen_option list = function
+  | Default_check -> []
+  | Assert p -> [Assert (transl_property p)]
+  | Assume p -> [Assume (transl_property p)]

backend/cmm_helpers.mli

@@ -1206,3 +1206,5 @@ val gc_root_table :
    If [None] is returned, that means "no estimate available". The expression
    should be assumed to be potentially large. *)
 val cmm_arith_size : expression -> int option
+
+val transl_attrib : Lambda.check_attribute -> Cmm.codegen_option list

backend/cmmgen.ml

@@ -1471,6 +1471,7 @@ let transl_function f =
     else
       transl env body in
   let fun_codegen_options =
+    transl_attrib f.check @
     if !Clflags.optimize_for_speed then
       []
     else

backend/printcmm.ml

@@ -339,11 +339,15 @@ and sequence ppf = function
 
 and expression ppf e = fprintf ppf "%a" expr e
 
+let property : Cmm.property -> string = function
+    | Noalloc -> "noalloc"
+
 let codegen_option = function
   | Reduce_code_size -> "reduce_code_size"
   | No_CSE -> "no_cse"
   | Use_linscan_regalloc -> "linscan"
-  | Noalloc_check -> "noalloc_check"
+  | Assert p -> "assert "^(property p)
+  | Assume p -> "assume "^(property p)
 
 let print_codegen_options ppf l =
   List.iter (fun c -> fprintf ppf " %s" (codegen_option c)) l

middle_end/clambda.ml

@@ -100,6 +100,7 @@ and ufunction = {
   dbg    : Debuginfo.t;
   env    : Backend_var.t option;
   mode   : Lambda.alloc_mode;
+  check  : Lambda.check_attribute;
 }
 
 and ulambda_switch =

middle_end/clambda.mli

@@ -111,6 +111,7 @@ and ufunction = {
   dbg    : Debuginfo.t;
   env    : Backend_var.t option;
   mode   : Lambda.alloc_mode;
+  check  : Lambda.check_attribute;
 }
 
 and ulambda_switch =

middle_end/closure/closure.ml

@@ -1394,9 +1394,10 @@ and close_functions { backend; fenv; cenv; mutable_vars } fun_defs =
   let uncurried_defs =
     List.map
       (function
-          (id, Lfunction({kind; params; return; body; loc; mode; region}
+          (id, Lfunction({kind; params; return; body; attr; loc; mode; region}
                          as funct)) ->
             Lambda.check_lfunction funct;
+            let attrib = attr.check in
             let label = Compilenv.make_fun_symbol loc (V.unique_name id) in
             let arity = List.length params in
             let fundesc =
@@ -1407,20 +1408,20 @@ and close_functions { backend; fenv; cenv; mutable_vars } fun_defs =
                fun_float_const_prop = !Clflags.float_const_prop;
                fun_region = region} in
             let dbg = Debuginfo.from_location loc in
-            (id, params, return, body, mode, fundesc, dbg)
+            (id, params, return, body, mode, attrib, fundesc, dbg)
         | (_, _) -> fatal_error "Closure.close_functions")
       fun_defs in
   (* Build an approximate fenv for compiling the functions *)
   let fenv_rec =
     List.fold_right
-      (fun (id, _params, _return, _body, mode, fundesc, _dbg) fenv ->
+      (fun (id, _params, _return, _body, mode, _attrib, fundesc, _dbg) fenv ->
         V.Map.add id (Value_closure(mode, fundesc, Value_unknown)) fenv)
       uncurried_defs fenv in
   (* Determine the offsets of each function's closure in the shared block *)
   let env_pos = ref (-1) in
   let clos_offsets =
     List.map
-      (fun (_id, _params, _return, _body, _mode, fundesc, _dbg) ->
+      (fun (_id, _params, _return, _body, _mode, _attrib, fundesc, _dbg) ->
         let pos = !env_pos + 1 in
         env_pos := !env_pos + 1 +
           (match fundesc.fun_arity with (Curried _, (0|1)) -> 2 | _ -> 3);
@@ -1431,13 +1432,13 @@ and close_functions { backend; fenv; cenv; mutable_vars } fun_defs =
      does not use its environment parameter is invalidated. *)
   let useless_env = ref initially_closed in
   (* Translate each function definition *)
-  let clos_fundef (id, params, return, body, mode, fundesc, dbg) env_pos =
+  let clos_fundef (id, params, return, body, mode, check, fundesc, dbg) env_pos =
     let env_param = V.create_local "env" in
     let cenv_fv =
       build_closure_env env_param (fv_pos - env_pos) fv in
     let cenv_body =
       List.fold_right2
-        (fun (id, _params, _return, _body, _mode, _fundesc, _dbg) pos env ->
+        (fun (id, _params, _return, _body, _mode, _attrib, _fundesc, _dbg) pos env ->
           V.Map.add id (Uoffset(Uvar env_param, pos - env_pos)) env)
         uncurried_defs clos_offsets cenv_fv in
     let (ubody, approx) =
@@ -1459,6 +1460,7 @@ and close_functions { backend; fenv; cenv; mutable_vars } fun_defs =
         dbg;
         env = Some env_param;
         mode;
+        check;
       }
     in
     (* give more chance of function with default parameters (i.e.
@@ -1497,7 +1499,7 @@ and close_functions { backend; fenv; cenv; mutable_vars } fun_defs =
          recompile *)
         Compilenv.backtrack snap; (* PR#6337 *)
         List.iter
-          (fun (_id, _params, _return, _body, _mode, fundesc, _dbg) ->
+          (fun (_id, _params, _return, _body, _mode, _attrib, fundesc, _dbg) ->
              fundesc.fun_closed <- false;
              fundesc.fun_inline <- None;
           )

middle_end/flambda/augment_specialised_args.ml

@@ -546,6 +546,7 @@ module Make (T : S) = struct
         ~stub:true
         ~inline:Default_inline
         ~specialise:Default_specialise
+        ~check:Default_check
         ~is_a_functor:false
         ~closure_origin:function_decl.closure_origin
     in
@@ -639,6 +640,7 @@ module Make (T : S) = struct
           ~stub:function_decl.stub
           ~inline:function_decl.inline
           ~specialise:function_decl.specialise
+          ~check:function_decl.check
           ~is_a_functor:function_decl.is_a_functor
           ~closure_origin
       in

middle_end/flambda/closure_conversion.ml

@@ -107,7 +107,7 @@ let tupled_function_call_stub original_params unboxed_version ~closure_bound_var
   let tuple_param = Parameter.wrap tuple_param_var alloc_mode in
   Flambda.create_function_declaration ~params:[tuple_param] ~alloc_mode ~region
     ~body ~stub:true ~inline:Default_inline
-    ~specialise:Default_specialise ~is_a_functor:false
+    ~specialise:Default_specialise ~check:Default_check ~is_a_functor:false
     ~closure_origin:(Closure_origin.create (Closure_id.wrap closure_bound_var))
 
 let register_const t (constant:Flambda.constant_defining_value) name
@@ -650,6 +650,7 @@ and close_functions t external_env function_declarations : Flambda.named =
         ~body ~stub
         ~inline:(Function_decl.inline decl)
         ~specialise:(Function_decl.specialise decl)
+        ~check:(Function_decl.check decl)
         ~is_a_functor:(Function_decl.is_a_functor decl)
         ~closure_origin
     in

middle_end/flambda/closure_conversion_aux.ml

@@ -125,6 +125,7 @@ module Function_decls = struct
     let free_idents t = t.free_idents_of_body
     let inline t = t.attr.inline
     let specialise t = t.attr.specialise
+    let check t = t.attr.check
     let is_a_functor t = t.attr.is_a_functor
     let stub t = t.attr.stub
     let loc t = t.loc

middle_end/flambda/closure_conversion_aux.mli

@@ -73,6 +73,7 @@ module Function_decls : sig
     val body : t -> Lambda.lambda
     val inline : t -> Lambda.inline_attribute
     val specialise : t -> Lambda.specialise_attribute
+    val check : t -> Lambda.check_attribute
     val is_a_functor : t -> bool
     val stub : t -> bool
     val loc : t -> Lambda.scoped_location

middle_end/flambda/export_info_for_pack.ml

@@ -146,6 +146,7 @@ and import_function_declarations_for_pack_aux units pack
           ~stub:function_decl.stub
           ~inline:function_decl.inline
           ~specialise:function_decl.specialise
+          ~check:function_decl.check
           ~is_a_functor:function_decl.is_a_functor
           ~closure_origin:function_decl.closure_origin)
       function_decls.funs

middle_end/flambda/flambda.ml

@@ -137,6 +137,7 @@ and function_declaration = {
   dbg : Debuginfo.t;
   inline : Lambda.inline_attribute;
   specialise : Lambda.specialise_attribute;
+  check : Lambda.check_attribute;
   is_a_functor : bool;
 }
 
@@ -406,8 +407,9 @@ and print_function_declaration ppf var (f : function_declaration) =
     | Never_specialise -> " *never_specialise*"
     | Default_specialise -> ""
   in
-  fprintf ppf "@[<2>(%a%s%s%s%s@ =@ fun@[<2>%a@] ->@ @[<2>%a@])@]@ "
+  fprintf ppf "@[<2>(%a%s%s%s%s%a@ =@ fun@[<2>%a@] ->@ @[<2>%a@])@]@ "
     Variable.print var stub is_a_functor inline specialise
+    Printlambda.check_attribute f.check
     params f.params lam f.body
 
 and print_set_of_closures ppf (set_of_closures : set_of_closures) =
@@ -1042,6 +1044,7 @@ let update_body_of_function_declaration (func_decl: function_declaration)
     stub = func_decl.stub;
     dbg = func_decl.dbg;
     inline = func_decl.inline;
+    check = func_decl.check;
     specialise = func_decl.specialise;
     is_a_functor = func_decl.is_a_functor;
   }
@@ -1056,7 +1059,9 @@ let rec check_param_modes mode = function
 
 let create_function_declaration ~params ~alloc_mode ~region ~body ~stub
       ~(inline : Lambda.inline_attribute)
-      ~(specialise : Lambda.specialise_attribute) ~is_a_functor
+      ~(specialise : Lambda.specialise_attribute)
+      ~(check : Lambda.check_attribute)
+      ~is_a_functor
       ~closure_origin
       : function_declaration =
   begin match stub, inline with
@@ -1090,6 +1095,7 @@ let create_function_declaration ~params ~alloc_mode ~region ~body ~stub
     dbg = dbg_origin;
     inline;
     specialise;
+    check;
     is_a_functor;
   }
 

middle_end/flambda/flambda.mli

@@ -336,6 +336,8 @@ and function_declaration = private {
   (** Inlining requirements from the source code. *)
   specialise : Lambda.specialise_attribute;
   (** Specialising requirements from the source code. *)
+  check : Lambda.check_attribute;
+  (** Check function properties requirements from the source code  *)
   is_a_functor : bool;
   (** Whether the function is known definitively to be a functor. *)
 }
@@ -567,6 +569,7 @@ val create_function_declaration
   -> stub:bool
   -> inline:Lambda.inline_attribute
   -> specialise:Lambda.specialise_attribute
+  -> check:Lambda.check_attribute
   -> is_a_functor:bool
   -> closure_origin:Closure_origin.t
   -> function_declaration

middle_end/flambda/flambda_to_clambda.ml

@@ -578,6 +578,7 @@ and to_clambda_set_of_closures t env
       dbg = function_decl.dbg;
       env = Some env_var;
       mode = set_of_closures.alloc_mode;
+      check = function_decl.check;
     }
   in
   let funs = List.map to_clambda_function all_functions in
@@ -627,6 +628,7 @@ and to_clambda_closed_set_of_closures t env symbol
       dbg = function_decl.dbg;
       env = None;
       mode = Lambda.alloc_heap;
+      check = function_decl.check;
     }
   in
   let ufunct = List.map to_clambda_function functions in

middle_end/flambda/flambda_utils.ml

@@ -364,7 +364,7 @@ let make_closure_declaration
     Flambda.create_function_declaration
       ~params:(List.map subst_param params) ~alloc_mode  ~region
       ~body ~stub ~inline:Default_inline
-      ~specialise:Default_specialise ~is_a_functor:false
+      ~specialise:Default_specialise ~check:Default_check ~is_a_functor:false
       ~closure_origin:(Closure_origin.create (Closure_id.wrap id))
   in
   assert (Variable.Set.equal (Variable.Set.map subst free_variables)

middle_end/flambda/freshening.ml

@@ -326,6 +326,7 @@ module Project_var = struct
             ~body
             ~stub:func_decl.stub
             ~inline:func_decl.inline ~specialise:func_decl.specialise
+            ~check:func_decl.check
             ~is_a_functor:func_decl.is_a_functor
             ~closure_origin:func_decl.closure_origin
         in