New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
inlining of GADT matches generates invalid assembly #6216
Comments
Comment author: @garrigue This looks like a hard one. |
Comment author: @garrigue Added a test in basic-more/pr6216.ml, but no idea yet how to fix that. |
Comment author: @alainfrisch Other potential optimizations might be affected as well (see #5204 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:
|
Comment author: @alainfrisch 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. |
Comment author: @xavierleroy This example is a lot of fun.
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. |
Comment author: @xavierleroy PS: the same problem occurs with Obj.magic, e.g. let f (x: float) = |
Comment author: @alainfrisch 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) (#5204 is one such strategy, other are possible). Don't you agree?
Does my patch look correct to you (in particular the fact that identifiers are mutated imperatively during the compilation)? |
Comment author: @xavierleroy 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. |
Comment author: @xavierleroy Fixed (as per cmmgen-patch.diff) in 4.01 branch (commit 14251) and in trunk (commit 14252). |
Original bug ID: 6216
Reporter: @mshinwell
Assigned to: @xavierleroy
Status: closed (set by @xavierleroy on 2015-12-11T18:25:31Z)
Resolution: fixed
Priority: high
Severity: major
Version: 4.01.0
Fixed in version: 4.01.1+dev
Category: back end (clambda to assembly)
Related to: #6277
Monitored by: @diml sweeks @alainfrisch
Bug 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.
File attachments
The text was updated successfully, but these errors were encountered: