Merge pull request #711 from viperproject/meilers_func_post_selfrefer…

…ences

Forbidding function self-references in postconditions for functions without decreases clauses

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

@@ -6,9 +6,9 @@
 
 package viper.silver.plugin.standard.termination
 
-import viper.silver.ast.utility.ViperStrategy
+import viper.silver.ast.utility.{Functions, ViperStrategy}
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
-import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
+import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, FuncApp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
 import viper.silver.plugin.standard.termination.transformation.Trafo
@@ -111,6 +111,34 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * Remove decreases clauses from the AST and add them as information to the AST nodes
    */
   override def beforeVerify(input: Program): Program = {
+    // Prevent potentially unsafe (mutually) recursive function calls in function postcondtions
+    // for all functions that don't have a decreases clause
+    lazy val cycles = Functions.findFunctionCyclesVia(input, func => func.body.toSeq, func => func.body.toSeq)
+    for (f <- input.functions) {
+      val hasDecreasesClause = (f.pres ++ f.posts).exists(p => p.shallowCollect {
+        case dc: DecreasesClause => dc
+      }.nonEmpty)
+      if (!hasDecreasesClause) {
+        val funcCycles = cycles.get(f)
+        val problematicFuncApps = f.posts.flatMap(p => p.shallowCollect {
+          case fa: FuncApp if fa.func(input) == f => fa
+          case fa: FuncApp if funcCycles.isDefined && funcCycles.get.contains(fa.func(input)) => fa
+        }).toSet
+        for (fa <- problematicFuncApps) {
+          val calledFunc = fa.func(input)
+          if (calledFunc == f) {
+            if (fa.args == f.formalArgs.map(_.localVar)) {
+              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use \"result\" instead to refer to the result of the function.", fa.pos))
+            } else {
+              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+            }
+          } else {
+            reportError(ConsistencyError(s"Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+          }
+        }
+      }
+    }
+
     // extract all decreases clauses from the program
     val newProgram: Program = extractDecreasesClauses.execute(input)
 

src/test/resources/all/issues/carbon/0239.vpr

@@ -4,6 +4,7 @@
 field val : Int
 
 function bool2Ref(b: Bool) : Ref
+  decreases *
   ensures result != null && bool2Ref(true) != bool2Ref(false) // injectivity - doesn't change the behaviour
 
 method m(x:Ref)

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

@@ -4,8 +4,10 @@
 function count(lo: Int, hi: Int, a: Dummy):Int
   ensures hi <= lo ==> result == 0
   ensures lo <= hi ==> count(lo, hi+1, a) == result + (loc(a, hi) ? 0 : 1)
+  decreases *
 
 function recfun(x: Int): Int
+  decreases *
   requires x > 0
   ensures recfun(x) < 0
 { -x }

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

@@ -2,6 +2,7 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 function int___box__(int: Int): Ref
+  decreases *
   ensures (forall other: Int ::  (int___box__(other) == result) == (other == int))
 
 method test(i: Int, j: Int) {

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

@@ -11,6 +11,7 @@ domain Epsilon {
 
 function tokCountRef(r:Ref): Ref
     ensures tokCountRef(temp(r))==result // removing this line makes the file verify with silicon
+    decreases *
 
 domain parallelHeaps { 
     function temp(x: Ref): Ref 

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

@@ -0,0 +1,84 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/int.vpr>
+
+// Testing consistency checks for functions with self-references in their postconditions.
+
+// w/o decreases
+function fac(i: Int): Int
+    requires i >= 0
+    //:: ExpectedOutput(consistency.error)
+    ensures fac(i) >= 1
+{
+    i == 0 ? 1 : i * fac(i - 1)
+}
+
+function faca(i: Int): Int
+    requires i >= 0
+    //:: ExpectedOutput(consistency.error)
+    ensures faca(i + 1) >= 1
+
+
+function fac1(i: Int): Int
+    requires i >= 0
+    //:: ExpectedOutput(consistency.error)
+    ensures fac2(i) >= 1
+{
+    i == 0 ? 1 : i * fac2(i - 1)
+}
+
+function fac2(i: Int): Int
+    requires i >= 0
+    //:: ExpectedOutput(consistency.error)
+    ensures fac1(i - 1) >= 1
+{
+    i == 0 ? 1 : i * fac1(i - 1)
+}
+
+function lol(i: Int): Int
+    //:: ExpectedOutput(consistency.error)
+    ensures lol(0) > 0
+{
+    i + 1
+}
+
+
+// same with all kinds of decreases clauses
+
+function dfac(i: Int): Int
+    requires i >= 0
+    ensures dfac(i) >= 1  // would raise a termination error if this file got to the verification stage
+    decreases i
+{
+    i == 0 ? 1 : i * dfac(i - 1)
+}
+
+function dfaca(i: Int): Int
+    requires i >= 0
+    ensures dfaca(i + 1) >= 1
+    decreases _
+
+
+function dfac1(i: Int): Int
+    requires i >= 0
+    ensures dfac2(i) >= 1  // would raise a termination error if this file got to the verification stage
+    decreases i
+{
+    i == 0 ? 1 : i * dfac2(i - 1)
+}
+
+function dfac2(i: Int): Int
+    decreases *
+    requires i >= 0
+    ensures dfac1(i - 1) >= 1  // would raise a termination error if this file got to the verification stage
+{
+    i == 0 ? 1 : i * dfac1(i - 1)
+}
+
+function dlol(i: Int): Int
+    ensures dlol(0) > 0  // would raise a termination error if this file got to the verification stage
+    decreases
+{
+    i + 1
+}