Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006216OCamlback end (clambda to assembly)public2013-10-29 21:142015-12-11 19:25
Assigned Toxleroy 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version4.01.1+dev 
Summary0006216: inlining of GADT matches generates invalid assembly
DescriptionInlining 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

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
/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.
TagsNo tags attached.
Attached Filesdiff file icon patch_6216.diff [^] (2,608 bytes) 2013-10-30 10:25 [Show Content]
diff file icon cmmgen-patch.diff [^] (2,501 bytes) 2013-10-30 11:46 [Show Content]

- Relationships
related to 0006277closed Compiler crash when turning on -unsafe option. 

-  Notes
garrigue (manager)
2013-10-30 01:08

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.
garrigue (manager)
2013-10-30 04:20

Added a test in basic-more/, 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.
frisch (developer)
2013-10-30 09:53

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, 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.
frisch (developer)
2013-10-30 10:27

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.
xleroy (administrator)
2013-10-30 10:33

This example is a lot of fun.

> Am I right that the problem is caused by the current float unboxing strategy in, 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.
xleroy (administrator)
2013-10-30 10:41

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)
frisch (developer)
2013-10-30 11:26
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)?

xleroy (administrator)
2013-10-30 11:50

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.
xleroy (administrator)
2013-10-30 15:15

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

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker