Round 2 of AntiAliasing changes #1252

mario-bucev · 2022-03-21T09:39:59Z

(note: without mutation, we couldn't create a cycle with epfl-lara/bolts#44 (without resorting to lazy evaluation) :p)

mario-bucev · 2022-03-21T12:45:47Z

Converting this to a draft due to some inefficiency introduced by #1245.
For instance, given:

import stainless._
import stainless.lang._

object i1251b {

  case class Box(var length: Int)

  def mutate(b: Box): Unit = { b.length = 123; }

  def h2(b1: Box, b2: Box, cond: Boolean): Unit = {
    val x = b1.length
    val c = if (cond) b1 else b2
    val d = c
    mutate(d)
    assert(b1.length == x)
  }
}

we generate:

val x: Int = b1.length
var c: Box = (if (cond) {
  b1
} else {
  b2
})
var d: Box = (if (cond) {
  b1
} else if (!cond) {
  b2
} else {
  c
})
var res: (Unit, Box) = mutate(@DropVCs (if (cond) {
  b1
} else if (!cond && !cond) {
  b2
} else if (!cond && !!cond) {
  if (cond) {
    b1
  } else if (!cond) {
    b2
  } else {
    c
  }
} else if (cond) {
  b1
} else if (!cond && !cond) {
  b2
} else if (!cond && !!cond) {
  c
} else {
  d
}))
(if (cond) {
  b1 = @DropVCs Box(@DropVCs res._2.length).asInstanceOf[Box]
} else {
  ()
})
(if (!cond && (!cond && !cond)) {
  b2 = @DropVCs Box(@DropVCs res._2.length).asInstanceOf[Box]
} else {
  ()
})
(if (!cond && (!(!cond && !cond) && (!cond && !!cond))) {
  c = @DropVCs Box(@DropVCs res._2.length).asInstanceOf[Box]
} else {
  ()
})
(if (!cond && (!(!cond && !cond) && !(!cond && !!cond))) {
  d = @DropVCs Box(@DropVCs res._2.length).asInstanceOf[Box]
} else {
  ()
})
res._1
assert(b1.length == x)
()

due to duplicating every occurrence of c and d with if (cond) b1 else b2.
Even if we were a bit more careful in substituting, we would still end up with expression duplication.
So maybe we should rethink env.rewritings?

samarion

About duplicating expressions, we're already doing this a lot in the imperative phase (e.g. during effect copying after function calls), so it's not necessarily a deal breaker.

You could try introducing some additional simplifications in the ImperativeCleanup phase to deal with these. Maybe using simplifyLets and/or simplifyExpr will give good results.

samarion · 2022-03-22T08:47:05Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -384,12 +390,12 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
            val updates1 =
              targets1 map { target =>
                val applied = updatedTarget(target, ArraySelect(array2, index2).setPos(swap))
-                transform(Assignment(target.receiver, applied).setPos(swap), env)
+                Assignment(target.receiver, applied).setPos(swap)


I think we still need to transform array1, index1, array2 and index2.

Good point, I've totally missed that out! I'll also add tests for these cases.

samarion · 2022-03-22T09:18:49Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

-              val applied = updatedTarget(target, v)
-              transform(Assignment(target.receiver, applied).copiedFrom(up), env)
+              val applied = updatedTarget(target, recV)
+              Assignment(target.receiver, applied).copiedFrom(up)


I think this transformation (and a few others) might be incorrectly dropping stuff from the input array expression. If there was a Block expression in a, then I believe it would be silently dropped in the output here.

I'm not sure what the cleanest approach to fix this is, though. I guess some options are:

adding a method which extracts the non-target part of an expression and join it into the output,

we could always include the expression in the output and hope simplification cleans it up later on by having the result be something like
Block(transform(a, env), Assignement(...))

we could have a pre-transformation which makes sure to bring all blocks/targets into a normal form which is compatible with target assignment. This option would also make sure that mutating calls inside targets are handled correctly.

Option 3 seems to also benefit #1068 (as you pointed out)

samarion · 2022-03-22T09:21:52Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

+          case au@ArrayUpdated(arr, i, arg) =>
+            val Seq(rewrArr, rewrI, rewrArg) = rewriteAndCheckArgs(au, Seq(arr, i, arg))
+            ArrayUpdated(transform(rewrArr, env), transform(rewrI, env), transform(rewrArg, env)).copiedFrom(au)
+
+          case mu@MapUpdated(map, k, v) =>
+            val Seq(rewrMap, rewrK, rewrV) = rewriteAndCheckArgs(mu, Seq(map, k, v))
+            MapUpdated(transform(rewrMap, env), transform(rewrK, env), transform(rewrV, env)).copiedFrom(mu)


I think these are only relevant when the array and map base types are mutable, no?

samarion · 2022-03-22T09:24:40Z

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

+      case _ =>
+        throw MalformedStainlessCode(expr, s"Couldn't compute effect targets of array copy update ${au.asString}")
+    }


This (and the corresponding MapUpdated logic) seems to strict. This will also prevent users from using the snapshot(a).updated(i, v) construct which we were discussing.

That's true, for instance, the SortedArray benchmark needs to be updated to account for that restriction (I'm realizing that we can also return Seq.empty if the effect kind is replacement).
For ModfiyingKind though, I do not think there is a way to express the concerned targets.

