Csmith testing reveals that I'm no good at probabilities (and lazy)
Pascal Cuoq - 10th Aug 2011Csmith testing
A typical Frama-C Csmith testing script repeats four actions in an infinite loop:
- getting a random program from Csmith;
- compiling and executing it;
- analyzing it with Frama-C;
- using the results from step 3, possibly together with those of step 2, to determine whether the program reveals something that would interest a Frama-C developer.
Step four is the difficult part. I definitely want to hear about varied events that could happen during the analysis, and step four represents about half the testing script's line count. One difficulty is that if a Frama-C bug has already been identified, but isn't fixed yet, I do not want to be warned again about that bug until it is supposed to have been fixed. Sometimes it is possible to use Csmith command-line options to generate only programs that do not trigger the bug. Sometimes, this is impossible, and you have to recognize the bug in step 4.
A particular known bug in Frama-C was characterized by the backtrace below, that I am posting in its entirety to give you a chance to identify my mistake before I tell you about it.
Raised at file \src/memory_state/new_offsetmap.ml" line 361 characters 26-37
Called from file "src/memory_state/new_offsetmap.ml" line 377 characters 17-64
Called from file "src/memory_state/new_offsetmap.ml" line 1394 characters 15-34
Called from file "src/memory_state/new_offsetmap.ml" line 1436 characters 18-114
Called from file "set.ml" line 293 characters 37-58
Called from file "src/memory_state/new_offsetmap.ml" line 1433 characters 11-399
Called from file "src/memory_state/offsetmap.ml" line 1308 characters 18-93
Called from file "src/memory_state/lmap.ml" line 641 characters 24-260
Called from file "src/memory_state/lmap.ml" line 626 characters 18-1023
Called from file "src/memory_state/cvalue.ml" line 1171 characters 12-50
Called from file "src/value/eval_exprs.ml" line 1399 characters 4-61
Called from file "src/value/eval_exprs.ml" line 1447 characters 4-75
Called from file "src/value/eval_exprs.ml" line 1058 characters 8-66
Called from file "src/value/eval_exprs.ml" line 986 characters 10-62
Called from file "src/value/eval_exprs.ml" line 1056 characters 8-52
Called from file "src/value/eval_exprs.ml" line 1207 characters 4-55
Called from file "src/value/eval_stmts.ml" line 446 characters 6-105
Called from file "src/value/eval_stmts.ml" line 880 characters 54-69
Called from file "list.ml" line 74 characters 24-34
Called from file "src/memory_state/state_set.ml" line 26 characters 2-24
Called from file "src/value/eval_stmts.ml" line 889 characters 14-232
Called from file "cil/src/ext/dataflow.ml" line 320 characters 29-47
Called from file "cil/src/ext/dataflow.ml" line 497 characters 8-21
Called from file "cil/src/ext/dataflow.ml" line 501 characters 9-22
Called from file "src/value/eval_funs.ml" line 100 characters 14-37
Called from file "src/value/eval_funs.ml" line 502 characters 8-63
Called from file "src/value/eval_stmts.ml" line 819 characters 12-71
Called from file "src/value/eval_stmts.ml" line 831 characters 10-114
Called from file "src/value/eval_stmts.ml" line 864 characters 38-62
Called from file "list.ml" line 74 characters 24-34
Called from file "src/value/eval_stmts.ml" line 920 characters 26-79
Called from file "cil/src/ext/dataflow.ml" line 320 characters 29-47
Called from file "cil/src/ext/dataflow.ml" line 497 characters 8-21
Called from file "cil/src/ext/dataflow.ml" line 501 characters 9-22
Called from file "src/value/eval_funs.ml" line 100 characters 14-37
Called from file "src/value/eval_funs.ml" line 502 characters 8-63
Called from file "src/value/eval_stmts.ml" line 819 characters 12-71
Called from file "src/value/eval_stmts.ml" line 831 characters 10-114
Called from file "src/value/eval_stmts.ml" line 864 characters 38-62
Called from file "list.ml" line 74 characters 24-34
Called from file "src/value/eval_stmts.ml" line 920 characters 26-79
Called from file "cil/src/ext/dataflow.ml" line 320 characters 29-47
Called from file "cil/src/ext/dataflow.ml" line 497 characters 8-21
Called from file "cil/src/ext/dataflow.ml" line 501 characters 9-22
Called from file "src/value/eval_funs.ml" line 100 characters 14-37
Called from file "src/value/eval_funs.ml" line 482 characters 4-67
Called from file "src/value/eval_funs.ml" line 564 characters 11-44
Re-raised at file "src/value/eval_funs.ml" line 578 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 49 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 (New_offsetmap.Make(V).End_reached).
The uncaught exception comes from new_offsetmap:361 in an auxiliary function but in this particular case the place whence this auxiliary function is called (line 377 in the same file) is a good way to identify the bug. If the auxiliary function raises the same exception when the function is called from another place it's another bug. If it's from the same call it's the same bug.
I adapted my shell script to include the following test in step 4:
if grep "line 377" analysis_log then true # I do not know how to negate a condition in shell and I do not want to learn else ... # continue classifying the analysis
I wanted to grep for file name and line number but in the backtrace the file name is surrounded by quotes and I didn't know how to escape the quotes inside the grep command-line.
Mergeable Interval Maps
The file new_offsetmap.ml contains the implementation of the data structure described in a now inaccessible article (http://studia.complexica.net/Art/RI090101.pdf). Pages 6 to 33 are in English. Incidentally Dotclear does not seem to offer any way to specify that a linked document is half in one language and half in another.
Although the new data structure's implementation is far from complete it is useful for handling unions to occasionally translate from the old datastructure to the new one. Csmith generates programs where unions can be written through a member and read from another (the members are only of integral types). The old data structure can handle most sequences of write combinations having occurred before an union is read but a few complex combinations are not handled. Richard Bonichon and I already wrote the code to handle all possible combinations in the new data structure and it would be a waste of time to backport this work to the old data structure at this point.
You may have guessed that an exception is raised in this module because it's newer and full of bugs but in fact what is currently implemented already works quite well (one of the advantages of having lots of tests and a trusted reference implementation). The reason the new implementation detects bugs is that knowing in advance what it was going to be used for we included lots of assertion checks for conditions we knew weren't supposed to happen. The bug comes in much earlier during parsing and cannot conveniently be worked around when it is detected in this module.
My mistake
What mistake did I make? The backtrace I have shown is 55 lines long. Each of them contains the pattern "xxx lines" where the values for "xxx" are not independent but we'll assume that they are for the sake of this argument. All files are more than 377 lines long and some of them are more than 3779 lines long. It is not sufficiently improbable that my script would hide from me another bug with a completely different backtrace that just happens to contain "line 377" or even "line 3775".
I noticed this a few days ago. Resolute in my decision not to learn how to escape quotes in shell I decided to make false negatives much less likely by grepping for "line 377 characters 17-64" instead.
This is when I updated Frama-C from source control. The file new_offsetmap.ml being work in progress the file had been modified and the line that characterized the bug changed. So I gave up and started to experiment with grepping special characters. It turns out that it's possible to grep for doubles quotes by using the simple syntax below.
grep 'Raised at file "src/memory_state/new_offsetmap.ml"' analysis_log
What is the moral of this story? What I refused to learn was very simple; I eventually replaced an approximate test by another that is just as approximate but in a different way; if you see other angles please write them in the comments.
Aside
Are you thinking "55 frames in the call stack? What a bunch of bloated analysis framework! This thing must be completely useless!"? Then you are making judgments based on criteria you are familiar with and ignoring those that are new to you. A more correct reaction would be "I know how to implement a much lighter analyzer that will have all the same functionality and will be just as precise in 5000 lines of my favorite language over a week-end; I'll do that and show them."
Zaynah Dargaye provided useful comments on an early version of this post.