typetools / checker-framework-inference Goto Github PK

Inference of pluggable types for Java

Python 0.82% Java 98.43% Shell 0.74%

checker-framework-inference's Introduction

This project is no longer maintained. However, a fork is being maintained: https://github.com/opprop/checker-framework-inference

Checker Framework Inference

This project is a general type inference framework, built upon the Checker Framework.

Given a program with no type annotations, Checker Framework Inference produces a program with type annotations.

By contrast, given a program with type annotations, the Checker Framework determines verifies the program's correctness or reveals errors in it.

Developer Notes

Continuous integration status of master:

If you want to extend the framework for your own type system or add additional constraint solvers, please send us mail.

The checker-framework-inference Google Drive folder contains additional documents for developers:

https://drive.google.com/drive/u/1/folders/0B7vOZvme6aAOfjQ0bWlFU1VoeVZCVjExVmJLM0lGY3NBV0VLcENYdm03c0RCNGFzZURHX2c

That information is being moved to here in the repository.

Configure Eclipse to edit Checker Framework Inference

The instructions here assumes you have cloned this project into a folder called checker-framework-inference.

Follow the instructions in the Checker Framework Manual to download, build, and configure Eclipse to edit the Checker Framework. The Checker Framework Inference Eclipse project depends on the eclipse projects from Checker Framework.
Follow the instructions below to build Checker Framework Inference
Build the dependencies jar file:

./gradlew dependenciesJar

Enter the main Eclipse working screen and in the “File” menu, select “Import” -> “General” -> “Existing Projects into workspace”. After the “Import Projects” window appears, select “Select Root Directory”, and select the checker-framework-inference directory. Eclipse should successfully build all the imported projects.

Requirements

You will need a JDK (version 8) and Gradle.

Following the instructions in the Checker Framework manual to install the Checker Framework from source.

NOTE: Gradle on Ubuntu 14.10 hard-codes JAVA_HOME. To change this, edit /usr/share/gradle/bin/gradle and replace

    export JAVA_HOME=/usr/lib/jvm/default-java

with

    [ -n "$JAVA_HOME" ] || export JAVA_HOME=/usr/lib/jvm/default-java

Building

To build:

./gradlew dist

Execution

Verify you have all of the requirements.

./scripts/inference

is the script used to run inference.

Example:

./scripts/inference --logLevel FINE --mode ROUNDTRIP --checker ostrusted.OsTrustedChecker --solver checkers.inference.solver.PropagationSolver -afud /path/to/Annotation/File/Utilities/output/directory [List of files]

There are a couple of required options:

--mode Specifies what the tools should do. Available options are [INFER, TYPECHECK, ROUNDTRIP, ROUNDTRIP_TYPECHECK]
- INFER: Generates and solves the constraints and writes the results to default.jaif file
- TYPECHECK: Typechecks the existin code
- ROUNDTRIP: Generates and solves the constraints and then inserts the results back into the original source code
- ROUNDTRIP_TYPECHECK: Executes roundtrip and then typechecks the result
--checker Specifies which checker to run. The two most supported checkers at the moment are checkers.ostrusted.OsTrustedChecker and checkers.tainting.TaintingChecker
--solver Which solver to use on the constraints.
--targetclasspath The classpath that is required by target program.

checkers.inference.solver.PropagationSolver is the only real solver at the moment. TODO: update

Omiting the solver will create an output that numbers all of the annotation positions in the program.

checkers.inference.solver.DebugSolver will output all of the constraints generated.

Other options can be found by ./scripts/inference --help.

checker-framework-inference's People

Contributors

Stargazers

Watchers

Forkers

jonathanburke jthaine wmdietl aas-integration topnessman opprop hsanchez bitterfox charlesz-chen bohdankm22 mernst smillst eisop t-rasmud kelloggm

checker-framework-inference's Issues

Create a checker-inference-qual.jar file

At the moment all CF classes are added to the runtime classpath:
https://github.com/typetools/checker-framework-inference/pull/72/files#diff-d80679221256a0135d284f4188189a2aR131

Like with checker-qual.jar, we should create a checker-inference-qual.jar that only contains the dependencies that are needed on the compilation classpath.

OsTrusted String concatenation test fails

The test at testdata/ostrusted/TestConcat.java is failing.
I skipped the test for now and created this issue.

IllegalArgumentException when visiting annotation on an array during inference

What steps will reproduce the problem?
./scripts/inference.py --checker ostrusted.OsTrustedChecker --mode roundtrip-typecheck --log-level FINE --solver checkers.inference.solver.MaxSat2TypeSolver bar.java

Contents of bar.java:

import ostrusted.quals.OsTrusted;
class bar {
void foo(@OsTrusted String @OsTrusted [] s){}
}

What is the expected output? What do you see instead?
Expect inference and typechecking to complete without errors. See an IllegalArgumentException instead (stack trace below).

What version of the product are you using?

master 167eb7f Add missing dependencies on sat4j.

Stack trace:

error: SourceChecker.typeProcess: unexpected Throwable (IllegalArgumentException) while processing bar.java; message: Unexpected tree (@OsTrusted()
String @OsTrusted() [] s) for type (@OsTrusted String @OsTrusted [])
Compilation unit: bar.java
Exception: java.lang.IllegalArgumentException: Unexpected tree (@OsTrusted()
String @OsTrusted() [] s) for type (@OsTrusted String @OsTrusted []); Stack trace: checkers.inference.VariableAnnotator.visitArray(VariableAnnotator.java:859)
checkers.inference.VariableAnnotator.visitArray(VariableAnnotator.java:91)
org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedArrayType.accept(AnnotatedTypeMirror.java:1348)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:99)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:89)
checkers.inference.VariableAnnotator.visitTogether(VariableAnnotator.java:1422)
checkers.inference.VariableAnnotator.handleMethodDeclaration(VariableAnnotator.java:1357)
checkers.inference.VariableAnnotator.visitExecutable(VariableAnnotator.java:1189)
checkers.inference.VariableAnnotator.visitExecutable(VariableAnnotator.java:91)
org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedExecutableType.accept(AnnotatedTypeMirror.java:1083)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:99)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:89)
checkers.inference.InferenceTreeAnnotator.visitMethod(InferenceTreeAnnotator.java:195)
checkers.inference.InferenceTreeAnnotator.visitMethod(InferenceTreeAnnotator.java:55)
com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:800)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:38)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:21)
com.sun.source.util.SimpleTreeVisitor.visitMethod(SimpleTreeVisitor.java:77)
org.checkerframework.framework.type.treeannotator.TreeAnnotator.visitMethod(TreeAnnotator.java:35)
org.checkerframework.framework.type.treeannotator.TreeAnnotator.visitMethod(TreeAnnotator.java:17)
com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:800)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
checkers.inference.InferenceAnnotatedTypeFactory.annotateImplicit(InferenceAnnotatedTypeFactory.java:466)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:882)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:722)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1826)
org.checkerframework.framework.type.TypesIntoElements.storeMethod(TypesIntoElements.java:91)
org.checkerframework.framework.type.TypesIntoElements.store(TypesIntoElements.java:80)
org.checkerframework.framework.type.AnnotatedTypeFactory.postProcessClassTree(AnnotatedTypeFactory.java:750)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:735)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1805)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:604)
checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:442)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:931)
checkers.inference.InferenceAnnotatedTypeFactory.annotateImplicit(InferenceAnnotatedTypeFactory.java:477)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:882)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:722)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1805)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:296)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:173)
com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:890)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:452)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:205)
com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
com.sun.tools.javac.main.Main.compile(Main.java:523)
com.sun.tools.javac.main.Main.compile(Main.java:381)
com.sun.tools.javac.main.Main.compile(Main.java:370)
com.sun.tools.javac.main.Main.compile(Main.java:361)
checkers.inference.CheckerFrameworkUtil.invokeCheckerFramework(CheckerFrameworkUtil.java:12)
checkers.inference.InferenceMain.startCheckerFramework(InferenceMain.java:159)
checkers.inference.InferenceMain.run(InferenceMain.java:112)
checkers.inference.InferenceCli.main(InferenceCli.java:92)

Inference error in scenario involving enums and generics

What steps will reproduce the problem?
Enable and run the following test: testdata/sparta-source/Issue6.java

What is the expected output? What do you see instead?
The test should pass. Instead, an exception is thrown:

[junit] INFO: - compiler.err.proc.messager: Unexpected AnnotatedTypeMirror with no primary annotation!
[junit] toSearch=Enum<capture#787 of ? extends Enum<capture#787 of ?>>
[junit] [email protected]
[junit] source=Enum<capture#787 of ? extends Enum<capture#787 of ?>>
[junit] Compilation unit: /Users/javier/sparta3/checker-framework-inference/testdata/sparta-source/Issue6.java
[junit] Exception: java.lang.Throwable; Stack trace: org.checkerframework.framework.source.SourceChecker.errorAbort(SourceChecker.java:669)
[junit] org.checkerframework.javacutil.ErrorReporter.errorAbort(ErrorReporter.java:28)
[junit] org.checkerframework.framework.util.AnnotatedTypes.findEffectiveAnnotationInHierarchy(AnnotatedTypes.java:1682)
[junit] org.checkerframework.framework.util.AnnotatedTypes.findEffectiveAnnotationInHierarchy(AnnotatedTypes.java:1638)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.subtypeAndCompare(StructuralEqualityComparer.java:349)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitTypevar_Typevar(StructuralEqualityComparer.java:300)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitTypevar_Typevar(StructuralEqualityComparer.java:36)
[junit] org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:598)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areEqual(StructuralEqualityComparer.java:92)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.checkOrAreEqual(StructuralEqualityComparer.java:163)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areAllEqual(StructuralEqualityComparer.java:145)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitTypeArgs(StructuralEqualityComparer.java:237)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitDeclared_Declared(StructuralEqualityComparer.java:214)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitDeclared_Declared(StructuralEqualityComparer.java:36)
[junit] org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:302)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areEqual(StructuralEqualityComparer.java:92)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitWildcard_Wildcard(StructuralEqualityComparer.java:383)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitWildcard_Wildcard(StructuralEqualityComparer.java:36)
[junit] org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:646)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areEqual(StructuralEqualityComparer.java:92)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.checkOrAreEqual(StructuralEqualityComparer.java:163)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areAllEqual(StructuralEqualityComparer.java:145)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitTypeArgs(StructuralEqualityComparer.java:237)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitDeclared_Declared(StructuralEqualityComparer.java:214)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.visitDeclared_Declared(StructuralEqualityComparer.java:36)
[junit] org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:302)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areEqual(StructuralEqualityComparer.java:75)
[junit] org.checkerframework.framework.type.StructuralEqualityComparer.areEqualInHierarchy(StructuralEqualityComparer.java:101)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.areEqualInHierarchy(DefaultTypeHierarchy.java:359)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.isContainedBy(DefaultTypeHierarchy.java:390)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.compareTypeArgs(DefaultTypeHierarchy.java:503)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.visitTypeArgs(DefaultTypeHierarchy.java:478)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:447)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:51)
[junit] org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:302)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:220)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:170)
[junit] org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:151)
[junit] checkers.inference.InferenceVisitor.commonAssignmentCheck(InferenceVisitor.java:535)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:1858)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.checkArguments(BaseTypeVisitor.java:2216)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:931)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:173)
[junit] com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept(JCTree.java:1477)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:273)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:173)
[junit] com.sun.source.util.TreeScanner.visitExpressionStatement(TreeScanner.java:243)
[junit] com.sun.tools.javac.tree.JCTree$JCExpressionStatement.accept(JCTree.java:1302)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:273)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:173)
[junit] com.sun.source.util.TreeScanner.scan(TreeScanner.java:91)
[junit] com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:162)
[junit] com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:918)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:273)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:173)
[junit] com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:81)
[junit] com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:144)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:507)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:173)
[junit] com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:800)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:273)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:173)
[junit] com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:81)
[junit] com.sun.source.util.TreeScanner.scan(TreeScanner.java:91)
[junit] com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:99)
[junit] com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:133)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:323)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:173)
[junit] com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
[junit] org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
[junit] org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:889)
[junit] org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:452)
[junit] org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:205)
[junit] com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
[junit] com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
[junit] com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
[junit] com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
[junit] com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
[junit] com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:523)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:381)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:370)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:361)
[junit] checkers.inference.CheckerFrameworkUtil.invokeCheckerFramework(CheckerFrameworkUtil.java:12)
[junit] checkers.inference.InferenceMain.startCheckerFramework(InferenceMain.java:173)
[junit] checkers.inference.InferenceMain.run(InferenceMain.java:135)
[junit] checkers.inference.InferenceMain.main(InferenceMain.java:107)

What version of the product are you using?
17f60a4 on branch: master

Google Drive link broken

The google drive link in https://github.com/typetools/checker-framework-inference/blob/master/README for the additional documents requires special permissions to access, and is inaccessible from a public computer with or without logging into any google account.

Check for plume.jar

checker-framework-inference/dist does not contain plume.jar, which checker-framework-inference/scripts/inference assumes it contains.
Furthermore, "gradle dist" does not fail if plume.jar is not found.

This works around the problem:
cd $JSR308
ln -s $pl .
cd $cfi
gradle dist

But "gradle dist" should fail if plume.jar is not found rather than continuing without error.

Add refinement variables for compound assignments

Refinement variables are not created for compound assignments. (This includes string concatenation compound assignments which are handled separately in dataflow.)

This will include changes to the following methods:
checkers.inference.dataflow.InferenceTransfer#visitAssignment
checkers.inference.dataflow.InferenceTransfer#visitStringConcatenateAssignment
checkers.inference.InferenceTreeAnnotator#visitCompoundAssignment

Make the propagation solver throw an exception if it sees an ExistentialConstraint

It should not silently continue.

Annotations on class declaration extends

We currently don't support annotations on implicit extends for class declarations see comment on:
VariableAnnotator#createImpliedExtendsLocation(com.sun.source.tree.ClassTree)
And according to the email exchange below, we should not.

Null pointer exception with Collection

Will add test case in /testdata/ostrusted/ as pull request once issue number given.

Creating and checking constraints in ConstraintManager

At the moment, all constraints are generated out of ConstraintManager, and once constraints are generated, we put them in ConstraintManager without any checking.
Professor Dietl and I discussed about current features of ConstraintManager, and we think that it is may be a good idea that we can create and check constraints inside ConstraintManager.
For example, we can add method public void addSubtypeConstraint(Slot subtype, Slot supertype) in ConstraintManager. The method generates a SubtypeConstraint for the two slots, and do some checking:
If supertype is ConstantSlot and the value of it is the top type, then we don't need to generate anything, and same for if subtype is bottom type.
If both supertype and subtype are ConstantSlot, then we check whether the two types satisfy subtype type rules, if they don't, the ConstraintManager reports type incompatible error.
The problem for this implementation is if we want to use report method in SourceChecker to report error, we need the second parameter of the method to indicate the location of the problem, but we cannot get that information from instance of Slot. Passing the Tree node to ConstraintManager through all the callers may need a lot of refinement. So we may need to think a better way to refine it.

Not terminating on code with compound string concatenation assignment in loop

Code:
String s = " ";
for (int i = 1; i < 1; i++) {
s += "|";
}
(Also checked in as testdata/sparta-source/Issue8.java)

Ran for 10 mins, did not terminate.

VarAnnots not inserted for primitive class literals

What steps will reproduce the problem?
Enable and run the following test: testdata/sparta-source/Issue7.java

What is the expected output? What do you see instead?
The test should pass. Instead, an exception is thrown:

[junit] INFO: - compiler.err.proc.messager: Missing VarAnnot annotation: boolean
[junit] Compilation unit: /Users/javier/sparta3/checker-framework-inference/testdata/sparta-source/Issue7.java
[junit] Exception: java.lang.Throwable; Stack trace: org.checkerframework.framework.source.SourceChecker.errorAbort(SourceChecker.java:669)
[junit] org.checkerframework.javacutil.ErrorReporter.errorAbort(ErrorReporter.java:28)
[junit] checkers.inference.DefaultSlotManager.getVariableSlot(DefaultSlotManager.java:166)
[junit] checkers.inference.VariableAnnotator.handleBinaryTree(VariableAnnotator.java:1526)
[junit] checkers.inference.VariableAnnotator.visitPrimitive(VariableAnnotator.java:1253)
[junit] checkers.inference.VariableAnnotator.visitPrimitive(VariableAnnotator.java:95)
[junit] org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedPrimitiveType.accept(AnnotatedTypeMirror.java:1828)
[junit] org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:99)
[junit] org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:89)
[junit] checkers.inference.InferenceTreeAnnotator.visitBinary(InferenceTreeAnnotator.java:433)
[junit] checkers.inference.InferenceTreeAnnotator.visitBinary(InferenceTreeAnnotator.java:58)
[junit] com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1795)
[junit] com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
[junit] org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:38)
[junit] org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:21)
[junit] com.sun.source.util.SimpleTreeVisitor.visitBinary(SimpleTreeVisitor.java:197)
[junit] com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1795)
[junit] com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
[junit] checkers.inference.InferenceAnnotatedTypeFactory.annotateImplicit(InferenceAnnotatedTypeFactory.java:479)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:882)
[junit] org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:722)
[junit] org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:172)
[junit] org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:483)
[junit] org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:96)
[junit] org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor.visitEqualTo(AbstractNodeVisitor.java:199)
[junit] org.checkerframework.framework.flow.CFAbstractTransfer.visitEqualTo(CFAbstractTransfer.java:621)
[junit] org.checkerframework.framework.flow.CFAbstractTransfer.visitEqualTo(CFAbstractTransfer.java:96)
[junit] org.checkerframework.dataflow.cfg.node.EqualToNode.accept(EqualToNode.java:52)
[junit] org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:362)
[junit] org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:199)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:761)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:732)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:678)
[junit] checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:455)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:931)
[junit] checkers.inference.InferenceAnnotatedTypeFactory.annotateImplicit(InferenceAnnotatedTypeFactory.java:490)
[junit] org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:882)
[junit] org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:722)
[junit] org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1810)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:296)
[junit] org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:173)
[junit] com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
[junit] com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
[junit] org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
[junit] org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:889)
[junit] org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:452)
[junit] org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:205)
[junit] com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
[junit] com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
[junit] com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
[junit] com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
[junit] com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
[junit] com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:523)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:381)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:370)
[junit] com.sun.tools.javac.main.Main.compile(Main.java:361)
[junit] checkers.inference.CheckerFrameworkUtil.invokeCheckerFramework(CheckerFrameworkUtil.java:12)
[junit] checkers.inference.InferenceMain.startCheckerFramework(InferenceMain.java:173)
[junit] checkers.inference.InferenceMain.run(InferenceMain.java:135)
[junit] checkers.inference.InferenceMain.main(InferenceMain.java:107)

What version of the product are you using?
17f60a4 on branch: master

Annotation not inserted for enum fields

What steps will reproduce the problem?
inference.py --solver sparta.checkers.SpartaSourceSolver --checker 
sparta.checkers.SpartaSourceChecker --log-level=FINEST 
--prog-args='--proconly=false --hackmode' --mode roundtrip --in-place 
EnumField.java

What is the expected output? What do you see instead?
enumField should have a @Source(READ_SMS) qualifier, but instead no annotations 
are inferred.


What version of the product are you using? 
99451307292c  on branch:      remove-scala

Original issue reported on code.google.com by [email protected] on 8 Sep 2014 at 4:35

Attachments:

EnumField.java

Intellij support for checker framework inference

Also where can I specify project name or project source path for which I want to run inference script ? I ran the below command and it failed.

 ./scripts/inference --logLevel FINE --mode TYPECHECK --checker ostrusted.OsTrustedChecker --solver checkers.inference.solver.PropagationSolver -afud [source_file_path_for_which_I_want_to_run_this_script]

--- Typechecking ---

javac: invalid flag: source_file_path_for_which_I_want_to_run_this_script
Usage: javac <options> <source files>
use -help for a list of possible options

--- Typechecking failed ---

I couldn't find any step by step instructions with example for running this tool on command line or on intellij. Suppose I have a java project on intellij how do I run this tool to auto generate type inference code from command line or from intellij?

Thanks,
Shashi