softwarelanguageslab / maf

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

Factor out reference types in SchemeLattice #23

Open noahvanes opened 3 years ago

noahvanes commented 3 years ago

From a design perspective, the Value trait in ModularSchemeLattice is currently somewhat abused, in that both a Pointer and a Vector/Cons/String are subclasses of Value. However, only pointers can be part of “real” values (i.e., they are expressible values). In contrast, a vector/pair/string is only bound to an address in the store (i.e., they are storable values). Put differently, a VarAddr and a PtrAddr are both bound to an abstract value of type List[Value] in the store, although the former is actually guaranteed to not contain any Vector/Cons/String in that list, while the latter is guaranteed to find a list of length 1 with a Vector/Cons/String in it. This, however, is not well-reflected in the current design, and not in any way indicated by the type system (which therefore considers more types than necessary and needs extra guidance sometimes).

One possible (though somewhat radical) solution would be to factor storable values (aka "reference types") out of SchemeLattice entirely (so that a VarAddr is always bound to a value of type L (with SchemeLattice[L]), a PaiAddr always to a pair of type P (with PairLattice[P]) and a VecAddr always to a vector of type V (with VectorLattice[V])).