Adapting termination plugin to new function permission semantics (#824)

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -276,7 +276,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       // if decreases checks are deactivated, only remove the decreases clauses from the program
       newProgram
     } else {
-      val trafo = new Trafo(newProgram, reportError)
+      val trafo = new Trafo(newProgram, reportError, config != null && config.respectFunctionPrePermAmounts())
 
       val finalProgram = trafo.getTransformedProgram
       finalProgram

src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala

@@ -7,10 +7,11 @@
 package viper.silver.plugin.standard.termination.transformation
 
 import org.jgrapht.graph.{DefaultDirectedGraph, DefaultEdge}
+import viper.silver.ast.utility.QuantifiedPermissions.SourceQuantifiedPermissionAssertion
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.ast.utility.{Simplifier, ViperStrategy}
-import viper.silver.ast.{And, Bool, ErrTrafo, Exp, FalseLit, FuncApp, Function, LocalVarDecl, Method, Node, NodeTrafo, Old, Result, Seqn, Stmt}
+import viper.silver.ast.{And, Bool, ErrTrafo, Exp, FalseLit, FieldAccessPredicate, FullPerm, FuncApp, Function, Implies, LocalVarDecl, Method, NoPerm, Node, NodeTrafo, Old, PermLtCmp, PredicateAccessPredicate, Result, Seqn, Stmt, TrueLit, Unfold, Unfolding, WildcardPerm}
 import viper.silver.plugin.standard.termination.{DecreasesSpecification, FunctionTerminationError}
 import viper.silver.verifier.errors.AssertFailed
 
@@ -34,7 +35,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
    *
    * @param f function
    */
-  protected def generateProofMethods(f: Function): Seq[Method] = {
+  protected def generateProofMethods(f: Function, respectFuncPermAmounts: Boolean): Seq[Method] = {
 
     getFunctionDecreasesSpecification(f.name) match {
       case DecreasesSpecification(None, _, _) => // no decreases tuple was defined, hence no proof methods required
@@ -125,7 +126,69 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         }
       } else Nil
     }
-    proofMethods
+    if (respectFuncPermAmounts)
+      proofMethods
+    else
+      proofMethods.map(removeConcretePermissionAmounts)
+  }
+
+  /**
+    * Given a method, removes all concrete permission amounts and replaces them with wildcard if they are positive,
+    * otherwise with none.
+    * The transformation is only defined for language constructs that are expected to occur in methods generated
+    * to check function termination, i.e., it assumes there are no fold statements, no method calls, no permission
+    * introspection etc. It would be unsound in the presence of permission introspection, and possibly incomplete
+    * in the presence of method calls etc.
+    */
+  def removeConcretePermissionAmounts[N <: Node](n: N): N = n.transform{
+    case u@Unfold(pap@PredicateAccessPredicate(loc, _)) =>
+      // Assume the permission amount is strictly positive; if not, there will be a verification error anyway.
+      Unfold(PredicateAccessPredicate(loc, Some(WildcardPerm()()))(pap.pos, pap.info, pap.errT))(u.pos, u.info, u.errT)
+    case u@Unfolding(pap@PredicateAccessPredicate(loc, _), b) =>
+      Unfolding(PredicateAccessPredicate(loc, Some(WildcardPerm()()))(pap.pos, pap.info, pap.errT), b)(u.pos, u.info, u.errT)
+    case pap@PredicateAccessPredicate(loc, op) if !op.exists(_.isInstanceOf[WildcardPerm]) =>
+      val papWc = PredicateAccessPredicate(loc, Some(WildcardPerm()()))(pap.pos, pap.info, pap.errT)
+      op match {
+        case None => papWc
+        case Some(p) =>
+          // Condition under which the amount is strictly positive; transform wildcard to write because wildcard
+          // must not be used outside acc(...) and since arithmetic involving wildcards is forbidden, any positive amount
+          // should behave exactly like wildcard.
+          val condition: Exp = Simplifier.simplify(PermLtCmp(NoPerm()(), p.transform{case WildcardPerm() => FullPerm()()})())
+          condition match {
+            case TrueLit() => papWc
+            case FalseLit() => TrueLit()()
+            case _ => Implies(condition, papWc)(pap.pos, pap.info, pap.errT)
+          }
+      }
+    case fap@FieldAccessPredicate(loc, op) if !op.exists(_.isInstanceOf[WildcardPerm]) =>
+      val fapWc = FieldAccessPredicate(loc, Some(WildcardPerm()()))(fap.pos, fap.info, fap.errT)
+      op match {
+        case None => fapWc
+        case Some(p) =>
+          val condition: Exp = Simplifier.simplify(PermLtCmp(NoPerm()(), p.transform{case WildcardPerm() => FullPerm()()})())
+          condition match {
+            case TrueLit() => fapWc
+            case FalseLit() => TrueLit()()
+            case _ => Implies(condition, fapWc)(fap.pos, fap.info, fap.errT)
+          }
+      }
+    case qp@SourceQuantifiedPermissionAssertion(_, Implies(lhs, rhs)) =>
+      // Handle this case explicitly to preserve QP format expected in the AST.
+      // If we do not do this, we could get QP assertions like
+      // forall vars :: lhs ==> (none < p == acc(loc, p))
+      // which the backends cannot handle. So we merge the implications into
+      // forall vars :: lhs && none < p ==> acc(loc, p)
+      val rhsTransformed = removeConcretePermissionAmounts(rhs)
+      rhsTransformed match {
+        case i@Implies(newLhs, newRhs) =>
+          val completeLhs = And(lhs, newLhs)(lhs.pos, lhs.info, lhs.errT)
+          val completeImplies = Implies(completeLhs, newRhs)(i.pos, i.info, i.errT)
+          qp.copy(exp = completeImplies)(qp.pos, qp.info, qp.errT)
+        case r =>
+          val completeImplies = Implies(lhs, rhsTransformed)(r.pos, r.info, r.errT)
+          qp.copy(exp = completeImplies)(qp.pos, qp.info, qp.errT)
+      }
   }
 
 

src/main/scala/viper/silver/plugin/standard/termination/transformation/Trafo.scala

@@ -18,7 +18,8 @@ import viper.silver.verifier.AbstractError
  * @param reportError Interface to report errors occurring during transformation.
  */
 final class Trafo(override val program: Program,
-                  override val reportError: AbstractError => Unit)
+                  override val reportError: AbstractError => Unit,
+                  val respectFuncPermAmounts: Boolean)
   extends ProgramManager with FunctionCheck with MethodCheck {
 
   private var transformedProgram: Option[Program] = None
@@ -29,7 +30,7 @@ final class Trafo(override val program: Program,
   def getTransformedProgram: Program = {
     transformedProgram.getOrElse({
 
-      val proofMethods: Seq[Method] = program.functions.flatMap(generateProofMethods)
+      val proofMethods: Seq[Method] = program.functions.flatMap(generateProofMethods(_, respectFuncPermAmounts))
       val newMethods: Seq[Method] = program.methods.map(transformMethod)
 
       val newProgram: Program = program.copy(methods = newMethods ++ proofMethods)(program.pos, program.info, program.errT)

src/test/resources/termination/functions/basic/permission_issues.vpr

@@ -0,0 +1,89 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// Tests making sure that the termination checks correctly use the different permission semantics for functions
+
+field f: Int
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+function get(x: Ref, term: Bool): Int
+    requires acc(x.f)
+    decreases 0 if term
+{
+    x.f
+}
+
+function fn(r: Ref): Int
+  requires acc(r.f)
+  requires acc(r.f)
+  decreases 0
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  fn(r)
+}
+
+function fnpost(r: Ref): Int
+  requires acc(r.f) && acc(r.f)
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  ensures result > fnpost(r)
+  decreases 0
+{
+  1
+}
+
+function g(x: Ref, i: Int): Int
+    requires acc(P(x), 1/4)
+    decreases i
+{
+    i <= 0 ? 0 : unfolding P(x) in x.f + g(x, i - 1)
+}
+
+function gnt(x: Ref, i: Int): Int
+    requires acc(P(x), 1/4)
+    decreases i
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    i <= 0 ? 0 : unfolding P(x) in x.f + gnt(x, i)
+}
+
+
+function g2(x: Ref, b: Bool): Int
+    requires acc(P(x), b ? 1/4 : none)
+    decreases 0
+{
+    b ? unfolding P(x) in x.f : 1
+}
+
+function g3(x: Ref, b: Bool): Int
+    requires acc(P(x), b ? wildcard : none)
+    decreases 0
+{
+    b ? unfolding P(x) in get(x, true) : 1
+}
+
+function g3f(x: Ref, b: Bool): Int
+    requires acc(P(x), b ? wildcard : none)
+    decreases 0
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    b ? unfolding P(x) in get(x, false) : 1
+}
+
+function g4(x: Ref, b: Bool): Int
+    requires acc(P(x), wildcard)
+    decreases 0
+{
+    unfolding P(x) in get(x, true)
+}
+
+
+function g4f(x: Ref, b: Bool): Int
+    requires acc(P(x), wildcard)
+    decreases 0
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    unfolding P(x) in get(x, false)
+}

src/test/resources/termination/functions/expressions/access.vpr

@@ -18,6 +18,7 @@ function test2(x: Ref): Bool
     decreases
     requires acc(x.f) && acc(x.f) && acc(x.g)
 {
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
     nonTerminating(x)
 }