Reimplement z3 bit vector solving for dataflow type system.

src/dataflow/solvers/backend/DataflowSolverEngine.java

@@ -0,0 +1,20 @@
+package dataflow.solvers.backend;
+
+import checkers.inference.solver.SolverEngine;
+import checkers.inference.solver.backend.SolverFactory;
+import checkers.inference.solver.backend.z3.Z3Solver;
+import checkers.inference.solver.util.NameUtils;
+
+import dataflow.solvers.backend.z3.DataflowZ3SolverFactory;
+
+public class DataflowSolverEngine extends SolverEngine {
+
+    @Override
+    protected SolverFactory createSolverFactory() {
+        if (NameUtils.getSolverName(Z3Solver.class).equals(solverName)) {
+            return new DataflowZ3SolverFactory();
+        } else {
+            return super.createSolverFactory();
+        }
+    }
+}

src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java

@@ -0,0 +1,169 @@
+package dataflow.solvers.backend.z3;
+
+import checkers.inference.InferenceMain;
+import checkers.inference.SlotManager;
+import checkers.inference.model.ConstantSlot;
+import checkers.inference.solver.backend.z3.Z3BitVectorCodec;
+
+
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
+import org.checkerframework.org.apache.commons.lang3.ArrayUtils;
+
+import java.math.BigInteger;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.AnnotationMirror;
+
+import dataflow.DataflowAnnotatedTypeFactory;
+import dataflow.qual.DataFlowInferenceBottom;
+import dataflow.qual.DataFlowTop;
+import dataflow.util.DataflowUtils;
+
+/**
+ * The Z3 bit vector codec for dataflow type system.
+ */
+public class DataflowZ3BitVectorCodec implements Z3BitVectorCodec {
+
+    /** The real annotated type factory. */
+    private final DataflowAnnotatedTypeFactory realATF;
+    /** The encoding key array containing java types exist in typeNames. */
+    private final String[] encodingKeyArr;
+    /** The encoding value array containing encoded bits for each java type in {@code encodingKeyArr}. */
+    private final BigInteger[] encodingValArr;
+    /** The root encoding key array containing java types exist in typeNameRoots. */
+    private final String[] rootEncodingKeyArr;
+    /** The root encoding value array containing encoded bits for each java type in {@code rootEncodingKeyArr}. */
+    private final BigInteger[] rootEncodingValArr;
+    /** The slot manager. */
+    private final SlotManager slotManager;
+
+    DataflowZ3BitVectorCodec() {
+        this.realATF = (DataflowAnnotatedTypeFactory) InferenceMain.getInstance().getRealTypeFactory();
+        this.slotManager = InferenceMain.getInstance().getSlotManager();
+        this.encodingKeyArr = createEncodingKeyArr(false);
+        this.rootEncodingKeyArr = createEncodingKeyArr(true);
+        this.encodingValArr = createEncodingValArr(0, this.encodingKeyArr.length);
+        this.rootEncodingValArr = createEncodingValArr(this.encodingKeyArr.length, this.rootEncodingKeyArr.length);
+    }
+
+    /**
+     * Traverse all the constant slots to get the values in typeNames/typeNameRoots of each
+     * {@code @DataFlow} annotation as the elements of encoding key array.
+     * @return the encoding key array
+     */
+    private String[] createEncodingKeyArr(boolean root) {
+        List<ConstantSlot> slots = this.slotManager
+            .getConstantSlots();
+        Set<String> set = new HashSet<>();
+        String[] types;
+        for (ConstantSlot each : slots) {
+            AnnotationMirror am = each.getValue();
+            if (AnnotationUtils.areSameByClass(am, DataFlowInferenceBottom.class) ||
+                AnnotationUtils.areSameByClass(am, DataFlowTop.class)) {
+                continue;
+            }
+            if (root) {
+                types = DataflowUtils.getTypeNameRoots(am);
+            } else {
+                types = DataflowUtils.getTypeNames(am);
+            }
+            set.addAll(Arrays.asList(types));
+        }
+        String[] encodingArr = new String[set.size()];
+        int i = 0;
+        for ( String entry : set) {
+            encodingArr[i] = entry;
+            i++;
+        }
+        return encodingArr;
+    }
+
+    /**
+     * Create both encoding value array and root encoding value array.
+     * @param ordinal the start ordinal
+     * @param size the size of the output array
+     * @return the encoded array
+     */
+    private BigInteger[] createEncodingValArr(int ordinal, int size) {
+        BigInteger[] encodingValArr = new BigInteger[size];
+        for (int i = 0; i < size; i++) {
+            BigInteger encode = BigInteger.ZERO.setBit(ordinal);
+            encodingValArr[i] = encode;
+            ordinal++;
+        }
+        return encodingValArr;
+    }
+
+    @Override
+    public int getFixedBitVectorSize() {
+        if ((this.encodingKeyArr.length / 2 + this.rootEncodingKeyArr.length / 2) > Integer.MAX_VALUE / 2) {
+            throw new BugInCF("(encodingKeyArr + rootEncodingKeyArr)'s size is too big.");
+        }
+        return this.encodingKeyArr.length + this.rootEncodingKeyArr.length;
+    }
+
+    @Override
+    public BigInteger encodeConstantAM(AnnotationMirror am) {
+        if (AnnotationUtils.areSameByClass(am, DataFlowTop.class)) {
+            return BigInteger.valueOf(-1);
+        }
+        if (AnnotationUtils.areSameByClass(am, DataFlowInferenceBottom.class)) {
+            return BigInteger.valueOf(0);
+        }
+        String[] typeNames = DataflowUtils.getTypeNames(am);
+        String[] typeNameRoots = DataflowUtils.getTypeNameRoots(am);
+        BigInteger encode = BigInteger.ZERO;
+        for (String each : typeNames) {
+            int i = ArrayUtils.indexOf(this.encodingKeyArr, each);
+            encode = encode.or(this.encodingValArr[i]);
+        }
+        for (String each : typeNameRoots) {
+            int i = ArrayUtils.indexOf(this.rootEncodingKeyArr, each);
+            encode = encode.or(this.rootEncodingValArr[i]);
+        }
+        return encode;
+    }
+
+    @Override
+    public AnnotationMirror decodeNumeralValue(BigInteger numeralValue,
+        ProcessingEnvironment processingEnvironment) {
+        Set<String> typeNamesSet;
+        Set<String> typeNameRootsSet;
+        if (numeralValue.equals(BigInteger.valueOf(-1))) {
+            return DataflowUtils.createDataflowTop(realATF.getProcessingEnv());
+        }
+        if (numeralValue.equals(BigInteger.valueOf(0))) {
+            return DataflowUtils.createDataflowBottom(realATF.getProcessingEnv());
+        }
+        typeNamesSet = find(numeralValue, this.encodingKeyArr, this.encodingValArr);
+        typeNameRootsSet = find(numeralValue, this.rootEncodingKeyArr, this.rootEncodingValArr);
+        return DataflowUtils.createDataflowAnnotationWithRoots(typeNamesSet, typeNameRootsSet, processingEnvironment);
+    }
+
+    /**
+     * Find the set of java types in string representation using the encoded numeral value.
+     * @param numeralValue the encoded bits
+     * @param keyArr the (root) encoding key array
+     * @param valArr the (root) encoding value array
+     * @return the decoded set of java types
+     */
+    private Set<String> find(BigInteger numeralValue, String[] keyArr, BigInteger[] valArr) {
+        Set<String> set = new HashSet<>();
+        for(int i = 0; i < keyArr.length; i++) {
+            String typeName = keyArr[i];
+            BigInteger value = valArr[i];
+            if (value.and(numeralValue).equals(value)) {
+                set.add(typeName);
+                if(numeralValue.equals(value)) {
+                    break;
+                }
+            }
+        }
+        return set;
+    }
+}