mario-bucev · 2022-04-19T15:44:52Z

It remains to comment on parts of the code, I'll notify you once (if ever...) I'm done :)

mario-bucev · 2022-04-20T14:41:30Z

@samarion Ready for re-review! (when & if you have the time and desire to do so, of course :) )

samarion

I've read through most of the change and left a few comments. I quite like the move away from rewritings with explicit target tracking instead.

I didn't check the normalization logic yet, but I'm surprised by some of the benchmarks which were disabled due to it (for example, the MutateInsideN benchmarks). Which problems are the block and let hoisting steps solving?

samarion · 2022-04-25T07:03:45Z

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

-        if (be.receiver == vd.toVariable) getTargets(e, kind, be.path.path)
-        else Seq(be)
+      val targs0 = getTargets(b, kind, path)
+      // TODO: Explain why


Please do :)

Oops, thank you for catching that!

samarion · 2022-04-25T07:09:00Z

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

      getAllTargets(expr) flatMap { (target: Target) =>
-        inEnv(target.toEffect(ModifyingKind), env)
+        inEnv(target.toEffect(ModifyingKind), env).toSet


Nit: you don't need the call to toSet here, right?

I have reverted the getTargets returning a Seq to return a Set (as it was before), but I forgot to review the parts in EffectsAnalyzer that depend on this Seq/Set return type (like for the commented snippet below!)

samarion · 2022-04-25T07:09:19Z

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

@@ -782,7 +821,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
          .filter(p => effects contains p._2)
          .flatMap(_._1)

-      case Assignment(v, value) => rec(value, env) ++ env.get(v)
+      case Assignment(v, value) => rec(value, env) ++ env.get(v).toSeq.flatten


Nit: why toSeq?

samarion · 2022-04-25T07:18:06Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

            val castedValue =
              if (adt.isInstanceOf[ADTType] && adt.asInstanceOf[ADTType].getSort.constructors.size == 1)
                newValue
              else
-                Annotated(AsInstanceOf(newValue, effect.receiver.getType), Seq(DropVCs)).copiedFrom(newValue)
-            Assignment(effect.receiver, castedValue).setPos(pos)
+                wrap(AsInstanceOf(newValue, target.receiver.getType))


Should we have AsInstanceOf(...).copiedFrom(newValue) to propagate positions?

Ah yes, good point!

samarion · 2022-04-25T07:22:29Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

+          }.filter(_._2.nonEmpty)
+        }
+
+        def aliasingValDefs2(updTargets: Set[Target], env: Env): Map[ValDef, Set[Target]] = {


Does overloading not work here? Adding the 2 suffix is more confusing IMO

I had some issues with overloading IRC, but I can try adding a DummyImplicit to resolve the issue

samarion · 2022-04-25T07:28:49Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

+                if (conds.isEmpty) None
+                else {


This case is redundant, calling orJoin on Seq() will return BooleanLiteral(true) and result in a None value for combinedCond.

Fair point!

Actually, orJoin returns BooleanLiteral(false) on an empty sequence (but andJoin does return BooleanLiteral(true))

Oh right, good point.

Hmm, but then shouldn't we consider an empty condition as implying BooleanLiteral(true)? It seems fishy to me that we have special handling of the empty case. Maybe conds should rather be defined as

val conds = tgs.map(_.condition.getOrElse(BooleanLiteral(true))

(and then we can just use orJoin and avoid the special case for empty conditions).

That's a more sensical thing to do indeed

samarion · 2022-04-25T07:39:42Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

+                  // But it also conditionally introduce a new target, namely Ref(123) when !cond1.
+                  // In such case, we introduce `y` as a new target, with condition !cond1.
+                  assert(targs.forall(_.condition.isDefined))
+                  val negatedConds = not(orJoin(targs.map(_.condition.get).toSeq))


Does this really work in practice? IIRC, the not and orJoin simplifications are really trivial so you might not even catch the case where you have cond and !cond as conditions. Maybe you could introduce some dedicated logic since you have a strong expectation of what the conditions will look like.

You are right, it doesn't work at all in practice (it ends up generating quite a lot of extra update statements, though it's not incorrect). I'll add something that at least catches things such as cond and !cond.

samarion · 2022-04-25T07:43:22Z

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

-            val ra = freshenLocals(replaceFromSymbols(env.rewritings, a))
-            val targets = getDirectTargets(ra, ArrayAccessor(i))
+            // Sanity check (the same as for Swap)
+            assert(Some(targets) == getDirectTargetsDealiased(transform(arr, env), ArrayAccessor(recI), env))


Isn't there a risk that target computation will fail on the transformed expression?

getDirectTargetsDealiased returns a None in case of failure (which would fire the assertion...)

Yes, I meant: won't this generate spurious failures? It's not clear to me that we expect getDirectTargetsDealiased to always work on transformed trees.

Ah ok, in that sense! Yes you are right, I can remove these checks

mario-bucev · 2022-04-25T09:15:30Z

Thank you for reviewing! For the normalization, the two main motivations are to sequence effects of function calls (and addresses issue such as #1068) and introduce val bindings for indices and keys.
As for hoisting let within let, I think this is a "by-product" of the normalization and not necessarily sought after (though the comment suggests it is... I'll change that).

samarion · 2022-04-25T09:45:57Z

Regarding block hoisting, could we maybe avoid flattening them? Blocks are somewhat useful in allowing local effects which is what the MutateInsideN benchmarks are testing.

mario-bucev · 2022-04-25T10:14:30Z

Will do!

mario-bucev mentioned this pull request Mar 21, 2022

Update SortedArray benchmark epfl-lara/bolts#44

Merged

mario-bucev force-pushed the antialiasing-round2 branch from 9a84d38 to cda82ca Compare March 21, 2022 09:51

mario-bucev linked an issue Mar 21, 2022 that may be closed by this pull request

Illegal aliasing with arrays update not caught #1218

Closed

mario-bucev force-pushed the antialiasing-round2 branch from cda82ca to 2bcebc1 Compare March 21, 2022 10:28

mario-bucev marked this pull request as draft March 21, 2022 12:37

vkuncak requested a review from samarion March 21, 2022 18:12

samarion reviewed Mar 22, 2022

View reviewed changes

samarion mentioned this pull request Mar 22, 2022

Effects in arguments of functions #1068

Closed

mario-bucev mentioned this pull request Mar 24, 2022

Precise alias of array element incorrectly tracked #1253

Closed

mario-bucev force-pushed the antialiasing-round2 branch from 2bcebc1 to d315f3f Compare April 19, 2022 15:42

Round 2 of AntiAliasing changes

ece5e16

mario-bucev force-pushed the antialiasing-round2 branch from d315f3f to ece5e16 Compare April 20, 2022 13:04

mario-bucev marked this pull request as ready for review April 20, 2022 14:40

samarion reviewed Apr 25, 2022

View reviewed changes

mario-bucev added 2 commits April 27, 2022 10:08

Applying suggestions

9ac63b0

Avoid special-casing empty condition

ac346b5

vkuncak merged commit a041c97 into epfl-lara:main Apr 28, 2022

mario-bucev mentioned this pull request May 2, 2022

Manual tuple destructuring in some lemmas for QOI epfl-lara/bolts#45

Merged

mario-bucev deleted the antialiasing-round2 branch June 8, 2022 14:25

Round 2 of AntiAliasing changes #1252

Round 2 of AntiAliasing changes #1252

Conversation

mario-bucev commented Mar 21, 2022 • edited Loading

mario-bucev commented Mar 21, 2022

samarion left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mario-bucev Mar 22, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mario-bucev commented Apr 19, 2022

mario-bucev commented Apr 20, 2022

samarion left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mario-bucev Apr 27, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mario-bucev commented Apr 25, 2022

samarion commented Apr 25, 2022

mario-bucev commented Apr 25, 2022

mario-bucev commented Mar 21, 2022 •

edited

Loading

samarion left a comment •

edited

Loading

mario-bucev Mar 22, 2022 •

edited

Loading

mario-bucev Apr 27, 2022 •

edited

Loading