Masterworkable

README.md

@@ -88,9 +88,7 @@ and then inserts the results back into the original source code.
 If the whole process runs successfully, the inserted output will be placed in `annotated` directory.
 
   ```
-  dljc -t inference --checker dataflow.DataflowChecker
-    --solver dataflow.solvers.classic.DataflowSolver -o logs 
-    -m ROUNDTRIP -afud annotated -- ant compile-project
+  dljc -t inference --checker dataflow.DataflowChecker --solver dataflow.solvers.backend.DataflowConstraintSolver --mode ROUNDTRIP --solverArgs="backEndType=maxsatbackend.MaxSat" -afud annotated -- ant compile-project
   ```
 
 3. Invoke the checker tool with `do-like-javac`.

scripts/dataflow/inference-MAXSAT-parallel.sh

@@ -5,6 +5,6 @@ export MYDIR=`dirname $0`/..
 export ROOT=$MYDIR/../..
 distDir=$CHINF"/dist"
 
-export CLASSPATH=$ROOT/generic-type-inference-solver/bin:.
+export CLASSPATH=$ROOT/generic-type-inference-solver/bin:/home/jianchu/jsr308/checker-framework-inference/dist/plume.jar:.
 
 $ROOT/checker-framework-inference/scripts/inference-dev checkers.inference.InferenceLauncher --solverArgs="backEndType=maxsatbackend.MaxSat" --checker dataflow.DataflowChecker --solver dataflow.solvers.backend.DataflowConstraintSolver --mode INFER --hacks=true $*

scripts/dataflow/inference-debug.sh

@@ -5,6 +5,6 @@ export MYDIR=`dirname $0`/..
 export ROOT=$MYDIR/../..
 distDir=$CHINF"/dist"
 
-export CLASSPATH=$ROOT/generic-type-inference-solver/bin:.
+export CLASSPATH=$ROOT/generic-type-inference-solver/bin:/home/jianchu/jsr308/checker-framework-inference/dist/plume.jar:.
 
 $ROOT/checker-framework-inference/scripts/inference-dev checkers.inference.InferenceLauncher --checker dataflow.DataflowChecker --solver checkers.inference.solver.DebugSolver --mode INFER --hacks=true $*

scripts/dataflow/inference-logiQL.sh

@@ -6,7 +6,7 @@ export ROOT=$MYDIR/../..
 export LOGICDATA=./logiqldata
 distDir=$CHINF"/dist"
 
-export CLASSPATH=$ROOT/generic-type-inference-solver/bin:.
+export CLASSPATH=$ROOT/generic-type-inference-solver/bin:/home/jianchu/jsr308/checker-framework-inference/dist/plume.jar:.
 
 $ROOT/checker-framework-inference/scripts/inference-dev checkers.inference.InferenceLauncher --solverArgs="backEndType=logiqlbackend.LogiQL" --checker dataflow.DataflowChecker --solver dataflow.solvers.backend.DataflowConstraintSolver --mode INFER --hacks=true $*
-rm -r $LOGICDATA
+#rm -r $LOGICDATA

scripts/dataflow/typecheck.sh

@@ -5,6 +5,6 @@ export MYDIR=`dirname $0`/..
 export ROOT=$MYDIR/../..
 distDir=$CHINF"/dist"
 
-export CLASSPATH=$ROOT/generic-type-inference-solver/bin:.
+export CLASSPATH=$ROOT/generic-type-inference-solver/bin:/home/jianchu/jsr308/checker-framework-inference/dist/plume.jar:.
 
 $ROOT/checker-framework-inference/scripts/inference-dev checkers.inference.InferenceLauncher --checker dataflow.DataflowChecker --mode TYPECHECK --hacks=true $*

scripts/ostrusted/typecheck.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+export MYDIR=`dirname $0`/..
+. $MYDIR/setup.sh
+export ROOT=$MYDIR/../..
+distDir=$CHINF"/dist"
+java -classpath "$distDir"/checker.jar:"$distDir"/plume.jar:"$distDir"/checker-framework-inference.jar:$ROOT/generic-type-inference-solver/bin:.  checkers.inference.InferenceLauncher --checker ostrusted.OsTrustedChecker --mode TYPECHECK --hacks=true $*

src/constraintgraph/ConstraintGraph.java

@@ -1,7 +1,6 @@
 package constraintgraph;
 
 import java.util.ArrayList;
