Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow for specialisation in core lattices interfaces #17

Open
noahvanes opened this issue Jan 19, 2021 · 0 comments
Open

Allow for specialisation in core lattices interfaces #17

noahvanes opened this issue Jan 19, 2021 · 0 comments
Labels
Abstract domain Enhancement New feature or request

Comments

@noahvanes
Copy link
Collaborator

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] and CharLattice[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.

@noahvanes noahvanes added Enhancement New feature or request Abstract domain labels Jan 19, 2021
@noahvanes noahvanes changed the title Improve core lattices interfaces Allow for specialisation in core lattices interfaces Jan 19, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Abstract domain Enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant