add immutable

Author: CatarinaGamboa

latte/src/main/java/context/PermissionEnvironment.java

@@ -117,6 +117,11 @@ public boolean usePermissionAs(SymbolicValue v, UniquenessAnnotation vPerm, Uniq
                     return true;
                 }
                 break;
+            case IMMUTABLE:
+                if (vPerm.isGreaterEqualThan(Uniqueness.IMMUTABLE)){
+                    return true;
+                }
+                break;
             case SHARED:
                 if (vPerm.annotationEquals(Uniqueness.SHARED) || vPerm.annotationEquals(Uniqueness.FREE)){
                     add(v, new UniquenessAnnotation(Uniqueness.SHARED));

latte/src/main/java/context/Uniqueness.java

@@ -5,7 +5,8 @@ public enum Uniqueness {
     SHARED (2),
     UNIQUE (3),
     BORROWED (4),
-    FREE (5);
+    IMMUTABLE(5),
+    FREE (6);
     // ALIAS (6),
 
     private final int order;

latte/src/main/java/context/UniquenessAnnotation.java

@@ -4,6 +4,8 @@
 
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtTypedElement;
+import spoon.reflect.reference.CtTypeReference;
 
 /**
  * Matched the annotation to the uniqueness enum type type
@@ -30,9 +32,19 @@ else if (an.contentEquals("specification.Free")) {
 			 }
 
 	    }
+		if (element instanceof CtTypedElement){ // TODO: change for typed param here when changing java version
+			CtTypedElement<?> typed = (CtTypedElement<?>) element;
+			CtTypeReference<?> typeRef = typed.getType();  
+			if(typeRef != null && typeRef.isPrimitive())
+				this.annotation = Uniqueness.IMMUTABLE;                                                                           
+		}
 		if (annotation == null) this.annotation = Uniqueness.SHARED; //Default
 	}
 
+	public static UniquenessAnnotation forPrimitives() {
+		return new UniquenessAnnotation(Uniqueness.IMMUTABLE);
+	}
+
 	public UniquenessAnnotation(Uniqueness at) {	
 		annotation = at;
 	}
@@ -66,6 +78,10 @@ public boolean isBottom() {
 		return annotation.equals(Uniqueness.BOTTOM);
 	}
 
+	public boolean isImmutable() {
+		return annotation.equals(Uniqueness.IMMUTABLE);
+	}
+
 	public boolean isLessEqualThan(Uniqueness other) {
 		return annotation.isLessEqualThan(other);
 	}

latte/src/main/java/typechecking/LatteTypeChecker.java

@@ -665,15 +665,15 @@ public <T> void visitCtLiteral(CtLiteral<T> literal) {
 
 		super.visitCtLiteral(literal);
 
-		// Get a fresh symbolic value and add it to the environment with a shared default value
+		// Get a fresh symbolic value and add it to the environment with an immutable default value
 		SymbolicValue sv = symbEnv.getFresh();
-		UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.SHARED);
-		
+		UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.IMMUTABLE);
+
 		if (literal.getValue() == null)
 			ua = new UniquenessAnnotation(Uniqueness.FREE);  // its a null literal
 
 
-		// Add the symbolic value to the environment with a shared default value
+		// Add the symbolic value to the environment with an immutable default value
 		permEnv.add(sv, ua);
 
 		// Store the symbolic value in metadata

latte/src/test/examples/PQNode.java

@@ -0,0 +1,31 @@
+package examples;
+
+import specification.Free;
+import specification.Unique;
+
+
+class PQNode {
+    // @Refinement("min(this) == value")
+    PQNode(int value, @Free PQNode next) {
+        this.value = value;
+        this.next = next;
+    }
+
+    int value;
+
+    //@Refinement("this.next == null || min(this.next) < this.value")
+    @Unique PQNode next;
+
+    // @Refinement(@Borrowed PQNode this, "min(this) <= v")
+    void insert(int v) {
+        if (v < this.value) {
+            PQNode nxt = this.next;
+            this.next = null;
+            PQNode newNode = new PQNode(this.value, nxt);
+            this.value = v; 
+            this.next = newNode; // note: if we swap this with the statement above, the refinement is briefly violated
+        } else {
+            next.insert(v);
+        }
+    }
+}

latte/src/test/java/AppTest.java

@@ -45,7 +45,8 @@ private static Stream<Arguments> provideCorrectTestCases() {
             Arguments.of("src/test/examples/MyNodeIfNoElse.java"),
             Arguments.of("src/test/examples/MyNodeIfPermissionCheck.java"),
             Arguments.of("src/test/examples/MyNodeInvocationIf.java"),
-            Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java")
+            Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java"),
+            Arguments.of("src/test/examples/PQNode.java")
         );
     }