Merges branch 'tmp-branch-for-#747-#755-#766' into 'ghost-field'

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -691,7 +691,7 @@ case class PImplicitSizeArrayType(elem: PType) extends PLiteralType
 
 case class PSliceType(elem: PType) extends PTypeLit with PLiteralType
 
-case class PVariadicType(elem: PType) extends PTypeLit with PLiteralType
+case class PVariadicType(elem: PType) extends PTypeLit
 
 case class PMapType(key: PType, elem: PType) extends PTypeLit with PLiteralType
 

src/main/scala/viper/gobra/frontend/info/implementation/property/UnderlyingType.scala

@@ -19,6 +19,10 @@ trait UnderlyingType { this: TypeInfoImpl =>
     def unapply(t: Type): Option[Type] = Some(underlyingType(t))
   }
 
+  object UnderlyingPType {
+    def unapply(t: PType): Option[PType] = underlyingTypeP(t)
+  }
+
   lazy val underlyingType: Type => Type =
     attr[Type, Type] {
       case Single(DeclaredT(t: PTypeDecl, context: ExternalTypeInfo)) => underlyingType(context.symbType(t.right))
@@ -44,11 +48,13 @@ trait UnderlyingType { this: TypeInfoImpl =>
           case value : PType => Some(value, this)
           case _ => None
         }
+        case st.AdtClause(_, typeDecl, _) => Some((typeDecl.right, this))
         case _ => None // type not defined
       }
       case PDot(_, id) => entity(id) match {
         case st.NamedType(decl, _, ctx) => inCtx(ctx, decl.right)
         case st.TypeAlias(decl, _, ctx) => inCtx(ctx, decl.right)
+        case st.AdtClause(_, typeDecl, _) => Some((typeDecl.right, this))
         case _ => None // type not defined
       }
       case t => Some((t, this))

src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala

@@ -144,9 +144,9 @@ trait NameResolution {
       case _ => violation("PIdnUnk always has a parent")
     }
 
-  // technically, `isGhostDef` should consider for implementation proofs whether the method getting implemented is ghost
-  // however, since implementation proofs are syntactically restricted, we assume for now that definitions in all
-  // implementation proofs are non-ghost.
+  // `isGhostDef` returns true if a node is part of ghost code. However, implementation proofs are considered being
+  // non-ghost, independently of whether they are for a ghost or non-ghost method. Thus, implementation proofs for ghost
+  // and non-ghost methods are type-checked in the same way, which is unproblematic due to their syntactic restrictions.
   private[resolution] lazy val isGhostDef: PNode => Boolean = n => isEnclosingGhost(n)
 
   private[resolution] def serialize(id: PIdnNode): String = id.name

src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala

@@ -346,7 +346,7 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl =>
     val expectedResults = result.outs.flatMap(nameFromParam).map(t => PNamedOperand(PIdnUse(t)))
 
     def isExpectedAssignment(ass: PAssignment): Boolean = ass match {
-      case PAssignment(Vector(i: PInvoke), left) if isExpectedCall(i) && expectedResults == left => true
+      case PAssignment(Vector(i: PInvoke), left) => isExpectedCall(i) && expectedResults == left
       case _ => false
     }
 

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

@@ -466,8 +466,23 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case n: PIsComparable => asExpr(n.exp).forall(go)
 
       case PCompositeLit(typ, _) => typ match {
-        case _: PArrayType | _: PImplicitSizeArrayType => !strong
-        case _ => true
+        case _: PImplicitSizeArrayType => true
+        case UnderlyingPType(t: PLiteralType) => t match {
+          case g: PGhostLiteralType => g match {
+            case _: PGhostSliceType => false
+            case _: PAdtType | _: PDomainType | _: PMathematicalMapType |
+              _: PMultisetType | _: POptionType | _: PSequenceType | _: PSetType => true
+          }
+          case _: PArrayType | _: PStructType => true
+          case _: PMapType | _: PSliceType => false
+          case d@(_: PDot | _: PNamedOperand) =>
+            // UnderlyingPType should never return any of these types
+            violation(s"Unexpected underlying type $d")
+        }
+        case t =>
+          // the type system should already have rejected composite literals whose underlying type is not a valid
+          // literal type.
+          violation(s"Unexpected literal type $t")
       }
 
       case POptionNone(_) => true

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

@@ -142,15 +142,15 @@ trait GhostWellDef { this: TypeInfoImpl =>
 
     case e: PNew =>
       if (isEnclosingGhost(e)) {
-        Violation.violation(exprType(e).isInstanceOf[GhostPointerT], s"All memory allocated within ghost code must be located on the ghost heap")
+        Violation.violation(exprType(e).isInstanceOf[GhostPointerT], s"Cannot allocate non-ghost memory in ghost code.")
       } else {
-        Violation.violation(exprType(e).isInstanceOf[ActualPointerT], s"All memory allocated within actual code must be located on the actual heap")
+        Violation.violation(exprType(e).isInstanceOf[ActualPointerT], s"Cannot allocate ghost memory in non-ghost code.")
       }
       noMessages
 
     case e: PMake => (e, isEnclosingGhost(e)) match {
       case (PMake(_: PGhostSliceType, _), true)  => noMessages
-      case (_, true) => error(e, "Allocating memory within ghost code is forbidden")
+      case (_, true) => error(e, "Allocating memory with make within ghost code is forbidden")
       case (PMake(_, args), false) => error(
         e,
         "ghost error: make expressions may not contain ghost expressions",

src/test/resources/regressions/features/arrays/array-length-simple2.gobra

@@ -6,7 +6,7 @@ package pkg
 const N = 42
 
 func foo() {
-	var a [N]int
-  assert len(a) == N
-  assert len(a) == 42
+    var a [N]int
+    assert len(a) == N
+    assert len(a) == 42
 }

src/test/resources/regressions/features/arrays/array-literal-simple1.gobra

@@ -60,3 +60,10 @@ func test10() {
   assert [4]int { 0, 1, 42, 8 }[2] == 42
   assert forall i int :: 0 <= i && i < 4 ==> ([4]int { 0, 2, 4, 6 })[i] == i + i
 }
+
+pure
+decreases
+func test11() [3]int {
+    // pure functions may contain array literals
+    return [3]int{}
+}

src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-fail01.gobra

@@ -135,7 +135,14 @@ func (r Foo) ActualNonPointerReceiver() int {
 decreases
 preserves acc(r)
 //:: ExpectedOutput(type_error)
-func (r gpointer[Foo]) ActualGhostPointerReceiver() int { // ghostpointer is only allowed for ghost methods
+func (r gpointer[Foo]) ActualGhostPointerReceiver() int { // a receiver of type ghostpointer is only allowed for ghost methods
+    r.field = 0
+    return r.field
+}
+
+decreases
+preserves acc(r)
+func ActualMethodWithGhostPointerParam(ghost r gpointer[Foo]) (ghost res int) { // actual methods can take a ghostpointer as a ghost parameter
     r.field = 0
     return r.field
 }

src/test/resources/regressions/features/ghost_pointer/ghost-write-fail02.gobra

@@ -0,0 +1,39 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package GhostWriteFail02
+
+// this testcase checks that an actual method cannot be called within ghost code as this method might modify
+// non-ghost memory.
+
+decreases
+requires acc(x)
+func foo(x *int) {
+  *x = 0
+}
+
+ghost
+decreases
+requires acc(x)
+func bar(x *int) {
+  // the following two calls are type-checked in the same way as we are already in a ghost context.
+  // each call technically results in two type errors, i.e., (1) calling a non-ghost method in a ghost context and
+  // (2) assigning a ghost variable `x` to a non-ghost parameter.
+
+  //:: ExpectedOutput(type_error)
+  ghost foo(x)
+
+  //:: ExpectedOutput(type_error)
+  foo(x)
+}
+
+decreases
+requires acc(x)
+func bar2(x *int) {
+  // the following call fails because we call a non-ghost method in a ghost context:
+  //:: ExpectedOutput(type_error)
+  ghost foo(x)
+
+  // this is fine since we are in a non-ghost context:
+  foo(x)
+}

src/test/resources/regressions/features/interfaces/ghostnessOfImplementation-fail1.gobra

@@ -0,0 +1,65 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this test makes sure that a method's implementation has the same ghostness as specified in the interface
+
+package pkg
+
+type itfWithActualMethod interface {
+    decreases
+    actualMethod() int
+}
+
+type itfWithActualPureMethod interface {
+    decreases
+    pure actualPureMethod() int
+}
+
+type itfWithGhostMethod interface {
+    ghost
+    decreases
+    ghostMethod() int
+}
+
+type itfWithGhostPureMethod interface {
+    ghost
+    decreases
+    pure ghostPureMethod() int
+}
+
+type someImplementation struct {
+    value int
+}
+
+// checks that `someImplementation` is indeed considered an implementation of each interface, i.e., that the ghost
+// attribute in the interface and implementation is correctly handled.
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithActualMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithActualPureMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithGhostMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithGhostPureMethod
+
+ghost
+decreases
+func (impl *someImplementation) actualMethod() int {
+    return 42
+}
+
+ghost
+decreases
+pure func (impl *someImplementation) actualPureMethod() int {
+    return 42
+}
+
+decreases
+func (impl *someImplementation) ghostMethod() int {
+    return 42
+}
+
+decreases
+pure func (impl *someImplementation) ghostPureMethod() int {
+    return 42
+}

src/test/resources/regressions/features/maps/maps-fail1.gobra

@@ -30,3 +30,12 @@ func test4() {
 	//:: ExpectedOutput(type_error)
 	_ = map[int]int {1: 2, 1: 3}
 }
+
+// error: expected pure expression without permissions, but got map[int]int { }
+pure
+decreases
+func test5() map[int]int {
+    // pure functions may NOT contain map literals
+    //:: ExpectedOutput(type_error)
+    return map[int]int{}
+}

src/test/resources/regressions/features/maps/maps-simple1.gobra

@@ -73,7 +73,8 @@ func test8() {
 	m := map[string]int { "hello": 5, "bye": 3 }
 	v, ok := m["hello"]
 	assert ok && v == 5
-	assert len(map[int]int{}) == 0
+	e := map[int]int{}
+	assert len(e) == 0
 }
 
 func test9() {

src/test/resources/regressions/features/slices/slice-literal-simple1.gobra

@@ -11,15 +11,17 @@ func test1() {
 }
 
 func test2() {
-	s@ := [][]int{[]int{1}, []int{2}}
+  s@ := [][]int{[]int{1}, []int{2}}
   assert len(s) == 2
 }
 
 func test3() {
-  assert len([]int { 1, 2, 3 }) == 3
-  assert cap([]int { 4, 5 }[:]) == 2
-  assert len([]int { 1, 2, 3 }[:2]) == 2
-  assert cap([]int { 4, 5 }[1:]) == 1
+  oneTwoThree := []int { 1, 2, 3 }
+  fourFive := []int { 4, 5 }
+  assert len(oneTwoThree) == 3
+  assert cap(fourFive[:]) == 2
+  assert len(oneTwoThree[:2]) == 2
+  assert cap(fourFive[1:]) == 1
 }
 
 func test4() {

src/test/resources/regressions/features/slices/slice-type-fail1.gobra

@@ -7,4 +7,13 @@ package pkg
 //:: ExpectedOutput(type_error)
 requires s == t
 func foo(s []int, t []int) { 
+}
+
+// error: expected pure expression without permissions, but got []int { }
+pure
+decreases
+func f() []int {
+    // pure functions may NOT contain slice literals
+    //:: ExpectedOutput(type_error)
+    return []int{}
 }

src/test/resources/regressions/issues/000037.gobra → src/test/resources/regressions/issues/000037-1.gobra

@@ -8,12 +8,17 @@ type Rectangle struct {
 }
 
 ghost
+decreases
 pure func GetHeight(r Rectangle) (res int) {
     return r.Height
 }
 
 func main() {
+    someActualVariable := 42
     r := Rectangle{Width: 2, Height: 5}
     h := GetHeight(r)
     assert h == GetHeight(r) && h == 5
-}
+    // h is implicitly a ghost variable. Thus, the following assignment (to a non-ghost variable) should fail:
+    //:: ExpectedOutput(type_error)
+    someActualVariable = h
+}

src/test/resources/regressions/issues/000037-2.gobra

@@ -0,0 +1,29 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+ghost
+decreases x
+pure func more(x int) int {
+  return x <= 0 ? 1 : more(x - 2) + 3
+}
+
+ghost /* lemma */
+decreases x
+ensures x < more(x)
+func increasing(x int)
+
+// returning b (a ghost variable) is not allowed as this is an actual function
+//:: ExpectedOutput(type_error)
+func exampleLemmaUse(a int) int {
+  increasing(a)
+  b := more(a)
+  c := more(b)
+  if a < 1000 {
+    increasing(more(a))
+    assert 2 <= c - a
+  }
+  assert 2 <= c - a || 200 <= a
+  return b
+}

src/test/resources/regressions/issues/000129-2.gobra

@@ -4,7 +4,8 @@
 package pkg
 
 func issue () {
-  assert []int{4: 20, 1: 10}[2] == 0
+  s := []int{4: 20, 1: 10}
+  assert s[2] == 0
 }
 
 func extra1() {

src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala

@@ -2843,13 +2843,13 @@ class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside {
     assert (frontend.wellDefExpr(expr)().valid)
   }
 
-  test("TypeChecker: should not let an array literal be classified as pure") {
+  test("TypeChecker: should classify an array literal containing only integer literals as pure") {
     val expr = PLiteral.array(
       PBoolType(),
       Vector(PIntLit(1), PIntLit(2))
     )
 
-    assert (!frontend.isPureExpr(expr)())
+    assert (frontend.isPureExpr(expr)())
   }
 
   test("TypeChecker: should not let a simple array literal be classified as ghost if its inner type isn't ghost") {