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.

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

CFI update for Value inference to work with hack mode #285

Open
wants to merge 63 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
63 commits
Select commit Hold shift + click to select a range
8fadcc7
Added Z3smt solver
Sep 23, 2019
ca34b12
correct z3smt package name
Sep 24, 2019
87ddb4c
clean up debug code and unused code
txiang61 Oct 1, 2019
ad0f0f3
little format adjestment
txiang61 Oct 1, 2019
80048c4
eliminate one TODO
txiang61 Oct 4, 2019
26e5c06
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
8a7c31b
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
f7b2b91
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
6f9b878
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
658c3ee
added preference for subtype constraints to prefer constant slot over…
txiang61 Oct 8, 2019
b6dc6dd
restructure Z3SmtSolver so it can be overriden by both the unit-infer…
txiang61 Oct 17, 2019
c62dbc0
reformat Z3SmtConstraintEncoderFactory
txiang61 Oct 17, 2019
f068fc7
Added operation kind for comparable constraints encoder and its slot
txiang61 Oct 23, 2019
8f1669d
added underlying type to Variable Slot
txiang61 Nov 1, 2019
1f62945
removed comparable slot
txiang61 Nov 1, 2019
ea8d0a5
added underlying type to Variable Slot
txiang61 Nov 1, 2019
a1f8853
Addded unary and compount assginment handling in variable annotator
txiang61 Nov 7, 2019
8748fa2
improve javadoc in variable annotator for unary and compound assignme…
txiang61 Nov 7, 2019
692c126
Merge branch 'unary_compound'
txiang61 Nov 7, 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
36fe6ed
Slot refactor. Make all slots that extends varaibleslot to extends sl…
txiang61 Nov 9, 2019
ad0c61d
Merge opprop master to this
txiang61 Nov 11, 2019
2193c77
Merge branch 'master' into add_z3
txiang61 Nov 11, 2019
d52c20f
slot refactoring. Remove all cast to VariableSlot and uses Slot instead
txiang61 Nov 11, 2019
30de4f6
slot refactoring. Remove all cast to VariableSlot and uses Slot instead
txiang61 Nov 11, 2019
07eb554
Merge branch 'master' of https://github.com/opprop/checker-framework-…
txiang61 Nov 12, 2019
abaeae7
add ArithmeticVariableSlot serialization and clean up some code
txiang61 Nov 14, 2019
9af2d34
add ArithmeticVariableSlot serialization and clean up some code
txiang61 Nov 14, 2019
b201b52
added Z3SmtSoftConstraintEncoder and moved all soft constraints encod…
txiang61 Nov 15, 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
0dea5d4
Merge pull request #1 from txiang61/add_variable_slot_type
txiang61 Nov 20, 2019
3364a49
Merge branch 'master' of https://github.com/txiang61/checker-framewor…
txiang61 Nov 20, 2019
5337de0
Merge remote-tracking branch 'opprop/master'
txiang61 Nov 20, 2019
95cbef7
Merge branch 'master' into add_z3
txiang61 Nov 20, 2019
4d28ec7
Merge pull request #2 from txiang61/add_z3
txiang61 Nov 20, 2019
a433be3
fix error
txiang61 Nov 20, 2019
57cd019
Change comparable constraint structure and rename operators
txiang61 Nov 21, 2019
4c0c314
create refinment slot when decalre variable with initialization
txiang61 Nov 24, 2019
d0e855e
create refinment slot when decalre variable with initialization
txiang61 Nov 24, 2019
4022263
Merge branch 'master' of https://github.com/txiang61/checker-framewor…
txiang61 Nov 28, 2019
c2fd065
create refinment variable for desugared trees since the desugared tre…
txiang61 Dec 11, 2019
59ac962
Update repo with changes in opprop/master
txiang61 Mar 22, 2020
9b3fd11
Merge remote-tracking branch 'opprop/master'
txiang61 Jul 19, 2020
9ddab04
Add comparison constraint instead of modifying comparable constriant …
txiang61 Jun 26, 2020
df85f55
clean up
txiang61 Jun 26, 2020
e5f6eeb
add variable slot create
txiang61 Jul 23, 2020
0b14f91
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
0191dd1
hacks
txiang61 Aug 25, 2020
5132e87
add hacks to fix poly problem
txiang61 Sep 1, 2020
162066f
add hacks to avoid null pointer exceptions
txiang61 Sep 2, 2020
87514a1
fix refinement to get declared instead of comparison slot
txiang61 Sep 10, 2020
a6c1efd
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
06e5e5e
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
9c961c5
Merge remote-tracking branch 'opprop/master'
txiang61 Oct 13, 2020
8911126
Merge branch 'master' into value-benchmark
txiang61 Oct 13, 2020
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
Prev Previous commit
Next Next commit
added underlying type to Variable Slot
  • Loading branch information
txiang61 committed Nov 7, 2019
commit ea8d0a5028364f3b6fd58198ed0da9fb99f8da13
7 changes: 4 additions & 3 deletions src/checkers/inference/DefaultSlotManager.java
Original file line number Diff line number Diff line change
@@ -17,6 +17,7 @@
import javax.annotation.processing.ProcessingEnvironment;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.AnnotationValue;
import javax.lang.model.type.TypeMirror;

import checkers.inference.model.LubVariableSlot;

@@ -300,17 +301,17 @@ public int getNumberOfSlots() {
}

@Override
public VariableSlot createVariableSlot(AnnotationLocation location) {
public VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror type) {
VariableSlot variableSlot;
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());
variableSlot = new VariableSlot(location, nextId(), type);
addToVariables(variableSlot);
} else if (locationCache.containsKey(location)) {
int id = locationCache.get(location);
variableSlot = getVariable(id);
} else {
variableSlot = new VariableSlot(location, nextId());
variableSlot = new VariableSlot(location, nextId(), type);
addToVariables(variableSlot);
locationCache.put(location, variableSlot.getId());
}
4 changes: 2 additions & 2 deletions src/checkers/inference/ImpliedTypeAnnotator.java
Original file line number Diff line number Diff line change
@@ -78,7 +78,7 @@ protected void insertExistentialVariable(AnnotatedTypeVariable typeVariableUse,
typeFactory.getAnnotatedType(typeVariableUse.getUnderlyingType().asElement());

AnnotationLocation location = getLocation(typeVariableUse, astRecords);
VariableSlot potentialVar = slotManager.createVariableSlot(location);
VariableSlot potentialVar = slotManager.createVariableSlot(location, typeVariableUse.getUnderlyingType());
existentialVariableInserter.insert(potentialVar, typeVariableUse, declaration);
}

