Merge pull request #742 from viperproject/meilers_axiom_instantiation

Fixing Silicon issue #753

Author: marcoeilers

src/main/scala/viper/silver/ast/utility/DomainInstances.scala

@@ -168,10 +168,13 @@ object DomainInstances {
           case Some(ps) =>
             ps.flatMap(f = pair => {
               //            assert(dfa.funcname==pair._1.funcname)
-              val d2 = p.findDomain(pair._2.domainName)
+              val d2 = p.findDomain(dfa.domainName)
               val tvs = d2.typVars
-              tryUnifyWithDefault(tvs, tvs.map(pair._1.typVarMap.getOrElse(_, Program.defaultType)), tvs.map(dfa.typVarMap.getOrElse(_, Program.defaultType))) match {
-                case Some(ts) => Set[Type](DomainType(pair._2.domainName, ts)(tvs))
+              val axDom = p.findDomain(pair._2.domainName)
+              val axTvs = axDom.typVars
+              tryUnifyWithDefault(axTvs, tvs.map(pair._1.typVarMap.get(_).get), tvs.map(dfa.typVarMap.get(_).get)) match {
+                case Some(ts) =>
+                  Set[Type](DomainType(pair._2.domainName, ts)(axTvs))
                 case None => Set[Type]()
               }
             }).toSet

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

@@ -0,0 +1,17 @@
+// 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) / 2
+}

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

@@ -0,0 +1,88 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Val  {}
+
+domain WellFoundedOrder[T]  {
+
+  function decreasing(arg1: T, arg2: T): Bool
+
+  function bounded(arg1: T): Bool
+}
+
+domain List[V]  {
+
+  function Nil(): List[V]
+
+  function Cons(value: V, tail: List[V]): List[V]
+
+  function get_List_value(t: List[V]): V
+
+  function get_List_tail(t: List[V]): List[V]
+
+  function List_tag(t: List[V]): Int
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      value == (get_List_value((Cons(value, tail): List[V])): V))
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      tail == (get_List_tail((Cons(value, tail): List[V])): List[V]))
+  }
+
+  axiom {
+    (List_tag((Nil(): List[V])): Int) == 1
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      (List_tag((Cons(value, tail): List[V])): Int) == 0)
+  }
+
+  axiom {
+    (forall t: List[V] ::
+      { (List_tag(t): Int) }
+      { (get_List_value(t): V) }
+      { (get_List_tail(t): List[V]) }
+      (List_tag(t) == 1 && t == (Nil(): List[V])) ||
+      (List_tag(t) == 0 && exists v: V, l: List[V] :: t == Cons(v, l))
+      //(t == (Cons((get_List_value(t): V), (get_List_tail(t): List[V])): List[V]))
+      )
+  }
+}
+
+domain ListWellFoundedOrder[V]  {
+
+  axiom {
+    (bounded((Nil(): List[V])): Bool)
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      (bounded((Cons(value, tail): List[V])): Bool) &&
+      (decreasing(tail, (Cons(value, tail): List[V])): Bool))
+  }
+}
+
+// decreases l
+function len(l: List[Val]): Int
+  ensures result >= 0
+{
+  ((List_tag(l): Int) == 1 ? 0 : 1 + len((get_List_tail(l): List[Val])))
+}
+
+// decreases l
+method len_termination_proof(l: List[Val])
+{
+  if ((List_tag(l): Int) == 1) {
+  } else {
+    assert (decreasing((get_List_tail(l): List[Val]), old(l)): Bool) &&
+      (bounded(old(l)): Bool)}
+}

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

@@ -85,7 +85,6 @@ function numberOfUsers(seq:Seq[Bool]): Int
 decreases seq
 {
     |seq| == 0 ? 0 :
-    //:: UnexpectedOutput(termination.failed:tuple.false, /silicon/issue/300/)
         seq[0] ? 1 + numberOfUsers(seq[1..]) : numberOfUsers(seq[1..])
 }