opprop / checker-framework-inference Goto Github PK
View Code? Open in Web Editor NEWThis project forked from typetools/checker-framework-inference
Inference of pluggable types for Java
This project forked from typetools/checker-framework-inference
Inference of pluggable types for Java
A constant constraint (consisted of all constant slots) can be early verified before passing them into solver, but currently we lack of this mechanism.
Should add early verification mechanism for verifying constant constraints.
An ideal place would be ConstraintManager
.
import ostrusted.qual.OsTrusted;
import ostrusted.qual.OsUntrusted;
public class A {
@OsTrusted Object trusted;
@OsUntrusted Object untrusted;
Object foo() {
return untrusted;
}
void bar() {
trusted = foo();
}
}
For the above code, the generated constraint doesn't make sense:
Created VariableSlot
10
:AstPath:
AstPathLocation( A.foo()Ljava/lang/Object;.null:A:foo()Ljava/lang/Object;::Method.parameter -1 )
11
:AstPath:
AstPathLocation( A.bar()V.null:A:bar()V::Method.parameter -1 )
5
:AstPath:
MissingLocation
6
:AstPath:
ClassDeclLocation( .A )
8
:AstPath:
AstPathLocation( A.<init>()V.null:A:<init>()V:: )
9
:AstPath:
AstPathLocation( A.foo()Ljava/lang/Object;.null:A:foo()Ljava/lang/Object;::Method.type )
Created RefinementVariableSlot
12: refines [@ostrusted.qual.OsTrusted]
:AstPath:
AstPathLocation( A.bar()V.null:A:bar()V::Method.body, Block.statement 0, ExpressionStatement.expression )
Created ExistentialVariableSlot
7: ( 6 | 3 )
:AstPath:
MissingLocation
Created CombVariableSlot
Created ConstantSlot
@OsTrusted(2)
@OsUntrusted(3)
@PolyAll(1)
@PolyOsTrusted(4)
Created these constraints:
11 <: 10
12: refines [@ostrusted.qual.OsTrusted] == 9
12: refines [@ostrusted.qual.OsTrusted] == @OsTrusted(2)
9 <: 12: refines [@ostrusted.qual.OsTrusted]
9 <: @OsUntrusted(3)
9 == @OsUntrusted(3)
@OsTrusted(2) <: @OsUntrusted(3)
@OsUntrusted(3) == @OsUntrusted(3)
We have no idea where following constraints come from.
9 <: @OsUntrusted(3)
9 == @OsUntrusted(3)
Where is the class that has the same functionality as this class: https://github.com/opprop/generic-type-inference-solver/blob/master/src/util/ConstantUtils.java ?
Testcase:
class Wrapper<T> {
Wrapper(T t) {}
}
public class NullDeclSlot {
public static void foo() {
new Wrapper<>("");
}
}
Command To Run: ./scripts/inference --checker ostrusted.OsTrustedChecker --logLevel=FINE --mode ROUNDTRIP --solver checkers.inference.solver.SolverEngine -afud . ../immutability/testinput/inference/bug/NullDeclSlot.java
Got exception:
...
Jan 13, 2018 3:22:30 PM checkers.inference.InferenceMain$DefaultResultHandler handleCompilerResult
SEVERE: Non-OK return code from javac! Quitting. Result code is: ERROR
Jan 13, 2018 3:22:30 PM checkers.inference.InferenceMain$DefaultResultHandler handleCompilerResult
SEVERE: error: Missing VarAnnot annotation: String
Compilation unit: ../immutability/testinput/inference/bug/NullDeclSlot.java
Exception: java.lang.Throwable; Stack trace: org.checkerframework.framework.source.SourceChecker.errorAbort(SourceChecker.java:726)
org.checkerframework.javacutil.ErrorReporter.errorAbort(ErrorReporter.java:25)
checkers.inference.DefaultSlotManager.getVariableSlot(DefaultSlotManager.java:198)
checkers.inference.InferenceTypeVariableSubstitutor.substituteTypeVariable(InferenceTypeVariableSubstitutor.java:72)
org.checkerframework.framework.type.TypeVariableSubstitutor$Visitor.visitTypeVariable(TypeVariableSubstitutor.java:141)
org.checkerframework.framework.type.TypeVariableSubstitutor$Visitor.visitTypeVariable(TypeVariableSubstitutor.java:59)
org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedTypeVariable.accept(AnnotatedTypeMirror.java:1389)
org.checkerframework.framework.type.AnnotatedTypeCopier.visit(AnnotatedTypeCopier.java:96)
org.checkerframework.framework.type.AnnotatedTypeCopier.visitExecutable(AnnotatedTypeCopier.java:219)
org.checkerframework.framework.type.AnnotatedTypeCopier.visitExecutable(AnnotatedTypeCopier.java:42)
org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedExecutableType.accept(AnnotatedTypeMirror.java:1028)
org.checkerframework.framework.type.AnnotatedTypeCopier.visit(AnnotatedTypeCopier.java:89)
org.checkerframework.framework.type.TypeVariableSubstitutor.substitute(TypeVariableSubstitutor.java:31)
org.checkerframework.framework.util.AnnotatedTypes.substituteTypeVariables(AnnotatedTypes.java:310)
org.checkerframework.framework.util.AnnotatedTypes.asMemberOfImpl(AnnotatedTypes.java:279)
org.checkerframework.framework.util.AnnotatedTypes.asMemberOf(AnnotatedTypes.java:234)
org.checkerframework.framework.util.AnnotatedTypes.asMemberOf(AnnotatedTypes.java:192)
checkers.inference.InferenceAnnotatedTypeFactory.constructorFromUse(InferenceAnnotatedTypeFactory.java:419)
org.checkerframework.framework.type.TypeFromExpressionVisitor.visitNewClass(TypeFromExpressionVisitor.java:260)
org.checkerframework.framework.type.TypeFromExpressionVisitor.visitNewClass(TypeFromExpressionVisitor.java:44)
com.sun.tools.javac.tree.JCTree$JCNewClass.accept(JCTree.java:1532)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
org.checkerframework.framework.type.TypeFromTree.fromExpression(TypeFromTree.java:36)
org.checkerframework.framework.type.AnnotatedTypeFactory.fromExpression(AnnotatedTypeFactory.java:1221)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:994)
org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:203)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:552)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:95)
org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor.visitObjectCreation(AbstractNodeVisitor.java:334)
org.checkerframework.framework.flow.CFAbstractTransfer.visitObjectCreation(CFAbstractTransfer.java:876)
org.checkerframework.framework.flow.CFAbstractTransfer.visitObjectCreation(CFAbstractTransfer.java:95)
org.checkerframework.dataflow.cfg.node.ObjectCreationNode.accept(ObjectCreationNode.java:52)
org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:405)
org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:226)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1158)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1115)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1045)
checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:490)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1422)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:247)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:282)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:163)
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:66)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:968)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:503)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:185)
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:192)
checkers.inference.InferenceMain.run(InferenceMain.java:144)
checkers.inference.InferenceMain.main(InferenceMain.java:116)
1 error
But if I manually add the Java type argument String
to the testcase:
class Wrapper<T> {
Wrapper(T t) {}
}
public class NullDeclSlot {
public static void foo() {
new Wrapper<String>("");
}
}
And I ran the same command, I got successful result:
...
--- Inference succeeded ---
--- Inserting annotations ---
getPositions returned 5 positions in tree for ../immutability/testinput/inference/bug/NullDeclSlot.java
Warning: IndexFileSpecification did not find classfile for: Wrapper
Warning: IndexFileSpecification did not find classfile for: NullDeclSlot
Read 5 annotations from default.jaif
Processing ../immutability/testinput/inference/bug/NullDeclSlot.java
Parsed ../immutability/testinput/inference/bug/NullDeclSlot.java
.....Writing /home/mier/jsr308/checker-framework-inference/./NullDeclSlot.java
--- Insert annotations succeeded ---
This is a bug that's very severe, as any diamond tree(tree with no type argument explicitly written but should be inferred) causes this failure but diamond tree is very commonly used in programs to make code clean.
In ConstraintManager
, it use qualifierHierarchy.isSubtype()
to do subtype relationship evaluation, for example:
However, the qualifierHierarchy
field is initialized by inferenceAnnotatedTypeFactory.getQualifierHierarchy()
:
By default, the qualifierHierarchy
in an inferenceAnnotatedTypeFactory
is an instance of InferenceQualifierHierarchy
:
The problem is InferenceQualifierHierarchy
doesn't do type evaluations, instead it generates constraints. For example, when calling InferenceQualifierHierarchy.isSubtype()
it will generates a subtype constraint instead of evaluating the subtype relationship. This means, all type evaluations by qualfierHierarchy.isSubtype()
in ConstraintManager
actually doesn't perform any evaluations and generates possible un-reasonable constraints.
We might need to re-think about how to get a normal qualifierHierarchy
in ConstraintManager
to let it perform type evaluations as expected.
https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/solver/backend/logiql/LogiQLFormatTranslator.java#L257
We should update this to have logic instead of null.
Should refactor the classes related to constraint graph in solver framework.
Brief reasons:
Edge representation: this is confusing. Edge
is undirected but its subclass SubtypeEdge
is directional. Also, there were no difference between these two classes. Think about a better representation.
Vertex: since Vertex is identified by slot id, maybe add a VertexBuilder for avoiding duplicate vertex objects with same slot id.
Design doc:
https://docs.google.com/document/d/1ilu3mOhOSSk-D-CDeGPg9tiSSy8ijMCM78bmFF_4sRs/edit?usp=sharing
Abstract Slot (with location, ID, SlotKind; hash on ID, eq on ID and getClass())
|
Concrete slot classes:
Tasks:
refactor architecture, ensure SlotManager, VariableSlotReplacer, VariableAnnotator, ExistentialVariableInserter etc all work correctly
update slot manager to sort slots by ID
update general stats tracking: always dump out total Constant slots, total non-constant slots, and counts of each kind of var slots.
future: update AbstractSlot to store a string based "source" of where a slot is generated: design doc mentions constant slots should reference annotations from bytecode, from implicit rules; var slots with AnnotationLocation.MISSING
Testcase:
AbstractClassConstructor.java
public abstract class AbstractClassConstructor {
AbstractClassConstructor(Object af) {}
}
MissingLocationProblem.java
public class MissingLocationProblem extends AbstractClassConstructor {
MissingLocationProblem(Object p) {
super(p);
}
}
I ran ./infer.sh testinput/inference/limited-inferrable-inf-fr/MissingLocationProblem.java testinput/inference/limited-inferrable-inf-fr/AbstractClassConstructor.java
Actual result: inference succeeded, But I got:
import qual.Immutable;
public abstract class AbstractClassConstructor {
@Immutable
AbstractClassConstructor(Object af) {}// af got solution @Immutable, and should be inserted @Immutable
}
import qual.Immutable;
public class MissingLocationProblem extends AbstractClassConstructor {
@Immutable
MissingLocationProblem(@Immutable Object p) {
super(p);
}
}
Expected result is af
was also inserted annotation. But it wasn't.
I found this was caused by:
IdentifierTree
is used, treeToLocation()
returns null, and the inserted VariableSlot
gets location MISSING_LOCATION
thus the solution for this VariableSlot wasn't inserted to the source code.Currently there were two constructors in GraphBuilder
, the difference is one of them asking for an additional top Qualifier, then assign it to field top
, and in another one it do nothing with field top
, i.e. this field is implicitly null.
It is better to make field top
final and remove the constructor that do nothing with field top
.
The reason is this field top
is used in BFS search process when building the graph, then set it to null
in one constructor makes code tricky and hard to understand.
Also, intuitively top
should be final and should not be changed during building the graph.
In addition, slots
parameter seems not been used in GraphBuilder
. Remove this parameter also.
Testcase:
class TestRefinement {
void test() {
Object o = new Object();// using variable tree to assign o
}
}
After insertion:
import checkers.inference.qual.VarAnnot;
class TestRefinement {
void test(@VarAnnot(12) TestRefinement this) {
@VarAnnot(9)
Object o = new @VarAnnot(10) Object();
}
}
RefinementVariableSlots generated(empty):
Created RefinementVariableSlot
But if I changed testcase tt:
class TestRefinement {
void test() {
Object o;
o = new Object();// Using identifier to assign o
}
}
Then I get insertion result:
import checkers.inference.qual.VarAnnot;
class TestRefinement {
void test(@VarAnnot(13) TestRefinement this) {
@VarAnnot(9)
Object o;
o = new @VarAnnot(10) Object();
}
}
And a refinement variable slot:
Created RefinementVariableSlot
12: refines [VariableSlot(9)]
:AstPath:
AstPathLocation( TestRefinement.test()V.null:TestRefinement:test()V::Method.body, Block.statement 1, ExpressionStatement.expression )
CFI should be consistent either when assigning to a variable tree or identifier tree. In this case, a RefinementVariableSlot
should always be generated in both assignments.
Currently PrintUtils
takes both responsibilities of printing records and take statistics.
Also it highly coupling with concrete solver types.
Also, the StatisticKey
enum class used in PrintUtil
is also mixed a lot with specific solver types.
Should decoupling them with concrete solver types, and make the statistic part extendable to specific solvers and type systems. I.e. a specific solver or a type system can make customized statistics.
The parameters in VariableCombos' methods are a bit strange:
it takes both slots and the constraint: e.g. var_var(VarSlot s1, VarSlot s2, Cons cons)
.
This is not good as it cannot guarantee the slots passing in are actually belongs to the constraint, and it cannot control the order of slots that caller passed in (e.g. in case of var_var
, it assume the first slot is subtype, but this cannot checked statically by compiler).
A better way would to apply a more detailed visitor pattern between Constraint
and Serializer
:
i.e. for each Constraint
type, it switches case of the slots combinations, and calling the corresponding method in Serializer
.
One is in checkers.inference.solver.util.VectorUtils
The other is checkers.inference.solver.backend.maxsat.VectorUtils
Please leave only one of the two. Thanks. @CharlesZ-Chen
I came across with this exception when running GUT inference on project dyn4j.
The below part of code(from src/org/dyn4j/geometry/Geometry.java
) causes inference to crash:
public static final <E extends Wound & Convex> Polygon minkowskiSum(E convex1, E convex2) {
if (convex1 == null) throw new NullPointerException(Messages.getString("geometry.nullMinkowskiSumConvex"));
if (convex2 == null) throw new NullPointerException(Messages.getString("geometry.nullMinkowskiSumConvex"));
return null;
...
}
2017-08-11 11:36:43,853 [main] checkers.inference.InferenceMain handleCompilerResult [FATAL] - error: QualifierHierarchy.leastUpperBounds: tried to determine LUB with sets of different sizes!
Set 1: [] Set 2: [@checkers.inference.qual.VarAnnot(2)]
Compilation unit: src/org/dyn4j/geometry/Geometry.java
Exception: java.lang.Throwable; Stack trace: org.checkerframework.framework.source.SourceChecker.errorAbort(SourceChecker.java:727)
org.checkerframework.javacutil.ErrorReporter.errorAbort(ErrorReporter.java:25)
org.checkerframework.framework.type.QualifierHierarchy.leastUpperBounds(QualifierHierarchy.java:187)
checkers.inference.VariableAnnotator.handleBinaryTree(VariableAnnotator.java:1543)
GUTI.GUTIAnnotatedTypeFactory$GUTIVariableAnnotator.visitPrimitive(GUTIAnnotatedTypeFactory.java:152)
GUTI.GUTIAnnotatedTypeFactory$GUTIVariableAnnotator.visitPrimitive(GUTIAnnotatedTypeFactory.java:136)
org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedPrimitiveType.accept(AnnotatedTypeMirror.java:1831)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:89)
org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:79)
checkers.inference.InferenceTreeAnnotator.visitBinary(InferenceTreeAnnotator.java:431)
checkers.inference.InferenceTreeAnnotator.visitBinary(InferenceTreeAnnotator.java:52)
com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1795)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:52)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:20)
com.sun.source.util.SimpleTreeVisitor.visitBinary(SimpleTreeVisitor.java:197)
org.checkerframework.framework.type.treeannotator.TreeAnnotator.visitBinary(TreeAnnotator.java:50)
org.checkerframework.framework.type.treeannotator.TreeAnnotator.visitBinary(TreeAnnotator.java:16)
com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1795)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
checkers.inference.InferenceAnnotatedTypeFactory.addComputedTypeAnnotations(InferenceAnnotatedTypeFactory.java:512)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1272)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:985)
org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:202)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:550)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:94)
org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor.visitEqualTo(AbstractNodeVisitor.java:191)
org.checkerframework.framework.flow.CFAbstractTransfer.visitEqualTo(CFAbstractTransfer.java:672)
org.checkerframework.framework.flow.CFAbstractTransfer.visitEqualTo(CFAbstractTransfer.java:94)
org.checkerframework.dataflow.cfg.node.EqualToNode.accept(EqualToNode.java:25)
org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:404)
org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:200)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1102)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1059)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:989)
checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:485)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1326)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:224)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:281)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:160)
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:66)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:962)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:494)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:185)
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:182)
checkers.inference.InferenceMain.run(InferenceMain.java:146)
checkers.inference.InferenceMain.main(InferenceMain.java:114)
1 error
The primary reason is that: getEffectiveAnnotations()
returns [] for E extends @1 Wound & @2 Convex
. But if I changed the upper bound to either @1 Wound
or @2 Convex
, then [@1] or [@2] were correctly returned and there won't be such exception.
Currently, TwoQualLattice
is a sub-class of Lattice
, which cause null
parameters passing in super constructor call, see:
Should have a better class hierarchy of Lattice to avoid null
passing around:
Have a common abstract class Lattice
, then:
Have two sub-classes NormalLattice
and TwoQualLattice
, where NormalLattice
is the original Lattice
class, and TwoQualLattice
should not be a subtype of NormalLattice
.
I got an error when I ran dljc on a project SimpleJavaCalculator that contains only three files. I have minimized the test case to two files.
package simplejavacalculator;
public class Calculator {
public Double calculateBi() {
return 0.0;
}
}
package simplejavacalculator;
public class UI {
private Calculator calc;
public void actionPerformed() {
writer(calc.calculateBi());
}
public void writer(final Double num) {
if (Double.isNaN(num)) {}
}
}
If I run ../universe/scripts/infer.sh src/simplejavacalculator/UI.java src/simplejavacalculator/Calculator.java
, it successfully infers result, but failed to insert some result into the source code.
But if I change the order of two files, i.e. when I run ../universe/scripts/infer.sh src/simplejavacalculator/Calculator.java src/simplejavacalculator/UI.java
, then inference fails with error message:
========== Inference failed because of the following inconsistent constraints ==========
25 = ( 24 ▷ @Any(1) )
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression, MethodInvocation.argument 0 )
26 = ( 21 ▷ 23 )
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression )
23 == @Bottom(2)
AstPathLocation( simplejavacalculator.UI.writer(Ljava/lang/Double;)V.null:simplejavacalculator.UI:writer(Ljava/lang/Double;)V::Method.body, Block.statement 0, If.condition, Parenthesized.expression )
25 <: 26
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression )
==================================== Related Slots =====================================
25: combines [CombVariableSlot(24), @GUT.qual.Any]
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression, MethodInvocation.argument 0 )
24: combines [VariableSlot(21), VariableSlot(18)]
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression, MethodInvocation.argument 0, MethodInvocation.methodSelect, MemberSelect.expression )
23
AstPathLocation( simplejavacalculator.UI.writer(Ljava/lang/Double;)V.null:simplejavacalculator.UI:writer(Ljava/lang/Double;)V::Method.parameter 0, Variable.type )
26: combines [VariableSlot(21), VariableSlot(23)]
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.body, Block.statement 0, ExpressionStatement.expression )
21
AstPathLocation( simplejavacalculator.UI.actionPerformed()V.null:simplejavacalculator.UI:actionPerformed()V::Method.parameter -1 )
=================================== Explanation Ends Here ==============================
After my investigation, I found that elementToTreeCache
contains null tree for element - calculateBi()
in the first class Calculator
when inference handles the second class UI
, and the method will be treated as if it is from bytecode. As a result, the variable slot created on the method return type will not be used. Instead, @Any
will be used for the method return type. Because the relatively stronger type rules of GUT, this failure is triggered. If we used the variable slot, then there will be solution.
So, when we do infer.sh A.java B.java
, what really happens is that: A.java is processed, then A's tree collapses, and the handles B.java. If B.java uses methods in A.java, then those methods are treated as if they are from bytecode.
@wmdietl Did you consider this tree collapsing issue when CFI was developed initially? If yes, what was your way around this problem?
@CharlesZ-Chen @Jianchu Do you have any idea towards this?
Any suggestions are appreciated.
In inference, we have a bunch of jar files in dist directory. When we run the inference, those jar files are added to the classpath in the alphabetical order, like annotation-file-utilities.jar is the first to be used.
What's worse is: annotation-file-utilities.jar are created by zipping class files from plume.jar in its own distribution, which is last updated three months ago.
plume.jar in plume-lib directory are zipped from classes in checker-qual-2.1.1.jar in its own distribution, which is last updated one month ago.
The question is: should we remove the class file duplication in the three jar files? Or we work around the problem by setting the classpath correctly in inference?
CFI uses the Unqualified
annotation in certain situations, e.g. here:
All these uses should be removed and the "real" type annotations should be used instead.
We need help from Jason to see which String can directly cause solver to fail.
For the following code snippet, CFI crashes when executing any inference checker. The bug is also present when executing Ontology and Units inference checkers.
class GenericMethods {
public <T extends Integer> Integer mInteger(T param){
return param + param;
}
}
The snippet compiles successfully with standard javac and CF javac.
Example command:
$CFI/scripts/inference --mode INFER --checker ostrusted.OsTrustedChecker --solver checkers.inference.solver.GeneralSolver --solverArgs solver=MaxSAT,useGraph=true,collectStatistic=true,solveInParallel=false GenericMethods.java
Stack trace:
--- Inferring ---
Mar 05, 2018 5:46:44 PM checkers.inference.InferenceMain startCheckerFramework
FINE: Starting checker framework with options: [-processor, checkers.inference.InferenceChecker, -Xmaxwarns, 1000, -Xmaxerrs, 1000, -XDignore.symbol.file, -AprintErrorStack, -Xbootclasspath/p:/home/jeff/jsr308/checker-framework-inference/dist/jdk8.jar, GenericMethods.java]
Mar 05, 2018 5:46:46 PM checkers.inference.InferenceAnnotatedTypeFactory setRoot
FINE:
CHANGING COMPILATION UNIT ( 0 ): GenericMethods.java
Mar 05, 2018 5:46:46 PM checkers.inference.VariableAnnotator createImpliedExtendsLocation
WARNING: Hack:VariableAnnotator::createImpliedExtendsLocation(classTree) not implemented
Mar 05, 2018 5:46:46 PM checkers.inference.VariableAnnotator handleClassDeclaration
FINE: Created variable for implicit extends on class:
5 => GenericMethods (extends Object)
Mar 05, 2018 5:46:46 PM checkers.inference.VariableAnnotator createVariable
FINE: Created variable for tree:
6 =>
class GenericMethods {
GenericMethods() {
super();
}
public <T extends Integer>int mInteger(T param) {
return param + param;
}
}
Mar 05, 2018 5:46:46 PM checkers.inference.InferenceMain$DefaultResultHandler handleCompilerResult
SEVERE: Error return code from javac! Quitting.
Mar 05, 2018 5:46:46 PM checkers.inference.InferenceMain$DefaultResultHandler handleCompilerResult
INFO: error: SourceChecker.typeProcess: unexpected Throwable (IllegalArgumentException) while processing GenericMethods.java; message: Not a primitive type: NONE
Compilation unit: GenericMethods.java
Exception: java.lang.IllegalArgumentException: Not a primitive type: NONE; Stack trace: com.sun.tools.javac.model.JavacTypes.getPrimitiveType(JavacTypes.java:157)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.binaryPromotedType(CFGBuilder.java:2119)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBinary(CFGBuilder.java:3117)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBinary(CFGBuilder.java:1503)
com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1795)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitReturn(CFGBuilder.java:4191)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitReturn(CFGBuilder.java:1503)
com.sun.tools.javac.tree.JCTree$JCReturn.accept(JCTree.java:1390)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:3317)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:1503)
com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:918)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.process(CFGBuilder.java:1624)
org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.process(CFGBuilder.java:1671)
org.checkerframework.framework.flow.CFCFGBuilder.run(CFCFGBuilder.java:63)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1143)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1120)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1050)
checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:494)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1427)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:247)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:296)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:167)
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:66)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:967)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:502)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:182)
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:190)
checkers.inference.InferenceMain.run(InferenceMain.java:143)
checkers.inference.InferenceMain.main(InferenceMain.java:115)
1 error
--- Inference failed ---
Currently there were a lot code duplication between MaxSatBackEnd
and LingelingBackEnd
.
Should better to refactor this:
Abstract a common Backend named MaxSatBackEnd
, that described the general solving logic for MaxSat-like solvers
Have two concrete sub-classes, Sat4j
and Lingeling
that adapt the concrete solvers.
Currently we have multiple layers of solving process, i.e from SolverEngine
to SolvingStrategy
to underlying Solver
. All of them have a public solve
method which takes necessary informations(constraints, slots, etc.) in and return solution back.
To be consistent, all of these solve()
methods should return InferenceSolution
, instead of return a Map that leaks the underlying implementation.
add it as a downstream travis target
error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing ../../universe/tests/GUTI/TypeVariableUse.java
Compilation unit: ../../universe/tests/GUTI/TypeVariableUse.java
Exception: java.lang.NullPointerException; Stack trace: checkers.inference.InferenceAnnotatedTypeFactory.addComputedTypeAnnotations(InferenceAnnotatedTypeFactory.java:556)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1109)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1015)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:2262)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:754)
checkers.inference.InferenceAnnotatedTypeFactory.performFlowAnalysis(InferenceAnnotatedTypeFactory.java:530)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1161)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:206)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:286)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:1)
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:66)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:978)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:464)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:208)
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:185)
checkers.inference.InferenceMain.run(InferenceMain.java:143)
checkers.inference.InferenceMain.main(InferenceMain.java:115)
2 errors
I'm confused about this part of code in InferenceAnnotatedTypeFactory:
if (this.getClass().equals(InferenceAnnotatedTypeFactory.class)) { this.postInit(); }
GUTIAnnotatedTypeFactory's class is GUTI.GUTIAnnotatedTypeFactory, so the postInit() doesn't get called. As a result treeAnnotator is null and throws NullPointerException. @CharlesZ-Chen
add it as a downstream travis target
context
and z3BitVectorCodec
are not used in Z3Solver. Is it better to instantiate Context
instance and Z3BitVectorCodec
instance in Z3FormatTranslator and provides a getter method to them? What was the point of having these two fields in Z3Solver
if they were not used.Z3FormatTranslator
, we'll not have the issue of creating encoders. due to initialization order no matter we use factory methods or abstract factory pattern.Now that we have a gradle task to generate javadoc, let's ensure it runs correctly and add it to the travis run.
Currently SolverEngine
is a god class and takes a lot of mixed responsibilities:
This makes SolverEngine
hard to be understand.
Should do a refactor of this class to achieve:
SolverEngine
only be an main entry of solver framework and as the central coordinator, and then:
Delegate solving strategy to concrete StrategySolver
s
Delegate statistic responsibility to concrete StatisticRecorder
So ideally the code in SolverEngine
would be something like:
public Map<Integer, AM> solve(Map<String, String> configuration, ...) {
StrategySolver strategySolver = createStrategySolver(configuration, ....);
solution = strategySolver.solve();
postStatistic(solution, ...);
return solution;
}
// Create the concrete Strategy Solver
protected StrategySolver createStrategySolver(....) {
}
// Takes the post-statistic responsibility after solving
protected void postStatistic(solution, ...) {
}
The encoding implementation in LogiQL seems strange:
For each constraint it adds \n
as delimiter, and then using a StringBuilder
concatenate all constraints, then using delimiter split up the String built by StringBuilder
.
It seems strange that using StringBuilder
accumulate constraints and then split it up. Maybe we can just use a List of String and avoid using StringBuilder.
Given variable slots V1 V2
Subtype:
V1 <: V2 where V1.ID == V2.ID ==> AlwaysTrue
else ==> SubtypeConstraint (only solver can compute whether V1 <: V2)
Equality:
V1 == V2 where V1.ID == V2.ID ==> AlwaysTrue
else ==> EqualityConstraint (only solver can compute whether V1 == V2)
Inequality:
V1 != V2 where ID same --> AlwaysFalse
Comparable:
V1 <> V2 where ID same --> AlwaysTrue
This gets rid of constraints such as
25 <: 25, where 25 is a Variable Slot.
idToExistance
to track if solution exists for a variable id, instead of checking whether getting from annotationResults
result is null or not.Using an enum class for managing Solver types result in this class need to be modified each time we add a new type of solver.
Instead of hard coding solver types in an enum class, should refactor to use class hierarchy to manage solver types, i.e.:
Have a root class SolverConfiguration
, that reflectively loading Solver and default translator.
Each concrete solver would have its own sub-class of SolverConfiguration
, and should naming them follow a consistent convention so that SolverEngine
can reflectively load them without require a fully qualified name from user.
Then in SolverEngine
(or in concrete StrategySolver
s), it loads SolverConfiguration
, and delegate the responsibility of initializing underlying solver and formatTranslator to SolverConfiguration
.
There is currently only Dataflow type system that enforces the soundness of MaxSAT solver engine. LogiQL and Z3BitVector backend don't have any tests that use them. It's easy to break the correctness during refactoring.
https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/InferenceVisitor.java#L197
It generates constraint between two ConstantSlots, which is wrong. Our initial purpose is to specify the the VarAnnot in ty is equal to the ConstantSlot that the mod represents. The reason is that, we are using : ty.getAnnotationInHierarchy(mod)
which gets real qualifier. I will propose a fix for this.
There are unique commits that have the same changesets but different hash due to some historical problem, for each of the two repositories. So, if I base my slotmanager on pascaliUWat master branch, there are always those unique commits entering my pull request, bringing in duplicate changes. Is the way of solving this merging each other's master branches first? Otherwise, those unique commits always cause duplication changesets in future pull request between opprop and pascaliUWat. @wmdietl
Last term, we discussed that we need to add two boolean flag: existential and viewpoint adaptation, so that we can separately consider them. My idea is to add withExistential() method to BaseInferrableChecker, and by default it returns true, to let the legacy code leave as they were. For type system like GUT, which has viewpoint adaptation, we override it to return false. Do you think it's a good idea? @wmdietl @CharlesZ-Chen
In InferenceQualifierHierarchy#leastUpperBound()
, it use CombVarSlot
for representing a newly created LUB for the given two VarAnnos.
This is improper as CombVarSlot
is order-sensitive (i.e. a CombVar with receiver a
and target b
is different with a CombVar with receiver b
and target a
a), while LUB of two VarAnno is order-insensitive (i.e. LUB of a
and b
is the same as LUB of b
and a
).
Should create a new type of slot, maybe LUBSlot
, for LUB representation, which internally maintain a set of VarAnnos instead of a list of VarAnnos.
instead of having to construct a list object outside, it can be created as part of the constructor call via array conversion to a list
Inference ATM should only contain one and only one annotation from VarAnnot hierarchy.
After opprop/checker-framework#26 we also need to update CFI to make use of it.
For example currently, inference might generate Bottom
annotations with GUT which shouldn't be the case.
on a SAT solution, the total number of annotations is the same as the number of slots, but what's more interesting is to report # of insert-able / inserted annotations (and in the future, number of annotations that match the default annotations)
each type system may also want to count specific annotations of interest to that type system, thus we should create a general method which can be optionally overridden by each type system to compute the inference solution statistics
https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/solver/backend/z3/Z3Solver.java#L82 should be changed to
serializedConstraint.simplify().isTrue()
see API docs: https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_expr.html#a1e655d15dd6f22b56d49e8cc6d804684
test with a simple equality constraint of say "false = false" as a z3 expression and without simplification, isTrue()
will return false as isTrue()
checks that the z3 expression is equalled to the z3 literal true. That is "false = false".isTrue() == false, whereas "true".isTrue() == true. The simplification is needed.
You might want to check that Ontology results are still the same with this change, hence I filed an issue instead of a PR.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.