diff --git a/src/main/resources/stubs/net/ip.gobra b/src/main/resources/stubs/net/ip.gobra index f6a3ee897..0c177d6bc 100644 --- a/src/main/resources/stubs/net/ip.gobra +++ b/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. diff --git a/src/main/resources/stubs/net/net.gobra b/src/main/resources/stubs/net/net.gobra index d1d1ff11e..0319d37dd 100644 --- a/src/main/resources/stubs/net/net.gobra +++ b/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 diff --git a/src/main/resources/stubs/strings/strings.gobra b/src/main/resources/stubs/strings/strings.gobra index 0307bf577..2d652bc53 100644 --- a/src/main/resources/stubs/strings/strings.gobra +++ b/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 diff --git a/src/main/resources/stubs/sync/mutex.gobra b/src/main/resources/stubs/sync/mutex.gobra index 9f400718c..94f4a2d2f 100644 --- a/src/main/resources/stubs/sync/mutex.gobra +++ b/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 diff --git a/src/main/resources/stubs/sync/waitgroup.gobra b/src/main/resources/stubs/sync/waitgroup.gobra index 2de127d4d..f42663519 100644 --- a/src/main/resources/stubs/sync/waitgroup.gobra +++ b/src/main/resources/stubs/sync/waitgroup.gobra @@ -17,17 +17,19 @@ 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 @@ -35,7 +37,7 @@ 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,7 +56,7 @@ 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 }. @@ -62,12 +64,13 @@ func (g *WaitGroup) PayDebt(ghost P pred()) 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!

) requires g.UnitDebt(PredTrue!) ensures g.UnitDebt(CollectFractions!) && g.UnitDebt(CollectFractions!) +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!) ensures g.UnitDebt(CollectFractions!) +decreases _ func (g *WaitGroup) SplitFractions(ghost P seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm], ghost permsR seq[perm]) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index fef81bce0..2d503c0f9 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/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(), ) } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index 0fcf977b9..a8fd70d43 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/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) => diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index 6ff5bef67..6fefc23d1 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/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) ++ diff --git a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala index c5416a789..ba6c8abab 100644 --- a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala +++ b/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( diff --git a/src/test/resources/regressions/examples/tutorial-examples/basicAnnotations.gobra b/src/test/resources/regressions/examples/tutorial-examples/basicAnnotations.gobra index 2c016db97..f2dd40403 100644 --- a/src/test/resources/regressions/examples/tutorial-examples/basicAnnotations.gobra +++ b/src/test/resources/regressions/examples/tutorial-examples/basicAnnotations.gobra @@ -5,11 +5,13 @@ 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 } @@ -17,12 +19,14 @@ func sum(n int) (sum int) { } 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 diff --git a/src/test/scala/viper/gobra/GobraPackageTests.scala b/src/test/scala/viper/gobra/GobraPackageTests.scala index 8e01bcc49..49738fd19 100644 --- a/src/test/scala/viper/gobra/GobraPackageTests.scala +++ b/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 diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala index d5ae82305..9de0ce90d 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/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 = { diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala index dd203575a..d71f9f84a 100644 --- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala +++ b/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") diff --git a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala b/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala index 25980a22a..a8fa3ee9f 100644 --- a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala +++ b/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) }