Helping the value analysis — part 1

Introduction

This post introduces a new series about the art of helping the value analysis to be more precise. Until now, in the numerical precision series of this blog, this was easy enough. There was a single input variable and the obvious way to get more precise output values was to subdivide the range for that input variable. Sometimes, it is more complicated.

The example

The example we are going to look at in this series is an interpolation function. It is similar to the sine example seen previously but here the divisions of the function's definition interval are not uniform. The sub-intervals on which the function is implemented as a linear interpolation have been carefully chosen by the designers to minimize the occupied memory while providing appropriate precision.

struct point { double x; double y; }; 
struct point t[] = 
  { 0.     1.  
    0.125  1.00782267782571089  
    0.25   1.03141309987957319  
    0.5    1.1276259652063807  
    1.     1.54308063481524371  
    2.     3.76219569108363139  
    5.     74.2099485247878476  
    10.    11013.2329201033244 }; 

The interpolation function calls function choose_segment to get an index i indicating the segment to use. It then computes its result by interpolation of x between the points t[i] and t[i+1].

/*@ requires 0. <= x <= 10. ; */ 
double interp(double x) 
{ 
  double x0  x1  y0  y1; 
  int i; 
  i = choose_segment(x); 
  x0 = t[i].x; 
  y0 = t[i].y; 
  x1 = t[i+1].x; 
  y1 = t[i+1].y; 
  return (y1 * (x - x0) + y0 * (x1 - x)) / (x1 - x0); 
} 

We are supposed to verify that function interp above is free of run-time errors but auxiliary function choose_segment is not yet available for some reason. All we have is the specification it is supposed to satisfy.

Part of the specification has been formally written in ACSL:

/*@ 
  requires 0. <= x <= 10. ; 
  assigns \ 
othing ; 
  ensures 0 <= \esult <= 6 ; */ 
int choose_segment(double x); 

Of course this ACSL specification of choose_segment is partial: it does not completely caracterize what the function is supposed to do (the function is supposed to select the right segment not just any segment which is what the ACSL contract says). Nevertheless if we can verify the safety of function interp using only this contract for function choose_segment it will be a feather in our cap and we will only need to check that choose_segment statisfies its own specification when it finally arrives.

First analysis

The first step is always to launch an imprecise analysis to gauge the situation:

frama-c -val -main interp interp.c 

Four messages in the log are related to the verification process:

interp.c:20:[value] Function interp: precondition got status unknown 

This is the pre-condition for the function we are verifying. It is normal for this property not to be verified: it is interp's callers' job to make sure that the condition expressed here is met.

interp.c:24:[value] Function choose_segment: precondition got status valid 

The value analysis has verified that auxiliary function choose_segment was called in the conditions defined by its contract.

interp.c:24:[value] Function choose_segment: postcondition got status unknown 

Again it is normal for the annotation here not to be verified: it is supposed to be ensured by choose_segment's body which is not available.

interp.c:28:[kernel] warning: float operation: assert \is_finite((double )((double )((double )(y1*(double )(x-x0))+(double ) (y0*(double )(x1-x)))/(double ) (x1-x0))); 

Because of subtle differences between ACSL and C a lot of casts have been inserted but this assertion means the analyzer is worried that the value computed by the function to be returned might be an infinite or NaN.

Inspecting the toplevel operation in the formula (which is the problematic one: the value analysis would warn individually about sub-expressions if it thought one contained an additional problem) we see it is a division by x1 - x0. An issue would be if this expression was zero or unreasonably close to zero. Further inspection shows that x0 = t[i].x and x1 = t[i+1].x. From this we deduce that x1 is always strictly greater than x0 and more specifically that x1 - x0 >= 0.125 which should preclude any possibility of overflow considering that the values for variables y0 and y1 cannot be unreasonably large themselves.

What next?

We could stop here if we wished: there was a single place the value analysis was worried about and we have used a code review to check that the dangerous-looking operation was indeed safe. This is a standard way of proceeding especially for non-critical code. However the reasoning we made to reach the conclusion that the division was safe is informal and there could be a mistake in it. In a next post we will try to make the analysis say that the division is safe which will be more satisfying. Here is the file in case you wish to try it at home. Another possible exercise if to complete the contract of choose_segment and/or implement it. If you do both you can check your implementation against your specification with a deductive verification plug-in.

This post is co-authored by Kerstin Hartig.