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:
val 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.