Currently, core lattices use single-parameter typeclasses to describe operations that need to be supported. For example, an implementation of the StringLattice[S] typeclass needs to define several string operations (e.g., stringRef, substring, append) for abstractions of strings represented by some type S.
The challenge is that some operations require a combination of several types. For instance, method stringRef of StringLattice[S] takes not only a string (of type S), but also an index as parameter. Currently, an implementation of method stringRef needs to work with any type I that is used to represent integers, given that a corresponding IntLattice[I] instance is provided.
The problem is that, by not being able to know the exact representation of I, the implementation becomes unnecessarily complex and inefficient. For instance, in the constant-propagation domain instance of StringLattice[S], method stringRef uses the following implementation:
def ref[I2: IntLattice, C2: CharLattice](s: S, i: I2): C2 = s match {
case Bottom => CharLattice[C2].bottom
case Top => CharLattice[C2].top
case Constant(x) =>
0.to(x.length)
.collect({
case i2
if BoolLattice[Concrete.B]
.isTrue(IntLattice[I2].eql[Concrete.B](i, IntLattice[I2].inject(i2))) &&
i2 < x.size =>
CharLattice[C2].inject(x.charAt(i2))
})
.foldLeft(CharLattice[C2].bottom)((c1, c2) => CharLattice[C2].join(c1, c2))
}
In case the given string (of known type S) itself is a known constant, it iterates over every possible index of that string to determine if it could possibly be abstracted by the given index (of unknown type I). Similar issues plague methods such as vectorRef and vectorSet for vectors, and make an efficient implementation of methods such as stringSet completely unfeasible (as it would need to work for any IntLattice[I]andCharLattice[C]).
In contrast, if these methods were specialised for all types of their parameters (since in practice, we typically use a fixed combination of abstract value representations for every analysis), they could have a simpler and more efficient implementation. As an example, an implementation of stringRef where both the string and the index are known to use a constant-propagation abstract domain would be trivial to implement.
One way to achieve this, would be to use multi-parameter typeclasses, so that for instance StringLattice[S] would become StringLattice[S, I, C]. Thanks to Scala's flexible type system and composable traits, it should be possible to avoid any code duplication between different StringLattice[S,I,C] instances, so that only methods that require it (such as stringRef) must be specialised. Optionally, a generic "fallback" instance of StringLattice[S,I,C] that works for any IntLattice[I] and any CharLattice[C] could still be provided, preserving all the benefits of the current generic approach in case no specialisation for those types is available yet.
Currently, core lattices use single-parameter typeclasses to describe operations that need to be supported. For example, an implementation of the
StringLattice[S]typeclass needs to define several string operations (e.g.,stringRef,substring,append) for abstractions of strings represented by some typeS.The challenge is that some operations require a combination of several types. For instance, method
stringRefofStringLattice[S]takes not only a string (of typeS), but also an index as parameter. Currently, an implementation of methodstringRefneeds to work with any typeIthat is used to represent integers, given that a correspondingIntLattice[I]instance is provided.The problem is that, by not being able to know the exact representation of
I, the implementation becomes unnecessarily complex and inefficient. For instance, in the constant-propagation domain instance ofStringLattice[S], methodstringRefuses the following implementation:In case the given string (of known type
S) itself is a known constant, it iterates over every possible index of that string to determine if it could possibly be abstracted by the given index (of unknown typeI). Similar issues plague methods such asvectorRefandvectorSetfor vectors, and make an efficient implementation of methods such asstringSetcompletely unfeasible (as it would need to work for anyIntLattice[I]andCharLattice[C]).In contrast, if these methods were specialised for all types of their parameters (since in practice, we typically use a fixed combination of abstract value representations for every analysis), they could have a simpler and more efficient implementation. As an example, an implementation of
stringRefwhere both the string and the index are known to use a constant-propagation abstract domain would be trivial to implement.One way to achieve this, would be to use multi-parameter typeclasses, so that for instance
StringLattice[S]would becomeStringLattice[S, I, C]. Thanks to Scala's flexible type system and composable traits, it should be possible to avoid any code duplication between differentStringLattice[S,I,C]instances, so that only methods that require it (such asstringRef) must be specialised. Optionally, a generic "fallback" instance ofStringLattice[S,I,C]that works for anyIntLattice[I]and anyCharLattice[C]could still be provided, preserving all the benefits of the current generic approach in case no specialisation for those types is available yet.