Adding test files for old permission semantics (#838)

src/test/resources/oldpermsemantics/call_semantics.vpr

@@ -0,0 +1,46 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+field g: Int
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+function foo(x: Ref): Int
+  requires acc(x.f)
+
+function foow(x: Ref): Int
+  requires acc(x.f, wildcard)
+
+function foop(x: Ref): Int
+  requires P(x)
+
+method caller_foo(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && acc(y.f, 1/2)
+    var f1 : Int
+    f1 := foo(x)
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    f1 := foo(y)
+}
+
+method caller_foop(x: Ref, y: Ref)
+{
+    inhale P(x) && acc(P(y), 1/2)
+    var f1 : Int
+    f1 := foop(x)
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    f1 := foop(y)
+}
+
+method caller_foow(x: Ref, y: Ref)
+{
+    inhale acc(x.f, 1/2)
+    var f1 : Int
+    f1 := foow(x)
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    f1 := foow(y)
+}

src/test/resources/oldpermsemantics/function_semantics.vpr

@@ -0,0 +1,78 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+field g: Int
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+function double(x: Ref): Int
+    requires acc(x.f) && acc(x.f)
+    ensures false
+{ 4 }
+
+function double2(x: Ref, y: Ref): Int
+    requires acc(x.f) && acc(y.f)
+    ensures x != y
+{ 4 }
+
+function takesFull(x: Ref): Int
+    requires acc(x.f)
+{ 4 }
+
+function takesFull2(x: Ref): Int
+    requires acc(x.f)
+{ takesFull(x) }
+
+function takesHalf(x: Ref): Int
+    requires acc(x.f, 1/2)
+//:: ExpectedOutput(application.precondition:insufficient.permission)
+{ takesFull(x)}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function pred(x: Ref): Int
+    requires acc(P(x), 1/2)
+{
+  unfolding P(x) in x.f
+}
+
+function pred2(x: Ref): Int
+    requires acc(P(x), 1/2)
+{
+  unfolding acc(P(x), 1/2) in x.f
+}
+
+function pred3(x: Ref): Int
+    requires acc(P(x), 1/2)
+{
+  unfolding acc(P(x), wildcard) in x.f
+}
+
+function pred4(x: Ref): Int
+    requires acc(P(x), wildcard)
+{
+  unfolding acc(P(x), wildcard) in (unfolding acc(P(x), wildcard) in x.f)
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function pred5(x: Ref): Int
+    requires acc(P(x), none)
+{
+  unfolding acc(P(x), wildcard) in x.f
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function pred6(x: Ref): Int
+    requires acc(P(x), 1/2)
+{
+  unfolding acc(P(x), 1/2) in (unfolding acc(P(x), 1/2) in x.f)
+}
+
+function pred7(x: Ref): Int
+    requires acc(P(x), write)
+{
+  unfolding acc(P(x), 1/2) in (unfolding acc(P(x), 1/2) in x.f)
+}

src/test/resources/oldpermsemantics/issues/carbon_196.vpr

@@ -0,0 +1,116 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+predicate P(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(Q(e), wildcard)}
+predicate P2(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(Q(e), 1/2)}
+predicate R(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(e.q, wildcard)}
+predicate R2(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(e.q, 1/2)}
+predicate Q(r: Ref)
+
+field q: Ref
+
+function refs(r: Ref) : Set[Ref]
+
+function get(r: Ref): Ref
+    ensures result in refs(r)
+
+function tester(r: Ref): Ref
+    requires acc(Q(r), wildcard)
+
+function testerFull(r: Ref): Ref
+    requires acc(Q(r), write)
+
+function testerfield(r: Ref): Ref
+    requires acc(r.q, wildcard)
+
+function testerfieldFull(r: Ref): Ref
+    requires acc(r.q, write)
+
+method pred1(r: Ref)
+    requires acc(P(r), wildcard)
+{
+    unfold acc(P(r), wildcard)
+    fold acc(P(r), wildcard)
+    unfold acc(P(r), wildcard)
+    var r2 : Ref := tester(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerFull(get(r))
+}
+
+method pred2(r: Ref)
+    requires acc(P(r), write)
+{
+    unfold acc(P(r))
+    fold acc(P(r))
+    unfold acc(P(r))
+    var r2 : Ref := tester(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerFull(get(r))
+}
+
+method pred3(r: Ref)
+    requires acc(P(r), write)
+{
+    unfold acc(P(r), 1/2)
+    fold acc(P(r), 1/2)
+    unfold acc(P(r), 1/2)
+    var r2 : Ref := tester(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerFull(get(r))
+}
+
+method pred4(r: Ref)
+    requires acc(P2(r), write)
+{
+    unfold acc(P2(r), wildcard)
+    fold acc(P2(r), wildcard)
+    unfold acc(P2(r), wildcard)
+    var r2 : Ref := tester(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerFull(get(r))
+}
+
+method func1(r: Ref)
+    requires acc(R(r), wildcard)
+{
+    unfold acc(R(r), wildcard)
+    fold acc(R(r), wildcard)
+    unfold acc(R(r), wildcard)
+    var r2 : Ref := testerfield(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerfieldFull(get(r))
+}
+
+method func2(r: Ref)
+    requires acc(R(r), write)
+{
+    unfold acc(R(r))
+    fold acc(R(r))
+    unfold acc(R(r))
+    var r2 : Ref := testerfield(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerfieldFull(get(r))
+}
+
+method func3(r: Ref)
+    requires acc(R(r), write)
+{
+    unfold acc(R(r), 1/2)
+    fold acc(R(r), 1/2)
+    unfold acc(R(r), 1/2)
+    var r2 : Ref := testerfield(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerfieldFull(get(r))
+}
+
+method func4(r: Ref)
+    requires acc(R2(r), write)
+{
+    unfold acc(R2(r), wildcard)
+    fold acc(R2(r), wildcard)
+    unfold acc(R2(r), wildcard)
+    var r2 : Ref := testerfield(get(r))
+    //:: ExpectedOutput(application.precondition:insufficient.permission)
+    var r3 : Ref := testerfieldFull(get(r))
+}

src/test/resources/oldpermsemantics/issues/silicon_240.vpr

@@ -0,0 +1,86 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field next: Ref
+field data: Int
+
+ predicate list(this: Ref) {
+        acc(this.next)
+   && acc(this.data)
+   && (this.next != null ==>
+            acc(list(this.next))
+         && unfolding list(this.next) in this.data <= this.next.data)
+ }
+method test01(this: Ref)
+  requires acc(list(this))
+{
+  unfold acc(list(this), 1/2)
+    /* Unexpectedly fails:
+     *   Unfolding list(this) might fail.
+     *   There might be insufficient permission to access list(this.next)
+     */
+}
+function foo(this: Ref): Bool
+  requires acc(list(this))
+{ true }
+predicate bla(this: Ref) {
+     acc(list(this))
+  && foo(this)
+}
+method test02(this: Ref)
+  requires acc(bla(this), 1/2)
+{
+  unfold acc(bla(this), 1/2)
+}
+method test03(this: Ref)
+  requires acc(list(this), 1/2)
+{
+  fold acc(bla(this), 1/2)
+}
+method test04a(this: Ref)
+  requires acc(bla(this), 1/2)
+{
+  assert unfolding acc(bla(this), 1/2) in true
+}
+method test04b(this: Ref)
+  requires acc(bla(this), 1/2)
+{
+  //:: ExpectedOutput(application.precondition:insufficient.permission)
+  assert unfolding acc(bla(this), 1/2) in foo(this)
+}
+
+predicate blabla(this: Ref) { bla(this) }
+method test05(this: Ref)
+  requires blabla(this)
+{
+  assert unfolding acc(blabla(this), 1/3) in unfolding acc(bla(this), 1/5) in true
+}
+function foo_qp(xs: Set[Ref]): Bool
+  requires forall x: Ref :: x in xs ==> acc(x.data)
+{ true }
+predicate bla_qp(xs: Set[Ref]) {
+     (forall x: Ref :: x in xs ==> acc(x.data))
+  && foo_qp(xs)
+}
+method test02_qp(xs: Set[Ref])
+  requires acc(bla_qp(xs), 1/2)
+{
+  unfold acc(bla_qp(xs), 1/2)
+}
+method test03_qp(xs: Set[Ref])
+  requires forall x: Ref :: x in xs ==> acc(x.data, 1/2)
+{
+  fold acc(bla_qp(xs), 1/2)
+}
+method test04a_qp(xs: Set[Ref])
+  requires acc(bla_qp(xs), 1/2)
+{
+  assert unfolding acc(bla_qp(xs), 1/2) in true
+}
+
+method test04b_qp(xs: Set[Ref])
+  requires acc(bla_qp(xs), 1/2)
+{
+  //:: ExpectedOutput(application.precondition:insufficient.permission)
+  assert unfolding acc(bla_qp(xs), 1/2) in foo_qp(xs)
+}

src/test/resources/oldpermsemantics/termination/func_expr_access.vpr

@@ -0,0 +1,24 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+field g: Int
+
+function test1(x: Ref): Bool
+    decreases
+    requires acc(x.f) && acc(x.g)
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    nonTerminating(x)
+}
+
+function test2(x: Ref): Bool
+    decreases
+    requires acc(x.f) && acc(x.f) && acc(x.g)
+{
+    nonTerminating(x)
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *

src/test/resources/oldpermsemantics/wildcard_consistency.vpr

@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+function foo2w(x: Ref, b: Bool): Int
+  //:: ExpectedOutput(consistency.error)
+  requires acc(x.f, b ? wildcard : none)