0000624: Logging huge messages makes kernel crashing

(0001270)
pascal (reporter)
2010-11-12 14:09

The crash is in the message-printing module. I guess that module should never request the creation of a string of length more than Sys.max_string_length, and display an explanation together with the beginning of the message being composed when it finds itself about to do so. You can circumvent the problem with option -quiet. Also, you can circumvent the problem by using the 64-bit version of Frama-C, where Sys.max_string_length is larger than you have memory for, but since we do not know what the message is and it's already unreasonably long, it may also fill your memory completely. The -quiet solution seems a better bet.

(0002537)
pascal (reporter)
2011-12-09 06:20

Backtrace rapportée par Stéphane Duprat le 9 décembre 2011: kernel] The full backtrace is: Raised by primitive operation at file "src/kernel/log.ml", line 197, characters 16-31 Called from file "format.ml", line 428, characters 6-72 Called from file "format.ml", line 435, characters 6-24 Called from file "format.ml", line 1145, characters 10-28 Called from file "src/memory_state/cvalue.ml", line 274, characters 12-44 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/memory_state/offsetmap.ml", line 253, characters 6-66 Called from file "src/lib/rangemap.ml", line 234, characters 16-21 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "format.ml", line 1154, characters 10-25 Called from file "format.ml", line 1154, characters 10-25 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "src/memory_state/lmap.ml", line 352, characters 9-241 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/value/eval_funs.ml", line 421, characters 6-136 Called from file "src/value/eval_funs.ml", line 554, characters 11-44 Re-raised at file "src/value/eval_funs.ml", line 570, characters 47-50 Called from file "src/project/state_builder.ml", line 1076, characters 9-13 Re-raised at file "src/project/state_builder.ml", line 1080, characters 15-18 Called from file "src/value/register.ml", line 46, characters 4-24 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8 Unexpected error (Invalid_argument("String.create")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Nitrogen-20111001. Note that a version and a backtrace alone often does not have information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [kernel] saving the current session into file "frama-c/out/IBU_Se_WriteUpdateObject.frm"

(0002644)
correnson (manager)
2012-01-30 12:58

This was temporary fixed in 17078, but the solution is not complete. Messages larger than 262144 bytes are truncated with an ellipsis ("...") in the *middle* of the message. This limit is not (yet) modifiable by command-line option. From my point of view, this limit is still too large. This hight limit prevent some tests oracles from being truncated (cruise-control for instance). But I still think that producing large messages with 'MyPlugin.result' is a not a good idea. Things to discuss or do: - adding a command line option for the limit - remove 'MyPlugin.result' - make 'MyPlugin.result' to dump messages in console, like Log.print_delayed / Log.print_on_output, without emitting a recorded event message (no limit applies). - keep 'MyPlugin.result' and add 'MuPlugin.bigresult' for this purpose. - modify all plugins that output large messages and make them use Log.print_delayed instead of MyPlugin.result. [...]

(0003877)
yakobowski (manager)
2013-05-23 13:28

Fixed in Neon and onwards.

Issue History
Date Modified	Username	Field	Change
2010-11-10 17:04	teamod	New Issue
2010-11-10 17:53	signoles	Assigned To	=> pascal
2010-11-10 17:53	signoles	Status	new => assigned
2010-11-10 17:53	signoles	Category	Kernel => Plug-in > value analysis
2010-11-10 17:57	signoles	Relationship added	related to 0000623
2010-11-12 14:05	pascal	Assigned To	pascal => correnson
2010-11-12 14:09	pascal	Note Added: 0001270
2010-12-13 14:55	correnson	Status	assigned => acknowledged
2010-12-13 14:55	correnson	Category	Plug-in > value analysis => Kernel
2010-12-13 14:55	correnson	Target Version	=> Frama-C Carbon-20110201
2010-12-13 14:55	correnson	Summary	Frama finally crashes in the issues of 0000623 => Logging huge messages makes kernel crashing
2011-02-02 10:39	correnson	Target Version	Frama-C Carbon-20110201 => Frama-C Nitrogen-20110901
2011-02-02 10:43	signoles	Relationship added	related to 0000232
2011-09-30 13:42	correnson	Target Version	Frama-C Nitrogen-20111001 => Frama-C Oxygen-2012xx01
2011-12-09 06:20	pascal	Note Added: 0002537
2012-01-30 12:58	correnson	Note Added: 0002644
2012-09-11 11:53	signoles	Target Version	Frama-C Oxygen-2012xx01 =>
2012-12-17 14:02	yakobowski	Priority	normal => urgent
2012-12-17 14:02	yakobowski	Target Version	=> Frama-C Fluorine
2013-04-16 09:48	svn	Checkin
2013-04-17 08:53	signoles	Target Version	Frama-C Fluorine => Frama-C Neon-20140301
2013-05-23 13:28	yakobowski	Note Added: 0003877
2013-05-23 13:28	yakobowski	Status	acknowledged => resolved
2013-05-23 13:28	yakobowski	Resolution	open => fixed
2013-05-23 17:07	signoles	Fixed in Version	=> Frama-C Fluorine-20130501
2013-05-23 17:07	signoles	Status	resolved => closed
2013-05-23 17:15	signoles	Status	closed => resolved
2013-05-23 17:15	signoles	Fixed in Version	Frama-C Fluorine-20130501 =>
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed

Notes
(0001270) pascal (reporter) 2010-11-12 14:09	The crash is in the message-printing module. I guess that module should never request the creation of a string of length more than Sys.max_string_length, and display an explanation together with the beginning of the message being composed when it finds itself about to do so. You can circumvent the problem with option -quiet. Also, you can circumvent the problem by using the 64-bit version of Frama-C, where Sys.max_string_length is larger than you have memory for, but since we do not know what the message is and it's already unreasonably long, it may also fill your memory completely. The -quiet solution seems a better bet.

(0002537) pascal (reporter) 2011-12-09 06:20	Backtrace rapportée par Stéphane Duprat le 9 décembre 2011: kernel] The full backtrace is: Raised by primitive operation at file "src/kernel/log.ml", line 197, characters 16-31 Called from file "format.ml", line 428, characters 6-72 Called from file "format.ml", line 435, characters 6-24 Called from file "format.ml", line 1145, characters 10-28 Called from file "src/memory_state/cvalue.ml", line 274, characters 12-44 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/memory_state/offsetmap.ml", line 253, characters 6-66 Called from file "src/lib/rangemap.ml", line 234, characters 16-21 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "format.ml", line 1154, characters 10-25 Called from file "format.ml", line 1154, characters 10-25 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "src/memory_state/lmap.ml", line 352, characters 9-241 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/value/eval_funs.ml", line 421, characters 6-136 Called from file "src/value/eval_funs.ml", line 554, characters 11-44 Re-raised at file "src/value/eval_funs.ml", line 570, characters 47-50 Called from file "src/project/state_builder.ml", line 1076, characters 9-13 Re-raised at file "src/project/state_builder.ml", line 1080, characters 15-18 Called from file "src/value/register.ml", line 46, characters 4-24 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8 Unexpected error (Invalid_argument("String.create")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Nitrogen-20111001. Note that a version and a backtrace alone often does not have information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [kernel] saving the current session into file "frama-c/out/IBU_Se_WriteUpdateObject.frm"

(0002644) correnson (manager) 2012-01-30 12:58	This was temporary fixed in 17078, but the solution is not complete. Messages larger than 262144 bytes are truncated with an ellipsis ("...") in the middle of the message. This limit is not (yet) modifiable by command-line option. From my point of view, this limit is still too large. This hight limit prevent some tests oracles from being truncated (cruise-control for instance). But I still think that producing large messages with 'MyPlugin.result' is a not a good idea. Things to discuss or do: - adding a command line option for the limit - remove 'MyPlugin.result' - make 'MyPlugin.result' to dump messages in console, like Log.print_delayed / Log.print_on_output, without emitting a recorded event message (no limit applies). - keep 'MyPlugin.result' and add 'MuPlugin.bigresult' for this purpose. - modify all plugins that output large messages and make them use Log.print_delayed instead of MyPlugin.result. [...]

(0003877) yakobowski (manager) 2013-05-23 13:28	Fixed in Neon and onwards.