Merge pull request #757 from viperproject/meilers_fix_termination_pre_inhale

Fix earlier termination plugin fix

Author: marcoeilers

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

@@ -19,13 +19,17 @@ import viper.silver.verifier.ConsistencyError
 trait ExpTransformer extends ProgramManager with ErrorReporter {
 
   /**
-   * Transforms an expression into a statement.
+   * Transforms an expression into a statement that checks the termination conditions for that expression.
+   * If inhaleExp is true, the expression is inhaled during the check.
    *
    * @return a statement representing the expression.
    */
-  def transformExp(e: Exp, c: ExpressionContext): Stmt = e match {
-    case And(fst, snd) =>
-      val fstStmt = transformExp(fst, c)
+  def transformExp(e: Exp, c: ExpressionContext, inhaleExp: Boolean): Stmt = e match {
+    case And(fst, snd) if inhaleExp =>
+      // Special case conjunctions s.t. we properly inhale the first expression before checking the second.
+      // This is necessary if fst contains e.g. a quantified permission, and snd is well-defined only if that quantified
+      // permission is available.
+      val fstStmt = transformExp(fst, c, inhaleExp)
       val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
       val assumeFalse = Inhale(FalseLit()())()
       val inhaleFst = Inhale(fst)()
@@ -39,20 +43,20 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
       }
       val fstIf = If(nonDetVarDecl.localVar, Seqn(Seq(fstStmt, assumeFalse), Nil)(), Seqn(Seq(inhaleFstStmt), Nil)())(e.pos, e.info, e.errT)
       val fstBlock = Seqn(Seq(fstIf), Seq(nonDetVarDecl))()
-      val sndStmt = transformExp(snd, c)
+      val sndStmt = transformExp(snd, c, inhaleExp)
       Seqn(Seq(fstBlock, sndStmt), Nil)()
     case CondExp(cond, thn, els) =>
-      val condStmt = transformExp(cond, c)
-      val thnStmt = transformExp(thn, c)
-      val elsStmt = transformExp(els, c)
+      val condStmt = transformExp(cond, c, false)
+      val thnStmt = transformExp(thn, c, inhaleExp)
+      val elsStmt = transformExp(els, c, inhaleExp)
 
       val ifStmt = If(cond, Seqn(Seq(thnStmt), Nil)(), Seqn(Seq(elsStmt), Nil)())()
 
       val stmts = Seq(condStmt, ifStmt)
       Seqn(stmts, Nil)()
     case Unfolding(acc, unfBody) =>
-      val permCheck = transformExp(acc.perm, c)
-      val unfoldBody = transformExp(unfBody, c)
+      val permCheck = transformExp(acc.perm, c, false)
+      val unfoldBody = transformExp(unfBody, c, inhaleExp)
       // only unfold and fold if body contains something
       val (unfold, fold) = (Unfold(acc)(), Fold(acc)())
 
@@ -61,32 +65,32 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case Applying(wand, body) =>
       // note that this case is untested -- it's not possible to write a function with an `applying` expression
       val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
-      val bodyStmt = transformExp(body, c)
+      val bodyStmt = transformExp(body, c, inhaleExp)
       val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val thnStmt = Seqn(Seq(Apply(wand)(e.pos, e.info, e.errT), bodyStmt, killBranchStmt), Nil)()
       val ifStmt = If(nonDetVarDecl.localVar, thnStmt, EmptyStmt)(e.pos, e.info, e.errT)
       Seqn(Seq(ifStmt), Seq(nonDetVarDecl))(e.pos, e.info, e.errT)
     case inex: InhaleExhaleExp =>
-      val inhaleStmt = transformExp(inex.in, c)
-      val exhaleStmt = transformExp(inex.ex, c)
+      val inhaleStmt = transformExp(inex.in, c, inhaleExp)
+      val exhaleStmt = transformExp(inex.ex, c, inhaleExp)
 
       c.conditionInEx match {
         case Some(conditionVar) => If(conditionVar.localVar, Seqn(Seq(inhaleStmt), Nil)(), Seqn(Seq(exhaleStmt), Nil)())()
         case None => Seqn(Seq(inhaleStmt, exhaleStmt), Nil)()
       }
     case letExp: Let =>
-      val expressionStmt = transformExp(letExp.exp, c)
+      val expressionStmt = transformExp(letExp.exp, c, false)
       val localVarDecl = letExp.variable
 
       val inhaleEq = Inhale(EqCmp(localVarDecl.localVar, letExp.exp)())()
 
-      val bodyStmt = transformExp(letExp.body, c)
+      val bodyStmt = transformExp(letExp.body, c, inhaleExp)
 
       Seqn(Seq(expressionStmt, inhaleEq, bodyStmt), Seq(localVarDecl))()
 
     case b: BinExp =>
-      val left = transformExp(b.left, c)
-      val right = transformExp(b.right, c)
+      val left = transformExp(b.left, c, inhaleExp)
+      val right = transformExp(b.right, c, inhaleExp)
 
       // Short circuit evaluation
       val pureLeft: Exp = toPureBooleanExp(c).execute(b.left)
@@ -111,21 +115,21 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case _: LocationAccess => EmptyStmt
 
     case ap: AccessPredicate =>
-      val check = transformExp(ap.perm, c)
+      val check = transformExp(ap.perm, c, false)
       val inhale = Inhale(ap)(ap.pos)
       Seqn(Seq(check, inhale), Nil)()
     case fa: Forall =>
       // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
       // for arbitrary values, which is similar to a forall introduction
       val (localDeclMapping, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       Seqn(Seq(expressionStmt), localDeclMapping.map(_._2))(fa.pos, fa.info, fa.errT)
     case fp: ForPerm =>
       // let's pick arbitrary values for the quantified variables and check the body given that the current heap has
       // sufficient permissions
       val (localDeclMapping, transformedExp) = substituteWithFreshVars(fp.variables, fp.exp)
       val transformedRes = applySubstitution(localDeclMapping, fp.resource)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val thnStmt = Seqn(Seq(expressionStmt, killBranchStmt), Nil)(e.pos, e.info, e.errT)
       val ifCond = GtCmp(CurrentPerm(transformedRes)(e.pos, e.info, e.errT), NoPerm()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
@@ -137,15 +141,15 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
       // we can't use an assume statement at this point because the `assume`s have already been rewritten
       // furthermore, Viper only allows pure existentially quantified expressions
       val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       Seqn(Seq(inhaleWitnesses, expressionStmt), localDeclMapping.map(_._2))(ex.pos, ex.info, ex.errT)
     case fa: FuncLikeApp =>
-      val argStmts = fa.args.map(transformExp(_, c))
+      val argStmts = fa.args.map(transformExp(_, c, false))
       Seqn(argStmts, Nil)()
     case e: ExtensionExp => reportUnsupportedExp(e)
 
     case _ =>
-      val sub = e.subExps.map(transformExp(_, c))
+      val sub = e.subExps.map(transformExp(_, c, false))
       Seqn(sub, Nil)()
   }
 

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

@@ -53,7 +53,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         val context = FContext(f)
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = Simplifier.simplify(transformExp(f.body.get, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(f.body.get, context, false))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -88,7 +88,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
           .reduce((e, p) => And(e, p)(e.pos))
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = Simplifier.simplify(transformExp(posts, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(posts, context, false))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -113,7 +113,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // concatenate all pres
         val pres = f.pres.reduce((e, p) => And(e, p)(e.pos))
 
-        val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context))
+        val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context, true))
 
         if (proofMethodBody != EmptyStmt) {
           val proofMethod = Method(proofMethodName, f.formalArgs, Nil, Nil, Nil,
@@ -136,12 +136,12 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
    *
    * @return a statement representing the expression
    */
-  override def transformExp(e: Exp, c: ExpressionContext): Stmt = (e, c) match {
+  override def transformExp(e: Exp, c: ExpressionContext, inhaleExp: Boolean): Stmt = (e, c) match {
     case (functionCall: FuncApp, context: FunctionContext @unchecked) =>
       val stmts = collection.mutable.ArrayBuffer[Stmt]()
 
       // check the arguments
-      val termChecksOfArgs: Seq[Stmt] = functionCall.getArgs map (a => transformExp(a, context))
+      val termChecksOfArgs: Seq[Stmt] = functionCall.getArgs map (a => transformExp(a, context, false))
       stmts.appendAll(termChecksOfArgs)
 
       getFunctionDecreasesSpecification(context.functionName).tuple match {
@@ -218,7 +218,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // should not happen
       }
       Seqn(stmts.toSeq, Nil)()
-    case _ => super.transformExp(e, c)
+    case _ => super.transformExp(e, c, inhaleExp)
   }
 
   // context creator

src/test/resources/all/issues/silicon/0768.vpr

@@ -86,4 +86,26 @@ function inp_to_seq_2(inp: pointer, n: Int): Seq[Int]
    decreases
 {
   Seq[Int]()
-}
+}
+
+// Regression test for a bug in the original fix:
+
+adt tree {
+    leaf(value: Int)
+    node(left: tree, right: tree)
+}
+
+function leafCount(t: tree): Int
+    decreases 1
+{
+    id(t.isleaf && t.isleaf ?
+        (1) :
+        //:: ExpectedOutput(termination.failed:tuple.false)
+        (leafCount(t.left) + leafCount(t.right)))
+}
+
+function id(i: Int): Int
+    decreases 0
+{
+    i
+}