Relax fallback condition of AntiAliasing handling of Let (#1495)

core/src/main/scala/stainless/extraction/innerfuns/Definitions.scala

@@ -101,7 +101,7 @@ trait Definitions extends extraction.Trees { self: Trees =>
     def unapply(i: Outer): Some[FunDef] = Some(i.fd)
   }
 
-  // We do not define Inner as a case class because the inherited `copy` method conflics with the compiler-generated one.
+  // We do not define Inner as a case class because the inherited `copy` method conflicts with the compiler-generated one.
   class Inner(val fd: LocalFunDef) extends FunAbstraction(
     fd.id, fd.tparams, fd.params, fd.returnType, fd.fullBody, fd.flags) {
     setPos(fd)

frontends/benchmarks/extraction/invalid/IllegalAliasing4.check

@@ -0,0 +1,5 @@
+[ Error  ] IllegalAliasing4.scala:15:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   counter: A
+               val b = {
+               ^^^^^^^^^...

frontends/benchmarks/extraction/invalid/IllegalAliasing4.scala

@@ -0,0 +1,26 @@
+object IllegalAliasing4 {
+
+  case class A(var i: BigInt)
+  case class B(a: A)
+  case class C(a: A, b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(alias)
+      }
+      else B(A(0))
+    }
+    b.a.i += 1
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+  }
+}

frontends/benchmarks/extraction/invalid/Initialization1.scalac.check

@@ -1,4 +1,5 @@
 [ Error  ] Initialization1.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(InitA)

frontends/benchmarks/extraction/invalid/Initialization2.scalac.check

@@ -1,4 +1,5 @@
 [ Error  ] Initialization2.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(Hello)

frontends/benchmarks/extraction/invalid/Initialization3.scalac.check

@@ -1,4 +1,5 @@
 [ Error  ] Initialization3.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)

frontends/benchmarks/extraction/invalid/Initialization4.scalac.check

@@ -1,4 +1,5 @@
 [ Error  ] Initialization4.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)

frontends/benchmarks/extraction/invalid/Initialization5.scalac.check

@@ -1,4 +1,5 @@
 [ Error  ] Initialization5.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)

frontends/benchmarks/extraction/invalid/MapAliasing1.check

@@ -1,3 +1,5 @@
-[ Error  ] MapAliasing1.scala:17:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] MapAliasing1.scala:17:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   m: MutableMap[BigInt,A]
                val a = f(m, 123)
                ^^^^^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/MapAliasing2.check

@@ -1,3 +1,5 @@
-[ Error  ] MapAliasing2.scala:15:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] MapAliasing2.scala:15:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   m: MutableMap[BigInt,A]
                val a = f(m, 123)
                ^^^^^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/i1099a.check

@@ -1,3 +1,5 @@
-[ Error  ] i1099a.scala:9:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099a.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a2)
                ^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/i1099b.check

@@ -1,3 +1,5 @@
-[ Error  ] i1099b.scala:9:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099b.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a2)
                ^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/i1099c.check

@@ -1,3 +1,5 @@
-[ Error  ] i1099c.scala:19:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099c.scala:19:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a3)
                ^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/i1099d.check

@@ -0,0 +1,5 @@
+[ Error  ] i1099d.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a0: A, a1: A
+               val c = C(a2)
+               ^^^^^^^^^^^^^

frontends/benchmarks/extraction/invalid/i1099d.scala

@@ -0,0 +1,14 @@
+object i1099d {
+  case class A(var x: Int)
+  case class C(a: A)
+
+  def f(a0: A, a1: A, cond: Boolean) = {
+    require(a0.x == 0 && a1.x == 1)
+    val a2 = if (cond) a0 else a1
+    // Illegal aliasing
+    val c = C(a2)
+    c.a.x += 1
+    val useA0 = a0
+    val useA1 = a1
+  }
+}

frontends/benchmarks/imperative/valid/TargetMutation3.scala

