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

Segmentation fault with a program compiled by OCaml 3.11.1, 3.11.2, 3.12.0beta1 (bytecode, native, Linux AMD64 and MacOS X) #5109

Closed
vicuna opened this issue Jul 19, 2010 · 13 comments
Assignees
Labels

Comments

@vicuna
Copy link

vicuna commented Jul 19, 2010

Original bug ID: 5109
Reporter: monate
Assigned to: @xavierleroy
Status: closed (set by @xavierleroy on 2012-03-24T14:01:41Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 3.12.0+beta1 or 3.12.0+rc1
Fixed in version: 3.12.1+dev
Category: ~DO NOT USE (was: OCaml general)
Monitored by: phillyg mehdi "Pascal Cuoq" @glondu "Julien Signoles" prevosto

Bug description

Dear OCaml developers,

The code contained in the tar file available at
http://frama-c.com/framac_stripped_bug.tar.bz2
produces a deterministic segmentation fault.
It can be reproduced using:
./configure
make
bin/toplevel.byte bug.c

I tried to recompile OCaml 3.11.1 with #define DEBUG added in byterun/gc_ctrl.c but the heap consistency checks are ok.
Using ocamldebug a backtrace is available and seems to indicate that the call to Cil_const.CurrentLoc fails.
Strangely if one removes the line 63 of cil/src/cil_const.ml the bug disappears.

Do not hesitate to ask for more advanced tests from me.
Cheers,
Benjamin

File attachments

@vicuna
Copy link
Author

vicuna commented Jul 20, 2010

Comment author: @ygrek

404

@vicuna
Copy link
Author

vicuna commented Jul 20, 2010

Comment author: monate

Sorry: the correct link is

http://frama-c.com/frama-c_stripped.tar.bz2

@vicuna
Copy link
Author

vicuna commented Jul 21, 2010

Comment author: Pascal Cuoq

Note: all references to Obj functions have been erased from this "stripped" reproduction case. There are references to Obj.t, but the expressions that take these types are all "raise exn;"

@vicuna
Copy link
Author

vicuna commented Jul 21, 2010

Comment author: @ygrek

cil/src/fronc/cparser.mly
insert in line 1372 (before doFunctionDef)
Printf.printf "parser %d %d %d\n%!" (Obj.magic (fst3 $2) : int) (Obj.magic (snd3 $2) : int) (Obj.magic (trd3 $2) : int);
$ bin/toplevel.byte bug.c | grep parser
parser 70006161577636 70006161585852 0
Adding
Format.printf "%a@." d_cabsloc (trd3 $2);
will crash right there in the parser

@vicuna
Copy link
Author

vicuna commented Jul 21, 2010

Comment author: monate

I'm impressed! How did you track this behavior?
If I understand correctly this looks like a bug of ocamlyacc: the representation of the value returned by Parsing.peek_val does not match the type it gets.

@vicuna
Copy link
Author

vicuna commented Jul 22, 2010

Comment author: @ygrek

The key is to note that v passed to CurrentLoc.set is bad (reason of a crash). Than trace it back to the point of origin with grep+sed+printf (or better camlp4 :)
(trd3 $2) corresponds to RBRACE, but ocamllex emits correct value, so indeed it seems like the bug in ocamlyacc, hard to believe though..

@vicuna
Copy link
Author

vicuna commented Nov 24, 2010

Comment author: Julien Signoles

The above link does not work anymore :-(.

See http://bts.frama-c.com/view.php?id=626 for an easy way to reproduce something which looks like the very same bug (but with an unstripped Frama-C version which contains references to Obj, sorry OCaml Folks).

@vicuna
Copy link
Author

vicuna commented Nov 24, 2010

Comment author: phillyg

Benjamin, I'm wondering whether you can still reproduce the bug on your linux machine. if so, please email me at philip@pgbovine.net ... i might be able to help debug.

@vicuna
Copy link
Author

vicuna commented Nov 26, 2010

Comment author: prevosto

A more or less minimal code (with only the two parsers and lexers for C and ACSL) that reproduces the issue is at

http://dl.dropbox.com/u/6149559/bug_5109_minimal.tar.gz

just type make to build it and run the test case

It seems that there is somehow an interference between Cparser and Logic_parser, which causes in the end Cparser to get a null pointer instead of the real CODE_ANNOT.
Note that there is no segfault anymore, as the program does not do anything with the value, still, we shouldn't get as output

In parser, annot is 0,

@vicuna
Copy link
Author

vicuna commented Nov 30, 2010

Comment author: @ygrek

There are two parsers used recursively (i.e. cparser calls clexer which calls logic_parser). IIUC this is not supported by ocamlyacc - see let env = in stdlib/parsing.ml - so either coalesce the parsers or use menhir..

@vicuna
Copy link
Author

vicuna commented Dec 1, 2010

Comment author: @xavierleroy

The repro case works, thanks. In response to ygrek: It is true that the Parsing module has some global state, but it tries to support nested parsers nonetheless (see function Parsing.yyparse). This said, the bug might very well be in this support for reentrancy.

@vicuna
Copy link
Author

vicuna commented Dec 6, 2010

Comment author: @ygrek

Looks like restoring env.lval solves this issue

@vicuna
Copy link
Author

vicuna commented Dec 22, 2010

Comment author: @xavierleroy

Thanks for the "restore_lval" patch, which I applied in the 3.12 bugfix branch. It will go in release 3.12.1.

For the record: the original code in Parsing envisioned the case where a parser is called from a semantic action of another parser, but not the case where a parser is called from the lexer of another parser, as in the case in the Frama-C example. In the former case, env.lval is irrelevant, but in the latter case, it is necessary to preserve its value.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants