Merge pull request #760 from viperproject/meilers_pull_put_assumptions

Pull assumptions out of quantifiers if they don't refer to quantified variable

src/main/scala/decider/PathConditions.scala

@@ -176,13 +176,24 @@ private trait LayeredPathConditionStackLike {
     val ignores = ignore.topLevelConjuncts
 
     for (layer <- layers) {
-      globals ++= layer.globalAssumptions
+      val actualBranchCondition = layer.branchCondition.getOrElse(True)
+      val relevantNonGlobals = layer.nonGlobalAssumptions -- ignores
+      val (trueNonGlobals, additionalGlobals) = if (!actualBranchCondition.existsDefined{ case t if qvars.contains(t) => }) {
+        // The branch condition is independent of all quantified variables
+        // Any assumptions that are also independent of all quantified variables can be treated as global assumptions.
+        val (trueNonGlobals, unconditionalGlobals) = relevantNonGlobals.partition(a => a.existsDefined{ case t if qvars.contains(t) => })
+        (trueNonGlobals, unconditionalGlobals.map(Implies(actualBranchCondition, _)))
+      } else {
+        (relevantNonGlobals, Seq())
+      }
+
+      globals ++= layer.globalAssumptions ++ additionalGlobals
 
       nonGlobals :+=
         Quantification(
           quantifier,
           qvars,
-          Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)),
+          Implies(actualBranchCondition, And(trueNonGlobals)),
           triggers,
           name,
           isGlobal)

src/test/resources/issue387/jonas_viktor.vpr

@@ -0,0 +1,71 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// first version of the example
+
+domain ArrayDomain {}
+
+field val_int: Int
+field val_ref: Ref
+
+function idx_into(a: ArrayDomain, a_len: Int): Int
+function array_len(a: ArrayDomain): Int
+function to_domain(self: Ref): ArrayDomain
+  requires acc(Array(self), read$())
+
+function read$(): Perm
+  ensures none < result
+  ensures result < write
+
+predicate Array(self: Ref)
+predicate usize(self: Ref) {
+  acc(self.val_int, write)
+}
+
+method foo() {
+  var a: Ref
+  var a_len: Int
+  var _3: Ref
+  var unknown: Ref
+  var i: Ref
+  inhale acc(a.val_ref, write) && acc(Array(a.val_ref), write)
+
+  inhale acc(_3.val_ref, write) && acc(usize(unknown), read$()) // <- removing this makes it pass
+
+  exhale acc(a.val_ref, read$())
+
+  inhale acc(usize(i), write) && acc(a.val_ref, read$())
+
+  inhale (unfolding acc(usize(i), write) in
+      (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
+        !(q < i.val_int) ||
+        idx_into(to_domain(a.val_ref), q) <=
+        idx_into(to_domain(a.val_ref), i.val_int)))
+  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/387/)
+  assert (unfolding acc(usize(i), write) in
+      (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
+        !(q < i.val_int) ||
+        idx_into(to_domain(a.val_ref), q) <=
+        idx_into(to_domain(a.val_ref), i.val_int)))
+}
+
+
+// second version of the example
+
+function holds(a: Ref, b: Int): Bool
+
+method foo2() {
+  var a: Ref
+  var _3: Ref
+
+  inhale acc(a.val_ref, write)
+
+  inhale acc(_3.val_ref, write) // <- removing this makes it pass
+
+  exhale acc(a.val_ref, 1 / 2)
+  inhale acc(a.val_ref, 1 / 2)
+
+  inhale forall q: Int :: holds(a.val_ref, q)
+  assert forall q: Int :: holds(a.val_ref, q)
+}

src/test/scala/SiliconTests.scala

@@ -15,7 +15,7 @@ import viper.silver.verifier.Verifier
 
 class SiliconTests extends SilSuite {
   private val siliconTestDirectories =
-    Seq("consistency", "issue387")
+    Seq("consistency")
 
   private val silTestDirectories =
     Seq("all",

src/test/scala/SiliconTestsMoreCompleteExhale.scala

@@ -7,7 +7,7 @@
 package viper.silicon.tests
 
 class SiliconTestsMoreCompleteExhale extends SiliconTests {
-  override val testDirectories: Seq[String] = Seq("moreCompleteExhale")
+  override val testDirectories: Seq[String] = Seq("moreCompleteExhale", "issue387")
 
  override val commandLineArguments: Seq[String] = Seq(
     "--timeout", "300" /* seconds */,