Merge pull request #469 from viperproject/meilers_unfold_none_2

Unfold, fold, and unfolding must have a strictly positive permission amount

Author: marcoeilers

silver

@@ -45,6 +45,16 @@ trait PermModule extends Module with CarbonStateComponent {
 
   def conservativeIsPositivePerm(e: sil.Exp): Boolean
 
+  /**
+    * Returns an expression representing that a permission amount is positive.
+    * Similar to [[permissionPositive]], but works directly on Viper expressions, *including* ones containing
+    * wildcards, and performs more aggressive simplifications.
+    *
+    * @param e the permission amount to be checked
+    * @return the expression representing the fact that the permission is positive
+    */
+  def isStrictlyPositivePerm(e: sil.Exp): Exp
+
   /**
    * The current mask.
    */

src/main/scala/viper/carbon/modules/PermModule.scala

@@ -20,6 +20,7 @@ import viper.silver.verifier.{NullPartialVerificationError, PartialVerificationE
 
 import scala.collection.mutable.ListBuffer
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
+import viper.silver.verifier.reasons.NonPositivePermission
 
 import scala.collection.mutable
 
@@ -927,7 +928,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
                            , statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): (Stmt,Stmt) = {
     duringFold = true
     foldInfo = acc
-    val stmt = exhaleSingleWithoutDefinedness(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error, havocHeap = false,
+    val stmt = Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++
+      exhaleSingleWithoutDefinedness(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error, havocHeap = false,
       statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) ++
       inhale(Seq((acc, error)), addDefinednessChecks = false, statesStackForPackageStmt, insidePackageStmt)
     val stmtLast =  Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ {
@@ -965,7 +967,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     duringUnfold = true
     duringUnfolding = isUnfolding
     unfoldInfo = acc
-    val stmt = Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++
+    val stmt = Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++
+      Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++
       {
         val location = acc.loc
         val predicate = verifier.program.findPredicate(location.predicateName)

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -1601,26 +1601,30 @@ class QuantifiedPermModule(val verifier: Verifier)
 
   override def conservativeIsPositivePerm(e: sil.Exp): Boolean = PermissionHelper.conservativeStaticIsStrictlyPositivePerm(e)
 
+  override def isStrictlyPositivePerm(e: sil.Exp): Exp = PermissionHelper.isStrictlyPositivePerm(e)
+
   object PermissionHelper {
 
     def isStrictlyPositivePerm(e: sil.Exp): Exp = {
       require(e isSubtype sil.Perm, s"found ${e.typ} ($e), but required Perm")
-      val backup = permissionPositiveInternal(translatePerm(e), Some(e))
+      // Use backup lazily when needed only. This allows the function to work on WildcardPerms for which
+      // translatePerm would throw an exception.
+      val backup = () => permissionPositiveInternal(translatePerm(e), Some(e))
       e match {
         case sil.NoPerm() => FalseLit()
         case sil.FullPerm() => TrueLit()
         case sil.WildcardPerm() => TrueLit()
         case sil.EpsilonPerm() =>  sys.error("epsilon permissions are not supported by this permission module")
         case x: sil.LocalVar if isAbstractRead(x) => TrueLit()
-        case sil.CurrentPerm(loc) => backup
+        case sil.CurrentPerm(loc) => backup()
         case sil.FractionalPerm(left, right) =>
           val (l, r) = (translateExp(left), translateExp(right))
           ((l > IntLit(0)) && (r > IntLit(0))) || ((l < IntLit(0)) && (r < IntLit(0)))
         case sil.PermMinus(a) =>
           isStrictlyNegativePerm(a)
         case sil.PermAdd(left, right) =>
-          (isStrictlyPositivePerm(left) && isStrictlyPositivePerm(right)) || backup
-        case sil.PermSub(left, right) => backup
+          (isStrictlyPositivePerm(left) && isStrictlyPositivePerm(right)) || backup()
+        case sil.PermSub(left, right) => backup()
         case sil.PermMul(a, b) =>
           (isStrictlyPositivePerm(a) && isStrictlyPositivePerm(b)) || (isStrictlyNegativePerm(a) && isStrictlyNegativePerm(b))
         case sil.PermDiv(a, b) =>
@@ -1633,7 +1637,7 @@ class QuantifiedPermModule(val verifier: Verifier)
           ((n > IntLit(0)) && isStrictlyPositivePerm(b)) || ((n < IntLit(0)) && isStrictlyNegativePerm(b))
         case sil.CondExp(cond, thn, els) =>
           CondExp(translateExp(cond), isStrictlyPositivePerm(thn), isStrictlyPositivePerm(els))
-        case _ => backup
+        case _ => backup()
       }
     }
 
@@ -1705,22 +1709,24 @@ class QuantifiedPermModule(val verifier: Verifier)
 
     def isStrictlyNegativePerm(e: sil.Exp): Exp = {
       require(e isSubtype sil.Perm)
-      val backup = UnExp(Not,permissionPositiveInternal(translatePerm(e), Some(e), true))
+      // Use backup lazily when needed only. This allows the function to work on WildcardPerms for which
+      // translatePerm would throw an exception.
+      val backup = () => UnExp(Not,permissionPositiveInternal(translatePerm(e), Some(e), true))
       e match {
         case sil.NoPerm() => FalseLit() // strictly negative
         case sil.FullPerm() => FalseLit()
         case sil.WildcardPerm() => FalseLit()
         case sil.EpsilonPerm() =>  sys.error("epsilon permissions are not supported by this permission module")
         case x: sil.LocalVar if isAbstractRead(x) => FalseLit()
-        case sil.CurrentPerm(loc) => backup
+        case sil.CurrentPerm(loc) => backup()
         case sil.FractionalPerm(left, right) =>
           val (l, r) = (translateExp(left), translateExp(right))
           ((l < IntLit(0)) && (r > IntLit(0))) || ((l > IntLit(0)) && (r < IntLit(0)))
         case sil.PermMinus(a) =>
           isStrictlyPositivePerm(a)
         case sil.PermAdd(left, right) =>
-          (isStrictlyNegativePerm(left) && isStrictlyNegativePerm(right)) || backup
-        case sil.PermSub(left, right) => backup
+          (isStrictlyNegativePerm(left) && isStrictlyNegativePerm(right)) || backup()
+        case sil.PermSub(left, right) => backup()
         case sil.PermMul(a, b) =>
           (isStrictlyPositivePerm(a) && isStrictlyNegativePerm(b)) || (isStrictlyNegativePerm(a) && isStrictlyPositivePerm(b))
         case sil.PermDiv(a, b) =>
@@ -1733,7 +1739,7 @@ class QuantifiedPermModule(val verifier: Verifier)
           ((n > IntLit(0)) && isStrictlyNegativePerm(b)) || ((n < IntLit(0)) && isStrictlyPositivePerm(b))
         case sil.CondExp(cond, thn, els) =>
           CondExp(translateExp(cond), isStrictlyNegativePerm(thn), isStrictlyNegativePerm(els))
-        case _ => backup
+        case _ => backup()
       }
     }