Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactored slot structure and add variable slot type #1

Merged
merged 13 commits into from
Nov 20, 2019
Merged

Refactored slot structure and add variable slot type #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
ea8d0a5
added underlying type to Variable Slot
txiang61 Nov 1, 2019
7476de4
Merge branch 'master' into add_variable_slot_type
xingweitian Nov 8, 2019
c1f65d1
Slot refactor. Make all slots that extends varaibleslot to extends sl…
txiang61 Nov 9, 2019
d31f22b
Merge branch 'add_variable_slot_type' of https://github.com/txiang61/…
txiang61 Nov 9, 2019
30de4f6
slot refactoring. Remove all cast to VariableSlot and uses Slot instead
txiang61 Nov 11, 2019
9af2d34
add ArithmeticVariableSlot serialization and clean up some code
txiang61 Nov 14, 2019
8bccb7d
update test files and correct variableslot insertion and utilize vari…
txiang61 Nov 15, 2019
9357851
Merge branch 'master' into add_variable_slot_type
txiang61 Nov 20, 2019
5908ead
Update Serializer.java
txiang61 Nov 20, 2019
23def40
Update CnfVecIntSerializer.java
txiang61 Nov 20, 2019
a6574c0
Update JsonSerializer.java
txiang61 Nov 20, 2019
e1a1850
Update ToStringSerializer.java
txiang61 Nov 20, 2019
cd33d90
Update PrintUtils.java
txiang61 Nov 20, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 28 additions & 28 deletions src/checkers/inference/DefaultSlotManager.java
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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