Fix epfl-lara#1268 epfl-lara#1269 epfl-lara#1270 epfl-lara#1272 epfl-…

…lara#1273 epfl-lara#1274

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

@@ -539,7 +539,12 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
               }
 
               val newBody = transform(b, env.withTargets(vd, targs ++ extraTarget).withBinding(vd))
-              LetVar(vd, newExpr, newBody).copiedFrom(l)
+              // Note: even though there are no effects on `vd`, we still need to re-assign it
+              // in case it aliases a target that gets updated.
+              // As such, we use appearsInAssignment (on the transformed body) instead of checking for effects (on the original body)
+              val canLetVal = !appearsInAssignment(vd.toVariable, newBody)
+              if (canLetVal) Let(vd, newExpr, newBody).copiedFrom(l)
+              else LetVar(vd, newExpr, newBody).copiedFrom(l)
             } else if ((varsOfExprDealiased(e, env) & varsOfExprDealiased(b, env)).forall(v => !isMutableType(v.tpe))) {
               // The above condition is similar to the one in EffectsChecker#check#traverser#traverse#Let, with the
               // difference that we also account for rewrites (which may introduce other variables, as in i1099.scala).
@@ -647,10 +652,14 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
             val vis: Set[Variable] = varsInScope(fd)
               .flatMap(v =>
                 env.targets.get(v.toVal).toSet.flatMap(_.map(_.receiver).toSet) ++ Set(v))
-            // Then, get all variables contained in the arguments, and follow their target aliases.
+            // Then, compute the (dealiased) targets for all arguments.
             // If we find out that a captured variable is also passed as an argument, we declare the program ill-formed
             // because the argument will alias the captured variable.
-            args.flatMap(varsOfExprDealiased(_, env)).find(vis contains _)
+            // For argument whose target cannot be computed, we resort to computing the set of mutable FV
+            // (and follow their aliases), which is less precise.
+            args.flatMap(a => getAllTargetsDealiased(a, env).map(_.map(_.receiver))
+              .getOrElse(varsOfExprDealiased(a, env)))
+              .find(vis contains _)
               .foreach(v => context.reporter.fatalError(alr.getPos, "Illegal passing of aliased local variable: " + v))
 
             val nfi = ApplyLetRec(
@@ -904,6 +913,19 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
       case e => Not(e).copiedFrom(e)
     }
 
+    def appearsInAssignment(vd: Variable, e: Expr): Boolean = {
+      class Traverser(var seen: Boolean = false) extends ConcreteOOSelfTreeTraverser {
+        override def traverse(e: Expr): Unit = e match {
+          case Assignment(`vd`, _) => seen = true
+          case _ => super.traverse(e)
+        }
+      }
+
+      val traverser = new Traverser
+      traverser.traverse(e)
+      traverser.seen
+    }
+
     // Pre-transformation phase to ease the burden of makeSideEffectsExplicit.
     // In particular, we:
     //   -Hoist blocks out of expressions.

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

@@ -94,6 +94,9 @@ class ImperativeCleanup(override val s: Trees, override val t: oo.Trees)
 
         case ReconstructTuple(tuple) => Some(tuple)
 
+        case s.LetRec(fds, body) =>
+          Some(s.LetRec(fds.map(fd => fd.copy(flags = fd.flags filterNot isImperativeFlag)), body))
+
         case _ => None
       } } (expr))
 

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

@@ -211,7 +211,8 @@ class ImperativeCodeElimination(override val s: Trees)(override val t: s.type)
               val (fdRes, fdScope, _) = toFunction(bd)
               fdScope(fdRes)
             }
-            val newFd = inner.copy(fullBody = reconstructSpecs(specs, newBody, inner.returnType))
+            val newSpecs = specs.map(rewriteSpecs)
+            val newFd = inner.copy(fullBody = reconstructSpecs(newSpecs, newBody, inner.returnType))
             val (bodyRes, bodyScope, bodyFun) = toFunction(b)
             (bodyRes, (b2: Expr) => LetRec(Seq(newFd.toLocal), bodyScope(b2)).setPos(fd).copiedFrom(expr), bodyFun)
           }
@@ -414,28 +415,36 @@ class ImperativeCodeElimination(override val s: Trees)(override val t: s.type)
       case _ => false
     }
 