@@ -6,7 +6,7 @@ object TargetMutation3 {
   case class Box(var value: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value = v;
+    b.value = v
   }
 
   def badManners(arr: Array[Box], otherArr: Array[Box], b1: Box, b2: Box, b3: Box, cond1: Boolean, cond2: Boolean, i: Int): Unit = {

frontends/benchmarks/imperative/valid/TargetMutation4.scala

@@ -7,7 +7,7 @@ object TargetMutation4 {
   case class Box(var value: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value = v;
+    b.value = v
   }
 
   def h1(x: Box, cond: Boolean): Unit = {

frontends/benchmarks/imperative/valid/TargetMutation5.scala

@@ -6,12 +6,12 @@ object TargetMutation5 {
   case class Box(var value1: Int, var value2: Int, var value3: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value1 = v;
+    b.value1 = v
   }
 
   def mmutate(b: Box, v1: Int, v2: Int): Unit = {
-    b.value1 = v1;
-    b.value2 = v2;
+    b.value1 = v1
+    b.value2 = v2
   }
 
   def t1(arr: Array[Box], i: Int): Unit = {

frontends/benchmarks/imperative/valid/TargetMutation6.scala

@@ -6,7 +6,7 @@ object TargetMutation6 {
   case class RefRef(var lhs: Ref, var rhs: Ref)
 
   def replaceLhs(rr: RefRef, v: Int): Unit = {
-    rr.lhs = Ref(v);
+    rr.lhs = Ref(v)
   }
 
   def t1(arr1: Array[Ref], arr2: Array[Ref], i: Int, j: Int, k: Int, cond: Boolean, gra: Ref): Unit = {

frontends/benchmarks/imperative/valid/TargetMutation7.scala

@@ -0,0 +1,70 @@
+object TargetMutation7 {
+
+  case class A(var i: BigInt)
+  case class B(var a1: A, var a2: A)
+  case class C(var a: A, var b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test1(n: BigInt, counter: A): C = {
+    val origCount = counter.i
+    val a0 = A(1234)
+    val b = {
+      if (n > 0) {
+        val b = B(A(0), A(1))
+        b.a1 = createA(1, counter)
+        b
+      } else B(A(123), A(456))
+    }
+    val a = createA(2, counter)
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+    C(a, b)
+  }
+
+  def test2(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) B(A(0), createA(n, alias))
+      else B(A(0), A(0))
+    }
+    b.a2.i += 1
+    assert(n <= 0 || counter.i == origCount + 1)
+    assert(n > 0 || counter.i == origCount)
+  }
+
+
+  def test3(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(A(0), alias)
+      }
+      else B(A(0), alias)
+    }
+    b.a2.i += 1
+    assert(n <= 0 || b.a2.i == origCount + 2)
+    assert(n > 0 || b.a2.i == origCount + 1)
+  }
+
+  def test4(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(A(0), counter)
+      }
+      else B(A(0), alias)
+    }
+    b.a2.i += 1
+    assert(n <= 0 || b.a2.i == origCount + 2)
+    assert(n > 0 || b.a2.i == origCount + 1)
+  }
+}

frontends/benchmarks/imperative/valid/TargetMutation8.scala

@@ -0,0 +1,32 @@
+object TargetMutation8 {
+
+  case class A(var i: BigInt)
+  case class B(arr: Array[A])
+  case class C(a: A, b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test(n: BigInt, counter: A): C = {
+    val origCount = counter.i
+    // This triggers AntiAliasing 2nd case for Let binding of mutable types
+    // *without* triggering EffectsChecker#check#traverser#traverse#Let
+    // because:
+    // -`b` is bound to a fresh expression (passes EffectsChecker#check#traverser#traverse#Let check)
+    // -the transformation of `b` produces an expression whose target cannot be computed
+    // -there are no sharing between the terminal variables of `b` and the rest of the body
+    val b = {
+      if (n > 0) {
+        val b = B(Array.fill(5)(A(0)))
+        b.arr(0) = createA(1, counter)
+        b
+      } else B(Array.fill(5)(A(0)))
+    }
+    val a = createA(2, counter)
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+    C(a, b)
+  }
+}

frontends/benchmarks/imperative/valid/TargetMutation9.scala

@@ -0,0 +1,58 @@
+object TargetMutation9 {
+
+  case class A(var x: BigInt)
+  case class C(a: A)
+  case class D(c: C)
+
+  def test1(n: BigInt): Unit = {
+    val a = A(n)
+    val c = C(a)
+    c.a.x = 3
+    assert(c.a.x == 3)
+  }
+
+  def test2(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test3(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val c2 = c
+      c2.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test4(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val d = D(c)
+      d.c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test5(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val d = D(c)
+      d.c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    a.x += 1
+    assert(n != 0 || a.x == 4)
+    assert(n == 0 || a.x == n + 1)
+  }
+}