Check by default that all pure and ghost functions have termination m…

…easures (#718)

* add desired functionality

* backup

* fix tests

* Apply suggestions from code review

Co-authored-by: Linard Arquint <[email protected]>

* fix tests

* check that all ghost methods have a termination measure as well

* fix tests

---------

Co-authored-by: Linard Arquint <[email protected]>

src/main/resources/stubs/net/ip.gobra

@@ -144,6 +144,7 @@ func (ip IP) To4() (res IP) {
 
 pure
 preserves forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/100000)
+decreases _
 func isZeros(s []byte) bool
 
 // To16 converts the IP address ip to a 16-byte representation.

src/main/resources/stubs/net/net.gobra

@@ -171,6 +171,7 @@ pred (op *OpError) Mem() {
 }
 
 requires acc(e.Mem(), _)
+decreases
 pure func (e *OpError) Unwrap() error { return unfolding acc(e.Mem(), _) in e.Err }
 
 requires acc(e.Mem())
@@ -271,8 +272,10 @@ type UnknownNetworkError string
 
 func (e UnknownNetworkError) Error() string   // { return "unknown network " + string(e) }
 ensures !res
+decreases
 pure func (e UnknownNetworkError) Timeout() (res bool)   { return false }
 ensures !res
+decreases
 pure func (e UnknownNetworkError) Temporary() (res bool) { return false }
 
 type InvalidAddrError string

src/main/resources/stubs/strings/strings.gobra

@@ -151,6 +151,7 @@ ensures len(elems) == 0 ==> res == ""
 ensures len(elems) == 1 ==> res == elems[0]
 // (joao) Leads to precondition of call might not hold (permission to elems[i] might not suffice)
 // ensures len(elems) > 1 ==> res == elems[0] + sep + Join(elems[1:], sep)
+decreases _
 pure func Join(elems []string, sep string) (res string) /*{
 	switch len(elems) {
 	case 0:
@@ -176,26 +177,18 @@ pure func Join(elems []string, sep string) (res string) /*{
 
 // HasPrefix tests whether the string s begins with prefix.
 pure
-ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix)
+decreases
 func HasPrefix(s, prefix string) (ret bool) {
 	return len(s) >= len(prefix) && (s[0:len(prefix)] == prefix)
 }
 
 // HasSuffix tests whether the string s ends with suffix.
 pure
-ensures ret == (len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix)
+decreases
 func HasSuffix(s, suffix string) (ret bool) {
 	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
 }
 
-// Map returns a copy of the string s with all its characters modified
-// according to the mapping function. If mapping returns a negative value, the character is
-// dropped from the string with no replacement.
-// (joao) no support for higher-order functions
-/*
-func Map(mapping func(rune) rune, s string) string 
-*/
-
 // Repeat returns a new string consisting of count copies of the string s.
 //
 // It panics if count is negative or if

src/main/resources/stubs/sync/mutex.gobra

@@ -14,6 +14,7 @@ pred (m *Mutex) UnlockP()
 
 ghost
 requires acc(m.LockP(), _)
+decreases _
 pure func (m *Mutex) LockInv() pred()
 
 ghost

src/main/resources/stubs/sync/waitgroup.gobra

@@ -17,25 +17,27 @@ pred (wg *WaitGroup) Token(t pred())
 
 ghost
 requires acc(g.WaitGroupP(), _)
+decreases _
 pure func (g *WaitGroup) WaitMode() bool
 
 ghost
 requires acc(g) && *g == WaitGroup{}
 ensures g.WaitGroupP() && !g.WaitMode()
-decreases
+decreases _
 func (g *WaitGroup) Init()
 
 ghost
 requires g.WaitGroupP()
 ensures g.WaitGroupP() && !g.WaitMode()
+decreases _
 func (g *WaitGroup) UnsetWaitMode()
 
 ghost
 requires p > 0
 requires acc(g.WaitGroupP(), p)
 requires !g.WaitMode() && g.UnitDebt(P)
 ensures g.UnitDebt(P) && acc(g.WaitGroupStarted(), p)
-decreases
+decreases _
 func (g *WaitGroup) Start(ghost p perm, ghost P pred())
 
 ghost
@@ -45,7 +47,7 @@ requires p + q == 1
 requires acc(g.WaitGroupP(), p)
 requires acc(g.WaitGroupStarted(), q)
 ensures g.WaitGroupP() && g.WaitMode()
-decreases
+decreases _
 func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 
 // Simplified version of the debt redistribution rule. The most general version cannot be written in Gobra
@@ -54,20 +56,21 @@ func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 ghost
 requires P() && g.UnitDebt(P)
 ensures g.UnitDebt(PredTrue!<!>)
-decreases
+decreases _
 func (g *WaitGroup) PayDebt(ghost P pred())
 
 // Simplified version of the debt redistribution rule, instantiated with P == { PredTrue!<!> } and Q == { R }.
 // This is the only rule that generates a Token.
 ghost
 requires g.UnitDebt(PredTrue!<!>)
 ensures g.UnitDebt(R) && g.Token(R)
-decreases
+decreases _
 func (g *WaitGroup) GenerateTokenAndDebt(ghost R pred())
 
 ghost
 requires R()
 ensures g.Token(R)
+decreases _
 func (g *WaitGroup) GenerateToken(ghost R pred())
 
 // Simplified version of Add as proposed in page 8 of Martin's latest document (as of 21/01/2021)
@@ -80,11 +83,11 @@ ensures (n > 0 && p == 0) ==> g.UnitDebt(P)
 ensures n > 0 ==> acc(g.UnitDebt(PredTrue!<!>), n/1)
 // this is actually necessary, otherwise Gobra cannot prove that Add does not modify the wait mode
 ensures (n > 0 && p > 0) ==> g.WaitMode() == old(g.WaitMode())
-decreases
+decreases _
 func (g *WaitGroup) Add(n int, ghost p perm, ghost P pred())
 
 requires g.UnitDebt(PredTrue!<!>)
-decreases
+decreases _
 func (g *WaitGroup) Done()
 
 requires p > 0
@@ -117,6 +120,7 @@ requires len(Q) == len(permsQ)
 requires g.UnitDebt(CollectFractions!<P ++ Q, permsP ++ permsQ!>)
 requires g.UnitDebt(PredTrue!<!>)
 ensures g.UnitDebt(CollectFractions!<P, permsP!>) && g.UnitDebt(CollectFractions!<Q, permsQ!>)
+decreases _
 func (g *WaitGroup) SplitSequence(ghost P seq[pred()], ghost Q seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm])
 
 // Special case of the debt redistribution rule
@@ -131,4 +135,5 @@ requires g.UnitDebt(PredTrue!<!>)
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] + permsQ[i] == permsR[i]
 ensures g.UnitDebt(CollectFractions!<P, permsP!>)
 ensures g.UnitDebt(CollectFractions!<P, permsQ!>)
+decreases _
 func (g *WaitGroup) SplitFractions(ghost P seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm], ghost permsR seq[perm])

src/main/scala/viper/gobra/frontend/Config.scala

@@ -74,6 +74,7 @@ object ConfigDefaults {
   lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
   lazy val DefaultRequireTriggers: Boolean = false
   lazy val DefaultDisableSetAxiomatization: Boolean = false
+  lazy val DefaultDisableCheckTerminationPureFns: Boolean = false
 }
 
 // More-complete exhale modes
@@ -141,6 +142,7 @@ case class Config(
                    // when enabled, all quantifiers without triggers are rejected
                    requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
                    disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
+                   disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
 ) {
 
   def merge(other: Config): Config = {
@@ -192,6 +194,7 @@ case class Config(
       parseAndTypeCheckMode = parseAndTypeCheckMode,
       requireTriggers = requireTriggers || other.requireTriggers,
       disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization,
+      disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
     )
   }
 
@@ -247,6 +250,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
                       requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
                       disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
+                      disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -306,6 +310,7 @@ trait RawConfig {
     parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode,
     requireTriggers = baseConfig.requireTriggers,
     disableSetAxiomatization = baseConfig.disableSetAxiomatization,
+    disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
   )
 }
 
@@ -710,6 +715,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true,
   )
 
+  val disableCheckTerminationPureFns: ScallopOption[Boolean] = opt[Boolean](
+    name = "disablePureFunctsTerminationRequirement",
+    descr = "Do not enforce that all pure functions must have termination measures",
+    default = Some(ConfigDefaults.DefaultDisableCheckTerminationPureFns),
+    noshort = true,
+  )
+
   val parseAndTypeCheckMode: ScallopOption[TaskManagerMode] = choice(
     name = "parseAndTypeCheckMode",
     choices = Seq("LAZY", "SEQUENTIAL", "PARALLEL"),
@@ -909,5 +921,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     parseAndTypeCheckMode = parseAndTypeCheckMode(),
     requireTriggers = requireTriggers(),
     disableSetAxiomatization = disableSetAxiomatization(),
+    disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
   )
 }

src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala

@@ -22,9 +22,16 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefActualMember(member: PActualMember): Messages = member match {
     case n: PFunctionDecl =>
-      wellDefVariadicArgs(n.args) ++ wellDefIfPureFunction(n) ++ wellDefIfInitBlock(n) ++ wellDefIfMain(n)
+      wellDefVariadicArgs(n.args) ++
+        wellDefIfPureFunction(n) ++
+        wellDefIfInitBlock(n) ++
+        wellDefIfMain(n) ++
+        wellFoundedIfNeeded(n)
     case m: PMethodDecl =>
-      wellDefVariadicArgs(m.args) ++ isReceiverType.errors(miscType(m.receiver))(member) ++ wellDefIfPureMethod(m)
+      wellDefVariadicArgs(m.args) ++
+        isReceiverType.errors(miscType(m.receiver))(member) ++
+        wellDefIfPureMethod(m) ++
+        wellFoundedIfNeeded(m)
     case b: PConstDecl =>
       b.specs.flatMap(wellDefConstSpec)
     case g: PVarDecl if isGlobalVarDeclaration(g) =>

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -7,11 +7,12 @@
 package viper.gobra.frontend.info.implementation.typing.ghost
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
-import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody}
+import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMember, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody}
 import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec}
 import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.BaseTyping
+import viper.gobra.util.Violation
 
 trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
@@ -58,8 +59,23 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
       }
   }
 
-  private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
+  private[typing] def wellFoundedIfNeeded(member: PMember): Messages = {
+    val spec = member match {
+      case m: PMethodDecl => m.spec
+      case f: PFunctionDecl => f.spec
+      case _ => Violation.violation("Unexpected member type")
+    }
+    val hasMeasureIfNeeded =
+      if (spec.isPure || isEnclosingGhost(member))
+        config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty
+      else
+        true
+    val needsMeasureError =
+      error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded)
+    needsMeasureError
+  }
 
+  private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
     if (member.spec.isPure) {
       isSingleResultArg(member) ++
         isSinglePureReturnExpr(member) ++

src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala

@@ -16,10 +16,12 @@ import viper.gobra.translator.Names
 import viper.gobra.translator.encodings.combinators.LeafTypeEncoding
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.util.FunctionGenerator
+import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.gobra.translator.util.ViperWriter.CodeLevel._
 import viper.gobra.translator.util.ViperWriter.CodeWriter
 import viper.gobra.util.TypeBounds
 import viper.silver.{ast => vpr}
+import viper.silver.plugin.standard.termination
 
 import scala.annotation.unused
 
@@ -181,6 +183,7 @@ class StringEncoding extends LeafTypeEncoding {
     *     requires l <= h
     *     requires h <= len(s)
     *     ensures strLen(s) == h - l
+    *     decreases _
     * where s is a string id and l and r are the lower and upper bounds of the slice
     */
   private val strSliceName: String = "strSlice"
@@ -197,7 +200,8 @@ class StringEncoding extends LeafTypeEncoding {
       pres = Seq(
         vpr.LeCmp(vpr.IntLit(0)(), argL.localVar)(),
         vpr.LeCmp(argL.localVar, argH.localVar)(),
-        vpr.LeCmp(argH.localVar, vpr.DomainFuncApp(lenFunc, Seq(argS.localVar), Map.empty)())()
+        vpr.LeCmp(argH.localVar, vpr.DomainFuncApp(lenFunc, Seq(argS.localVar), Map.empty)())(),
+        synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate"),
       ),
       posts = Seq(
         vpr.EqCmp(

src/test/resources/regressions/examples/tutorial-examples/basicAnnotations.gobra

@@ -5,24 +5,28 @@ package tutorial
 
 requires 0 <= n // precondition
 ensures sum == n * (n+1)/2 // postcondition
+decreases
 func sum(n int) (sum int) {
 	sum := 0
 
 	invariant 0 <= i && i <= n + 1 
 	invariant sum == i * (i-1)/2
+	decreases n - i
 	for i := 0; i <= n; i++ {
 			sum += i
 	}
 	return sum
 }
 
 ensures res == (n % 2 == 0)
+decreases
 pure func isEven(n int) (res bool) {
 	return n % 2 == 0
 }
 
 ensures isEven(n) ==> res == n / 2
 ensures !isEven(n) ==> res == n / 2 + 1
+decreases
 func halfRoundedUp(n int) (res int) {
 	if isEven(n) {
 		res = n / 2

src/test/scala/viper/gobra/GobraPackageTests.scala

@@ -62,7 +62,10 @@ class GobraPackageTests extends GobraTests {
             "--logLevel", "INFO",
             "--directory", currentDir.toFile.getPath,
             "--projectRoot", currentDir.toFile.getPath, // otherwise, it assumes Gobra's root directory as the project root
-            "-I", currentDir.toFile.getPath
+            "-I", currentDir.toFile.getPath,
+            // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
+            // but requires some work to add termination measures all over the test suite.
+            "--disablePureFunctsTerminationRequirement",
           ))
         } yield config
 

src/test/scala/viper/gobra/GobraTests.scala

@@ -56,6 +56,9 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
       checkConsistency = true,
       cacheParserAndTypeChecker = cacheParserAndTypeChecker,
       z3Exe = z3Exe,
+      // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
+      // but requires some work to add termination measures all over the test suite.
+      disableCheckTerminationPureFns = true,
     )
 
   override def runTests(testName: Option[String], args: Args): Status = {

src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala

@@ -341,7 +341,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
         new PackageInfo("pkg", "pkg", false)
       )
       val tree = new Info.GoTree(pkg)
-      val config = Config()
+      val config = Config(disableCheckTerminationPureFns = true)
       val info = new TypeInfoImpl(tree, Map.empty)(config)
       info.errors match {
         case Vector(msgs) => fail(s"Type-checking failed: $msgs")

src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala

@@ -32,12 +32,12 @@ class StatsCollectorTests extends AnyFunSuite with BeforeAndAfterAll {
   }
 
   test("Integration without chopper") {
-    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--disablePureFunctsTerminationRequirement"))
     runIntegration(config)
   }
 
   test("Integration with chopper") {
-    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--chop", "10"))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--chop", "10", "--disablePureFunctsTerminationRequirement"))
     runPackagesSeparately(config)
     runIntegration(config)
   }