Merge pull request #698 from viperproject/meilers_allow_heapdep_func_calls

Allow calls of non-domain functions without preconditions from domain axioms

Author: marcoeilers

src/main/scala/viper/silver/parser/Resolver.scala

@@ -658,13 +658,13 @@ case class TypeChecker(names: NameAnalyser) {
                       pfa.function = fd
                       ensure(fd.formalArgs.size == args.size, pfa, "wrong number of arguments")
                       fd match {
-                        case PFunction(_, _, _, _, _, _) =>
+                        case PFunction(_, _, _, pres, _, _) =>
                           checkMember(fd) {
                             check(fd.typ)
                             fd.formalArgs foreach (a => check(a.typ))
                           }
-                          if (inAxiomScope(Some(pfa)))
-                            issueError(func, func.name + " is not a domain function")
+                          if (inAxiomScope(Some(pfa)) && pres.nonEmpty)
+                            issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom")
 
                         case pdf@PDomainFunction(_, _, _, _, _) =>
                           val domain = names.definition(curMember)(pdf.domainName).get.asInstanceOf[PDomain]

src/test/resources/all/domains/axiom_call_func.vpr

@@ -0,0 +1,23 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function interp(i: Int): Int
+{
+    i + 1
+}
+
+domain d {
+    function unint(i: Int): Int
+
+    axiom {
+        forall i: Int :: {unint(i)} unint(i) == interp(i) + 1
+    }
+}
+
+method huh()
+{
+  assert unint(4) == 6
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert unint(14) == 14
+}

src/test/resources/all/domains/axiom_call_func2.vpr

@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function interp(i: Int): Int
+  requires i > 5
+{
+    i + 1
+}
+
+domain d {
+    function unint(i: Int): Int
+
+    axiom {
+        //:: ExpectedOutput(typechecker.error)
+        forall i: Int :: {unint(i)} unint(i) == interp(i) + 1
+    }
+}

src/test/resources/all/domains/axiom_call_func3.vpr

@@ -0,0 +1,62 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function interp(i: Int): Int
+{
+    i + 1
+}
+
+function uninterp(i: Int): Int
+    ensures result == i + 4
+
+function heapDep(r: Ref): Int
+    requires acc(r.f)
+{
+    r.f + 2
+}
+
+function heapDep2(r: Ref): Int
+    requires acc(r.f)
+{
+    heapDep(r) + heapDepUnint(r) + 10
+}
+
+function heapDepUnint(r: Ref): Int
+    requires acc(r.f)
+    ensures result == r.f + 3
+
+domain d {
+    function dfunc(i: Int): Int
+
+    function dfunc2(i: Int): Int
+
+    axiom {
+        forall i: Int :: {dfunc(i)} dfunc(i) == interp(i) + 5
+    }
+
+    axiom {
+        forall i: Int :: {dfunc2(i)} dfunc2(i) == uninterp(i) + 7
+    }
+}
+
+method main()
+{
+  var x: Ref
+  x := new(f)
+  var y: Ref
+  y := new(f)
+
+  x.f := 20
+  y.f := 3
+  assert dfunc2(x.f) == 31
+  assert heapDep2(x) == 15 + 20 + 20
+
+  assert dfunc(x.f + 1) == 27
+  assert interp(34) == 35
+  assert heapDep(y) + dfunc2(x.f + 5) == 41
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert heapDepUnint(x) == 24
+}

src/test/resources/all/issues/silver/0238.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 // Test case 1
 domain A1 {
   axiom x1 {
@@ -26,7 +26,6 @@ function q2(s:Int) : Bool
 // Example 3
 domain A3 {
   axiom x3 {
-    //:: ExpectedOutput(typechecker.error)
     g3()
   }
 }
@@ -45,6 +44,7 @@ domain A4 {
 }
 
 function g4(): Bool
+  requires true
 
 // Example 5
 domain A5 {