Skip to content

Commit

Permalink
Rename ReceiverDependantMutable to ReceiverDependentMutable
Browse files Browse the repository at this point in the history
  • Loading branch information
Ao-senXiong committed May 31, 2024
1 parent 5c5a016 commit 1104d9e
Show file tree
Hide file tree
Showing 81 changed files with 482 additions and 476 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
import qual.Mutable;
import qual.PolyMutable;
import qual.Readonly;
import qual.ReceiverDependantMutable;
import qual.ReceiverDependentMutable;

import static pico.typecheck.PICOAnnotationMirrorHolder.*;

Expand Down Expand Up @@ -80,7 +80,7 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
PolyMutable.class,
Readonly.class,
Mutable.class,
ReceiverDependantMutable.class,
ReceiverDependentMutable.class,
Immutable.class,
Bottom.class));
}
Expand Down
10 changes: 5 additions & 5 deletions src/main/java/pico/inference/PICOInferenceValidator.java
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ public PICOInferenceValidator(BaseTypeChecker checker, InferenceVisitor<?, ?> vi

@Override
public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) {
checkStaticReceiverDependantMutableError(type, tree);
checkStaticReceiverDependentMutableError(type, tree);
checkImplicitlyImmutableTypeError(type, tree);
checkOnlyOneAssignabilityModifierOnField(tree);
// AnnotatedDeclaredType defaultType =
Expand Down Expand Up @@ -70,7 +70,7 @@ protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedT

@Override
public Void visitArray(AnnotatedArrayType type, Tree tree) {
checkStaticReceiverDependantMutableError(type, tree);
checkStaticReceiverDependentMutableError(type, tree);
return super.visitArray(type, tree);
}

Expand Down Expand Up @@ -114,15 +114,15 @@ protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(AnnotatedTypeMirror
return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree);
}

private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) {
private void checkStaticReceiverDependentMutableError(AnnotatedTypeMirror type, Tree tree) {
// Static inner class is considered within the static scope.
// Added condition to ensure not class decl.
if (PICOTypeUtil.inStaticScope(visitor.getCurrentPath()) && !type.isDeclaration()) {
if (infer) {
((PICOInferenceVisitor)visitor).mainIsNot(type, RECEIVER_DEPENDANT_MUTABLE, "static.receiverdependantmutable.forbidden", tree);
((PICOInferenceVisitor)visitor).mainIsNot(type, RECEIVER_DEPENDANT_MUTABLE, "static.receiverDependentMutable.forbidden", tree);
} else {
if (type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) {
reportValidityResult("static.receiverdependantmutable.forbidden", type, tree);
reportValidityResult("static.receiverDependentMutable.forbidden", type, tree);
}
}
// TODO set isValid or move to visitor
Expand Down
12 changes: 6 additions & 6 deletions src/main/java/pico/inference/PICOInferenceVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@
import pico.common.ExtendedViewpointAdapter;
import pico.common.ViewpointAdapterGettable;
import pico.common.PICOTypeUtil;
import qual.ReceiverDependantMutable;
import qual.ReceiverDependentMutable;

import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.Element;
Expand Down Expand Up @@ -203,14 +203,14 @@ private void addMutableImmutableRdmIncompatibleConstraints(AnnotatedDeclaredType
Constraint isMutable = constraintManager.createEqualityConstraint(declSlot, mutable);
Constraint notImmutable = constraintManager.createInequalityConstraint(useSlot, immutable);
constraintManager.addImplicationConstraint(Arrays.asList(isMutable), notImmutable);
// declType == @Mutable -> useType != @ReceiverDependantMutable
// declType == @Mutable -> useType != @ReceiverDependentMutable
Constraint notRDM = constraintManager.createInequalityConstraint(useSlot, rdm);
constraintManager.addImplicationConstraint(Arrays.asList(isMutable), notRDM);
// declType == @Immutable -> useType != @Mutable
Constraint isImmutable = constraintManager.createEqualityConstraint(declSlot, immutable);
Constraint notMutable = constraintManager.createInequalityConstraint(useSlot, mutable);
constraintManager.addImplicationConstraint(Arrays.asList(isImmutable), notMutable);
// declType == @Immutable -> useType != @ReceiverDependantMutable
// declType == @Immutable -> useType != @ReceiverDependentMutable
constraintManager.addImplicationConstraint(Arrays.asList(isImmutable), notRDM);
}

Expand Down Expand Up @@ -517,7 +517,7 @@ public Void visitMethod(MethodTree node, Void p) {
Slot rdmSlot = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE);
Constraint inequalityConstraint = constraintManager.createInequalityConstraint(boundSlot, rdmSlot);
Constraint subtypeConstraint = constraintManager.createSubtypeConstraint(consRetSlot, boundSlot);
// bound != @ReceiverDependantMutable -> consRet <: bound
// bound != @ReceiverDependentMutable -> consRet <: bound
constraintManager.addImplicationConstraint(Collections.singletonList(inequalityConstraint), subtypeConstraint);
// TODO Add typecheck for this?
}
Expand Down Expand Up @@ -779,7 +779,7 @@ private void checkAssignableField(ExpressionTree node, ExpressionTree variable,
private void checkInitializingObject(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { // todo: haifeng we only need to do this in one statement
// TODO rm infer after mainIsNot returns bool
if (infer) {
// Can be anything from mutable, immutable or receiverdependantmutable
// Can be anything from mutable, immutable or ReceiverDependentMutable
mainIsNot(receiverType, READONLY, "illegal.field.write", node);
} else {
if (receiverType.hasAnnotation(READONLY)) {
Expand Down Expand Up @@ -886,7 +886,7 @@ public Void visitNewArray(NewArrayTree node, Void p) {
private void checkNewInstanceCreation(Tree node) {
AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node);
if (infer) {
// Ensure only @Mutable/@Immutable/@ReceiverDependantMutable are inferred on new instance creation
// Ensure only @Mutable/@Immutable/@ReceiverDependentMutable are inferred on new instance creation
mainIsNoneOf(type, new AnnotationMirror[]{READONLY, BOTTOM}, "pico.new.invalid", node);
} else {
if (!(type.hasAnnotation(IMMUTABLE) || type.hasAnnotation(MUTABLE) ||
Expand Down
110 changes: 55 additions & 55 deletions src/main/java/pico/inference/jdk.astub
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
import qual.Mutable;
import qual.Immutable;
import qual.ReceiverDependantMutable;
import qual.ReceiverDependentMutable;
import qual.Readonly;
import qual.ObjectIdentityMethod;
import java.util.Collection;

package java.lang;

@ReceiverDependantMutable
@ReceiverDependentMutable
class Object {
@ReceiverDependantMutable Object();
@ReceiverDependentMutable Object();
Class<?> getClass(@Readonly Object this);
String toString(@Readonly Object this);
int hashCode(@Readonly Object this);
boolean equals(@Readonly Object this, @Readonly Object var1);
@ReceiverDependantMutable Object clone(@ReceiverDependantMutable Object this);
@ReceiverDependentMutable Object clone(@ReceiverDependentMutable Object this);
@ObjectIdentityMethod
final native Class<?> getClass();
}
Expand Down Expand Up @@ -50,17 +50,17 @@ class StringBuffer {
int lastIndexOf(@Readonly StringBuffer this, String str, int fromIndex);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class Throwable {
String getMessage(@ReceiverDependantMutable Throwable this);
String getLocalizedMessage(@ReceiverDependantMutable Throwable this);
Throwable getCause(@ReceiverDependantMutable Throwable this);
void printStackTrace(@ReceiverDependantMutable Throwable this);
void printStackTrace(@ReceiverDependantMutable Throwable this, PrintStream var1);
void printStackTrace(@ReceiverDependantMutable Throwable this, Throwable.PrintStreamOrWriter var1);
String getMessage(@ReceiverDependentMutable Throwable this);
String getLocalizedMessage(@ReceiverDependentMutable Throwable this);
Throwable getCause(@ReceiverDependentMutable Throwable this);
void printStackTrace(@ReceiverDependentMutable Throwable this);
void printStackTrace(@ReceiverDependentMutable Throwable this, PrintStream var1);
void printStackTrace(@ReceiverDependentMutable Throwable this, Throwable.PrintStreamOrWriter var1);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface CharSequence {
int length(@Readonly CharSequence this);
char charAt(@Readonly CharSequence this, int index);
Expand All @@ -69,13 +69,13 @@ interface CharSequence {
public default IntStream codePoints(@Readonly CharSequence this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class RuntimeException {
@ReceiverDependantMutable RuntimeException(@Readonly Throwable var1);
@ReceiverDependantMutable RuntimeException(String var1, @Readonly Throwable var2, boolean var3, boolean var4);
@ReceiverDependentMutable RuntimeException(@Readonly Throwable var1);
@ReceiverDependentMutable RuntimeException(String var1, @Readonly Throwable var2, boolean var3, boolean var4);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class IndexOutOfBoundsException {}

@Immutable
Expand All @@ -84,42 +84,42 @@ class Enum<E extends @Immutable Enum<E>> {
int ordinal(@Immutable Enum<E> this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Cloneable {}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Comparable<T> {}

package java.util;

@ReceiverDependantMutable
@ReceiverDependentMutable
class Properties {
@Readonly Object put(@Immutable Object key, @Readonly Object value);
}

interface Iterator<E extends @Readonly Object> {}

@ReceiverDependantMutable
@ReceiverDependentMutable
class Date {
@ReceiverDependantMutable Date();
@ReceiverDependantMutable Date(long var1);
int getHours(@ReceiverDependantMutable Date this);
@ReceiverDependentMutable Date();
@ReceiverDependentMutable Date(long var1);
int getHours(@ReceiverDependentMutable Date this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Collection<E> {
boolean contains(@Readonly Collection<E> this, @Readonly Object o);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
public abstract class AbstractCollection<E> implements Collection<E> {
public abstract int size(@Readonly AbstractCollection this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class ArrayList<E> {
@ReceiverDependantMutable ArrayList();
@ReceiverDependantMutable ArrayList(@Readonly Collection<? extends E> var1);
@ReceiverDependentMutable ArrayList();
@ReceiverDependentMutable ArrayList(@Readonly Collection<? extends E> var1);
boolean add(E var1);
boolean addAll(@Readonly Collection<? extends E> c);
E get(@Readonly ArrayList<E> this, int index);
Expand All @@ -131,7 +131,7 @@ class ArrayList<E> {
Iterator<E> iterator(@Readonly ArrayList<E> this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface List<E> {
int size(@Readonly List<E> this);
boolean isEmpty(@Readonly List<E> this);
Expand All @@ -151,13 +151,13 @@ interface List<E> {
ListIterator<E> listIterator(@Readonly List<E> this, int index);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class AbstractList<E> {
@ReceiverDependantMutable AbstractList();
@ReceiverDependentMutable AbstractList();
void add(@Mutable AbstractList<E> this, int var1, E var2);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Set<E> {
int size(@Readonly Set<E> this);
boolean isEmpty(@Readonly Set<E> this);
Expand All @@ -170,15 +170,15 @@ interface Set<E> {
boolean addAll(@Readonly Collection<? extends E> c);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class HashSet<E> {
@ReceiverDependantMutable HashSet();
@ReceiverDependantMutable HashSet(@Readonly Collection<? extends E> var1);
@ReceiverDependentMutable HashSet();
@ReceiverDependentMutable HashSet(@Readonly Collection<? extends E> var1);
boolean contains(@Readonly HashSet<E> this, @Readonly Object var1);
boolean remove(@Readonly Object var1);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Map<K extends @Immutable Object, V> {
int size(@Readonly Map<K, V> this);
boolean isEmpty(@Readonly Map<K, V> this);
Expand All @@ -192,10 +192,10 @@ interface Map<K extends @Immutable Object, V> {
Set<Map.Entry<K, V>> entrySet(@Readonly Map<K, V> this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class HashMap<K extends @Immutable Object, V> {
@ReceiverDependantMutable HashMap();
@ReceiverDependantMutable HashMap(@Readonly Map<? extends K, ? extends V> var1);
@ReceiverDependentMutable HashMap();
@ReceiverDependentMutable HashMap(@Readonly Map<? extends K, ? extends V> var1);
V get(@Readonly HashMap<K, V> this, @Readonly Object key);
boolean containsKey(@Readonly HashMap<K, V> this, @Readonly Object key);
boolean containsValue(@Readonly HashMap<K, V> this, @Readonly Object value);
Expand Down Expand Up @@ -224,18 +224,18 @@ class Objects {
static boolean equals(@Readonly Object a, @Readonly Object b);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class Stack<E> {
E peek(@ReceiverDependantMutable Stack<E> this);
boolean empty(@ReceiverDependantMutable Stack<E> this);
E peek(@ReceiverDependentMutable Stack<E> this);
boolean empty(@ReceiverDependentMutable Stack<E> this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class Vector<E> {
boolean isEmpty(@Readonly Vector<E> this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class Hashtable<K extends @Immutable Object,V> {
V get(@Readonly Hashtable<K,V> this, @Readonly Object key);
boolean containsKey(@Readonly Hashtable<K,V> this, @Readonly Object key);
Expand All @@ -258,43 +258,43 @@ class Pattern {

package java.io;

@ReceiverDependantMutable
@ReceiverDependentMutable
class PrintStream {
void print(@ReceiverDependantMutable PrintStream this, String var1);
PrintStream printf(@ReceiverDependantMutable PrintStream this, String var1, @Readonly Object @Readonly ... var2);
void print(@ReceiverDependentMutable PrintStream this, String var1);
PrintStream printf(@ReceiverDependentMutable PrintStream this, String var1, @Readonly Object @Readonly ... var2);
PrintStream format(String format, @Readonly Object @Readonly ... args);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class PrintWriter {
PrintWriter printf(@ReceiverDependantMutable PrintWriter this, String var1, @Readonly Object @Readonly ... var2);
PrintWriter printf(@ReceiverDependentMutable PrintWriter this, String var1, @Readonly Object @Readonly ... var2);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class File {
@ReceiverDependantMutable File(@Readonly File parent, String child);
@ReceiverDependentMutable File(@Readonly File parent, String child);
boolean isFile(@Readonly File this);
String[] list(@Readonly File this);
String getPath(@Readonly File this);
long length(@Readonly File this);
String getName(@Readonly File this);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
class FileInputStream {
@ReceiverDependantMutable FileInputStream(@Readonly File file);
@ReceiverDependentMutable FileInputStream(@Readonly File file);
}

class ObjectOutputStream {
void writeObject(@Readonly Object obj);
}

@ReceiverDependantMutable
@ReceiverDependentMutable
interface Serializable {}

package java.awt;

@ReceiverDependantMutable
@ReceiverDependentMutable
class Container {
void add(@Readonly Component comp, @Readonly Object constraints);
}
2 changes: 1 addition & 1 deletion src/main/java/pico/inference/messages.properties
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ subclass.bound.incompatible=Incompatible subclass bound: %s
subtype.constraint.violated=%s is not the subtype of %s
illegal.field.write=Cannot write field via receiver: %s
illegal.array.write=Cannot write array via receiver: %s
static.receiverdependantmutable.forbidden=%s is forbidden in static context
static.receiverdependentmutable.forbidden=%s is forbidden in static context
pico.new.invalid=Invalid new instance type: %s
field.polymutable.forbidden=Field %s cannot be @PolyMutable
one.assignability.invalid=Only one assignability qualifier is allowed on %s
Expand Down
Loading

0 comments on commit 1104d9e

Please sign in to comment.