From 982b00a059301dd4e7931fc155864dbe619b77e1 Mon Sep 17 00:00:00 2001 From: Weitian Xing Date: Wed, 4 Nov 2020 06:08:08 -0500 Subject: [PATCH 1/5] Reimplement dataflow z3 bit vector. --- .../DataflowAnnotatedTypeFactory.java | 14 +- .../solvers/backend/DataflowSolverEngine.java | 20 ++ .../backend/z3/DataflowZ3BitVectorCodec.java | 191 ++++++++++++++++++ .../z3/DataflowZ3FormatTranslator.java | 17 ++ .../backend/z3/DataflowZ3SolverFactory.java | 14 ++ ...owZ3BitVectorConstraintEncoderFactory.java | 18 ++ src/dataflow/util/DataflowUtils.java | 23 +++ .../dataflowexample/runZ3BitVectorSolver.sh | 25 +++ testing/dataflowexample/travis-test.sh | 5 + 9 files changed, 320 insertions(+), 7 deletions(-) create mode 100644 src/dataflow/solvers/backend/DataflowSolverEngine.java create mode 100644 src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java create mode 100644 src/dataflow/solvers/backend/z3/DataflowZ3FormatTranslator.java create mode 100644 src/dataflow/solvers/backend/z3/DataflowZ3SolverFactory.java create mode 100644 src/dataflow/solvers/backend/z3/encoder/DataflowZ3BitVectorConstraintEncoderFactory.java create mode 100755 testing/dataflowexample/runZ3BitVectorSolver.sh diff --git a/src/dataflow/DataflowAnnotatedTypeFactory.java b/src/dataflow/DataflowAnnotatedTypeFactory.java index 6b2eed359..88cedfe8e 100644 --- a/src/dataflow/DataflowAnnotatedTypeFactory.java +++ b/src/dataflow/DataflowAnnotatedTypeFactory.java @@ -45,7 +45,7 @@ * DataflowAnnotatedTypeFactory is the type factory for Dataflow type system. It * defines the subtype relationship of Dataflow type system, annotate the base * cases, and implements simplification algorithm. - * + * * @author jianchu * */ @@ -117,7 +117,7 @@ public DataFlowQualifierHierarchy(MultiGraphFactory f, AnnotationMirror bottom) /** * This method checks whether rhs is subtype of lhs. rhs and lhs are * both Dataflow types with typeNameRoots argument. - * + * * @param rhs * @param lhs * @return true is rhs is subtype of lhs, otherwise return false. @@ -156,7 +156,7 @@ private boolean isSubtypeWithRoots(AnnotationMirror rhs, AnnotationMirror lhs) { * both Dataflow types without typeNameRoots argument. Currently this * method is not used, but we can use it for a lightweight dataflow type * system. (One without typeNameRoots argument). - * + * * @param rhs * @param lhs * @return true is rhs is subtype of lhs, otherwise return false. @@ -244,11 +244,11 @@ public Void visitMethodInvocation(MethodInvocationTree node, AnnotatedTypeMirror return super.visitMethodInvocation(node, type); } } - + /** - * Simplefication algoirthm. - * - * @param type + * Simplification algorithm. + * + * @param type an annotation mirror to be simplified * @return A simplified annotation. */ public AnnotationMirror refineDataflow(AnnotationMirror type) { diff --git a/src/dataflow/solvers/backend/DataflowSolverEngine.java b/src/dataflow/solvers/backend/DataflowSolverEngine.java new file mode 100644 index 000000000..c76034501 --- /dev/null +++ b/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(); + } + } +} diff --git a/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java b/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java new file mode 100644 index 000000000..81def118b --- /dev/null +++ b/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java @@ -0,0 +1,191 @@ +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(); + this.rootEncodingKeyArr = createRootEncodingKeyArr(); + 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 of each + * {@code @DataFlow annotation} as the elements of encoding key array. + * @return the encoding key array + */ + private String[] createEncodingKeyArr() { + List slots = this.slotManager + .getConstantSlots(); + Set typeNamesSet = new HashSet<>(); + for (ConstantSlot each : slots) { + AnnotationMirror am = each.getValue(); + if (AnnotationUtils.areSameByClass(am, DataFlowInferenceBottom.class) || + AnnotationUtils.areSameByClass(am, DataFlowTop.class)) { + continue; + } + String[] typeNames = DataflowUtils.getTypeNames(am); + typeNamesSet.addAll(Arrays.asList(typeNames)); + } + String[] encodingArr = new String[typeNamesSet.size()]; + int i = 0; + for ( String entry : typeNamesSet) { + encodingArr[i] = entry; + i++; + } + return encodingArr; + } + + /** + * Traverse all the constant slots to get the values in typeNameRoots of each + * {@code @DataFlow annotation} as the elements of root encoding key array. + * @return the root encoding key array + */ + private String[] createRootEncodingKeyArr() { + List slots = this.slotManager + .getConstantSlots(); + Set typeNameRootsSet = new HashSet<>(); + for (ConstantSlot each : slots) { + AnnotationMirror am = each.getValue(); + if (AnnotationUtils.areSameByClass(am, DataFlowInferenceBottom.class) || + AnnotationUtils.areSameByClass(am, DataFlowTop.class)) { + continue; + } + String[] typeNameRoots = DataflowUtils.getTypeNameRoots(am); + typeNameRootsSet.addAll(Arrays.asList(typeNameRoots)); + } + String[] rootEncodingArr = new String[typeNameRootsSet.size()]; + int i = 0; + for ( String entry : typeNameRootsSet) { + rootEncodingArr[i] = entry; + i++; + } + return rootEncodingArr; + } + + /** + * 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 typeNamesSet; + Set 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 find(BigInteger numeralValue, String[] keyArr, BigInteger[] valArr) { + Set 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; + } +} diff --git a/src/dataflow/solvers/backend/z3/DataflowZ3FormatTranslator.java b/src/dataflow/solvers/backend/z3/DataflowZ3FormatTranslator.java new file mode 100644 index 000000000..f1285dffd --- /dev/null +++ b/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(); + } +} diff --git a/src/dataflow/solvers/backend/z3/DataflowZ3SolverFactory.java b/src/dataflow/solvers/backend/z3/DataflowZ3SolverFactory.java new file mode 100644 index 000000000..21a41acb0 --- /dev/null +++ b/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); + } +} diff --git a/src/dataflow/solvers/backend/z3/encoder/DataflowZ3BitVectorConstraintEncoderFactory.java b/src/dataflow/solvers/backend/z3/encoder/DataflowZ3BitVectorConstraintEncoderFactory.java new file mode 100644 index 000000000..091712875 --- /dev/null +++ b/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); + } +} diff --git a/src/dataflow/util/DataflowUtils.java b/src/dataflow/util/DataflowUtils.java index 995b0af2e..bdc53c7dd 100644 --- a/src/dataflow/util/DataflowUtils.java +++ b/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 datatypes, final AnnotationBuilder builder) { String[] datatypesInArray = new String[datatypes.size()]; diff --git a/testing/dataflowexample/runZ3BitVectorSolver.sh b/testing/dataflowexample/runZ3BitVectorSolver.sh new file mode 100755 index 000000000..6fa450880 --- /dev/null +++ b/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 ) diff --git a/testing/dataflowexample/travis-test.sh b/testing/dataflowexample/travis-test.sh index f23a7a8e6..4b3964ffc 100755 --- a/testing/dataflowexample/travis-test.sh +++ b/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 From 1d8de38256007fb2d3d5b689dc9937794f45d38b Mon Sep 17 00:00:00 2001 From: Weitian Xing Date: Wed, 4 Nov 2020 07:51:30 -0500 Subject: [PATCH 2/5] Update README.md. --- src/dataflow/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dataflow/README.md b/src/dataflow/README.md index 9e86afb10..aa5fa7c3a 100644 --- a/src/dataflow/README.md +++ b/src/dataflow/README.md @@ -55,7 +55,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.general.DataflowGeneralSolver --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project + dljc -t inference --checker dataflow.DataflowChecker --solver checkers.inference.solver.SolverEngine --mode ROUNDTRIP --solverArgs="solvingStrategy=Graph,solver=MaxSat" -afud annotated -- ant compile-project ``` 4. Invoke the checker tool with `do-like-javac`. From fa868e535fd4663ef22fc4c4c185bca5598c1495 Mon Sep 17 00:00:00 2001 From: Weitian Xing Date: Wed, 4 Nov 2020 07:52:50 -0500 Subject: [PATCH 3/5] Revert unrelated changes. --- src/dataflow/DataflowAnnotatedTypeFactory.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/dataflow/DataflowAnnotatedTypeFactory.java b/src/dataflow/DataflowAnnotatedTypeFactory.java index 88cedfe8e..6b2eed359 100644 --- a/src/dataflow/DataflowAnnotatedTypeFactory.java +++ b/src/dataflow/DataflowAnnotatedTypeFactory.java @@ -45,7 +45,7 @@ * DataflowAnnotatedTypeFactory is the type factory for Dataflow type system. It * defines the subtype relationship of Dataflow type system, annotate the base * cases, and implements simplification algorithm. - * + * * @author jianchu * */ @@ -117,7 +117,7 @@ public DataFlowQualifierHierarchy(MultiGraphFactory f, AnnotationMirror bottom) /** * This method checks whether rhs is subtype of lhs. rhs and lhs are * both Dataflow types with typeNameRoots argument. - * + * * @param rhs * @param lhs * @return true is rhs is subtype of lhs, otherwise return false. @@ -156,7 +156,7 @@ private boolean isSubtypeWithRoots(AnnotationMirror rhs, AnnotationMirror lhs) { * both Dataflow types without typeNameRoots argument. Currently this * method is not used, but we can use it for a lightweight dataflow type * system. (One without typeNameRoots argument). - * + * * @param rhs * @param lhs * @return true is rhs is subtype of lhs, otherwise return false. @@ -244,11 +244,11 @@ public Void visitMethodInvocation(MethodInvocationTree node, AnnotatedTypeMirror return super.visitMethodInvocation(node, type); } } - + /** - * Simplification algorithm. - * - * @param type an annotation mirror to be simplified + * Simplefication algoirthm. + * + * @param type * @return A simplified annotation. */ public AnnotationMirror refineDataflow(AnnotationMirror type) { From f5d31ba92a12b799470789bc3243b1ac8b8fa59b Mon Sep 17 00:00:00 2001 From: Weitian Xing Date: Wed, 4 Nov 2020 07:53:23 -0500 Subject: [PATCH 4/5] Revert "Update README.md." This reverts commit 1d8de382 --- src/dataflow/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dataflow/README.md b/src/dataflow/README.md index aa5fa7c3a..9e86afb10 100644 --- a/src/dataflow/README.md +++ b/src/dataflow/README.md @@ -55,7 +55,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 checkers.inference.solver.SolverEngine --mode ROUNDTRIP --solverArgs="solvingStrategy=Graph,solver=MaxSat" -afud annotated -- ant compile-project + dljc -t inference --checker dataflow.DataflowChecker --solver dataflow.solvers.general.DataflowGeneralSolver --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project ``` 4. Invoke the checker tool with `do-like-javac`. From b9db60e628d3b486c4b418729a920db842532315 Mon Sep 17 00:00:00 2001 From: Weitian Xing Date: Wed, 4 Nov 2020 08:32:08 -0500 Subject: [PATCH 5/5] Improve code. --- .../backend/z3/DataflowZ3BitVectorCodec.java | 52 ++++++------------- 1 file changed, 15 insertions(+), 37 deletions(-) diff --git a/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java b/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java index 81def118b..e9d711a00 100644 --- a/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java +++ b/src/dataflow/solvers/backend/z3/DataflowZ3BitVectorCodec.java @@ -45,66 +45,44 @@ public class DataflowZ3BitVectorCodec implements Z3BitVectorCodec { DataflowZ3BitVectorCodec() { this.realATF = (DataflowAnnotatedTypeFactory) InferenceMain.getInstance().getRealTypeFactory(); this.slotManager = InferenceMain.getInstance().getSlotManager(); - this.encodingKeyArr = createEncodingKeyArr(); - this.rootEncodingKeyArr = createRootEncodingKeyArr(); + 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 of each - * {@code @DataFlow annotation} as the elements of encoding key array. + * 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() { + private String[] createEncodingKeyArr(boolean root) { List slots = this.slotManager .getConstantSlots(); - Set typeNamesSet = new HashSet<>(); + Set 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; } - String[] typeNames = DataflowUtils.getTypeNames(am); - typeNamesSet.addAll(Arrays.asList(typeNames)); + if (root) { + types = DataflowUtils.getTypeNameRoots(am); + } else { + types = DataflowUtils.getTypeNames(am); + } + set.addAll(Arrays.asList(types)); } - String[] encodingArr = new String[typeNamesSet.size()]; + String[] encodingArr = new String[set.size()]; int i = 0; - for ( String entry : typeNamesSet) { + for ( String entry : set) { encodingArr[i] = entry; i++; } return encodingArr; } - /** - * Traverse all the constant slots to get the values in typeNameRoots of each - * {@code @DataFlow annotation} as the elements of root encoding key array. - * @return the root encoding key array - */ - private String[] createRootEncodingKeyArr() { - List slots = this.slotManager - .getConstantSlots(); - Set typeNameRootsSet = new HashSet<>(); - for (ConstantSlot each : slots) { - AnnotationMirror am = each.getValue(); - if (AnnotationUtils.areSameByClass(am, DataFlowInferenceBottom.class) || - AnnotationUtils.areSameByClass(am, DataFlowTop.class)) { - continue; - } - String[] typeNameRoots = DataflowUtils.getTypeNameRoots(am); - typeNameRootsSet.addAll(Arrays.asList(typeNameRoots)); - } - String[] rootEncodingArr = new String[typeNameRootsSet.size()]; - int i = 0; - for ( String entry : typeNameRootsSet) { - rootEncodingArr[i] = entry; - i++; - } - return rootEncodingArr; - } - /** * Create both encoding value array and root encoding value array. * @param ordinal the start ordinal