+    // NOTE: We assume that lets wrapping specs require no rewriting
+    def rewriteSpecs(spec: Specification)(using State): Specification = {
+      def toFn(expr: Expr): Expr = {
+        val (res, scope, _) = toFunction(expr)
+        scope(res)
+      }
+      spec match {
+        case Postcondition(ld @ Lambda(params, body)) =>
+          // Remove `Old` trees for function parameters on which no effect occurred
+          val newBody = replaceSingle(
+            fd.params.map(vd => Old(vd.toVariable) -> vd.toVariable).toMap,
+            body
+          )
+          Postcondition(Lambda(params, toFn(newBody)).copiedFrom(ld))
+
+        case spec => spec.transform(toFn)
+      }
+    }
+
     if (exprOps.exists(requireRewriting)(fd.fullBody)) {
+      given State = State(fd, Set(), Map())
       def topLevelRewrite(expr: Expr): Expr = {
-        val (res, scope, _) = toFunction(expr)(using State(fd, Set(), Map()))
+        val (res, scope, _) = toFunction(expr)
         scope(res)
       }
 
       val specced = BodyWithSpecs(fd.fullBody)
 
-      // NOTE: We assume that lets wrapping specs require no rewriting
       val newSpecced = specced.copy(
-        specs = specced.specs.map {
-          case Postcondition(ld @ Lambda(params, body)) =>
-            // Remove `Old` trees for function parameters on which no effect occurred
-            val newBody = replaceSingle(
-              fd.params.map(vd => Old(vd.toVariable) -> vd.toVariable).toMap,
-              body
-            )
-            Postcondition(Lambda(params, topLevelRewrite(newBody)).copiedFrom(ld))
-
-          case spec => spec.transform(topLevelRewrite(_))
-        },
-
+        specs = specced.specs.map(rewriteSpecs),
         body = topLevelRewrite(specced.body)
       )
 

frontends/benchmarks/extraction/invalid/ImpurePure.scala → frontends/benchmarks/extraction/invalid/ImpurePure1.scala

@@ -1,6 +1,6 @@
 import stainless.annotation.pure
 
-object ImpurePure {
+object ImpurePure1 {
   case class Box(var length: Int)
   def makeBox(): Box = Box(0)
 

frontends/benchmarks/extraction/invalid/ImpurePure2.scala

@@ -0,0 +1,12 @@
+import stainless.annotation.pure
+
+object ImpurePure2 {
+  case class Box(var value: Int)
+
+  @pure
+  def outer(b: Box): Unit = { // A lying "pure" function!
+    def inner: Unit = {
+      b.value = 1234
+    }
+  }
+}

frontends/benchmarks/extraction/invalid/InnerfunArgAliasing.scala → frontends/benchmarks/extraction/invalid/InnerfunArgAliasing1.scala

@@ -2,7 +2,7 @@ import stainless._
 import stainless.lang._
 import stainless.annotation._
 
-object InnerfunArgAliasing {
+object InnerfunArgAliasing1 {
 
   case class Box(var value: Int)
 

frontends/benchmarks/extraction/invalid/InnerfunArgAliasing2.scala

@@ -0,0 +1,24 @@
+import stainless._
+import stainless.lang._
+import stainless.annotation._
+
+object InnerfunArgAliasing2 {
+
+  case class Box(var value: Int)
+  case class BBox(var box: Box)
+
+  def outer(x: BBox, y: BBox, cond: Boolean): Unit = {
+    val z = if (cond) y else x
+
+    def inner(innoncentLooking: Box): Unit = {
+      val oldX = x.box.value
+      innoncentLooking.value = 1234
+      assert(innoncentLooking.value == 1234)
+      // This must hold because we assume x.box and innoncentLooking are disjoint
+      assert(x.box.value == oldX)
+    }
+
+    // Illegal aliasing due to z.box aliasing x.box for cond = false
+    inner(z.box)
+  }
+}

frontends/benchmarks/extraction/invalid/InnerfunArgAliasing3.scala

@@ -0,0 +1,26 @@
+import stainless._
+import stainless.lang._
+import stainless.annotation._
+
+object InnerfunArgAliasing3 {
+
+  case class Box(var value: Int)
+
+  def outer(boxes: Array[Box], i: Int, j: Int): Unit = {
+    require(0 <= i && i < boxes.length)
+    require(0 <= j && j < boxes.length)
+
+    val boxi = boxes(i)
+
+    def inner(innoncentLooking: Box): Unit = {
+      val oldI = boxi.value
+      innoncentLooking.value = 1234
+      assert(innoncentLooking.value == 1234)
+      // This must hold because we assume boxi and innoncentLooking are disjoint
+      assert(boxi.value == oldI)
+    }
+
+    // Illegal aliasing due to boxi aliasing boxes(j) for i == j
+    inner(boxes(j))
+  }
+}

frontends/benchmarks/extraction/invalid/InnerfunArgAliasing4.scala

@@ -0,0 +1,27 @@
+import stainless._
+import stainless.lang._
+import stainless.annotation._
+
+object InnerfunArgAliasing4 {
+
+  case class Box(var value: Int)
+
+  def outer(boxes: Array[Box], i: Int, j: Int, z: Int): Unit = {
+    require(0 <= i && i < boxes.length)
+    require(0 <= j && j < boxes.length)
+    require(0 <= z && z < boxes.length)
+
+    val boxi = boxes(i)
+
+    def inner(innoncentLooking: Box): Unit = {
+      val oldI = boxi.value
+      innoncentLooking.value = 1234
+      assert(innoncentLooking.value == 1234)
+      // This must hold because we assume boxi and innoncentLooking are disjoint
+      assert(boxi.value == oldI)
+    }
+
+    // Illegal aliasing due to boxi aliasing boxes(z) for i == z and j != z
+    inner(boxes.updated(j, Box(123))(z))
+  }
+}

frontends/benchmarks/extraction/invalid/i1274a.scala

@@ -0,0 +1,13 @@
+import stainless.annotation._
+
+object i1274a {
+  @extern
+  def f(x: BigInt): Unit = {
+    var t = x
+    t += 1
+    // This require is not properly extracted into a spec (due to having impure constructs before)
+    // It will disappear because bodies of @extern functions are removed
+    // As this is in general not the behavior one expects, we should reject the program.
+    require(t >= 10)
+  }
+}

frontends/benchmarks/extraction/invalid/i1274b.scala

@@ -0,0 +1,16 @@
+import stainless.annotation._
+
+object i1274b {
+  @extern
+  def f(x: BigInt, y: BigInt): Unit = {
+    require(x >= 10)
+    val t = x.toString // Unsupported construct
+    // This extern function contract still misses the following require
+    // but we can't resume the extraction after having encountered an
+    // unsupported feature. We must reject to program because this require
+    // will be erased, akin to SneakySpecsInExtern1.
+    require(x >= y)
+  }
+
+  def callF: Unit = f(10, 10)
+}

frontends/benchmarks/extraction/valid/i1273.scala

@@ -0,0 +1,10 @@
+import stainless._
+import stainless.lang._
+import stainless.annotation._
+
+object PureFnWithInnerFn {
+  @pure
+  def outer: Unit = {
+    def inner: Unit = ()
+  }
+}

frontends/benchmarks/imperative/invalid/i1268.scala

@@ -0,0 +1,14 @@
+object i1268 {
+  case class Box(var value: Int)
+
+  def outer(cond: Boolean): Unit = {
+    val box = Box(123)
+    assert(box.value == 123)
+
+    def inner: Unit = {
+      assert(box.value == 123) // invalid (though we never actually call inner)
+    }
+
+    if (cond) box.value = 456
+  }
+}

frontends/benchmarks/imperative/invalid/i1272.scala

@@ -0,0 +1,9 @@
+import stainless.io._
+
+object i1272 {
+
+  def writing(fos: FileOutputStream): Unit = {
+    // Invalid, we need fos.isOpen
+    fos.write(1)
+  }
+}

frontends/benchmarks/imperative/valid/i1268a.scala

@@ -0,0 +1,12 @@
+object i1268a {
+  case class Box(var value: Int)
+
+  def outer: Unit = {
+    val box = Box(123)
+    assert(box.value == 123)
+
+    def inner: Unit = {
+      assert(box.value == 123)
+    }
+  }
+}

frontends/benchmarks/imperative/valid/i1268b.scala

@@ -0,0 +1,22 @@
+import stainless.lang._
+
+object i1268b {
+  case class Box(var value: BigInt) {
+    def increment: Box = {
+      value += 1
+      this
+    }
+  }
+
+  def outer(b1: Box): Unit = {
+    val oldb1 = b1.value
+    val b2 = freshCopy(b1).increment
+    assert(b1.value == oldb1)
+    assert(b2.value == b1.value + 1)
+
+    def inner: Unit = {
+      assert(b1.value == oldb1)
+      assert(b2.value == b1.value + 1)
+    }
+  }
+}

frontends/benchmarks/imperative/valid/i1269.scala

@@ -0,0 +1,26 @@
+import stainless._
+import stainless.lang._
+import StaticChecks._
+
+object i1269 {
+  case class Box(var value: Int)
+
+  def outer1(b: Box): Unit = {
+    require(b.value == 123)
+
+    def inner1a: Unit = ().ensuring(_ => snapshot(b).value == 123)
+
+    def inner1b(v: Int): Unit = {
+      require(snapshot(b).value == v)
+      assert(v == 123)
+    }
+  }
+
+  def outer2(b: Box): Unit = {
+    require(b.value == 123)
+
+    def inner2: Unit = {
+      b.value = 456
+    }.ensuring(_ => snapshot(b).value == 456)
+  }
+}

frontends/benchmarks/imperative/valid/i1270.scala

@@ -0,0 +1,10 @@
+object i1270 {
+  case class Box(var value: Int)
+
+  def outer(b: Box): Unit = {
+    def inner(v: Int): Unit = {
+      require(b.value == v)
+    }
+    inner(b.value)
+  }
+}

frontends/benchmarks/imperative/valid/i1272.scala

@@ -0,0 +1,15 @@
+import stainless.io._
+
+object i1272 {
+  def read(fis: FileInputStream)(implicit s: State): Unit = {
+    require(fis.isOpen)
+    val a1 = fis.tryReadByte()
+    val a2 = fis.tryReadByte()
+  }
+
+  def write(fos: FileOutputStream): Unit = {
+    require(fos.isOpen)
+    fos.write(1)
+    fos.write(2)
+  }
+}