src/dataflow/solvers/backend/z3/DataflowZ3FormatTranslator.java

@@ -0,0 +1,17 @@
+package dataflow.solvers.backend.z3;
+
+import checkers.inference.solver.backend.z3.Z3BitVectorCodec;
+import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator;
+import checkers.inference.solver.frontend.Lattice;
+
+public class DataflowZ3FormatTranslator extends Z3BitVectorFormatTranslator {
+
+    public DataflowZ3FormatTranslator(Lattice lattice) {
+        super(lattice);
+    }
+
+    @Override
+    protected Z3BitVectorCodec createZ3BitVectorCodec() {
+        return new DataflowZ3BitVectorCodec();
+    }
+}

src/dataflow/solvers/backend/z3/DataflowZ3SolverFactory.java

@@ -0,0 +1,14 @@
+package dataflow.solvers.backend.z3;
+
+import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator;
+import checkers.inference.solver.backend.z3.Z3SolverFactory;
+import checkers.inference.solver.frontend.Lattice;
+
+
+public class DataflowZ3SolverFactory extends Z3SolverFactory {
+
+    @Override
+    protected Z3BitVectorFormatTranslator createFormatTranslator(Lattice lattice) {
+        return new DataflowZ3FormatTranslator(lattice);
+    }
+}

src/dataflow/solvers/backend/z3/encoder/DataflowZ3BitVectorConstraintEncoderFactory.java

@@ -0,0 +1,18 @@
+package dataflow.solvers.backend.z3.encoder;
+
+import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator;
+import checkers.inference.solver.backend.z3.encoder.Z3BitVectorConstraintEncoderFactory;
+import checkers.inference.solver.frontend.Lattice;
+
+import com.microsoft.z3.Context;
+
+public class DataflowZ3BitVectorConstraintEncoderFactory extends
+    Z3BitVectorConstraintEncoderFactory {
+
+    public DataflowZ3BitVectorConstraintEncoderFactory(
+        Lattice lattice,
+        Context context,
+        Z3BitVectorFormatTranslator formatTranslator) {
+        super(lattice, context, formatTranslator);
+    }
+}

src/dataflow/util/DataflowUtils.java

@@ -1,5 +1,6 @@
 package dataflow.util;
 
+import java.lang.annotation.Annotation;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -16,6 +17,8 @@
 import com.sun.source.tree.LiteralTree;
 
 import dataflow.qual.DataFlow;
+import dataflow.qual.DataFlowInferenceBottom;
+import dataflow.qual.DataFlowTop;
 
 /**
  * Utility class for Dataflow type system.
@@ -53,6 +56,26 @@ public static AnnotationMirror createDataflowAnnotationForByte(String[] dataType
         return builder.build();
     }
 
+    /**
+     * Create a {@code @DataFlowTop}.
+     * @param processingEnv the processing environment
+     * @return a DataFlowTop annotation mirror
+     */
+    public static AnnotationMirror createDataflowTop(ProcessingEnvironment processingEnv) {
+        AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlowTop.class);
+        return builder.build();
+    }
+
+    /**
+     * Create a {@code @DataFlowInferenceBottom}.
+     * @param processingEnv the processing environment
+     * @return a DataFlowInferenceBottom annotation mirror
+     */
+    public static AnnotationMirror createDataflowBottom(ProcessingEnvironment processingEnv) {
+        AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DataFlowInferenceBottom.class);
+        return builder.build();
+    }
+
     private static AnnotationMirror createDataflowAnnotation(final Set<String> datatypes,
             final AnnotationBuilder builder) {
         String[] datatypesInArray = new String[datatypes.size()];

testing/dataflowexample/runZ3BitVectorSolver.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+WORKING_DIR=$(cd $(dirname "$0") && pwd)
+
+JSR308=$(cd $WORKING_DIR/../../../ && pwd)
+
+CFI=$JSR308/checker-framework-inference
+
+Z3=$JSR308/z3/bin
+export PATH=$Z3:$PATH
+
+DLJC=$JSR308/do-like-javac
+
+CFI_LIB=$CFI/lib
+export DYLD_LIBRARY_PATH=$CFI_LIB
+export LD_LIBRARY_PATH=$CFI_LIB
+
+( cd $WORKING_DIR && \
+$DLJC/dljc -t inference \
+    --guess --crashExit \
+    --checker dataflow.DataflowChecker \
+    --solver dataflow.solvers.backend.DataflowSolverEngine \
+    --solverArgs="solver=Z3" \
+    --mode ROUNDTRIP -o $WORKING_DIR/logs \
+    -afud $WORKING_DIR/annotated -- ant compile-project )

testing/dataflowexample/travis-test.sh

@@ -28,3 +28,8 @@ $WORKING_DIR/cleanup.sh
 echo -e "\nRunning LingelingSolver\n"
 $WORKING_DIR/runLingelingSolver.sh
 $WORKING_DIR/cleanup.sh
+
+# test using z3 (external) solver
+echo -e "\nRunning Z3Solver\n"
+$WORKING_DIR/runZ3BitVectorSolver.sh
+$WORKING_DIR/cleanup.sh