TP 3 - Interval analysis

The goal of this session is to transform the denotational interpreter for our simple language developed in the first session into an abstract interpreter over the interval domain.

In addition to the provided front-end, the analyzer consists in two modules:

• an interval abstract domain;
• an iterator for our language.

These two parts should be made into modules as independent as possible so that:

• you can replace the interval domain with another one without changing the iterator (we will do this next week);
• you can reuse the interval domain for the static analysis project, which uses a different language and a very different intermediate representation for programs.

Iterator

The iterator should work by induction on the syntax tree of the program. It is actually very similar to the iterator used for the denotational concrete semantics. You can either start from your solution or start from scratch. The original archive with the parser is available here.

The main difference with the concrete semantics is the use of a widening to ensure the termination of the analysis For this practical exercise, we will focus on the simplest widening (no thresholds, no decreasing iterations).

Interval domain

We suggest that you create two modules:

• a module abstracting sets of integers as intervals;
• a functor lifting abstractions of sets of integers into abstractions of sets of mappings from variables to integers, using a non-relational abstraction (i.e. a map from variables to abstract sets of integers).

Additional advices on the project page.

During this practical exercise, you will only need to handle precisely simple tests, such as comparing a variable with another variable or a constant (we leave the case of arbitrary conditions for the project). In case the test is not simple, the analyzer should still be sound (e.g., by returning its environment argument unchanged).