Skip to content
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

Closed
vicuna opened this issue Oct 29, 2013 · 9 comments
Closed

inlining of GADT matches generates invalid assembly #6216

vicuna opened this issue Oct 29, 2013 · 9 comments

Comments

@vicuna
Copy link

vicuna commented Oct 29, 2013

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

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

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:

  • 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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

Comment author: @xavierleroy

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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

Comment author: @xavierleroy

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)

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

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?

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)?

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

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.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2013

Comment author: @xavierleroy

Fixed (as per cmmgen-patch.diff) in 4.01 branch (commit 14251) and in trunk (commit 14252).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants