diff --git a/.travis-build.sh b/.travis-build.sh index 9b7dcb5e9..99dded74f 100755 --- a/.travis-build.sh +++ b/.travis-build.sh @@ -34,7 +34,7 @@ if [[ "${GROUP}" == "cfi-tests" || "${GROUP}" == "all" ]]; then ./gradlew test - ./gradlew testDataflowExternalSolvers + ./gradlew testRefValExternalSolvers fi # Downstream tests diff --git a/README.md b/README.md index 3a1067773..3969df063 100644 --- a/README.md +++ b/README.md @@ -88,7 +88,7 @@ To test the build: ```` ./gradlew testCheckerInferenceScript ./gradlew testCheckerInferenceDevScript -./gradlew testDataflowExternalSolvers +./gradlew testRefValExternalSolvers ```` @@ -133,9 +133,9 @@ Specifies which checker to run. The three most supported checkers at the moment are `ostrusted.OsTrustedChecker`, `checkers.tainting.TaintingChecker` and -`dataflow.DataflowChecker`. +`refval.RefValChecker`. - You can find details of `dataflow.DataflowChecker` in [README.dataflow](src/dataflow/README.md) + You can find details of `refval.RefValChecker` in [README.refval](src/refval/README.md) * `--solver` Which solver to use on the constraints. diff --git a/build.gradle b/build.gradle index e1dc1a368..f4e82944a 100644 --- a/build.gradle +++ b/build.gradle @@ -270,9 +270,9 @@ task testCheckerInferenceDevScript(type: Exec, dependsOn: [dist, dependenciesJar 'testdata/interning/MapAssignment.java'] } -task testDataflowExternalSolvers(type: Exec, dependsOn: [dist, dependenciesJar]) { - description 'Test Dataflow type system on its external solvers Lingeling and LogicBlox' - executable './testing/dataflowexample/travis-test.sh' +task testRefValExternalSolvers(type: Exec, dependsOn: [dist, dependenciesJar]) { + description 'Test Reference Value type system on its external solvers Lingeling and LogicBlox' + executable './testing/refval-example/travis-test.sh' } afterEvaluate { diff --git a/src/checkers/inference/DefaultInferenceResult.java b/src/checkers/inference/DefaultInferenceResult.java index a674497e9..f736cf84e 100644 --- a/src/checkers/inference/DefaultInferenceResult.java +++ b/src/checkers/inference/DefaultInferenceResult.java @@ -53,7 +53,7 @@ public class DefaultInferenceResult implements InferenceResult { * 1) Try to create empty solution * 2) Subclass calls this super constructor to begin with an empty map. Then subclass * has its logic to adding solutions to the mapping {@link #varIdToAnnotation}. The existing two - * subclasses are: {@link dataflow.solvers.classic.DataflowResult} and {@link sparta.checkers.sat.IFlowResult}. + * subclasses are: {@link refval.solvers.classic.RefValResult} and {@link sparta.checkers.sat.IFlowResult}. */ public DefaultInferenceResult() { this(new HashMap<>()); diff --git a/src/checkers/inference/solver/constraintgraph/GraphBuilder.java b/src/checkers/inference/solver/constraintgraph/GraphBuilder.java index b4e3b35e1..c71554949 100644 --- a/src/checkers/inference/solver/constraintgraph/GraphBuilder.java +++ b/src/checkers/inference/solver/constraintgraph/GraphBuilder.java @@ -19,8 +19,8 @@ import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.Slot; import checkers.inference.model.SubtypeConstraint; -import dataflow.DataflowVisitor; -import dataflow.util.DataflowUtils; +import refval.RefValVisitor; +import refval.util.RefValUtils; /** * GraphBuilder builds the constraint graph and runs graph traversal algorithms @@ -133,8 +133,8 @@ private Set BFSSearch(Vertex vertex) { if (AnnotationUtils.areSame(top, next.getValue())) { continue; } else { - if (InferenceMain.getInstance().getVisitor() instanceof DataflowVisitor) { - String[] typeNames = DataflowUtils.getTypeNames(next.getValue()); + if (InferenceMain.getInstance().getVisitor() instanceof RefValVisitor) { + String[] typeNames = RefValUtils.getTypeNames(next.getValue()); if (typeNames.length == 1 && typeNames[0].length() == 0) { continue; } diff --git a/src/dataflow/solvers/classic/DatatypeSolution.java b/src/dataflow/solvers/classic/DatatypeSolution.java deleted file mode 100644 index 35922a0a7..000000000 --- a/src/dataflow/solvers/classic/DatatypeSolution.java +++ /dev/null @@ -1,37 +0,0 @@ -package dataflow.solvers.classic; - -import java.util.HashMap; -import java.util.Map; - -public class DatatypeSolution { - private final Map result; - private final String datatype; - private final boolean isRoot; - - public DatatypeSolution(Map result, String datatype, boolean isRoot) { - this.result = result; - this.datatype = datatype; - this.isRoot = isRoot; - } - - private DatatypeSolution(String datatype, boolean isRoot) { - this(new HashMap(), datatype, isRoot); - } - - public Map getResult() { - return result; - } - - public String getDatatype() { - return datatype; - } - - public static DatatypeSolution noSolution(String datatype) { - return new DatatypeSolution(datatype, false); - } - - public boolean isRoot() { - return this.isRoot; - } - -} diff --git a/src/dataflow/util/DataflowUtils.java b/src/dataflow/util/DataflowUtils.java deleted file mode 100644 index 995b0af2e..000000000 --- a/src/dataflow/util/DataflowUtils.java +++ /dev/null @@ -1,202 +0,0 @@ -package dataflow.util; - -import java.util.HashSet; -import java.util.List; -import java.util.Set; - -import javax.annotation.processing.ProcessingEnvironment; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeMirror; - -import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.javacutil.AnnotationBuilder; -import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.BugInCF; - -import com.sun.source.tree.LiteralTree; - -import dataflow.qual.DataFlow; - -/** - * Utility class for Dataflow type system. - * - * @author jianchu - * - */ -public class DataflowUtils { - - public static String[] getTypeNames(AnnotationMirror type) { - return getDataflowValue(type, "typeNames"); - } - - public static String[] getTypeNameRoots(AnnotationMirror type) { - return getDataflowValue(type, "typeNameRoots"); - } - - private static String[] getDataflowValue(AnnotationMirror type, String valueName) { - List allTypesList = AnnotationUtils.getElementValueArray(type, valueName, String.class, - true); - // types in this list is org.checkerframework.framework.util.AnnotationBuilder. - String[] allTypesInArray = new String[allTypesList.size()]; - int i = 0; - for (Object o : allTypesList) { - allTypesInArray[i] = o.toString(); - i++; - } - return allTypesInArray; - } - - public static AnnotationMirror createDataflowAnnotationForByte(String[] dataType, - ProcessingEnvironment processingEnv) { - AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlow.class); - builder.setValue("typeNameRoots", dataType); - return builder.build(); - } - - private static AnnotationMirror createDataflowAnnotation(final Set datatypes, - final AnnotationBuilder builder) { - String[] datatypesInArray = new String[datatypes.size()]; - int i = 0; - for (String datatype : datatypes) { - datatypesInArray[i] = datatype.toString(); - i++; - } - builder.setValue("typeNames", datatypesInArray); - return builder.build(); - } - - private static AnnotationMirror createDataflowAnnotationWithoutName(final Set roots, - final AnnotationBuilder builder) { - String[] datatypesInArray = new String[roots.size()]; - int i = 0; - for (String datatype : roots) { - datatypesInArray[i] = datatype.toString(); - i++; - } - builder.setValue("typeNameRoots", datatypesInArray); - return builder.build(); - } - - public static AnnotationMirror createDataflowAnnotation(Set datatypes, - ProcessingEnvironment processingEnv) { - AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlow.class); - - return createDataflowAnnotation(datatypes, builder); - } - - public static AnnotationMirror createDataflowAnnotationWithoutName(Set roots, - ProcessingEnvironment processingEnv) { - AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlow.class); - return createDataflowAnnotationWithoutName(roots, builder); - - } - - public static AnnotationMirror createDataflowAnnotation(String[] dataType, - ProcessingEnvironment processingEnv) { - AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlow.class); - builder.setValue("typeNames", dataType); - return builder.build(); - } - - public static AnnotationMirror createDataflowAnnotationWithRoots(Set datatypes, - Set datatypesRoots, ProcessingEnvironment processingEnv) { - AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlow.class); - return createDataflowAnnotationWithRoots(datatypes, datatypesRoots, builder); - } - - private static AnnotationMirror createDataflowAnnotationWithRoots(final Set datatypes, - final Set datatypesRoots, final AnnotationBuilder builder) { - String[] datatypesInArray = new String[datatypes.size()]; - int i = 0; - for (String datatype : datatypes) { - datatypesInArray[i] = datatype.toString(); - i++; - } - - String[] datatypesRootInArray = new String[datatypesRoots.size()]; - int j = 0; - for (String datatypesRoot : datatypesRoots) { - datatypesRootInArray[j] = datatypesRoot.toString(); - j++; - } - if (datatypesRootInArray.length > 0) { - builder.setValue("typeNameRoots", datatypesRootInArray); - } - if (datatypesInArray.length > 0) { - builder.setValue("typeNames", datatypesInArray); - } - - return builder.build(); - } - - public static AnnotationMirror genereateDataflowAnnoFromNewClass(AnnotatedTypeMirror type, - ProcessingEnvironment processingEnv) { - TypeMirror tm = type.getUnderlyingType(); - String className = tm.toString(); - AnnotationMirror dataFlowType = createDataflowAnnotation(convert(className), processingEnv); - return dataFlowType; - } - - public static AnnotationMirror genereateDataflowAnnoFromByteCode(AnnotatedTypeMirror type, - ProcessingEnvironment processingEnv) { - TypeMirror tm = type.getUnderlyingType(); - String className = tm.toString(); - AnnotationMirror dataFlowType = createDataflowAnnotationForByte(convert(className), - processingEnv); - return dataFlowType; - } - - public static AnnotationMirror generateDataflowAnnoFromLiteral(AnnotatedTypeMirror type, - ProcessingEnvironment processingEnv) { - String datatypeInArray[] = convert(type.getUnderlyingType().toString()); - AnnotationMirror dataFlowType = createDataflowAnnotation(datatypeInArray, processingEnv); - return dataFlowType; - } - - public static AnnotationMirror generateDataflowAnnoFromLiteral(LiteralTree node, - ProcessingEnvironment processingEnv) { - String datatypeInArray[] = { "" }; - switch (node.getKind()) { - case STRING_LITERAL: - datatypeInArray = convert(String.class.toString().split(" ")[1]); - break; - case INT_LITERAL: - datatypeInArray = convert(int.class.toString()); - break; - case LONG_LITERAL: - datatypeInArray = convert(long.class.toString()); - break; - case FLOAT_LITERAL: - datatypeInArray = convert(float.class.toString()); - break; - case DOUBLE_LITERAL: - datatypeInArray = convert(double.class.toString()); - break; - case BOOLEAN_LITERAL: - datatypeInArray = convert(boolean.class.toString()); - break; - case CHAR_LITERAL: - datatypeInArray = convert(char.class.toString()); - break; - case NULL_LITERAL: - // Null literal wouldn't be passed here. - break; - default: - throw new BugInCF("Unknown literal tree: " + node.getKind().toString()); - } - AnnotationMirror dataFlowType = createDataflowAnnotation(datatypeInArray, processingEnv); - return dataFlowType; - } - - public static String[] convert(String... typeName) { - return typeName; - } - - public static AnnotationMirror createDataflowAnnotation(String typeName, - ProcessingEnvironment processingEnv) { - Set typeNames = new HashSet(); - typeNames.add(typeName); - AnnotationMirror am = DataflowUtils.createDataflowAnnotation(typeNames, processingEnv); - return am; - } -} diff --git a/src/dataflow/README.md b/src/refval/README.md similarity index 61% rename from src/dataflow/README.md rename to src/refval/README.md index 9e86afb10..04be9c1c5 100644 --- a/src/dataflow/README.md +++ b/src/refval/README.md @@ -1,10 +1,10 @@ -Dataflow type system README +Reference Value type system README =========================== Requirements ------------ -In order to use the dataflow type system, you first need to set up the +In order to use the refval type system, you first need to set up the following four projects: - https://github.com/typetools/annotation-tools @@ -32,15 +32,15 @@ The tool `graphviz` could visualize the dot files that are generated by checker- Running Example --------------- -`dataflowexample` can be found under `/the/path/to/checker-framework-inference/testing`. This is a sample project that is annotated without any @Dataflow annotations, so you can play around with it: type check, type infer, insert the inferred annotations to source code, visualize the control flow graph, etc. +`refvalexample` can be found under `/the/path/to/checker-framework-inference/testing`. This is a sample project that is annotated without any @Refval annotations, so you can play around with it: type check, type infer, insert the inferred annotations to source code, visualize the control flow graph, etc. Here are some instructions that shows how to do these tasks with `do-like-javac`: -1. Change into the dataflowexample directory: +1. Change into the refvalexample directory: ``` - cd /the/path/to/checker-framework-inference/testing/dataflowexample + cd /the/path/to/checker-framework-inference/testing/refvalexample ``` 2. Compile sub-project `libs` that is referenced by sub-project `project`: @@ -55,7 +55,7 @@ and then inserts the results back into the original source code. If the whole process runs successfully, the inserted output will be placed in `annotated` directory. ``` - dljc -t inference --checker dataflow.DataflowChecker --solver dataflow.solvers.general.DataflowGeneralSolver --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project + dljc -t inference --checker refval.RefValChecker --solver refval.solvers.general.RefvalSolverEngine --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project ``` 4. Invoke the checker tool with `do-like-javac`. @@ -64,7 +64,7 @@ This step will type check the newly created source code, and generate control flow graph. ``` - dljc -t checker --checker "dataflow.DataflowChecker -Aflowdotdir=./dotfiles" -o logs -- ant check-annotated-src + dljc -t checker --checker "refval.RefValChecker -Aflowdotdir=./dotfiles" -o logs -- ant check-annotated-src ``` Note the quotes around the `--checker` argument to ensure the whole string is used. @@ -73,26 +73,26 @@ whole string is used. 5. Visualize the dot files by tool `graphviz`. This step will generate a pdf file that contains the control flow graph. ``` - dot -Tpdf dotfiles/_init_Dataflow.dot -o CFG.pdf + dot -Tpdf dotfiles/_init_Refval.dot -o CFG.pdf ``` If you compare the original source code with the source code generated by the third step, you can find the string field `thisIsString` and `thisShouldbeString` are annotated with -`@DataFlow(typeNames={"java.lang.String"})` in the new source code, although the declared type of `thisShouldbeString` is `Object`. +`@RefVal(typeNames={"java.lang.String"})` in the new source code, although the declared type of `thisShouldbeString` is `Object`. -Alternatively, you can simply execute `sh ./runDataflowSolver.sh` under `/the/path/to/checker-framework-inference/testing/dataflowexample` to run the dataflow example. +Alternatively, you can simply execute `sh ./runRefValSolver.sh` under `/the/path/to/checker-framework-inference/testing/refvalexample` to run the refval example. Running On Open Source --------------- -If you want to infer Dataflow annotations for large open source projects, the steps are very similar to the above instructions. +If you want to infer Refval annotations for large open source projects, the steps are very similar to the above instructions. In second step, instead of running: ``` - dljc -t inference --checker dataflow.DataflowChecker - --solver dataflow.solvers.classic.DataflowSolver -o logs + dljc -t inference --checker refval.RefValChecker + --solver refval.solvers.classic.RefValSolver -o logs -m ROUNDTRIP -afud annotated -- ant compile-project ``` Changing `ant compile-project` to the build command for the open source project, and if the whole process runs successfully, the output with annotations inserted will be placed in `annotated` directory. diff --git a/src/dataflow/DataflowAnnotatedTypeFactory.java b/src/refval/RefValAnnotatedTypeFactory.java similarity index 73% rename from src/dataflow/DataflowAnnotatedTypeFactory.java rename to src/refval/RefValAnnotatedTypeFactory.java index 6b2eed359..af0fc2426 100644 --- a/src/dataflow/DataflowAnnotatedTypeFactory.java +++ b/src/refval/RefValAnnotatedTypeFactory.java @@ -1,4 +1,4 @@ -package dataflow; +package refval; import java.util.ArrayList; import java.util.Arrays; @@ -37,54 +37,54 @@ import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree.Kind; -import dataflow.qual.DataFlow; -import dataflow.qual.DataFlowTop; -import dataflow.util.DataflowUtils; +import refval.qual.RefVal; +import refval.qual.UnknownRefVal; +import refval.util.RefValUtils; /** - * DataflowAnnotatedTypeFactory is the type factory for Dataflow type system. It - * defines the subtype relationship of Dataflow type system, annotate the base + * RefValAnnotatedTypeFactory is the type factory for RefVal type system. It + * defines the subtype relationship of RefVal type system, annotate the base * cases, and implements simplification algorithm. * * @author jianchu * */ -public class DataflowAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { +public class RefValAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { - protected final AnnotationMirror DATAFLOW, DATAFLOWBOTTOM, DATAFLOWTOP; + protected final AnnotationMirror REFVAL, BOTTOMREFVAL, UnknownREFVAL; /** * For each Java type is present in the target program, typeNamesMap maps * String of the type to the TypeMirror. */ private final Map typeNamesMap = new HashMap(); - public DataflowAnnotatedTypeFactory(BaseTypeChecker checker) { + public RefValAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); - DATAFLOW = AnnotationBuilder.fromClass(elements, DataFlow.class); - DATAFLOWBOTTOM = DataflowUtils.createDataflowAnnotation(DataflowUtils.convert(""), processingEnv); - DATAFLOWTOP = AnnotationBuilder.fromClass(elements, DataFlowTop.class); + REFVAL = AnnotationBuilder.fromClass(elements, RefVal.class); + BOTTOMREFVAL = RefValUtils.createRefValAnnotation(RefValUtils.convert(""), processingEnv); + UnknownREFVAL = AnnotationBuilder.fromClass(elements, UnknownRefVal.class); postInit(); } @Override public TreeAnnotator createTreeAnnotator() { - return new ListTreeAnnotator(super.createTreeAnnotator(), new DataflowTreeAnnotator()); + return new ListTreeAnnotator(super.createTreeAnnotator(), new RefValTreeAnnotator()); } @Override public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { - return new DataFlowQualifierHierarchy(factory, DATAFLOWBOTTOM); + return new RefValQualifierHierarchy(factory, BOTTOMREFVAL); } /** * This method handles autoboxing for primitive type. * For statements, Integer i = 3; - * The annotation for i should be @DataFlow(typeNames = {"Integer"}). + * The annotation for i should be @RefVal(typeNames = {"Integer"}). */ @Override public AnnotatedDeclaredType getBoxedType(AnnotatedPrimitiveType type) { TypeElement typeElt = types.boxedClass(type.getUnderlyingType()); - AnnotationMirror am = DataflowUtils.createDataflowAnnotation(typeElt.asType().toString(), + AnnotationMirror am = RefValUtils.createRefValAnnotation(typeElt.asType().toString(), this.processingEnv); AnnotatedDeclaredType dt = fromElement(typeElt); dt.addAnnotation(am); @@ -94,13 +94,13 @@ public AnnotatedDeclaredType getBoxedType(AnnotatedPrimitiveType type) { /** * This method handles unboxing for reference type. * For statements, int i = new Integer(3); - * The annotation for i should be @DataFlow(typeNames = {"int"}). + * The annotation for i should be @RefVal(typeNames = {"int"}). */ @Override public AnnotatedPrimitiveType getUnboxedType(AnnotatedDeclaredType type) throws IllegalArgumentException { PrimitiveType primitiveType = types.unboxedType(type.getUnderlyingType()); - AnnotationMirror am = DataflowUtils.createDataflowAnnotation(primitiveType.toString(), + AnnotationMirror am = RefValUtils.createRefValAnnotation(primitiveType.toString(), this.processingEnv); AnnotatedPrimitiveType pt = (AnnotatedPrimitiveType) AnnotatedTypeMirror.createType( primitiveType, this, false); @@ -108,29 +108,29 @@ public AnnotatedPrimitiveType getUnboxedType(AnnotatedDeclaredType type) return pt; } - private final class DataFlowQualifierHierarchy extends GraphQualifierHierarchy { + private final class RefValQualifierHierarchy extends GraphQualifierHierarchy { - public DataFlowQualifierHierarchy(MultiGraphFactory f, AnnotationMirror bottom) { + public RefValQualifierHierarchy(MultiGraphFactory f, AnnotationMirror bottom) { super(f, bottom); } /** * This method checks whether rhs is subtype of lhs. rhs and lhs are - * both Dataflow types with typeNameRoots argument. + * both RefVal types with typeNameRoots argument. * - * @param rhs - * @param lhs + * @param rhs the right hand side annotation mirror + * @param lhs the left hand side annotation mirror * @return true is rhs is subtype of lhs, otherwise return false. */ private boolean isSubtypeWithRoots(AnnotationMirror rhs, AnnotationMirror lhs) { - Set rTypeNamesSet = new HashSet(Arrays.asList(DataflowUtils + Set rTypeNamesSet = new HashSet(Arrays.asList(RefValUtils .getTypeNames(rhs))); - Set lTypeNamesSet = new HashSet(Arrays.asList(DataflowUtils + Set lTypeNamesSet = new HashSet(Arrays.asList(RefValUtils .getTypeNames(lhs))); - Set rRootsSet = new HashSet(Arrays.asList(DataflowUtils + Set rRootsSet = new HashSet(Arrays.asList(RefValUtils .getTypeNameRoots(rhs))); - Set lRootsSet = new HashSet(Arrays.asList(DataflowUtils + Set lRootsSet = new HashSet(Arrays.asList(RefValUtils .getTypeNameRoots(lhs))); Set combinedTypeNames = new HashSet(); combinedTypeNames.addAll(rTypeNamesSet); @@ -139,10 +139,10 @@ private boolean isSubtypeWithRoots(AnnotationMirror rhs, AnnotationMirror lhs) { combinedRoots.addAll(rRootsSet); combinedRoots.addAll(lRootsSet); - AnnotationMirror combinedAnno = DataflowUtils.createDataflowAnnotationWithRoots( + AnnotationMirror combinedAnno = RefValUtils.createRefValAnnotationWithRoots( combinedTypeNames, combinedRoots, processingEnv); - AnnotationMirror refinedCombinedAnno = refineDataflow(combinedAnno); - AnnotationMirror refinedLhs = refineDataflow(lhs); + AnnotationMirror refinedCombinedAnno = refineRefVal(combinedAnno); + AnnotationMirror refinedLhs = refineRefVal(lhs); if (AnnotationUtils.areSame(refinedCombinedAnno, refinedLhs)) { return true; @@ -153,18 +153,18 @@ private boolean isSubtypeWithRoots(AnnotationMirror rhs, AnnotationMirror lhs) { /** * This method checks whether rhs is subtype of lhs. rhs and lhs are - * both Dataflow types without typeNameRoots argument. Currently this - * method is not used, but we can use it for a lightweight dataflow type + * both RefVal types without typeNameRoots argument. Currently this + * method is not used, but we can use it for a lightweight RefVal type * system. (One without typeNameRoots argument). * - * @param rhs - * @param lhs + * @param rhs the right hand side annotation mirror + * @param lhs the left hand side annotation mirror * @return true is rhs is subtype of lhs, otherwise return false. */ private boolean isSubtypeWithoutRoots(AnnotationMirror rhs, AnnotationMirror lhs) { - Set rTypeNamesSet = new HashSet(Arrays.asList(DataflowUtils + Set rTypeNamesSet = new HashSet(Arrays.asList(RefValUtils .getTypeNames(rhs))); - Set lTypeNamesSet = new HashSet(Arrays.asList(DataflowUtils + Set lTypeNamesSet = new HashSet(Arrays.asList(RefValUtils .getTypeNames(lhs))); if (lTypeNamesSet.containsAll(rTypeNamesSet)) { return true; @@ -175,44 +175,44 @@ private boolean isSubtypeWithoutRoots(AnnotationMirror rhs, AnnotationMirror lhs @Override public boolean isSubtype(AnnotationMirror rhs, AnnotationMirror lhs) { - if (AnnotationUtils.areSameByName(rhs, DATAFLOW) - && AnnotationUtils.areSameByName(lhs, DATAFLOW)) { + if (AnnotationUtils.areSameByName(rhs, REFVAL) + && AnnotationUtils.areSameByName(lhs, REFVAL)) { return isSubtypeWithRoots(rhs, lhs); // return isSubtypeWithoutRoots(rhs, lhs); } else { // if (rhs != null && lhs != null) - if (AnnotationUtils.areSameByName(rhs, DATAFLOW)) { - rhs = DATAFLOW; - } else if (AnnotationUtils.areSameByName(lhs, DATAFLOW)) { - lhs = DATAFLOW; + if (AnnotationUtils.areSameByName(rhs, REFVAL)) { + rhs = REFVAL; + } else if (AnnotationUtils.areSameByName(lhs, REFVAL)) { + lhs = REFVAL; } return super.isSubtype(rhs, lhs); } } } - public class DataflowTreeAnnotator extends TreeAnnotator { - public DataflowTreeAnnotator() { - super(DataflowAnnotatedTypeFactory.this); + public class RefValTreeAnnotator extends TreeAnnotator { + public RefValTreeAnnotator() { + super(RefValAnnotatedTypeFactory.this); } @Override public Void visitNewArray(final NewArrayTree node, final AnnotatedTypeMirror type) { - AnnotationMirror dataFlowType = DataflowUtils.genereateDataflowAnnoFromNewClass(type, + AnnotationMirror refValType = RefValUtils.generateRefValAnnoFromNewClass(type, processingEnv); TypeMirror tm = type.getUnderlyingType(); typeNamesMap.put(tm.toString(), tm); - type.replaceAnnotation(dataFlowType); + type.replaceAnnotation(refValType); return super.visitNewArray(node, type); } @Override public Void visitNewClass(NewClassTree node, AnnotatedTypeMirror type) { - AnnotationMirror dataFlowType = DataflowUtils.genereateDataflowAnnoFromNewClass(type, + AnnotationMirror refValType = RefValUtils.generateRefValAnnoFromNewClass(type, processingEnv); TypeMirror tm = type.getUnderlyingType(); typeNamesMap.put(tm.toString(), tm); - type.replaceAnnotation(dataFlowType); + type.replaceAnnotation(refValType); return super.visitNewClass(node, type); } @@ -220,9 +220,9 @@ public Void visitNewClass(NewClassTree node, AnnotatedTypeMirror type) { public Void visitLiteral(LiteralTree node, AnnotatedTypeMirror type) { if (!node.getKind().equals(Kind.NULL_LITERAL)) { AnnotatedTypeMirror annoType = type; - AnnotationMirror dataFlowType = DataflowUtils.generateDataflowAnnoFromLiteral(annoType, + AnnotationMirror refValType = RefValUtils.generateRefValAnnoFromLiteral(annoType, processingEnv); - type.replaceAnnotation(dataFlowType); + type.replaceAnnotation(refValType); } return super.visitLiteral(node, type); } @@ -232,27 +232,27 @@ public Void visitMethodInvocation(MethodInvocationTree node, AnnotatedTypeMirror ExecutableElement methodElement = TreeUtils.elementFromUse(node); boolean isBytecode = ElementUtils.isElementFromByteCode(methodElement); if (isBytecode) { - AnnotationMirror dataFlowType = DataflowUtils.genereateDataflowAnnoFromByteCode(type, + AnnotationMirror refValType = RefValUtils.generateRefValAnnoFromByteCode(type, processingEnv); TypeMirror tm = type.getUnderlyingType(); if (tm.getKind() == TypeKind.ARRAY) { replaceArrayComponentATM((AnnotatedArrayType) type); } typeNamesMap.put(tm.toString(), tm); - type.replaceAnnotation(dataFlowType); + type.replaceAnnotation(refValType); } return super.visitMethodInvocation(node, type); } } /** - * Simplefication algoirthm. + * Simplification algorithm. * - * @param type - * @return A simplified annotation. + * @param type the annotation mirror to simplify + * @return the simplified annotation */ - public AnnotationMirror refineDataflow(AnnotationMirror type) { - String[] typeNameRoots = DataflowUtils.getTypeNameRoots(type); + public AnnotationMirror refineRefVal(AnnotationMirror type) { + String[] typeNameRoots = RefValUtils.getTypeNameRoots(type); Set refinedRoots = new HashSet(); if (typeNameRoots.length == 0) { @@ -270,13 +270,13 @@ public AnnotationMirror refineDataflow(AnnotationMirror type) { } } - String[] typeNames = DataflowUtils.getTypeNames(type); + String[] typeNames = RefValUtils.getTypeNames(type); Arrays.sort(typeNames); - Set refinedtypeNames = new HashSet(); + Set refinedTypeNames = new HashSet(); if (refinedRoots.size() == 0) { - refinedtypeNames = new HashSet(Arrays.asList(typeNames)); - return DataflowUtils.createDataflowAnnotation(refinedtypeNames, processingEnv); + refinedTypeNames = new HashSet(Arrays.asList(typeNames)); + return RefValUtils.createRefValAnnotation(refinedTypeNames, processingEnv); } else { for (String typeName : typeNames) { if (typeName == "") { @@ -284,25 +284,25 @@ public AnnotationMirror refineDataflow(AnnotationMirror type) { } TypeMirror decType = getTypeMirror(typeName); if (shouldPresent(decType, refinedRoots)) { - refinedtypeNames.add(typeName); + refinedTypeNames.add(typeName); } } } - return DataflowUtils.createDataflowAnnotationWithRoots(refinedtypeNames, refinedRoots, + return RefValUtils.createRefValAnnotationWithRoots(refinedTypeNames, refinedRoots, processingEnv); } /** - * Add the bytecode default Dataflow annotation for component type of the given {@link AnnotatedArrayType}. + * Add the bytecode default RefVal annotation for component type of the given {@link AnnotatedArrayType}. * - *

For multi-dimensional array, this method will recursively add bytecode default Dataflow annotation to array's component type. + *

For multi-dimensional array, this method will recursively add bytecode default RefVal annotation to array's component type. * * @param arrayAtm the given {@link AnnotatedArrayType}, whose component type will be added the bytecode default. */ private void replaceArrayComponentATM(AnnotatedArrayType arrayAtm) { AnnotatedTypeMirror componentAtm = arrayAtm.getComponentType(); - AnnotationMirror componentAnno = DataflowUtils.genereateDataflowAnnoFromByteCode(componentAtm, + AnnotationMirror componentAnno = RefValUtils.generateRefValAnnoFromByteCode(componentAtm, processingEnv); componentAtm.replaceAnnotation(componentAnno); if (componentAtm.getKind() == TypeKind.ARRAY) { diff --git a/src/dataflow/DataflowChecker.java b/src/refval/RefValChecker.java similarity index 53% rename from src/dataflow/DataflowChecker.java rename to src/refval/RefValChecker.java index cae662658..54b7eb561 100644 --- a/src/dataflow/DataflowChecker.java +++ b/src/refval/RefValChecker.java @@ -1,4 +1,4 @@ -package dataflow; +package refval; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.util.Elements; @@ -11,17 +11,17 @@ import checkers.inference.InferrableChecker; import checkers.inference.SlotManager; import checkers.inference.model.ConstraintManager; -import dataflow.qual.DataFlow; -import dataflow.qual.DataFlowTop; +import refval.qual.RefVal; +import refval.qual.UnknownRefVal; /** - * Checker for Dataflow type system. + * Checker for RefVal type system. * * @author jianchu * */ -public class DataflowChecker extends BaseInferrableChecker { - public AnnotationMirror DATAFLOW, DATAFLOWTOP; +public class RefValChecker extends BaseInferrableChecker { + public AnnotationMirror REFVAL, UNKNOWNREFVAL; @Override public void initChecker() { @@ -31,28 +31,28 @@ public void initChecker() { protected void setAnnotations() { final Elements elements = processingEnv.getElementUtils(); - DATAFLOW = AnnotationBuilder.fromClass(elements, DataFlow.class); - DATAFLOWTOP = AnnotationBuilder.fromClass(elements, DataFlowTop.class); + REFVAL = AnnotationBuilder.fromClass(elements, RefVal.class); + UNKNOWNREFVAL = AnnotationBuilder.fromClass(elements, UnknownRefVal.class); } @Override - public DataflowVisitor createVisitor(InferenceChecker ichecker, BaseAnnotatedTypeFactory factory, + public RefValVisitor createVisitor(InferenceChecker ichecker, BaseAnnotatedTypeFactory factory, boolean infer) { - return new DataflowVisitor(this, ichecker, factory, infer); + return new RefValVisitor(this, ichecker, factory, infer); } @Override - public DataflowAnnotatedTypeFactory createRealTypeFactory() { - return new DataflowAnnotatedTypeFactory(this); + public RefValAnnotatedTypeFactory createRealTypeFactory() { + return new RefValAnnotatedTypeFactory(this); } @Override - public DataflowInferenceAnnotatedTypeFactory createInferenceATF(InferenceChecker inferenceChecker, + public RefValInferenceAnnotatedTypeFactory createInferenceATF(InferenceChecker inferenceChecker, InferrableChecker realChecker, BaseAnnotatedTypeFactory realTypeFactory, SlotManager slotManager, ConstraintManager constraintManager) { - DataflowInferenceAnnotatedTypeFactory dataflowInferenceTypeFactory = new DataflowInferenceAnnotatedTypeFactory( + RefValInferenceAnnotatedTypeFactory refValInferenceTypeFactory = new RefValInferenceAnnotatedTypeFactory( inferenceChecker, realChecker.withCombineConstraints(), realTypeFactory, realChecker, slotManager, constraintManager); - return dataflowInferenceTypeFactory; + return refValInferenceTypeFactory; } } \ No newline at end of file diff --git a/src/dataflow/DataflowInferenceAnnotatedTypeFactory.java b/src/refval/RefValInferenceAnnotatedTypeFactory.java similarity index 80% rename from src/dataflow/DataflowInferenceAnnotatedTypeFactory.java rename to src/refval/RefValInferenceAnnotatedTypeFactory.java index 4cf755f6e..98f9cd4ea 100644 --- a/src/dataflow/DataflowInferenceAnnotatedTypeFactory.java +++ b/src/refval/RefValInferenceAnnotatedTypeFactory.java @@ -1,4 +1,4 @@ -package dataflow; +package refval; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -19,19 +19,19 @@ import checkers.inference.SlotManager; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; -import dataflow.util.DataflowUtils; +import refval.util.RefValUtils; /** - * DataflowInferenceAnnotatedTypeFactory handles boxing and unboxing for - * primitive types. The Dataflow type should always same as declared type for + * RefValInferenceAnnotatedTypeFactory handles boxing and unboxing for + * primitive types. The RefVal type should always same as declared type for * both cases. * * @author jianchu * */ -public class DataflowInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory { +public class RefValInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory { - public DataflowInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, + public RefValInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, boolean withCombineConstraints, BaseAnnotatedTypeFactory realTypeFactory, InferrableChecker realChecker, SlotManager slotManager, ConstraintManager constraintManager) { super(inferenceChecker, withCombineConstraints, realTypeFactory, realChecker, slotManager, @@ -42,14 +42,14 @@ public DataflowInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator(new LiteralTreeAnnotator(this), - new DataflowInferenceTreeAnnotator(this, realChecker, realTypeFactory, + new RefValInferenceTreeAnnotator(this, realChecker, realTypeFactory, variableAnnotator, slotManager)); } @Override public AnnotatedDeclaredType getBoxedType(AnnotatedPrimitiveType type) { TypeElement typeElt = types.boxedClass(type.getUnderlyingType()); - AnnotationMirror am = DataflowUtils.createDataflowAnnotation(typeElt.asType().toString(), + AnnotationMirror am = RefValUtils.createRefValAnnotation(typeElt.asType().toString(), this.processingEnv); AnnotatedDeclaredType dt = fromElement(typeElt); ConstantSlot cs = InferenceMain.getInstance().getSlotManager().createConstantSlot(am); @@ -62,7 +62,7 @@ public AnnotatedDeclaredType getBoxedType(AnnotatedPrimitiveType type) { public AnnotatedPrimitiveType getUnboxedType(AnnotatedDeclaredType type) throws IllegalArgumentException { PrimitiveType primitiveType = types.unboxedType(type.getUnderlyingType()); - AnnotationMirror am = DataflowUtils.createDataflowAnnotation(primitiveType.toString(), + AnnotationMirror am = RefValUtils.createRefValAnnotation(primitiveType.toString(), this.processingEnv); AnnotatedPrimitiveType pt = (AnnotatedPrimitiveType) AnnotatedTypeMirror.createType( primitiveType, this, false); diff --git a/src/dataflow/DataflowInferenceTreeAnnotator.java b/src/refval/RefValInferenceTreeAnnotator.java similarity index 78% rename from src/dataflow/DataflowInferenceTreeAnnotator.java rename to src/refval/RefValInferenceTreeAnnotator.java index 407b15f83..f6fb7eedc 100644 --- a/src/dataflow/DataflowInferenceTreeAnnotator.java +++ b/src/refval/RefValInferenceTreeAnnotator.java @@ -1,4 +1,4 @@ -package dataflow; +package refval; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -30,21 +30,21 @@ import com.sun.source.tree.Tree.Kind; import com.sun.source.util.TreePath; -import dataflow.util.DataflowUtils; +import refval.util.RefValUtils; /** - * DataflowInferenceTreeAnnotator creates constant slot for base cases. + * RefValInferenceTreeAnnotator creates constant slot for base cases. * * @author jianchu * */ -public class DataflowInferenceTreeAnnotator extends InferenceTreeAnnotator { +public class RefValInferenceTreeAnnotator extends InferenceTreeAnnotator { private final VariableAnnotator variableAnnotator; private final AnnotatedTypeFactory realTypeFactory; private final SlotManager slotManager; - public DataflowInferenceTreeAnnotator(InferenceAnnotatedTypeFactory atypeFactory, + public RefValInferenceTreeAnnotator(InferenceAnnotatedTypeFactory atypeFactory, InferrableChecker realChecker, AnnotatedTypeFactory realAnnotatedTypeFactory, VariableAnnotator variableAnnotator, SlotManager slotManager) { super(atypeFactory, realChecker, realAnnotatedTypeFactory, variableAnnotator, slotManager); @@ -57,7 +57,7 @@ public DataflowInferenceTreeAnnotator(InferenceAnnotatedTypeFactory atypeFactory @Override public Void visitLiteral(final LiteralTree literalTree, final AnnotatedTypeMirror atm) { if (!literalTree.getKind().equals(Kind.NULL_LITERAL)) { - AnnotationMirror anno = DataflowUtils.generateDataflowAnnoFromLiteral(literalTree, + AnnotationMirror anno = RefValUtils.generateRefValAnnoFromLiteral(literalTree, this.realTypeFactory.getProcessingEnv()); replaceATM(atm, anno); } else { @@ -69,8 +69,8 @@ public Void visitLiteral(final LiteralTree literalTree, final AnnotatedTypeMirro @Override public Void visitNewClass(final NewClassTree newClassTree, final AnnotatedTypeMirror atm) { TypeMirror tm = atm.getUnderlyingType(); - ((DataflowAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap().put(tm.toString(), tm); - AnnotationMirror anno = DataflowUtils.genereateDataflowAnnoFromNewClass(atm, + ((RefValAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap().put(tm.toString(), tm); + AnnotationMirror anno = RefValUtils.generateRefValAnnoFromNewClass(atm, this.realTypeFactory.getProcessingEnv()); replaceATM(atm, anno); variableAnnotator.visit(atm, newClassTree.getIdentifier()); @@ -93,8 +93,8 @@ public Void visitParameterizedType(final ParameterizedTypeTree param, final Anno @Override public Void visitNewArray(final NewArrayTree newArrayTree, final AnnotatedTypeMirror atm) { TypeMirror tm = atm.getUnderlyingType(); - ((DataflowAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap().put(tm.toString(), tm); - AnnotationMirror anno = DataflowUtils.genereateDataflowAnnoFromNewClass(atm, + ((RefValAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap().put(tm.toString(), tm); + AnnotationMirror anno = RefValUtils.generateRefValAnnoFromNewClass(atm, this.realTypeFactory.getProcessingEnv()); replaceATM(atm, anno); return null; @@ -107,14 +107,14 @@ public Void visitMethodInvocation(MethodInvocationTree methodInvocationTree, boolean isBytecode = ElementUtils.isElementFromByteCode(methodElement); if (isBytecode) { TypeMirror tm = atm.getUnderlyingType(); - ((DataflowAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap() + ((RefValAnnotatedTypeFactory) this.realTypeFactory).getTypeNameMap() .put(tm.toString(), tm); - AnnotationMirror anno = DataflowUtils.genereateDataflowAnnoFromByteCode(atm, + AnnotationMirror anno = RefValUtils.generateRefValAnnoFromByteCode(atm, this.realTypeFactory.getProcessingEnv()); if (atm.getKind() == TypeKind.ARRAY) { // If the return type of a byte code method is Array type, - // also generated Dataflow Annotation on Array component type. + // also generated RefVal Annotation on Array component type. replaceArrayComponentATM((AnnotatedArrayType) atm); } @@ -125,9 +125,9 @@ public Void visitMethodInvocation(MethodInvocationTree methodInvocationTree, } } - private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror dataflowAM) { - final ConstantSlot cs = slotManager.createConstantSlot(dataflowAM); - slotManager.createConstantSlot(dataflowAM); + private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror refValAM) { + final ConstantSlot cs = slotManager.createConstantSlot(refValAM); + slotManager.createConstantSlot(refValAM); AnnotationBuilder ab = new AnnotationBuilder(realTypeFactory.getProcessingEnv(), VarAnnot.class); ab.setValue("value", cs.getId()); AnnotationMirror varAnno = ab.build(); @@ -135,15 +135,15 @@ private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror dataflowAM) { } /** - * Add the bytecode default Dataflow annotation for component type of the given {@link AnnotatedArrayType}. + * Add the bytecode default RefVal annotation for component type of the given {@link AnnotatedArrayType}. * - *

For multi-dimensional array, this method will recursively add bytecode default Dataflow annotation to array's component type. + *

For multi-dimensional array, this method will recursively add bytecode default RefVal annotation to array's component type. * * @param arrayAtm the given {@link AnnotatedArrayType}, whose component type will be added the bytecode default. */ private void replaceArrayComponentATM(AnnotatedArrayType arrayAtm) { AnnotatedTypeMirror componentAtm = arrayAtm.getComponentType(); - AnnotationMirror componentAnno = DataflowUtils.genereateDataflowAnnoFromByteCode(componentAtm, + AnnotationMirror componentAnno = RefValUtils.generateRefValAnnoFromByteCode(componentAtm, this.realTypeFactory.getProcessingEnv()); replaceATM(componentAtm, componentAnno); diff --git a/src/dataflow/DataflowVisitor.java b/src/refval/RefValVisitor.java similarity index 54% rename from src/dataflow/DataflowVisitor.java rename to src/refval/RefValVisitor.java index 6de6009eb..44fc0679e 100644 --- a/src/dataflow/DataflowVisitor.java +++ b/src/refval/RefValVisitor.java @@ -1,4 +1,4 @@ -package dataflow; +package refval; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; @@ -6,14 +6,14 @@ import checkers.inference.InferenceVisitor; /** - * Don't generate any special constraint for Dataflow type system. + * Don't generate any special constraint for RefVal type system. * * @author jianchu * */ -public class DataflowVisitor extends InferenceVisitor { +public class RefValVisitor extends InferenceVisitor { - public DataflowVisitor(DataflowChecker checker, InferenceChecker ichecker, + public RefValVisitor(RefValChecker checker, InferenceChecker ichecker, BaseAnnotatedTypeFactory factory, boolean infer) { super(checker, ichecker, factory, infer); } diff --git a/src/dataflow/qual/DataFlowInferenceBottom.java b/src/refval/qual/BottomRefVal.java similarity index 75% rename from src/dataflow/qual/DataFlowInferenceBottom.java rename to src/refval/qual/BottomRefVal.java index 1f3d8e5e7..55e708213 100644 --- a/src/dataflow/qual/DataFlowInferenceBottom.java +++ b/src/refval/qual/BottomRefVal.java @@ -1,4 +1,4 @@ -package dataflow.qual; +package refval.qual; import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; @@ -9,14 +9,12 @@ import java.lang.annotation.Target; /** - * Annotation for inferring dataflow type system. + * Annotation for inferring refval type system. * @author jianchu * */ @InvisibleQualifier -@SubtypeOf({ DataFlow.class }) +@SubtypeOf({ RefVal.class }) @Target({ ElementType.TYPE_USE }) @TargetLocations({ TypeUseLocation.EXPLICIT_LOWER_BOUND }) -public @interface DataFlowInferenceBottom { - -} +public @interface BottomRefVal {} diff --git a/src/dataflow/qual/DataFlow.java b/src/refval/qual/RefVal.java similarity index 78% rename from src/dataflow/qual/DataFlow.java rename to src/refval/qual/RefVal.java index 44f4b5e86..8ab44f5fa 100644 --- a/src/dataflow/qual/DataFlow.java +++ b/src/refval/qual/RefVal.java @@ -1,4 +1,4 @@ -package dataflow.qual; +package refval.qual; import org.checkerframework.framework.qual.SubtypeOf; @@ -8,9 +8,8 @@ @Documented @Target({ ElementType.TYPE_USE, ElementType.TYPE_PARAMETER }) -@SubtypeOf({ DataFlowTop.class }) -public @interface DataFlow { +@SubtypeOf({ UnknownRefVal.class }) +public @interface RefVal { String[] typeNames() default {}; - String[] typeNameRoots() default {}; -} \ No newline at end of file +} diff --git a/src/dataflow/qual/DataFlowTop.java b/src/refval/qual/UnknownRefVal.java similarity index 90% rename from src/dataflow/qual/DataFlowTop.java rename to src/refval/qual/UnknownRefVal.java index ad9d6ae69..0d2b8821c 100644 --- a/src/dataflow/qual/DataFlowTop.java +++ b/src/refval/qual/UnknownRefVal.java @@ -1,4 +1,4 @@ -package dataflow.qual; +package refval.qual; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; import org.checkerframework.framework.qual.InvisibleQualifier; @@ -14,6 +14,4 @@ @SubtypeOf({}) @Target({ ElementType.TYPE_USE }) @TargetLocations({ TypeUseLocation.EXPLICIT_UPPER_BOUND }) -public @interface DataFlowTop { - -} \ No newline at end of file +public @interface UnknownRefVal {} diff --git a/src/dataflow/solvers/classic/DataflowResult.java b/src/refval/solvers/classic/RefValResult.java similarity index 77% rename from src/dataflow/solvers/classic/DataflowResult.java rename to src/refval/solvers/classic/RefValResult.java index 796a127d6..5c88f5c43 100644 --- a/src/dataflow/solvers/classic/DataflowResult.java +++ b/src/refval/solvers/classic/RefValResult.java @@ -1,4 +1,4 @@ -package dataflow.solvers.classic; +package refval.solvers.classic; import java.util.Collection; import java.util.HashMap; @@ -13,39 +13,39 @@ import checkers.inference.DefaultInferenceResult; import checkers.inference.InferenceMain; import checkers.inference.solver.util.PrintUtils; -import dataflow.DataflowAnnotatedTypeFactory; -import dataflow.util.DataflowUtils; +import refval.RefValAnnotatedTypeFactory; +import refval.util.RefValUtils; -public class DataflowResult extends DefaultInferenceResult { +public class RefValResult extends DefaultInferenceResult { private final Map> typeNameResults; private final Map> typeRootResults; private final Map idToExistance; - private final DataflowAnnotatedTypeFactory realTypeFactory; + private final RefValAnnotatedTypeFactory realTypeFactory; - public DataflowResult(Collection solutions, ProcessingEnvironment processingEnv) { + public RefValResult(Collection solutions, ProcessingEnvironment processingEnv) { // Legacy solver doesn't support explanation super(); this.typeNameResults = new HashMap<>(); this.typeRootResults = new HashMap<>(); this.idToExistance = new HashMap<>(); - this.realTypeFactory = (DataflowAnnotatedTypeFactory)InferenceMain.getInstance().getRealTypeFactory(); + this.realTypeFactory = (RefValAnnotatedTypeFactory)InferenceMain.getInstance().getRealTypeFactory(); mergeSolutions(solutions); createAnnotations(processingEnv); simplifyAnnotation(); PrintUtils.printSolutions(varIdToAnnotation); } - public void mergeSolutions(Collection solutions) { - for (DatatypeSolution solution : solutions) { + public void mergeSolutions(Collection solutions) { + for (RefValTypeSolution solution : solutions) { mergeSingleSolution(solution); mergeIdToExistance(solution); } } - private void mergeSingleSolution(DatatypeSolution solution) { + private void mergeSingleSolution(RefValTypeSolution solution) { for (Map.Entry entry : solution.getResult().entrySet()) { boolean shouldContainDatatype = shouldContainDatatype(entry); - String datatype = solution.getDatatype(); + String datatype = solution.getRefValType(); if (solution.isRoot()) { Set dataRoots = typeRootResults.get(entry.getKey()); if (dataRoots == null) { @@ -79,9 +79,9 @@ private void createAnnotations(ProcessingEnvironment processingEnv) { Set roots = typeRootResults.get(slotId); AnnotationMirror anno; if (roots != null) { - anno = DataflowUtils.createDataflowAnnotationWithRoots(datatypes, typeRootResults.get(slotId), processingEnv); + anno = RefValUtils.createRefValAnnotationWithRoots(datatypes, typeRootResults.get(slotId), processingEnv); } else { - anno = DataflowUtils.createDataflowAnnotation(datatypes, processingEnv); + anno = RefValUtils.createRefValAnnotation(datatypes, processingEnv); } varIdToAnnotation.put(slotId, anno); } @@ -91,7 +91,8 @@ private void createAnnotations(ProcessingEnvironment processingEnv) { Set roots = entry.getValue(); Set typeNames = typeNameResults.get(slotId); if (typeNames == null) { - AnnotationMirror anno = DataflowUtils.createDataflowAnnotationWithoutName(roots, processingEnv); + AnnotationMirror anno = RefValUtils + .createRefValAnnotationWithoutName(roots, processingEnv); varIdToAnnotation.put(slotId, anno); } } @@ -100,12 +101,12 @@ private void createAnnotations(ProcessingEnvironment processingEnv) { private void simplifyAnnotation() { for (Map.Entry entry : varIdToAnnotation.entrySet()) { - AnnotationMirror refinedDataflow = this.realTypeFactory.refineDataflow(entry.getValue()); - entry.setValue(refinedDataflow); + AnnotationMirror refinedRefVal = this.realTypeFactory.refineRefVal(entry.getValue()); + entry.setValue(refinedRefVal); } } - private void mergeIdToExistance(DatatypeSolution solution) { + private void mergeIdToExistance(RefValTypeSolution solution) { for (Map.Entry entry : solution.getResult().entrySet()) { int id = entry.getKey(); boolean existsDatatype = entry.getValue(); diff --git a/src/dataflow/solvers/classic/DataflowSerializer.java b/src/refval/solvers/classic/RefValSerializer.java similarity index 79% rename from src/dataflow/solvers/classic/DataflowSerializer.java rename to src/refval/solvers/classic/RefValSerializer.java index 2c7817e51..4d041e5c4 100644 --- a/src/dataflow/solvers/classic/DataflowSerializer.java +++ b/src/refval/solvers/classic/RefValSerializer.java @@ -1,4 +1,4 @@ -package dataflow.solvers.classic; +package refval.solvers.classic; import org.checkerframework.javacutil.AnnotationUtils; @@ -15,15 +15,15 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.serialization.CnfVecIntSerializer; -import dataflow.qual.DataFlowTop; -import dataflow.util.DataflowUtils; +import refval.qual.UnknownRefVal; +import refval.util.RefValUtils; -public class DataflowSerializer extends CnfVecIntSerializer { +public class RefValSerializer extends CnfVecIntSerializer { protected final String datatype; private final Set touchedSlots = new HashSet(); private boolean isRoot = false; - public DataflowSerializer(String datatype, boolean isRoot) { + public RefValSerializer(String datatype, boolean isRoot) { super(InferenceMain.getInstance().getSlotManager()); this.datatype = datatype; this.isRoot = isRoot; @@ -37,14 +37,14 @@ protected boolean isTop(ConstantSlot constantSlot) { } private boolean annoIsPresented(AnnotationMirror anno) { - if (AnnotationUtils.areSameByClass(anno, DataFlowTop.class)) { + if (AnnotationUtils.areSameByClass(anno, UnknownRefVal.class)) { return true; } String[] datatypes; if (this.isRoot) { - datatypes = DataflowUtils.getTypeNameRoots(anno); + datatypes = RefValUtils.getTypeNameRoots(anno); } else { - datatypes = DataflowUtils.getTypeNames(anno); + datatypes = RefValUtils.getTypeNames(anno); } return Arrays.asList(datatypes).contains(datatype); diff --git a/src/dataflow/solvers/classic/DataflowSolver.java b/src/refval/solvers/classic/RefValSolver.java similarity index 55% rename from src/dataflow/solvers/classic/DataflowSolver.java rename to src/refval/solvers/classic/RefValSolver.java index a95aa258c..bf599964c 100644 --- a/src/dataflow/solvers/classic/DataflowSolver.java +++ b/src/refval/solvers/classic/RefValSolver.java @@ -1,4 +1,4 @@ -package dataflow.solvers.classic; +package refval.solvers.classic; import java.util.ArrayList; import java.util.Collection; @@ -26,18 +26,18 @@ import checkers.inference.solver.constraintgraph.ConstraintGraph; import checkers.inference.solver.constraintgraph.GraphBuilder; import checkers.inference.solver.constraintgraph.Vertex; -import dataflow.qual.DataFlow; -import dataflow.util.DataflowUtils; +import refval.qual.RefVal; +import refval.util.RefValUtils; /** - * A solver for dataflow type system that is independent from GeneralSolver. + * A solver for refval type system that is independent from GeneralSolver. * * @author jianchu * */ -public class DataflowSolver implements InferenceSolver { +public class RefValSolver implements InferenceSolver { - protected AnnotationMirror DATAFLOW; + protected AnnotationMirror REFVAL; @Override public InferenceResult solve(Map configuration, @@ -46,32 +46,32 @@ public InferenceResult solve(Map configuration, ProcessingEnvironment processingEnvironment) { Elements elements = processingEnvironment.getElementUtils(); - DATAFLOW = AnnotationBuilder.fromClass(elements, DataFlow.class); + REFVAL = AnnotationBuilder.fromClass(elements, RefVal.class); GraphBuilder graphBuilder = new GraphBuilder(slots, constraints); ConstraintGraph constraintGraph = graphBuilder.buildGraph(); - List dataflowSolvers = new ArrayList<>(); + List refValSolvers = new ArrayList<>(); // Configure datatype solvers for (Map.Entry> entry : constraintGraph.getConstantPath().entrySet()) { AnnotationMirror anno = entry.getKey().getValue(); - if (AnnotationUtils.areSameByName(anno, DATAFLOW)) { - String[] dataflowValues = DataflowUtils.getTypeNames(anno); - String[] dataflowRoots = DataflowUtils.getTypeNameRoots(anno); - if (dataflowValues.length == 1) { - DatatypeSolver solver = new DatatypeSolver(dataflowValues[0], entry.getValue(),getSerializer(dataflowValues[0], false)); - dataflowSolvers.add(solver); - } else if (dataflowRoots.length == 1) { - DatatypeSolver solver = new DatatypeSolver(dataflowRoots[0], entry.getValue(),getSerializer(dataflowRoots[0], true)); - dataflowSolvers.add(solver); + if (AnnotationUtils.areSameByName(anno, REFVAL)) { + String[] refValValues = RefValUtils.getTypeNames(anno); + String[] refValRoots = RefValUtils.getTypeNameRoots(anno); + if (refValValues.length == 1) { + RefValTypeSolver solver = new RefValTypeSolver(refValValues[0], entry.getValue(),getSerializer(refValValues[0], false)); + refValSolvers.add(solver); + } else if (refValRoots.length == 1) { + RefValTypeSolver solver = new RefValTypeSolver(refValRoots[0], entry.getValue(),getSerializer(refValRoots[0], true)); + refValSolvers.add(solver); } } } - List solutions = new ArrayList<>(); + List solutions = new ArrayList<>(); try { - if (dataflowSolvers.size() > 0) { - solutions = solveInparallel(dataflowSolvers); + if (refValSolvers.size() > 0) { + solutions = solveInparallel(refValSolvers); } } catch (InterruptedException | ExecutionException e) { e.printStackTrace(); @@ -80,16 +80,16 @@ public InferenceResult solve(Map configuration, return getMergedResultFromSolutions(processingEnvironment, solutions); } - private List solveInparallel(List dataflowSolvers) + private List solveInparallel(List refValSolvers) throws InterruptedException, ExecutionException { - ExecutorService service = Executors.newFixedThreadPool(dataflowSolvers.size()); + ExecutorService service = Executors.newFixedThreadPool(refValSolvers.size()); - List> futures = new ArrayList>(); + List> futures = new ArrayList>(); - for (final DatatypeSolver solver : dataflowSolvers) { - Callable callable = new Callable() { + for (final RefValTypeSolver solver : refValSolvers) { + Callable callable = new Callable() { @Override - public DatatypeSolution call() throws Exception { + public RefValTypeSolution call() throws Exception { return solver.solve(); } }; @@ -97,19 +97,19 @@ public DatatypeSolution call() throws Exception { } service.shutdown(); - List solutions = new ArrayList<>(); - for (Future future : futures) { + List solutions = new ArrayList<>(); + for (Future future : futures) { solutions.add(future.get()); } return solutions; } - protected DataflowSerializer getSerializer(String datatype, boolean isRoot) { - return new DataflowSerializer(datatype, isRoot); + protected RefValSerializer getSerializer(String datatype, boolean isRoot) { + return new RefValSerializer(datatype, isRoot); } protected InferenceResult getMergedResultFromSolutions(ProcessingEnvironment processingEnvironment, - List solutions) { - return new DataflowResult(solutions, processingEnvironment); + List solutions) { + return new RefValResult(solutions, processingEnvironment); } } diff --git a/src/refval/solvers/classic/RefValTypeSolution.java b/src/refval/solvers/classic/RefValTypeSolution.java new file mode 100644 index 000000000..34a329f9c --- /dev/null +++ b/src/refval/solvers/classic/RefValTypeSolution.java @@ -0,0 +1,37 @@ +package refval.solvers.classic; + +import java.util.HashMap; +import java.util.Map; + +public class RefValTypeSolution { + private final Map result; + private final String refValType; + private final boolean isRoot; + + public RefValTypeSolution(Map result, String refValType, boolean isRoot) { + this.result = result; + this.refValType = refValType; + this.isRoot = isRoot; + } + + private RefValTypeSolution(String refValType, boolean isRoot) { + this(new HashMap(), refValType, isRoot); + } + + public Map getResult() { + return result; + } + + public String getRefValType() { + return refValType; + } + + public static RefValTypeSolution noSolution(String datatype) { + return new RefValTypeSolution(datatype, false); + } + + public boolean isRoot() { + return this.isRoot; + } + +} diff --git a/src/dataflow/solvers/classic/DatatypeSolver.java b/src/refval/solvers/classic/RefValTypeSolver.java similarity index 89% rename from src/dataflow/solvers/classic/DatatypeSolver.java rename to src/refval/solvers/classic/RefValTypeSolver.java index f8aae259b..de5e0a657 100644 --- a/src/dataflow/solvers/classic/DatatypeSolver.java +++ b/src/refval/solvers/classic/RefValTypeSolver.java @@ -1,4 +1,4 @@ -package dataflow.solvers.classic; +package refval.solvers.classic; import java.io.File; import java.io.PrintWriter; @@ -14,13 +14,13 @@ import checkers.inference.SlotManager; import checkers.inference.model.Constraint; -public class DatatypeSolver { +public class RefValTypeSolver { private final SlotManager slotManager; private final String datatype; - private final DataflowSerializer serializer; + private final RefValSerializer serializer; private final List clauses; - public DatatypeSolver(String datatype, Collection constraints, DataflowSerializer serializer) { + public RefValTypeSolver(String datatype, Collection constraints, RefValSerializer serializer) { this.datatype = datatype; this.serializer = serializer; this.slotManager = InferenceMain.getInstance().getSlotManager(); @@ -59,7 +59,7 @@ private List convertToCNF(Collection constraints) { return serializer.convertAll(constraints); } - public DatatypeSolution solve() { + public RefValTypeSolution solve() { Map idToExistence = new HashMap<>(); Map result = new HashMap<>(); @@ -102,13 +102,13 @@ public DatatypeSolution solve() { // means this top(type) should present: // If the solution is false, that means top was // inferred. - // For dataflow, that means that the annotation should + // For refval, that means that the annotation should // have the type. result.put(var, !varIsTrue); } } // System.out.println("*******************************"); - return new DatatypeSolution(result, datatype, this.serializer.isRoot()); + return new RefValTypeSolution(result, datatype, this.serializer.isRoot()); } } catch (Throwable th) { @@ -116,6 +116,6 @@ public DatatypeSolution solve() { throw new RuntimeException("Error MAX-SAT solving! " + lastClause, th); } - return DatatypeSolution.noSolution(datatype); + return RefValTypeSolution.noSolution(datatype); } } diff --git a/src/dataflow/solvers/general/DataflowGraphSolvingStrategy.java b/src/refval/solvers/general/RefValGraphSolvingStrategy.java similarity index 63% rename from src/dataflow/solvers/general/DataflowGraphSolvingStrategy.java rename to src/refval/solvers/general/RefValGraphSolvingStrategy.java index f185a5e0a..871fb86c6 100644 --- a/src/dataflow/solvers/general/DataflowGraphSolvingStrategy.java +++ b/src/refval/solvers/general/RefValGraphSolvingStrategy.java @@ -1,4 +1,4 @@ -package dataflow.solvers.general; +package refval.solvers.general; import java.util.ArrayList; import java.util.Collection; @@ -29,20 +29,19 @@ import checkers.inference.solver.frontend.LatticeBuilder; import checkers.inference.solver.frontend.TwoQualifiersLattice; import checkers.inference.solver.strategy.GraphSolvingStrategy; -import checkers.inference.solver.util.PrintUtils; import checkers.inference.solver.util.SolverEnvironment; import checkers.inference.solver.util.Statistics; -import dataflow.DataflowAnnotatedTypeFactory; -import dataflow.qual.DataFlow; -import dataflow.qual.DataFlowInferenceBottom; -import dataflow.qual.DataFlowTop; -import dataflow.util.DataflowUtils; +import refval.RefValAnnotatedTypeFactory; +import refval.qual.RefVal; +import refval.qual.BottomRefVal; +import refval.qual.UnknownRefVal; +import refval.util.RefValUtils; -public class DataflowGraphSolvingStrategy extends GraphSolvingStrategy { +public class RefValGraphSolvingStrategy extends GraphSolvingStrategy { protected ProcessingEnvironment processingEnvironment; - public DataflowGraphSolvingStrategy(SolverFactory solverFactory) { + public RefValGraphSolvingStrategy(SolverFactory solverFactory) { super(solverFactory); } @@ -56,27 +55,27 @@ public InferenceResult solve(SolverEnvironment solverEnvironment, Collection> separateGraph(SolverEnvironment solverEnvironment, ConstraintGraph constraintGraph, Collection slots, Collection constraints, Lattice lattice) { - AnnotationMirror DATAFLOW = AnnotationBuilder.fromClass(processingEnvironment.getElementUtils(), DataFlow.class); - AnnotationMirror DATAFLOWBOTTOM = AnnotationBuilder.fromClass(processingEnvironment.getElementUtils(), - DataFlowInferenceBottom.class); + AnnotationMirror REFVAL = AnnotationBuilder.fromClass(processingEnvironment.getElementUtils(), RefVal.class); + AnnotationMirror BOTTOMREFVAL = AnnotationBuilder.fromClass(processingEnvironment.getElementUtils(), + BottomRefVal.class); List> solvers = new ArrayList<>(); Statistics.addOrIncrementEntry("graph_size", constraintGraph.getConstantPath().size()); for (Map.Entry> entry : constraintGraph.getConstantPath().entrySet()) { AnnotationMirror anno = entry.getKey().getValue(); - if (AnnotationUtils.areSameByName(anno, DATAFLOW)) { - String[] dataflowValues = DataflowUtils.getTypeNames(anno); - String[] dataflowRoots = DataflowUtils.getTypeNameRoots(anno); - if (dataflowValues.length == 1) { - AnnotationMirror DATAFLOWTOP = DataflowUtils.createDataflowAnnotation( - DataflowUtils.convert(dataflowValues), processingEnvironment); - TwoQualifiersLattice latticeFor2 = new LatticeBuilder().buildTwoTypeLattice(DATAFLOWTOP, DATAFLOWBOTTOM); + if (AnnotationUtils.areSameByName(anno, REFVAL)) { + String[] refValValues = RefValUtils.getTypeNames(anno); + String[] refValRoots = RefValUtils.getTypeNameRoots(anno); + if (refValValues.length == 1) { + AnnotationMirror UNKNOWNREFVAL = RefValUtils.createRefValAnnotation( + RefValUtils.convert(refValValues), processingEnvironment); + TwoQualifiersLattice latticeFor2 = new LatticeBuilder().buildTwoTypeLattice(UNKNOWNREFVAL, BOTTOMREFVAL); solvers.add(solverFactory.createSolver(solverEnvironment, slots, entry.getValue(), latticeFor2)); - } else if (dataflowRoots.length == 1) { - AnnotationMirror DATAFLOWTOP = DataflowUtils.createDataflowAnnotationForByte( - DataflowUtils.convert(dataflowRoots), processingEnvironment); - TwoQualifiersLattice latticeFor2 = new LatticeBuilder().buildTwoTypeLattice(DATAFLOWTOP, DATAFLOWBOTTOM); + } else if (refValRoots.length == 1) { + AnnotationMirror UNKNOWNREFVAL = RefValUtils.createRefValAnnotationForByte( + RefValUtils.convert(refValRoots), processingEnvironment); + TwoQualifiersLattice latticeFor2 = new LatticeBuilder().buildTwoTypeLattice(UNKNOWNREFVAL, BOTTOMREFVAL); solvers.add(solverFactory.createSolver(solverEnvironment, slots, entry.getValue(), latticeFor2)); } } @@ -88,9 +87,9 @@ protected List> separateGraph(SolverEnvironment solverEnvironment, Con @Override protected ConstraintGraph generateGraph(Collection slots, Collection constraints, ProcessingEnvironment processingEnvironment) { - AnnotationMirror DATAFLOWTOP = AnnotationBuilder.fromClass( - processingEnvironment.getElementUtils(), DataFlowTop.class); - GraphBuilder graphBuilder = new GraphBuilder(slots, constraints, DATAFLOWTOP); + AnnotationMirror UNKNOWNREFVAL = AnnotationBuilder.fromClass( + processingEnvironment.getElementUtils(), UnknownRefVal.class); + GraphBuilder graphBuilder = new GraphBuilder(slots, constraints, UNKNOWNREFVAL); ConstraintGraph constraintGraph = graphBuilder.buildGraph(); return constraintGraph; } @@ -98,21 +97,21 @@ protected ConstraintGraph generateGraph(Collection slots, Collection, Collection>> inferenceResults) { Map solutions = new HashMap<>(); - Map> dataflowResults = new HashMap<>(); + Map> refValResults = new HashMap<>(); for (Pair, Collection> inferenceResult : inferenceResults) { Map inferenceSolutionMap = inferenceResult.fst; if (inferenceResult.fst != null) { for (Map.Entry entry : inferenceSolutionMap.entrySet()) { Integer id = entry.getKey(); - AnnotationMirror dataflowAnno = entry.getValue(); - if (AnnotationUtils.areSameByClass(dataflowAnno, DataFlow.class)) { - Set datas = dataflowResults.get(id); + AnnotationMirror refValAnno = entry.getValue(); + if (AnnotationUtils.areSameByClass(refValAnno, RefVal.class)) { + Set datas = refValResults.get(id); if (datas == null) { datas = AnnotationUtils.createAnnotationSet(); - dataflowResults.put(id, datas); + refValResults.put(id, datas); } - datas.add(dataflowAnno); + datas.add(refValAnno); } } } else { @@ -121,12 +120,12 @@ protected InferenceResult mergeInferenceResults(List> entry : dataflowResults.entrySet()) { + for (Map.Entry> entry : refValResults.entrySet()) { Set dataTypes = new HashSet(); Set dataRoots = new HashSet(); for (AnnotationMirror anno : entry.getValue()) { - String[] dataTypesArr = DataflowUtils.getTypeNames(anno); - String[] dataRootsArr = DataflowUtils.getTypeNameRoots(anno); + String[] dataTypesArr = RefValUtils.getTypeNames(anno); + String[] dataRootsArr = RefValUtils.getTypeNameRoots(anno); if (dataTypesArr.length == 1) { dataTypes.add(dataTypesArr[0]); } @@ -134,14 +133,14 @@ protected InferenceResult mergeInferenceResults(List entry : solutions.entrySet()) { - AnnotationMirror refinedDataflow = ((DataflowAnnotatedTypeFactory) InferenceMain - .getInstance().getRealTypeFactory()).refineDataflow(entry.getValue()); - entry.setValue(refinedDataflow); + AnnotationMirror refinedRefVal = ((RefValAnnotatedTypeFactory) InferenceMain + .getInstance().getRealTypeFactory()).refineRefVal(entry.getValue()); + entry.setValue(refinedRefVal); } Statistics.addOrIncrementEntry("annotation_size", solutions.size()); diff --git a/src/dataflow/solvers/general/DataflowSolverEngine.java b/src/refval/solvers/general/RefValSolverEngine.java similarity index 66% rename from src/dataflow/solvers/general/DataflowSolverEngine.java rename to src/refval/solvers/general/RefValSolverEngine.java index 89fd99dd0..044a97324 100644 --- a/src/dataflow/solvers/general/DataflowSolverEngine.java +++ b/src/refval/solvers/general/RefValSolverEngine.java @@ -1,4 +1,4 @@ -package dataflow.solvers.general; +package refval.solvers.general; import checkers.inference.InferenceMain; import checkers.inference.solver.SolverEngine; @@ -8,23 +8,23 @@ import checkers.inference.solver.util.NameUtils; /** - * DataflowGeneralSolver is the solver for dataflow type system. It encode - * dataflow type hierarchy as two qualifiers type system. + * RefValSolverEngine is the solver for RefVal type system. It encode + * RefVal type hierarchy as two qualifiers type system. * * @author jianchu * */ -public class DataflowSolverEngine extends SolverEngine { +public class RefValSolverEngine extends SolverEngine { @Override protected SolvingStrategy createSolvingStrategy(SolverFactory solverFactory) { - return new DataflowGraphSolvingStrategy(solverFactory); + return new RefValGraphSolvingStrategy(solverFactory); } @Override protected void sanitizeSolverEngineArgs() { if (!NameUtils.getStrategyName(GraphSolvingStrategy.class).equals(strategyName)) { - InferenceMain.getInstance().logger.warning("Dataflow type system must use graph solve strategy." + InferenceMain.getInstance().logger.warning("RefVal type system must use graph solve strategy." + "Change strategy from " + strategyName + " to graph."); strategyName = NameUtils.getStrategyName(GraphSolvingStrategy.class); } diff --git a/src/refval/util/RefValUtils.java b/src/refval/util/RefValUtils.java new file mode 100644 index 000000000..359f5b7f6 --- /dev/null +++ b/src/refval/util/RefValUtils.java @@ -0,0 +1,202 @@ +package refval.util; + +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; + +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; + +import com.sun.source.tree.LiteralTree; + +import refval.qual.RefVal; + +/** + * Utility class for RefVal type system. + * + * @author jianchu + * + */ +public class RefValUtils { + + public static String[] getTypeNames(AnnotationMirror type) { + return getReferenceValue(type, "typeNames"); + } + + public static String[] getTypeNameRoots(AnnotationMirror type) { + return getReferenceValue(type, "typeNameRoots"); + } + + private static String[] getReferenceValue(AnnotationMirror type, String valueName) { + List allTypesList = AnnotationUtils.getElementValueArray(type, valueName, String.class, + true); + // types in this list is org.checkerframework.framework.util.AnnotationBuilder. + String[] allTypesInArray = new String[allTypesList.size()]; + int i = 0; + for (Object o : allTypesList) { + allTypesInArray[i] = o.toString(); + i++; + } + return allTypesInArray; + } + + public static AnnotationMirror createRefValAnnotationForByte(String[] refValType, + ProcessingEnvironment processingEnv) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, RefVal.class); + builder.setValue("typeNameRoots", refValType); + return builder.build(); + } + + private static AnnotationMirror createRefValAnnotation(final Set refValTypes, + final AnnotationBuilder builder) { + String[] refValTypesInArray = new String[refValTypes.size()]; + int i = 0; + for (String refValType : refValTypes) { + refValTypesInArray[i] = refValType.toString(); + i++; + } + builder.setValue("typeNames", refValTypesInArray); + return builder.build(); + } + + private static AnnotationMirror createRefValAnnotationWithoutName(final Set roots, + final AnnotationBuilder builder) { + String[] refValTypesInArray = new String[roots.size()]; + int i = 0; + for (String refValType : roots) { + refValTypesInArray[i] = refValType.toString(); + i++; + } + builder.setValue("typeNameRoots", refValTypesInArray); + return builder.build(); + } + + public static AnnotationMirror createRefValAnnotation(Set refValTypes, + ProcessingEnvironment processingEnv) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, RefVal.class); + + return createRefValAnnotation(refValTypes, builder); + } + + public static AnnotationMirror createRefValAnnotationWithoutName(Set roots, + ProcessingEnvironment processingEnv) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, RefVal.class); + return createRefValAnnotationWithoutName(roots, builder); + + } + + public static AnnotationMirror createRefValAnnotation(String[] refValType, + ProcessingEnvironment processingEnv) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, RefVal.class); + builder.setValue("typeNames", refValType); + return builder.build(); + } + + public static AnnotationMirror createRefValAnnotationWithRoots(Set refValTypes, + Set refValTypesRoots, ProcessingEnvironment processingEnv) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, RefVal.class); + return createRefValAnnotationWithRoots(refValTypes, refValTypesRoots, builder); + } + + private static AnnotationMirror createRefValAnnotationWithRoots(final Set refValTypes, + final Set refValTypesRoots, final AnnotationBuilder builder) { + String[] refValTypesInArray = new String[refValTypes.size()]; + int i = 0; + for (String refValType : refValTypes) { + refValTypesInArray[i] = refValType.toString(); + i++; + } + + String[] refValTypesRootInArray = new String[refValTypesRoots.size()]; + int j = 0; + for (String refValTypesRoot : refValTypesRoots) { + refValTypesRootInArray[j] = refValTypesRoot.toString(); + j++; + } + if (refValTypesRootInArray.length > 0) { + builder.setValue("typeNameRoots", refValTypesRootInArray); + } + if (refValTypesInArray.length > 0) { + builder.setValue("typeNames", refValTypesInArray); + } + + return builder.build(); + } + + public static AnnotationMirror generateRefValAnnoFromNewClass(AnnotatedTypeMirror type, + ProcessingEnvironment processingEnv) { + TypeMirror tm = type.getUnderlyingType(); + String className = tm.toString(); + AnnotationMirror refValType = createRefValAnnotation(convert(className), processingEnv); + return refValType; + } + + public static AnnotationMirror generateRefValAnnoFromByteCode(AnnotatedTypeMirror type, + ProcessingEnvironment processingEnv) { + TypeMirror tm = type.getUnderlyingType(); + String className = tm.toString(); + AnnotationMirror refValType = createRefValAnnotationForByte(convert(className), + processingEnv); + return refValType; + } + + public static AnnotationMirror generateRefValAnnoFromLiteral(AnnotatedTypeMirror type, + ProcessingEnvironment processingEnv) { + String refValTypeInArray[] = convert(type.getUnderlyingType().toString()); + AnnotationMirror refValType = createRefValAnnotation(refValTypeInArray, processingEnv); + return refValType; + } + + public static AnnotationMirror generateRefValAnnoFromLiteral(LiteralTree node, + ProcessingEnvironment processingEnv) { + String refValTypeInArray[] = { "" }; + switch (node.getKind()) { + case STRING_LITERAL: + refValTypeInArray = convert(String.class.toString().split(" ")[1]); + break; + case INT_LITERAL: + refValTypeInArray = convert(int.class.toString()); + break; + case LONG_LITERAL: + refValTypeInArray = convert(long.class.toString()); + break; + case FLOAT_LITERAL: + refValTypeInArray = convert(float.class.toString()); + break; + case DOUBLE_LITERAL: + refValTypeInArray = convert(double.class.toString()); + break; + case BOOLEAN_LITERAL: + refValTypeInArray = convert(boolean.class.toString()); + break; + case CHAR_LITERAL: + refValTypeInArray = convert(char.class.toString()); + break; + case NULL_LITERAL: + // Null literal wouldn't be passed here. + break; + default: + throw new BugInCF("Unknown literal tree: " + node.getKind().toString()); + } + AnnotationMirror refValType = createRefValAnnotation(refValTypeInArray, processingEnv); + return refValType; + } + + public static String[] convert(String... typeName) { + return typeName; + } + + public static AnnotationMirror createRefValAnnotation(String typeName, + ProcessingEnvironment processingEnv) { + Set typeNames = new HashSet(); + typeNames.add(typeName); + AnnotationMirror am = RefValUtils.createRefValAnnotation(typeNames, processingEnv); + return am; + } +} diff --git a/testing/dataflow-not-inferrable-test/TestCharInvalid.java b/testing/dataflow-not-inferrable-test/TestCharInvalid.java deleted file mode 100644 index 407c636e5..000000000 --- a/testing/dataflow-not-inferrable-test/TestCharInvalid.java +++ /dev/null @@ -1,7 +0,0 @@ -import dataflow.qual.DataFlow; - -public class TestCharInvalid { - - // :: error: (assignment.type.incompatible) - @DataFlow(typeNames = {"int"}) char invalidChar = 'L'; -} diff --git a/testing/dataflow-not-inferrable-test/TestDoubleInvalid.java b/testing/dataflow-not-inferrable-test/TestDoubleInvalid.java deleted file mode 100644 index 2859c5150..000000000 --- a/testing/dataflow-not-inferrable-test/TestDoubleInvalid.java +++ /dev/null @@ -1,7 +0,0 @@ -import dataflow.qual.DataFlow; - -public class TestDoubleInvalid { - - // :: error: (assignment.type.incompatible) - @DataFlow(typeNames = {"int"}) double invalidDouble = 3.14; -} diff --git a/testing/dataflow-not-inferrable-test/TestIntInvalid.java b/testing/dataflow-not-inferrable-test/TestIntInvalid.java deleted file mode 100644 index ebcebf50b..000000000 --- a/testing/dataflow-not-inferrable-test/TestIntInvalid.java +++ /dev/null @@ -1,7 +0,0 @@ -import dataflow.qual.DataFlow; - -public class TestIntInvalid { - - // :: error: (assignment.type.incompatible) - @DataFlow(typeNames = {"float"}) int invalidInteger = 3; -} diff --git a/testing/dataflow-not-inferrable-test/TestNewInvalid.java b/testing/dataflow-not-inferrable-test/TestNewInvalid.java deleted file mode 100644 index 1c896b41f..000000000 --- a/testing/dataflow-not-inferrable-test/TestNewInvalid.java +++ /dev/null @@ -1,9 +0,0 @@ -import dataflow.qual.DataFlow; - -import java.util.ArrayList; - -public class TestNewInvalid { - - // :: error: (assignment.type.incompatible) - @DataFlow(typeNames = {"java.util.List"}) ArrayList invalidNew = new ArrayList(); -} diff --git a/testing/dataflow-not-inferrable-test/TestStringInvalid.java b/testing/dataflow-not-inferrable-test/TestStringInvalid.java deleted file mode 100644 index cef5c8db6..000000000 --- a/testing/dataflow-not-inferrable-test/TestStringInvalid.java +++ /dev/null @@ -1,7 +0,0 @@ -import dataflow.qual.DataFlow; - -public class TestStringInvalid { - - // :: error: (assignment.type.incompatible) - @DataFlow(typeNames = {"java.lang.Object"}) String invalidString = "I am a String!"; -} diff --git a/testing/dataflowexample/build.xml b/testing/refval-example/build.xml similarity index 100% rename from testing/dataflowexample/build.xml rename to testing/refval-example/build.xml diff --git a/testing/dataflowexample/cleanup.sh b/testing/refval-example/cleanup.sh similarity index 100% rename from testing/dataflowexample/cleanup.sh rename to testing/refval-example/cleanup.sh diff --git a/testing/dataflowexample/libs/src/Foo.java b/testing/refval-example/libs/src/Foo.java similarity index 100% rename from testing/dataflowexample/libs/src/Foo.java rename to testing/refval-example/libs/src/Foo.java diff --git a/testing/dataflowexample/project/src/Bar.java b/testing/refval-example/project/src/Bar.java similarity index 100% rename from testing/dataflowexample/project/src/Bar.java rename to testing/refval-example/project/src/Bar.java diff --git a/testing/dataflowexample/runLingelingSolver.sh b/testing/refval-example/runLingelingSolver.sh similarity index 91% rename from testing/dataflowexample/runLingelingSolver.sh rename to testing/refval-example/runLingelingSolver.sh index 510c95b57..fd82170ae 100755 --- a/testing/dataflowexample/runLingelingSolver.sh +++ b/testing/refval-example/runLingelingSolver.sh @@ -9,7 +9,7 @@ DLJC=$JSR308/do-like-javac ( cd $WORKING_DIR && \ $DLJC/dljc -t inference \ --guess --crashExit \ - --checker dataflow.DataflowChecker \ + --checker refval.RefValChecker \ --solver checkers.inference.solver.SolverEngine \ --solverArgs="solvingStrategy=Graph,solver=Lingeling" \ --mode ROUNDTRIP -o $WORKING_DIR/logs \ diff --git a/testing/dataflowexample/runMaxSatSolver.sh b/testing/refval-example/runMaxSatSolver.sh similarity index 91% rename from testing/dataflowexample/runMaxSatSolver.sh rename to testing/refval-example/runMaxSatSolver.sh index 70c408945..1be5b3e81 100755 --- a/testing/dataflowexample/runMaxSatSolver.sh +++ b/testing/refval-example/runMaxSatSolver.sh @@ -9,7 +9,7 @@ DLJC=$JSR308/do-like-javac ( cd $WORKING_DIR && \ $DLJC/dljc -t inference \ --guess --crashExit \ - --checker dataflow.DataflowChecker \ + --checker refval.RefValChecker \ --solver checkers.inference.solver.SolverEngine \ --solverArgs="solvingStrategy=Graph,solver=MaxSat" \ --mode ROUNDTRIP -o $WORKING_DIR/logs \ diff --git a/testing/dataflowexample/runDataflowSolver.sh b/testing/refval-example/runRefValSolver.sh similarity index 75% rename from testing/dataflowexample/runDataflowSolver.sh rename to testing/refval-example/runRefValSolver.sh index ae1c69ad7..bf2292a26 100755 --- a/testing/dataflowexample/runDataflowSolver.sh +++ b/testing/refval-example/runRefValSolver.sh @@ -10,7 +10,7 @@ cd $WORKING_DIR $DLJC/dljc -t inference \ --guess --crashExit \ - --checker dataflow.DataflowChecker \ - --solver dataflow.solvers.classic.DataflowSolver \ + --checker refval.RefValChecker \ + --solver refval.solvers.classic.RefValSolver \ --mode ROUNDTRIP -o $WORKING_DIR/logs \ -afud $WORKING_DIR/annotated -- ant compile-project diff --git a/testing/dataflowexample/travis-test.sh b/testing/refval-example/travis-test.sh similarity index 85% rename from testing/dataflowexample/travis-test.sh rename to testing/refval-example/travis-test.sh index f23a7a8e6..3cda95246 100755 --- a/testing/dataflowexample/travis-test.sh +++ b/testing/refval-example/travis-test.sh @@ -14,9 +14,9 @@ export PATH=$LINGELING:$AFU/scripts:$PATH ## Build libs for test (cd $WORKING_DIR && ant compile-libs) -# test using basic dataflow solver -echo -e "\nRunning DataflowSolver\n" -$WORKING_DIR/runDataflowSolver.sh +# test using basic RefVal solver +echo -e "\nRunning RefValSolver\n" +$WORKING_DIR/runRefValSolver.sh $WORKING_DIR/cleanup.sh # test using maxsat (internal) solver diff --git a/testing/dataflow-inferrable-test/TestByteCode.java b/testing/refval-inferrable-test/TestByteCode.java similarity index 100% rename from testing/dataflow-inferrable-test/TestByteCode.java rename to testing/refval-inferrable-test/TestByteCode.java diff --git a/testing/dataflow-inferrable-test/TestByteCodeMethodArrayComponentType.java b/testing/refval-inferrable-test/TestByteCodeMethodArrayComponentType.java similarity index 86% rename from testing/dataflow-inferrable-test/TestByteCodeMethodArrayComponentType.java rename to testing/refval-inferrable-test/TestByteCodeMethodArrayComponentType.java index d65ae1fb1..76b37fc9b 100644 --- a/testing/dataflow-inferrable-test/TestByteCodeMethodArrayComponentType.java +++ b/testing/refval-inferrable-test/TestByteCodeMethodArrayComponentType.java @@ -5,13 +5,13 @@ import java.util.regex.Matcher; import java.util.regex.Pattern; -import dataflow.qual.DataFlow; +import refval.qual.RefVal; class TestByteCodeMethodArrayComponentType { public void test(String path) { // :: fixable-error: (assignment.type.incompatible) - @DataFlow(typeNameRoots = {"java.lang.String"}) String str = getPath(path); + @RefVal(typeNameRoots = {"java.lang.String"}) String str = getPath(path); } public String getPath(String pathPart) { diff --git a/testing/dataflow-inferrable-test/TestChar.java b/testing/refval-inferrable-test/TestChar.java similarity index 100% rename from testing/dataflow-inferrable-test/TestChar.java rename to testing/refval-inferrable-test/TestChar.java diff --git a/testing/dataflow-inferrable-test/TestCollectionType.java b/testing/refval-inferrable-test/TestCollectionType.java similarity index 100% rename from testing/dataflow-inferrable-test/TestCollectionType.java rename to testing/refval-inferrable-test/TestCollectionType.java diff --git a/testing/dataflow-inferrable-test/TestDouble.java b/testing/refval-inferrable-test/TestDouble.java similarity index 100% rename from testing/dataflow-inferrable-test/TestDouble.java rename to testing/refval-inferrable-test/TestDouble.java diff --git a/testing/dataflow-inferrable-test/TestInt.java b/testing/refval-inferrable-test/TestInt.java similarity index 100% rename from testing/dataflow-inferrable-test/TestInt.java rename to testing/refval-inferrable-test/TestInt.java diff --git a/testing/dataflow-inferrable-test/TestList.java b/testing/refval-inferrable-test/TestList.java similarity index 100% rename from testing/dataflow-inferrable-test/TestList.java rename to testing/refval-inferrable-test/TestList.java diff --git a/testing/dataflow-inferrable-test/TestNew.java b/testing/refval-inferrable-test/TestNew.java similarity index 100% rename from testing/dataflow-inferrable-test/TestNew.java rename to testing/refval-inferrable-test/TestNew.java diff --git a/testing/dataflow-inferrable-test/TestString.java b/testing/refval-inferrable-test/TestString.java similarity index 100% rename from testing/dataflow-inferrable-test/TestString.java rename to testing/refval-inferrable-test/TestString.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound1.java b/testing/refval-inferrable-test/TestUpperBound1.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound1.java rename to testing/refval-inferrable-test/TestUpperBound1.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound2.java b/testing/refval-inferrable-test/TestUpperBound2.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound2.java rename to testing/refval-inferrable-test/TestUpperBound2.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound3.java b/testing/refval-inferrable-test/TestUpperBound3.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound3.java rename to testing/refval-inferrable-test/TestUpperBound3.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound4.java b/testing/refval-inferrable-test/TestUpperBound4.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound4.java rename to testing/refval-inferrable-test/TestUpperBound4.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound5.java b/testing/refval-inferrable-test/TestUpperBound5.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound5.java rename to testing/refval-inferrable-test/TestUpperBound5.java diff --git a/testing/dataflow-inferrable-test/TestUpperBound6.java b/testing/refval-inferrable-test/TestUpperBound6.java similarity index 100% rename from testing/dataflow-inferrable-test/TestUpperBound6.java rename to testing/refval-inferrable-test/TestUpperBound6.java diff --git a/testing/refval-not-inferrable-test/TestCharInvalid.java b/testing/refval-not-inferrable-test/TestCharInvalid.java new file mode 100644 index 000000000..f4b8ed7f5 --- /dev/null +++ b/testing/refval-not-inferrable-test/TestCharInvalid.java @@ -0,0 +1,7 @@ +import refval.qual.RefVal; + +public class TestCharInvalid { + + // :: error: (assignment.type.incompatible) + @RefVal(typeNames = {"int"}) char invalidChar = 'L'; +} diff --git a/testing/dataflow-not-inferrable-test/TestCollectionTypeInvalid.java b/testing/refval-not-inferrable-test/TestCollectionTypeInvalid.java similarity index 66% rename from testing/dataflow-not-inferrable-test/TestCollectionTypeInvalid.java rename to testing/refval-not-inferrable-test/TestCollectionTypeInvalid.java index 4afcc25f5..efc50d68a 100644 --- a/testing/dataflow-not-inferrable-test/TestCollectionTypeInvalid.java +++ b/testing/refval-not-inferrable-test/TestCollectionTypeInvalid.java @@ -1,10 +1,10 @@ import java.util.ArrayList; -import dataflow.qual.DataFlow; +import refval.qual.RefVal; public class TestCollectionTypeInvalid { - @DataFlow(typeNames = {"java.util.ArrayList"}) + @RefVal(typeNames = {"java.util.ArrayList"}) // :: error: (assignment.type.incompatible) ArrayList invalidCollection = new ArrayList(); } diff --git a/testing/refval-not-inferrable-test/TestDoubleInvalid.java b/testing/refval-not-inferrable-test/TestDoubleInvalid.java new file mode 100644 index 000000000..a86dbbb93 --- /dev/null +++ b/testing/refval-not-inferrable-test/TestDoubleInvalid.java @@ -0,0 +1,7 @@ +import refval.qual.RefVal; + +public class TestDoubleInvalid { + + // :: error: (assignment.type.incompatible) + @RefVal(typeNames = {"int"}) double invalidDouble = 3.14; +} diff --git a/testing/refval-not-inferrable-test/TestIntInvalid.java b/testing/refval-not-inferrable-test/TestIntInvalid.java new file mode 100644 index 000000000..b00bf79b6 --- /dev/null +++ b/testing/refval-not-inferrable-test/TestIntInvalid.java @@ -0,0 +1,7 @@ +import refval.qual.RefVal; + +public class TestIntInvalid { + + // :: error: (assignment.type.incompatible) + @RefVal(typeNames = {"float"}) int invalidInteger = 3; +} diff --git a/testing/refval-not-inferrable-test/TestNewInvalid.java b/testing/refval-not-inferrable-test/TestNewInvalid.java new file mode 100644 index 000000000..cbe665115 --- /dev/null +++ b/testing/refval-not-inferrable-test/TestNewInvalid.java @@ -0,0 +1,9 @@ +import refval.qual.RefVal; + +import java.util.ArrayList; + +public class TestNewInvalid { + + // :: error: (assignment.type.incompatible) + @RefVal(typeNames = {"java.util.List"}) ArrayList invalidNew = new ArrayList(); +} diff --git a/testing/refval-not-inferrable-test/TestStringInvalid.java b/testing/refval-not-inferrable-test/TestStringInvalid.java new file mode 100644 index 000000000..99e7c956a --- /dev/null +++ b/testing/refval-not-inferrable-test/TestStringInvalid.java @@ -0,0 +1,7 @@ +import refval.qual.RefVal; + +public class TestStringInvalid { + + // :: error: (assignment.type.incompatible) + @RefVal(typeNames = {"java.lang.Object"}) String invalidString = "I am a String!"; +} diff --git a/testing/dataflow-not-inferrable-test/TestUpperBound1Invalid.java b/testing/refval-not-inferrable-test/TestUpperBound1Invalid.java similarity index 66% rename from testing/dataflow-not-inferrable-test/TestUpperBound1Invalid.java rename to testing/refval-not-inferrable-test/TestUpperBound1Invalid.java index fc7ed8db3..af5f2b021 100644 --- a/testing/dataflow-not-inferrable-test/TestUpperBound1Invalid.java +++ b/testing/refval-not-inferrable-test/TestUpperBound1Invalid.java @@ -1,8 +1,8 @@ -import dataflow.qual.DataFlow; +import refval.qual.RefVal; public class TestUpperBound1Invalid { - public @DataFlow(typeNames = {"float"}) + public @RefVal(typeNames = {"float"}) int invalidUpperBound(int c) { // :: error: (return.type.incompatible) return 3; diff --git a/testing/dataflow-not-inferrable-test/TestUpperBound2Invalid.java b/testing/refval-not-inferrable-test/TestUpperBound2Invalid.java similarity index 66% rename from testing/dataflow-not-inferrable-test/TestUpperBound2Invalid.java rename to testing/refval-not-inferrable-test/TestUpperBound2Invalid.java index a277fb232..c0ae2d6e8 100644 --- a/testing/dataflow-not-inferrable-test/TestUpperBound2Invalid.java +++ b/testing/refval-not-inferrable-test/TestUpperBound2Invalid.java @@ -1,8 +1,8 @@ -import dataflow.qual.DataFlow; +import refval.qual.RefVal; public class TestUpperBound2Invalid { - public @DataFlow(typeNames = {"java.lang.Object"}) + public @RefVal(typeNames = {"java.lang.Object"}) Object invalidUpperBound(int c) { // :: error: (return.type.incompatible) return "I am a String!"; diff --git a/testing/dataflow-not-inferrable-test/TestUpperBound3Invalid.java b/testing/refval-not-inferrable-test/TestUpperBound3Invalid.java similarity index 70% rename from testing/dataflow-not-inferrable-test/TestUpperBound3Invalid.java rename to testing/refval-not-inferrable-test/TestUpperBound3Invalid.java index 544a5a1fb..cebbc74d8 100644 --- a/testing/dataflow-not-inferrable-test/TestUpperBound3Invalid.java +++ b/testing/refval-not-inferrable-test/TestUpperBound3Invalid.java @@ -1,8 +1,8 @@ -import dataflow.qual.DataFlow; +import refval.qual.RefVal; public class TestUpperBound3Invalid { - public @DataFlow(typeNames = {"float", "java.lang.String"}) + public @RefVal(typeNames = {"float", "java.lang.String"}) Object invalidUpperBound(int c) { if (c > 0) { // :: error: (return.type.incompatible) diff --git a/testing/dataflow-not-inferrable-test/TestUpperBound4Invalid.java b/testing/refval-not-inferrable-test/TestUpperBound4Invalid.java similarity index 77% rename from testing/dataflow-not-inferrable-test/TestUpperBound4Invalid.java rename to testing/refval-not-inferrable-test/TestUpperBound4Invalid.java index b5a4fd21e..6a21c1f87 100644 --- a/testing/dataflow-not-inferrable-test/TestUpperBound4Invalid.java +++ b/testing/refval-not-inferrable-test/TestUpperBound4Invalid.java @@ -1,8 +1,8 @@ -import dataflow.qual.DataFlow; +import refval.qual.RefVal; public class TestUpperBound4Invalid { - public @DataFlow(typeNames = {"java.lang.Object"}) + public @RefVal(typeNames = {"java.lang.Object"}) Object invalidUpperBound(int c) { if (c > 0) { // :: error: (return.type.incompatible) diff --git a/tests/checkers/inference/DataflowInferenceTest.java b/tests/checkers/inference/RefValInferenceTest.java similarity index 68% rename from tests/checkers/inference/DataflowInferenceTest.java rename to tests/checkers/inference/RefValInferenceTest.java index bb530736f..d74713c2e 100644 --- a/tests/checkers/inference/DataflowInferenceTest.java +++ b/tests/checkers/inference/RefValInferenceTest.java @@ -9,18 +9,20 @@ import org.junit.runners.Parameterized.Parameters; import checkers.inference.test.CFInferenceTest; -import dataflow.solvers.general.DataflowSolverEngine; -public class DataflowInferenceTest extends CFInferenceTest { +import refval.RefValChecker; +import refval.solvers.general.RefValSolverEngine; - public DataflowInferenceTest(File testFile) { - super(testFile, dataflow.DataflowChecker.class, "dataflow", +public class RefValInferenceTest extends CFInferenceTest { + + public RefValInferenceTest(File testFile) { + super(testFile, RefValChecker.class, "refval", "-Anomsgtext", "-d", "tests/build/outputdir"); } @Override public Pair> getSolverNameAndOptions() { - return Pair.> of(DataflowSolverEngine.class.getCanonicalName(), + return Pair.> of(RefValSolverEngine.class.getCanonicalName(), new ArrayList()); } @@ -32,7 +34,7 @@ public boolean useHacks() { @Parameters public static List getTestFiles(){ List testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests(); - testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testing", "dataflow-inferrable-test")); + testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testing", "refval-inferrable-test")); return testfiles; } } diff --git a/tests/checkers/typecheck/DataflowTypecheckTest.java b/tests/checkers/typecheck/RefValTypecheckTest.java similarity index 69% rename from tests/checkers/typecheck/DataflowTypecheckTest.java rename to tests/checkers/typecheck/RefValTypecheckTest.java index 560a439f2..b0a3b2d06 100644 --- a/tests/checkers/typecheck/DataflowTypecheckTest.java +++ b/tests/checkers/typecheck/RefValTypecheckTest.java @@ -8,17 +8,19 @@ import java.util.ArrayList; import java.util.List; -public class DataflowTypecheckTest extends CheckerFrameworkPerFileTest { +import refval.RefValChecker; - public DataflowTypecheckTest(File testFile) { - super(testFile, dataflow.DataflowChecker.class, "dataflow", +public class RefValTypecheckTest extends CheckerFrameworkPerFileTest { + + public RefValTypecheckTest(File testFile) { + super(testFile, RefValChecker.class, "refval", "-Anomsgtext", "-d", "tests/build/outputdir"); } @Parameters public static List getTestFiles(){ List testfiles = new ArrayList<>(); - testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testing", "dataflow-not-inferrable-test")); + testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testing", "refval-not-inferrable-test")); return testfiles; } }