Merge pull request #710 from viperproject/meilers_decreases_autoimport

Auto-including well-foundedness functions and axioms when they are used

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"

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)}

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)
+    }
+}

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 semantic 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
+    }
+  }
+}

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, WarningsDuringTypechecking}
 
 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: Seq[PDecreasesClause] = Seq.empty
+
   /**
    * Keyword used to define decreases clauses
    */
@@ -93,7 +97,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)
@@ -104,6 +113,126 @@ 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 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)
+      }
+      !typeNames.exists(tn => wfTypeName.contains(tn))
+    }
+
+    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(())
+      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
+
+    // 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 <Type>WellFoundedOrder instead.", d.pos._1))))
+    }
+
+    val importStmts = allClauseTypes flatMap {
+      case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
+      case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")
+      case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import <decreases/bool.vpr>")
+      case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") && !presentDomains.contains("PermWellFoundedOrder") => Some("import <decreases/perm.vpr>")
+      case PMultisetType(_) if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import <decreases/multiset.vpr>")
+      case PSeqType(_) if !presentDomains.contains("SeqWellFoundedOrder") => Some("import <decreases/seq.vpr>")
+      case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import <decreases/set.vpr>")
+      case PPredicateType() if !presentDomains.contains("PredicateInstancesWellFoundedOrder") =>
+        Some("import <decreases/predicate_instance.vpr>")
+      case _ if !presentDomains.contains("WellFoundedOrder") => Some("import <decreases/declaration.vpr>")
+      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

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 <decreases/int.vpr>
-import <decreases/predicate_instance.vpr>
 
 function factorialPure(n: Int): Int
     decreases // wrong termination measure

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 <decreases/int.vpr>
 
 domain list {
 

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 <decreases/all.vpr>
+import <decreases/multiset.vpr>
 
 //Example decreasing Int
 function fact(x:Int): Int

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)
+}

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 <decreases/int.vpr>
 
 function mc(n:Int): Int
 decreases 100-n

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 <decreases/declaration.vpr>
 
 field f: Int