From d31b01f6946e2b32ed96a4d872fc740beba25300 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 10:03:57 +0200 Subject: [PATCH 1/5] add ghost annotation to unfold argument, to be able to call it outside of ghost enviroment --- .../imperative/valid/OpaqueUnfoldGhost.scala | 26 +++++++++++++++++++ .../library/stainless/lang/package.scala | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) create mode 100644 frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala diff --git a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala new file mode 100644 index 000000000..08a48ec18 --- /dev/null +++ b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala @@ -0,0 +1,26 @@ +import stainless.lang.{ghost => ghostExpr, _} +import stainless.proof._ +import stainless.annotation._ +import StaticChecks._ + +object OpaqueMutation2 { + case class Box(var cnt: BigInt) { + @opaque + @ghost + @pure + def valid: Boolean = cnt > 0 // Invariant that is hidden from the outside + + def operation(): Unit = { + require({ + unfold(valid) + valid + }) + unfold(valid) // Shouldn't be consider to be ghost, even with a ghost argument + assert(cnt > 0) + cnt += 1 + assert(cnt > 0) + }.ensuring(_ => + unfold(valid) + valid) + } +} diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala index f019c7449..dd6ae2268 100644 --- a/frontends/library/stainless/lang/package.scala +++ b/frontends/library/stainless/lang/package.scala @@ -179,7 +179,7 @@ package object lang { // typically used when `call` invokes an `opaque` function // this adds an equality between the call, and the inlined call @library - def unfold[T](call: T): Unit = () + def unfold[T](@ghost call: T): Unit = () @ignore @library implicit class ArrayUpdating[T](a: Array[T]) { From d38dcf0168595471ce4da3b31a9df0e7e20c32e1 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 10:05:12 +0200 Subject: [PATCH 2/5] format --- .../benchmarks/imperative/valid/OpaqueUnfoldGhost.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala index 08a48ec18..b9c5f5938 100644 --- a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala +++ b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala @@ -15,12 +15,12 @@ object OpaqueMutation2 { unfold(valid) valid }) - unfold(valid) // Shouldn't be consider to be ghost, even with a ghost argument + unfold( + valid + ) // Shouldn't be consider to be ghost, even with a ghost argument assert(cnt > 0) cnt += 1 assert(cnt > 0) - }.ensuring(_ => - unfold(valid) - valid) + }.ensuring(_ => unfold(valid) valid) } } From f3441632acb6d6672f5d1d8934ab05c364eceaff Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 10:57:35 +0200 Subject: [PATCH 3/5] rename object in benchmark --- frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala index b9c5f5938..96ec8a88b 100644 --- a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala +++ b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala @@ -3,7 +3,7 @@ import stainless.proof._ import stainless.annotation._ import StaticChecks._ -object OpaqueMutation2 { +object OpaqueUnfoldGhost { case class Box(var cnt: BigInt) { @opaque @ghost From b62248713c54e87ce377433cad6689994526c563 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 13:58:22 +0200 Subject: [PATCH 4/5] reformat to solve issue --- .../benchmarks/imperative/valid/OpaqueUnfoldGhost.scala | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala index 96ec8a88b..9dc9de546 100644 --- a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala +++ b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala @@ -15,12 +15,13 @@ object OpaqueUnfoldGhost { unfold(valid) valid }) - unfold( - valid - ) // Shouldn't be consider to be ghost, even with a ghost argument + unfold(valid) // Shouldn't be consider to be ghost, even with a ghost argument assert(cnt > 0) cnt += 1 assert(cnt > 0) - }.ensuring(_ => unfold(valid) valid) + }.ensuring(_ => { + unfold(valid) + valid + }) } } From 4049e0deac4a844024c3dc06985f71f929cd3be1 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 14 Aug 2024 14:20:45 +0200 Subject: [PATCH 5/5] rename unfold to unfolding --- .../extraction/imperative/AntiAliasing.scala | 4 +-- .../extraction/inlining/UnfoldOpaque.scala | 2 +- .../imperative/invalid/OpaqueMutation1.scala | 6 ++--- .../imperative/invalid/OpaqueMutation2.scala | 6 ++--- .../imperative/valid/OpaqueMutation1.scala | 10 +++---- .../imperative/valid/OpaqueMutation2.scala | 6 ++--- .../imperative/valid/OpaqueUnfoldGhost.scala | 27 ------------------- .../imperative/valid/UnfoldOpaqueMutate.scala | 6 ++--- .../valid/MicroTests/VisibleOpaque.scala | 4 +-- .../verification/valid/UnfoldOpaqueVal.scala | 4 +-- .../library/stainless/lang/package.scala | 2 +- 11 files changed, 25 insertions(+), 52 deletions(-) delete mode 100644 frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala index 2850de3d2..7c084e830 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala @@ -261,7 +261,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override // * `selectResult` selects the first element of the tuple returned by the transformed function // (the others elements are the "updated" version of the mutated parameters). // By default, it should be set to `true`. - // However, in the particular case of `unfold(fn(...))`, we would like *not* to have this selection be performed + // However, in the particular case of `unfolding(fn(...))`, we would like *not* to have this selection be performed // due to the following. `AntiAliasing` will transform this call to: // unfold { // val res = fn(...) @@ -1055,7 +1055,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override object UnfoldOpaque { def unapply(e: Expr): Option[(Identifier, FunctionInvocation)] = e match { - case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(fi: s.FunctionInvocation)) => + case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(fi: s.FunctionInvocation)) => Some((id, fi)) case _ => None } diff --git a/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala b/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala index 249e6ff33..4a8192fc5 100644 --- a/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala +++ b/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala @@ -24,7 +24,7 @@ class UnfoldOpaque(override val s: Trees, override val t: Trees) override def transform(e: Expr, env: Env): t.Expr = { e match { - case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(maybeFi)) => + case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(maybeFi)) => // Lookup the bindings recursively to unveil a call to a function which we would need to unfold val r = dealiasedAndStripped(maybeFi, env) r match { diff --git a/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala index 2e8b840f7..599dae69d 100644 --- a/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala +++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala @@ -14,8 +14,8 @@ object OpaqueMutation1 { @ghost val oldBox = snapshot(this) cnt += 1 ghostExpr { - unfold(secretSauce(other)) - unfold(oldBox.secretSauce(other)) + unfolding(secretSauce(other)) + unfolding(oldBox.secretSauce(other)) check(oldBox.secretSauce(other) + 1 == this.secretSauce(other)) } }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other)) @@ -29,4 +29,4 @@ object OpaqueMutation1 { // 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 index 6f0498bc7..69d8a083c 100644 --- a/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala +++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala @@ -15,8 +15,8 @@ object OpaqueMutation2 { @ghost val oldBox = snapshot(this) cnt += 1 ghostExpr { - unfold(secretSauce(smallerBox.otherCnt)) - unfold(oldBox.secretSauce(smallerBox.otherCnt)) + unfolding(secretSauce(smallerBox.otherCnt)) + unfolding(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)) @@ -30,4 +30,4 @@ object OpaqueMutation2 { // 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/OpaqueMutation1.scala b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala index 577b7c5bf..e30cb23eb 100644 --- a/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala +++ b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala @@ -13,8 +13,8 @@ object OpaqueMutation1 { @ghost val oldBox = snapshot(this) cnt += 1 ghostExpr { - unfold(secretSauce(other)) - unfold(oldBox.secretSauce(other)) + unfolding(secretSauce(other)) + unfolding(oldBox.secretSauce(other)) check(oldBox.secretSauce(other) + 1 == this.secretSauce(other)) } }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other)) @@ -24,8 +24,8 @@ object OpaqueMutation1 { def incrementPure(): (Unit, Box) = { val newThis = Box(cnt + 1, other) ghostExpr { - unfold(newThis.secretSauce(other)) - unfold(this.secretSauce(other)) + unfolding(newThis.secretSauce(other)) + unfolding(this.secretSauce(other)) check(this.secretSauce(other) + 1 == newThis.secretSauce(other)) } ((), newThis) @@ -67,4 +67,4 @@ object OpaqueMutation1 { 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 index 0e9e914f8..5a3037e35 100644 --- a/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala +++ b/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala @@ -15,8 +15,8 @@ object OpaqueMutation2 { @ghost val oldBox = snapshot(this) cnt += 1 ghostExpr { - unfold(secretSauce(smallerBox.otherCnt)) - unfold(oldBox.secretSauce(smallerBox.otherCnt)) + unfolding(secretSauce(smallerBox.otherCnt)) + unfolding(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)) @@ -41,4 +41,4 @@ object OpaqueMutation2 { 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/OpaqueUnfoldGhost.scala b/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala deleted file mode 100644 index 9dc9de546..000000000 --- a/frontends/benchmarks/imperative/valid/OpaqueUnfoldGhost.scala +++ /dev/null @@ -1,27 +0,0 @@ -import stainless.lang.{ghost => ghostExpr, _} -import stainless.proof._ -import stainless.annotation._ -import StaticChecks._ - -object OpaqueUnfoldGhost { - case class Box(var cnt: BigInt) { - @opaque - @ghost - @pure - def valid: Boolean = cnt > 0 // Invariant that is hidden from the outside - - def operation(): Unit = { - require({ - unfold(valid) - valid - }) - unfold(valid) // Shouldn't be consider to be ghost, even with a ghost argument - assert(cnt > 0) - cnt += 1 - assert(cnt > 0) - }.ensuring(_ => { - unfold(valid) - valid - }) - } -} diff --git a/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala b/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala index 47b02ce69..24e50a640 100644 --- a/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala +++ b/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala @@ -19,12 +19,12 @@ object UnfoldOpaqueMutate { def test1(wb: WrappedBox, x: BigInt): Unit = { @ghost val oldWb = snapshot(wb) - unfold(wb.opaqueMutMeth1(x)) + unfolding(wb.opaqueMutMeth1(x)) assert(wb.box.cnt == oldWb.box.cnt + x) } def test2(wb: WrappedBox, x: BigInt): Unit = { - unfold(wb.opaqueMutMeth2(x)) + unfolding(wb.opaqueMutMeth2(x)) assert(wb.box == Box(x * 2)) } -} \ No newline at end of file +} diff --git a/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala b/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala index 0f4e4b669..03c1bf866 100644 --- a/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala +++ b/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala @@ -1,11 +1,11 @@ import stainless.annotation._ -import stainless.lang.unfold +import stainless.lang.unfolding object VisibleOpaque { @opaque def p(x: Int) = x > 0 def test(x: Int): Unit = { - unfold(p(x)) + unfolding(p(x)) assert(p(x) == x > 0) } } diff --git a/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala b/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala index e62ba09bb..00323a7bb 100644 --- a/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala +++ b/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala @@ -7,7 +7,7 @@ object UnfoldOpaqueVal { def test(x: BigInt): Unit = { val y = opaqueFn(x) - unfold(y) + unfolding(y) assert(y == x + 1) } -} \ No newline at end of file +} diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala index dd6ae2268..55fdfa773 100644 --- a/frontends/library/stainless/lang/package.scala +++ b/frontends/library/stainless/lang/package.scala @@ -179,7 +179,7 @@ package object lang { // typically used when `call` invokes an `opaque` function // this adds an equality between the call, and the inlined call @library - def unfold[T](@ghost call: T): Unit = () + def unfolding[T](call: T): Unit = () @ignore @library implicit class ArrayUpdating[T](a: Array[T]) {