From c667d67d43f64e3efcddc8bcd6a50c2c1ee8f7fe Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 7 Jun 2023 17:34:02 +0200 Subject: [PATCH 1/6] Auto-including decreases functions and axioms when they are used --- .../silver/frontend/ViperPAstProvider.scala | 100 ++++++++++++++++++ .../termination/TerminationPlugin.scala | 80 +++++++++++++- .../errorMessages/multipleErrors.vpr | 1 - .../termination/functions/basic/adt.vpr | 1 - .../termination/functions/basic/allTypes.vpr | 2 +- .../existingExamples/McCarthys91Fnc.sil | 1 - 6 files changed, 179 insertions(+), 6 deletions(-) create mode 100644 src/main/scala/viper/silver/frontend/ViperPAstProvider.scala diff --git a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala new file mode 100644 index 000000000..8d8757cce --- /dev/null +++ b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala @@ -0,0 +1,100 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2021 ETH Zurich. + +package viper.silver.frontend + + +import ch.qos.logback.classic.Logger +import viper.silver.ast.Program +import viper.silver.logger.ViperStdOutLogger +import viper.silver.plugin.SilverPluginManager +import viper.silver.reporter.{AstConstructionFailureMessage, AstConstructionSuccessMessage, Reporter} +import viper.silver.verifier.{Failure, Success, VerificationResult, Verifier} + +import java.nio.file.Path + + +class ViperPAstProvider(override val reporter: Reporter, + override implicit val logger: Logger = ViperStdOutLogger("ViperPAstProvider", "INFO").get, + private val disablePlugins: Boolean = false) extends SilFrontend { + + class Config(args: Seq[String]) extends SilFrontendConfig(args, "ViperPAstProviderConfig") { + verify() + } + + class PAstProvidingVerifier(rep: Reporter) extends Verifier { + private var _config: Config = _ + + def config: Config = _config + + override def name = "Viper PAST Constructor" + + override def version = "" + + override def buildVersion = "" + + override def copyright: String = "(c) Copyright ETH Zurich 2012 - 2023" + + override def signature: String = name + + override def debugInfo(info: Seq[(String, Any)]): Unit = {} + + override def dependencies: Seq[Nothing] = Nil + + override def start(): Unit = () + + override def stop(): Unit = {} + + override def verify(program: Program): VerificationResult = Success + + override def parseCommandLine(args: Seq[String]): Unit = { + _config = new Config(args) + } + + override def reporter: Reporter = rep + } + + // All phases after sematic analysis omitted + override val phases: Seq[Phase] = Seq(Parsing, SemanticAnalysis) + + override def result: VerificationResult = { + + if (_errors.isEmpty) { + require(state >= DefaultStates.SemanticAnalysis) + Success + } + else { + Failure(_errors) + } + } + + protected var instance: PAstProvidingVerifier = _ + + override def createVerifier(fullCmd: String): Verifier = { + instance = new PAstProvidingVerifier(reporter) + instance + } + + override def configureVerifier(args: Seq[String]): SilFrontendConfig = { + instance.parseCommandLine(args) + instance.config + } + + override def reset(input: Path): Unit = { + super.reset(input) + if (_config != null) { + noPluginsManager = SilverPluginManager(None)(reporter, logger, _config, fp) + } + } + + private var noPluginsManager = SilverPluginManager(None)(reporter, logger, _config, fp) + override def plugins: SilverPluginManager = { + if (disablePlugins) noPluginsManager + else { + super.plugins + } + } +} \ No newline at end of file diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index 8baa5fb3d..86960b7ed 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -16,8 +16,10 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} import viper.silver.verifier.errors.AssertFailed import viper.silver.verifier._ import fastparse._ +import viper.silver.frontend.{DefaultStates, ViperPAstProvider} +import viper.silver.logger.SilentLogger import viper.silver.parser.FastParserCompanion.whitespace -import viper.silver.reporter.Entity +import viper.silver.reporter.{Entity, NoopReporter} import scala.annotation.unused @@ -29,6 +31,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false) + private var decreasesClauses: Set[PDecreasesClause] = Set.empty + /** * Keyword used to define decreases clauses */ @@ -95,7 +99,12 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, // Apply the predicate access to instance transformation only to decreases clauses. val newProgram: PProgram = StrategyBuilder.Slim[PNode]({ - case dt: PDecreasesTuple => transformPredicateInstances.execute(dt): PDecreasesTuple + case dt: PDecreasesTuple => + decreasesClauses = decreasesClauses + dt + transformPredicateInstances.execute(dt): PDecreasesTuple + case dc : PDecreasesClause => + decreasesClauses = decreasesClauses + dc + dc case d => d }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies case PProgram(_, _, _, _, functions, _, methods, _, _) => Seq(functions, methods) @@ -106,6 +115,73 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, newProgram } + override def beforeTranslate(input: PProgram): PProgram = { + val allClauses = decreasesClauses.flatMap{ + case PDecreasesTuple(exps, _) => exps.map(e => e.typ match { + case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ + case _ => e.typ + }) + case _ => Seq() + } + val presentDomains = input.domains.map(_.idndef.name).toSet + + val importStmts = allClauses flatMap { + case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import ") + case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import ") + case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import ") + case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") => Some("import ") + case PMultisetType(_) if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import ") + case PSeqType(_) if !presentDomains.contains("SeqWellFoundedOrder") => Some("import ") + case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import ") + case PPredicateType() if !presentDomains.contains("PredicateInstancesWellFoundedOrder") => + Some("import ") + case _ => None + } + if (importStmts.nonEmpty) { + val importOnlyProgram = importStmts.mkString("\n") + val importPProgram = PAstProvider.generateViperPAst(importOnlyProgram) + val mergedDomains = input.domains.filter(_.idndef.name != "WellFoundedOrder") ++ importPProgram.get.domains + + val mergedProgram = input.copy(domains = mergedDomains)(input.pos) + super.beforeTranslate(mergedProgram) + } else { + super.beforeTranslate(input) + } + } + + object PAstProvider extends ViperPAstProvider(NoopReporter, SilentLogger().get) { + def generateViperPAst(code: String): Option[PProgram] = { + val code_id = code.hashCode.asInstanceOf[Short].toString + _input = Some(code) + execute(Array("--ignoreFile", code_id)) + + if (errors.isEmpty) { + Some(semanticAnalysisResult) + } else { + None + } + } + + def setCode(code: String): Unit = { + _input = Some(code) + } + + override def reset(input: java.nio.file.Path): Unit = { + if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.") + _state = DefaultStates.InputSet + _inputFile = Some(input) + + /** must be set by [[setCode]] */ + // _input = None + _errors = Seq() + _parsingResult = None + _semanticAnalysisResult = None + _verificationResult = None + _program = None + resetMessages() + } + } + /** * Remove decreases clauses from the AST and add them as information to the AST nodes diff --git a/src/test/resources/termination/errorMessages/multipleErrors.vpr b/src/test/resources/termination/errorMessages/multipleErrors.vpr index 1873155f9..3b2425f7a 100644 --- a/src/test/resources/termination/errorMessages/multipleErrors.vpr +++ b/src/test/resources/termination/errorMessages/multipleErrors.vpr @@ -4,7 +4,6 @@ // failure filtering by Silicon should not filter out one of the failures but correctly return both errors import -import function factorialPure(n: Int): Int decreases // wrong termination measure diff --git a/src/test/resources/termination/functions/basic/adt.vpr b/src/test/resources/termination/functions/basic/adt.vpr index ffb07d25e..54095d7a2 100644 --- a/src/test/resources/termination/functions/basic/adt.vpr +++ b/src/test/resources/termination/functions/basic/adt.vpr @@ -1,7 +1,6 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -import domain list { diff --git a/src/test/resources/termination/functions/basic/allTypes.vpr b/src/test/resources/termination/functions/basic/allTypes.vpr index 12df6c866..04aa18733 100644 --- a/src/test/resources/termination/functions/basic/allTypes.vpr +++ b/src/test/resources/termination/functions/basic/allTypes.vpr @@ -1,7 +1,7 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -import +import //Example decreasing Int function fact(x:Int): Int diff --git a/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil b/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil index abc8a33d4..e4e97bee7 100644 --- a/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil +++ b/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil @@ -1,7 +1,6 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -import function mc(n:Int): Int decreases 100-n From fb41857252d2ef73152ad6775822c495482bfce9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 7 Jun 2023 23:55:21 +0200 Subject: [PATCH 2/6] Properly handling unknown types, empty decreases clauses --- .../standard/termination/TerminationPlugin.scala | 4 +++- .../functions/basic/unconstrainedType.vpr | 13 +++++++++++++ .../termination/functions/expressions/forall.vpr | 1 - 3 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 src/test/resources/termination/functions/basic/unconstrainedType.vpr diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index 86960b7ed..bbf4f10f9 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -116,7 +116,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, } override def beforeTranslate(input: PProgram): PProgram = { - val allClauses = decreasesClauses.flatMap{ + val allClauses: Set[Any] = decreasesClauses.flatMap{ + case PDecreasesTuple(Seq(), _) => Seq(()) case PDecreasesTuple(exps, _) => exps.map(e => e.typ match { case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ case _ => e.typ @@ -135,6 +136,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import ") case PPredicateType() if !presentDomains.contains("PredicateInstancesWellFoundedOrder") => Some("import ") + case _ if !presentDomains.contains("WellFoundedOrder") => Some("import ") case _ => None } if (importStmts.nonEmpty) { diff --git a/src/test/resources/termination/functions/basic/unconstrainedType.vpr b/src/test/resources/termination/functions/basic/unconstrainedType.vpr new file mode 100644 index 000000000..07ebd45ae --- /dev/null +++ b/src/test/resources/termination/functions/basic/unconstrainedType.vpr @@ -0,0 +1,13 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + + +domain Huh {} + +function fac(i: Int, h: Huh): Int + requires i >= 0 + decreases h +{ + //:: ExpectedOutput(termination.failed:tuple.false) + i == 0 ? 1 : i * fac(i - 1, h) +} \ No newline at end of file diff --git a/src/test/resources/termination/functions/expressions/forall.vpr b/src/test/resources/termination/functions/expressions/forall.vpr index e1ebb0c82..dbcb61004 100644 --- a/src/test/resources/termination/functions/expressions/forall.vpr +++ b/src/test/resources/termination/functions/expressions/forall.vpr @@ -1,7 +1,6 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -import field f: Int From 273c8c53da4fe37d901437ff452db8c67f381c17 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 8 Jun 2023 00:26:15 +0200 Subject: [PATCH 3/6] Removed now invalid test, fixed issue of equal decreases expressions disappearing (because sets), fixed typo in multiset well-def domain --- .../resources/import/decreases/multiset.vpr | 2 +- .../termination/TerminationPlugin.scala | 12 ++++----- .../termination/errorMessages/notDefined.vpr | 27 ------------------- 3 files changed, 7 insertions(+), 34 deletions(-) delete mode 100644 src/test/resources/termination/errorMessages/notDefined.vpr diff --git a/src/main/resources/import/decreases/multiset.vpr b/src/main/resources/import/decreases/multiset.vpr index 6ad7e8d8d..b129b69b0 100644 --- a/src/main/resources/import/decreases/multiset.vpr +++ b/src/main/resources/import/decreases/multiset.vpr @@ -3,7 +3,7 @@ import "declaration.vpr" -domain MuliSetWellFoundedOrder[S]{ +domain MultiSetWellFoundedOrder[S]{ //MultiSet axiom multiset_ax_dec{ forall mSet1: Multiset[S], mSet2: Multiset[S] :: {decreasing(mSet1, mSet2)} diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index bbf4f10f9..6f83848c6 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -31,7 +31,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false) - private var decreasesClauses: Set[PDecreasesClause] = Set.empty + private var decreasesClauses: Seq[PDecreasesClause] = Seq.empty /** * Keyword used to define decreases clauses @@ -100,10 +100,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, // Apply the predicate access to instance transformation only to decreases clauses. val newProgram: PProgram = StrategyBuilder.Slim[PNode]({ case dt: PDecreasesTuple => - decreasesClauses = decreasesClauses + dt + decreasesClauses = decreasesClauses :+ dt transformPredicateInstances.execute(dt): PDecreasesTuple case dc : PDecreasesClause => - decreasesClauses = decreasesClauses + dc + decreasesClauses = decreasesClauses :+ dc dc case d => d }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies @@ -116,17 +116,17 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, } override def beforeTranslate(input: PProgram): PProgram = { - val allClauses: Set[Any] = decreasesClauses.flatMap{ + val allClauseTypes: Set[Any] = decreasesClauses.flatMap{ case PDecreasesTuple(Seq(), _) => Seq(()) case PDecreasesTuple(exps, _) => exps.map(e => e.typ match { case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ case _ => e.typ }) case _ => Seq() - } + }.toSet val presentDomains = input.domains.map(_.idndef.name).toSet - val importStmts = allClauses flatMap { + val importStmts = allClauseTypes flatMap { case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import ") case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import ") case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import ") diff --git a/src/test/resources/termination/errorMessages/notDefined.vpr b/src/test/resources/termination/errorMessages/notDefined.vpr deleted file mode 100644 index 4401cf0b8..000000000 --- a/src/test/resources/termination/errorMessages/notDefined.vpr +++ /dev/null @@ -1,27 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -// decreases and bounded functions are not imported - -function f(x: Int): Int - //:: ExpectedOutput(consistency.error) - decreases x - requires x >= 0 -{ - x == 0 ? 0 : f(x-1) + f(x) -} - -method m(x: Int) - //:: ExpectedOutput(consistency.error) - decreases x -{ - var y: Int := x - while (y >= 0) - //:: ExpectedOutput(consistency.error) - decreases y - { - y := y-1 - } - - m(y) -} \ No newline at end of file From f2fb201b57fe825c9b09d9fbdfb0f347c7cd7c32 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 18 Jul 2023 16:42:52 +0200 Subject: [PATCH 4/6] Fix typo Co-authored-by: Linard Arquint --- src/main/scala/viper/silver/frontend/ViperPAstProvider.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala index 8d8757cce..8acc71924 100644 --- a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala +++ b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala @@ -57,7 +57,7 @@ class ViperPAstProvider(override val reporter: Reporter, override def reporter: Reporter = rep } - // All phases after sematic analysis omitted + // All phases after semantic analysis omitted override val phases: Seq[Phase] = Seq(Parsing, SemanticAnalysis) override def result: VerificationResult = { From d38b2a486b8b5d5c041d9b7b72cf1d0a231a4779 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 20 Jul 2023 12:23:25 +0200 Subject: [PATCH 5/6] Emit warning if well-foundedness functions are constrained by incorrectly-named domain --- .../termination/TerminationPlugin.scala | 53 ++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index 61a0ae256..ca17ad5e9 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -19,7 +19,7 @@ import fastparse._ import viper.silver.frontend.{DefaultStates, ViperPAstProvider} import viper.silver.logger.SilentLogger import viper.silver.parser.FastParserCompanion.whitespace -import viper.silver.reporter.{Entity, NoopReporter} +import viper.silver.reporter.{Entity, NoopReporter, WarningsDuringTypechecking} import scala.annotation.unused @@ -113,6 +113,45 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, newProgram } + private def constrainsWellfoundednessUnexpectedly(ax: PAxiom, wfTypeName: Option[String]): Seq[PType] = { + + def isWellFoundedFunctionCall(c: PCall): Boolean = { + if (!c.isDomainFunction) + return false + if (!(c.idnuse.name == "decreases" || c.idnuse.name == "bounded")) + return false + c.function match { + case df: PDomainFunction => df.domainName.name == "WellFoundedOrder" + case _ => false + } + } + + def isNotExpectedConstrainedType(t: PType): Boolean = { + if (!t.isValidOrUndeclared) + return false + if (wfTypeName.isEmpty) + return true + val typeName = t match { + case PPrimitiv("Perm") => "Rational" + case PPrimitiv(n) => n + case PSeqType(_) => "Seq" + case PSetType(_) => "Set" + case PMultisetType(_) => "MultiSet" + case PMapType(_, _) => "Map" + case PDomainType(d, _) if d.name == "PredicateInstance" => "PredicateInstances" + case PDomainType(d, _) => d.name + } + !wfTypeName.contains(typeName) + } + + ax.exp.shallowCollect{ + case c: PCall if isWellFoundedFunctionCall(c) && c.domainSubstitution.isDefined && + c.domainSubstitution.get.contains("T") && + isNotExpectedConstrainedType(c.domainSubstitution.get.get("T").get) => + c.domainSubstitution.get.get("T").get + } + } + override def beforeTranslate(input: PProgram): PProgram = { val allClauseTypes: Set[Any] = decreasesClauses.flatMap{ case PDecreasesTuple(Seq(), _) => Seq(()) @@ -124,6 +163,18 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, }.toSet val presentDomains = input.domains.map(_.idndef.name).toSet + // Check if the program contains any domains that define decreasing and bounded functions that do *not* have the expected names. + for (d <- input.domains) { + val name = d.idndef.name + val typeName = if (name.endsWith("WellFoundedOrder")) + Some(name.substring(0, name.length - 16)) + else + None + val wronglyConstrainedTypes = d.axioms.flatMap(a => constrainsWellfoundednessUnexpectedly(a, typeName)) + reporter.report(WarningsDuringTypechecking(wronglyConstrainedTypes.map(t => + TypecheckerWarning(s"Domain ${d.idndef.name} constrains well-foundedness functions for type ${t} and should be named WellFoundedOrder instead.", d.pos._1)))) + } + val importStmts = allClauseTypes flatMap { case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import ") case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import ") From 91fc42e9fc7df30101b6e55ea5c4769f7db1fea4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 20 Jul 2023 14:20:14 +0200 Subject: [PATCH 6/6] Deprecating rational well founded order, adding perm replacement, adapting autoimport and warning code --- src/main/resources/import/decreases/all.vpr | 2 +- src/main/resources/import/decreases/perm.vpr | 16 ++++++++++++++ .../termination/TerminationPlugin.scala | 22 +++++++++---------- 3 files changed, 28 insertions(+), 12 deletions(-) create mode 100644 src/main/resources/import/decreases/perm.vpr diff --git a/src/main/resources/import/decreases/all.vpr b/src/main/resources/import/decreases/all.vpr index dc6debd40..f3d471de5 100644 --- a/src/main/resources/import/decreases/all.vpr +++ b/src/main/resources/import/decreases/all.vpr @@ -5,7 +5,7 @@ import "bool.vpr" import "int.vpr" import "multiset.vpr" import "predicate_instance.vpr" -import "rational.vpr" +import "perm.vpr" import "ref.vpr" import "seq.vpr" import "set.vpr" \ No newline at end of file diff --git a/src/main/resources/import/decreases/perm.vpr b/src/main/resources/import/decreases/perm.vpr new file mode 100644 index 000000000..050729145 --- /dev/null +++ b/src/main/resources/import/decreases/perm.vpr @@ -0,0 +1,16 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +import "declaration.vpr" + +domain PermWellFoundedOrder{ + //Rationals + axiom rational_ax_dec{ + forall int1: Perm, int2: Perm :: {decreasing(int1, int2)} + (int1 <= int2 - 1/1) ==> decreasing(int1, int2) + } + axiom rational_ax_bound{ + forall int1: Perm :: {bounded(int1)} + int1 >= 0/1 ==> bounded(int1) + } +} \ No newline at end of file diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index ca17ad5e9..a03f9ca01 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -131,17 +131,17 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, return false if (wfTypeName.isEmpty) return true - val typeName = t match { - case PPrimitiv("Perm") => "Rational" - case PPrimitiv(n) => n - case PSeqType(_) => "Seq" - case PSetType(_) => "Set" - case PMultisetType(_) => "MultiSet" - case PMapType(_, _) => "Map" - case PDomainType(d, _) if d.name == "PredicateInstance" => "PredicateInstances" - case PDomainType(d, _) => d.name + val typeNames = t match { + case PPrimitiv("Perm") => Seq("Rational", "Perm") + case PPrimitiv(n) => Seq(n) + case PSeqType(_) => Seq("Seq") + case PSetType(_) => Seq("Set") + case PMultisetType(_) => Seq("MultiSet") + case PMapType(_, _) => Seq("Map") + case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances") + case PDomainType(d, _) => Seq(d.name) } - !wfTypeName.contains(typeName) + !typeNames.exists(tn => wfTypeName.contains(tn)) } ax.exp.shallowCollect{ @@ -179,7 +179,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import ") case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import ") case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import ") - case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") => Some("import ") + case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") && !presentDomains.contains("PermWellFoundedOrder") => Some("import ") case PMultisetType(_) if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import ") case PSeqType(_) if !presentDomains.contains("SeqWellFoundedOrder") => Some("import ") case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import ")