Fix purity classification of composite literals (#768)

* Fix pure classification of composite literals

* fix tests

* fix failing test

* add case for ghost slice

* implement feedback from PR review

* use unapply

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

@@ -689,7 +689,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/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/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/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/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") {