Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007653OCamltypingpublic2017-10-06 16:572017-10-09 19:21
Reportergasche 
Assigned Togasche 
PriorityhighSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.06.0+dev 
Target Version4.06.0+devFixed in Version4.06.0+dev 
Summary0007653: Infinite loop when typing Frama-C cabs2cil.ml (4.06-only regression)
DescriptionUnder 4.06.0+beta1+unsafe-string-default, ocamlc.opt barfs on the file

  src/kernel_internals/typing/cabs2cil.ml

of the Frama-C Silicon release (frama-c.20161101):

  https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/kernel_internals/typing/cabs2cil.ml [^]

This is a 4.06 regression, it compiles fine under 4.05.
Steps To Reproduceopam switch install 4.06.0+beta1+default-unsafe-string
opam install ocamlfind num ocamlgraph.1.8.7
cd /tmp
wget http://frama-c.com/download/frama-c-Silicon-20161101.tar.gz [^]
tar -xzvf frama-c-Silicon-20161101.tar.gz
cd frama-c-Silicon-20161101
wget https://raw.githubusercontent.com/ocaml/opam-repository/master/packages/frama-c-base/frama-c-base.20161101/files/4.05-support.patch [^]
patch -p1 < 4.05-support.patch
./configure
make
Additional InformationI noticed the problem because on Gallium's beefy machine, the compilation has been running for an hour and has not failed yet (but it now consumes 9Gio of memory).

On my personal machine, I just get a stack overflow. In my opam-builder runs on an equally weak machine, I got a nice (but long) stack trace, which I'll upload as a separate file on this issue.
TagsNo tags attached.
Attached Filestxt file icon backtrace.txt [^] (22,297 bytes) 2017-10-06 16:58 [Show Content]

- Relationships

-  Notes
(0018497)
gasche (developer)
2017-10-07 00:21

Bisecting indicates that this comes from (or was revealed by) the new let-rec check: https://github.com/ocaml/ocaml/pull/556 [^]
(0018502)
xleroy (administrator)
2017-10-07 17:01

For the record: ocamlgraph 1.8.7 from the main OPAM repo doesn't compile in 4.06 (string/bytes issue) so this cannot be reproduced easily.
(0018503)
gasche (developer)
2017-10-07 17:03

I edited the reproduction instruction (sorry) to use the switch 4.06.0+beta1+default-unsafe-string.
(0018505)
gasche (developer)
2017-10-07 17:18

I instrumented Typecore.check_recursive_bindings, which prints the following before the stack overflow:

<CHECK>
doSpecList convertCVtoAttr makeVarInfoCabs makeVarSizeVarInfo doAttr doAttributes cabsPartitionAttributes doType isVariableSizedArray doOnlyType makeCompType preprocessCast getIntConstExp isIntegerConstant doExp doBinOp doCondExp compileCondExp doCondition doPureExp doFullExp doInitializer blockInitializer doInit createGlobal createLocal doAliasFun doDecl doTypedef doOnlyTypedef assignInit blockInit doBody doStatement
BINDING: doSpecList
BINDING: convertCVtoAttr
BINDING: makeVarInfoCabs
BINDING: makeVarSizeVarInfo
BINDING: doAttr
BINDING: doAttributes
BINDING: cabsPartitionAttributes
BINDING: doType
BINDING: isVariableSizedArray
BINDING: doOnlyType
BINDING: makeCompType
BINDING: preprocessCast
BINDING: getIntConstExp
BINDING: isIntegerConstant
BINDING: doExp

It first displays the name of all recursively-defined identifiers, and then the one that is currently being checked. This means that the error occur while checking this binding:

  https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/kernel_internals/typing/cabs2cil.ml#L5239-L7084 [^]

which is only 1845 lines long...
(0018508)
gasche (developer)
2017-10-07 18:52

I am starting to believe that this may be an extreme performance degradation (instead of an infinite loop) caused by design or implementation choices in the let-rec check. I'll start a discussion in the original let-rec check PR.
(0018509)
gasche (developer)
2017-10-07 21:57

Re-reading the discussion in GPR#556, I just noticed that this very specific performance issue was already noticed by Jeremy and fixed by replacing Ident.tbl by Map. Except the patch that finally went into 4.06 does not have this change! I think Jeremy did a mistake in a rebase and some of this work did not get into the merge version...
(0018518)
gasche (developer)
2017-10-09 19:21

The bug was indeed fixed by merging Jeremy's missing patch (in 4.06 and trunk).

- Issue History
Date Modified Username Field Change
2017-10-06 16:57 gasche New Issue
2017-10-06 16:58 gasche File Added: backtrace.txt
2017-10-07 00:21 gasche Note Added: 0018497
2017-10-07 17:01 xleroy Note Added: 0018502
2017-10-07 17:02 gasche Steps to Reproduce Updated View Revisions
2017-10-07 17:03 gasche Note Added: 0018503
2017-10-07 17:18 gasche Note Added: 0018505
2017-10-07 17:42 xleroy Severity minor => major
2017-10-07 17:42 xleroy Status new => acknowledged
2017-10-07 18:52 gasche Note Added: 0018508
2017-10-07 21:57 gasche Note Added: 0018509
2017-10-09 19:21 gasche Note Added: 0018518
2017-10-09 19:21 gasche Status acknowledged => resolved
2017-10-09 19:21 gasche Fixed in Version => 4.06.0+dev
2017-10-09 19:21 gasche Resolution open => fixed
2017-10-09 19:21 gasche Assigned To => gasche


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker