Possible bugs found my Modelchecker

[GoogleCodeExporter]

I tried to verify that the baseflight firmware does not have any obvious bugs 
like division by zero, array access out of bound, ...

To do this I used CBMC to verify the loop function in mw.c. Until now CBMC 
found two possible bugs. I'm not sure if this are real bugs as the tool works 
with non-deterministic assumptions and cannot check if the values that trigger 
the bug are present during normal operation.

In the function annexCode line 125: array out of bound when tmp=500 in statement

rcCommand[axis] = lookupPitchRollRC[tmp2] + (tmp - tmp2 * 100) * 
(lookupPitchRollRC[tmp2 + 1] - lookupPitchRollRC[tmp2]) / 100;

Line 803: possible integer overflow in statement

cycleTime = (int32_t)(currentTime - previousTime);

The verification is not finished yet and more bugs may be found. I will report 
back any further results.

Regards,
Johannes

Original issue reported on code.google.com by johannes...@gmail.com on 10 Oct 2013 at 11:41

[GoogleCodeExporter]

With some modifications the verification was successful.

Array out of bound access happens in the following statement when tmp=10

rcCommand[THROTTLE] = lookupThrottleRC[tmp2] + (tmp - tmp2 * 100) * 
(lookupThrottleRC[tmp2 + 1] - lookupThrottleRC[tmp2]) / 100;    // [0;1000] -> 
expo -> [MINTHROTTLE;MAXTHROTTLE] 

Some more integer overflow are reported. Most of them in context with access to 
the currentTime variable. 

Regards,
Johannes

Original comment by johannes...@gmail.com on 10 Oct 2013 at 2:19

[GoogleCodeExporter]

Interesting (and not surprising) about the out of bounds in that dumb code.
As for integer overflow, that's kind of intended.
Because in the calculations we just care about delta, so even if it overflows, 
the delta value is still OK.

Original comment by time...@gmail.com on 11 Oct 2013 at 1:39

[GoogleCodeExporter]

I checked the multiwii source and the same array out of bound access is present 
there. I will post this issue in the multiwii forum.

Original comment by johannes...@gmail.com on 11 Oct 2013 at 8:31

[GoogleCodeExporter]

Only one of the two array out of bound access bugs is present in the original 
multiwii source as well.

The according statement in the original firmware does not have this bug in the 
current version. 

annexCode line 125: array out of bound when tmp=500 in statement
rcCommand[axis] = lookupPitchRollRC[tmp2] + (tmp - tmp2 * 100) * 
(lookupPitchRollRC[tmp2 + 1] - lookupPitchRollRC[tmp2]) / 100;

The illegal access to the array lookupThrottleRC[tmp2 + 1] is also in the 
current multiwii version.

Original comment by johannes...@gmail.com on 11 Oct 2013 at 8:52

[GoogleCodeExporter]

I refined the verification procedure and found more issues. This time the cbmc 
does not use the default configuration but rather chooses an arbitrary 
configuration from the allowed range (I used the definitions of cli to generate 
those assumptions). This way every possible combination of configuration values 
are checked. This resulted in additional potential issues.

1) Div by zero in mw.c when mcfg.mincheck is 2000 in function annexCode
tmp = (uint32_t) (tmp - mcfg.mincheck) * 1000 / (2000 - mcfg.mincheck);       
// [MINCHECK;2000] -> [0;1000]

2) Div by zero in mw.c in function pidMultiWii
error = (int32_t)rcCommand[axis] * 10 * 8 / cfg.P8[axis];

3) arithmetic overflow on + in function pidMultiWii
errorGyroI[axis] = constrain(errorGyroI[axis] + error, -16000, +16000); // 
WindUp

4) Div by zero in function pidRewrite
delta = (delta * ((uint16_t)0xFFFF / (cycleTime >> 4))) >> 6;

5) arithmetic overflow on signed type conversion in function pidRewrite
axisPID[axis] = PTerm + ITerm + DTerm;

6) arithmetic overflow on float to signed integer type conversion in function 
mixTable
motor[i] = rcCommand[THROTTLE] * currentMixer[i].throttle + axisPID[PITCH] * 
currentMixer[i].pitch + axisPID[ROLL] * currentMixer[i].roll + 
-cfg.yaw_direction * axisPID[YAW] * currentMixer[i].yaw;

7) I'm not sure if this an arithmetic overflow that can really occur but cbmc 
reported it in function mixTable
motor[i] -= maxMotor - mcfg.maxthrottle;

8) Div by zero in getEstimatedAltitude (in the function getEstimatedAltitude 
many overflows/nan/... can occur)
vel_acc = (float)accSum[2] * accVelScale * (float)accTimeSum / 
(float)accSumCount;

Original comment by johannes...@gmail.com on 12 Oct 2013 at 1:22