Merge #548

548: Improving the Import of Termination Axioms r=ArquintL a=ArquintL

This PR optimizes the import of axioms for termination measures to only import those that are actually needed based on the type of termination measure tuples.

Furthermore, this PR sorts the Viper members reported by `GeneratedViperMessage`

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

src/main/scala/viper/gobra/reporting/Message.scala

@@ -166,7 +166,7 @@ case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAs
   override val name: String = s"generated_viper_message"
 
   override def toString: String = s"generated_viper_message(" +
-    s"taskName=$taskName"
+    s"taskName=$taskName" +
     s"files=$inputs, " +
     s"vprFormated=$vprAstFormatted)"
 

src/main/scala/viper/gobra/translator/Translator.scala

@@ -15,6 +15,8 @@ import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
 import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.{ast => vpr}
 
 object Translator {
 
@@ -37,8 +39,34 @@ object Translator {
       case (t, transformer) => transformer.transform(t)
     }
 
-    config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => transformedTask.program, () => transformedTask.backtrack)
+    config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => sortAst(transformedTask.program), () => transformedTask.backtrack)
     transformedTask
   }
 
+  /**
+    * sorts AST members alphabetically to ease the comparison of (similar) Viper ASTs
+    */
+  def sortAst(program: vpr.Program): vpr.Program = {
+    lazy val memberOrdering: Ordering[vpr.Member] = Ordering.by(_.name)
+    implicit lazy val domainFnOrdering: Ordering[vpr.DomainFunc] = Ordering.by(_.name)
+    implicit lazy val domainAxOrdering: Ordering[vpr.DomainAxiom] = Ordering.by(FastPrettyPrinter.pretty(_))
+
+    def sortDomain(domain: vpr.Domain): vpr.Domain = {
+      vpr.Domain(
+        domain.name,
+        domain.functions.sorted,
+        domain.axioms.sorted,
+        domain.typVars
+      )(domain.pos, domain.info, domain.errT)
+    }
+
+    vpr.Program(
+      program.domains.map(sortDomain).sorted(memberOrdering),
+      program.fields.sorted(memberOrdering),
+      program.functions.sorted(memberOrdering),
+      program.predicates.sorted(memberOrdering),
+      program.methods.sorted(memberOrdering),
+      program.extensions.sorted(memberOrdering),
+    )(program.pos, program.info, program.errT)
+  }
 }

src/main/scala/viper/gobra/translator/transformers/TerminationTransformer.scala

@@ -6,13 +6,13 @@
 
 package viper.gobra.translator.transformers
 import java.nio.file.Path
-
 import viper.gobra.backend.BackendVerifier
 import viper.gobra.util.Violation
 import viper.silicon.Silicon
 import viper.silver.{ast => vpr}
 import viper.silver.frontend.{DefaultStates, ViperAstProvider}
-import viper.silver.plugin.standard.termination.TerminationPlugin
+import viper.silver.plugin.standard.predicateinstance.PredicateInstance.PredicateInstanceDomainName
+import viper.silver.plugin.standard.termination.{DecreasesTuple, TerminationPlugin}
 import viper.silver.reporter.{NoopReporter, Reporter}
 import viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin
 
@@ -26,9 +26,33 @@ class TerminationTransformer extends ViperTransformer {
     // constructs a separate Viper program (as a string) that should be parsed
     // after parsing this separate Viper program, the resulting AST is combined with `task`
 
+    val allImport = "decreases/all.vpr"
+    def type2Import(typ: vpr.Type): String = typ match {
+      case vpr.Bool => "decreases/bool.vpr"
+      case vpr.Int => "decreases/int.vpr"
+      case vpr.MultisetType(_) => "decreases/multiset.vpr"
+      case vpr.Perm => "decreases/rational.vpr"
+      case vpr.Ref => "decreases/ref.vpr"
+      case vpr.SeqType(_) => "decreases/seq.vpr"
+      case vpr.SetType(_) => "decreases/set.vpr"
+      case vpr.DomainType(name, _) if name == PredicateInstanceDomainName => "decreases/predicate_instance.vpr"
+      case _ => allImport // fallback
+    }
+
+    // find the types of all expressions used as decreases measues
+    val measureTypes = task.program.deepCollect {
+      case DecreasesTuple(tupleExpressions, _) => tupleExpressions.map(_.typ)
+    }.flatten.distinct
+    // map these types to the respective files that should be imported
+    val imports = measureTypes
+      .map(type2Import)
+      .distinct
+    // if `allImport` is in the list of files that should be imported, we can ignore all others and instead only import
+    // `allImport`
+    val importsAll = imports.contains(allImport)
     /** list of Viper standard imports that should be parsed */
-    val imports = Seq("decreases/all.vpr")
-    val progWithImports = imports.map(p => s"import <${p}>").mkString("\n")
+    val filteredImports = if (importsAll) Seq(allImport) else imports
+    val progWithImports = filteredImports.map(p => s"import <${p}>").mkString("\n")
     val vprProgram = parseVpr(progWithImports)
     combine(task, vprProgram)
   }