@@ -120,7 +120,7 @@ protected Void scan(AnnotatedTypeMirror type, Map<AnnotatedTypeMirror, ASTRecord
*/
protected void addVariablePrimaryAnnotation(final AnnotatedTypeMirror type, Map<AnnotatedTypeMirror, ASTRecord> astRecords) {
AnnotationLocation location = getLocation(type, astRecords);
VariableSlot slot = slotManager.createVariableSlot(location);
VariableSlot slot = slotManager.createVariableSlot(location, type.getUnderlyingType());
type.addAnnotation(slotManager.getAnnotation(slot));
}

3 changes: 2 additions & 1 deletion src/checkers/inference/SlotManager.java
Original file line number Diff line number Diff line change
@@ -6,6 +6,7 @@
import java.util.List;

import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.type.TypeMirror;

import checkers.inference.model.AnnotationLocation;
import checkers.inference.model.ArithmeticVariableSlot;
@@ -40,7 +41,7 @@ public interface SlotManager {
* used to locate this variable in code
* @return VariableSlot that corresponds to this location
*/
VariableSlot createVariableSlot(AnnotationLocation location);
VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror type);

/**
* Create new RefinementVariableSlot and return the reference to it if no
21 changes: 13 additions & 8 deletions src/checkers/inference/VariableAnnotator.java
Original file line number Diff line number Diff line change
@@ -37,6 +37,7 @@
import javax.lang.model.element.TypeElement;
import javax.lang.model.element.TypeParameterElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;

import com.sun.source.tree.AnnotatedTypeTree;
import com.sun.source.tree.ArrayTypeTree;
@@ -195,6 +196,10 @@ protected AnnotationLocation treeToLocation(Tree tree) {
return treeToLocation(inferenceTypeFactory, tree);
}

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

/**
* For each method call that uses a method with a polymorphic qualifier, we replace all uses of that polymorphic
* qualifier with a Variable. Sometimes we might have to later retrieve that qualifier for a given invocation
@@ -205,7 +210,7 @@ protected AnnotationLocation treeToLocation(Tree tree) {
public VariableSlot getOrCreatePolyVar(Tree tree) {
VariableSlot polyVar = treeToPolyVar.get(tree);
if (polyVar == null) {
polyVar = slotManager.createVariableSlot(treeToLocation(tree));
polyVar = slotManager.createVariableSlot(treeToLocation(tree), treeToType(tree));
treeToPolyVar.put(tree, polyVar);
}

@@ -224,7 +229,7 @@ public VariableSlot getOrCreatePolyVar(Tree tree) {
* @return A new VariableSlot corresponding to tree
*/
private VariableSlot createVariable(final Tree tree) {
final VariableSlot varSlot = createVariable(treeToLocation(tree));
final VariableSlot varSlot = createVariable(treeToLocation(tree), treeToType(tree));

// if (path != null) {
// Element element = inferenceTypeFactory.getTreeUtils().getElement(path);
@@ -251,9 +256,9 @@ private VariableSlot createVariable(final Tree tree) {
* actual implied tree appended to it.
* @return A new VariableSlot corresponding to tree
*/
private VariableSlot createVariable(final AnnotationLocation location) {
private VariableSlot createVariable(final AnnotationLocation location, TypeMirror type) {
final VariableSlot variableSlot = slotManager
.createVariableSlot(location);
.createVariableSlot(location, type);
return variableSlot;
}

@@ -528,7 +533,7 @@ private VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree
* the type.
*/
public VariableSlot addImpliedPrimaryVariable(AnnotatedTypeMirror atm, final AnnotationLocation location) {
VariableSlot variable = slotManager.createVariableSlot(location);
VariableSlot variable = slotManager.createVariableSlot(location, atm.getUnderlyingType());
atm.addAnnotation(slotManager.getAnnotation(variable));

AnnotationMirror realAnno = atm.getAnnotationInHierarchy(realTop);
@@ -564,7 +569,7 @@ private VariableSlot replaceOrCreateEquivalentVarAnno(AnnotatedTypeMirror atm, T
realQualifier = realTypeFactory.getAnnotatedType(tree).getAnnotationInHierarchy(realTop);
varSlot = slotManager.createConstantSlot(realQualifier);
} else {
varSlot = createVariable(location);
varSlot = createVariable(location, atm.getUnderlyingType());
}

atm.replaceAnnotation(slotManager.getAnnotation(varSlot));
@@ -757,7 +762,7 @@ private void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree c
if (!extendsMissingTrees.containsKey(classElement)) {
// TODO: SEE COMMENT ON createImpliedExtendsLocation
AnnotationLocation location = createImpliedExtendsLocation(classTree);
extendsSlot = createVariable(location);
extendsSlot = createVariable(location, classType.getUnderlyingType());
extendsMissingTrees.put(classElement, extendsSlot);
logger.fine("Created variable for implicit extends on class:\n" +
extendsSlot.getId() + " => " + classElement + " (extends Object)");
@@ -1211,7 +1216,7 @@ public Void visitTypeVariable(AnnotatedTypeVariable typeVar, Tree tree) {
final VariableSlot extendsSlot;
if (!extendsMissingTrees.containsKey(typeVarElement)) {
AnnotationLocation location = createImpliedExtendsLocation(typeParameterTree);
extendsSlot = createVariable(location);
extendsSlot = createVariable(location, typeVar.getUnderlyingType());
extendsMissingTrees.put(typeVarElement, extendsSlot);
logger.fine("Created variable for implicit extends on type parameter:\n" +
extendsSlot.getId() + " => " + typeVarElement + " (extends Object)");
33 changes: 33 additions & 0 deletions src/checkers/inference/model/VariableSlot.java
Original file line number Diff line number Diff line change
@@ -4,6 +4,8 @@
import java.util.HashSet;
import java.util.Set;

import javax.lang.model.type.TypeMirror;

/**
* VariableSlot is a Slot representing an undetermined value (i.e. a variable we are solving for).
* After the Solver is run, each VariableSlot should have an assigned value which is then written
@@ -36,15 +38,31 @@ public class VariableSlot extends Slot implements Comparable<VariableSlot>{
*/
private boolean insertable = true;

/** Actual type wrapped with this TypeMirror. */
protected final TypeMirror actualType;

/**
* @param location Used to locate this variable in code, see @AnnotationLocation
* @param id Unique identifier for this variable
*/
public VariableSlot(AnnotationLocation location, int id) {
super(location);
this.id = id;
this.actualType = null;
}

/**
* @param location Used to locate this variable in code, see @AnnotationLocation
* @param id Unique identifier for this variable
* @param type the underlying type
*/
public VariableSlot(AnnotationLocation location, int id, TypeMirror type) {
super(location);
this.id = id;
this.actualType = type;
}


// Slots this variable has been merged to.
private final Set<LubVariableSlot> mergedToSlots = new HashSet<>();

@@ -74,12 +92,27 @@ public boolean isMergedTo(VariableSlot other) {
return false;
}

/**
* Returns the underlying unannotated Java type, which this wraps.
*
* @return the underlying type
*/
public TypeMirror getUnderlyingType() {
return actualType;
}

public int getId() {
return id;
}

public VariableSlot(int id) {
this.id = id;
this.actualType = null;
}

public VariableSlot(int id, TypeMirror type) {
this.id = id;
this.actualType = type;
}

public Set<LubVariableSlot> getMergedToSlots() {