Added transitivity axiom, added tests

src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

@@ -40,10 +40,6 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
         config.plugin.toOption.getOrElse("").split(":").contains("viper.silver.plugin.standard.termination.TerminationPlugin"))
   }
 
-  private def generateWellFoundednessAxioms(prog: Program): Boolean = {
-    isTerminationPluginActive && prog.domainsByName.contains("WellFoundedOrder")
-  }
-
   def adtDerivingFunc[$: P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) }
 
   override def beforeParse(input: String, isImported: Boolean): String = {
@@ -141,7 +137,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     if (deactivated) {
       return input
     }
-    new AdtEncoder(input).encode(generateWellFoundednessAxioms(input))
+    new AdtEncoder(input).encode(isTerminationPluginActive)
   }
 
 }

src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala

@@ -32,13 +32,18 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     *
     * @return The encoded program.
     */
-  def encode(generateWellFoundedness: Boolean): Program = {
+  def encode(isTerminationPluginActive: Boolean): Program = {
+    def generateWellFoundedness(a: Adt) =  {
+      isTerminationPluginActive &&
+        program.domainsByName.contains(getWellFoundedOrderDeclarationDomainName) &&
+        !program.domainsByName.contains(getWellFoundedDomainName(a.name))
+    }
 
     // In a first step encode all adt top level declarations and constructor calls
     var newProgram: Program = StrategyBuilder.Slim[Node]({
       case p@Program(domains, fields, functions, predicates, methods, extensions) =>
         val remainingExtensions = extensions filter { case _: Adt => false; case _ => true }
-        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, generateWellFoundedness) }
+        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, generateWellFoundedness(a)) }
         val encodedAdtsAsDomains: Seq[Domain] = tmp.flatten
         Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT)
       case aca: AdtConstructorApp => encodeAdtConstructorApp(aca)
@@ -92,7 +97,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         val newAdtDomain = domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
 
         if (generateWellFoundedness) {
-          val decreasesAxioms = constructors map generateDecreasesAxiom(domain)
+          val decreasesAxioms = (constructors map generateDecreasesAxiom(domain)) :+ generateDecreasesTransitivityAxiom(domain)
           val wellFoundedDomain = Domain(getWellFoundedDomainName(domain.name), Seq(), decreasesAxioms, domain.typVars)(adt.pos, adt.info, adt.errT)
           Seq(newAdtDomain, wellFoundedDomain)
         }else {
@@ -436,7 +441,31 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
   }
 
-  //private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {}
+  private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {
+    val dt = DomainType(domain, defaultTypeVarsFromDomain(domain))
+    val v1 = LocalVarDecl("v1", dt)()
+    val v2 = LocalVarDecl("v2", dt)()
+    val v3 = LocalVarDecl("v3", dt)()
+    val decreases12 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v1.localVar, v2.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val decreases23 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v2.localVar, v3.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val decreases13 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v1.localVar, v3.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val trigger = Trigger(Seq(decreases12, decreases23))(domain.pos, domain.info, domain.errT)
+    val body = Implies(And(decreases12, decreases23)(domain.pos, domain.info, domain.errT), decreases13)(domain.pos, domain.info, domain.errT)
+    val forall = Forall(Seq(v1, v2, v3), Seq(trigger), body)()
+    AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
+  }
 
   private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")

src/test/resources/adt/termination_1.vpr

@@ -0,0 +1,105 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}
+
+////////////////////////
+
+adt IntList {
+    INil()
+    ICons(ivalue: Int, itail: IntList)
+}
+
+function ilen(l: IntList): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isINil ? 0 : 1 + ilen(l.itail)
+}
+
+function ilen2(l: IntList): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isINil ? 0 : (l.itail.isINil ? 1 : 2 + ilen2(l.itail.itail))
+}
+
+function ilenBad(l: IntList, v: Int): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ ilenBad(ICons(v, INil()), v)
+}
+
+////////////////////////
+
+// non-recursive data type with two type variables
+adt Pair[T, V] {
+    pair(fst: T, snd: V)
+}
+
+function stupidFunc(p: Pair[Int, Val]): Val
+  decreases p
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  stupidFunc(p)
+}
+
+// two type variables
+adt DList[V, T] {
+    DNil()
+    DCons(dvalue1: V, dvalue2: T, dtail: DList[V, T])
+}
+
+function dlen(l: DList[Int, Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isDNil ? 0 : 1 + dlen(l.dtail)
+}
+
+function dlenBad(l: DList[Int, Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isDNil ? 0 : 1 + dlenBad(l)
+}
+

src/test/resources/adt/termination_2.vpr

@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// Part of termination_1.vpr, but with the WellFoundedness domain already there.
+import <decreases/declaration.vpr>
+
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}

src/test/resources/adt/termination_3.vpr

@@ -0,0 +1,51 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// Part of termination_1.vpr, but with the WellFoundedness domain already there and a custom domain for
+// the list well founded order.
+import <decreases/declaration.vpr>
+
+domain ListWellFoundedOrder[W] {
+    // Domain already being present will prevent auto-generation of axioms.
+    // Thus, we should not be able to prove termination based on List measures here.
+}
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}

src/test/resources/all/issues/silicon/0751.vpr

@@ -1,12 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 domain $domain$to_int  {
 
   function to_int(to_int1: Perm): Int interpretation "to_int"
 }
 
 function round(x: Perm): Perm
   decreases
+  ensures x == 3/1 ==> result == 3/2
   //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures result == to_int(x) / 1
 {
-  to_int(x + (1/2)) / 1
+  to_int(x) / 2
 }

src/test/resources/termination/functions/basic/preventAutoImport.vpr

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+domain IntWellFoundedOrder{
+	// Domain already being present will prevent auto-import of the default domain.
+	// Thus, we have no defined order for type Int and proofs should fail.
+}
+
+//Example decreasing Int
+function fact(x:Int): Int
+  decreases x
+  requires x>=0
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    x==0 ? 1 : x*fact(x-1)
+}