softwarelanguageslab/maf

Parameterising the abstract domains for Scheme vectors and pairs

Opened this issue · 0 comments

While the abstract domains of most types that participate in ModularSchemeLattice are parameterised (e.g., you can use Constant.I for integers and Concrete.Sym for symbols in the same modular lattice), the way vectors are represented is not configurable. At the same time, multiple interesting representations of vectors are possible, and one may be preferable to another depending on the required precision (and performance) in the analysis. For instance, vectors can be represented with as much precision as possible (as was done previously), or they can be represented without any field-sensitivity by joining all values in that vector.

It should be relatively easy to define a VectorLattice[V] type class, for which different implementations can be provided that can be plugged into ModularSchemeLattice. Similarly (although less interesting), the abstract domain used to represent pairs ("cons-cells") could also be parameterised using a PairLattice[P] typeclass. As an added bonus, in terms of design and implementation, it would also be nice if all vector/pair-related operations could be factored out of ModularSchemeLattice, as they already are for other subdomains.