Skip to content

Commit

Permalink
Merge pull request #1 from txiang61/add_variable_slot_type
Browse files Browse the repository at this point in the history 
Refactored slot structure and add variable slot type
  • Loading branch information
@txiang61
txiang61 authored Nov 20, 2019
2 parents 07eb554 + cd33d90 commit 0dea5d4
Show file tree
Hide file tree
Showing 18 changed files with 121 additions and 104 deletions.
56 changes: 28 additions & 28 deletions src/checkers/inference/DefaultSlotManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ public class DefaultSlotManager implements SlotManager {
* ConstantSlots are also stored in this map, since ConstantSlot is subclass
* of Slot.
*/
private final Map<Integer, Slot> variables;
private final Map<Integer, Slot> slots;

/**
* A map of {@link AnnotationMirror} to {@link Integer} for caching
Expand Down Expand Up @@ -113,7 +113,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
this.processingEnvironment = processingEnvironment;
// sort the qualifiers so that they are always assigned the same varId
this.realQualifiers = sortAnnotationClasses(realQualifiers);
variables = new LinkedHashMap<>();
slots = new LinkedHashMap<>();

AnnotationBuilder builder = new AnnotationBuilder(processingEnvironment, VarAnnot.class);
builder.setValue("value", -1 );
Expand All @@ -132,7 +132,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
Set<? extends AnnotationMirror> mirrors = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy().getTypeQualifiers();
for (AnnotationMirror am : mirrors) {
ConstantSlot constantSlot = new ConstantSlot(am, nextId());
addToVariables(constantSlot);
addToSlots(constantSlot);
constantCache.put(am, constantSlot.getId());
}
}
Expand Down Expand Up @@ -166,16 +166,16 @@ private int nextId() {
return nextId++;
}

private void addToVariables(final Slot slot) {
variables.put(slot.getId(), slot);
private void addToSlots(final Slot slot) {
slots.put(slot.getId(), slot);
}

/**
* @inheritDoc
*/
@Override
public Slot getVariable( int id ) {
return variables.get(id);
public Slot getSlot( int id ) {
return slots.get(id);
}

/**
Expand Down Expand Up @@ -236,12 +236,12 @@ public Slot getSlot( final AnnotationMirror annotationMirror ) {
id = Integer.valueOf( annoValue.toString() );
}

return getVariable( id );
return getSlot( id );

} else {

if (constantCache.containsKey(annotationMirror)) {
ConstantSlot constantSlot = (ConstantSlot) getVariable(
ConstantSlot constantSlot = (ConstantSlot) getSlot(
constantCache.get(annotationMirror));
return constantSlot;

Expand All @@ -266,7 +266,7 @@ public Slot getSlot( final AnnotationMirror annotationMirror ) {
*/
@Override
public List<Slot> getSlots() {
return new ArrayList<Slot>(this.variables.values());
return new ArrayList<Slot>(this.slots.values());
}

// Sometimes, I miss scala.
Expand All @@ -276,7 +276,7 @@ public List<Slot> getSlots() {
@Override
public List<Slot> getVariableSlots() {
List<Slot> varSlots = new ArrayList<>();
for (Slot slot : variables.values()) {
for (Slot slot : slots.values()) {
if (slot.isVariable()) {
varSlots.add(slot);
}
Expand All @@ -290,7 +290,7 @@ public List<Slot> getVariableSlots() {
@Override
public List<ConstantSlot> getConstantSlots() {
List<ConstantSlot> constants = new ArrayList<>();
for (Slot slot : variables.values()) {
for (Slot slot : slots.values()) {
if (slot.isConstant()) {
constants.add((ConstantSlot) slot);
}
Expand All @@ -309,13 +309,13 @@ public VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror t
if (location.getKind() == AnnotationLocation.Kind.MISSING) {
//Don't cache slot for MISSING LOCATION. Just create a new one and return.
variableSlot = new VariableSlot(location, nextId(), type);
addToVariables(variableSlot);
addToSlots(variableSlot);
} else if (locationCache.containsKey(location)) {
int id = locationCache.get(location);
variableSlot = (VariableSlot) getVariable(id);
variableSlot = (VariableSlot) getSlot(id);
} else {
variableSlot = new VariableSlot(location, nextId(), type);
addToVariables(variableSlot);
addToSlots(variableSlot);
locationCache.put(location, variableSlot.getId());
}
return variableSlot;
Expand All @@ -327,13 +327,13 @@ public RefinementVariableSlot createRefinementVariableSlot(AnnotationLocation lo
if (location.getKind() == AnnotationLocation.Kind.MISSING) {
//Don't cache slot for MISSING LOCATION. Just create a new one and return.
refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined);
addToVariables(refinementVariableSlot);
addToSlots(refinementVariableSlot);
} else if (locationCache.containsKey(location)) {
int id = locationCache.get(location);
refinementVariableSlot = (RefinementVariableSlot) getVariable(id);
refinementVariableSlot = (RefinementVariableSlot) getSlot(id);
} else {
refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined);
addToVariables(refinementVariableSlot);
addToSlots(refinementVariableSlot);
locationCache.put(location, refinementVariableSlot.getId());
}
return refinementVariableSlot;
Expand All @@ -344,10 +344,10 @@ public ConstantSlot createConstantSlot(AnnotationMirror value) {
ConstantSlot constantSlot;
if (constantCache.containsKey(value)) {
int id = constantCache.get(value);
constantSlot = (ConstantSlot) getVariable(id);
constantSlot = (ConstantSlot) getSlot(id);
} else {
constantSlot = new ConstantSlot(value, nextId());
addToVariables(constantSlot);
addToSlots(constantSlot);
constantCache.put(value, constantSlot.getId());
}
return constantSlot;
Expand All @@ -359,10 +359,10 @@ public CombVariableSlot createCombVariableSlot(Slot receiver, Slot declared) {
Pair<Slot, Slot> pair = new Pair<>(receiver, declared);
if (combSlotPairCache.containsKey(pair)) {
int id = combSlotPairCache.get(pair);
combVariableSlot = (CombVariableSlot) getVariable(id);
combVariableSlot = (CombVariableSlot) getSlot(id);
} else {
combVariableSlot = new CombVariableSlot(null, nextId(), receiver, declared);
addToVariables(combVariableSlot);
addToSlots(combVariableSlot);
combSlotPairCache.put(pair, combVariableSlot.getId());
}
return combVariableSlot;
Expand All @@ -375,11 +375,11 @@ public LubVariableSlot createLubVariableSlot(Slot left, Slot right) {
Pair<Slot, Slot> pair = new Pair<>(left, right);
if (lubSlotPairCache.containsKey(pair)) {
int id = lubSlotPairCache.get(pair);
lubVariableSlot = (LubVariableSlot) getVariable(id);
lubVariableSlot = (LubVariableSlot) getSlot(id);
} else {
// We need a non-null location in the future for better debugging outputs
lubVariableSlot = new LubVariableSlot(null, nextId(), left, right);
addToVariables(lubVariableSlot);
addToSlots(lubVariableSlot);
lubSlotPairCache.put(pair, lubVariableSlot.getId());
}
return lubVariableSlot;
Expand All @@ -391,10 +391,10 @@ public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot,
Pair<Slot, Slot> pair = new Pair<>(potentialSlot, alternativeSlot);
if (existentialSlotPairCache.containsKey(pair)) {
int id = existentialSlotPairCache.get(pair);
existentialVariableSlot = (ExistentialVariableSlot) getVariable(id);
existentialVariableSlot = (ExistentialVariableSlot) getSlot(id);
} else {
existentialVariableSlot = new ExistentialVariableSlot(nextId(), potentialSlot, alternativeSlot);
addToVariables(existentialVariableSlot);
addToSlots(existentialVariableSlot);
existentialSlotPairCache.put(pair, existentialVariableSlot.getId());
}
return existentialVariableSlot;
Expand All @@ -410,7 +410,7 @@ public ArithmeticVariableSlot createArithmeticVariableSlot(AnnotationLocation lo
// create the arithmetic var slot if it doesn't exist for the given location
if (!arithmeticSlotCache.containsKey(location)) {
ArithmeticVariableSlot slot = new ArithmeticVariableSlot(location, nextId());
addToVariables(slot);
addToSlots(slot);
arithmeticSlotCache.put(location, slot.getId());
return slot;
}
Expand All @@ -427,7 +427,7 @@ public ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation locat
if (!arithmeticSlotCache.containsKey(location)) {
return null;
} else {
return (ArithmeticVariableSlot) getVariable(arithmeticSlotCache.get(location));
return (ArithmeticVariableSlot) getSlot(arithmeticSlotCache.get(location));
}
}

Expand Down
29 changes: 13 additions & 16 deletions src/checkers/inference/InferenceQualifierHierarchy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,32 +264,29 @@ public AnnotationMirror leastUpperBound(final AnnotationMirror a1, final Annotat
Slot constantSlot = slotMgr.createConstantSlot(realLub);
return slotMgr.getAnnotation(constantSlot);
} else {
Slot var1 = slot1;
Slot var2 = slot2;

if (var1 == var2) {
if (slot1 == slot2) {
// They are the same slot.
return slotMgr.getAnnotation(var1);
return slotMgr.getAnnotation(slot1);

} else if (!Collections.disjoint(var1.getMergedToSlots(), var2.getMergedToSlots())) {
} else if (!Collections.disjoint(slot1.getMergedToSlots(), slot2.getMergedToSlots())) {
// They have common merge variables, return the annotations on one of the common merged variables.
Slot commonMergedSlot = getOneIntersected(var1.getMergedToSlots(), var2.getMergedToSlots());
Slot commonMergedSlot = getOneIntersected(slot1.getMergedToSlots(), slot2.getMergedToSlots());
return slotMgr.getAnnotation(commonMergedSlot);

} else if (var1.isMergedTo(var2)) {
} else if (slot1.isMergedTo(slot2)) {
// var2 is a merge variable that var1 has been merged to. So just return annotation on var2.
return slotMgr.getAnnotation(var2);
} else if (var2.isMergedTo(var1)) {
return slotMgr.getAnnotation(slot2);
} else if (slot2.isMergedTo(slot1)) {
// Vice versa.
return slotMgr.getAnnotation(var1);
return slotMgr.getAnnotation(slot1);
} else {
// Create a new LubVariable for var1 and var2.
final LubVariableSlot mergeVariableSlot = slotMgr.createLubVariableSlot(var1, var2);
constraintMgr.addSubtypeConstraint(var1, mergeVariableSlot);
constraintMgr.addSubtypeConstraint(var2, mergeVariableSlot);
final LubVariableSlot mergeVariableSlot = slotMgr.createLubVariableSlot(slot1, slot2);
constraintMgr.addSubtypeConstraint(slot1, mergeVariableSlot);
constraintMgr.addSubtypeConstraint(slot2, mergeVariableSlot);

var1.addMergedToSlot(mergeVariableSlot);
var2.addMergedToSlot(mergeVariableSlot);
slot1.addMergedToSlot(mergeVariableSlot);
slot2.addMergedToSlot(mergeVariableSlot);

return slotMgr.getAnnotation(mergeVariableSlot);
}
Expand Down
5 changes: 2 additions & 3 deletions src/checkers/inference/InferenceTypeVariableSubstitutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,9 +71,8 @@ protected AnnotatedTypeMirror substituteTypeVariable(AnnotatedTypeMirror argumen
if (argument.getKind() != TypeKind.TYPEVAR) {
final Slot altSlot = slotManager.getVariableSlot(argument);

final Slot alternative = altSlot;
if (alternative != null) {
final ExistentialVariableSlot slot = slotManager.createExistentialVariableSlot(potentialSlot, alternative);
if (altSlot != null) {
final ExistentialVariableSlot slot = slotManager.createExistentialVariableSlot(potentialSlot, altSlot);
argument.replaceAnnotation(slotManager.getAnnotation(slot));
} else {
if (!InferenceMain.isHackMode()) {
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/SlotManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ public interface SlotManager {
AnnotationMirror createEquivalentVarAnno(final AnnotationMirror realQualifier);

/** Return the variable identified by the given id or null if no such variable has been added */
Slot getVariable( int id );
Slot getSlot( int id );

/**
* Given a slot return an annotation that represents the slot when added to an AnnotatedTypeMirror.
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/VariableAnnotator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ protected AnnotationLocation treeToLocation(Tree tree) {
}

protected TypeMirror treeToType(Tree tree) {
return InferenceMain.getInstance().getRealTypeFactory().getAnnotatedType(tree).getUnderlyingType();
return TreeUtils.typeOf(tree);
}

/**
Expand Down
22 changes: 10 additions & 12 deletions src/checkers/inference/dataflow/InferenceValue.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,29 +119,27 @@ public CFValue mostSpecific(CFValue other, CFValue backup) {
*/
public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, final CFValue other, final CFValue backup) {
if (thisSlot.isVariable() && otherSlot.isVariable()) {
Slot thisVarSlot = thisSlot;
Slot otherVarSlot = otherSlot;
if (thisVarSlot.isMergedTo(otherVarSlot)) {
if (thisSlot.isMergedTo(otherSlot)) {
return other;
} else if (otherVarSlot.isMergedTo(thisVarSlot)) {
} else if (otherSlot.isMergedTo(thisSlot)) {
return this;
} else if (thisVarSlot instanceof RefinementVariableSlot
&& ((RefinementVariableSlot) thisVarSlot).getRefined().equals(otherVarSlot)) {
} else if (thisSlot instanceof RefinementVariableSlot
&& ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) {

return this;
} else if (otherVarSlot instanceof RefinementVariableSlot
&& ((RefinementVariableSlot) otherVarSlot).getRefined().equals(thisVarSlot)) {
} else if (otherSlot instanceof RefinementVariableSlot
&& ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) {

return other;
} else {
// Check if one of these has refinement variables that were merged to the other.
for (RefinementVariableSlot slot : thisVarSlot.getRefinedToSlots()) {
if (slot.isMergedTo(otherVarSlot)) {
for (RefinementVariableSlot slot : thisSlot.getRefinedToSlots()) {
if (slot.isMergedTo(otherSlot)) {
return other;
}
}
for (RefinementVariableSlot slot : otherVarSlot.getRefinedToSlots()) {
if (slot.isMergedTo(thisVarSlot)) {
for (RefinementVariableSlot slot : otherSlot.getRefinedToSlots()) {
if (slot.isMergedTo(thisSlot)) {
return this;
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/checkers/inference/model/Serializer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,6 @@ public interface Serializer<S, T> {

T serialize(InequalityConstraint constraint);

S serialize(Slot slot);

S serialize(VariableSlot slot);

S serialize(ConstantSlot slot);
Expand All @@ -40,6 +38,8 @@ public interface Serializer<S, T> {

S serialize(LubVariableSlot slot);

S serialize(ArithmeticVariableSlot slot);

T serialize(ComparableConstraint comparableConstraint);

T serialize(CombineConstraint combineConstraint);
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/model/VariableSlot.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,6 @@ public TypeMirror getUnderlyingType() {
*/
@Override
public boolean isInsertable() {
return false;
return true;
}
}
13 changes: 7 additions & 6 deletions src/checkers/inference/model/serialization/CnfVecIntSerializer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

import checkers.inference.SlotManager;
import checkers.inference.model.ArithmeticConstraint;
import checkers.inference.model.ArithmeticVariableSlot;
import checkers.inference.model.CombVariableSlot;
import checkers.inference.model.CombineConstraint;
import checkers.inference.model.ComparableConstraint;
Expand Down Expand Up @@ -215,12 +216,6 @@ public boolean emptyClause(VecInt ... clauses) {
return false;
}

@Override
public VecInt[] serialize(Slot slot) {
// doesn't really mean anything
return null;
}

@Override
public VecInt[] serialize(VariableSlot slot) {
// doesn't really mean anything
Expand Down Expand Up @@ -249,6 +244,12 @@ public VecInt[] serialize(CombVariableSlot slot) {
public VecInt[] serialize(LubVariableSlot slot) {
return null;
}

@Override
public VecInt[] serialize(ArithmeticVariableSlot slot) {
// doesn't really mean anything
return null;
}

@Override
public VecInt[] serialize(ExistentialVariableSlot slot) {
Expand Down
Loading

0 comments on commit 0dea5d4

Please sign in to comment.