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

(0005609)
ygrek (reporter)
2010-07-20 09:10

404

(0005610)
monate (reporter)
2010-07-20 09:55

Sorry: the correct link is

http://frama-c.com/frama-c_stripped.tar.bz2 [^]

(0005611)
Pascal Cuoq (reporter)
2010-07-21 13:01

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;"

(0005612)
ygrek (reporter)
2010-07-21 18:46

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

(0005613)
monate (reporter)
2010-07-21 19:08

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.

(0005615)
ygrek (reporter)
2010-07-22 17:08

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

(0005714)
Julien Signoles (reporter)
2010-11-24 15:31

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

(0005716)
phillyg (reporter)
2010-11-24 19:13

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.

(0005720)
prevosto (reporter)
2010-11-26 19:34

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,

(0005726)
ygrek (reporter)
2010-11-30 11:47

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

(0005727)
xleroy (administrator)
2010-12-01 13:37

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.

(0005728)
ygrek (reporter)
2010-12-06 10:35

Looks like restoring env.lval solves this issue

(0005749)
xleroy (administrator)
2010-12-22 14:09

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.

Notes
(0005609) ygrek (reporter) 2010-07-20 09:10	404

(0005610) monate (reporter) 2010-07-20 09:55	Sorry: the correct link is http://frama-c.com/frama-c_stripped.tar.bz2 [^]

(0005611) Pascal Cuoq (reporter) 2010-07-21 13:01	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;"

(0005612) ygrek (reporter) 2010-07-21 18:46	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

(0005613) monate (reporter) 2010-07-21 19:08	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.

(0005615) ygrek (reporter) 2010-07-22 17:08	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..

(0005714) Julien Signoles (reporter) 2010-11-24 15:31	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).

(0005716) phillyg (reporter) 2010-11-24 19:13	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.

(0005720) prevosto (reporter) 2010-11-26 19:34	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,

(0005726) ygrek (reporter) 2010-11-30 11:47	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..

(0005727) xleroy (administrator) 2010-12-01 13:37	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.

(0005728) ygrek (reporter) 2010-12-06 10:35	Looks like restoring env.lval solves this issue

(0005749) xleroy (administrator) 2010-12-22 14:09	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.

Issue History
Date Modified	Username	Field	Change
2010-07-19 19:28	monate	New Issue
2010-07-20 09:10	ygrek	Note Added: 0005609
2010-07-20 09:55	monate	Note Added: 0005610
2010-07-21 13:01	Pascal Cuoq	Note Added: 0005611
2010-07-21 18:46	ygrek	Note Added: 0005612
2010-07-21 19:08	monate	Note Added: 0005613
2010-07-22 17:08	ygrek	Note Added: 0005615
2010-11-24 15:31	Julien Signoles	Note Added: 0005714
2010-11-24 19:13	phillyg	Note Added: 0005716
2010-11-26 19:34	prevosto	Note Added: 0005720
2010-11-30 11:47	ygrek	Note Added: 0005726
2010-12-01 13:37	xleroy	Note Added: 0005727
2010-12-01 13:37	xleroy	Status	new => acknowledged
2010-12-06 10:30	ygrek	File Added: restore_lval.diff
2010-12-06 10:35	ygrek	Note Added: 0005728
2010-12-22 14:09	xleroy	Note Added: 0005749
2010-12-22 14:09	xleroy	Status	acknowledged => resolved
2010-12-22 14:09	xleroy	Resolution	open => fixed
2010-12-22 14:09	xleroy	Fixed in Version	=> 3.12.1+dev
2010-12-22 14:11	xleroy	Assigned To	=> xleroy
2012-03-24 15:01	xleroy	Status	resolved => closed

Relationships