-import java.util.Collection;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.LinkedList;
@@ -27,7 +26,6 @@ public class ConstraintGraph {
     private Map<Vertex, Set<Constraint>> constantPath;
     private Map<Integer, Vertex> verticies;
     private List<Set<Constraint>> independentPath;
-    private Collection<Constraint> missingConstraints = new HashSet<>();
 
     protected ConstraintGraph() {
         this.edges = new HashSet<Edge>();
@@ -63,11 +61,6 @@ protected void addConstantPath(Vertex vertex, Set<Constraint> constraints) {
         this.constantPath.put(vertex, constraints);
     }
 
-    protected void addEdgeToConstantPath(Vertex vertex, Constraint constraint) {
-        Set<Constraint> constrants = this.constantPath.get(vertex);
-        constrants.add(constraint);
-    }
-
     public List<Set<Constraint>> getIndependentPath() {
         return this.independentPath;
     }
@@ -81,15 +74,6 @@ protected void addConstant(Vertex vertex) {
             this.constantVerticies.add(vertex);
         }
     }
-
-    public Edge findEdge(Constraint constraint) {
-        for (Edge edge : this.edges) {
-            if (edge.getConstraint().equals(constraint)) {
-                return edge;
-            }
-        }
-        return null;
-    }
 
     protected void createEdge(Slot slot1, Slot slot2, Constraint constraint) {
         Integer slot1Id = ((VariableSlot) slot1).getId();
@@ -121,12 +105,4 @@ protected void createEdge(Slot slot1, Slot slot2, Constraint constraint) {
 
         this.addEdge(edge);
     }
-
-    public Collection<Constraint> getMissingConstraints() {
-        return this.missingConstraints;
-    }
-
-    public void SetMissingConstraints(Collection<Constraint> missingConstraint) {
-        this.missingConstraints = missingConstraint;
-    }
-}
+}

src/constraintgraph/Edge.java

@@ -64,4 +64,4 @@ public boolean equals(Object o) {
     public int hashCode() {
         return Objects.hash(from, to);
     }
-}
+}

src/constraintgraph/GraphBuilder.java

@@ -1,19 +1,24 @@
 package constraintgraph;
 
+import org.checkerframework.javacutil.AnnotationUtils;
+
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.HashMap;
 import java.util.HashSet;
 import java.util.LinkedList;
 import java.util.Map;
 import java.util.Queue;
 import java.util.Set;
 
+import javax.lang.model.element.AnnotationMirror;
+
+import checkers.inference.model.AnnotationLocation.Kind;
 import checkers.inference.model.ConstantSlot;
 import checkers.inference.model.Constraint;
 import checkers.inference.model.ExistentialConstraint;
 import checkers.inference.model.Slot;
 import checkers.inference.model.SubtypeConstraint;
+import dataflow.util.DataflowUtils;
 
 /**
  * ConstraintGraph Builder
@@ -26,37 +31,34 @@ public class GraphBuilder {
     private final Collection<Slot> slots;
     private final Collection<Constraint> constraints;
     private final ConstraintGraph graph;
-    private SubtypeDirection subtypeDirection = SubtypeDirection.UNDIRECTED;
-    private Map<Vertex, Set<Vertex>> vertexCache = new HashMap<>();
-    private Collection<Constraint> missingConstraints = new HashSet<>();
-
+    private AnnotationMirror top;
+
     public GraphBuilder(Collection<Slot> slots, Collection<Constraint> constraints) {
         this.slots = slots;
         this.constraints = constraints;
         this.graph = new ConstraintGraph();
     }
 
-    public GraphBuilder(Collection<Slot> slots, Collection<Constraint> constraints,
-            SubtypeDirection subtypeDirection) {
+    public GraphBuilder(Collection<Slot> slots, Collection<Constraint> constraints, AnnotationMirror top) {
         this(slots, constraints);
-        this.subtypeDirection = subtypeDirection;
+        this.top = top;
     }
 
     public ConstraintGraph buildGraph() {
         for (Constraint constraint : constraints) {
             if (constraint instanceof SubtypeConstraint) {
                 addSubtypeEdge((SubtypeConstraint) constraint);
-            } else if (!(constraint instanceof ExistentialConstraint)) {
+            } else if (constraint instanceof ExistentialConstraint) {
+                continue;
+            } else {
                 ArrayList<Slot> slots = new ArrayList<Slot>();
                 slots.addAll(constraint.getSlots());
                 addEdges(slots, constraint);
             }
         }
-
         addConstant();
         calculateIndependentPath();
         calculateConstantPath();
-        // System.out.println(this.missingConstraint);
         // printEdges();
         // printGraph();
         return getGraph();
@@ -87,31 +89,10 @@ private void calculateIndependentPath() {
     }
 
     private void calculateConstantPath() {
-        Collection<Constraint> alias = new HashSet<Constraint>(this.constraints);
         for (Vertex vertex : this.graph.getConstantVerticies()) {
             Set<Constraint> constantPathConstraints = BFSSearch(vertex);
-            alias.removeAll(constantPathConstraints);
             this.graph.addConstantPath(vertex, constantPathConstraints);
         }
-        this.graph.SetMissingConstraints(alias);
-        missingConstraints = alias;
-        // addMissingVertex(alias);
-    }
-
-    private void addMissingVertex(Collection<Constraint> alias) {
-        for (Constraint constraint : alias) {
-            Edge edge = this.graph.findEdge(constraint);
-            if (edge != null) {
-                Vertex from = edge.getFromVertex();
-                Vertex to = edge.getToVertex();
-                for (Map.Entry<Vertex, Set<Vertex>> entry : this.vertexCache.entrySet()) {
-                    Set<Vertex> vertexes = entry.getValue();
-                    if (vertexes.contains(from) || vertexes.contains(to)) {
-                        this.graph.addEdgeToConstantPath(entry.getKey(), constraint);
-                    }
-                }
-            }
-        }
     }
 
     private Set<Constraint> BFSSearch(Vertex vertex) {
@@ -123,27 +104,28 @@ private Set<Constraint> BFSSearch(Vertex vertex) {
             Vertex current = queue.remove();
             visited.add(current);
             for (Edge edge : current.getEdges()) {
-                if (edge instanceof SubtypeEdge) {
-                    if (this.subtypeDirection.equals(SubtypeDirection.FROMSUBTYPE)
-                            && current.equals(edge.to)) {
-                        continue;
-                    } else if (this.subtypeDirection.equals(SubtypeDirection.FROMSUPERTYPE)
-                            && current.equals(edge.from)) {
-                        continue;
-                    }
+                if ((edge instanceof SubtypeEdge) && current.equals(edge.to)) {
+                    continue;
                 }
-                constantPathConstraints.add(edge.getConstraint());
                 Vertex next = edge.getToVertex();
-                Set<Vertex> cacheSet;
-                if (this.vertexCache.keySet().contains(vertex)) {
-                    cacheSet = vertexCache.get(vertex);
-                } else {
-                    cacheSet = new HashSet<Vertex>();
-                }
-                cacheSet.add(current);
-                cacheSet.add(next);
-                this.vertexCache.put(vertex, cacheSet);
+                constantPathConstraints.add(edge.getConstraint());
                 if (!visited.contains(next)) {
+                    if (next.isConstant()) {
+                        if (AnnotationUtils.areSame(top, next.getValue())) {
+                            continue;
+                        } else {
+                            String[] typeNames = DataflowUtils.getTypeNames(next.getValue());
+                            if (typeNames.length == 1 && typeNames[0].length() == 0) {
+                                continue;
+                            }
+                        }
+                    } else {
+                        if (next.getSlot().getLocation() != null) {
+                            if (next.getSlot().getLocation().getKind().equals(Kind.MISSING)) {
+                                continue;
+                            }
+                        }
+                    }
                     queue.add(next);
                 }
             }
@@ -195,9 +177,6 @@ private void printEdges() {
         for (Map.Entry<Vertex, Set<Constraint>> entry : this.graph.getConstantPath().entrySet()) {
             System.out.println(entry.getKey().getSlot());
             for (Constraint constraint : entry.getValue()) {
-                if (constraint instanceof ExistentialConstraint) {
-                    continue;
-                }
                 System.out.println(constraint);
             }
             System.out.println("**************");
@@ -225,8 +204,4 @@ private void printGraph() {
             System.out.println(vertex.getId());
         }
     }
-
-    public enum SubtypeDirection {
-        UNDIRECTED, FROMSUBTYPE, FROMSUPERTYPE
-    }
-}
+}

src/constraintgraph/Vertex.java

@@ -48,7 +48,7 @@ protected void addEdge(Edge edge) {
         }
     }
 
-    public Slot getSlot() {
+    protected Slot getSlot() {
         return this.slot;
     }
 
@@ -82,4 +82,4 @@ public boolean equals(Object o) {
     public int hashCode() {
         return id;
     }
-}
+}