Infinite loop when typing Frama-C cabs2cil.ml (4.06-only regression) #7653
Comments
|
Comment author: @xavierleroy 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. |
|
Comment author: @gasche I edited the reproduction instruction (sorry) to use the switch 4.06.0+beta1+default-unsafe-string. |
|
Comment author: @gasche I instrumented Typecore.check_recursive_bindings, which prints the following before the stack overflow: 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: doExpIt 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: which is only 1845 lines long... |
|
Comment author: @gasche 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. |
|
Comment author: @gasche Re-reading the discussion in #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... |
|
Comment author: @gasche The bug was indeed fixed by merging Jeremy's missing patch (in 4.06 and trunk). |
Original bug ID: 7653
Reporter: @gasche
Assigned to: @gasche
Status: resolved (set by @gasche on 2017-10-09T17:21:23Z)
Resolution: fixed
Priority: high
Severity: major
Version: 4.06.0 +dev/beta1/beta2/rc1
Target version: 4.06.0 +dev/beta1/beta2/rc1
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Monitored by: @gasche @yakobowski
Bug description
Under 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 reproduce
opam 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 information
I 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.
File attachments
The text was updated successfully, but these errors were encountered: