Fix issue 943 (#947)

* add bug witness

* add fix

* fix wrong stub in the std lib

* Update src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

Author: jcp19

src/main/resources/stubs/net/ip.gobra

@@ -143,7 +143,7 @@ func (ip IP) To4() (res IP) {
 }
 
 pure
-preserves forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/100000)
+requires forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])
 decreases _
 func isZeros(s []byte) bool
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -462,8 +462,11 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case _: PUnfolding => true
       case _: PLet => true // the well-definedness check makes sure that both sub-expressions are pure.
       case _: POld | _: PLabeledOld | _: PBefore => true
-      case _: PForall => true
-      case _: PExists => true
+      case f: PForall => go(f.body)
+      case e: PExists =>
+        // The type checker currently enforces that all existential quantifiers must be strongly pure, so we wouldn't need to recurse here.
+        // Nonetheless, this implementation is safer in case that ever changes.
+        go(e.body)
 
       case PConditional(cond, thn, els) => Seq(cond, thn, els).forall(go)
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -52,11 +52,22 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
       isSingleResultArg(member) ++
         isSinglePureReturnExpr(member) ++
         isPurePostcondition(member.spec) ++
+        pureMembersCannotHavePreserves(member.spec) ++
         nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
 
+  // Preserves clauses are unnecessary in pure functions. Any condition that holds on entry is guaranteed to
+  // hold on exit, thus it is redundant to make properties both pre- and postconditions.
+  private[typing] def pureMembersCannotHavePreserves(member: PFunctionSpec): Messages = {
+    assert(member.isPure)
+    member.preserves flatMap { c =>
+      error(c, "Pure functions and pure methods cannot have preserves clauses." +
+        "Considering replacing this preserves clause with a precondition.")
+    }
+  }
+
   private[typing] def wellDefIfPureMethodImplementationProof(implProof: PMethodImplementationProof): Messages = {
     if (implProof.isPure) {
       isSinglePureReturnExpr(implProof) // all other checks are taken care of by super implementation
@@ -68,6 +79,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
       isSingleResultArg(member) ++
         isSinglePureReturnExpr(member) ++
         isPurePostcondition(member.spec) ++
+        pureMembersCannotHavePreserves(member.spec) ++
         nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages

src/test/resources/regressions/issues/000943.gobra

@@ -0,0 +1,24 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000943
+
+//:: ExpectedOutput(type_error)
+preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i])
+decreases
+pure func test1(b []int) bool
+
+//:: ExpectedOutput(type_error)
+ensures forall i int :: 0 <= i && i < len(b) ==> acc(&b[i])
+decreases
+pure func test2(b []int) bool
+
+// Preserves clauses are always unnecessary in pure functions.
+// One should always prefer writing 'requires A' over 'preserves A',
+// as preconditions of pure functions are guaranteed to hold after the
+// call anyway. Gobra now actively rejects the use of preserves clauses
+// in pure functions.
+//:: ExpectedOutput(type_error)
+preserves true
+decreases
+pure func test3(b []int) bool