Astrée: RTE Analysis Examples

Control/command programs, in particular synchronous ones, manipulate thousands of boolean variables. Analyzing which program run-time properties hold when each boolean variable is either true or false rapidly leads to a combinatorial explosion of the number of cases to be considered.

Thanks to sophisticated algorithms, Astrée can handle thousands of boolean variables with just enough precision to avoid both false alarms and combinatorial explosion.

Here’s a simple example:

/* boolean.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN B;
void main () {
  unsigned int X, Y;
  while (1) {
    /* ... */
    B = (X == 0);
    /* ... */
    if (!B) {
      Y = 1 / X;
    };
    /* ... */
  };
}

The analysis of the above code by Astrée yields no warnings, thanks to the automatically de­termined relationship between B and X. Integer divide-by-zero can never happen when executing this program.

Command programs controlling complex physical systems are derived from mathematical mod­els designed with real numbers whereas computer programs perform floating-point computations. The two computation models are completely different, which can yield very surprising results.

Consider the following two programs:

/* float-error.c */
int main () {
    float x, y, z, r;

    x = 1.000000019e+38;
    y = x + 1.0e21;
    z = x - 1.0e21;
    r = y - z;
    printf("%f\n", r);
}
% gcc float-error.c
% ./a.out
0.000000

/* double-error.c */
int main () {
  double x; float y, z, r;
  /* x = ldexp(1.,50)+ldexp(1.,26); */
  x = 1125899973951488.0; 
  y = x + 1;
  z = x - 1;
  r = y - z;
  printf("%f\n", r);
}
% gcc double-error.c
% ./a.out
134217728.000000

One would expect these programs to print 2.0e21 and 2.0, respectively, based on the reasoning that (x+a)-(x-a) = 2a. However, this reasoning turns out to be wrong due to rounding errors.

Astrée is sound for floating-point computations and handles them precisely and safely. It takes all possible rounding errors into account, in addition to considering possible cumulative effects in programs running for hours.

Here’s another example:

/* float.c */
void main () {
  float x,y,z;
  if ((x < -1.0e38) || (x > 1.0e38)) return;
  while (1) {
    y = x+1.0e21;
    z = x-1.0e21;
    x = y-z;
  }
}

Astrée proves that the above program is free of run-time errors when running on a machine with floats on 32 bits.

Control/command programs perform lots of digital filtering, as shown by the following example:

/* filter.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN INIT;
float P, X;

void filter () {
  static float E[2], S[2];
  if (INIT) {
    S[0] = X;
    P = X;
    E[0] = X;
  } else {
    P = (((((0.5*X)-(E[0]*0.7))+(E[1]*0.4))+(S[0]*1.5))-(S[1]*0.7));
  }
  E[1] = E[0];
  E[0] = X;
  S[1] = S[0];
  S[0] = P;
}

void main () {
  X = 0.2 * X + 5;
  INIT = TRUE;
  while (1) {
    X = 0.9 * X + 35;
    filter ();
    INIT = FALSE;
  }
}

The absence of overflow (and more precisely that P is in [-1327.05, 1327.05] as found by Astrée) is not obvious, in particular because of 32-bit floating-point computations. The situa­tion becomes even more inextricable in the presence of boolean control or cascades of filters. Astrée knows enough about control theory to analyze filters precisely.