Re: [boost] Formal Review for Interval Library beginning

From: Fernando Cacciola (fcacciola_at_[hidden])
Date: 2002-09-06 13:56:29

----- Original Message -----
From: "Douglas Gregor" <gregod_at_[hidden]>
To: <boost_at_[hidden]>
Sent: Friday, September 06, 2002 3:11 PM
Subject: Re: [boost] Formal Review for Interval Library beginning

> On Friday 06 September 2002 01:30 pm, Fernando Cacciola wrote:
> > If the expression (x<y) is of type bool, then the static analysis of a
> > program containing it can 'trace' either of two execution branches.
> > If the expression (x<y) if of type tribool, then the static analysis of
a
> > program containing it can 'trace' both branches simultaneously. I
> > understand that such an analysis is very useful, for instance, for
> > optimizers (is this what you are actually doing?)
> >
> > But, is then tribool useful *only* for the static analysis of the
program?
>
> I think you've been snagged by the linguistic trap that hides near static
> analysis discussions :)

Oh... silly me :-)

>We're talking about two different programs here: (1)
> the user program which uses only integers and booleans and (2) the static
> analyzer program.
>
> This is a user program:
>
> 1:  int x, y;
> 2:  // x and y get their values here
> 3:  if (x < y)
> 4:    foo();
> 5:  else
> 6:    bar();
>
> No tribools, intervals, etc. in the program. When it executes the 'x < y',
we
> will get either true or false, because integer comparisons in the user
> program only use 2-state logic.
>
> Now, consider writing the static analyzer. Because the program's input
changes
> every time it is run, we have to approximate the values of program
variables
> (e.g., x, y, and the result of 'x < y') in a way that covers _all_
executions
> of the code. One common way to represent the values that an integer
variable
> (in the user program) could take is via intervals. For instance, in some
> simple user code like this:
>
> 1: int x;
> 2: if (some_condition)
> 3:   x = 3;
> 4: else
> 5:   x = 5;
> 6: // ...
>
> When we get to line 6 when the user program is running (really running,
not in
> the analysis), the value of 'x' will be either 3 or 5. However, when we
> analyze all paths, we end up following the code like this:
>
> at line 1, x is somewhere in the interval [-Infinity, Infinity]
> at line 2, we don't know what the condition does, so follow both 'if' and
> 'else' simultaneously
> at line 3: x is in the interval [3:3]
> at line 5: x is in the interval [5:5]
> at line 6, x might be in the interval [3,3] (if some_condition) or it
might be
> in the interval [5,5] (if !some_condition), so we approximate by taking
the
> union of its possible values, so we know only that x is in the interval
> [3,5].
>
> The same example works for boolean user variables with the 'tribool'
class:
>
> 1: bool b;
> 2: if (some_condition)
> 3:   b = true;
> 4: else
> 5:   b = false;
> 6: // ...
>
> When the static analysis _symbolically_ runs the program, at line 6 it
only
> knows that b might be true, or it might be false; so it needs the value of
b
> to be the indeterminate state. Just like we approximate integer values by
the
> intervals that are bounded in, we approximate boolean values using this
> indeterminate state.
>
> Of course, as soon as we approximate, we lose some information. Back to
> 'if (x < y)' example: when the program actually runs (not symbolically!),
x
> and y have definite values so 'x < y' gives a boolean result; but when we
> analyze the program (running it symbolically), the inaccuracies of the
> interval bounding representation of 'x' and 'y' make it possible that we
> don't know the exact relationship between 'x' and 'y' (remember: this
> relationship could change because of different inputs to the program when
it
> actually runs), thus the result of comparison is any of 'true for every
> program input', 'false for every program input', or 'can't determine if it
is
> true or false for all program inputs'.
>
OK. Thank you for this short but quite clear introduction to static
analysis!

So, the analyzer code uses intervals to track the possible values of the
symbolic variables.
And conditional expressions are symbolically deal with tribool.
I can see that...

Fernando Cacciola
Sierra s.r.l.
fcacciola_at_[hidden]
www.gosierra.com