Merge branch 'master' into meilers_conditional_join_point_calculation

src/main/scala/extensions/ConditionalPermissionRewriter.scala

@@ -30,18 +30,20 @@ class ConditionalPermissionRewriter {
     case (i@Implies(cond, acc: AccessPredicate), cc) =>
       // Found an implication b ==> acc(...)
       // Transformation causes issues if the permission involve a wildcard, so we avoid that case.
-      val res = if (!acc.perm.contains[WildcardPerm])
+      // Also, we cannot push perm and forperm expressions further in, since their value may be different at different
+      // places in the same assertion.
+      val res = if (!acc.perm.contains[WildcardPerm] && !Expressions.containsPermissionIntrospection(cond))
         (conditionalize(acc, cc.c &*& cond), cc) // Won't recurse into acc's children (see recurseFunc below)
       else
         (Implies(And(cc.c.exp, cond)(), acc)(i.pos, i.info, i.errT), cc)
       alreadySeen.add(res._1)
       res
 
     case (i@Implies(cond, l: Let), cc) if !l.isPure =>
-      if (Expressions.proofObligations(l.exp)(p).isEmpty) {
+      if (Expressions.proofObligations(l.exp)(p).isEmpty && !Expressions.containsPermissionIntrospection(cond)) {
         (l, cc.updateContext(cc.c &*& cond))
       } else {
-        // bound expression might only be well-defined under context conditiond;
+        // bound expression might only be well-defined under context condition;
         // thus, don't push conditions further in.
         val res = (Implies(And(cc.c.exp, cond)(), l)(i.pos, i.info, i.errT), cc)
         alreadySeen.add(res._1)
@@ -50,7 +52,11 @@ class ConditionalPermissionRewriter {
 
     case (impl: Implies, cc) if !impl.right.isPure =>
       // Entering an implication b ==> A, where A is not pure, i.e. contains an accessibility accessibility
-      (impl.right, cc.updateContext(cc.c &*& impl.left))
+      if (Expressions.containsPermissionIntrospection(impl.left)) {
+        (Implies(And(cc.c.exp, impl.left)(), impl.right)(impl.pos, impl.info, impl.errT), cc)
+      } else {
+        (impl.right, cc.updateContext(cc.c &*& impl.left))
+      }
 
     case (acc: AccessPredicate, cc) if cc.c.optExp.nonEmpty =>
       // Found an accessibility predicate nested under some conditionals
@@ -86,7 +92,8 @@ class ConditionalPermissionRewriter {
   // Rewrite impure ternary expressions to a conjuction of implications in order to be able to use the implication
   // rewriter above.
   private val ternaryRewriter = ViperStrategy.Slim{
-    case ce@CondExp(cond, tExp, fExp) if !tExp.isPure || !fExp.isPure =>
+    case ce@CondExp(cond, tExp, fExp)
+        if (!tExp.isPure || !fExp.isPure) && !Expressions.containsPermissionIntrospection(cond) =>
       And(Implies(cond, tExp)(ce.pos, ce.info, ce.errT),
         Implies(Not(cond)(cond.pos, cond.info, cond.errT), fExp)(ce.pos, ce.info, ce.errT))(ce.pos, ce.info, ce.errT)
   }

src/test/resources/conditionalizePermissions/carbon_0179.vpr

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate P1(r$: Ref)
+
+predicate P3(r$: Ref)
+
+method test2()
+{
+    var b: Ref
+    var k: Perm
+
+    inhale acc(P1(b))
+    inhale acc(P3(b))
+
+    exhale perm(P3(b)) >= write ? acc(P3(b)) : (perm(P1(b)) > none ? acc(P1(b), write - perm(P3(b))) : true)
+
+    assert perm(P1(b)) == write
+}

src/test/resources/conditionalizePermissions/let.vpr

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function ok(): Bool
+
+
+function val(): Ref
+    requires ok()
+
+method test()
+{
+    // Test that the condition is not pushed inside the let expression to get e.g.
+    // inhale let x == (val()) in acc(x.f, ok() ? write : none)
+    // which would not be well-defined.
+    inhale ok() ==> let x == (val()) in acc(x.f)
+}

src/test/resources/conditionalizePermissions/silicon_0008.vpr

@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+method deAlias(x: Ref, y: Ref, k: Perm)
+  requires k >= none
+  requires acc(x.f, k) && acc(y.f, k)
+  // The following postcondition should fail in default greedy Silicon because --conditionalizePermissions creates a
+  // situation where the two chunks may or may not alias in the same branch, so they cannot definitively be merged,
+  // so greedy Silicon cannot prove the postcondition using any individual chunk.
+  //:: ExpectedOutput(postcondition.violated:insufficient.permission)
+  ensures x == y ==> acc(x.f, 2 * k)
+{}

src/test/resources/conditionalizePermissions/silicon_0713.vpr

@@ -0,0 +1,27 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field int: Int
+field unrelated: Int
+
+method conv_layer(a: Set[Ref])
+  requires (forall r: Ref :: r in a ==> acc(r.int, write))
+{
+  label beforeFrame
+  while (true)
+    invariant true ==>
+      (forall r: Ref :: r in a ==> acc(r.int, write)) &&
+      [
+        // on inhale
+        (forperm
+          obj: Ref [obj.unrelated] :: obj.unrelated ==
+          old[beforeFrame](obj.unrelated)) &&
+        (forperm
+          obj: Ref [obj.int] :: obj.int == old[beforeFrame](obj.int)),
+
+        // on exhale
+        true
+      ]
+  { inhale false }
+}

src/test/resources/conditionalizePermissions/welldef.vpr

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function ok(): Bool
+
+
+function val(): Ref
+    requires ok()
+
+
+method test()
+{
+    inhale ok() ==> acc(val().f)
+}

src/test/scala/SiliconTestsConditionalizePermissions.scala

@@ -0,0 +1,15 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2022 ETH Zurich.
+
+package viper.silicon.tests
+
+class SiliconTestsConditionalizePermissions extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("conditionalizePermissions")
+
+ override val commandLineArguments: Seq[String] = Seq(
+    "--timeout", "300" /* seconds */,
+    "--conditionalizePermissions")
+}