Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007702OCamlback end (clambda to assembly)public2017-12-30 15:152018-01-11 12:12
Reporterchengsun 
Assigned Togasche 
PrioritynormalSeveritycrashReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.06.0 
Target VersionFixed in Version4.07.0+dev 
Summary0007702: cmm miscompile: cross-module inlining causes catch ID collision
DescriptionThe attached code miscompiles (on 4.03.0 through trunk, no flambda) due to cross-module inlining.

The cmm generated for b.ml looks incorrect. As far as I can tell, an ID is generated for a catch lambda using next_raise_count, but this ID is already used in the clambda inlined from a.ml.


a.ml:

let _unused _ = try () with _ -> ()

let trigger_bug x =
  let ok =
    match x with
    | None
    | Some "" -> true
    | Some _ -> false
  in
  if x = Some "" && not ok then
    failwith "impossible"
[@@inline always]


b.ml:

let bug x = A.trigger_bug x


c.ml:

let () =
  B.bug (Some "");
  Printf.printf "Bug failed to trigger :(\n
Steps To Reproduce$ tar xzf bug.tar.gz
$ ./compile.sh
$ ./a.out
Fatal error: exception Failure("impossible")
TagsNo tags attached.
Attached Filesgz file icon bug.tar.gz [^] (452 bytes) 2017-12-30 15:15

- Relationships

-  Notes
(0018798)
nojebar (developer)
2017-12-31 10:00
edited on: 2017-12-31 10:04

The 4.06 cmm for A.trigger_bug is

(function{a.ml:3,16-166} camlA__trigger_bug_1004 (x/1005: val)
 (let
   ok/1006
     (catch
       (if (!= x/1005 1)
         (let switch/1210 (load_mut val x/1005)
           (catch
             (let size/1212 (>>u (load_mut int (+a switch/1210 -8)) 10)
               (if (>= size/1212 2) (exit 5)
                 (let cell/1211 (load_mut int (+a switch/1210 0))
                   (if (== cell/1211 504403158265495552a) (exit 2) (exit 5)))))
           with(5) 1a))
         (exit 2))
     with(2) 3a)
   (catch
     (if (!= (extcall "caml_equal"{a.ml:10,5-16} x/1005 "camlA__2" val) 1)
       (if (!= ok/1006 1) (exit 4)
         (app{a.ml:11,4-25} "camlPervasives__failwith_1005" "camlA__3" val))
       (exit 4))
   with(4) 1a)))

and the inlined cmm for A.trigger_bug inside B.bug is

(function{b.ml:1,8-27} camlB__bug_1002 (x/1003: val)
 (let
   ok/1008
     (catch
       (if (!= x/1003 1)
         (let switch/1009 (load_mut val x/1003)
           (catch
             (let size/1011 (>>u (load_mut int (+a switch/1009 -8)) 10)
               (if (>= size/1011 2) (exit 2)
                 (let cell/1010 (load_mut int (+a switch/1009 0))
                   (if (== cell/1010 504403158265495552a) (exit 2) (exit 2)))))
           with(2) 1a))
         (exit 2))
     with(2) 3a)
   (catch
     (if (!= (extcall "caml_equal"{a.ml:10,5-16} x/1003 "camlA__2" val) 1)
       (if (!= ok/1008 1) (exit 1)
         (app{a.ml:11,4-25} "camlPervasives__failwith_1005" "camlA__3" val))
       (exit 1))
   with(1) 1a)))

which is wrong because the two different catch ids 2, 5 in the first (catch ...) term appear as 2, 2 when inlined.

(0018799)
nojebar (developer)
2017-12-31 10:27

I think the problem is in the "string matching" compiler in strmatch.ml.
(0018800)
vlaviron (reporter)
2017-12-31 16:30
edited on: 2017-12-31 17:37

From a quick look: the bug comes from the cross-module inlining in closure.ml. Code loaded from external modules can contain staticfail indices that are bigger than Lambda.raise_count, which will cause the bug. This doesn't happen in flambda because flambda systematically recreates indices, but closure simply copies them, which is wrong with cross-module inlining.
I think the implementation of Closure.substitute from GPR#1482 would make a good start, if anyone else wants to work on it.

(0018801)
xclerc (reporter)
2018-01-02 12:24

Tentative patch, following vlaviron suggestion: https://github.com/ocaml/ocaml/pull/1553 [^]
(0018822)
gasche (developer)
2018-01-11 11:33

This was fixed in trunk by xclerc's pull request.
(0018823)
xclerc (reporter)
2018-01-11 12:00

As suggest by hhugo in the PR, shouldn't this be
back ported to 4.06?
(0018824)
gasche (developer)
2018-01-11 12:12

I don't know, and I don't have the bandwidth to deal with the question right now, so I just added a label on the PR.

- Issue History
Date Modified Username Field Change
2017-12-30 15:15 chengsun New Issue
2017-12-30 15:15 chengsun File Added: bug.tar.gz
2017-12-31 09:23 nojebar Status new => confirmed
2017-12-31 10:00 nojebar Note Added: 0018798
2017-12-31 10:04 nojebar Note Edited: 0018798 View Revisions
2017-12-31 10:27 nojebar Note Added: 0018799
2017-12-31 16:30 vlaviron Note Added: 0018800
2017-12-31 17:37 vlaviron Note Edited: 0018800 View Revisions
2018-01-02 12:24 xclerc Note Added: 0018801
2018-01-11 11:33 gasche Note Added: 0018822
2018-01-11 11:33 gasche Status confirmed => resolved
2018-01-11 11:33 gasche Fixed in Version => 4.07.0+dev
2018-01-11 11:33 gasche Resolution open => fixed
2018-01-11 11:33 gasche Assigned To => gasche
2018-01-11 12:00 xclerc Note Added: 0018823
2018-01-11 12:12 gasche Note Added: 0018824


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker