TD 2. Interval analysis in PAG/WWW, Part 1.

TD 2 : Interval analysis in PAG/WWW, Part 1.

You are expected to build a small interval analysis under PAG/WWW. You can start from scratch or from the constant propagation analysis. Here are a few guidelines to help you build your analysis step by step:

Definition of the abstraction

There are several possible representations of the lattice of intervals. Please discuss some possible representations, and shortly present your arguments in favour of your preference. Some questions you must ask yourselves are how do you represent the intervals top, bottom, whether you will plan to represent intervals with one finite and one infinite bound (or only both finite or both infinite, which is simpler but slightly less expressive) etc.

Now, you can:

write the TYPE section,
adapt the initializations in the PROBLEM section,
comment everything that is not strictly necessary in your analysis (for instance, have all transfer functions return something obviously true, that you will progressively refine) and compile it

Transfer functions: arithmetic operations

complete the evalAExp function so that it returns intervals (it may be convenient to define and use support functions addabstract, subabstract, multabstract ... taking 2 intervals as parameters, and returning respectively their sum, subtraction, multiplication, etc) so that your evalExp function will be easier to read
test your analysis at this point on test1.w and test2.w

Note that if you represent intervals by couples, in FULA, writing (a,b) creates the couple (a,b). And for a couple c=(a,b), c#1 gives its first element (a) and c#2 its second element (b). See also the documentation of the FULA language.

For the time being, we only analyzed programs where variables took point values:

propose a test example where arithmetic operations occur between variables that can take any value, or between a constant and a variable that can take any value, and make sure you analyze it correctly
propose a test example where the values of a variable at the end of the program can be in interval [0,2]; is it correctly analyzed, why ?

Transfer functions: lattice operations

define the union operator over States (for example join :: State * State -> State ) and use this union as the combine operator of your domain.
To define function join over states, you can use predefined function crunch (see the documentation of Built-in PAG/WWW functions) of PAG, which applies a function, given as a parameter to crunch, independently to each variable of the states (remember the states are defined as functions of the program variables to intervals).
For instance you can define
```
join :: State * State -> State 
join(a, b) = crunch(a,b,join_int)  
```
where function crunch applies independently to each variable of states a and b some function join_int over intervals (union of two intervals). Now you have to define this function:
```
join_int :: Interval * Interval -> Interval
join_int(i1,i2) = ...
  
```
you can now test your analysis on programs where the union is necessary:test3.w and test4.w (as well as your own examples)