opprop / checker-framework-inference Goto Github PK

View Code? Open in Web Editor NEW

This project forked from typetools/checker-framework-inference

6.0 6.0 13.0 4.48 MB

Inference of pluggable types for Java

Shell 1.11% Java 98.36% Python 0.53%

checker-framework-inference's People

Contributors

Stargazers

Watchers

Forkers

jyluo luqmana pascaliuwat baoruiz xingweitian txiang61 zcai1 leoliu49 d367wang al3xliu piyush-j andrewshf ao-senxiong

checker-framework-inference's Issues

[Solver Framework] Early verification of constant constraints

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.

Potential bugs at constraint generation stage.

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 ConstantUtils in old GTIS?

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 ？

Missing VarAnnot for inferred type argument

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.

Wrong use of InferenceQualifierHierarchy.isSubtype() in ConstraintManager

In ConstraintManager, it use qualifierHierarchy.isSubtype() to do subtype relationship evaluation, for example:

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/model/ConstraintManager.java#L73

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/model/ConstraintManager.java#L121

However, the qualifierHierarchy field is initialized by inferenceAnnotatedTypeFactory.getQualifierHierarchy():

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/model/ConstraintManager.java#L41

By default, the qualifierHierarchy in an inferenceAnnotatedTypeFactory is an instance of InferenceQualifierHierarchy:

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/InferenceAnnotatedTypeFactory.java#L196

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.

LogiQLFormatTranslator does nothing in decodeSolution() method

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.

[solver framework] Constraint graph refactor

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.

Cleanup all hashcode() methods to use hashcode utils

Refactor architecture of Slots

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:

ConstantSlot
(Plain)VariableSlot (insertable; for all other constraint variables not represented by one of the ones below)
ExistentialVariableSlot
RefinementVariableSlot
LUBVariableSlot
CombVariableSlot
ArithmeticVariableSlot
PolyInvokeVariableSlot (constraint variable created to replace "PolyAll", etc, at each method call site, and never inserted; also enables more fine grained statistics tracking)

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

Unable to insert super constructor parameter which is not in current compilation unit tree

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:

checker-framework-inference/src/checkers/inference/VariableAnnotator.java

Line 635 in 85c6088

VariableSlot primary = addPrimaryVariable(adt, tree);

When 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.

[Solver Framework] Refactor GraphBuilder

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.

CFI doesn't create refinement variable slot for local variable tree

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.

[Solver framework] Refactor PrintUtils and StatisticKey

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.

[Solver Framework] Refactor VariableCombos

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.

Duplicate VectorUtils in CFI

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

getEffectiveAnnotations() return empty set for type variable with intersection typed upper bound

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.

[Solver Framework] Refactor Lattice class

Currently, TwoQualLattice is a sub-class of Lattice, which cause null parameters passing in super constructor call, see:

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/solver/frontend/TwoQualifiersLattice.java#L25

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.

Order matters when doing inference

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.

checker.jar is not used first in inference

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?

Remove uses of CF `Unqualified` annotation

CFI uses the Unqualified annotation in certain situations, e.g. here:

https://github.com/opprop/checker-framework-inference/blob/master/src/checkers/inference/InferenceAnnotatedTypeFactory.java#L148

All these uses should be removed and the "real" type annotations should be used instead.

Lacking contradictory value for LogiQLAbstractConstraintEncoder

We need help from Jason to see which String can directly cause solver to fail.

Inference crashes in CFGBuilder CFGTranslationPhaseOne

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 ---

[Solver Framework] Refactor MaxSat Backends

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.

add Units as a travis downstream target

All solve() method should return InferenceSolution consistently.

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.

Update Serializer<S, T> type parameter names after new constraints and slots are merged

Update PICO to be compatible with latest opprop/CFI changes

add it as a downstream travis target

postInit() doesns't get called in GUTInferenceAnnotatedTypeFactory

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

[Solver framework] Refactor `SolverAdapter` ( original `BackEnd`) class

Update GUT to be compatible with latest opprop/CFI changes

add it as a downstream travis target

Unused context and z3BitVectorCodec field in Z3Solver

checker-framework-inference/src/checkers/inference/solver/backend/z3/Z3Solver.java

Line 28 in 168aba4

protected final Context context;

checker-framework-inference/src/checkers/inference/solver/backend/z3/Z3Solver.java

Line 30 in 168aba4

protected final Z3BitVectorCodec z3BitVectorCodec;

Field 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.
If we move them to Z3FormatTranslator, we'll not have the issue of creating encoders. due to initialization order no matter we use factory methods or abstract factory pattern.

Fix javadoc issues

Now that we have a gradle task to generate javadoc, let's ensure it runs correctly and add it to the travis run.

[Solver framework] Refactor `SolverEngine` (original `GeneralSolver`) class

Currently SolverEngine is a god class and takes a lot of mixed responsibilities:

user end solver configuration
statistics
algorithm template definition for concrete solving strategies (grape solving, single solver solving, etc.)

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 StrategySolvers
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, ...) {
}

[Solver Framework] Refactor encoding for LogiQL

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.

CFI creates empty ASTPath for constructor return

Once slots (constraint variables) have IDs, further add normalization cases to binary cosntraints

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.

No action taken if existence conflicts happens in IFlowSolution and DataflowSolution

checker-framework-inference/src/sparta/checkers/sat/IFlowSolution.java

Line 83 in 85c6088

 InferenceMain.getInstance().logger.log(Level.INFO, "Mismatch between existance of annotation"); 

At the above line, if existence conflict happens(alreadyExists and existsPermission), instead of simply logging an info message, no action is taken at all. This sounds like a mismatch. Is this really correct? @wmdietl
Same thing exists in DataflowSolution.
This causes the consequence that we need to have a separate map idToExistance to track if solution exists for a variable id, instead of checking whether getting from annotationResults result is null or not.

[solver framework] Refactor `SolverType` enum class

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 StrategySolvers), it loads SolverConfiguration, and delegate the responsibility of initializing underlying solver and formatTranslator to SolverConfiguration.

Lack of testcases for LogiQL and Z3BitVector backend

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.

Adapt Dataflow type system to use SolverEngine and MaxSat / Lingeling backends

1 Wrong constraint generation because of wrong hierarchy

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.

How to solve the discrepencies between opprop master and pascaliUWat master

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

Add withExistential() into BaseInferrableChecker?

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

Don't use CombVarSlot for LUB representation

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 aa), 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.

Constraint constructors should take in a vararg of Slots

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

Really remove real qualifier from inference atm

Inference ATM should only contain one and only one annotation from VarAnnot hierarchy.

Enforce TargetLocations in CFI

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.

Add counting of inference solutions' annotations as a statistic output

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

z3 constraints need to be simplified to check for tautology

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.