This blog post is a revised version of part of my submission to the ICPC 2011 Industry Challenge. Please, go ahead and read the challenge description. I could only paraphrase it without adding anything to it, and so I won't.
The study was made with the April development version of Frama-C, which differs from the last released version in a number of bugfixes (list of reported issues) and minor new features. Specifically, it uses the value analysis and dependencies computations (documented in this manual) and code navigation features. The latter reuse building blocks that were implemented for slicing.
The ever important first step: identify missing library functions
The first step, as the faithful reader of this blog would now know, before using the value analysis for anything is to identify library functions the program depends on:
frama-c impls.c main.c roco.c sim.c main_testcase_1.c -metrics -cpp-command "gcc -DTESTCASE=1 -C -E" ... Undefined functions (10): __builtin_inf (15 calls); __builtin_inff (15 calls); fprintf (2 calls); __swbuf (10 calls); __builtin_fabsf (15 calls); exp (1 call); __builtin_infl (15 calls); __builtin_fabsl (15 calls); __builtin_fabs (15 calls); fabs (9 calls); ...
The host computer's standard headers have been used, hence the
confusing __builtin_
prefixes. Better not rely on them: the robot's
operating system probably bears little resemblance to the host's.
Placeholder headers provided with Frama-C can be used instead:
frama-c impls.c main.c roco.c sim.c main_testcase_1.c -metrics -cpp-command "gcc -DTESTCASE=1 -C -E -nostdinc -I. -I/usr/local/share/frama-c/libc" ... Undefined functions (3): exp (1 call); fabs (9 calls); fprintf (2 calls); ...
Standard functions exp()
and fabs()
are missing from the Carbon release, but
have been added to the development version. With the development version, one
simply needs to list /usr/local/share/frama-c/libc/math.c
as a file of
the analysis project. Function exp()
is implemented as a value analysis
builtin, taking advantage of the host's own exp()
function.
If you wish to reproduce at home, you have to provide
your own implementation for exp()
. It may not need to be very accurate,
but it needs to be analyzable with Carbon's value analysis. A good way would
be to clean up the implementation from Sun that
everyone is using.
As I already said in previous posts, accessing the bits of a floating-point
representation directly is so 1990s. If someone removed these ugly and
obsolete manipulations, we would end up with a better implementation for
exp()
(and it would be analyzable with the value analysis from Carbon).
For fabs()
,
you can use the function below. An implementation from a library would
probably unset the sign bit in the IEEE 754 representation but, again,
Carbon's value analysis doesn't handle this precisely yet.
The implementation below is handled
precisely in the sense that a singleton for the input x
results in
a singleton for the returned value.
double fabs(double x){ if (x==0.0) return 0.0; if (x>0.0) return x; return -x; }
Finally, calls to fprintf()
, that do not have any
repercussions on the continuing execution, can be replaced with
calls to the Frama_C_show_each()
built-in. We can let the
pre-processor to do this for us,
passing the option -Dfprintf=Frama_C_show_each
to GCC when pre-processing.
Looking for unspecified/undefined behaviors
We are now ready to launch the value analysis. Since we anticipate testcases 2 and 3 to be very similar, we write a short script:
#!/bin/bash export CPP="gcc -Dfprintf=Frama_C_show_each -DTESTCASE=$1 -C -E -nostdinc -I. -I/usr/local/share/frama-c/libc" FILES="/usr/local/share/frama-c/libc/math.c impls.c main.c roco.c sim.c" TESTCASE="main_testcase_$1.c" exec frama-c ${FILES} ${TESTCASE} -val -slevel 50000 -unspecified-access -val-signed-overflow-alarms -calldeps -save state$1
About ten minutes after running script.sh 1 > log1
,
we obtain a log (long:~70MiB) and a state (~1MiB).
The log is long because it contains progression messages that are only intended to help identify
analysis issues, and can be ignored most of the time. The state contains all the information
that has been computed about the program, including values of variables,
in a very compact format.
The analysis is completely unrolled (because of option -slevel 50000
)
and precise until the end. This means that the value analysis has in
effect simulated the execution of the program with the inputs
provided in main_testcase_1.c
.
The log, despite its size, does not warn about any of the undefined or unspecified behaviors that the value analysis is guaranteed to identify (uninitialized access, use of a dangling pointer, overflows in signed integer arithmetics, invalid memory access, invalid comparison of pointers, division by zero, undefined logical shift, overflows in conversions from floating-point to integer, infinite or NaN resulting from a floating-point operation, undefined side-effects in expressions). This is very important. It means that we can rest assured that the strange dynamic behavior we are going to investigate is not caused by the misuse of one of C's dangerous constructs. Nothing would be more frustating than having to track the value of a variable which, according to the source code, is not supposed to change, but is modified through a buffer overflow. The value analysis guarantees we won't have to do that for this execution.
What would of course be better would be to verify that there can be none of the above undefined behaviors for any command sequence. This would be a much stronger result, but would also require a lot more work. When simulating a single execution inside the analyzer, we only check that that particular execution is free of undefined behavior, but it does not require any work from us (only a few minutes of work from the computer).
Exploiting the value analysis' results for program comprehension
The values computed and stored in state1
can be observed in
Frama-C's GUI, using the command-line frama-c-gui -load state1
.
The GUI can also be used to identify the definition
site(s) of a variable's value: select the variable at the program point you are interested in,
and in the contextual menu, invoke Dependencies → Show defs.
Here, it is the value of variable RoCo_engineVoltage
as displayed by the call to fprintf()
(that we transformed into a call
to Frama_C_show_each()
) that is wrong, so we request the definition site(s)
of that value:
The GUI has pointed us to a call to function RoCo_Process()
(using the yellow mark),
so we now request the definition
sites of RoCo_engineVoltage
by the return;
statement of that function.
We obtain the two sites identified below:
The condition that decides which branch is executing is the one shown in the screenshot below.
The value analysis tell us the value of RoCo_isActive
can be either 0
or 1
at this point during execution, but this variable is one of the variables whose value is printed in
the analysis log, and its value was 1
at the instant we are interested in. We therefore focus
on the definition site where the value assigned to RoCo_engineVoltage
is computed
in a call to PT1_Filter()
.
The dependencies of the particular call to PT1_Filter()
we are
interested in were computed by option -calldeps and can be found in the log.
The call we are interested in is at statement 433. The log contains:
call PT1_Filter at statement 433: voltageFilter FROM state; x; t1; dt; voltageFilter \result FROM state; x; t1; dt; voltageFilter
Apart from reading its arguments state
, x
, t1
, and dt
, the call accesses
a static variable voltageFilter
. The address of voltageFilter
is taken,
so we have to be careful: this variable could be modified erroneously
through a pointer (although the address-taking appears to be only to
pass it to PT1_Filter()
, which is innocent enough).
In fact, at this point, we have no idea which of the variables involved
in the computation of the result of this call to PT1_Filter()
is wrong.
Clicking on a variable in the GUI provides the set of values for this
variable at this program point, but this is still too imprecise here,
since it mixes all 10000 or so passages through the statement.
Let us take advantage of the "blackboard" structure of the analyzed
program and dump the entire program state at this statement,
by inserting a call to Frama_C_dump_each()
.
See this previous post for
a list of advantages of this built-in function over printf()
or a
debugger.
--- roco.c (revision 12956) +++ roco.c (working copy) @@ -293,6 +293,7 @@ desiredEngineVoltage, Engine_maxVoltage_PARAM); limitationActive = (Engine_maxVoltage_PARAM == desiredEngineVoltage) || (Engine_minVoltage_PARAM == desiredEngineVoltage); + Frama_C_dump_each(); RoCo_engineVoltage = PT1_Filter (&voltageFilter, desiredEngineVoltage, t13, dT); wasInit = init;
We need to launch the analysis again and find something to do for 10 minutes. This is a good time to start looking at bugs 2 and 3.
The log now contains state dumps for each passage through the statement
where RoCo_engineVoltage
is computed.
According to the ReadMe.txt
in the challenge package,
an order is given at t=50s. The log shows that this order
fails to be executed speedily.
The state dump at which lastTime
contains 50000
and the next few ones show that of RoCo_engineVoltage
's dependencies,
variable desiredEngineVoltage
is the one with the suspicious value: it is only
-0.8
, whereas parameters in file roco_config_testcase_1.h
and values of the variable elsewhere in our
log show that this voltage can go much higher. We are therefore left with the sub-problem of identifying why
this variable has this value at this program point.
We use the same tools we have already
used for RoCo_engineVoltage
, this time applied to variable desiredEngineVoltage
and this program point. The screenshot below shows the definitions sites for that value.
The value of variable desiredEngineVoltage
is defined by the call to function Limiter_Out()
,
whose argument is in turn defined by the call to Interpolate_from_curve()
above.
Option -calldeps computed the implicit inputs of this call, which can be found in the log:
call Interpolate_from_curve at statement 423: \result FROM curve; x; EngineSpeedToVoltage_CURVE{.numPoints; .x[0..4]; .y[1..3]; }
The state dump in which lastTime==50000
shows that a low value for
angleDiffRequest
is the cause for the low value of desiredEngineVoltage
.
The "Show defs" action in the GUI finds three possible definition sites for
this value of angleDiffRequest
, shown in the screenshots below.
We find in the log that variable rampValue
remains at 0
in the cycles
that follow instant 50000
. The value we observe for angleDiffRequest
is compatible with the algorithm and values of variables at lines
264-277 of file roco.c. So it looks like the cause of the issue
is the value of variable rampValue
. Action "Show defs" in the GUI
indicates that this value is computed by the call to Ramp_out()
at line 240.
The value of rampTarget
is computed as 0.0
or 1.0
from a number of
variables, and of these variables, RoCo_legAngleValid
was always 1,
and direction
was always 0
or 1
. The latter is suspicious, since
in this execution, orders are given to move in both directions:
The command "Show defs" applied to variable direction
shows that indeed,
the variable may have been set to 0
or 1
in three different sites.
The site that corresponds to the MoveByAngle command, the middle one in the screenshot above,
is suspicious: in the file main_testcase_1.c, the angle passed to this command is negative.
This is not just a strange convention, because the computation below for the third
definition site determined the direction for the other commands, that are all in
the opposite direction, and variable direction
was assigned 1
again there.
This suggests the fix below.
--- roco.c (revision 13019) +++ roco.c (working copy) @@ -211,7 +211,7 @@ direction = 0; } else { - direction = (RoCo_desiredDeltaAngle > 0.0) ? -1 : 1; + direction = (RoCo_desiredDeltaAngle > 0.0) ? 1 : -1; } RoCo_commandMoveByAngle = FALSE; }
Looking at the source code for related issues, one may notice that the value given to direction
is also affected by the piece of code below. It would be worth the time testing different values of
t9
and RoCo_hasMinMaxAngles_PARAM
, although that complex computation is
only active when using commands other than MoveByAngle.
if ((fabs(t9) > t11) && (direction == 0)) { direction = ((((!RoCo_hasMinMaxAngles_PARAM) || (fabs(t9) >= 180.0)) ? t9 : -t9) > 0.0) ? 1 : -1; }
Thanks, and Next
My colleagues Benjamin Monate and Virgile Prevosto found the challenge and set up the files in the development repository, so that the only thing that was left to do was to identify the bugs, and started looking at them with me. Anne Pacalet and David Mentré have provided feedback for transforming this submission into a blog post. Anne Pacalet also implemented of all the code navigation features used in this study. The organizers Jochen Quante and Andrew Begel have done an impressive job of making this challenge interesting, and indeed, challenging.
I have also submitted my explanation of tasks 2 and 3 in the challenge.
However, I thought someone might want
to look at these themselves now that I have shown how easy it is on task 1.
The only difficult part is finding an exp()
function.
To be continued...