flambda-backend: zero alloc: assume on calls (ocaml-flambda#2165)

Author: gretay-js

.depend

@@ -282,6 +282,11 @@ utils/warnings.cmx : \
     utils/misc.cmx \
     utils/warnings.cmi
 utils/warnings.cmi :
+utils/zero_alloc_utils.cmo : \
+    utils/zero_alloc_utils.cmi
+utils/zero_alloc_utils.cmx : \
+    utils/zero_alloc_utils.cmi
+utils/zero_alloc_utils.cmi :
 parsing/ast_helper.cmo : \
     parsing/syntaxerr.cmi \
     parsing/parsetree.cmi \
@@ -3943,25 +3948,36 @@ middle_end/variable.cmi : \
     utils/identifiable.cmi \
     typing/ident.cmi \
     utils/compilation_unit.cmi
+lambda/assume_info.cmo : \
+    utils/zero_alloc_utils.cmi \
+    lambda/assume_info.cmi
+lambda/assume_info.cmx : \
+    utils/zero_alloc_utils.cmx \
+    lambda/assume_info.cmi
+lambda/assume_info.cmi : \
+    utils/zero_alloc_utils.cmi
 lambda/debuginfo.cmo : \
     parsing/location.cmi \
     utils/int_replace_polymorphic_compare.cmi \
     typing/ident.cmi \
     utils/compilation_unit.cmi \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmi \
     lambda/debuginfo.cmi
 lambda/debuginfo.cmx : \
     parsing/location.cmx \
     utils/int_replace_polymorphic_compare.cmx \
     typing/ident.cmx \
     utils/compilation_unit.cmx \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmx \
     lambda/debuginfo.cmi
 lambda/debuginfo.cmi : \
     parsing/location.cmi \
     typing/ident.cmi \
     utils/compilation_unit.cmi \
-    parsing/asttypes.cmi
+    parsing/asttypes.cmi \
+    lambda/assume_info.cmi
 lambda/lambda.cmo : \
     typing/types.cmi \
     typing/typedtree.cmi \
@@ -4231,6 +4247,7 @@ lambda/translattribute.cmo : \
     utils/clflags.cmi \
     parsing/builtin_attributes.cmi \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmi \
     lambda/translattribute.cmi
 lambda/translattribute.cmx : \
     utils/warnings.cmx \
@@ -4244,12 +4261,14 @@ lambda/translattribute.cmx : \
     utils/clflags.cmx \
     parsing/builtin_attributes.cmx \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmx \
     lambda/translattribute.cmi
 lambda/translattribute.cmi : \
     typing/typedtree.cmi \
     parsing/parsetree.cmi \
     parsing/location.cmi \
-    lambda/lambda.cmi
+    lambda/lambda.cmi \
+    lambda/assume_info.cmi
 lambda/translclass.cmo : \
     typing/types.cmi \
     typing/typeopt.cmi \
@@ -4325,6 +4344,7 @@ lambda/translcore.cmo : \
     utils/clflags.cmi \
     typing/btype.cmi \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmi \
     lambda/translcore.cmi
 lambda/translcore.cmx : \
     typing/types.cmx \
@@ -4358,6 +4378,7 @@ lambda/translcore.cmx : \
     utils/clflags.cmx \
     typing/btype.cmx \
     parsing/asttypes.cmi \
+    lambda/assume_info.cmx \
     lambda/translcore.cmi
 lambda/translcore.cmi : \
     typing/types.cmi \

compilerlibs/Makefile.compilerlibs

@@ -53,6 +53,7 @@ UTILS = \
   utils/compilation_unit.cmo utils/linkage_name.cmo utils/symbol.cmo \
   utils/import_info.cmo \
   utils/lazy_backtrack.cmo \
+  utils/zero_alloc_utils.cmo \
   utils/diffing.cmo \
   utils/diffing_with_keys.cmo
 UTILS_CMI = \
@@ -124,6 +125,7 @@ TYPING = \
   typing/typedecl_properties.cmo \
   typing/typedecl_variance.cmo \
   typing/typedecl_separability.cmo \
+  lambda/assume_info.cmo \
   lambda/debuginfo.cmo lambda/lambda.cmo \
   typing/typedecl.cmo \
   typing/typeopt.cmo \

dune

@@ -77,6 +77,7 @@
    local_store target_system compilation_unit import_info linkage_name symbol
    lazy_backtrack diffing diffing_with_keys
    language_extension_kernel language_extension
+   zero_alloc_utils
 
    ;; PARSING
    location longident docstrings printast syntaxerr ast_helper
@@ -98,7 +99,7 @@
    annot outcometree
 
    ;; lambda/
-   debuginfo lambda matching printlambda runtimedef runtimetags tmc simplif switch
+   assume_info debuginfo lambda matching printlambda runtimedef runtimetags tmc simplif switch
    translmode
    transl_comprehension_utils
    transl_array_comprehension transl_list_comprehension
@@ -329,6 +330,7 @@
     (annot.mli as compiler-libs/annot.mli)
     (outcometree.mli as compiler-libs/outcometree.mli)
     (debuginfo.mli as compiler-libs/debuginfo.mli)
+    (assume_info.mli as compiler-libs/assume_info.mli)
     (lambda.mli as compiler-libs/lambda.mli)
     (matching.mli as compiler-libs/matching.mli)
     (printlambda.mli as compiler-libs/printlambda.mli)
@@ -359,5 +361,6 @@
     (compilation_unit.mli as compiler-libs/compilation_unit.mli)
     (linkage_name.mli as compiler-libs/linkage_name.mli)
     (symbol.mli as compiler-libs/symbol.mli)
+    (zero_alloc_utils.mli as compiler-libs/zero_alloc_utils.mli)
 
   ))

