softwarelanguageslab / maf

Static Analysis Framework for Modular Analyses
Other
13 stars 12 forks source link

Parameterising the abstract domains for Scheme vectors and pairs #20

Open noahvanes opened 3 years ago

noahvanes commented 3 years ago

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.