diff --git a/.depend b/.depend index d7a12f33b634..cb5514d3361d 100644 --- a/.depend +++ b/.depend @@ -558,6 +558,7 @@ typing/datarepr.cmo : \ typing/path.cmi \ parsing/location.cmi \ typing/ident.cmi \ + parsing/builtin_attributes.cmi \ typing/btype.cmi \ parsing/asttypes.cmi \ typing/datarepr.cmi @@ -566,6 +567,7 @@ typing/datarepr.cmx : \ typing/path.cmx \ parsing/location.cmx \ typing/ident.cmx \ + parsing/builtin_attributes.cmx \ typing/btype.cmx \ parsing/asttypes.cmi \ typing/datarepr.cmi @@ -1543,18 +1545,31 @@ typing/typedecl_separability.cmi : \ typing/env.cmi typing/typedecl_unboxed.cmo : \ typing/types.cmi \ + typing/printtyp.cmi \ typing/predef.cmi \ + typing/path.cmi \ + parsing/location.cmi \ typing/env.cmi \ typing/ctype.cmi \ + utils/config.cmi \ + utils/clflags.cmi \ + typing/btype.cmi \ typing/typedecl_unboxed.cmi typing/typedecl_unboxed.cmx : \ typing/types.cmx \ + typing/printtyp.cmx \ typing/predef.cmx \ + typing/path.cmx \ + parsing/location.cmx \ typing/env.cmx \ typing/ctype.cmx \ + utils/config.cmx \ + utils/clflags.cmx \ + typing/btype.cmx \ typing/typedecl_unboxed.cmi typing/typedecl_unboxed.cmi : \ typing/types.cmi \ + typing/path.cmi \ typing/env.cmi typing/typedecl_variance.cmo : \ typing/types.cmi \ @@ -3425,6 +3440,8 @@ lambda/matching.cmo : \ typing/types.cmi \ typing/typeopt.cmi \ typing/typedtree.cmi \ + typing/typedecl_unboxed.cmi \ + typing/typedecl.cmi \ lambda/switch.cmi \ typing/printpat.cmi \ lambda/printlambda.cmi \ @@ -3447,6 +3464,8 @@ lambda/matching.cmx : \ typing/types.cmx \ typing/typeopt.cmx \ typing/typedtree.cmx \ + typing/typedecl_unboxed.cmx \ + typing/typedecl.cmx \ lambda/switch.cmx \ typing/printpat.cmx \ lambda/printlambda.cmx \ diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md new file mode 100644 index 000000000000..ba89bffdaa2b --- /dev/null +++ b/HEAD_SHAPE.impl.md @@ -0,0 +1,324 @@ +# Constructor unboxing + +This PR implements a variant of the "constructor unboxing" feature proposed by Jeremy Yallop in [RFC #14](https://github.com/ocaml/RFCs/pull/14), which extends the current `[@@unboxed]` annotation for single-constructor variant types (or single-field record types). The PR was implemented by @nchataing during an internship supervised by @gasche. + +## Short example + +The following is now accepted: + +```ocaml +type bignum = + | Short of int [@unboxed] (* represented directly by an integer *) + | Long of Gmp.t (* Block of tag 0 (first non-unboxed constructor) *) +``` + +In a [small benchmark](https://github.com/gasche/ocaml/pull/10), we tested that this representation provides the same performances as the current Zarith implementation when computations remain in the "short integer" range -- Zarith uses [dirty unsafe tricks](https://github.com/ocaml/Zarith/blob/2be3c25/z.ml#L28-L37) to avoid boxing short integers, which we can replace with [natural OCaml code](https://github.com/gasche/ocaml/blob/head_shape_zarith/Zarith/test.ml#L110-L125). + +(Note: Zarith does not box the Long case either, checking for a Custom tag instead. We do not support this yet, but it would be a natural extension of this PR.) + +The intent of the currently presented work is to do the simplest possible step in the direction of more unboxing. Most advanced aspects were left to future work. We believe that it would be reasonable to integrate the PR with its current feature scope: it provides values for users, and should not hamper further extensions. + +## Precise specification + +See [HEAD_SHAPE.spec.md](HEAD_SHAPE.spec.md). + +## Implementation strategy + +The main components required for this feature are: +1. We need to compute head shape information for unboxed constructors, which in turn requires computing head shape information for whole type. +2. At type-declaration time, we need to check disjointness of head shapes and reject invalid declarations. +3. We need to compile unboxed constructors in expressions. +4. We need to compile unboxed constructors in patterns. + +(3) is in fact very easy: unboxed constructors in expressions are implemented by doing [nothing at all](https://github.com/gasche/ocaml/blob/head_shape/lambda/translcore.ml#L336-L337). + +(1) and (2) proved fairly difficult to implement cleanly due in large part to accidental complexity. + +### Head shapes + +Representing head shapes by their set of possible values is not practical, as `(Imm, _)` (the shape of all immediate values) would be too large a set. Instead we use a representation with an explicit "any" value in either domains (for immediates or for tags): + +```ocaml +(* Over-approximation of the possible values of a type, + used to verify and compile unboxed head constructors. + + We represent the "head" of the values: their value if + it is an immediate, or their tag if is a block. + A head "shape" is a set of possible heads. +*) +and head_shape = + { head_imm : imm shape; (* set of immediates the head can be *) + head_blocks : tag shape; (* set of tags the head can have *) + } + +(* A description of a set of ['a] elements. *) +and 'a shape = + | Shape_set of 'a list (* An element among a finite list. *) + | Shape_any (* Any element (Top/Unknown). *) + +and imm = int +and tag = int +``` + +This definition is found in typing/types.mli: https://github.com/gasche/ocaml/blob/head_shape/typing/types.mli#L624-L642 + +Remark: we tried turning `imm` and `tag` into single-constructor variants for more safety, but this proved very cumbersome as many auxiliary functions happily process either sorts of tags to compute numeric aggregates. + +Remark: in practice we don't know of any use type in OCaml that contains the `(Block, _)` shape without also allowing `(Imm, _)`. (So we could do without `(Block, _)` and have two tops, "any immediate" or "any value whatsoever") No type describes "any block but not immediates". Allowing it in the compiler implementation makes the code more regular, and it could come handy in the future (if we wanted, say, to assign shapes to Cmm-level types) or for weird FFI projects. + +### Compiling unboxed constructors in pattern-matching + +Pattern-matching compilation is done in [lambda/matching.ml](https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml). + +Remark: The other pattern-matching-heavy module, [typing/parmatch.ml](https://github.com/gasche/ocaml/blob/head_shape/typing/parmatch.ml), is in charge of checking for exhaustiveness and other type-checking-time warnings; it required basically no change, given that unboxing a constructor does not change the observable behavior of pattern-matching, unboxed constructors are handled just like usual constructors for exhaustiveness and all other static-analysis purpose. + +The pattern-matching compiler works by decomposing pattern-matching clauses into a lower-level representation built from "switches", a lower-level control-flow construct that just dispatches on the value of immediates and tags of a head block. Those switches are then lowered further to Lambda constructs (`Lifthenelse` + tag accesses, or a native `Lswitch` instruction used for the bytecode compiler). + +A switch is a list of switch clauses, which are of the form `(cstr_tag, action)`, where `cstr_tag` is either an immediate value or a block tag, and actions are pieces of lambda-code. Our implementation adds a new sort of `cstr_tag`, morally `Cstr_unboxed of head_shape` (representation details in the next section); these "unboxed tags" are "expanded away" by replacing clauses witch unboxed tags by clauses for the underlying elements of the head shape. + +For example, consider the following type declarations: + +```ocaml +type internal = Foo | Bar of string [@unboxed] (* head shape: {(Imm, 0); (Block, 252)} *) +type t = First of int | Second of internal [@unboxed] +``` + +An exhaustive switch on a value of type `t` may look like + +```ocaml +| Cstr_block 0 -> act1 +| Cstr_unboxed [{(Imm, 0); (Block, 252)}] -> act2) +``` + +and we expand it to a switch without unboxed constructors, to be compiled by the existing machinery: + +```ocaml +| Cstr_block 0 -> act1 +| Cstr_constant 0 -> act2 +| Cstr_block 252 -> act2 +``` + +This is the general idea, but in fact we need slightly more sophistication to deal with `(Imm, _)` or `(Block, _)` shapes. We change the definition of clauses to contain both: +- either a list of specific actions for some immediates, or an "any" action for all immediates, and +- either a list of specific actions for some block tags, or an "any" action for all blocks + +The code that lowers switches into `Lifthenelse` or `Lswitch` has to be adapted to deal with this new structure. We tried to make it possible/easy to check that, in absence of unboxed constructors, the code generated is the same as it was previously. (The cost of this approach is that sometimes the code is more verbose / less regular than it could be if written from scratch, accepting some changes in compilation.) + +Remark: To emit `Lswitch` instructions, the compiler needs to know of the range of possible immediate values and tags (when we don't have `any_{const,nonconst}` actions). More precisely, we want the maximal possible immediate constructor and block tag at this type (minimal values are always assumed to be 0). + +This new representation of switches with "any immediate" or "any block tag" cases is in a new `Cases` submodule: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2738-L2790 + +The expansion of unboxed constructors in switches is performed in the `split_cases` function: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2792-L2827 + +Finally, the lowering of those switches to Lambda code is done in the `combine_constructor` function: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2914-L3080 + + +### General approach to computing head shapes + +We use the "on-demand" approach advertised by @lpw25 and @stedolan to compute type properties on-demand, at each type declaration with unboxed constructors, instead of trying to compute the property modularly for all type definitions (which may or may not occur in the type of an unboxed constructor later). + +Here "demand" is defined as either: +- a type declaration using some unboxed constructors is processed by the type-checker + (this "demands" computing the shape of each unboxed constructor) +- the pattern-matching compiler encounters an unboxed constructor + +In particular, it can happen that an unboxed-constructor is compiled *without* the type-checker having processed its declaration first! This is the case where the type declaration comes from a .cmi – it has been checked by a previous run of the compiler, and is then imported as-is into the environment without being re-checked. + +The head shape computed for an unboxed constructor is cached on first demand, and will not be recomputed several times. The computation requires a typing environment -- which must be an extension of the environment in which the constructor was defined -- to unfold the definition of typing constructors used in the unboxed constructor parameter type, and further constructions reachable from them. + +The details of how we perform repeated expansion of type constructors while ensuring termination are tricky, they are discussed in [this ML Workshop extended abstract](http://gallium.inria.fr/~scherer/research/constructor-unboxing/constructor-unboxing-ml-workshop-2021.pdf) and [PR #10479](https://github.com/ocaml/ocaml/pull/10479). + +The computation of the head shape is done in the functions `of_type_expr` and `of_typedescr` in a new `Head_shape` module of [typing/typedecl_unboxed.ml](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml). + +In particular, the definition of head shape on "base types" relies on a [`match_primitive`](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L65) function recognized a set of builtin type paths (we borrowed the logic from [Typeopt.classify](https://github.com/gasche/ocaml/blob/head_shape/typing/typeopt.ml#L75)). + +### Storing unboxing information in type descriptions + +This, surprisingly, turned out to be the most difficult part of the PR to get right. + +As discussed above, we need to store two different kind of information for compilation: +- per-unboxed-constructor information: what is the shape of the unboxed constructor argument +- per-sum-type information: how many unboxed constructors are there, + what is the maximal value of the immediates and block tags they contain + +The existing codebase already computes per-constructor information (imm/tag values) and per-sum-type information (the number of constant and non-constant constructors) in [typing/datarepr.ml : constructor_descrs](https://github.com/gasche/ocaml/blob/head_shape_base/typing/datarepr.ml#L95). This function is called (through `Datarepr.constructors_of_type`) from the `Env` module, which is in the business of converting type *declarations* (as provided by the user) into type *descriptions* (with extra information for compilation) as stored in the typing environment. + +Unfortunately, this scheme cannot be extended for our unboxing-related information. Computing the head shape of an unboxed constructor requires unfolding type constructors from the typing environment, so in particular the function doing the computation needs an Env.t argument and depends on the Env module. It cannot be put in the module Datarepr that itself is called from Env, as this would be create a circular dependency. + +We tried many ways to avoid this cyclic dependency (for example we went half-way through large refactorings trying to compute type descriptions in Typedecl, and pass it to Env-extending functions, instead of computing them within Env). + +In the end we settled on a very simple approach: the per-unboxed-constructor information has type `head_shape option ref`, and the per-sum-type information has type `unboxed_type_data option ref`, they are initialized to `ref None` by the Datarepr module, and then filled on-demand -- from a module that *can* depend on Env. Caching the on-demand computation is hidden under accessor-style functions (that fills the cache if the value was not computed yet): +- per-unboxed-constructor information are accessed using [Typedecl_unboxed.Head_shape.get](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L398); it is also computed and cached for all unboxed constructors of a given type by [Typedecl_unboxed.Head_shape.check_typedecl]. +- per-sum-type information is placed in an `unboxed_type_data option ref` [field](https://github.com/gasche/ocaml/blob/head_shape/typing/types.mli#L592) of the `Types.constructor_description` type -- we sheepishly extended the dubious existing approach of storing per-sum-type information in each of its constructors. It is computed by [Typedecl_unboxed.unboxed_type_data_of_shape](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L347). + +Note: the `unboxed_type_data option ref` field is not meant to be accessed directly, but through helper functions in Typedecl, that export its content as fields: + +```ocaml +cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option +cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option +cstr_unboxed_numconsts : Env.t -> constructor_description -> int option +cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option +``` + +Morally those are fields of a constructor description; the main difference is that, unlike other fields, they can only be computed "later than Datarepr", when a typing environment is available. We first tried having each of them be a mutable field, but this made it difficult to give a type to a function computing all of them at once, as [unboxed_type_data_of_shape] does. + +## Testing + +TODO: describe our testing approach and testsuite + +## In scope for this PR, but not yet implemented + +We are submitting this PR in the interest of gathering feedback, and getting the review train rolling. (We know it takes a while from people reading about the work to actually reviewing it. Please start right now!) There are still a few things *we* want to changes before we consider it mergeable -- and surely other suggestions from the reviewers. + + +### Handle cyclic types in the termination checker + +The termination-checking algorithm currently does not take cyclic +types into account, and may non-terminate on those. This should be +fixed easily by keeping track of the set of type nodes we have already +encountered in head position during reduction. + + +### Distinguish "good" from "bad" cycles + +Our cycle-detection algorithm will sometimes reject definitions that indeed are cyclic, but do admit a valid fixpoint: + +```ocaml +(* this bad declaration should be rejected *) +type t = Loop of t [@unboxed] | Other +(* because `Other` and `Loop Other` would have the same representation *) + +(* this weird declaration could be accepted +type t = Loop of t [@unboxed] +(* because it is just an empty type *) +``` + +"Good cycle" types have no value of their own and they can go to hell as far as we are concerned. However, Stephen Dolan (@stedolan) pointed out that they can be introduced by revealing the definition of an abstract type: `type t = Loop of abstract [@unboxed]` (accepted, even though we could have `abstract = t`). This introduces a case where revealing type abstractions makes a definition rejected, breaking some reasonable properties of the type system. + +It would be nice to put in the work to distinguish "good cycles" from "bad cycles" to avoid this small defect of the current strategy of rejecting *all* cycles. + + +### Enforce "separability" of resulting types + +It is unsound in presence of the flat-float-array optimization to have types that contain both floating-point values and non-floating-point values. Our current approach does not enforce this, so it will allow this unsound definition: + +```ocaml +type t = Float of float [@unboxed] | Other +``` + +One possibility to fix this: +- Extend the domain of shapes, in addition to "imm" and "block" we add a "separated" domain, which is a single bit (true/false), which indicates whether the set of values we approximate is separated. + (a set of OCaml values is "separated" if it contains either (1) only `float` values or (2) no `float` value.) +- When taking the disjoint union of two shapes, compute the "separated" bit (take the conjunction of the two input bits, and also set to 'false' if the resulting domain contains both 'Obj.double_tag' and something else). +- Existential variables of GADT constructors do not get the current "top" shape (separated=true), but a "non-separated top" with separated=false. +- If a type declaration has a non-separated final shape, reject the declaration. + +Question: would it be possible to just get rid of the current separability computation for type declarations, and use this shape analysis instead? (This would be a nice simplification to the type-checker codebase.) We could try this by implementing this logic, disabling the pre-existing 'separability' check, and running the separability testsuite. + +Remark: without this extension, shapes have a natural denotational semantics, where each shape is interpreted by a set of OCaml values. + + interp(s) = { v | head(v) ∈ s } + +With this extension, shapes can be interpreted as *sets of sets* of OCaml values: + + interp(s) = { S | ∀v∈S, head(v) ∈ s /\ s.separated <=> is_separated(S) } + +## Future work + +We know about some improvements that we are interested in working on eventually, but we believe are out of scope for this PR. + +### Nice shape-conflict error messages + +If a type definition is rejected due to shape conflict, it would be nice to give a clear explanation to the user, with the location of the two constructors (possibly both in different variant declarations than the one being checked) that introduce the incompatibility. One way to do this is to track, for each part of the shape, the location of the constructor that introduced it in the shape. + +### GADTs + +Finer-grained shape computations for GADTs: to compute the shape of a type `foo t` when `t` is a GADT, instead of taking the disjoint union of the shape of all constructors, we can filter only the constructors that are "compatible" with `foo` (we cannot prove that the types are disjoint). This is simple enough and gives good, interesting results in practice, but it also requires refining the termination-checking strategy for GADTs (in addition to the head type constructor, we need to track the set of compatible constructors for the particular expansion that was done). For now we punt on this by not doing any special handling of GADTs, even though it is less precise. + + +### Shape annotations on abstract types + +If an abstract type is meant to be defined through the FFI, the OCaml-side could come with an annotation restricting its shape from the pessimal default "{ (Imm, _); (Block, _) }" to the actual shape of FFI-produced values for this type. This requires blindly trusting the programmer, but this blind trust is the foundation of our FFI model already. + +Having shape annotations on abstract types means that shape-inclusion has to be checked when verifying that a type definition in a module matches a type declaration in its interface. (Currently we don't have any work there, because means of abstractions always either preserve the head shape or turn it into "top".) + +### Arity tracking + +Another information we could add to our "head shape" approximation is the size of the block. For example, in theory we could allow this: + +```ocaml +type 'a pair = ('a * 'a) +type 'a triple = ('a * 'a * 'a) + +type 'a t = + | Pair of 'a pair [@unboxed] (* tag 0, size 2 *) + | Triple of 'a triple [@unboxed] (* tag 0, size 3 *) +``` + +### Compilation strategy + +The pattern-matching compilation strategy could be improved in some cases, at the cost of substantial changes to our current implementation. Consider `type t = Int of int [@unboxed] | String of string [@unboxed] and u = T of t [@unboxed] | Float of float [@unboxed]`. A matching of the form + +```ocaml +match arg with +| Float _ -> 0 +| T (Int _) -> 1 +| T (String _) -> 2 +``` + +will generate two nested switches: + +``` +match-shape arg with +| (Block, Obj.double_tag) -> 0 +| (Imm, _) | (Block, Obj.string_tag) -> + match-shape arg with + | (Imm, _) -> 1 + | (Block, Obj.string_tag) -> 2 +``` + +(This is the exact same generated-code shape that we would have without unboxing, except that one dereference is gone, but the first switch is now more expensive as the now-unboxed input values are not in a small consecutive interval of tags.) + +It would of course be better to generate a single switch instead. We see two approaches to do this: + +1. We could "merge" some switches after the fact. +2. We could remove unboxed constructors much earlier in the pattern-matching compiler, before matrix decomposition, so that morally `T (Int _)` is handled as having a single head constructor `T ∘ Int`. + +We are not considering either of those ambitious changes a priority, because: +1. We expect the performance wins from unboxing (if any) to come from tighter memory representations; + the pattern-matching branches are comparatively unexpansive +2. In practice most examples of unboxed constructors we have in mind do *not* hit this bad situation. + +In particular, if you unboxed a constructor with only immediate +values, then the generated code will split the query space by checking +`Obj.is_int`, which is the optimal strategy in any case (what the +native compiler will do for the merged switch as well). For example, +these produce exactly the same native code: + +```ocaml +(* what we get today *) +match-shape arg with +| (Imm, _) -> -1 +| (Block, 0) | (Block, 1) -> + match-shape arg with + | (Block, 0) -> 0 + | (Block, 1) -> 1 + +(* what switch-merging would give *) +match-shape arg with +| (Imm, _) -> -1 +| (Block, 0) -> 0 +| (Block, 1) -> 1 +``` + +The two forms get compiled to the following + +```ocaml +if Obj.is_int arg then -1 +else match Obj.tag arg with + | 0 -> 0 + | 1 -> 1 +``` \ No newline at end of file diff --git a/HEAD_SHAPE.spec.md b/HEAD_SHAPE.spec.md new file mode 100644 index 000000000000..fc055b8a21cf --- /dev/null +++ b/HEAD_SHAPE.spec.md @@ -0,0 +1,159 @@ +# Constructor unboxing specification + +We (@nchataing as intern, @gasche as advisor) implemented a variant of @yallop's constructor-unboxing specification as an experimental branch that we would now like to discuss and consider for upstreaming. + +Our intent was to implement the simplest possible form of unboxing in presence of several constructors, and leave more advanced aspects -- anything that could be left off -- to further work. + +We support a per-constructor `[@unboxed]` attribute, that can be used in a variant type as long as the set of values corresponding to each constructor (boxed or unboxed) remain disjoint. + +For example: + +```ocaml +type bignum = + | Short of int [@unboxed] (* represented directly by an integer *) + | Long of Gmp.t (* Block of tag 0 (first non-unboxed constructor) *) +``` + +## Precise specification + +We define the *head* of an OCaml value as follows: +- the head of an immediate value `v` is the pair `(Imm, v)` +- the head of a heap block with tag `t` is the pair `(Block, t)`. + +(In other words, the head tracks whether a value is immediate or a block, and for blocks only keeps the tag.) + +The "head shape" of a type is a (slight over-approximation of) the set of heads of all possible values of this type. + +Now consider a variant type declaration containing one or several constructors annotated with `[@unboxed]`: + +```ocaml +type ('a, 'b, ...) t = + | Const0 (* some constant constructors *) + | Const1 + | ... + | Const{m} + | NonConst0 of t00 * t01 * ... + | Nonconst1 of t10 * t11 * ... + | ... + | NonConst{n} of t{n}0 * t{n}1 * ... + | Unboxed1 of u0 [@unboxed] + | Unboxed2 of u1 [@unboxed] + | ... + | Unboxed{l} of u{l} [@unboxed] +``` + +(For simplicity we wrote above all constant constructors first, then all non-constant constructors then all unboxed constructors. But in fact we support arbitrary interleaving of these categories, and the representation is exactly the same as long as the ordering within constant constructors and within non-constant constructors is preserved.) + +The compiled representation of this type is as follows: +- as before, constant constructors `Const{k}` are represented by the immediate number `k` +- as before, non-constant constructors `Nonconst{k} of ...` are represented by a heap block with tag `k` +- unboxed constructors `Unboxed{k} of u{k}` are represented directly by the value of type `u{k}`, without + any boxing + +This definition is *rejected* statically if the unboxed constructors overlap with the other values of the type, in the following precise sense: + +1. We compute the "boxed head shape" `BS` of this type *without* the unboxed constructors; by definition of the head shape, this is the set `{(Imm, 0), (Imm, 1), ..., (Imm, m)} ∪ {(Block, 0), (Block, 1), ,.., (Block, n)}`. + +2. Then we compute the "unboxed shapes" `US{k}` of each unboxed constructor, that is the head shape of `u{k}`. + +3. The type is accepted if and only if the shapes `BS, US0, US1, ..., US{l}` are disjoint from each other. The head shape of the whole shape is then the disjoint union `BS ⊎ US0 ⊎ US1 ⊎ ... ⊎ US{l}`. + +Unknown/abstract types are assumed to have a "top" shape with containing potentially all heads. (This should be refined when the abstract type is used to represent an FFI type with a precise shape implemented in C; supporting head shape assertions on abstract types is future work.) + + +## Examples + +```ocaml +(* rejected *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Unit (* shape: (Imm, 0), conflicts with Int above *) + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Box of t (* shape: (Block, 0), as the first non-constant non-unboxed constructor *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* accepted *) +type prod = t * t +and t = + | Int of int [@unboxed] (* shape: (Imm, _): any immediate *) + | String of string [@unboxed] (* shape: (Block, Obj.string_tag) (Obj.string_tag is 252) *) + | Prod of prod [@unboxed] (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0), (Block, Obj.string_tag)} *) + + +(** With abstract types *) + +type abstract + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Abs of abstract (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t = + | Int of int (* shape: (Block, 0) *) + | Abs of abstract [@unboxed] (* any shape, conflicts with Int *) + + +(** Nested unboxing *) + +type t1 = + | Int of int [@unboxed] + | Block of unit + (* shape(t1): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t2 = + | T1 of t1 [@unboxed] (* shape: (Imm, _) ∪ {(Block, 0)} *) + | S of string (* shape: (Block, 0), conflicts with T1 *) + +(* accepted *) +type t3 = + | T1 of t1 [@unboxed] (* shape: {(Imm, _), (Block, 0)} *) + | S of string [@unboxed] (* shape: (Block, Obj.stringₜag) *) + (* shape(t3): (Imm, _) ∪ {(Block, 0)} ∪ {(Block, Obj.string_tag)} *) +``` + + +### Comparison with Yallop's proposal [RFC#14](https://github.com/ocaml/RFCs/pull/14) + +Jeremy Yallop's proposal uses a global annotation `[@@unboxed]` on all constructors at once, we use a per-constructor annotation `[@unboxed]`. (The RFC mentions this as a possible extension in "Extension: partial unboxing".) It would be easy to interpret `[@@unboxed]` as just "[@unboxed] on all constructors", but we have not implemented this yet. + +A major difference is that the RFC#14 specification suggests renumbering constructors in some cases, where the representation of `C of foo [@unboxed]` is taken to be different from the representation of `foo`, in order to avoid conflicts with other constructors at this type. We do not support any such renumbering: +- the representation of `Unboxed of foo [@unboxed]` is always the representation of `foo` +- the representation of `Boxed of foo` always uses the block tag consecutive/next/succedent to the previous boxed-constructor tag in the declaration (filtering out unboxed constructors). + +(Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) + + +## separability + +When the compiler is in `flat-float-array` mode, soundness relies on the property that all OCaml types are "separated": they contain either (1) only `float` values, or (2) no `float` value. New forms of unboxing must preserve this property. + +We can track separatedness as part of the head-shape computation for unboxed type declaration, by adding to head-shape data a "separated" bit (see the details in [HEAD_SHAPE.impl.md](HEAD_SHAPE.impl.md)). We reject type declarations whose head-shape is not separated (when in `flat-float-array` mode). + +It may be that this tracking is precise enough to entirely replace the pre-existing "separability analysis" of the type-checker. We have not implemented it yet, and have not evaluated this possibility. + + +## Leftover question: how close to the compiler-distribution runtime should the specification be? + +We define static accept/reject decisions for partially-unboxed types using "head shapes", which are defined in terms of the value-representation strategy of the main OCaml implementation. Should we have a more abstract definition, that leaves more room to other representations in alternative implementations? + +We have not studied this question yet and we believe it is a pressing question. In particular, any choice that would end up being merged in the language probably MUST support the js_of_ocaml value representation. (Do you know of a reference document that describes the js_of_ocaml value representation? Pointers are welcome are we are not jsoo experts ourselves. cc @hhugo.) + +Our intuition is that we could fine a "weakening" of our current specification that distinguishes less different sort of shapes -- thus rejects more definitions -- and gives good flexibility for alternative implementations. Here are some things we could do: + +- We could stop making assumptions about the shape of function closures (currently: {Closure_tag, Infix_tag}), preventing the unboxing of closure-holding constructors. +- We could also weaken our assumptions about built-in containers (string/byte, arrays, double-arrays, etc.) +- We could stop distinguishing "float" from immediates (ouch!) if jsoo does this. What about Int32, Int64, should they be known as custom values? + +In other words: what amount of runtime type information should we require from OCaml implementations? + +At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for language implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. + +This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @yallop, @stedolan, @lpw25, @let-def, etc.). diff --git a/driver/main_args.ml b/driver/main_args.ml index 07acf216439d..70dc20219192 100644 --- a/driver/main_args.ml +++ b/driver/main_args.ml @@ -844,6 +844,10 @@ let mk_dinterval f = "-dinterval", Arg.Unit f, " (undocumented)" ;; +let mk_dheadshape f = + "-dheadshape", Arg.Unit f, " (undocumented)" +;; + let mk_dstartup f = "-dstartup", Arg.Unit f, " (undocumented)" ;; @@ -950,6 +954,7 @@ module type Core_options = sig val _dtypedtree : unit -> unit val _drawlambda : unit -> unit val _dlambda : unit -> unit + val _dheadshape : unit -> unit end @@ -1244,6 +1249,7 @@ struct mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; mk_drawlambda F._drawlambda; + mk_dheadshape F._dheadshape; mk_dlambda F._dlambda; mk_dinstr F._dinstr; mk_dcamlprimc F._dcamlprimc; @@ -1310,6 +1316,7 @@ struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_dlambda F._dlambda; mk_dinstr F._dinstr; @@ -1441,6 +1448,7 @@ struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_dlambda F._dlambda; mk_drawclambda F._drawclambda; @@ -1551,6 +1559,7 @@ module Make_opttop_options (F : Opttop_options) = struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_drawclambda F._drawclambda; mk_dclambda F._dclambda; @@ -1715,6 +1724,7 @@ module Default = struct let _drawlambda = set dump_rawlambda let _dsource = set dump_source let _dtypedtree = set dump_typedtree + let _dheadshape = set dump_headshape let _dunique_ids = set unique_ids let _dno_unique_ids = clear unique_ids let _dlocations = set locations @@ -1747,6 +1757,7 @@ module Default = struct let _dflambda_verbose () = set dump_flambda (); set dump_flambda_verbose () let _dinterval = set dump_interval + let _dheadshape = set dump_headshape let _dinterf = set dump_interf let _dlinear = set dump_linear let _dlive () = dump_live := true diff --git a/driver/main_args.mli b/driver/main_args.mli index 236111d33d79..aa25e20ed5f6 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -67,6 +67,7 @@ module type Core_options = sig val _dtypedtree : unit -> unit val _drawlambda : unit -> unit val _dlambda : unit -> unit + val _dheadshape : unit -> unit end diff --git a/lambda/matching.ml b/lambda/matching.ml index 0e143dd6a61d..715aaf91e056 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -1777,7 +1777,7 @@ let get_expr_args_constr ~scopes head (arg, _mut) rem = | Cstr_constant _ | Cstr_block _ -> make_field_accesses Alias 0 (cstr.cstr_arity - 1) rem - | Cstr_unboxed -> (arg, Alias) :: rem + | Cstr_unboxed _ -> (arg, Alias) :: rem | Cstr_extension _ -> make_field_accesses Alias 1 cstr.cstr_arity rem let divide_constructor ~scopes ctx pm = @@ -2734,20 +2734,103 @@ let combine_constant loc arg cst partial ctx def in (lambda1, Jumps.union local_jumps total) -let split_cases tag_lambda_list = + +(* The [split_cases] function below is in charge of taking a shallow + pattern-matching on a variant type, and splitting the corresponding + constructor+action pairs into constant constructor cases and + non-constant constructor cases. + + In the presence of unboxed constructors: + + - A matching on a single source-level unboxed constructor may turn + into several cases, one for each possible head of the constructor + parameter. + + - If the head shape of an unboxed constructor contains Shape_any + (for immediate values or block tags), it must be compiled + specially. + + The Cases.t datastructure tracks such [any_const] or [any_nonconst] + actions. Note that if [any_const] is Some, then [consts] must be empty. +*) +module Cases = struct + type 'k domain_cases = + | Any of lambda + | Set of ('k * lambda) list + + let add_case k act = function + | Any _ -> invalid_arg "Cases.add_case: Any" + | Set li -> Set ((k, act) :: li) + + let add_any act = function + | Set [] -> Any act + | Any _ -> invalid_arg "Cases.add_any: already Any" + | Set (_ :: _) -> invalid_arg "Cases.add_any: Set (_ :: _)" + + let sort_domain = function + | Any act -> Any act + | Set li -> Set (sort_int_lambda_list li) + + type t = { + consts: imm domain_cases; + nonconsts: tag domain_cases; + } + + let empty = { + consts = Set []; + nonconsts = Set []; + } + + let add_const tag act cases = + { cases with consts = add_case tag act cases.consts } + + let add_nonconst tag act cases = + { cases with nonconsts = add_case tag act cases.nonconsts } + + let add_any_const act cases = + { cases with consts = add_any act cases.consts } + + let add_any_nonconst act cases = + { cases with nonconsts = add_any act cases.nonconsts } + + let sort cases = { + consts = sort_domain cases.consts; + nonconsts = sort_domain cases.nonconsts; + } +end + +let split_cases pat_env tag_lambda_list = let rec split_rec = function - | [] -> ([], []) + | [] -> Cases.empty | (cstr_tag, act) :: rem -> ( - let consts, nonconsts = split_rec rem in + let cases = split_rec rem in match cstr_tag with - | Cstr_constant n -> ((n, act) :: consts, nonconsts) - | Cstr_block n -> (consts, (n, act) :: nonconsts) - | Cstr_unboxed -> (consts, (0, act) :: nonconsts) + | Cstr_constant n -> Cases.add_const n act cases + | Cstr_block n -> Cases.add_nonconst n act cases + | Cstr_unboxed cache -> + let head_shape = + Typedecl_unboxed.Head_shape.get pat_env cache + in + let cases = + match head_shape.head_imm with + | Shape_set s -> + List.fold_left + (fun cases n -> Cases.add_const n act cases) + cases s + | Shape_any -> Cases.add_any_const act cases + in + let cases = + match head_shape.head_blocks with + | Shape_set s -> + List.fold_left + (fun cases n -> Cases.add_nonconst n act cases) + cases s + | Shape_any -> Cases.add_any_nonconst act cases + in cases | Cstr_extension _ -> assert false ) in - let const, nonconst = split_rec tag_lambda_list in - (sort_int_lambda_list const, sort_int_lambda_list nonconst) + Cases.sort (split_rec tag_lambda_list) let split_extension_cases tag_lambda_list = let rec split_rec = function @@ -2762,6 +2845,17 @@ let split_extension_cases tag_lambda_list = in split_rec tag_lambda_list +let split_variant_cases pat_env tag_lambda_list = + let Cases.{consts; nonconsts} = + split_cases pat_env tag_lambda_list in + match consts, nonconsts with + | Any _, _ | _, Any _ -> + (* We assume there are no unboxed constructors + for polymorphic variants *) + assert false + | Set consts, Set nonconsts -> + (consts, nonconsts) + let combine_constructor loc arg pat_env cstr partial ctx def (descr_lambda_list, total1, pats) = let tag_lambda (cstr, act) = (cstr.cstr_tag, act) in @@ -2807,7 +2901,8 @@ let combine_constructor loc arg pat_env cstr partial ctx def | _ -> (* Regular concrete type *) let ncases = List.length descr_lambda_list - and nconstrs = cstr.cstr_consts + cstr.cstr_nonconsts in + and nconstrs = + cstr.cstr_consts + cstr.cstr_nonconsts + cstr.cstr_unboxed in let sig_complete = ncases = nconstrs in let fail_opt, fails, local_jumps = if sig_complete then @@ -2819,47 +2914,155 @@ let combine_constructor loc arg pat_env cstr partial ctx def mk_failaction_pos partial constrs ctx def in let descr_lambda_list = fails @ descr_lambda_list in - let consts, nonconsts = - split_cases (List.map tag_lambda descr_lambda_list) in let lambda1 = match (fail_opt, same_actions descr_lambda_list) with | None, Some act -> act (* Identical actions, no failure *) | _ -> ( + let cases = split_cases pat_env + (List.map tag_lambda descr_lambda_list) in match - (cstr.cstr_consts, cstr.cstr_nonconsts, consts, nonconsts) + (cstr.cstr_consts, cstr.cstr_nonconsts, cases) with - | 1, 1, [ (0, act1) ], [ (0, act2) ] -> + | 1, 1, { consts = Set [ (0, act1) ]; nonconsts = (Set [ (0, act2) ]) } + | 1, 0, { consts = Set [ (0, act1) ]; nonconsts = Any act2 } -> (* Typically, match on lists, will avoid isint primitive in that - case *) + case *) Lifthenelse (arg, act2, act1) - | n, 0, _, [] -> + | n, 0, { consts; nonconsts= Set []; } -> (* The type defines constant constructors only *) - call_switcher loc fail_opt arg 0 (n - 1) consts - | n, _, _, _ -> ( - let act0 = - (* = Some act when all non-const constructors match to act *) - match (fail_opt, nonconsts) with - | Some a, [] -> Some a - | Some _, _ -> - if List.length nonconsts = cstr.cstr_nonconsts then - same_actions nonconsts + begin match consts with + | Any act -> act + | Set consts -> + call_switcher loc fail_opt arg 0 (n - 1) consts + end + | n, _, _ -> ( + let single_action cases complete_case_count = + (* = Some act when all actions are the same, + either on constant or non-constant domain. + + [any_case] is either [any_const] or + [any_nonconst]; it is None if all values of this + domain are accepted. In this case + complete_case_count is also None, otherwise it + must be the total number of heads at this domain. + *) + let same_actions cases = + match same_actions cases with + | Some act -> Ok act + | None -> Error cases + in + match (fail_opt, cases) with + | Some act, Cases.Set [] + | _, Cases.Any act -> Ok act + | None, Cases.Set cases -> + same_actions cases + | Some _, Cases.Set cases -> + (* if any_case is None, complete_case_count + must be Some *) + let count = Option.get complete_case_count in + if List.length cases = count then + same_actions cases else - None - | None, _ -> same_actions nonconsts + Error cases in - match act0 with - | Some act -> - Lifthenelse - ( Lprim (Pisint, [ arg ], loc), - call_switcher loc fail_opt arg 0 (n - 1) consts, - act ) - | None -> - (* Emit a switch, as bytecode implements this sophisticated - instruction *) + (* [numconsts] and [numnonconsts] count the number + of valid head constructors at this type in the domain + (only constant constructors, or only + non-constant constructors). *) + let single_const_act = + let numconsts = + Typedecl.cstr_unboxed_numconsts pat_env cstr in + single_action cases.consts numconsts + in + let single_nonconst_act = + let numnonconsts = + Typedecl.cstr_unboxed_numnonconsts pat_env cstr in + single_action cases.nonconsts numnonconsts + in + let test_isint const_act nonconst_act = + Lifthenelse + ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) + in + (* We check specifically for single_nonconst_act, not for + single_const_act: for constant constructors we can generate + better code than a switch in some cases, but for tests on + non-constant constructors we prefer to always emit a switch, + as bytecode implements this sophisticated instruction. *) + match single_nonconst_act, cases.consts with + | Ok nonconst_act, _ -> + (* Note: we already checked that not all actions are + identical, so the constant-constructor actions cannot + be empty. *) + let int_actions = + match single_const_act with + | Ok const_act -> const_act + | Error const_acts -> + call_switcher loc fail_opt arg 0 (n - 1) const_acts + in test_isint int_actions nonconst_act + | Error nonconsts, Set consts -> + (* Switch is a low-level control-flow construct that must + handle an interval of contiguous values (on + both domains); [sw_numconsts] and [sw_numblocks] + correspond to the size of this interval, from 0 to the + maximum head value + 1. *) + let sw_numconsts = + match Typedecl.cstr_max_imm_value pat_env cstr with + | Some n -> n + 1 + | None -> + (* cases.any_const is None *) + assert false + in + let sw_numblocks = + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> + n + 1 + (* Remark: in presence of constructor unboxing, + some block tags may be above + Obj.last_non_constant_constructor_tag (245): + + type t = + | Unit of unit (* tag 0 *) + | Bool of bool (* tag 1 *) + | String of string [@unboxed] + (* tag String_tag = 252 *) + + With the native-code compiler, the Switcher + will cluster the cases into two dense clusters + and generate good code. But in bytecode, the compiler + will always produce a single Switch instruction, + generating a switch of around 256 cases, which is + wasteful. + + We are not sure how to generate better code + -- for example, generating a test for tags above 245 + may duplicate the computation of the value tag. + + TODO: try the following strategy: here (in + this function), if we detect that max_block_tag is + above 245, generate either + + if isint v then + + else let n = Obj.tag v in + + + This should generate slower bytecode, but much more + compact bytecode. (slower: typically 2-4 instructions + executed instead of 1) (more compact: typically + ~10 integers instead of ~256) + *) + + | None -> + (* single_nonconst_act is None, so there must be at + least two distinct non-constant actions, + any_nonconst is impossible. *) + assert false + in let sw = - { sw_numconsts = cstr.cstr_consts; + { sw_numconsts; sw_consts = consts; - sw_numblocks = cstr.cstr_nonconsts; + sw_numblocks; sw_blocks = nonconsts; sw_failaction = fail_opt } @@ -2867,6 +3070,27 @@ let combine_constructor loc arg pat_env cstr partial ctx def let hs, sw = share_actions_sw sw in let sw = reintroduce_fail sw in hs (Lswitch (arg, sw, loc)) + | Error nonconsts, Any const_act -> + (* Generate a switch on nonconst_act under a Pisint test + to handle the any_const action *) + let sw_numblocks = + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> n + 1 + | None -> assert false (* same as above *) + in + let nonconst_act = + Lswitch + ( arg, + { sw_numconsts = 0; + sw_consts = []; + sw_numblocks; + sw_blocks = nonconsts; + sw_failaction = fail_opt; + }, + loc + ) + in + test_isint const_act nonconst_act ) ) in @@ -2888,7 +3112,8 @@ let call_switcher_variant_constr loc fail arg int_lambda_list = Lprim (Pfield 0, [ arg ], loc), call_switcher loc fail (Lvar v) min_int max_int int_lambda_list ) -let combine_variant loc row arg partial ctx def (tag_lambda_list, total1, _pats) +let combine_variant loc row arg pat_env partial ctx def + (tag_lambda_list, total1, _pats) = let row = Btype.row_repr row in let num_constr = ref 0 in @@ -2920,7 +3145,8 @@ let combine_variant loc row arg partial ctx def (tag_lambda_list, total1, _pats) else mk_failaction_neg partial ctx def in - let consts, nonconsts = split_cases tag_lambda_list in + let (consts, nonconsts) = + split_variant_cases pat_env tag_lambda_list in let lambda1 = match (fail, one_action) with | None, Some act -> act @@ -3304,7 +3530,7 @@ and do_compile_matching ~scopes repr partial ctx pmh = compile_test (compile_match ~scopes repr partial) partial (divide_variant ~scopes !row) - (combine_variant ploc !row arg partial) + (combine_variant ploc !row arg ph.pat_env partial) ctx pm ) | PmVar { inside = pmh } -> diff --git a/lambda/translcore.ml b/lambda/translcore.ml index e9a3f659ee91..84874ec65ff4 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -333,7 +333,7 @@ and transl_exp0 ~in_new_scope ~scopes e = end else begin match cstr.cstr_tag with Cstr_constant n -> Lconst(const_int n) - | Cstr_unboxed -> + | Cstr_unboxed _ -> (match ll with [v] -> v | _ -> assert false) | Cstr_block n -> begin try diff --git a/testsuite/tests/letrec-check/unboxed.ml b/testsuite/tests/letrec-check/unboxed.ml index 7c04199ec986..0449e01bbe5e 100644 --- a/testsuite/tests/letrec-check/unboxed.ml +++ b/testsuite/tests/letrec-check/unboxed.ml @@ -20,14 +20,18 @@ Line 2, characters 12-19: Error: This kind of expression is not allowed as right-hand side of `let rec' |}];; +(* Note: this declaration is currently rejected by the + termination criterion, but ideally we would want to allow it + as it is a case of benign cycle that can occur by revealing + an abstract type. See #10485. *) type r = A of r [@@unboxed] let rec y = A y;; [%%expect{| -type r = A of r [@@unboxed] -Line 2, characters 12-15: -2 | let rec y = A y;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of `let rec' +Line 1, characters 0-27: +1 | type r = A of r [@@unboxed] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + r/95[3] appears unboxed at the head of its own definition. |}];; (* This test is not allowed if 'a' is unboxed, but should be accepted diff --git a/testsuite/tests/tool-toplevel/printval.ml b/testsuite/tests/tool-toplevel/printval.ml index 17c2744440b9..b7f220dd3ba6 100644 --- a/testsuite/tests/tool-toplevel/printval.ml +++ b/testsuite/tests/tool-toplevel/printval.ml @@ -58,3 +58,34 @@ T 'x' type _ t += T : 'a -> ('a * bool) t - : (char * bool) t = T 'x' |}] + + +(* printing of unboxed constructors *) +type t = + | Int of int [@unboxed] + | Str of string [@unboxed] + | Pair of t * t + | Proxy of t +;; +[%%expect {| +type t = + Int of int [@unboxed] + | Str of string [@unboxed] + | Pair of t * t + | Proxy of t +|}];; + +Int 42;; +[%%expect {| +- : t = Int 42 +|}];; + +Str "foo";; +[%%expect {| +- : t = Str "foo" +|}];; + +Pair (Int 42, Proxy (Str "foo"));; +[%%expect {| +- : t = Pair (Int 42, Proxy (Str "foo")) +|}] diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index 5e81a3d75faa..32e32a7859fe 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -94,14 +94,19 @@ Error: This type cannot be unboxed because (* let rec must be rejected *) type t10 = A of t10 [@@ocaml.unboxed];; [%%expect{| -type t10 = A of t10 [@@unboxed] +Line 1, characters 0-37: +1 | type t10 = A of t10 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + t10/188[22] appears unboxed at the head of its own definition. |}];; let rec x = A x;; [%%expect{| -Line 1, characters 12-15: +Line 1, characters 14-15: 1 | let rec x = A x;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of `let rec' + ^ +Error: This expression has type t1 but an expression was expected of type + string |}];; (* Representation mismatch between module and signature must be rejected *) @@ -260,17 +265,29 @@ in assert (f x = L 3.14);; (* Check for a potential infinite loop in the typing algorithm. *) type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; [%%expect{| -type 'a t12 = M of 'a t12 [@@unboxed] +Line 1, characters 0-43: +1 | type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + t12/553[43] appears unboxed at the head of its own definition. |}];; let f (a : int t12 array) = a.(0);; [%%expect{| -val f : int t12 array -> int t12 = +Line 1, characters 15-18: +1 | let f (a : int t12 array) = a.(0);; + ^^^ +Error: Unbound type constructor t12 +Hint: Did you mean t1, t11 or t2? |}];; (* Check for another possible loop *) type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; [%%expect{| -type t13 = A : 'a t12 -> t13 [@@unboxed] +Line 1, characters 17-20: +1 | type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; + ^^^ +Error: Unbound type constructor t12 +Hint: Did you mean t1, t11, t13 or t2? |}];; diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml new file mode 100644 index 000000000000..7e9de2a0dd6c --- /dev/null +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml @@ -0,0 +1,74 @@ +(* TEST + flags = "-dheadshape" + * expect +*) + +(* Check the unboxing of constructors *) +type t = A of int | B;; +[%%expect{| +SHAPE(t/88[1]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0]; head_separated = true} +type t = A of int | B +|}];; + +type t = A of int | B of float | C | D;; +[%%expect{| +SHAPE(t/91[2]) {head_imm = Shape_set [0; 1]; head_blocks = Shape_set [0; 1]; head_separated = true} +type t = A of int | B of float | C | D +|}];; + +type t = A of int [@unboxed] | B;; +[%%expect{| +SHAPE(t/96[3]) CONFLICT +Line 1, characters 0-32: +1 | type t = A of int [@unboxed] | B;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This declaration is invalid, some [@unboxed] annotations introduce + overlapping representations. +|}];; + +type t = A of float [@unboxed] | B;; +[%%expect{| +t/99[4] IS NOT SEPARABLE +SHAPE(t/99[4]) {head_imm = Shape_set [0]; head_blocks = Shape_set [253]; head_separated = false} +type t = A of float [@unboxed] | B +|}];; + +type t = A of float [@unboxed] | B of string [@unboxed] | C | D of int;; +[%%expect{| +t/102[5] IS NOT SEPARABLE +SHAPE(t/102[5]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0; 252; 253]; head_separated = false} +type t = A of float [@unboxed] | B of string [@unboxed] | C | D of int +|}];; + +type t = K of int u u [@unboxed] +and 'a u = 'a id +and 'a id = Id of 'a [@unboxed];; +[%%expect{| +SHAPE(t/107[6]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} +SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = true} +type t = K of int u u [@unboxed] +and 'a u = 'a id +and 'a id = Id of 'a [@unboxed] +|}];; + +type t = { a : int } [@@unboxed] +and tt = A of t [@unboxed];; +[%%expect{| +SHAPE(tt/113[7]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} +type t = { a : int; } [@@unboxed] +and tt = A of t [@unboxed] +|}];; + +type t = A of { a : int } [@unboxed];; +[%%expect{| +SHAPE(t/116[8]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} +type t = A of { a : int; } [@unboxed] +|}];; + +type ('a, 'r) u = 'r +and 'a t = A of { body : 'r. ('a, 'r) u } [@unboxed];; +[%%expect{| +SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = true} +type ('a, 'r) u = 'r +and 'a t = A of { body : 'r. ('a, 'r) u; } [@unboxed] +|}];; diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml new file mode 100644 index 000000000000..9a598f606a39 --- /dev/null +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml @@ -0,0 +1,39 @@ +(* TEST + * setup-ocamlc.byte-build-env + ** ocamlc.byte + *** check-ocamlc.byte-output + **** run + ***** check-program-output +*) + +module A = struct + type t = A of int | B of string [@unboxed] + + let f = function A _ -> 0 | B _ -> 1 + + let test () = + assert (f (A 0) = 0); + assert (f (B "0") = 1) +end + +let () = A.test () + +module B = struct + type t = A of int | B of float + type tt = A' of t [@unboxed] | B' + + let f = function A' _ -> 0 | B' -> 1 + + let test () = + assert (f (A' (A 0)) = 0); + assert (f (A' (B 0.)) = 0); + assert (f B' = 1) +end + +let () = B.test () + +module C = struct + type t = I of int [@unboxed] | C1 of unit | C2 of unit + + let f = function I i -> i | C1 () -> 0 | C2 () -> 1 +end diff --git a/testsuite/tests/typing-unboxed/test.ml b/testsuite/tests/typing-unboxed/test.ml index 850713cf6ae5..c3b0c90b752b 100644 --- a/testsuite/tests/typing-unboxed/test.ml +++ b/testsuite/tests/typing-unboxed/test.ml @@ -744,7 +744,11 @@ Error: [@The native code version of the primitive is mandatory (* PR#7424 *) type 'a b = B of 'a b b [@@unboxed];; [%%expect{| -type 'a b = B of 'a b b [@@unboxed] +Line 1, characters 0-35: +1 | type 'a b = B of 'a b b [@@unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + b/182[29] appears unboxed at the head of its own definition. |}] diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index dd8bb73049b9..1965d2ceb30b 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -377,73 +377,23 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_constr (Oide_ident (Out_name.create "lazy"), [v]) end | Tconstr(path, ty_list, _) -> begin - try - let decl = Env.find_type path env in + match Env.find_type path env with + | exception Not_found -> + Oval_stuff "" + | decl -> begin match decl with | {type_kind = Type_abstract; type_manifest = None} -> Oval_stuff "" | {type_kind = Type_abstract; type_manifest = Some body} -> tree_of_val depth obj (instantiate_type env decl.type_params ty_list body) - | {type_kind = Type_variant (constr_list,rep)} -> - let unbx = (rep = Variant_unboxed) in - let tag = - if unbx then Cstr_unboxed - else if O.is_block obj - then Cstr_block(O.tag obj) - else Cstr_constant(O.obj obj) in - let {cd_id;cd_args;cd_res} = - Datarepr.find_constr_by_tag tag constr_list in - let type_params = - match cd_res with - Some t -> - begin match get_desc t with - Tconstr (_,params,_) -> - params - | _ -> assert false end - | None -> decl.type_params - in - begin - match cd_args with - | Cstr_tuple l -> - let ty_args = - instantiate_types env type_params ty_list l in - tree_of_constr_with_args (tree_of_constr env path) - (Ident.name cd_id) false 0 depth obj - ty_args unbx - | Cstr_record lbls -> - let r = - tree_of_record_fields depth - env path type_params ty_list - lbls 0 obj unbx - in - Oval_constr(tree_of_constr env path - (Out_name.create (Ident.name cd_id)), - [ r ]) - end + | {type_kind = Type_variant (constr_list, rep)} -> + tree_of_variant depth env decl path ty_list obj constr_list rep | {type_kind = Type_record(lbl_list, rep)} -> - begin match check_depth depth obj ty with - Some x -> x - | None -> - let pos = - match rep with - | Record_extension _ -> 1 - | _ -> 0 - in - let unbx = - match rep with Record_unboxed _ -> true | _ -> false - in - tree_of_record_fields depth - env path decl.type_params ty_list - lbl_list pos obj unbx - end + tree_of_record depth env decl path ty_list obj lbl_list rep | {type_kind = Type_open} -> tree_of_extension path ty_list depth obj - with - Not_found -> (* raised by Env.find_type *) - Oval_stuff "" - | Datarepr.Constr_not_found -> (* raised by find_constr_by_tag *) - Oval_stuff "" + end end | Tvariant row -> let row = Btype.row_repr row in @@ -481,6 +431,83 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_stuff "" end + and tree_of_variant depth env decl path ty_list obj constr_decl_list rep = + let constr_descr_list = + match Env.find_type_descrs path env with + | exception Not_found -> assert false + | Type_variant (constr_list, _) -> constr_list + | Type_abstract | Type_record _ | Type_open -> assert false + in + let unbx = (rep = Variant_unboxed) in + let obj_head = + (* We cannot use Typedecl_unbodex.Head.of_val directly + as we are functorized over the implementation of Obj. *) + let module Head = Typedecl_unboxed.Head in + if O.is_block obj + then Head.Block (O.tag obj) + else Head.Imm (O.obj obj : int) + in + let cstr_info = + List.combine constr_decl_list constr_descr_list + |> List.find_opt (fun (_decl, descr) -> + let cstr_shape = Typedecl_unboxed.Head_shape.of_cstr env descr.cstr_tag in + Typedecl_unboxed.Head.mem obj_head cstr_shape + ) + in + match cstr_info with + | None -> + Oval_stuff "" + | Some ({cd_id; cd_args; cd_res; _}, {cstr_tag; _}) -> + let type_params = + match cd_res with + | Some t -> + begin match get_desc t with + Tconstr (_,params,_) -> + params + | _ -> assert false end + | None -> decl.type_params + in + let unbx = + unbx || match cstr_tag with + | Cstr_unboxed _ -> true + | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> false + in + begin + match cd_args with + | Cstr_tuple l -> + let ty_args = + instantiate_types env type_params ty_list l in + tree_of_constr_with_args (tree_of_constr env path) + (Ident.name cd_id) false 0 depth obj + ty_args unbx + | Cstr_record lbls -> + let r = + tree_of_record_fields depth + env path type_params ty_list + lbls 0 obj unbx + in + Oval_constr(tree_of_constr env path + (Out_name.create (Ident.name cd_id)), + [ r ]) + end + + and tree_of_record depth env decl path ty_list obj lbl_list rep = + match check_depth depth obj ty with + | Some x -> x + | None -> + let pos = + match rep with + | Record_extension _ -> 1 + | _ -> 0 + in + let unbx = + match rep with Record_unboxed _ -> true | _ -> false + in + tree_of_record_fields depth + env path decl.type_params ty_list + lbl_list pos obj unbx + + and tree_of_record_fields depth env path type_params ty_list lbl_list pos obj unboxed = let rec tree_of_fields pos = function diff --git a/typing/btype.ml b/typing/btype.ml index 62e8195368be..a839f1ce23eb 100644 --- a/typing/btype.ml +++ b/typing/btype.ml @@ -40,6 +40,7 @@ module TypeMap = struct include TransientTypeMap let add ty = wrap_repr add ty let find ty = wrap_repr find ty + let mem ty = wrap_repr mem ty let singleton ty = wrap_repr singleton ty let fold f = TransientTypeMap.fold (wrap_type_expr f) end @@ -48,6 +49,7 @@ module TypeHash = struct include TransientTypeHash let add hash = wrap_repr (add hash) let find hash = wrap_repr (find hash) + let mem hash = wrap_repr (mem hash) let iter f = TransientTypeHash.iter (wrap_type_expr f) end module TransientTypePairs = diff --git a/typing/btype.mli b/typing/btype.mli index 08ee2f13209e..e3eafd8ac34d 100644 --- a/typing/btype.mli +++ b/typing/btype.mli @@ -34,6 +34,7 @@ module TypeMap : sig and type 'a t = 'a TransientTypeMap.t val add: type_expr -> 'a -> 'a t -> 'a t val find: type_expr -> 'a t -> 'a + val mem: type_expr -> 'a t -> bool val singleton: type_expr -> 'a -> 'a t val fold: (type_expr -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b end @@ -41,6 +42,7 @@ module TypeHash : sig include Hashtbl.S with type key = transient_expr val add: 'a t -> type_expr -> 'a -> unit val find: 'a t -> type_expr -> 'a + val mem: 'a t -> type_expr -> bool val iter: (type_expr -> 'a -> unit) -> 'a t -> unit end module TypePairs : sig diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 9d51817bc0f4..817fa997bc14 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -20,6 +20,12 @@ open Asttypes open Types open Btype +(* TODO: register an error printer for this type. *) +type error = + | Multiple_args_unboxed_constructor of Ident.t + +exception Error of Location.t * error + (* Simplified version of Ctype.free_vars *) let free_vars ?(param=false) ty = let ret = ref TypeSet.empty in @@ -94,11 +100,17 @@ let constructor_args ~current_unit priv cd_args cd_res path rep = let constructor_descrs ~current_unit ty_path decl cstrs rep = let ty_res = newgenconstr ty_path decl.type_params in - let num_consts = ref 0 and num_nonconsts = ref 0 in + let variant_unboxed = Builtin_attributes.has_unboxed decl.type_attributes in + let num_consts = ref 0 and num_nonconsts = ref 0 and num_unboxed = ref 0 in List.iter - (fun {cd_args; _} -> - if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts) - cstrs; + (fun {cd_args; cd_attributes; _} -> + if variant_unboxed || Builtin_attributes.has_unboxed cd_attributes + then incr num_unboxed + else if cd_args = Cstr_tuple [] then incr num_consts + else incr num_nonconsts; + ) cstrs; + (* Unboxed type data is shared among constructors of the same variant type *) + let unboxed_type_data = ref None in let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> @@ -107,17 +119,23 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = | Some ty_res' -> ty_res' | None -> ty_res in + (* A constructor is unboxed if the whole declaration has the + [@@unboxed] attr, or if it has the [@unboxed] attr *) + let cstr_is_unboxed = variant_unboxed || + Builtin_attributes.has_unboxed cd_attributes + in let (tag, descr_rem) = - match cd_args, rep with - | _, Variant_unboxed -> - assert (rem = []); - (Cstr_unboxed, []) - | Cstr_tuple [], Variant_regular -> - (Cstr_constant idx_const, - describe_constructors (idx_const+1) idx_nonconst rem) - | _, Variant_regular -> - (Cstr_block idx_nonconst, - describe_constructors idx_const (idx_nonconst+1) rem) in + match cstr_is_unboxed, cd_args with + | true, Cstr_tuple [ty] + | true, Cstr_record [{ld_type=ty; _}] -> + (Cstr_unboxed {unboxed_ty = ty; unboxed_shape = ref None}, + describe_constructors idx_const idx_nonconst rem) + | true, _ -> + raise (Error (cd_loc, Multiple_args_unboxed_constructor cd_id)) + | false, Cstr_tuple [] -> (Cstr_constant idx_const, + describe_constructors (idx_const+1) idx_nonconst rem) + | false, _ -> (Cstr_block idx_nonconst, + describe_constructors idx_const (idx_nonconst+1) rem) in let cstr_name = Ident.name cd_id in let existentials, cstr_args, cstr_inlined = let representation = @@ -137,6 +155,8 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = cstr_tag = tag; cstr_consts = !num_consts; cstr_nonconsts = !num_nonconsts; + cstr_unboxed = !num_unboxed; + cstr_unboxed_type_data = unboxed_type_data; cstr_private = decl.type_private; cstr_generalized = cd_res <> None; cstr_loc = cd_loc; @@ -165,6 +185,8 @@ let extension_descr ~current_unit path_ext ext = cstr_tag = Cstr_extension(path_ext, cstr_args = []); cstr_consts = -1; cstr_nonconsts = -1; + cstr_unboxed = -1; + cstr_unboxed_type_data = ref None; cstr_private = ext.ext_private; cstr_generalized = ext.ext_ret_type <> None; cstr_loc = ext.ext_loc; @@ -218,7 +240,8 @@ let rec find_constr tag num_const num_nonconst = function then c else find_constr tag (num_const + 1) num_nonconst rem | c :: rem -> - if tag = Cstr_block num_nonconst || tag = Cstr_unboxed + if tag = Cstr_block num_nonconst (* || tag = Cstr_unboxed [] *) + (* XXX changes needed in the check above *) then c else find_constr tag num_const (num_nonconst + 1) rem diff --git a/typing/oprint.ml b/typing/oprint.ml index 7a47cab446e3..eba942d11b56 100644 --- a/typing/oprint.ml +++ b/typing/oprint.ml @@ -495,6 +495,16 @@ let collect_functor_args mty = let l, rest = collect_functor_args [] mty in List.rev l, rest +let constructor_of_extension_constructor + (ext : out_extension_constructor) : out_constructor += + { + ocstr_name = ext.oext_name; + ocstr_args = ext.oext_args; + ocstr_return_type = ext.oext_ret_type; + ocstr_unboxed = false; + } + let split_anon_functor_arguments params = let rec uncollect_anonymous_suffix acc rest = match acc with | Some (None, mty_arg) :: acc -> @@ -560,13 +570,13 @@ and print_out_signature ppf = match items with Osig_typext(ext, Oext_next) :: items -> gather_extensions - ((ext.oext_name, ext.oext_args, ext.oext_ret_type) :: acc) + (constructor_of_extension_constructor ext :: acc) items | _ -> (List.rev acc, items) in let exts, items = gather_extensions - [(ext.oext_name, ext.oext_args, ext.oext_ret_type)] + [constructor_of_extension_constructor ext] items in let te = @@ -592,7 +602,7 @@ and print_out_sig_item ppf = name !out_class_type clt | Osig_typext (ext, Oext_exception) -> fprintf ppf "@[<2>exception %a@]" - print_out_constr (ext.oext_name, ext.oext_args, ext.oext_ret_type) + print_out_constr (constructor_of_extension_constructor ext) | Osig_typext (ext, _es) -> print_out_extension_constructor ppf ext | Osig_modtype (name, Omty_abstract) -> @@ -702,29 +712,43 @@ and print_out_type_decl kwd ppf td = print_immediate print_unboxed -and print_out_constr ppf (name, tyl,ret_type_opt) = +and print_out_constr ppf constr = + let { + ocstr_name = name; + ocstr_args = tyl; + ocstr_return_type = return_type; + ocstr_unboxed = unboxed; + } = constr in let name = match name with | "::" -> "(::)" (* #7200 *) | s -> s in - match ret_type_opt with + let pp_unboxed ppf = function + | false -> () + | true -> fprintf ppf "@ [@unboxed]" + in + match return_type with | None -> begin match tyl with | [] -> pp_print_string ppf name | _ -> - fprintf ppf "@[<2>%s of@ %a@]" name + fprintf ppf "@[<2>%s of@ %a%a@]" name (print_typlist print_simple_out_type " *") tyl + pp_unboxed unboxed end | Some ret_type -> begin match tyl with | [] -> - fprintf ppf "@[<2>%s :@ %a@]" name print_simple_out_type ret_type + fprintf ppf "@[<2>%s :@ %a%a@]" name + print_simple_out_type ret_type + pp_unboxed unboxed | _ -> - fprintf ppf "@[<2>%s :@ %a -> %a@]" name + fprintf ppf "@[<2>%s :@ %a -> %a%a@]" name (print_typlist print_simple_out_type " *") tyl print_simple_out_type ret_type + pp_unboxed unboxed end and print_out_extension_constructor ppf ext = @@ -745,7 +769,8 @@ and print_out_extension_constructor ppf ext = fprintf ppf "@[type %t +=%s@;<1 2>%a@]" print_extended_type (if ext.oext_private = Asttypes.Private then " private" else "") - print_out_constr (ext.oext_name, ext.oext_args, ext.oext_ret_type) + print_out_constr + (constructor_of_extension_constructor ext) and print_out_type_extension ppf te = let print_extended_type ppf = @@ -795,13 +820,13 @@ let rec print_items ppf = match items with (Osig_typext(ext, Oext_next), None) :: items -> gather_extensions - ((ext.oext_name, ext.oext_args, ext.oext_ret_type) :: acc) + (constructor_of_extension_constructor ext :: acc) items | _ -> (List.rev acc, items) in let exts, items = gather_extensions - [(ext.oext_name, ext.oext_args, ext.oext_ret_type)] + [constructor_of_extension_constructor ext] items in let te = diff --git a/typing/oprint.mli b/typing/oprint.mli index bafd17ccf126..baa733d82457 100644 --- a/typing/oprint.mli +++ b/typing/oprint.mli @@ -20,8 +20,7 @@ val out_ident : (formatter -> out_ident -> unit) ref val out_value : (formatter -> out_value -> unit) ref val out_label : (formatter -> string * bool * out_type -> unit) ref val out_type : (formatter -> out_type -> unit) ref -val out_constr : - (formatter -> string * out_type list * out_type option -> unit) ref +val out_constr : (formatter -> out_constructor -> unit) ref val out_class_type : (formatter -> out_class_type -> unit) ref val out_module_type : (formatter -> out_module_type -> unit) ref val out_sig_item : (formatter -> out_sig_item -> unit) ref diff --git a/typing/outcometree.mli b/typing/outcometree.mli index d9b4f04c1c71..bd6e7e0bcf7a 100644 --- a/typing/outcometree.mli +++ b/typing/outcometree.mli @@ -69,7 +69,7 @@ type out_type = | Otyp_object of (string * out_type) list * bool option | Otyp_record of (string * bool * out_type) list | Otyp_stuff of string - | Otyp_sum of (string * out_type list * out_type option) list + | Otyp_sum of out_constructor list | Otyp_tuple of out_type list | Otyp_var of bool * string | Otyp_variant of @@ -78,6 +78,13 @@ type out_type = | Otyp_module of out_ident * (string * out_type) list | Otyp_attribute of out_type * out_attribute +and out_constructor = { + ocstr_name: string; + ocstr_args: out_type list; + ocstr_return_type: out_type option; + ocstr_unboxed: bool; +} + and out_variant = | Ovar_fields of (string * bool * out_type list) list | Ovar_typ of out_type @@ -128,7 +135,7 @@ and out_extension_constructor = and out_type_extension = { otyext_name: string; otyext_params: string list; - otyext_constructors: (string * out_type list * out_type option) list; + otyext_constructors: out_constructor list; otyext_private: Asttypes.private_flag } and out_val_decl = { oval_name: string; diff --git a/typing/parmatch.ml b/typing/parmatch.ml index 10fc10a00921..bb522f3291e8 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -749,7 +749,8 @@ let full_match closing env = match env with match discr.pat_desc with | Any -> assert false | Construct { cstr_tag = Cstr_extension _ ; _ } -> false - | Construct c -> List.length env = c.cstr_consts + c.cstr_nonconsts + | Construct c -> + List.length env = c.cstr_consts + c.cstr_nonconsts + c.cstr_unboxed | Variant { type_row; _ } -> let fields = List.map @@ -793,7 +794,7 @@ let should_extend ext env = match ext with | (p,_)::_ -> let open Patterns.Head in begin match p.pat_desc with - | Construct {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed)} -> + | Construct {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed _)} -> let path = get_constructor_type_path p.pat_type p.pat_env in Path.same path ext | Construct {cstr_tag=(Cstr_extension _)} -> false @@ -882,7 +883,7 @@ let build_other_constrs env p = match p.pat_desc with | Construct ({ cstr_tag = Cstr_extension _ }) -> extra_pat | Construct - ({ cstr_tag = Cstr_constant _ | Cstr_block _ | Cstr_unboxed } as c) -> + ({ cstr_tag = Cstr_constant _ | Cstr_block _ | Cstr_unboxed _ } as c) -> let constr = { p with pat_desc = c } in let get_constr q = match q.pat_desc with @@ -2004,7 +2005,7 @@ let extendable_path path = Path.same path Predef.path_option) let rec collect_paths_from_pat r p = match p.pat_desc with -| Tpat_construct(_, {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed)}, +| Tpat_construct(_, {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed _)}, ps, _) -> let path = get_constructor_type_path p.pat_type p.pat_env in List.fold_left diff --git a/typing/printtyp.ml b/typing/printtyp.ml index c35b7e8a1e21..16c43c5056c7 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1420,13 +1420,24 @@ and tree_of_constructor_arguments = function and tree_of_constructor cd = let name = Ident.name cd.cd_id in let arg () = tree_of_constructor_arguments cd.cd_args in + let unboxed = Builtin_attributes.has_unboxed cd.cd_attributes in match cd.cd_res with - | None -> (name, arg (), None) + | None -> { + ocstr_name = name; + ocstr_args = arg (); + ocstr_return_type = None; + ocstr_unboxed = unboxed; + } | Some res -> Names.with_local_names (fun () -> let ret = tree_of_typexp Type res in let args = arg () in - (name, args, Some ret)) + { + ocstr_name = name; + ocstr_args = args; + ocstr_return_type = Some ret; + ocstr_unboxed = unboxed; + }) and tree_of_label l = (Ident.name l.ld_id, l.ld_mutable = Mutable, tree_of_typexp Type l.ld_type) @@ -1511,7 +1522,12 @@ let extension_only_constructor id ppf ext = ext.ext_ret_type in Format.fprintf ppf "@[%a@]" - !Oprint.out_constr (name, args, ret) + !Oprint.out_constr { + ocstr_name = name; + ocstr_args = args; + ocstr_return_type = ret; + ocstr_unboxed = false; + } (* Print a value declaration *) diff --git a/typing/rec_check.ml b/typing/rec_check.ml index 75091497a378..2d0be0a1ebda 100644 --- a/typing/rec_check.ml +++ b/typing/rec_check.ml @@ -157,7 +157,7 @@ let classify_expression : Typedtree.expression -> sd = | Texp_letexception (_, e) -> classify_expression env e - | Texp_construct (_, {cstr_tag = Cstr_unboxed}, [e]) -> + | Texp_construct (_, {cstr_tag = Cstr_unboxed _}, [e]) -> classify_expression env e | Texp_construct _ -> Static @@ -606,7 +606,7 @@ let rec expression : Typedtree.expression -> term_judg = | _ -> empty in let m' = match desc.cstr_tag with - | Cstr_unboxed -> + | Cstr_unboxed _ -> Return | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> Guard diff --git a/typing/typecore.ml b/typing/typecore.ml index 7595d7dc6e93..b2b485546acd 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -4753,7 +4753,7 @@ and type_construct env loc lid sarg ty_expected_explained attrs = begin match constr.cstr_tag with | Cstr_extension _ -> raise(Error(loc, env, Private_constructor (constr, ty_res))) - | Cstr_constant _ | Cstr_block _ | Cstr_unboxed -> + | Cstr_constant _ | Cstr_block _ | Cstr_unboxed _ -> raise (Error(loc, env, Private_type ty_res)); end; (* NOTE: shouldn't we call "re" on this final expression? -- AF *) diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 7ca17507b9c7..8afcab2c0722 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -979,6 +979,11 @@ let transl_type_decl env rec_flag sdecl_list = let final_env = add_types_to_env decls env in (* Check re-exportation *) List.iter2 (check_abbrev final_env) sdecl_list decls; + (* Check head shape conflicts *) + List.iter (fun (id, decl) -> + let path = Path.Pident id in + Typedecl_unboxed.Head_shape.check_typedecl final_env (path, decl) + ) decls; (* Keep original declaration *) let final_decls = List.map2 @@ -1919,3 +1924,28 @@ let () = | _ -> None ) + +let get_unboxed_type_data env cstr_desc = + match !(cstr_desc.cstr_unboxed_type_data) with + | Some data-> data + | None -> + let open Typedecl_unboxed in + let unboxed_type_data = + let path = Btype.cstr_type_path cstr_desc in + let shape = Head_shape.of_type env path in + Head_shape.unboxed_type_data_of_shape shape + in + cstr_desc.cstr_unboxed_type_data := Some unboxed_type_data; + unboxed_type_data + +let cstr_max_block_tag env cstr_desc = + (get_unboxed_type_data env cstr_desc).utd_max_block_tag + +let cstr_max_imm_value env cstr_desc = + (get_unboxed_type_data env cstr_desc).utd_max_imm_value + +let cstr_unboxed_numconsts env cstr_desc = + (get_unboxed_type_data env cstr_desc).utd_unboxed_numconsts + +let cstr_unboxed_numnonconsts env cstr_desc = + (get_unboxed_type_data env cstr_desc).utd_unboxed_numnonconsts diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 067319f041a8..063f75a8c6a3 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -108,3 +108,12 @@ type error = exception Error of Location.t * error val report_error: formatter -> error -> unit + +(* See [unboxed_type_data] in types.mli *) +val cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option + +val cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option + +val cstr_unboxed_numconsts : Env.t -> constructor_description -> int option + +val cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 85a4273382ee..059a206f5b9a 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -51,3 +51,479 @@ let get_unboxed_type_representation env ty = (* Do not give too much fuel: PR#7424 *) get_unboxed_type_representation env ty 100 ;; + +type primitive_type = + | Int + | Float + | String + | Bytes + | Array + | Floatarray + | Lazy + | Custom + +let match_primitive_type p = + let open Predef in + let tbl = [ + (path_int, Int); + (path_float, Float); + (path_string, String); + (path_bytes, Bytes); + (path_array, Array); + (path_floatarray, Floatarray); + (path_lazy_t, Lazy); + (path_nativeint, Custom); + (path_int32, Custom); + (path_int64, Custom); + ] in + List.find_opt (fun (p', _) -> Path.same p p') tbl |> Option.map snd + +module Head = struct + type t = + | Imm of imm + | Block of tag + + let of_val (obj : Obj.t) = + if Obj.is_block obj + then Block (Obj.tag obj) + else Imm (Obj.obj obj : int) + + let mem head shape = + let mem h = function + | Shape_any -> true + | Shape_set hs -> List.mem h hs + in + match head with + | Imm n -> mem n shape.head_imm + | Block t -> mem t shape.head_blocks +end + +module Head_shape = struct + + exception Conflict + (* TODO: add more information to be able to display proper + error messages. *) + + type t = head_shape + + let pp_shape ppf = function + | Shape_any -> Format.fprintf ppf "Shape_any" + | Shape_set l -> + Format.fprintf ppf "Shape_set [%a]" + (Format.pp_print_list + ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") + Format.pp_print_int) l + + let pp ppf {head_imm; head_blocks; head_separated} = + Format.fprintf ppf "{head_imm = %a; head_blocks = %a; head_separated = %b}" + pp_shape head_imm + pp_shape head_blocks + head_separated + + let has_float ~blocks = + match blocks with + | Shape_any -> true + | Shape_set tags -> List.mem Obj.double_tag tags + + let has_nonfloat ~imm ~blocks = + match imm with + | Shape_set (_ :: _) + | Shape_any -> true + | Shape_set [] -> + match blocks with + | Shape_any -> true + | Shape_set tags -> + List.exists (fun t -> t <> Obj.double_tag) tags + + let separated ~imm ~blocks = + not (has_float ~blocks && has_nonfloat ~imm ~blocks) + + let head_has_float hd = + has_float ~blocks:hd.head_blocks + + let head_has_nonfloat hd = + has_nonfloat ~imm:hd.head_imm ~blocks:hd.head_blocks + + let any_shape = { + head_imm = Shape_any; + head_blocks = Shape_any; + head_separated = true; + } + + let _poison_shape = { + head_imm = Shape_any; + head_blocks = Shape_any; + head_separated = false; + } + + let empty_shape = + { + head_imm = Shape_set []; + head_blocks = Shape_set []; + head_separated = true; + } + + let imm_shape vals = + { + head_imm = Shape_set vals; + head_blocks = Shape_set []; + head_separated = true; + } + + let block_shape tags = + let imm = Shape_set [] in + let blocks = Shape_set tags in + { + head_imm = imm; + head_blocks = blocks; + head_separated = separated ~imm ~blocks; + } + + let cstrs_shape ~num_consts ~num_nonconsts = + let int_list n = List.init n Fun.id in + { + head_imm = Shape_set (int_list num_consts); + head_blocks = Shape_set (int_list num_nonconsts); + head_separated = + (assert (num_nonconsts < Obj.double_tag); + true); + } + + let disjoint_union hd1 hd2 = + let union s1 s2 = match s1, s2 with + | Shape_any, Shape_set [] | Shape_set [], Shape_any -> Shape_any + | Shape_any, _ | _, Shape_any -> raise Conflict + | Shape_set l1, Shape_set l2 -> + (* invariant : l1 and l2 are sorted *) + let rec merge l1 l2 = match l1, l2 with + | [], l | l, [] -> l + | x :: xx, y :: yy -> + if x = y then raise Conflict + else if x < y then x :: (merge xx l2) + else y :: (merge l1 yy) + in Shape_set (merge l1 l2) + in + let head_imm = union hd1.head_imm hd2.head_imm in + let head_blocks = union hd1.head_blocks hd2.head_blocks in + let head_separated = + hd1.head_separated && + hd2.head_separated && + not (head_has_float hd1 && head_has_nonfloat hd2) && + not (head_has_float hd2 && head_has_nonfloat hd1) + in + { head_imm; head_blocks; head_separated } + + module Callstack = struct + type t = Path.t list + + module TypeMap = Btype.TypeMap + type map = t TypeMap.t + + let visit p callstack : t = + p :: callstack + + let visited p callstack = + List.exists (Path.same p) callstack + + let head (callstack_map : map) ty = + TypeMap.find ty callstack_map + + let rec extend callstack_map ty new_callstack = + if TypeMap.mem ty callstack_map then callstack_map + else + let callstack_map = TypeMap.add ty new_callstack callstack_map in + Btype.fold_type_expr (fun callstack_map ty' -> + extend callstack_map ty' new_callstack + ) callstack_map ty + + let fill ty callstack = extend TypeMap.empty ty callstack + end + + (* Useful to interactively debug 'of_type_expr' below. *) + let _print_annotations ty callstack_map = + Format.eprintf "@[CALLSTACK(%a): @[" + Printtyp.type_expr ty; + let pp_sep ppf () = Format.fprintf ppf ",@ " in + Callstack.TypeMap.to_rev_seq callstack_map |> Seq.iter + (fun (ty, callstack) -> + Format.eprintf "@ @[%a@ [%a]@]" + Printtyp.type_expr (Types.Transient_expr.type_expr ty) + (Format.pp_print_list ~pp_sep Printtyp.path) callstack + ); + Format.eprintf "@]@]@."; + () + + let check_annotated ty callstack = + let hash = Btype.TypeHash.create 42 in + let rec loop ty = + if Btype.TypeHash.mem hash ty then () + else begin + Btype.TypeHash.add hash ty (); + assert (Btype.TypeMap.mem ty callstack); + Btype.iter_type_expr loop ty; + end + in loop ty + + let ty_of_poly ty = match get_desc ty with + | Tpoly (t, _) -> t + | _ -> ty + + let of_primitive_type = function + | Int -> + { + head_imm = Shape_any; + head_blocks = Shape_set []; + head_separated = true; + } + | Float -> block_shape [Obj.double_tag] + | String + | Bytes -> block_shape [Obj.string_tag] + | Array -> + block_shape + (if Config.flat_float_array then [0] + else [0; Obj.double_array_tag]) + | Floatarray -> block_shape [Obj.double_array_tag] + | Lazy -> any_shape + (* Lazy values can 'shortcut' the lazy block, and thus have many + different tags. When Config.flat_float_array, they + cannot be floats, so we might want to refine that if there + are strong use-cases. *) + | Custom -> block_shape [Obj.custom_tag] + + let rec of_type_expr env ty callstack_map = + (* TODO : try the Ctype.expand_head_opt version here *) + check_annotated ty callstack_map; + match get_desc ty with + | Tvar _ | Tunivar _ -> + (* FIXME: variables that are universally quantified (including type parameters) + should get [any_shape] as here, but GADT variables that are existentially quantified + should get [poison_shape] instead -- they are not separated. *) + any_shape + | Tconstr (p, args, _abbrev) -> + begin match match_primitive_type p with + | Some prim_type -> of_primitive_type prim_type + | None -> + let head_callstack = Callstack.head callstack_map ty in + if Callstack.visited p head_callstack then + let loc = + match Env.find_type p env with + | decl -> Some decl.type_loc + | exception Not_found -> None in + Location.raise_errorf ?loc + "Cyclic type expansion during [@unboxed] verification.@ \ + %a appears unboxed at the head of its own definition." + Path.print p + else match Env.find_type_descrs p env, Env.find_type p env with + | exception Not_found -> + (* FIXME: if one of the parameters is non-separated, then + this unknown type should be considered non-separated as well. + (It may be a projection into this parameter.) + This corresponds to the DeepSep case of the separability analysis. *) + any_shape + | descr, decl -> + of_typedescr env descr decl ~args callstack_map + (Callstack.visit p head_callstack) + end + | Ttuple _ -> block_shape [0] + | Tarrow _ -> block_shape [Obj.closure_tag; Obj.infix_tag] + | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) + any_shape + | Tlink _ | Tsubst _ | Tpoly _ | Tfield _ -> + assert false + + + and of_typedescr env ty_descr ty_decl ~args + callstack_map new_callstack = + let of_type_expr_with_params ty = + (* We instantiate the formal type variables with the + type expression parameters at use site. + + We build a callstack for this new type by mapping all new + nodes, corresponding to the spine of 'ty', to the current + call stack. *) + let ty = ty_of_poly ty in + let params = ty_decl.type_params in + let ty = Ctype.apply env params ty args in + let callstack_map = + Callstack.extend callstack_map ty new_callstack in + of_type_expr env ty callstack_map + in + match ty_descr with + | Type_abstract -> + begin match ty_decl.type_manifest with + | None -> any_shape + | Some ty -> of_type_expr_with_params ty + end + | Type_record (_, Record_regular) -> block_shape [0] + | Type_record (_, Record_float) -> block_shape [Obj.double_array_tag] + | Type_record (fields, Record_unboxed _) -> + begin match fields with + | [{lbl_arg = ty; _}] -> of_type_expr_with_params ty + | _ -> assert false + end + | Type_record (_, Record_inlined _) + | Type_record (_, Record_extension _) -> failwith "TODO" + | Type_open -> block_shape [0] + | Type_variant ([],_) -> empty_shape + | Type_variant ((fst_descr :: _) as cstr_descrs,_) -> + (* we compute the shape of all boxed constructors, then the shapes of + each unboxed constructors *) + let num_consts = fst_descr.cstr_consts in + let num_nonconsts = fst_descr.cstr_nonconsts in + (* the head shape of boxed constructors is equivalent to the nb of + constant constructors and the nb of non constant constructors *) + let boxed_shape = cstrs_shape ~num_consts ~num_nonconsts in + let unboxed_shapes = List.filter_map + (fun descr -> + match descr.cstr_tag with + | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> None + | Cstr_unboxed {unboxed_ty; _}-> + Some (of_type_expr_with_params unboxed_ty) + ) cstr_descrs + in + (* now checking that the unboxed constructors are compatible with the + shape of boxed constructors *) + List.fold_left disjoint_union boxed_shape unboxed_shapes + + (* Remark on the life cycle of [unboxed_shape] information. + + The [cstr_tag] data that contains [unboxed_shape] is created + un-initialized by Datarepr, when entering a type declaration + inside the current typing environment. We cannot compute the + head-shape at this point: Env depends on Datarepr, so Datarepr + functions cannot depend on Env.t. + + Type declarations coming from the user code are "checked" after + being entered in the environment by the Typedecl module; at this + point the [check_typedecl] function below is called, and the + [unboxed_shape] information for their unboxed constructors is + computed and cached at this point. Conflicts are turned into + proper user-facing errors. + + However, the environment can also be extended by type + declarations coming from other compilation units (signatures in + .cmi files), and the head-shape information is not present or + computed at this point -- we are still within Env, and cannot + call [of_type] below without creating cyclic dependencies. Note + that these type-declarations have already been checked when + compiling their own module, so they must not contain head-shape + conflicts. In this case a type declaration can leave the + type-checking phase with its [head_shape] field still + un-initialized. + + When compiling variant constructors in pattern-matching, we need + the head-shape information again. It is obtained by calling the + [get] function below, which will re-compute and cache this + information if the [unboxed_shape] field is still + un-initialized. The typing environment used for computation at + this point is the [pat_env] environment of the pattern-matching, + which we assume is an extension of the environment used at + variant constructor declaration time. + + Error handling: [check_typedecl] handles Conflict exceptions by + showing a proper error to the user -- the error is in the user + code. On the other hand, [get] and [of_type] must never see + a shape conflict, as we assume the only un-initialized + [unboxed_shape] fields come from already-checked imported + declarations. If a conflict arises in those functions, it is + a programming error in the compiler codebase: a type declaration + has somehow been entered in the environment without being + validated by [check_typedecl] first. + *) + let fill_and_get env {unboxed_ty; unboxed_shape} = + match !unboxed_shape with + | Some shape -> shape + | None -> + let ty = ty_of_poly unboxed_ty in + let callstacks = Callstack.fill ty [] in + let shape = of_type_expr env ty callstacks in + unboxed_shape := Some shape; + shape + + let fill_cache env unboxed_cache = + ignore (fill_and_get env unboxed_cache) + + let of_cstr env = function + | Cstr_constant n -> imm_shape [n] + | Cstr_block t -> block_shape [t] + | Cstr_unboxed data -> fill_and_get env data + | Cstr_extension (_t, constant) -> + if constant + then block_shape [Obj.object_tag] + else block_shape [0] + + let unboxed_type_data_of_shape shape = + let bound_of_shape = function + | Shape_set l -> Some (List.fold_left max 0 l) + | Shape_any -> None + in + let num_of_shape = function + | Shape_set l -> Some (List.length l) + | Shape_any -> None + in + { + utd_max_imm_value = bound_of_shape shape.head_imm; + utd_max_block_tag = bound_of_shape shape.head_blocks; + utd_unboxed_numconsts = num_of_shape shape.head_imm; + utd_unboxed_numnonconsts = num_of_shape shape.head_blocks; + } + + let check_typedecl env (path,decl) = + match Env.find_type_descrs path env with + | exception Not_found -> failwith "XXX" + | Type_variant (cstrs, _repr) -> begin + try begin + cstrs |> List.iter (fun {cstr_tag; _} -> match cstr_tag with + | Cstr_unboxed cache -> fill_cache env cache + | _ -> () + ); + (* now check the whole shape for conflict between variants *) + let params = decl.type_params in + let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in + let callstack_map = Callstack.fill ty [] in + let shape = of_type_expr env ty callstack_map in + if Config.flat_float_array && not shape.head_separated then + Format.fprintf Format.err_formatter "%a IS NOT SEPARABLE@." + Path.print path; + (* Fill the variant data *) + match cstrs with + | [] -> () + | cstr :: _ -> + cstr.cstr_unboxed_type_data := + Some (unboxed_type_data_of_shape shape); + if !Clflags.dump_headshape then + (* TODO improve the printing to something nicer. *) + Format.fprintf Format.err_formatter "SHAPE(%a) %a@." + Path.print path + pp shape + end + with Conflict -> + if !Clflags.dump_headshape then + Format.fprintf Format.err_formatter "SHAPE(%a) CONFLICT@." + Path.print path; + (* TODO raise a fatal error with a registered printer, + instead of what is below. *) + Location.raise_errorf ~loc:decl.type_loc + "%a" + Format.pp_print_text + "This declaration is invalid, some [@unboxed] annotations \ + introduce overlapping representations." + end + | _ -> () + + let get env unboxed_data = + match fill_and_get env unboxed_data with + | exception Conflict -> + Misc.fatal_error + "Head_shape.get: check_typedecl should have run first." + | shape -> shape + + let of_type env path = + let decl = Env.find_type path env in + let ty = Btype.newgenty (Tconstr (path, decl.type_params, ref Mnil)) in + let callstacks = Callstack.fill ty [] in + try of_type_expr env ty callstacks + with Conflict -> + Misc.fatal_error + "Head_shape.of_type: check_typedecl should have run first." +end diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 9afd38e87975..f86db2669903 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -23,3 +23,46 @@ type t = (* for typeopt.ml *) val get_unboxed_type_representation: Env.t -> type_expr -> t + +module Head : sig + type t = + | Imm of imm + | Block of tag + + val of_val : Obj.t -> t + + val mem : t -> Types.head_shape -> bool + (** [mem head head_shape] checks whether the [head] is included + in the set of heads represented by the [head_shape] approximation. *) +end + +module Head_shape : sig + type t = Types.head_shape + + val pp : Format.formatter -> t -> unit + + (** Check a new type decalaration, that may be a variant type + containing unboxed constructors, to verify that the unboxing + requests respect the "disjointness" requirement of constructor + unboxing -- the values of two constructors must not conflict. + + This function fails with a fatal error if the declaration is + unsafe. *) + val check_typedecl : Env.t -> Path.t * Types.type_declaration -> unit + + (** Returns the head shape information of an unboxed constructor, + computing it on the fly if necessary. The typing environment must + be an extension of the environment in which the unboxed + constructor was declared. *) + val get : Env.t -> Types.unboxed_data -> head_shape + + (** Returns the head shape information of variant type path, + similarly to [get] above. *) + val of_type : Env.t -> Path.t -> t + + (** Returns the head shape information corresponding to the tag + of a datatype constructor. *) + val of_cstr : Env.t -> constructor_tag -> t + + val unboxed_type_data_of_shape : t -> Types.unboxed_type_data +end diff --git a/typing/types.ml b/typing/types.ml index 8be5bebf24cc..bc40bdb9b4df 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -406,6 +406,10 @@ type constructor_description = cstr_tag: constructor_tag; (* Tag for heap blocks *) cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_unboxed_type_data: unboxed_type_data option ref; + (* Type-global data that depends + on unboxing / head-shape information. *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -417,18 +421,46 @@ type constructor_description = and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) - | Cstr_unboxed (* Constructor of an unboxed type *) + | Cstr_unboxed of unboxed_data (* Constructor of an unboxed type *) | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) +and unboxed_data = + { unboxed_ty: type_expr; + unboxed_shape: head_shape option ref; + } + +and head_shape = + { head_imm: imm shape; (* set of immediates the head can be *) + head_blocks: tag shape; (* set of tags the head can have *) + head_separated: bool; (* is the set of values separated? *) + } + +and 'a shape = + (* TODO add some comment *) + | Shape_set of 'a list + | Shape_any + +and imm = int +and tag = int + +and unboxed_type_data = + { utd_max_imm_value: int option; + utd_max_block_tag: int option; + utd_unboxed_numconsts: int option; + utd_unboxed_numnonconsts: int option; + } let equal_tag t1 t2 = match (t1, t2) with | Cstr_constant i1, Cstr_constant i2 -> i2 = i1 | Cstr_block i1, Cstr_block i2 -> i2 = i1 - | Cstr_unboxed, Cstr_unboxed -> true + | Cstr_unboxed c1, Cstr_unboxed c2 -> + (* Possible tags of different unboxed constructors are disjoint, + so in particular their types must be different. *) + c1.unboxed_shape == c2.unboxed_shape | Cstr_extension (path1, b1), Cstr_extension (path2, b2) -> Path.same path1 path2 && b1 = b2 - | (Cstr_constant _|Cstr_block _|Cstr_unboxed|Cstr_extension _), _ -> false + | (Cstr_constant _|Cstr_block _|Cstr_unboxed _|Cstr_extension _), _ -> false let may_equal_constr c1 c2 = c1.cstr_arity = c2.cstr_arity diff --git a/typing/types.mli b/typing/types.mli index 6bfdae6b6bdc..15bd0d98b584 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -582,22 +582,116 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) + + (* The following group of fields store information not on this constructor, + but on all constructors of the variant, for pattern-matching compilation + purposes. *) cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_unboxed_type_data: unboxed_type_data option ref; + (* This mutable reference is shared among all + constructor_description for the same type, and depends on its + head shape. It is computed "later" (when a type environment + is available) by Typedecl.get_unboxed_type_data. *) + cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; cstr_attributes: Parsetree.attributes; cstr_inlined: type_declaration option; cstr_uid: Uid.t; - } + } and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) - | Cstr_unboxed (* Constructor of an unboxed type *) + | Cstr_unboxed of unboxed_data (* Unboxed constructor *) | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) +and unboxed_data = + { unboxed_ty: type_expr; (* type of the constructor parameter *) + unboxed_shape: + head_shape option ref; + (* The head-shape information is not available at type-declaration + construction time. It is computed later, from the type + environment, see Typedecl_unboxed.Head_Shape.get; either at + tpe-declaration checking time or (for types imported from + a .cmi) at first query of the information by the + pattern-matching compiler. *) + } + +(* Over-approximation of the possible values of a type, + used to verify and compile unboxed head constructors. + + We represent the "head" of the values: their value if + it is an immediate, or their tag if is a block. + A head "shape" is a set of possible heads. +*) +and head_shape = + { head_imm : imm shape; (* set of immediates the head can be *) + head_blocks : tag shape; (* set of tags the head can have *) + head_separated : bool; (* is the set of value separated? *) + } + +(* A description of a set of ['a] elements. *) +and 'a shape = + | Shape_set of 'a list (* An element among a finite list. *) + | Shape_any (* Any element (Top/Unknown). *) + +and imm = int +and tag = int + +(* Type-global data that depends on unboxing / head-shape information. + + Note: the fields below should not be accessed directly, but through + the helper functions in Typedecl + + cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option + cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option + cstr_unboxed_numconsts : Env.t -> constructor_description -> int option + cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option + + which take care of caching the [unboxed_type_data] field. +*) +and unboxed_type_data = + { utd_max_imm_value: int option; + (* The maximal immediate value at this type after unboxing; + None is used in the Shape_any case -- any immediate can occur.*) + + utd_max_block_tag: int option; + (* The maximal block tag at this type after unboxing; + None is used in the Shape_any case -- any tag can occur.*) + + utd_unboxed_numconsts: int option; + (* The number of constant constructors after unboxing. *) + + utd_unboxed_numnonconsts: int option; + (* The number of non-constant constructors after unboxing. *) + } +(* + Consider for example + + type t = + | Int of int [@unboxed] + | List of t list + | Str of string [@unboxed + + After unboxing, the representations of values at this type may be: + - any immediate value (coming from Int) + - a block of tag 0 (for List) + - a string value of tag String_tag (252) + + We have: { + utd_max_imm_value = None; + utd_max_block_tag = Some 252; + utd_unboxed_numconsts = None; + utd_unboxed_numnonconsts = Some 2; + } + + This information is needed by lambda/matching.ml to compile switches + on these constructors. +*) (* Constructors are the same *) val equal_tag : constructor_tag -> constructor_tag -> bool diff --git a/utils/clflags.ml b/utils/clflags.ml index b9f60cb0861c..634531804ae4 100644 --- a/utils/clflags.ml +++ b/utils/clflags.ml @@ -128,6 +128,7 @@ let dump_reload = ref false (* -dreload *) let dump_scheduling = ref false (* -dscheduling *) let dump_linear = ref false (* -dlinear *) let dump_interval = ref false (* -dinterval *) +let dump_headshape = ref false (* -dheadshape *) let keep_startup_file = ref false (* -dstartup *) let dump_combine = ref false (* -dcombine *) let profile_columns : Profile.column list ref = ref [] (* -dprofile/-dtimings *) diff --git a/utils/clflags.mli b/utils/clflags.mli index 06b478d3b63c..8d26c1bf9690 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -153,6 +153,7 @@ val dump_reload : bool ref val dump_scheduling : bool ref val dump_linear : bool ref val dump_interval : bool ref +val dump_headshape : bool ref val keep_startup_file : bool ref val dump_combine : bool ref val native_code : bool ref