Efficient interval representation

Hi,

I've a basic question. Let's assume I want to statically
analyze a program using abstract interpretation. I want
to represent an unsigned char variable in its abstract
form using intervals. Further, let's assume that the variable
is represented by the interval <10..255> at some point
of the program (program under analysis is a C source, so the
data type unsigned char has a bit length of 8).

When I now add a constant to that value, let's say <5..5>,
I have a wrap-around. IMHO, there are not two ways how to
represent the result:
a) again <0..255>. However, here I have a loss of precision
since the values <5..14> are actually not possible in the
sum
b) the result is represented by two intervals:
<0..4> and <15..255>. This form fosters precision since just
feasible values are given

The first representation has the advantage that I keep the
number of intervals small (just one interval for each
variable) but loose precision so that I probably get high
overestimations the longer the analysis proceeds. On the
other hand, the second representation keeps the calculations
precise but the computation complexity increases and might
end up in a state explosion that becomes too complex to compute.

What is done in practice in such a case?

One idea to handle this trade-off between complexity and precision
that comes into my mind might be to define the number of maximal
intervals for each variable (if further intervals are required they
must be somehow merged with the present results to not exceed the
max. #intervals).

Or do you see any other solutions?

Best regards,
Tim
.

Relevant Pages

  • Re: Efficient interval representation
    ... analyze a program using abstract interpretation. ... data type unsigned char has a bit length of 8). ... here I have a loss of precision since the values are actually not possible in the ... The first representation has the advantage that I keep the ...
    (comp.programming)
  • Efficient interval representation
    ... analyze a program using abstract interpretation. ... data type unsigned char has a bit length of 8). ... here I have a loss of precision ... The first representation has the advantage that I keep the ...
    (comp.theory)
  • Re: The spinoza papers: design of the extra-precision number object 2
    ... doesnt terminate, which cause practical problems, e.g in representation ... that we have an exact number. ... Limiting the precision doesn't change this claim. ... including quantum uncertainty represented as ...
    (comp.programming)
  • Re: more than 16 significant figures
    ... >> Java specifies IEEE 754-1985 representation for floating point. ... It specifies 53 bits of precision for doubles, ... one non-significant bit results in a value with two non-significant ... loss of any extended precision available to the hardware. ...
    (comp.lang.java.programmer)
  • Re: Maths error
    ... quantities delivers the exact decimal result, /provided/ that precision is ... they both lose info when rounding does occur. ... All forms of fp are subject to representation and rounding errors. ... precision is set high enough to retain all the input digits. ...
    (comp.lang.python)