Refactor alias analysis (WIP) #819
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -85,10 +85,10 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| trait EffectsAnalysis { self: TransformerContext => | ||
| implicit val symbols: s.Symbols | ||
|
|
||
| private[this] def computeFunEffects(fd: FunAbstraction, current: Result): Set[Effect] = | ||
| exprOps.withoutSpecs(fd.fullBody) match { | ||
| case Some(body) => | ||
| computeExprEffects(body, current) | ||
| case None if !fd.flags.contains(IsPure) => | ||
| fd.params | ||
| .filter(vd => symbols.isMutableType(vd.getType) && !vd.flags.contains(IsPure)) | ||
|
|
@@ -121,7 +121,7 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| inners.flatMap { case (_, inners) => inners.map(fun => fun.id -> fun) }) | ||
|
|
||
| val result = inox.utils.fixpoint[Result] { case res @ Result(effects, locals) => | ||
| Result(effects.map { case (fd, _) => fd -> computeFunEffects(fd, res) }, locals) | ||
| } (prevResult merge baseResult) | ||
|
|
||
| for ((fd, inners) <- inners) { | ||
|
|
@@ -137,14 +137,14 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| results merge newResult | ||
| } | ||
|
|
||
| def funEffects(fd: FunDef): Set[Effect] = result.effects(Outer(fd)) | ||
| def funEffects(fun: FunAbstraction): Set[Effect] = result.effects(fun) | ||
| def exprEffects(expr: Expr): Set[Effect] = computeExprEffects(expr, result) | ||
|
|
||
| private[imperative] def local(id: Identifier): FunAbstraction = result.locals(id) | ||
|
|
||
| private[imperative] def getAliasedParams(fd: FunAbstraction): Seq[ValDef] = { | ||
| val receivers = funEffects(fd).map(_.receiver) | ||
| fd.params.filter(vd => receivers(vd.toVariable)) | ||
| } | ||
|
|
||
|
|
@@ -170,7 +170,8 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| def +:(elem: Accessor): Path = Path(elem +: path) | ||
| def ++(that: Path): Path = Path(this.path ++ that.path) | ||
|
|
||
| // Compute all the effect targets of a given expression extended by selections of this path. | ||
| def targetsOn(that: Expr)(implicit symbols: Symbols): Set[Target] = { | ||
| def rec(expr: Expr, path: Seq[Accessor]): Option[Expr] = path match { | ||
| case ADTFieldAccessor(id) +: xs => | ||
| rec(ADTSelector(expr, id), xs) | ||
|
|
@@ -198,7 +199,21 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| Some(expr) | ||
| } | ||
|
|
||
| // Check that this path is valid on the given expression, otherwise return the empty set. | ||
| // Note that if this path is valid on `expr`, we end up simply computing the targets of | ||
| // `expr` with `this` appended, since computeTargets will initially strip away the selectors. | ||
| rec(that, path) match { | ||
| case None => | ||
| // NOTE(gsps): I believe this check is redundant except for the cases where we try to | ||
| // select class fields on expressions whose type is an abstract type def. | ||
| // We have a test case (extraction/valid/TypeMembers2.scala) in which we expand an | ||
| // abstract base class' method to a dispatcher, and such type defs appear. Simply omitting | ||
| // the effect by returning the empty set in such cases actually seems an odd choice to me, | ||
| // though I can't see how to exploit it for unsoundness. | ||
| Set.empty | ||
| case Some(pathOnExpr) => | ||
| computeTargets(pathOnExpr) | ||
| } | ||
| } | ||
|
|
||
| def prefixOf(that: Path): Boolean = { | ||
|
|
@@ -283,9 +298,9 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| case class Effect(receiver: Variable, path: Path) { | ||
| def +(elem: Accessor) = Effect(receiver, path :+ elem) | ||
|
|
||
| // Compute all the effects one gets from replacing this effect's receiver by a given expression. | ||
| def effectsOn(that: Expr)(implicit symbols: Symbols): Set[Effect] = | ||
| path.targetsOn(that).map(_.toEffect) | ||
|
|
||
| def prefixOf(that: Effect): Boolean = | ||
| receiver == that.receiver && (path prefixOf that.path) | ||
|
|
@@ -301,7 +316,23 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| override def toString: String = asString | ||
| } | ||
|
|
||
| // Computes the effect targets of a given expression. | ||
| // The effect targets of an expression represent all the possible variables in scope that might | ||
| // be affected, if one were to mutate the given expression. | ||
| // | ||
| // Individual cases are represented by one Target each. Targets consist of | ||
| // - the variable being modified (the receiver), | ||
| // - the path condition under which this happens, and | ||
| // - the selection path at which this variable is being modified (if any). | ||
| // | ||
| // There is no support for the case where we don't have a name for the target's receiver. | ||
| // (For instance, imagine computing the targets of some temporary ADT value that isn't bound to a | ||
| // variable.) | ||
| // | ||
| // This function provides an under-approximation in some cases; in particular, it might return | ||
| // an empty set for certain "non-local" constructs like function invocations. These seem to be | ||
| // handled specially elsewhere. | ||
|
Comment on lines
+332
to
+334
There was a problem hiding this comment. In Regis' approach to aliasing, function invocations never return an aliased value (it is always fresh). We relaxed this to allow aliasing in non-recursive functions, but left is disabled in recursive ones. I thought we used to check this constraint in the There was a problem hiding this comment. I suppose you're referring to this? The recursive case will fall through to return There was a problem hiding this comment. I think the idea is that an empty set means nothing will be mutated. Since we assume that function invocation results are always fresh (i.e. contain no aliased values), we can safely return an empty set of targets since mutating a function invocation result won't affect any state. I do agree that What I meant about the There was a problem hiding this comment. Thanks, that's a very useful remark. Looking at a concrete case where the empty set case is differentiated from the non-empty case, I'm still a bit puzzled though. That particular piece of code translates On the other hand, if we find the set of effects to be empty (or, implicitly, if an error occurred), we translate the binding as a LetVar and allow it to be mutated later on. That's somewhat surprising to me. What kind of mutation could be applied to that binding that would be detected by (I realize I might be asking a very implementation-specific question here, so don't feel obliged to do any digging, if it's not obvious to you either.) There was a problem hiding this comment.
I think what's really meant by "effect" in this phase is "observable effects on the environment". That is, There was a problem hiding this comment.
For let-bindings with mutable type, we're dealing with the following two cases:
It seems to me that the case where we couldn't compute exact aliasing information and the rhs is not fresh isn't handled here. Maybe that case was ruled out in one of the previous checks? I agree it would make sense to improve the
Ah, I wasn't clear with what I meant by "nothing will be mutated". I meant that given some expression 'E[t]' where 'E[.]' applies some mutation on 't', if (This might be the same thing you're saying :) getting a good mental image of effects is always a bit difficult.) There was a problem hiding this comment. (Sorry for the wall of text. Been appending to this since yesterday night.)
We also have
I've been toying with some different representations for the result of
The way it is actually implemented right now only keeps track of the latter (cumulatively represented as a I'm not completely sure whether it's worth explicitly representing the first two cases. But looking through the various cases where we combine targets, I noted that the behavior of
So, to summarize the current situation: Even without I think the only reason why this doesn't break lots of tests is that we usually go through Speaking of
Now based on these insights, I managed to find some new unsound examples:
import stainless.annotation.pure
case class Box(var length: Int)
object Foo {
def makeBox(): Box = Box(0)
// Passes and omits effect on b
// (Notice that this function is in fact *not* pure!)
@pure def f(b: Box): Unit = {
val c = // => Set.empty!
if (true) b // Set(Target(b, ...))
else makeBox() // Set.empty
c.length = 1 // Just affects c locally, and leaves b unchanged
}
def mutate(b: Box): Unit = { b.length = 123; }
// Crash in ImperativeCodeElimination and "duplicates" effect on both b1 and b2
def g(b1: Box, b2: Box): Unit = {
val c = if (true) b1 else b2
mutate(c)
// The above call leads AntiAliasing to produce nonsensical conditions for mutating b1 and b2:
// > var res: (Unit, Box) = mutate(if (true) b1 else b2)
// > (if (res._2.isInstanceOf[Box]) {
// > b1 = @unchecked Box(@unchecked res._2.asInstanceOf[Box].length).asInstanceOf[Box]
// > } else {
// > ()
// > })
// > (if (res._2.isInstanceOf[Box]) {
// > b2 = @unchecked Box(@unchecked res._2.asInstanceOf[Box].length).asInstanceOf[Box]
// > } else {
// > ()
// > })
}
// Crash in ImperativeCodeElimination and omits effect on b1/b2
def h(b1: Box, b2: Box): Unit = {
val c = if (true) b1 else b2
val d = c // Interacts with Let handling `computeExprEffects`
// We try to assign to val c (and nothing else!)
mutate(d)
}
} |
||
| def computeTargets(expr: Expr)(implicit symbols: Symbols): Set[Target] = { | ||
| def rec(expr: Expr, path: Seq[Accessor]): Set[Target] = expr match { | ||
| case v: Variable => Set(Target(v, None, Path(path))) | ||
| case _ if variablesOf(expr).forall(v => !symbols.isMutableType(v.tpe)) => Set.empty | ||
|
|
@@ -336,6 +367,9 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| And(Not(cnd).setPos(cnd), e.setPos(cnd)).setPos(cnd) | ||
| } getOrElse(Not(cnd).setPos(cnd)) | ||
|
|
||
| // FIXME: This seems wrong: why are we ignoring t.condition? | ||
|
There was a problem hiding this comment. Yes, it should likely be conjoined with |
||
| // FIXME: This also seems inefficient: is it really a good idea to "ground" all the paths | ||
| // rather than representing them as some sort of tree? | ||
| for { | ||
| t <- rec(thn, path) | ||
| e <- rec(els, path) | ||
|
|
@@ -362,8 +396,9 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| rec(b, path) | ||
|
|
||
| case Let(vd, e, b) => | ||
| // FIXME(gsps): This seems exceedingly cryptic. | ||
| val bEffects = rec(b, path) | ||
| val res = for (ee <- computeTargets(e); be <- bEffects) yield { | ||
| if (be.receiver == vd.toVariable) ee.append(be) else be | ||
| } | ||
|
|
||
|
|
@@ -379,13 +414,15 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| rec(expr, Seq.empty) | ||
| } | ||
|
|
||
| // Like computeTargets, but never under-approximates. | ||
| def computeExactTargets(expr: Expr)(implicit symbols: Symbols): Set[Target] = computeTargets(expr) match { | ||
| case targets if targets.nonEmpty => targets | ||
| case _ => throw MalformedStainlessCode(expr, s"Couldn't compute exact effect targets in: $expr") | ||
| } | ||
|
|
||
| // Like computeTargets, but replaces some unsupported cases by the (empty) under-approximation. | ||
| def computeKnownTargets(expr: Expr)(implicit symbols: Symbols): Set[Target] = try { | ||
| computeTargets(expr) | ||
| } catch { | ||
| case _: MalformedStainlessCode => Set.empty | ||
| } | ||
|
|
@@ -410,15 +447,15 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| * | ||
| * We are assuming no aliasing. | ||
| */ | ||
| private def computeExprEffects(expr: Expr, result: Result)(implicit symbols: Symbols): Set[Effect] = { | ||
| import symbols._ | ||
| val freeVars = variablesOf(expr) | ||
|
|
||
| def inEnv(effect: Effect, env: Map[Variable, Effect]): Option[Effect] = | ||
| env.get(effect.receiver).map(e => e.copy(path = e.path ++ effect.path)) | ||
|
|
||
| def effect(expr: Expr, env: Map[Variable, Effect]): Set[Effect] = | ||
| computeTargets(expr) flatMap { (target: Target) => | ||
| inEnv(target.toEffect, env).toSet | ||
| } | ||
|
|
||
|
|
@@ -474,7 +511,7 @@ trait EffectsAnalyzer extends oo.CachingPhase { | |
| val currentEffects: Set[Effect] = result.effects(fun) | ||
| val paramSubst = (fun.params.map(_.toVariable) zip args).toMap | ||
| val invocEffects = currentEffects.flatMap(e => paramSubst.get(e.receiver) match { | ||
| case Some(arg) => e.effectsOn(arg).flatMap(inEnv(_, env)) | ||
| case None => Seq(e) // This effect occurs on some variable captured from scope | ||
| }) | ||
|
|
||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This rather sounds like a bug to me. I'm not sure I understand why we get the
Nonecase here, though. Shouldn'tasClassTyperesolve the type def to a real class?@romac: I think you wrote this code, why are we using an
Optionin rec? Shouldn't we just crash if we find a class selector on a non-class type (after abstract type resolution)?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, it's a bit complicated, I spent a couple of hours grokking all this yesterday. Basically, the abstract method in the test case gets expanded to something like
At the call site of
c_we try to relate some effects ont_(the parameter ofc_) tot(the argument being passed here). This involves taking the effect ont_.xfromc_and "rebasing" it ont. Since we aren't flow-sensitive, the type oftincis still an abstractthiss.T, though, so the sanity check fails here.Note that initially I thought none of this might be a problem and we could just call
computeTargetsanyways, but it turns out that we reject it later (with a MalformedStainlessCode exception, I believe). I forgot where exactly where it fails.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure I understand, at the call site in
testdo we see a call tocorc_? I would expect the Scala compiler to know that we're callingc_here since the receiver type is concrete.If it's a call to
c_, then we shouldn't need any flow analysis to determine thatthiss.Thas a concrete override sincethissshould have typeF. What am I missing?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, I wasn't very clear here, I was just talking about the snippet I had posted. You can completely ignore
test, the issue also occurs without it.It's a call to
c_, but a synthetic one that we introduced when expanding the abstractcto something that model virtual dispatch. So there's no chance forscalacto infer anything.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ahhh, I see.
I wonder if we should be injecting a cast on
tin the synthetic dispatch then. Something liket.asInstanceOf[thiss.asInstanceOf[F].T]? I assume this would allow type parameter resolution.Is the type check even valid without that cast?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wouldn't we just inline the non-recursive calls until we see a
t.asInstanceOf[thiss.asInstanceOf[F].T]receiver?Actually, in which situations are we calling
targetsOn? I would have thought that it wouldn't be invoked at all without thetestmethod in the original benchmark. Which effect are we trying to resolve when it's absent?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We call it only in the situation mentioned in the second comment above (see the part of comment that goes "At the call site of c_ we try to ..."). There's no inlining happening there (this is in
computeExprEffectsrather thancomputeTargets) -- but perhaps you are suggesting to add inlining here?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Are you talking about this line?
If I understand the code correctly, we enter that case when we've found a concrete effect that occurs in the body of the callee (in this case,
c_has an effect ont_.x). We then try to resolve this effect on the provided argument (i.e.thiss).It seems to me that if we find an effect for the function parameter, we should correctly encode all the information we need to resolve it on the provided argument. This might include a path condition and possibly some casts if necessary. I thought we had support for this anyway? Don't we need those to support effects on
this?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, we do (minus the casts): that's essentially
Target. The existing code mostly projects these down toEffects, which drop the path condition, however. As far as I can tell, the current situation is that whenever we deal with a function invocation we take these as an approximation of the function's effects, i.e., we disregard the path conditions.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, I think the rationale is that updating the aliased variable is fine even when the path condition doesn't hold (the update will just be a noop). This is probably necessary to deal with recursion. There is some support for inferring a minimal path condition while updating ADT fields when we might be given a different constructor instance: see mapApplication.
That code is fairly horrible, though... and I'm not sure it will translate well to type defs where the instance-of needs to be applied to a different argument (
thissinstead oft).