-
Notifications
You must be signed in to change notification settings - Fork 49
Dynamic Dispatch with Closure
Dynamic dispatch is a nice extension to Leon as it increases code readability and enables support for other more complex features.
Since we are working above the Z3 SMT solver, the available data-structures are quite limited. We therefore don't have much of a choice in encoding our objects as ADTs. ADTs have no concept of this, so we must translate dynamic dispatch to a single large match-case statement (per method) that handles the dispatching.
For example, the following program fragment
sealed abstract class List[T] {
def size: Int
}
case class Cons[T](head: T, tail: List[T]) extends List[T] {
def size: Int = 1 + tail.size
}
case class Nil[T]() extends List[T] {
def size: Int = 0
}will be translated to
sealed abstract class List[T]
case class Cons[T](head: T, tail: List[T]) extends List[T]
case class Nil[T]() extends List[T]
def List.size[T](list: List[T]): Int = list match {
case Cons(head, tail) => 1 + List.size(tail)
case Nil() => 0
}Of course this only works when the abstract class is sealed, but Z3 enforces this for ADTs in any case, so we don't lose any flexibility by requiring such a feature.
We want to follow the same basic idea as in the ADT case by building a large match-case statement. This means taking all anonymous functions in the program and merging their bodies into a single function definition body and then matching on some anonymous function identifier.
The following simple program (assuming List type defined as above)
def map(f: Int => Int, list: List[Int]): List[Int] = list match {
case Cons(head, tail) => Cons(f(head), map(f, tail))
case Nil() => Nil()
}
def add1(list: List[Int]): List[Int] = map((i: Int) => i + 1, list)would be translated to
def map(f: Int => Int, list: List[Int]): List[Int] = list match {
case Cons(head, tail) => Cons(apply(f, head), map(f, tail))
case Nil() => Nil()
}
def add1(list: List[Int]): List[Int] = map(af1, list)
def apply(f: Int => Int, a: Int): Int = {
if (f == af1) a + 1
else error("Unknown function identifier " + f) // or something else...
}Such a transformation remains fairly simple insofar as one must provide a different apply definition for each anonymous function type signature encountered in program. This could be alleviated by the introduction of the Any type into Leon (the splitting into multiple apply definitions would still need to be performed, but a different component could handle that part at a later time).
However, when closure gets involved, things become slightly more messy. Indeed, closure requires the definition of a context variable that will be associated to the match-case inputs when performing dispatch. In order for the match-case to type check, all possible contexts must be sub-type of a general Context type.
If we modify the previous fragment slightly to introduce closure
def addX(x: Int, list: List[Int]): List[Int] = map((i: Int) => i + x, list)we see that our apply function must now take a context variable as input
def map(f: Context, list: List[Int): List[Int] = list match {
case Cons(head, tail) => Cons(apply(f, head), map(f, tail))
case Nil() => Nil()
}
def addX(x: Int, list: List[Int]): List[Int] = map(new AF1Context(x), list)
def apply(f: Context, a: Int): Int = f match {
case AF1Context(x) => a + x
case _ => error("Unknown context type " + f.getClass) // or something else...
}Notice that we can encode the identifier of the anonymous function into the Context type that is given to the apply function to keep code simple.
Since the only sub-typing relation available in Z3 is the one found in ADTs, we have to define the Context type as one big ADT:
sealed abstract class Context
case class AF1Context(x: Int) extends Context
...The astute reader will have noticed that the map function defined above was voluntarily restrained by making it non-generic. A more typical implementation would have the following signature:
def map[A,B](f: A => B, list: List[A]): List[B]The solution presented above cannot handle a generic map function since the apply function takes an Int typed parameter (whereas list.head has type A). To handle such generic typed inputs, the apply function must be split up into sub-functions that each handle different function types.
def applyA2B[A,B](f: Context, a: A): B = f match {
case _ => error("Unknown context type in applyA2A " + f.getClass) // or something else...
}
def applyInt2Int(f: Context, a: Int): Int = f match {
case AF1Context(x) => a + x
case _ => error("Unknown context type in applyInt2Int" + f.getClass) // or something else...
}The simplest way of then dispatching between specific apply sub-functions would be to use Any polymorphism with casts, but these features are unfortunately unavailable in Z3. Therefore, we defer the choice until type parameters are completely known by using a special DynamicApply(c: Context, a: Expr) AST. We could use the standard FunctionInvocation AST and check the name, but using a specific AST is clearer and shows that special handling must take place.
The remaining issue to discuss is the handling of generic type parameters in a closure. If we have the following code
def example[A](list: List[A], elem: A): List[A] = {
map((x: A) => someCombinationOf(a, elem), list)
}then the anonymous function (x: A) => someCombinationOf(a, elem) has elem : A in its closure and the associated Context sub-type must therefore be generic as well! Because of Z3/Leon limitations, there must exist a bijection between any parent and child type parameters. This means that if a sub-type of Context has type parameters, then the Context type must have at least as many parameters itself, and all Context children must have at least as many type parameters as the parent Context type does. This is easily achieved by getting the maximum number of type parameters in all Context sub-types and assigning this number of parameters to each Context type.
Certain Context sub-types will have too many type parameters for the associated closure. Such cases can be handled by assigning dummy concrete types to the extra type parameters (like Unit), for example. If we look at the following code fragment
def example1[A](list: List[A]): Int => Int = {
(x: Int) => list.size + x
}
def example2(i: Int): Int => Int = {
(x: Int) => i + x
}we find two different anonymous functions with signatures Int => Int. These will give rise to the following Context types and apply definition:
sealed abstract class Context[T]
case class AF1Context[T](list: List[T]) extends Context[T] // for (x: Int) => list.size + x
case class AF2Context[T](i: Int) extends Context[T] // for (x: Int) => i + x
def applyInt2Int[T](c: Context[T], x: Int): Int = c match {
case AF1Context(list) => list.size + x
case AF2Context(i) => i + x
case _ => error("Unknown context type in applyInt2Int" + c.getClass) // or something else...
}Since the Context type is now generic, all function definitions that take function typed arguments will now be generic as well in the number of type parameters assigned to the Context type times the number of function typed arguments, to maintain type safety.
Once dynamic dispatch with closures is implemented, one could adapt the same techniques to deal with traits. Indeed, anonymous functions can be viewed as objects extending the Function[A,B] trait that guarantees an apply method to all sub-types. This is actually how Scala handles these anonymous functions.
Such an extension would require the modification of the DynamicApply construct to accept different method names. Again, since these are known at Z3 translation time, this doesn't (seem to) pose a problem and can be smoothly handled during translation.
As a slight improvement, it may be possible to use a different Context ADT for each different trait structure. However, mixins may become quite difficult in this case...