|Anonymous | Login | Signup for a new account||2017-05-25 20:05 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006216||OCaml||back end (clambda to assembly)||public||2013-10-29 21:14||2015-12-11 19:25|
|Target Version||Fixed in Version||4.01.1+dev|
|Summary||0006216: inlining of GADT matches generates invalid assembly|
|Description||Inlining of GADT matches can generate invalid assembly in cases of the match that are dead.|
For example, in the code attached to this issue, the [String] case is dead after inlining. I think the compiler needs to eliminate these cases, since (e.g.) the register assignments---influenced by the specialized type parameters---may be invalid in the dead cases.
|Steps To Reproduce||bug.ml|
type _ t =
| Float : float t
| String : string t
let f : type a . a t -> a -> unit = fun t a ->
match t with
| Float -> ()
| String -> ignore (String.length a : int)
let _g (kind : float t) (x : float) : unit = f kind (x *. 13.)
$ ocamlopt -inline 20 -o bug bug.ml
/tmp/camlasmd28c07.s: Assembler messages:
/tmp/camlasmd28c07.s:67: Error: suffix or operands invalid for `movapd'
/tmp/camlasmd28c07.s:70: Error: suffix or operands invalid for `sub'
Without "-inline 20", compilation appears to be successful.
|Tags||No tags attached.|
|Attached Files|| patch_6216.diff [^] (2,608 bytes) 2013-10-30 10:25 [Show Content]
cmmgen-patch.diff [^] (2,501 bytes) 2013-10-30 11:46 [Show Content]
This looks like a hard one.
Since we're not going to do type inference in the backend, the only solution I see is to disable inlining for GADT pattern-matching, at least as long as we cannot reduce to a specific branch.
Added a test in basic-more/pr6216.ml, but no idea yet how to fix that.
I can write the code which detects dangerous matches, but I'm not sure how to propagate that to the backend.
Other potential optimizations might be affected as well (see 0005204 for a proposal which would require extra care since the introduction of GADT).
Am I right that the problem is caused by the current float unboxing strategy in cmmgen.ml, which assumes that an identifier bound to a float (case for Ulet / Boxed_float) is really a float everywhere in the function?
I can see two approaches for fixing this issue, both are which seem preferable to simply disabling inlining in presence of GADT matching:
- Propagate a limited form of type information. For instance, one could decide on the Typedtree which identifiers are of type "float" and mark them as such for later phases, instead of trying to infer this information again in the backend.
- Add a marker in the lambda+ulambda code to represent the boundary of a scope which brings in more type equalites from opening a GADT. This can be used to disable the float unboxing in cmmgen as soon as the identifier is used in such a GADT branch.
|I attach a quick (and dirty) POC for my first proposal, where the fact that an identifier is bound to a float is decided during the generation of lambda code. This is implemented with an extra flag on the identifier, which is set imperatively in the compilation of pattern matching.|
This example is a lot of fun.
> Am I right that the problem is caused by the current float unboxing strategy in cmmgen.ml, which assumes that an identifier bound to a float (case for Ulet / Boxed_float) is really a float everywhere in the function?
Roughly speaking, yes. The problem comes from Cmmgen.subst_boxed_number, which assumes the following: if a Cmm var v is let-bound to a boxed number, in the body of the "let" any memory load from v is an unboxing of this number and cancels out with the boxing.
In the example, v is bound to "box (... *. 13.)" and "String.length a" causes a load from v which is not a float unboxing load, but instead an integer load from the header block.
The best fix, in my opinion, is to be more prudent in subst_boxed_number, only optimizing loads that are proper inverses of the boxing operation we are considering. E.g. for a float boxing, these would be loads of Double or Double_u quantities with offset 0. Give me a few days to experiment with this approach.
I'd rather not propagate more types down the back-end, because I think it's much easier to make the back-end robust against (seemingly) ill-typed intermediate code.
PS: the same problem occurs with Obj.magic, e.g.
let f (x: float) =
let y = x *. 2.0 in String.length (Obj.magic y)
edited on: 2013-10-30 11:32
Xavier: indeed, making subst_boxed_number more restrictive in its interpretation of unboxing patterns is likely to fix this issue. But being able to tell if an identifier is necessarily bound to a float can enable different and useful unboxing strategies (also for function parameters, for identifiers bound to the result of a function call, etc) (0005204 is one such strategy, other are possible). Don't you agree?
> I'd rather not propagate more types down the back-end
Does my patch look correct to you (in particular the fact that identifiers are mutated imperatively during the compilation)?
I attach "cmmgen-patch.diff" that implements my solution.
I'm in the process of testing it for correctness and performance regressions.
Concerning frisch's patch: note that the problem is not specific to floats but also occurs with other numerical boxed types (int32, int64, nativeint). I haven't reviewed this patch in more details.
|Fixed (as per cmmgen-patch.diff) in 4.01 branch (commit 14251) and in trunk (commit 14252).|
|2013-10-29 21:14||shinwell||New Issue|
|2013-10-29 21:14||shinwell||Status||new => assigned|
|2013-10-29 21:14||shinwell||Assigned To||=> garrigue|
|2013-10-30 01:08||garrigue||Note Added: 0010541|
|2013-10-30 04:20||garrigue||Note Added: 0010542|
|2013-10-30 09:53||frisch||Note Added: 0010543|
|2013-10-30 10:25||frisch||File Added: patch_6216.diff|
|2013-10-30 10:27||frisch||Note Added: 0010544|
|2013-10-30 10:33||xleroy||Note Added: 0010545|
|2013-10-30 10:41||xleroy||Note Added: 0010546|
|2013-10-30 11:26||frisch||Note Added: 0010547|
|2013-10-30 11:32||frisch||Note Edited: 0010547||View Revisions|
|2013-10-30 11:46||xleroy||File Added: cmmgen-patch.diff|
|2013-10-30 11:50||xleroy||Note Added: 0010548|
|2013-10-30 15:15||xleroy||Note Added: 0010549|
|2013-10-30 15:15||xleroy||Assigned To||garrigue => xleroy|
|2013-10-30 15:15||xleroy||Status||assigned => resolved|
|2013-10-30 15:15||xleroy||Resolution||open => fixed|
|2013-10-30 15:15||xleroy||Fixed in Version||=> 4.01.1+dev|
|2013-12-18 15:39||xleroy||Relationship added||related to 0006277|
|2015-12-11 19:25||xleroy||Status||resolved => closed|
|2017-02-23 16:35||doligez||Category||OCaml backend (code generation) => Back end (clambda to assembly)|
|2017-02-23 16:44||doligez||Category||Back end (clambda to assembly) => back end (clambda to assembly)|
|Copyright © 2000 - 2011 MantisBT Group|