From aed89cca720896320befefae1d50f6372ce14ab9 Mon Sep 17 00:00:00 2001
From: Mario Bucev <mario.bucev@epfl.ch>
Date: Tue, 30 Jan 2024 15:09:31 +0100
Subject: [PATCH] Add missing dropVCs annotation in AntiAliasing

---
 .../extraction/imperative/AntiAliasing.scala  |  3 +-
 .../valid/ClassReconstruction.scala           | 51 +++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 frontends/benchmarks/imperative/valid/ClassReconstruction.scala

diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
index d0c915851..f470dfc67 100644
--- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -936,11 +936,12 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
           throw MalformedStainlessCode(condition, s"Effects are not allowed in condition of effects: ${condition.asString}")
 
         case Target(receiver, Some(condition), path) =>
+          val recRecv = rec(receiver, path.toSeq)
           Annotated(
             AsInstanceOf(
               IfExpr(
                 condition.setPos(newValue),
-                rec(receiver, path.toSeq),
+                Annotated(recRecv, Seq(DropVCs)).copiedFrom(recRecv),
                 receiver
               ).copiedFrom(newValue),
               receiver.getType
diff --git a/frontends/benchmarks/imperative/valid/ClassReconstruction.scala b/frontends/benchmarks/imperative/valid/ClassReconstruction.scala
new file mode 100644
index 000000000..7937a9ce8
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/ClassReconstruction.scala
@@ -0,0 +1,51 @@
+import stainless.annotation._
+
+object ClassReconstruction {
+
+  case class BoundedCounter(var counter: BigInt, var bound: BigInt) {
+    require(0 <= counter && counter < bound)
+
+    @opaque // Note the opaque
+    def bcTryAdd(i: BigInt): Unit = {
+      if (0 <= i && counter + i < bound) {
+        counter += i
+      }
+    }
+  }
+
+  @mutable
+  trait BoundedCounterContainer {
+    val boundedCounter: BoundedCounter
+
+    final def tryAdd(i: BigInt): Unit = {
+      boundedCounter.bcTryAdd(i)
+    }
+
+    final def tryAdd2(i: BigInt): Unit = {
+      // After AntiAliasing, `tryAdd2` is as follows:
+      //
+      //   var thiss: BoundedCounterContainer = thiss
+      //   ({
+      //     var res: (Unit, BoundedCounterContainer) = tryAdd(thiss, i)
+      //     thiss = @DropVCs (if (res._2.isInstanceOf[BoundedCounterContainerExt]) {
+      //        @DropVCs BoundedCounterContainerExt(
+      //          @DropVCs thiss.asInstanceOf[BoundedCounterContainerExt].__x,
+      //          BoundedCounter(
+      //            @DropVCs res._2.asInstanceOf[BoundedCounterContainerExt].boundedCounter.counter,
+      //            @DropVCs thiss.asInstanceOf[BoundedCounterContainerExt].boundedCounter.bound))
+      //     } else {
+      //       thiss
+      //     }).asInstanceOf[BoundedCounterContainer]
+      //     res._1
+      //   }, thiss)
+      //
+      // Note that we are constructing a new BoundedCounter with `res._2.counter` and this.boundedCounter.bound.
+      // Since `bcTryAdd` is opaque, the solver does not know the relationship between `res._2.counter` and `this.boundedCounter.bound`.
+      // So without further constraints, this will result in an invalid VC.
+      // However we know that calling `tryAdd` (which in turns calls `bcTryAdd`) leads to a valid `BoundedCounter`,
+      // and that this.boundedCounter.bound is equal to res._2.boundedCounter.bound, therefore making this VC valid by construction
+      // We therefore must annotate it with @DropVCs
+      tryAdd(i)
+    }
+  }
+}
\ No newline at end of file