diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala index f470dfc67f..a93df2aff7 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala @@ -256,39 +256,187 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override } // NOTE: `args` must refer to the arguments of the function invocation before transformation (the original args) - def mapApplication(formalArgs: Seq[ValDef], args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Effect], env: Env): Expr = { + def mapApplication(formalArgs: Seq[ValDef], args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Effect], isOpaqueOrExtern: Boolean, env: Env): Expr = { + + def affectedBindings(updTarget: Target, isReplacement: Boolean): Map[ValDef, Set[Target]] = { + def isAffected(t: Target): Boolean = { + if (isReplacement) t.maybeProperPrefixOf(updTarget) + else t.maybePrefixOf(updTarget) || updTarget.maybePrefixOf(t) + } + env.targets.map { + case (vd, targets) => + val affected = targets.filter(isAffected) + vd -> affected + }.filter(_._2.nonEmpty) + } + if (fiEffects.exists(e => formalArgs contains e.receiver.toVal)) { - val localEffects: Seq[Set[(Effect, Set[(Effect, Option[Expr])])]] = (formalArgs zip args) - .map { case (vd, arg) => (fiEffects.filter(_.receiver == vd.toVariable), arg) } - .filter { case (effects, _) => effects.nonEmpty } - .map { case (effects, arg) => effects map (e => (e, e on arg)) } + val localEffects = formalArgs.zip(args) + .map { case (vd, arg) => + // Effects for each parameter + (vd.toVariable, fiEffects.filter(_.receiver == vd.toVariable), arg) + }.filter { case (_, effects, _) => effects.nonEmpty } val freshRes = ValDef(FreshIdentifier("res"), nfiType).copiedFrom(nfi) - val assgns = (for { - (effects, index) <- localEffects.zipWithIndex - (outerEffect0, innerEffects) <- effects - (effect0, effectCond) <- innerEffects - } yield { - val outerEffect = outerEffect0.removeUnknownAccessor - val effect = effect0.removeUnknownAccessor - val pos = args(index).getPos - val resSelect = TupleSelect(freshRes.toVariable, index + 2) - // Follow all aliases of the updated target (may include self if it has no alias) - val primaryTargs = dealiasTarget(effect.toTarget(effectCond), env) - val assignedPrimaryTargs = primaryTargs.toSeq - .map(t => makeAssignment(pos, resSelect, outerEffect.path.path, t, dropVcs = true)) - val updAliasingValDefs = updatedAliasingValDefs(primaryTargs, env, pos) - - assignedPrimaryTargs ++ updAliasingValDefs - }).flatten - val extractResults = Block(assgns, TupleSelect(freshRes.toVariable, 1)) - - if (isMutableType(nfiType)) { - LetVar(freshRes, nfi, extractResults) - } else { - Let(freshRes, nfi, extractResults) + val assgns = localEffects.zipWithIndex.flatMap { + case ((vd, effects, arg), effIndex) => + // +1 because we are a tuple and +1 because the first component is for the result of the function + val resSelect = TupleSelect(freshRes.toVariable, effIndex + 2) + // All effects on the given parameter, applied to the given argument + val paramWithArgsEffect = for { + outerEffect0 <- effects + (effect0, effectCond) <- outerEffect0 on arg + } yield { + val outerEffect = outerEffect0.removeUnknownAccessor + val effect = effect0.removeUnknownAccessor + val primaryTargs = dealiasTarget(effect.toTarget(effectCond), env) + (outerEffect, primaryTargs) + } + // Suppose we have the following definitions: + // case class Ref(var x: Int, var y: Int) + // case class RefRef(var lhs: Ref, var rhs: Ref) + // + // def modifyLhs(rr: RefRef, v: Int): Unit = { + // rr.lhs.x = v + // rr.lhs.y = v + // } + // def test1(testRR: RefRef): Unit = { + // val rrAlias = testRR + // val lhsAlias = testRR.lhs + // modifyLhs(testRR, 123) + // // ... + // } + // `modifyLhs` is (essentially) transformed as follows by `AntiAliasing` (not here in `mapApplication`): + // def modifyLhs(rr: RefRef, v: Int): (Unit, RefRef) = { + // ((), RefRef(Ref(v, v), rr.rhs) + // } + // The transformed `modifyLhs` returns a copy of the "updated" `rr`. + // + // Our task here in `mapApplication` is to transform the call to `modifyLhs`. + // Intuitively, in this case, we can "update" `testRR` to point to the "updated" version + // returned by `modifyLhs`, and update the aliases accordingly: + // def test1(testRR: RefRef): Unit = { + // val rrAlias = testRR + // val lhsAlias = testRR.lhs + // val res = modifyLhs(testRR, 123) + // testRR = res._2 + // rrAlias = testRR + // lhsAlias = testRR.lhs + // // ... + // } + // We can do so because we know precisely the `Targets` of the argument, namely `testRR` + // and we can update its aliases accordingly. + // This correspond to the `Success` case of having a `ModifyingEffect` on `vd` (here: `rr`) + // applied on `arg` (here: `testRR`). + // + // However, sometimes, we may not always succeed in computing the precise targets, + // as in the following example: + // def test2(testRR: RefRef): Unit = { + // val lhsAlias = testRR.lhs + // val rhsAlias = testRR.rhs + // modifyLhs(RefRef(lhsAlias, rhsAlias), 123) + // } + // Here, we are not able to compute the targets of `RefRef(lhsAlias, rhsAlias)`, + // which corresponds to the `Failure` case. As such, we cannot simply "update" + // the `testRR` variable using the returned result as-is (as we did for `test1`). + // + // Instead, we need to apply each effect of `modifyLhs` *individually* on the argument. + // The effects for `modifyLhs` are (stored in `localEffects`): + // rr -> Set(ReplacementEffect(rr.lhs.x), ReplacementEffect(rr.lhs.y))) + // So we need to apply two `ReplacementEffect`, one on `rr.lhs.x` and one on `rr.lhs.y` on the argument. + // Doing so with `paramWithArgsEffect` gives us: + // ReplacementEffect(rr.lhs.x) -> Set(Target(testRR, None, .lhs.x)) + // ReplacementEffect(rr.lhs.y) -> Set(Target(testRR, None, .lhs.y)) + // which we can then use to update `testRR` (alongside their aliases): + // def test2(testRR: RefRef): Unit = { + // var lhsAlias: Ref = testRR.lhs + // val rhsAlias: Ref = testRR.rhs + // val res: (Unit, RefRef) = modifyLhs(RefRef(lhsAlias, rhsAlias), 123) + // // Note that we "update" each field individually, this is due to + // // having each effect applied separately! + // testRR = RefRef(Ref(res._2.lhs.x, testRR.lhs.y), testRR.rhs) + // lhsAlias = testRR.lhs + // testRR = RefRef(Ref(testRR.lhs.x, res._2.lhs.y), testRR.rhs) + // lhsAlias = testRR.lhs + // // ... + // } + // + // Note that we can always apply this second technique even if we have precise aliases. + // However, this tends to "rebuild" the object instead of reusing the "updated" result + // which can lead to verification inefficiency (and does not work well in presence of + // @opaque or @extern functions). + Try(ModifyingEffect(vd, Path.empty).on(arg)) match { + case Success(modEffect) => + // Update everything that the argument is aliasing + val primaryTargs = modEffect.flatMap { case (eff, cond) => dealiasTarget(eff.toTarget(cond), env) } + val assignedPrimaryTargs = primaryTargs + // The order of assignments does not matter between "primary targets" + // but it must precede the update of aliases (`updAliasingValDefs`) + .toSeq + .map(t => makeAssignment(arg.getPos, resSelect, Seq.empty, t, dropVcs = true)) + // We need to be careful with what we are updating here. + // If we expand on the above example with the following function: + // def t3(refref: RefRef): Unit = { + // val lhs = refref.lhs + // val oldLhs = lhs.x + // replaceLhs(refref, 123) + // assert(lhs.x == oldLhs) + // assert(refref.lhs.x == 123) + // } + // In `replaceLhs`, we have a ReplacementEffect on `rr.lhs`, this means + // that `rr.lhs` is replaced with a new `Ref`, leaving all aliases of `rr.lhs` + // (in `t3`, the `val lhs`) untouched. So, after the call to `replaceLhs`, + // any modification to `rr.lhs` do not alter the other aliases (here, `lhs`). + // The function `t3` should be transformed as follows: + // def t3(refref: RefRef): Unit = { + // val lhs = refref.lhs + // val oldLhs = lhs.x + // val res = replaceLhs(refref, 123) + // refref = res._2 + // assert(lhs.x == oldLhs) + // assert(refref.lhs.x == 123) + // } + // In particular, note that we *do not* touch `lhs`: the following transformation is incorrect: + // var lhs = refref.lhs + // val oldLhs = lhs.x + // val res = replaceLhs(refref, 123) + // refref = res._2 + // lhs = refref.lhs + // because after the call to `replaceLhs`, `lhs` and `refref.lhs` become unrelated. + // Note that, for @opaque and @extern function, we assume the object was mutated in each of its field + // and therefore update all aliases. + val aliasingVds = { + if (isOpaqueOrExtern) { + primaryTargs.flatMap(affectedBindings(_, false)) + } else { + paramWithArgsEffect.flatMap { + case (eff, targs) => + targs.flatMap(affectedBindings(_, eff.kind == ReplacementKind)) + } + } + } + val updAliasingValDefs = aliasingVds + .toSeq // See comment on `assignedPrimaryTargs` + .flatMap { case (vd, targs) => + targs.map(t => makeAssignment(arg.getPos, t.wrap.get, Seq.empty, Target(vd.toVariable, t.condition, Path.empty), true)) + } + assignedPrimaryTargs ++ updAliasingValDefs + case Failure(_) => + paramWithArgsEffect.toSeq.flatMap { case (outerEffect, primaryTargs) => + // Update everything that the argument is aliasing + val assignedPrimaryTargs = primaryTargs + .toSeq + .map(t => makeAssignment(arg.getPos, resSelect, outerEffect.path.path, t, dropVcs = true)) + // Update everything aliasing the argument + val updAliasingValDefs = updatedAliasingValDefs(primaryTargs, env, arg.getPos) + assignedPrimaryTargs ++ updAliasingValDefs + } + } } + + val extractResults = Block(assgns, TupleSelect(freshRes.toVariable, 1)) + Let(freshRes, nfi, extractResults) } else { nfi } @@ -724,8 +872,8 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override val nfi = FunctionInvocation( id, tps, args.map(transform(_, env)) ).copiedFrom(fi) - - mapApplication(fd.params, args, nfi, fi.tfd.instantiate(analysis.getReturnType(fd)), effects(fd), env) + val isExternOrOpaque = symbols.getFunction(id).flags.exists(f => f == Extern || f == Opaque) + mapApplication(fd.params, args, nfi, fi.tfd.instantiate(analysis.getReturnType(fd)), effects(fd), isExternOrOpaque, env) case alr @ ApplyLetRec(id, tparams, tpe, tps, args) => val fd = Inner(env.locals(id)) @@ -752,7 +900,8 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override ).copiedFrom(alr) val resultType = typeOps.instantiateType(analysis.getReturnType(fd), (tparams zip tps).toMap) - mapApplication(fd.params, args, nfi, resultType, effects(fd), env) + val isExternOrOpaque = env.locals(id).flags.exists(f => f == Extern || f == Opaque) + mapApplication(fd.params, args, nfi, resultType, effects(fd), isExternOrOpaque, env) case app @ Application(callee, args) => checkAliasing(app, args, env) @@ -770,7 +919,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override case (vd, i) if ftEffects(i) => ModifyingEffect(vd.toVariable, Path.empty) } val to = makeFunctionTypeExplicit(ft).asInstanceOf[FunctionType].to - mapApplication(params, args, nfi, to, appEffects.toSet, env) + mapApplication(params, args, nfi, to, appEffects.toSet, false, env) } else { Application(transform(callee, env), args.map(transform(_, env))).copiedFrom(app) } diff --git a/frontends/benchmarks/imperative/invalid/ExternMutation.scala b/frontends/benchmarks/imperative/invalid/ExternMutation.scala index c1dc35bc50..bc961c668e 100644 --- a/frontends/benchmarks/imperative/invalid/ExternMutation.scala +++ b/frontends/benchmarks/imperative/invalid/ExternMutation.scala @@ -1,4 +1,6 @@ +import stainless.lang._ import stainless.annotation._ +import StaticChecks._ object ExternMutation { case class Box(var value: BigInt) @@ -8,7 +10,7 @@ object ExternMutation { def f2(b: Container[Box]): Unit = ??? def g2(b: Container[Box]) = { - val b0 = b + @ghost val b0 = snapshot(b) f2(b) assert(b == b0) // fails because `Container` is mutable } diff --git a/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala new file mode 100644 index 0000000000..2e8b840f71 --- /dev/null +++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala @@ -0,0 +1,32 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object OpaqueMutation1 { + + case class Box(var cnt: BigInt, var other: BigInt) { + @opaque // Note the opaque + def secretSauce(x: BigInt): BigInt = cnt + x // Nobody thought of it! + + @opaque // Note the opaque here as well + def increment(): Unit = { + @ghost val oldBox = snapshot(this) + cnt += 1 + ghostExpr { + unfold(secretSauce(other)) + unfold(oldBox.secretSauce(other)) + check(oldBox.secretSauce(other) + 1 == this.secretSauce(other)) + } + }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other)) + } + + def test(b: Box): Unit = { + @ghost val oldBox = snapshot(b) + b.increment() + // Note that, even though the implementation of `increment` does not alter `other`, + // we do not have that knowledge here since the function is marked as opaque. + // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`) + assert(oldBox.secretSauce(oldBox.other) + 1 == b.secretSauce(oldBox.other)) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala b/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala new file mode 100644 index 0000000000..6f0498bc77 --- /dev/null +++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala @@ -0,0 +1,33 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object OpaqueMutation2 { + case class SmallerBox(var otherCnt: BigInt) + + case class Box(var cnt: BigInt, var smallerBox: SmallerBox) { + @opaque // Note the opaque + def secretSauce(x: BigInt): BigInt = cnt + x // Nobody thought of it! + + @opaque // Note the opaque here as well + def increment(): Unit = { + @ghost val oldBox = snapshot(this) + cnt += 1 + ghostExpr { + unfold(secretSauce(smallerBox.otherCnt)) + unfold(oldBox.secretSauce(smallerBox.otherCnt)) + check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt)) + } + }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt)) + } + + def test(b: Box): Unit = { + @ghost val oldBox = snapshot(b) + b.increment() + // Note that, even though the implementation of `increment` does not alter `smallerBox`, + // we do not have that knowledge here since the function is marked as opaque. + // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`) + assert(oldBox.secretSauce(oldBox.smallerBox.otherCnt) + 1 == b.secretSauce(oldBox.smallerBox.otherCnt)) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/imperative/valid/ExternMutation.scala b/frontends/benchmarks/imperative/valid/ExternMutation.scala new file mode 100644 index 0000000000..4ad7281ed1 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/ExternMutation.scala @@ -0,0 +1,15 @@ +import stainless.annotation._ + +object ExternMutation { + case class Box(var value: BigInt) + case class Container[@mutable T](t: T) + + @extern + def f2(b: Container[Box]): Unit = ??? + + def g2(b: Container[Box]) = { + val b0 = b + f2(b) + assert(b == b0) // Ok, even though `b` is assumed to be modified because `b0` is an alias of `b` + } +} diff --git a/frontends/benchmarks/imperative/valid/MutableTuple.scala b/frontends/benchmarks/imperative/valid/MutableTuple.scala index 9a1869ff63..ae9122cf32 100644 --- a/frontends/benchmarks/imperative/valid/MutableTuple.scala +++ b/frontends/benchmarks/imperative/valid/MutableTuple.scala @@ -24,8 +24,8 @@ object MutableTuple { } def t3(): (Foo, Bar) = { - val bar = Bar(1) - val foo = Foo(2) + val bar = Bar(10) + val foo = Foo(20) (foo, bar) } diff --git a/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala new file mode 100644 index 0000000000..577b7c5bf5 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala @@ -0,0 +1,70 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object OpaqueMutation1 { + case class Box(var cnt: BigInt, var other: BigInt) { + @opaque // Note the opaque + def secretSauce(x: BigInt): BigInt = cnt + x // Nobody thought of it! + + @opaque // Note the opaque here as well + def increment(): Unit = { + @ghost val oldBox = snapshot(this) + cnt += 1 + ghostExpr { + unfold(secretSauce(other)) + unfold(oldBox.secretSauce(other)) + check(oldBox.secretSauce(other) + 1 == this.secretSauce(other)) + } + }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other)) + + // What `increment` looks like after `AntiAliasing` + @opaque @pure + def incrementPure(): (Unit, Box) = { + val newThis = Box(cnt + 1, other) + ghostExpr { + unfold(newThis.secretSauce(other)) + unfold(this.secretSauce(other)) + check(this.secretSauce(other) + 1 == newThis.secretSauce(other)) + } + ((), newThis) + }.ensuring { case (_, newThis) => this.secretSauce(newThis.other) + 1 == newThis.secretSauce(newThis.other) } + } + + def test1(b: Box, cond: Boolean): Unit = { + @ghost val oldBox = snapshot(b) + val b2 = if (cond) b else Box(1, 1) + b.increment() + assert(oldBox.secretSauce(b.other) + 1 == b.secretSauce(b.other)) + assert(cond ==> (oldBox.secretSauce(b2.other) + 1 == b2.secretSauce(b.other))) + } + + // What `test1` looks like after `AntiAliasing` + def test1Pure(b: Box, cond: Boolean): Unit = { + val oldBox = b + val b2 = if (cond) b else Box(1, 1) + val (_, newB) = b.incrementPure() + val newB2 = if (cond) newB else b2 + assert(oldBox.secretSauce(newB.other) + 1 == newB.secretSauce(newB.other)) + assert(cond ==> (oldBox.secretSauce(newB2.other) + 1 == newB2.secretSauce(newB.other))) + } + + def test2(b: Box, cond: Boolean): Unit = { + val b2 = if (cond) b else Box(1, 1) + @ghost val oldB2 = snapshot(b2) + b2.increment() + assert(oldB2.secretSauce(b2.other) + 1 == b2.secretSauce(b2.other)) + assert(cond ==> (oldB2.secretSauce(b.other) + 1 == b.secretSauce(b.other))) + } + + // What `test2` looks like after `AntiAliasing` + def test2Pure(b: Box, cond: Boolean): Unit = { + val b2 = if (cond) b else Box(1, 1) + val oldB2 = b2 + val (_, newB2) = b2.incrementPure() + val newB = if (cond) newB2 else b + assert(oldB2.secretSauce(newB2.other) + 1 == newB2.secretSauce(newB2.other)) + assert(cond ==> (oldB2.secretSauce(newB.other) + 1 == newB.secretSauce(newB.other))) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala b/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala new file mode 100644 index 0000000000..0e9e914f85 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala @@ -0,0 +1,44 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object OpaqueMutation2 { + case class SmallerBox(var otherCnt: BigInt) + + case class Box(var cnt: BigInt, var smallerBox: SmallerBox) { + @opaque // Note the opaque + def secretSauce(x: BigInt): BigInt = cnt + x // Nobody thought of it! + + @opaque // Note the opaque here as well + def increment(): Unit = { + @ghost val oldBox = snapshot(this) + cnt += 1 + ghostExpr { + unfold(secretSauce(smallerBox.otherCnt)) + unfold(oldBox.secretSauce(smallerBox.otherCnt)) + check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt)) + } + }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt)) + } + + def test1(b: Box, cond: Boolean): Unit = { + @ghost val oldBox = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123)) + val smallerBoxAlias = b.smallerBox + b.increment() + assert(b.smallerBox.otherCnt == smallerBoxAlias.otherCnt) + assert(oldBox.secretSauce(b.smallerBox.otherCnt) + 1 == b.secretSauce(b.smallerBox.otherCnt)) + assert(oldBox.secretSauce(smallerBoxAlias.otherCnt) + 1 == b.secretSauce(smallerBoxAlias.otherCnt)) + assert(cond ==> (oldBox.secretSauce(b2.smallerBox.otherCnt) + 1 == b2.secretSauce(b.smallerBox.otherCnt))) + assert(cond ==> (oldBox.secretSauce(smallerBoxAlias.otherCnt) + 1 == b2.secretSauce(smallerBoxAlias.otherCnt))) + } + + def test2(b: Box, cond: Boolean): Unit = { + val b2 = if (cond) b else Box(1, SmallerBox(123)) + @ghost val oldB2 = snapshot(b2) + b2.increment() + assert(oldB2.secretSauce(b2.smallerBox.otherCnt) + 1 == b2.secretSauce(b2.smallerBox.otherCnt)) + assert(cond ==> (oldB2.secretSauce(b.smallerBox.otherCnt) + 1 == b.secretSauce(b.smallerBox.otherCnt))) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/imperative/valid/PassByRef.scala b/frontends/benchmarks/imperative/valid/PassByRef.scala new file mode 100644 index 0000000000..a2a9ce71e5 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/PassByRef.scala @@ -0,0 +1,12 @@ +object PassByRef { + case class Box(var value: BigInt) + case class Container(b: Box) + + def f2(b: Container): Unit = b.b.value = 3 + + def g2(b: Container) = { + val b0 = b + f2(b) + assert(b == b0) // Yes, because `b` and `b0` are aliases + } +} diff --git a/frontends/benchmarks/imperative/valid/TargetMutation10.scala b/frontends/benchmarks/imperative/valid/TargetMutation10.scala new file mode 100644 index 0000000000..aaaa5a3667 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/TargetMutation10.scala @@ -0,0 +1,193 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object TargetMutation10 { + case class EvenSmallerBox(var lastCnt: BigInt) + + case class SmallerBox(var otherCnt: BigInt, var evenSmallerBox: EvenSmallerBox) { + def increment(): Unit = { + otherCnt += 1 + evenSmallerBox.lastCnt += 1 + } + } + + case class Box(var cnt: BigInt, var smallerBox: SmallerBox) { + def increment(): Unit = { + cnt += 1 + smallerBox.otherCnt += 1 + smallerBox.evenSmallerBox.lastCnt += 1 + } + def replaceSmallerBox(): Unit = { + cnt += 1 + smallerBox = SmallerBox(-1, EvenSmallerBox(-2)) + } + } + + def test1(b: Box, cond: Boolean): Unit = { + @ghost val oldBox = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + val smallerBoxAlias = b.smallerBox + val smallerBoxAlias2 = if (cond) b.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + b.increment() + assert(cond ==> (b2.cnt == b.cnt)) + assert(!cond ==> (b2.cnt == 1)) + assert(oldBox.cnt + 1 == b.cnt) + assert(b.smallerBox.otherCnt == smallerBoxAlias.otherCnt) + assert(b.smallerBox.evenSmallerBox.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(evenSmallerBoxAliasBis.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(cond ==> (b2.smallerBox.otherCnt == smallerBoxAlias.otherCnt)) + assert(cond ==> (evenSmallerBoxAlias2.lastCnt == b.smallerBox.evenSmallerBox.lastCnt)) + assert(evenSmallerBoxAlias2.lastCnt == evenSmallerBoxAlias2Bis.lastCnt) + assert(!cond ==> (b2.smallerBox.otherCnt == 123)) + assert(!cond ==> (evenSmallerBoxAlias2.lastCnt == 456)) + assert(cond ==> (smallerBoxAlias2.otherCnt == b.smallerBox.otherCnt)) + assert(!cond ==> (smallerBoxAlias2.otherCnt == 456)) + } + + def test2(b: Box, cond: Boolean): Unit = { + @ghost val oldb = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + @ghost val oldb2 = snapshot(b2) + val smallerBoxAlias = b.smallerBox + val smallerBoxAlias2 = if (cond) b.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + b2.increment() + assert(cond ==> (b2.cnt == b.cnt)) + assert(!cond ==> (b2.cnt == 2)) + assert(!cond ==> (oldb.cnt == b.cnt)) + assert(b.smallerBox.otherCnt == smallerBoxAlias.otherCnt) + assert(b.smallerBox.evenSmallerBox.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(evenSmallerBoxAliasBis.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(cond ==> (b2.smallerBox.otherCnt == smallerBoxAlias.otherCnt)) + assert(cond ==> (evenSmallerBoxAlias2.lastCnt == b.smallerBox.evenSmallerBox.lastCnt)) + assert(evenSmallerBoxAlias2.lastCnt == evenSmallerBoxAlias2Bis.lastCnt) + assert(!cond ==> (b.smallerBox.otherCnt == oldb.smallerBox.otherCnt)) + assert(cond ==> (smallerBoxAlias2.otherCnt == b.smallerBox.otherCnt)) + } + + def test3(b: Box, cond: Boolean): Unit = { + @ghost val oldBox = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + val smallerBoxAlias = b.smallerBox + val smallerBoxAlias2 = if (cond) b.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + b.smallerBox.increment() + assert(b.smallerBox.otherCnt == smallerBoxAlias.otherCnt) + assert(b.smallerBox.evenSmallerBox.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(evenSmallerBoxAliasBis.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(cond ==> (b2.smallerBox.otherCnt == smallerBoxAlias.otherCnt)) + assert(cond ==> (evenSmallerBoxAlias2.lastCnt == b.smallerBox.evenSmallerBox.lastCnt)) + assert(evenSmallerBoxAlias2.lastCnt == evenSmallerBoxAlias2Bis.lastCnt) + assert(!cond ==> (b2.smallerBox.otherCnt == 123)) + assert(!cond ==> (evenSmallerBoxAlias2.lastCnt == 456)) + assert(cond ==> (smallerBoxAlias2.otherCnt == b.smallerBox.otherCnt)) + assert(!cond ==> (smallerBoxAlias2.otherCnt == 456)) + } + + def test4(b: Box, cond: Boolean): Unit = { + @ghost val oldb = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + @ghost val oldb2 = snapshot(b2) + val smallerBoxAlias = b.smallerBox + val smallerBoxAlias2 = if (cond) b.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + b2.smallerBox.increment() + assert(b.smallerBox.otherCnt == smallerBoxAlias.otherCnt) + assert(b.smallerBox.evenSmallerBox.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(evenSmallerBoxAliasBis.lastCnt == evenSmallerBoxAlias.lastCnt) + assert(cond ==> (b2.smallerBox.otherCnt == smallerBoxAlias.otherCnt)) + assert(cond ==> (evenSmallerBoxAlias2.lastCnt == b.smallerBox.evenSmallerBox.lastCnt)) + assert(evenSmallerBoxAlias2.lastCnt == evenSmallerBoxAlias2Bis.lastCnt) + assert(!cond ==> (b.smallerBox.otherCnt == oldb.smallerBox.otherCnt)) + assert(cond ==> (smallerBoxAlias2.otherCnt == b.smallerBox.otherCnt)) + } + + def test5(b: Box, cond: Boolean): Unit = { + @ghost val oldBox = snapshot(b) + val oldOtherCnt = b.smallerBox.otherCnt + val oldLastCnt = b.smallerBox.evenSmallerBox.lastCnt + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + val smallerBoxAlias = b.smallerBox + val smallerBoxAlias2 = if (cond) b.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + + b.replaceSmallerBox() + + assert(cond ==> (b2.cnt == b.cnt)) + assert(!cond ==> (b2.cnt == 1)) + assert(oldBox.cnt + 1 == b.cnt) + + assert(b.smallerBox.otherCnt == -1) + assert(b.smallerBox.evenSmallerBox.lastCnt == -2) + + assert(oldBox.smallerBox.otherCnt == oldOtherCnt) + assert(oldBox.smallerBox.evenSmallerBox.lastCnt == oldLastCnt) + + assert(smallerBoxAlias.otherCnt == oldOtherCnt) + assert(evenSmallerBoxAlias.lastCnt == oldLastCnt) + + assert(cond ==> (smallerBoxAlias.otherCnt == oldOtherCnt)) + assert(cond ==> (evenSmallerBoxAlias.lastCnt == oldLastCnt)) + assert(cond ==> (b2.smallerBox.otherCnt == -1)) + assert(cond ==> (b2.smallerBox.evenSmallerBox.lastCnt == -2)) + + assert(!cond ==> (b2.smallerBox.otherCnt == 123)) + assert(!cond ==> (evenSmallerBoxAlias2.lastCnt == 456)) + assert(!cond ==> (smallerBoxAlias2.otherCnt == 456)) + } + + def test6(b: Box, cond: Boolean): Unit = { + @ghost val oldb = snapshot(b) + val b2 = if (cond) b else Box(1, SmallerBox(123, EvenSmallerBox(10))) + val oldOtherCnt = b2.smallerBox.otherCnt + val oldLastCnt = b2.smallerBox.evenSmallerBox.lastCnt + @ghost val oldb2 = snapshot(b2) + val smallerBoxAlias = b2.smallerBox + val smallerBoxAlias2 = if (cond) b2.smallerBox else SmallerBox(456, EvenSmallerBox(20)) + val evenSmallerBoxAlias = b2.smallerBox.evenSmallerBox + val evenSmallerBoxAliasBis = smallerBoxAlias.evenSmallerBox + val evenSmallerBoxAlias2 = if (cond) b2.smallerBox.evenSmallerBox else EvenSmallerBox(456) + val evenSmallerBoxAlias2Bis = if (cond) smallerBoxAlias.evenSmallerBox else EvenSmallerBox(456) + + b2.replaceSmallerBox() + + assert(cond ==> (b2.cnt == b.cnt)) + assert(oldb2.cnt + 1 == b2.cnt) + + assert(b2.smallerBox.otherCnt == -1) + assert(b2.smallerBox.evenSmallerBox.lastCnt == -2) + assert(cond ==> (b.smallerBox.otherCnt == -1)) + assert(cond ==> (b.smallerBox.evenSmallerBox.lastCnt == -2)) + + assert(oldb2.smallerBox.otherCnt == oldOtherCnt) + assert(oldb2.smallerBox.evenSmallerBox.lastCnt == oldLastCnt) + + assert(smallerBoxAlias.otherCnt == oldOtherCnt) + assert(evenSmallerBoxAlias.lastCnt == oldLastCnt) + + assert(cond ==> (smallerBoxAlias.otherCnt == oldOtherCnt)) + assert(cond ==> (evenSmallerBoxAlias.lastCnt == oldLastCnt)) + + assert(!cond ==> (evenSmallerBoxAlias2.lastCnt == 456)) + assert(!cond ==> (smallerBoxAlias2.otherCnt == 456)) + } + +} \ No newline at end of file diff --git a/frontends/benchmarks/imperative/valid/TargetMutation4.scala b/frontends/benchmarks/imperative/valid/TargetMutation4.scala index d426878a02..fc7c27f201 100644 --- a/frontends/benchmarks/imperative/valid/TargetMutation4.scala +++ b/frontends/benchmarks/imperative/valid/TargetMutation4.scala @@ -77,4 +77,23 @@ object TargetMutation4 { assert(y.value == 111) assert(z.value == 111) } + + def h4(x: Box, z: Box, cond: Boolean): Unit = { + val oldX = x.value + val y = if (cond) x else z + y.value = 456 + assert(y.value == 456) + assert(cond ==> (x.value == 456)) + assert(!cond ==> (x.value == oldX)) + } + + def h4Mutate(x: Box, z: Box, cond: Boolean): Unit = { + val oldX = x.value + val y = if (cond) x else z + mutate(y, 456) + assert(y.value == 456) + assert(cond ==> (x.value == 456)) + assert(!cond ==> (x.value == oldX)) + } + } diff --git a/frontends/benchmarks/imperative/valid/TargetMutation6.scala b/frontends/benchmarks/imperative/valid/TargetMutation6.scala index c353316874..5b3353bd23 100644 --- a/frontends/benchmarks/imperative/valid/TargetMutation6.scala +++ b/frontends/benchmarks/imperative/valid/TargetMutation6.scala @@ -9,6 +9,10 @@ object TargetMutation6 { rr.lhs = Ref(v) } + def modifyLhs(rr: RefRef, v: Int): Unit = { + rr.lhs.x = v + } + def t1(arr1: Array[Ref], arr2: Array[Ref], i: Int, j: Int, k: Int, cond: Boolean, gra: Ref): Unit = { require(arr1.length >= 10) require(arr2.length >= arr1.length) @@ -27,6 +31,7 @@ object TargetMutation6 { val oldLhs = lhs.x refref.lhs = Ref(123) assert(lhs.x == oldLhs) + assert(refref.lhs.x == 123) } def t3(refref: RefRef): Unit = { @@ -34,5 +39,17 @@ object TargetMutation6 { val oldLhs = lhs.x replaceLhs(refref, 123) assert(lhs.x == oldLhs) + assert(refref.lhs.x == 123) + } + + def t4(refref: RefRef): Unit = { + val lhs = refref.lhs + val oldLhs = lhs.x + modifyLhs(refref, 123) + assert(lhs.x == 123) + assert(refref.lhs.x == 123) + refref.lhs.x = 456 + assert(lhs.x == 456) + assert(refref.lhs.x == 456) } } diff --git a/frontends/benchmarks/verification/false-valid/i1506.scala b/frontends/benchmarks/verification/false-valid/i1506.scala new file mode 100644 index 0000000000..41b9336f36 --- /dev/null +++ b/frontends/benchmarks/verification/false-valid/i1506.scala @@ -0,0 +1,21 @@ +// Unsoundness due to an incorrect AntiAliasing transformation +// See https://github.com/epfl-lara/stainless/issues/1506 +object i1506 { + case class Ref(var x: Int) + case class RefRef(var lhs: Ref, var rhs: Ref) + + def replaceLhs(rr: RefRef, v: Int): Unit = { + rr.lhs = Ref(v) + } + + def t3(refref: RefRef): Unit = { + val lhs = refref.lhs + val oldLhs = lhs.x + replaceLhs(refref, 123) + assert(lhs.x == oldLhs) + assert(refref.lhs.x == 123) + refref.lhs.x = 456 + assert(lhs.x == 456) // Incorrect because `lhs` and `refref.lhs` become unrelated after the call to `replaceLhs` + assert(refref.lhs.x == 456) + } +}