TP5 - Reduced products
The goal of this session is to implement in our analyzer the reduced products between two simple non-relational domains: the interval domain and the parity domain.
Parity domain
A first (straightforward) step is to implement a parity domain, able to discover whether each variable is even or odd. We suggest implementing a domain able to abstract a set of integers into a parity information (VALUE_DOMAIN signature), and apply it to the generic NonRelational functor we developed in the previous sessions, able to lift a VALUE_DOMAIN into an ENVIRONMENT_DOMAIN by assigning an abstract property independently to each variable.
Reduction
We wish to implement the reduced product in a generic way, with as few dependencies as possible on the domains we wish to combine.
Note that there are two choices: we can either develop a reduction at the ENVIRONMENT_DOMAIN level, or at the VALUE_DOMAIN level (as seen in the course). The later is simpler but is limited to non-relational domains. Nevertheless, we suggest working at the VALUE_DOMAIN level for simplicity, as this is all what is needed to combine intervals and parities.
Ideally, the reduced product is then a generic functor ReducedProduct taking three arguments:
- a first abstract domain module A:VALUE_DOMAIN;
- a second abstract domain module B:VALUE_DOMAIN;
- a module containing only the reduction function between the two domains: reduce:A.t -> B.t -> A.t * B.t
and the functor outputs a module of signature VALUE_DOMAIN.
(equivalently, the functor can take a single module argument that packs the two abstract domains and a reduction function)
That way, given two existing domain implementations, building their reduced product boils down to implementing only one new module, with a single function.
Author: Antoine Miné