lambda/.ocamlformat-enable

@@ -0,0 +1,2 @@
+assume_info.ml
+assume_info.mli

lambda/assume_info.ml

@@ -0,0 +1,103 @@
+(*
+
+   The meaning of keywords [strict] and [never_returns_normally]
+   is defined in terms of abstract values as follows:
+
+   relaxed (default):         nor = Safe and exn = Top  and div = Top
+   strict:                    nor = Safe and exn = Safe and div = Safe
+   never_returns_normally:    nor = Bot  and exn = Top  and div = Top
+
+   where [nor] means normal return of the call, [exn] means return via an exception,
+   [div] means diverging (non-terminating) executions,
+   and the meaning and order of elements is:
+
+   Top    may allocate
+   Safe   does not allocate on any execution paths
+   Bot    unreachable
+
+   Using more than one keyword means intersection (i.e., meet of the  elements,
+   pointwise lifted to tuples), so we get the following:
+
+   [@zero_alloc assume]                               nor = Safe and exn = Top  and div = Top
+   [@zero_alloc assume strict]                        nor = Safe and exn = Safe and div = Safe
+   [@zero_alloc assume strict never_returns_normally] nor = Bot  and exn = Safe and div = Safe
+   [@zero_alloc assume never_returns_normally]        nor = Bot  and exn = Top  and div = Top
+
+   See [Value] and [Annotation] in [backend/checkmach.ml].
+*)
+(* CR gyorsh: should we move [Value] and [Annotation] here or maybe "utils" and use them
+   directly, instead of the weird compare function that abstracts them? Perhaps we
+   should translate "strict" and "never_returns_normally" directly into (nor,exn,div)
+*)
+
+module Witnesses = struct
+  type t = unit
+
+  let join _ _ = ()
+  let meet _ _ = ()
+  let print _ _ = ()
+  let empty = ()
+  let compare _ _ = 0
+end
+
+include Zero_alloc_utils.Make (Witnesses)
+
+type t = No_assume | Assume of Value.t
+
+let compare t1 t2 =
+  match (t1, t2) with
+  | No_assume, No_assume -> 0
+  | Assume v1, Assume v2 -> Value.compare v1 v2
+  | No_assume, Assume _ -> -1
+  | Assume _, No_assume -> 1
+
+let equal t1 t2 = compare t1 t2 = 0
+
+let print ppf = function
+  | No_assume -> ()
+  | Assume v -> Format.fprintf ppf "%a" (Value.print ~witnesses:false) v
+
+let to_string v = Format.asprintf "%a" print v
+
+let join t1 t2 =
+  match (t1, t2) with
+  | No_assume, No_assume -> No_assume
+  | No_assume, Assume _
+  | Assume _, No_assume ->
+      No_assume
+  | Assume t1, Assume t2 -> Assume (Value.join t1 t2)
+
+let meet t1 t2 =
+  match (t1, t2) with
+  | No_assume, No_assume -> No_assume
+  | No_assume, (Assume _ as t)
+  | (Assume _ as t), No_assume ->
+      t
+  | Assume t1, Assume t2 -> Assume (Value.meet t1 t2)
+
+let none = No_assume
+
+let create ~strict ~never_returns_normally =
+  let res =
+    if strict then
+      Value.safe
+    else
+      Value.relaxed Witnesses.empty
+  in
+  let res =
+    if never_returns_normally then
+      { res with nor = V.Bot }
+    else
+      res
+  in
+  Assume res
+
+let get_value t =
+  match t with
+  | No_assume -> None
+  | Assume v -> Some v
+
+let is_none t =
+  match t with
+  | No_assume -> true
+  | Assume _ -> false

lambda/assume_info.mli

@@ -0,0 +1,24 @@
+type t
+
+val none : t
+val create : strict:bool -> never_returns_normally:bool -> t
+val compare : t -> t -> int
+val equal : t -> t -> bool
+val join : t -> t -> t
+val meet : t -> t -> t
+val to_string : t -> string
+val print : Format.formatter -> t -> unit
+val is_none : t -> bool
+
+module Witnesses : sig
+  type t = unit
+
+  val join : t -> t -> t
+  val meet : t -> t -> t
+  val print : Format.formatter -> t -> unit
+  val compare : t -> t -> int
+end
+
+include module type of Zero_alloc_utils.Make (Witnesses)
+
+val get_value : t -> Value.t option