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

Infinite loop when typing Frama-C cabs2cil.ml (4.06-only regression) #7653

Closed
vicuna opened this Issue Oct 6, 2017 · 7 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

commented Oct 6, 2017

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 6, 2017

Comment author: @gasche

Bisecting indicates that this comes from (or was revealed by) the new let-rec check: #556

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 7, 2017

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 7, 2017

Comment author: @gasche

I edited the reproduction instruction (sorry) to use the switch 4.06.0+beta1+default-unsafe-string.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 7, 2017

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 7, 2017

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 7, 2017

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 9, 2017

Comment author: @gasche

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

@vicuna vicuna closed this Oct 9, 2017

@vicuna vicuna added this to the 4.06.0 milestone Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.