From 528c2d511d2a520b663be63c44be0a3e05e2741b Mon Sep 17 00:00:00 2001 From: txiang61 Date: Wed, 23 Oct 2019 16:33:13 -0400 Subject: [PATCH 01/24] Added operation kind for comparable constraints encoder and its slot --- .../inference/DefaultSlotManager.java | 41 +++++++ src/checkers/inference/SlotManager.java | 24 ++++ .../inference/model/ArithmeticConstraint.java | 20 +++- .../inference/model/ComparableConstraint.java | 104 +++++++++++++++++- .../model/ComparableVariableSlot.java | 36 ++++++ .../inference/model/ConstraintManager.java | 18 +++ src/checkers/inference/model/Slot.java | 1 + .../binary/ComparableConstraintEncoder.java | 15 +++ .../LogiQLComparableConstraintEncoder.java | 42 ++++++- .../MaxSATComparableConstraintEncoder.java | 26 +++++ 10 files changed, 320 insertions(+), 7 deletions(-) create mode 100644 src/checkers/inference/model/ComparableVariableSlot.java diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index ad01eef4c..92e8aca8e 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -25,6 +25,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -94,6 +95,14 @@ public class DefaultSlotManager implements SlotManager { * {@link ArithmeticVariableSlot}. */ private final Map arithmeticSlotCache; + + /** + * A map of {@link AnnotationLocation} to {@link Integer} for caching + * {@link ComparableVariableSlot}s. The annotation location uniquely identifies an + * {@link ComparableVariableSlot}. The {@link Integer} is the Id of the corresponding + * {@link ComparableVariableSlot}. + */ + private final Map comparableSlotCache; private final Set> realQualifiers; private final ProcessingEnvironment processingEnvironment; @@ -117,6 +126,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment, combSlotPairCache = new LinkedHashMap<>(); lubSlotPairCache = new LinkedHashMap<>(); arithmeticSlotCache = new LinkedHashMap<>(); + comparableSlotCache = new LinkedHashMap<>(); if (storeConstants) { Set mirrors = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy().getTypeQualifiers(); @@ -395,6 +405,37 @@ public ExistentialVariableSlot createExistentialVariableSlot(VariableSlot potent } return existentialVariableSlot; } + + @Override + public ComparableVariableSlot createComparableVariableSlot(AnnotationLocation location) { + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "Cannot create an ComparableVariableSlot with a missing annotation location."); + } + + // create the arithmetic var slot if it doesn't exist for the given location + if (!comparableSlotCache.containsKey(location)) { + ComparableVariableSlot slot = new ComparableVariableSlot(location, nextId()); + addToVariables(slot); + comparableSlotCache.put(location, slot.getId()); + return slot; + } + + return getComparableVariableSlot(location); + } + + @Override + public ComparableVariableSlot getComparableVariableSlot(AnnotationLocation location) { + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "ComparableVariableSlot are never created with a missing annotation location."); + } + if (!comparableSlotCache.containsKey(location)) { + return null; + } else { + return (ComparableVariableSlot) getVariable(comparableSlotCache.get(location)); + } + } @Override public ArithmeticVariableSlot createArithmeticVariableSlot(AnnotationLocation location) { diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 8a10e81ab..cda1bf55d 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -10,6 +10,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -141,6 +142,29 @@ public interface SlotManager { * @return the ArithmeticVariableSlot for the given location, or null if none exists */ ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation location); + + /** + * Create new ComparableVariableSlot at the given location and return a reference to it if no + * ComparableVariableSlots exists for the location. Otherwise, returns the existing + * ComparableVariableSlot. + * + * @param location an AnnotationLocation used to locate this variable in code + * @return the ComparableVariableSlot for the given location + */ + ComparableVariableSlot createComparableVariableSlot(AnnotationLocation location); + + /** + * Retrieves the ComparableVariableSlot created for the given location if it has been previously + * created, otherwise null is returned. + * + * This method allows faster retrieval of already created ComparableVariableSlot during + * traversals of binary trees in an InferenceVisitor subclass, which does not have direct access + * to the ATM containing this slot. + * + * @param location an AnnotationLocation used to locate this variable in code + * @return the ComparableVariableSlot for the given location, or null if none exists + */ + ComparableVariableSlot getComparableVariableSlot(AnnotationLocation location); /** * Create a VarAnnot equivalent to the given realQualifier. diff --git a/src/checkers/inference/model/ArithmeticConstraint.java b/src/checkers/inference/model/ArithmeticConstraint.java index b4e608478..5907d044a 100644 --- a/src/checkers/inference/model/ArithmeticConstraint.java +++ b/src/checkers/inference/model/ArithmeticConstraint.java @@ -18,7 +18,13 @@ public enum ArithmeticOperationKind { MINUS("-"), MULTIPLY("*"), DIVIDE("/"), - REMAINDER("%"); + REMAINDER("%"), + LEFT_SHIFT("<<"), + RIGHT_SHIFT(">>"), + UNSIGNED_RIGHT_SHIFT(">>>"), + AND("&"), + OR("|"), + XOR("^"); // stores the symbol of the operation private final String opSymbol; @@ -39,6 +45,18 @@ public static ArithmeticOperationKind fromTreeKind(Kind kind) { return DIVIDE; case REMAINDER: return REMAINDER; + case LEFT_SHIFT: + return LEFT_SHIFT; + case RIGHT_SHIFT: + return RIGHT_SHIFT; + case UNSIGNED_RIGHT_SHIFT: + return UNSIGNED_RIGHT_SHIFT; + case AND: + return AND; + case OR: + return OR; + case XOR: + return XOR; default: throw new BugInCF("There are no defined ArithmeticOperationKinds " + "for the given com.sun.source.tree.Tree.Kind: " + kind); diff --git a/src/checkers/inference/model/ComparableConstraint.java b/src/checkers/inference/model/ComparableConstraint.java index a756e7a85..5f4a04c39 100644 --- a/src/checkers/inference/model/ComparableConstraint.java +++ b/src/checkers/inference/model/ComparableConstraint.java @@ -5,25 +5,93 @@ import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.BugInCF; +import com.sun.source.tree.Tree.Kind; + +import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; + /** * Represents a constraint that two slots must be comparable. * */ public class ComparableConstraint extends Constraint implements BinaryConstraint { + private final ComparableOperationKind operation; private final Slot first; private final Slot second; + private final ComparableVariableSlot result; + + public enum ComparableOperationKind { + EQUAL_TO("=="), + NOT_EQUAL_TO("!="), + GREATER_THAN(">"), + GREATER_THAN_EQUAL(">="), + LESS_THAN("<"), + LESS_THAN_EQUAL("<="); + + // stores the symbol of the operation + private final String opSymbol; + + private ComparableOperationKind(String opSymbol) { + this.opSymbol = opSymbol; + } + + public static ComparableOperationKind fromTreeKind(Kind kind) { + switch (kind) { + case EQUAL_TO: + return EQUAL_TO; + case NOT_EQUAL_TO: + return NOT_EQUAL_TO; + case GREATER_THAN: + return GREATER_THAN; + case GREATER_THAN_EQUAL: + return GREATER_THAN_EQUAL; + case LESS_THAN: + return LESS_THAN; + case LESS_THAN_EQUAL: + return LESS_THAN_EQUAL; + default: + throw new BugInCF("There are no defined ComparableOperationKind " + + "for the given com.sun.source.tree.Tree.Kind: " + kind); + } + } + public String getSymbol() { + return opSymbol; + } + } + private ComparableConstraint(Slot first, Slot second, AnnotationLocation location) { super(Arrays.asList(first, second), location); this.first = first; this.second = second; + this.operation = null; + this.result = null; } - + private ComparableConstraint(Slot first, Slot second) { super(Arrays.asList(first, second)); this.first = first; this.second = second; + this.operation = null; + this.result = null; + } + + private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, + ComparableVariableSlot result, AnnotationLocation location) { + super(Arrays.asList(first, second), location); + this.first = first; + this.second = second; + this.operation = operation; + this.result = result; + } + + private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, + ComparableVariableSlot result) { + super(Arrays.asList(first, second)); + this.first = first; + this.second = second; + this.operation = operation; + this.result = result; } protected static Constraint create(Slot first, Slot second, AnnotationLocation location, @@ -57,12 +125,32 @@ protected static Constraint create(Slot first, Slot second, AnnotationLocation l // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT return new ComparableConstraint(first, second, location); } + + protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, + ComparableVariableSlot result, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { + if (operation == null || first == null || second == null || result == null) { + throw new BugInCF("Create comparable constraint with null argument. " + + "Operation: " + operation + " Subtype: " + + first + " Supertype: " + second + " Result: " + result); + } + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "Cannot create an ArithmeticConstraint with a missing annotation location."); + } + + // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT + return new ComparableConstraint(operation, first, second, result, location); + } @Override public T serialize(Serializer serializer) { return serializer.serialize(this); } + public ComparableOperationKind getOperation() { + return operation; + } + @Override public Slot getFirst() { return first; @@ -73,6 +161,10 @@ public Slot getSecond() { return second; } + public ComparableVariableSlot getResult() { + return result; + } + @Override public Constraint make(Slot first, Slot second) { return new ComparableConstraint(first, second); @@ -80,10 +172,12 @@ public Constraint make(Slot first, Slot second) { @Override public int hashCode() { - int result = 1; - result = result + ((first == null) ? 0 : first.hashCode()); - result = result + ((second == null) ? 0 : second.hashCode()); - return result; + int code = 1; + code = code + ((first == null) ? 0 : first.hashCode()); + code = code + ((second == null) ? 0 : second.hashCode()); + code = code + ((operation == null) ? 0 : operation.hashCode()); + code = code + ((result == null) ? 0 : result.hashCode()); + return code; } @Override diff --git a/src/checkers/inference/model/ComparableVariableSlot.java b/src/checkers/inference/model/ComparableVariableSlot.java new file mode 100644 index 000000000..859f5fb95 --- /dev/null +++ b/src/checkers/inference/model/ComparableVariableSlot.java @@ -0,0 +1,36 @@ +package checkers.inference.model; + +import checkers.inference.model.Slot.Kind; + +/** + * ComparableVariableSlot represent the result of an comparable operation between two other + * {@link VariableSlot}s. Note that this slot is serialized identically to a {@link VariableSlot}. + */ +public class ComparableVariableSlot extends VariableSlot { + + public ComparableVariableSlot(AnnotationLocation location, int id) { + super(location, id); + // TODO Auto-generated constructor stub + } + + @Override + public Kind getKind() { + return Kind.COMPARABLE_VARIABLE; + } + + @Override + public S serialize(Serializer serializer) { + return serializer.serialize(this); + } + + /** + * ComparableVariables should never be re-inserted into the source code. + * + * @return false + */ + @Override + public boolean isInsertable() { + return false; + } + +} diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index aa54a2257..1c3c4f04f 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -11,6 +11,7 @@ import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.VariableAnnotator; import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; /** * Constraint manager holds constraints that are generated by InferenceVisitor. @@ -118,6 +119,15 @@ public Constraint createInequalityConstraint(Slot first, Slot second) { public Constraint createComparableConstraint(Slot first, Slot second) { return ComparableConstraint.create(first, second, getCurrentLocation(), realQualHierarchy); } + + /** + * Creates a {@link ComparableConstraint} between the two slots, which may be normalized to + * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. + */ + public Constraint createComparableConstraint(ComparableOperationKind operation, Slot first, + Slot second, ComparableVariableSlot result) { + return ComparableConstraint.create(operation, first, second, result, getCurrentLocation(), realQualHierarchy); + } /** * Creates a {@link CombineConstraint} between the three slots. @@ -249,6 +259,14 @@ public void addComparableConstraint(Slot first, Slot second) { add(constraint); } } + + /** + * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set. + */ + public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, + ComparableVariableSlot result) { + add(createComparableConstraint(operation, first, second, result)); + } /** * Creates and adds a {@link CombineConstraint} to the constraint set. diff --git a/src/checkers/inference/model/Slot.java b/src/checkers/inference/model/Slot.java index 9a368ddae..de038b974 100644 --- a/src/checkers/inference/model/Slot.java +++ b/src/checkers/inference/model/Slot.java @@ -50,6 +50,7 @@ public enum Kind { EXISTENTIAL_VARIABLE, COMB_VARIABLE, ARITHMETIC_VARIABLE, + COMPARABLE_VARIABLE, LUB_VARIABLE } diff --git a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java index 4efb41b05..9c6ebe7c7 100644 --- a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java @@ -1,5 +1,9 @@ package checkers.inference.solver.backend.encoder.binary; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; +import checkers.inference.model.ComparableVariableSlot; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; /** @@ -11,4 +15,15 @@ * @see AbstractConstraintEncoderFactory#createComparableConstraintEncoder() */ public interface ComparableConstraintEncoder extends BinaryConstraintEncoder { + ConstraintEncodingT encodeVariable_Variable(ComparableOperationKind operation, + VariableSlot fst, VariableSlot snd, ComparableVariableSlot result); + + ConstraintEncodingT encodeVariable_Constant(ComparableOperationKind operation, + VariableSlot fst, ConstantSlot snd, ComparableVariableSlot result); + + ConstraintEncodingT encodeConstant_Variable(ComparableOperationKind operation, + ConstantSlot fst, VariableSlot snd, ComparableVariableSlot result); + + ConstraintEncodingT encodeConstant_Constant(ComparableOperationKind operation, + ConstantSlot fst, ConstantSlot snd, ComparableVariableSlot result); } diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 68a127f22..0cab2e93f 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -1,5 +1,7 @@ package checkers.inference.solver.backend.logiql.encoder; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; +import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; @@ -28,8 +30,46 @@ public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); - String logiQLData = "+equalityConstraintContainsConstant(c, v), +constant(c), +hasconstantName[c] = \"" + String logiQLData = "+comparableConstraint(c, v), +constant(c), +hasconstantName[c] = \"" + constantName + "\", +variable(v), +hasvariableName[v] = " + variableId + ".\n"; return logiQLData; } + + @Override + public String encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd, + ComparableVariableSlot result) { + String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; + return logiQLData; + } + + @Override + public String encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd, + ComparableVariableSlot result) { + String constantName = NameUtils.getSimpleName(snd.getValue()); + int variableId = fst.getId(); + String logiQLData = "+comparableConstraint(v, c), +variable(v), +hasvariableName[v] = \"" + + variableId + "\", +constant(c), +hasconstantName[c] = " + constantName + ".\n"; + return logiQLData; + } + + @Override + public String encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd, + ComparableVariableSlot result) { + String constantName = NameUtils.getSimpleName(fst.getValue()); + int variableId = snd.getId(); + String logiQLData = "+comparableConstraint(c, v), +constant(c), +hasconstantName[c] = \"" + + constantName + "\", +variable(v), +hasvariableName[v] = " + variableId + ".\n"; + return logiQLData; + } + + @Override + public String encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd, + ComparableVariableSlot result) { + String constantNamefst = NameUtils.getSimpleName(fst.getValue()); + String constantNamesnd = NameUtils.getSimpleName(snd.getValue()); + String logiQLData = "+comparableConstraint(c1, c2), +constant(c1), +hasconstantName[c1] = \"" + + constantNamefst + "\", +constant(c2), +hasconstantName[c2] = " + constantNamesnd + ".\n"; + return logiQLData; + } } diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index a9cb02d9a..dff2c273e 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -1,5 +1,7 @@ package checkers.inference.solver.backend.maxsat.encoder; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; +import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; @@ -59,4 +61,28 @@ public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encodeVariable_Constant(snd, fst); } + + @Override + public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd, + ComparableVariableSlot result) { + return encodeVariable_Variable(fst, snd); + } + + @Override + public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd, + ComparableVariableSlot result) { + return encodeVariable_Constant(fst, snd); + } + + @Override + public VecInt[] encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd, + ComparableVariableSlot result) { + return encodeConstant_Variable(fst, snd); + } + + @Override + public VecInt[] encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd, + ComparableVariableSlot result) { + return null; + } } From 32777f46dd7e4a408516ba9437d9e3db9f1dc814 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Fri, 1 Nov 2019 12:09:56 -0400 Subject: [PATCH 02/24] removed comparable slot --- .../inference/DefaultSlotManager.java | 32 ----------------- src/checkers/inference/SlotManager.java | 24 ------------- .../inference/model/ComparableConstraint.java | 27 ++++---------- .../model/ComparableVariableSlot.java | 36 ------------------- .../inference/model/ConstraintManager.java | 9 +++-- .../binary/ComparableConstraintEncoder.java | 9 +++-- .../LogiQLComparableConstraintEncoder.java | 13 +++---- .../MaxSATComparableConstraintEncoder.java | 13 +++---- 8 files changed, 22 insertions(+), 141 deletions(-) delete mode 100644 src/checkers/inference/model/ComparableVariableSlot.java diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 92e8aca8e..59ed4a607 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -25,7 +25,6 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; -import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -405,37 +404,6 @@ public ExistentialVariableSlot createExistentialVariableSlot(VariableSlot potent } return existentialVariableSlot; } - - @Override - public ComparableVariableSlot createComparableVariableSlot(AnnotationLocation location) { - if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { - throw new BugInCF( - "Cannot create an ComparableVariableSlot with a missing annotation location."); - } - - // create the arithmetic var slot if it doesn't exist for the given location - if (!comparableSlotCache.containsKey(location)) { - ComparableVariableSlot slot = new ComparableVariableSlot(location, nextId()); - addToVariables(slot); - comparableSlotCache.put(location, slot.getId()); - return slot; - } - - return getComparableVariableSlot(location); - } - - @Override - public ComparableVariableSlot getComparableVariableSlot(AnnotationLocation location) { - if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { - throw new BugInCF( - "ComparableVariableSlot are never created with a missing annotation location."); - } - if (!comparableSlotCache.containsKey(location)) { - return null; - } else { - return (ComparableVariableSlot) getVariable(comparableSlotCache.get(location)); - } - } @Override public ArithmeticVariableSlot createArithmeticVariableSlot(AnnotationLocation location) { diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index cda1bf55d..8a10e81ab 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -10,7 +10,6 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; -import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -142,29 +141,6 @@ public interface SlotManager { * @return the ArithmeticVariableSlot for the given location, or null if none exists */ ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation location); - - /** - * Create new ComparableVariableSlot at the given location and return a reference to it if no - * ComparableVariableSlots exists for the location. Otherwise, returns the existing - * ComparableVariableSlot. - * - * @param location an AnnotationLocation used to locate this variable in code - * @return the ComparableVariableSlot for the given location - */ - ComparableVariableSlot createComparableVariableSlot(AnnotationLocation location); - - /** - * Retrieves the ComparableVariableSlot created for the given location if it has been previously - * created, otherwise null is returned. - * - * This method allows faster retrieval of already created ComparableVariableSlot during - * traversals of binary trees in an InferenceVisitor subclass, which does not have direct access - * to the ATM containing this slot. - * - * @param location an AnnotationLocation used to locate this variable in code - * @return the ComparableVariableSlot for the given location, or null if none exists - */ - ComparableVariableSlot getComparableVariableSlot(AnnotationLocation location); /** * Create a VarAnnot equivalent to the given realQualifier. diff --git a/src/checkers/inference/model/ComparableConstraint.java b/src/checkers/inference/model/ComparableConstraint.java index 5f4a04c39..a3d36a16e 100644 --- a/src/checkers/inference/model/ComparableConstraint.java +++ b/src/checkers/inference/model/ComparableConstraint.java @@ -7,8 +7,6 @@ import com.sun.source.tree.Tree.Kind; -import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; - /** * Represents a constraint that two slots must be comparable. * @@ -18,7 +16,6 @@ public class ComparableConstraint extends Constraint implements BinaryConstraint private final ComparableOperationKind operation; private final Slot first; private final Slot second; - private final ComparableVariableSlot result; public enum ComparableOperationKind { EQUAL_TO("=="), @@ -65,7 +62,6 @@ private ComparableConstraint(Slot first, Slot second, AnnotationLocation locatio this.first = first; this.second = second; this.operation = null; - this.result = null; } private ComparableConstraint(Slot first, Slot second) { @@ -73,25 +69,20 @@ private ComparableConstraint(Slot first, Slot second) { this.first = first; this.second = second; this.operation = null; - this.result = null; } - private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, - ComparableVariableSlot result, AnnotationLocation location) { + private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, AnnotationLocation location) { super(Arrays.asList(first, second), location); this.first = first; this.second = second; this.operation = operation; - this.result = result; } - private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, - ComparableVariableSlot result) { + private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { super(Arrays.asList(first, second)); this.first = first; this.second = second; this.operation = operation; - this.result = result; } protected static Constraint create(Slot first, Slot second, AnnotationLocation location, @@ -126,12 +117,11 @@ protected static Constraint create(Slot first, Slot second, AnnotationLocation l return new ComparableConstraint(first, second, location); } - protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, - ComparableVariableSlot result, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { - if (operation == null || first == null || second == null || result == null) { + protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { + if (operation == null || first == null || second == null) { throw new BugInCF("Create comparable constraint with null argument. " + "Operation: " + operation + " Subtype: " - + first + " Supertype: " + second + " Result: " + result); + + first + " Supertype: " + second); } if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { throw new BugInCF( @@ -139,7 +129,7 @@ protected static Constraint create(ComparableOperationKind operation, Slot first } // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT - return new ComparableConstraint(operation, first, second, result, location); + return new ComparableConstraint(operation, first, second, location); } @Override @@ -161,10 +151,6 @@ public Slot getSecond() { return second; } - public ComparableVariableSlot getResult() { - return result; - } - @Override public Constraint make(Slot first, Slot second) { return new ComparableConstraint(first, second); @@ -176,7 +162,6 @@ public int hashCode() { code = code + ((first == null) ? 0 : first.hashCode()); code = code + ((second == null) ? 0 : second.hashCode()); code = code + ((operation == null) ? 0 : operation.hashCode()); - code = code + ((result == null) ? 0 : result.hashCode()); return code; } diff --git a/src/checkers/inference/model/ComparableVariableSlot.java b/src/checkers/inference/model/ComparableVariableSlot.java deleted file mode 100644 index 859f5fb95..000000000 --- a/src/checkers/inference/model/ComparableVariableSlot.java +++ /dev/null @@ -1,36 +0,0 @@ -package checkers.inference.model; - -import checkers.inference.model.Slot.Kind; - -/** - * ComparableVariableSlot represent the result of an comparable operation between two other - * {@link VariableSlot}s. Note that this slot is serialized identically to a {@link VariableSlot}. - */ -public class ComparableVariableSlot extends VariableSlot { - - public ComparableVariableSlot(AnnotationLocation location, int id) { - super(location, id); - // TODO Auto-generated constructor stub - } - - @Override - public Kind getKind() { - return Kind.COMPARABLE_VARIABLE; - } - - @Override - public S serialize(Serializer serializer) { - return serializer.serialize(this); - } - - /** - * ComparableVariables should never be re-inserted into the source code. - * - * @return false - */ - @Override - public boolean isInsertable() { - return false; - } - -} diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index 1c3c4f04f..b6699f38b 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -125,8 +125,8 @@ public Constraint createComparableConstraint(Slot first, Slot second) { * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. */ public Constraint createComparableConstraint(ComparableOperationKind operation, Slot first, - Slot second, ComparableVariableSlot result) { - return ComparableConstraint.create(operation, first, second, result, getCurrentLocation(), realQualHierarchy); + Slot second) { + return ComparableConstraint.create(operation, first, second, getCurrentLocation(), realQualHierarchy); } /** @@ -263,9 +263,8 @@ public void addComparableConstraint(Slot first, Slot second) { /** * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set. */ - public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, - ComparableVariableSlot result) { - add(createComparableConstraint(operation, first, second, result)); + public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { + add(createComparableConstraint(operation, first, second)); } /** diff --git a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java index 9c6ebe7c7..e3e3e26ec 100644 --- a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java @@ -1,7 +1,6 @@ package checkers.inference.solver.backend.encoder.binary; import checkers.inference.model.ComparableConstraint.ComparableOperationKind; -import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; @@ -16,14 +15,14 @@ */ public interface ComparableConstraintEncoder extends BinaryConstraintEncoder { ConstraintEncodingT encodeVariable_Variable(ComparableOperationKind operation, - VariableSlot fst, VariableSlot snd, ComparableVariableSlot result); + VariableSlot fst, VariableSlot snd); ConstraintEncodingT encodeVariable_Constant(ComparableOperationKind operation, - VariableSlot fst, ConstantSlot snd, ComparableVariableSlot result); + VariableSlot fst, ConstantSlot snd); ConstraintEncodingT encodeConstant_Variable(ComparableOperationKind operation, - ConstantSlot fst, VariableSlot snd, ComparableVariableSlot result); + ConstantSlot fst, VariableSlot snd); ConstraintEncodingT encodeConstant_Constant(ComparableOperationKind operation, - ConstantSlot fst, ConstantSlot snd, ComparableVariableSlot result); + ConstantSlot fst, ConstantSlot snd); } diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 0cab2e93f..8920e20a9 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -1,7 +1,6 @@ package checkers.inference.solver.backend.logiql.encoder; import checkers.inference.model.ComparableConstraint.ComparableOperationKind; -import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; @@ -36,16 +35,14 @@ public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { } @Override - public String encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd, - ComparableVariableSlot result) { + public String encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; return logiQLData; } @Override - public String encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd, - ComparableVariableSlot result) { + public String encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { String constantName = NameUtils.getSimpleName(snd.getValue()); int variableId = fst.getId(); String logiQLData = "+comparableConstraint(v, c), +variable(v), +hasvariableName[v] = \"" @@ -54,8 +51,7 @@ public String encodeVariable_Constant(ComparableOperationKind operation, Variabl } @Override - public String encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd, - ComparableVariableSlot result) { + public String encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); String logiQLData = "+comparableConstraint(c, v), +constant(c), +hasconstantName[c] = \"" @@ -64,8 +60,7 @@ public String encodeConstant_Variable(ComparableOperationKind operation, Constan } @Override - public String encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd, - ComparableVariableSlot result) { + public String encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd) { String constantNamefst = NameUtils.getSimpleName(fst.getValue()); String constantNamesnd = NameUtils.getSimpleName(snd.getValue()); String logiQLData = "+comparableConstraint(c1, c2), +constant(c1), +hasconstantName[c1] = \"" diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index dff2c273e..a402e9fde 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -1,7 +1,6 @@ package checkers.inference.solver.backend.maxsat.encoder; import checkers.inference.model.ComparableConstraint.ComparableOperationKind; -import checkers.inference.model.ComparableVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; @@ -63,26 +62,22 @@ public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { } @Override - public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd, - ComparableVariableSlot result) { + public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { return encodeVariable_Variable(fst, snd); } @Override - public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd, - ComparableVariableSlot result) { + public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { return encodeVariable_Constant(fst, snd); } @Override - public VecInt[] encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd, - ComparableVariableSlot result) { + public VecInt[] encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { return encodeConstant_Variable(fst, snd); } @Override - public VecInt[] encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd, - ComparableVariableSlot result) { + public VecInt[] encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd) { return null; } } From 6c475a981990e96c1ea174de915a2964fef8ec87 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Thu, 7 Nov 2019 14:53:06 -0500 Subject: [PATCH 03/24] remove unused code comparable slot cache --- src/checkers/inference/DefaultSlotManager.java | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 59ed4a607..ad01eef4c 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -94,14 +94,6 @@ public class DefaultSlotManager implements SlotManager { * {@link ArithmeticVariableSlot}. */ private final Map arithmeticSlotCache; - - /** - * A map of {@link AnnotationLocation} to {@link Integer} for caching - * {@link ComparableVariableSlot}s. The annotation location uniquely identifies an - * {@link ComparableVariableSlot}. The {@link Integer} is the Id of the corresponding - * {@link ComparableVariableSlot}. - */ - private final Map comparableSlotCache; private final Set> realQualifiers; private final ProcessingEnvironment processingEnvironment; @@ -125,7 +117,6 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment, combSlotPairCache = new LinkedHashMap<>(); lubSlotPairCache = new LinkedHashMap<>(); arithmeticSlotCache = new LinkedHashMap<>(); - comparableSlotCache = new LinkedHashMap<>(); if (storeConstants) { Set mirrors = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy().getTypeQualifiers(); From 3f4a4a0ddddca729ca6a605def94c63559a0825f Mon Sep 17 00:00:00 2001 From: txiang61 Date: Fri, 15 Nov 2019 17:29:07 -0500 Subject: [PATCH 04/24] added comparable operation kind ANY and clean up code --- .../inference/model/ComparableConstraint.java | 55 +++++-------------- .../inference/model/ConstraintManager.java | 18 +++--- 2 files changed, 24 insertions(+), 49 deletions(-) diff --git a/src/checkers/inference/model/ComparableConstraint.java b/src/checkers/inference/model/ComparableConstraint.java index a3d36a16e..3a1a7b33c 100644 --- a/src/checkers/inference/model/ComparableConstraint.java +++ b/src/checkers/inference/model/ComparableConstraint.java @@ -18,6 +18,7 @@ public class ComparableConstraint extends Constraint implements BinaryConstraint private final Slot second; public enum ComparableOperationKind { + ANY(""), EQUAL_TO("=="), NOT_EQUAL_TO("!="), GREATER_THAN(">"), @@ -56,22 +57,9 @@ public String getSymbol() { return opSymbol; } } - - private ComparableConstraint(Slot first, Slot second, AnnotationLocation location) { - super(Arrays.asList(first, second), location); - this.first = first; - this.second = second; - this.operation = null; - } - - private ComparableConstraint(Slot first, Slot second) { - super(Arrays.asList(first, second)); - this.first = first; - this.second = second; - this.operation = null; - } - private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, AnnotationLocation location) { + private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, + AnnotationLocation location) { super(Arrays.asList(first, second), location); this.first = first; this.second = second; @@ -84,11 +72,12 @@ private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot this.second = second; this.operation = operation; } - - protected static Constraint create(Slot first, Slot second, AnnotationLocation location, - QualifierHierarchy realQualHierarchy) { - if (first == null || second == null) { - throw new BugInCF("Create comparable constraint with null argument. Subtype: " + + protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, + AnnotationLocation location, QualifierHierarchy realQualHierarchy) { + if (operation == null || first == null || second == null) { + throw new BugInCF("Create comparable constraint with null argument. " + + "Operation: " + operation + " Subtype: " + first + " Supertype: " + second); } @@ -98,7 +87,8 @@ protected static Constraint create(Slot first, Slot second, AnnotationLocation l // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT // C1 <~> C2 => TRUE/FALSE depending on relationship - if (first instanceof ConstantSlot && second instanceof ConstantSlot) { + if (first instanceof ConstantSlot && second instanceof ConstantSlot + && operation == ComparableOperationKind.ANY) { ConstantSlot firstConst = (ConstantSlot) first; ConstantSlot secondConst = (ConstantSlot) second; @@ -107,27 +97,12 @@ protected static Constraint create(Slot first, Slot second, AnnotationLocation l ? AlwaysTrueConstraint.create() : AlwaysFalseConstraint.create(); } - + // V <~> V => TRUE (every type is always comparable to itself) if (first == second) { return AlwaysTrueConstraint.create(); } - // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT - return new ComparableConstraint(first, second, location); - } - - protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { - if (operation == null || first == null || second == null) { - throw new BugInCF("Create comparable constraint with null argument. " - + "Operation: " + operation + " Subtype: " - + first + " Supertype: " + second); - } - if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { - throw new BugInCF( - "Cannot create an ArithmeticConstraint with a missing annotation location."); - } - // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT return new ComparableConstraint(operation, first, second, location); } @@ -153,7 +128,7 @@ public Slot getSecond() { @Override public Constraint make(Slot first, Slot second) { - return new ComparableConstraint(first, second); + return new ComparableConstraint(ComparableOperationKind.ANY, first, second); } @Override @@ -174,8 +149,8 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; ComparableConstraint other = (ComparableConstraint) obj; - if ((first.equals(other.first) && second.equals(other.second)) - || (first.equals(other.second) && (second.equals(other.first)))) { + if (first.equals(other.first) && second.equals(other.second) + && operation.equals(other.operation)) { return true; } else { return false; diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index b6699f38b..e262f5395 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -117,7 +117,7 @@ public Constraint createInequalityConstraint(Slot first, Slot second) { * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. */ public Constraint createComparableConstraint(Slot first, Slot second) { - return ComparableConstraint.create(first, second, getCurrentLocation(), realQualHierarchy); + return createComparableConstraint(ComparableOperationKind.ANY, first, second); } /** @@ -251,20 +251,20 @@ public void addInequalityConstraint(Slot first, Slot second) { * {@link ComparableConstraint} is always unsatisfiable. */ public void addComparableConstraint(Slot first, Slot second) { - Constraint constraint = createComparableConstraint(first, second); - if (constraint instanceof AlwaysFalseConstraint) { - checker.report(Result.failure("comparable.constraint.unsatisfiable", first, second), - visitorState.getPath().getLeaf()); - } else { - add(constraint); - } + addComparableConstraint(ComparableOperationKind.ANY, first, second); } /** * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set. */ public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { - add(createComparableConstraint(operation, first, second)); + Constraint constraint = createComparableConstraint(operation, first, second); + if (constraint instanceof AlwaysFalseConstraint) { + checker.report(Result.failure("comparable.constraint.unsatisfiable", first, second), + visitorState.getPath().getLeaf()); + } else { + add(constraint); + } } /** From 97e7261e5d6f3c476004fdeba36432fcf1cb79ff Mon Sep 17 00:00:00 2001 From: txiang61 Date: Thu, 21 Nov 2019 17:30:54 -0500 Subject: [PATCH 05/24] Change comparable constraint structure and rename operators --- src/checkers/inference/InferenceVisitor.java | 5 +- .../inference/model/ComparableConstraint.java | 77 +++++++++---------- .../inference/model/ConstraintManager.java | 21 +---- .../model/serialization/JsonDeserializer.java | 9 ++- .../model/serialization/JsonSerializer.java | 6 +- .../serialization/ToStringSerializer.java | 4 +- .../backend/AbstractFormatTranslator.java | 2 +- .../ComparableConstraintEncoder.java | 14 ++-- .../encoder/ConstraintEncoderCoordinator.java | 25 ++++++ .../encoder/ConstraintEncoderFactory.java | 1 - .../LogiQLComparableConstraintEncoder.java | 23 +----- .../LogiQLConstraintEncoderFactory.java | 2 +- .../MaxSATComparableConstraintEncoder.java | 33 +++----- .../Z3BitVectorConstraintEncoderFactory.java | 2 +- .../inference/solver/util/PrintUtils.java | 4 +- 15 files changed, 102 insertions(+), 126 deletions(-) rename src/checkers/inference/solver/backend/encoder/{binary => }/ComparableConstraintEncoder.java (72%) diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index e76cd9468..217470af2 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/src/checkers/inference/InferenceVisitor.java @@ -31,6 +31,7 @@ import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.RefinementVariableSlot; @@ -39,6 +40,7 @@ import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceUtil; +import com.sun.source.tree.BinaryTree; import com.sun.source.tree.CatchTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodTree; @@ -330,7 +332,8 @@ public void areComparable(AnnotatedTypeMirror ty1, AnnotatedTypeMirror ty2, Stri } else { if (!InferenceMain.getInstance().isPerformingFlow()) { logger.fine("InferenceVisitor::areComparable: Comparable constraint constructor invocation."); - InferenceMain.getInstance().getConstraintManager().addComparableConstraint(el1, el2); + ComparableOperationKind opKind = ComparableOperationKind.fromTreeKind(node.getKind()); + InferenceMain.getInstance().getConstraintManager().addComparableConstraint(opKind, el1, el2); } } } else { diff --git a/src/checkers/inference/model/ComparableConstraint.java b/src/checkers/inference/model/ComparableConstraint.java index 3a1a7b33c..e2c732f43 100644 --- a/src/checkers/inference/model/ComparableConstraint.java +++ b/src/checkers/inference/model/ComparableConstraint.java @@ -11,20 +11,21 @@ * Represents a constraint that two slots must be comparable. * */ -public class ComparableConstraint extends Constraint implements BinaryConstraint { +public class ComparableConstraint extends Constraint { private final ComparableOperationKind operation; - private final Slot first; - private final Slot second; + private final Slot left; + private final Slot right; public enum ComparableOperationKind { - ANY(""), + REFERENCE(""), EQUAL_TO("=="), NOT_EQUAL_TO("!="), GREATER_THAN(">"), GREATER_THAN_EQUAL(">="), LESS_THAN("<"), - LESS_THAN_EQUAL("<="); + LESS_THAN_EQUAL("<="), + OTHER("?"); // stores the symbol of the operation private final String opSymbol; @@ -47,9 +48,12 @@ public static ComparableOperationKind fromTreeKind(Kind kind) { return LESS_THAN; case LESS_THAN_EQUAL: return LESS_THAN_EQUAL; + case INSTANCE_OF: + case TYPE_CAST: + return REFERENCE; default: - throw new BugInCF("There are no defined ComparableOperationKind " - + "for the given com.sun.source.tree.Tree.Kind: " + kind); + // TODO: Handle all cases and throw error on unsupported operations + return OTHER; } } @@ -58,27 +62,27 @@ public String getSymbol() { } } - private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second, + private ComparableConstraint(ComparableOperationKind operation, Slot left, Slot right, AnnotationLocation location) { - super(Arrays.asList(first, second), location); - this.first = first; - this.second = second; + super(Arrays.asList(left, right), location); + this.left = left; + this.right = right; this.operation = operation; } - private ComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { - super(Arrays.asList(first, second)); - this.first = first; - this.second = second; + private ComparableConstraint(ComparableOperationKind operation, Slot left, Slot right) { + super(Arrays.asList(left, right)); + this.left = left; + this.right = right; this.operation = operation; } - protected static Constraint create(ComparableOperationKind operation, Slot first, Slot second, + protected static Constraint create(ComparableOperationKind operation, Slot left, Slot right, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { - if (operation == null || first == null || second == null) { + if (operation == null || left == null || right == null) { throw new BugInCF("Create comparable constraint with null argument. " + "Operation: " + operation + " Subtype: " - + first + " Supertype: " + second); + + left + " Supertype: " + right); } // Normalization cases: @@ -87,24 +91,24 @@ protected static Constraint create(ComparableOperationKind operation, Slot first // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT // C1 <~> C2 => TRUE/FALSE depending on relationship - if (first instanceof ConstantSlot && second instanceof ConstantSlot - && operation == ComparableOperationKind.ANY) { - ConstantSlot firstConst = (ConstantSlot) first; - ConstantSlot secondConst = (ConstantSlot) second; + if (left instanceof ConstantSlot && right instanceof ConstantSlot + && operation == ComparableOperationKind.REFERENCE) { + ConstantSlot leftConst = (ConstantSlot) left; + ConstantSlot rightConst = (ConstantSlot) right; - return realQualHierarchy.isSubtype(firstConst.getValue(), secondConst.getValue()) - || realQualHierarchy.isSubtype(secondConst.getValue(), firstConst.getValue()) + return realQualHierarchy.isSubtype(leftConst.getValue(), rightConst.getValue()) + || realQualHierarchy.isSubtype(rightConst.getValue(), leftConst.getValue()) ? AlwaysTrueConstraint.create() : AlwaysFalseConstraint.create(); } // V <~> V => TRUE (every type is always comparable to itself) - if (first == second) { + if (left == right) { return AlwaysTrueConstraint.create(); } // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT - return new ComparableConstraint(operation, first, second, location); + return new ComparableConstraint(operation, left, right, location); } @Override @@ -116,26 +120,19 @@ public ComparableOperationKind getOperation() { return operation; } - @Override - public Slot getFirst() { - return first; + public Slot getLeft() { + return left; } - @Override - public Slot getSecond() { - return second; - } - - @Override - public Constraint make(Slot first, Slot second) { - return new ComparableConstraint(ComparableOperationKind.ANY, first, second); + public Slot getRight() { + return right; } @Override public int hashCode() { int code = 1; - code = code + ((first == null) ? 0 : first.hashCode()); - code = code + ((second == null) ? 0 : second.hashCode()); + code = code + ((left == null) ? 0 : left.hashCode()); + code = code + ((right == null) ? 0 : right.hashCode()); code = code + ((operation == null) ? 0 : operation.hashCode()); return code; } @@ -149,7 +146,7 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; ComparableConstraint other = (ComparableConstraint) obj; - if (first.equals(other.first) && second.equals(other.second) + if (left.equals(other.left) && right.equals(other.right) && operation.equals(other.operation)) { return true; } else { diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index e262f5395..f9b94735e 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -112,14 +112,6 @@ public Constraint createInequalityConstraint(Slot first, Slot second) { return InequalityConstraint.create(first, second, getCurrentLocation()); } - /** - * Creates a {@link ComparableConstraint} between the two slots, which may be normalized to - * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. - */ - public Constraint createComparableConstraint(Slot first, Slot second) { - return createComparableConstraint(ComparableOperationKind.ANY, first, second); - } - /** * Creates a {@link ComparableConstraint} between the two slots, which may be normalized to * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. @@ -244,18 +236,11 @@ public void addInequalityConstraint(Slot first, Slot second) { add(constraint); } } - - /** - * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set, - * which may be normalized to {@link AlwaysTrueConstraint}. An error is issued if the - * {@link ComparableConstraint} is always unsatisfiable. - */ - public void addComparableConstraint(Slot first, Slot second) { - addComparableConstraint(ComparableOperationKind.ANY, first, second); - } /** - * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set. + * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set, + * which may be normalized to {@link AlwaysTrueConstraint} if kidn is a reference. + * An error is issued if the {@link ComparableConstraint} is always unsatisfiable. */ public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { Constraint constraint = createComparableConstraint(operation, first, second); diff --git a/src/checkers/inference/model/serialization/JsonDeserializer.java b/src/checkers/inference/model/serialization/JsonDeserializer.java index 639a3aad2..6df6bc71e 100644 --- a/src/checkers/inference/model/serialization/JsonDeserializer.java +++ b/src/checkers/inference/model/serialization/JsonDeserializer.java @@ -17,6 +17,7 @@ import org.json.simple.parser.ParseException; import checkers.inference.InferenceMain; +import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.Constraint; import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; @@ -35,6 +36,8 @@ import static checkers.inference.model.serialization.JsonSerializer.INEQUALITY_CONSTRAINT_KEY; import static checkers.inference.model.serialization.JsonSerializer.INEQUALITY_LHS; import static checkers.inference.model.serialization.JsonSerializer.INEQUALITY_RHS; +import static checkers.inference.model.serialization.JsonSerializer.COMP_LHS; +import static checkers.inference.model.serialization.JsonSerializer.COMP_RHS; import static checkers.inference.model.serialization.JsonSerializer.SUBTYPE_CONSTRAINT_KEY; import static checkers.inference.model.serialization.JsonSerializer.SUBTYPE_SUB_KEY; import static checkers.inference.model.serialization.JsonSerializer.SUBTYPE_SUPER_KEY; @@ -106,9 +109,9 @@ public List jsonArrayToConstraints(final JSONArray jsonConstraints) Slot rhs = parseSlot((String) constraint.get(INEQUALITY_RHS)); results.add(constraintManager.createInequalityConstraint(lhs, rhs)); } else if (COMP_CONSTRAINT_KEY.equals(constraintType)) { - Slot lhs = parseSlot((String) constraint.get(INEQUALITY_LHS)); - Slot rhs = parseSlot((String) constraint.get(INEQUALITY_RHS)); - results.add(constraintManager.createComparableConstraint(lhs, rhs)); + Slot lhs = parseSlot((String) constraint.get(COMP_LHS)); + Slot rhs = parseSlot((String) constraint.get(COMP_RHS)); + results.add(constraintManager.createComparableConstraint(ComparableOperationKind.OTHER, lhs, rhs)); } else if (EXISTENTIAL_CONSTRAINT_KEY.equals(constraintType)) { Slot potential = parseSlot((String) constraint.get(EXISTENTIAL_ID)); List thenConstraints = diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index 485059545..9d0282890 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -300,14 +300,14 @@ public JSONObject serialize(InequalityConstraint constraint) { @SuppressWarnings("unchecked") @Override public JSONObject serialize(ComparableConstraint constraint) { - if (constraint.getFirst() == null || constraint.getSecond() == null) { + if (constraint.getLeft() == null || constraint.getRight() == null) { return null; } JSONObject obj = new JSONObject(); obj.put(CONSTRAINT_KEY, COMP_CONSTRAINT_KEY); - obj.put(COMP_LHS, constraint.getFirst().serialize(this)); - obj.put(COMP_RHS, constraint.getSecond().serialize(this)); + obj.put(COMP_LHS, constraint.getLeft().serialize(this)); + obj.put(COMP_RHS, constraint.getRight().serialize(this)); return obj; } diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 660800fa2..21bef8442 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -199,9 +199,9 @@ public String serialize(ComparableConstraint constraint) { showVerboseVars = false; final StringBuilder sb = new StringBuilder(); sb.append(getCurrentIndentString()) - .append(constraint.getFirst().serialize(this)) + .append(constraint.getLeft().serialize(this)) .append(" <~> ") - .append(constraint.getSecond().serialize(this)); + .append(constraint.getRight().serialize(this)); showVerboseVars = prevShowVerboseVars; return sb.toString(); } diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index b84f82c7f..8f7b312a4 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -16,9 +16,9 @@ import checkers.inference.model.SubtypeConstraint; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.ConstraintEncoderCoordinator; import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; diff --git a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java similarity index 72% rename from src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java rename to src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java index e3e3e26ec..72c401e73 100644 --- a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java @@ -1,9 +1,9 @@ -package checkers.inference.solver.backend.encoder.binary; +package checkers.inference.solver.backend.encoder; import checkers.inference.model.ComparableConstraint.ComparableOperationKind; +import checkers.inference.solver.backend.encoder.binary.BinaryConstraintEncoder; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; /** * A marker interface that all constraint encoders that support encoding {@link checkers.inference.model.ComparableConstraint} @@ -13,16 +13,16 @@ * @see checkers.inference.model.ComparableConstraint * @see AbstractConstraintEncoderFactory#createComparableConstraintEncoder() */ -public interface ComparableConstraintEncoder extends BinaryConstraintEncoder { +public interface ComparableConstraintEncoder { ConstraintEncodingT encodeVariable_Variable(ComparableOperationKind operation, - VariableSlot fst, VariableSlot snd); + VariableSlot left, VariableSlot right); ConstraintEncodingT encodeVariable_Constant(ComparableOperationKind operation, - VariableSlot fst, ConstantSlot snd); + VariableSlot left, ConstantSlot right); ConstraintEncodingT encodeConstant_Variable(ComparableOperationKind operation, - ConstantSlot fst, VariableSlot snd); + ConstantSlot left, VariableSlot right); ConstraintEncodingT encodeConstant_Constant(ComparableOperationKind operation, - ConstantSlot fst, ConstantSlot snd); + ConstantSlot left, ConstantSlot right); } diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java index 5cb031b97..a5c12702e 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java @@ -4,6 +4,7 @@ import checkers.inference.model.ArithmeticConstraint; import checkers.inference.model.BinaryConstraint; import checkers.inference.model.CombineConstraint; +import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ImplicationConstraint; @@ -78,6 +79,30 @@ public static ConstraintEncodingT dispatch(CombineConstrai throw new BugInCF("Unsupported SlotSlotCombo enum."); } } + + public static ConstraintEncodingT dispatch( + ComparableConstraint constraint, + ComparableConstraintEncoder encoder) { + switch (SlotSlotCombo.valueOf(constraint.getLeft(), constraint.getRight())) { + case VARIABLE_VARIABLE: + return encoder.encodeVariable_Variable(constraint.getOperation(), + (VariableSlot) constraint.getLeft(), + (VariableSlot) constraint.getRight()); + case VARIABLE_CONSTANT: + return encoder.encodeVariable_Constant(constraint.getOperation(), + (VariableSlot) constraint.getLeft(), + (ConstantSlot) constraint.getRight()); + case CONSTANT_VARIABLE: + return encoder.encodeConstant_Variable(constraint.getOperation(), + (ConstantSlot) constraint.getLeft(), + (VariableSlot) constraint.getRight()); + case CONSTANT_CONSTANT: + return encoder.encodeConstant_Constant(constraint.getOperation(), + (ConstantSlot) constraint.getLeft(), + (ConstantSlot) constraint.getRight()); + } + return null; + } public static ConstraintEncodingT dispatch( ArithmeticConstraint constraint, diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java index a0c451c34..d3bd1143d 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java @@ -1,6 +1,5 @@ package checkers.inference.solver.backend.encoder; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 8920e20a9..7caf1998f 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -3,7 +3,7 @@ import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,27 +13,6 @@ public LogiQLComparableConstraintEncoder(Lattice lattice) { super(lattice); } - @Override - public String encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { - String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " - + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; - return logiQLData; - } - - @Override - public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { - return encodeConstant_Variable(snd, fst); - } - - @Override - public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { - String constantName = NameUtils.getSimpleName(fst.getValue()); - int variableId = snd.getId(); - String logiQLData = "+comparableConstraint(c, v), +constant(c), +hasconstantName[c] = \"" - + constantName + "\", +variable(v), +hasvariableName[v] = " + variableId + ".\n"; - return logiQLData; - } - @Override public String encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java index adcfe0ed5..4c6c12116 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java @@ -2,7 +2,7 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index a402e9fde..7574298d1 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -3,7 +3,7 @@ import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; import checkers.inference.solver.frontend.Lattice; @@ -20,9 +20,9 @@ public MaxSATComparableConstraintEncoder(Lattice lattice, Map !b which is the same as (!a v !b) & (b v a) + @Override + public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { + // a <=> !b which is the same as (!a v !b) & (b v a) List list = new ArrayList(); for (AnnotationMirror type : lattice.allTypes) { if (lattice.incomparableType.keySet().contains(type)) { @@ -37,11 +37,11 @@ public VecInt[] encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { } VecInt[] result = list.toArray(new VecInt[list.size()]); return result; - } + } - @Override - public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { - if (lattice.incomparableType.keySet().contains(snd.getValue())) { + @Override + public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { + if (lattice.incomparableType.keySet().contains(snd.getValue())) { List resultList = new ArrayList<>(); for (AnnotationMirror incomparable : lattice.incomparableType.get(snd.getValue())) { // Should not be equal to incomparable @@ -54,26 +54,11 @@ public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { } else { return emptyValue; } - } - - @Override - public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { - return encodeVariable_Constant(snd, fst); - } - - @Override - public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { - return encodeVariable_Variable(fst, snd); - } - - @Override - public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { - return encodeVariable_Constant(fst, snd); } @Override public VecInt[] encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { - return encodeConstant_Variable(fst, snd); + return encodeVariable_Constant(operation, snd, fst); } @Override diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java index 3d8c3dc1d..f1d396379 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java @@ -2,7 +2,7 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; -import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index b977b2519..e052c3c3e 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -246,8 +246,8 @@ public Void serialize(InequalityConstraint constraint) { @Override public Void serialize(ComparableConstraint constraint) { - constraint.getFirst().serialize(this); - constraint.getSecond().serialize(this); + constraint.getLeft().serialize(this); + constraint.getRight().serialize(this); return null; } From 905597515c46ef2405e88c9042d5daa6f5689ffd Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Jun 2020 14:21:14 -0400 Subject: [PATCH 06/24] Add comparison constraint instead of modifying comparable constriant and add comparison result --- src/checkers/inference/InferenceVisitor.java | 5 +- .../inference/model/ArithmeticConstraint.java | 6 +- .../inference/model/ComparableConstraint.java | 129 +++++----------- .../inference/model/ComparisonConstraint.java | 140 ++++++++++++++++++ .../model/ComparisonVariableSlot.java | 35 +++++ .../inference/model/ConstraintManager.java | 31 +++- src/checkers/inference/model/Serializer.java | 2 + src/checkers/inference/model/Slot.java | 1 + .../serialization/CnfVecIntSerializer.java | 7 + .../model/serialization/JsonDeserializer.java | 3 +- .../model/serialization/JsonSerializer.java | 27 +++- .../serialization/ToStringSerializer.java | 25 +++- .../backend/AbstractFormatTranslator.java | 15 +- .../encoder/ComparableConstraintEncoder.java | 28 ---- .../encoder/ComparisonConstraintEncoder.java | 28 ++++ .../encoder/ConstraintEncoderCoordinator.java | 14 +- .../encoder/ConstraintEncoderFactory.java | 4 + .../binary/ComparableConstraintEncoder.java | 14 ++ .../LogiQLComparableConstraintEncoder.java | 44 ++---- .../LogiQLConstraintEncoderFactory.java | 8 +- .../MaxSATComparableConstraintEncoder.java | 34 ++--- .../MaxSATConstraintEncoderFactory.java | 7 + .../Z3BitVectorConstraintEncoderFactory.java | 8 +- .../inference/solver/util/PrintUtils.java | 9 ++ 24 files changed, 426 insertions(+), 198 deletions(-) create mode 100644 src/checkers/inference/model/ComparisonConstraint.java create mode 100644 src/checkers/inference/model/ComparisonVariableSlot.java delete mode 100644 src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java create mode 100644 src/checkers/inference/solver/backend/encoder/ComparisonConstraintEncoder.java create mode 100644 src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index bae258f78..1d9b6d17c 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/src/checkers/inference/InferenceVisitor.java @@ -30,7 +30,6 @@ import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.RefinementVariableSlot; @@ -318,7 +317,6 @@ private void annoIsNoneOf(AnnotatedTypeMirror sourceType, AnnotationMirror effec } } - public void areComparable(AnnotatedTypeMirror ty1, AnnotatedTypeMirror ty2, String msgkey, Tree node) { if (infer) { final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); @@ -331,8 +329,7 @@ public void areComparable(AnnotatedTypeMirror ty1, AnnotatedTypeMirror ty2, Stri } else { if (!InferenceMain.getInstance().isPerformingFlow()) { logger.fine("InferenceVisitor::areComparable: Comparable constraint constructor invocation."); - ComparableOperationKind opKind = ComparableOperationKind.fromTreeKind(node.getKind()); - InferenceMain.getInstance().getConstraintManager().addComparableConstraint(opKind, el1, el2); + InferenceMain.getInstance().getConstraintManager().addComparableConstraint(el1, el2); } } } else { diff --git a/src/checkers/inference/model/ArithmeticConstraint.java b/src/checkers/inference/model/ArithmeticConstraint.java index 5907d044a..96fc6e3e5 100644 --- a/src/checkers/inference/model/ArithmeticConstraint.java +++ b/src/checkers/inference/model/ArithmeticConstraint.java @@ -22,9 +22,9 @@ public enum ArithmeticOperationKind { LEFT_SHIFT("<<"), RIGHT_SHIFT(">>"), UNSIGNED_RIGHT_SHIFT(">>>"), - AND("&"), - OR("|"), - XOR("^"); + AND("&"), + OR("|"), + XOR("^"); // stores the symbol of the operation private final String opSymbol; diff --git a/src/checkers/inference/model/ComparableConstraint.java b/src/checkers/inference/model/ComparableConstraint.java index e2c732f43..a756e7a85 100644 --- a/src/checkers/inference/model/ComparableConstraint.java +++ b/src/checkers/inference/model/ComparableConstraint.java @@ -5,84 +5,32 @@ import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.BugInCF; -import com.sun.source.tree.Tree.Kind; - /** * Represents a constraint that two slots must be comparable. * */ -public class ComparableConstraint extends Constraint { - - private final ComparableOperationKind operation; - private final Slot left; - private final Slot right; - - public enum ComparableOperationKind { - REFERENCE(""), - EQUAL_TO("=="), - NOT_EQUAL_TO("!="), - GREATER_THAN(">"), - GREATER_THAN_EQUAL(">="), - LESS_THAN("<"), - LESS_THAN_EQUAL("<="), - OTHER("?"); - - // stores the symbol of the operation - private final String opSymbol; - - private ComparableOperationKind(String opSymbol) { - this.opSymbol = opSymbol; - } +public class ComparableConstraint extends Constraint implements BinaryConstraint { - public static ComparableOperationKind fromTreeKind(Kind kind) { - switch (kind) { - case EQUAL_TO: - return EQUAL_TO; - case NOT_EQUAL_TO: - return NOT_EQUAL_TO; - case GREATER_THAN: - return GREATER_THAN; - case GREATER_THAN_EQUAL: - return GREATER_THAN_EQUAL; - case LESS_THAN: - return LESS_THAN; - case LESS_THAN_EQUAL: - return LESS_THAN_EQUAL; - case INSTANCE_OF: - case TYPE_CAST: - return REFERENCE; - default: - // TODO: Handle all cases and throw error on unsupported operations - return OTHER; - } - } + private final Slot first; + private final Slot second; - public String getSymbol() { - return opSymbol; - } + private ComparableConstraint(Slot first, Slot second, AnnotationLocation location) { + super(Arrays.asList(first, second), location); + this.first = first; + this.second = second; } - private ComparableConstraint(ComparableOperationKind operation, Slot left, Slot right, - AnnotationLocation location) { - super(Arrays.asList(left, right), location); - this.left = left; - this.right = right; - this.operation = operation; + private ComparableConstraint(Slot first, Slot second) { + super(Arrays.asList(first, second)); + this.first = first; + this.second = second; } - private ComparableConstraint(ComparableOperationKind operation, Slot left, Slot right) { - super(Arrays.asList(left, right)); - this.left = left; - this.right = right; - this.operation = operation; - } - - protected static Constraint create(ComparableOperationKind operation, Slot left, Slot right, - AnnotationLocation location, QualifierHierarchy realQualHierarchy) { - if (operation == null || left == null || right == null) { - throw new BugInCF("Create comparable constraint with null argument. " - + "Operation: " + operation + " Subtype: " - + left + " Supertype: " + right); + protected static Constraint create(Slot first, Slot second, AnnotationLocation location, + QualifierHierarchy realQualHierarchy) { + if (first == null || second == null) { + throw new BugInCF("Create comparable constraint with null argument. Subtype: " + + first + " Supertype: " + second); } // Normalization cases: @@ -91,24 +39,23 @@ protected static Constraint create(ComparableOperationKind operation, Slot left, // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT // C1 <~> C2 => TRUE/FALSE depending on relationship - if (left instanceof ConstantSlot && right instanceof ConstantSlot - && operation == ComparableOperationKind.REFERENCE) { - ConstantSlot leftConst = (ConstantSlot) left; - ConstantSlot rightConst = (ConstantSlot) right; + if (first instanceof ConstantSlot && second instanceof ConstantSlot) { + ConstantSlot firstConst = (ConstantSlot) first; + ConstantSlot secondConst = (ConstantSlot) second; - return realQualHierarchy.isSubtype(leftConst.getValue(), rightConst.getValue()) - || realQualHierarchy.isSubtype(rightConst.getValue(), leftConst.getValue()) + return realQualHierarchy.isSubtype(firstConst.getValue(), secondConst.getValue()) + || realQualHierarchy.isSubtype(secondConst.getValue(), firstConst.getValue()) ? AlwaysTrueConstraint.create() : AlwaysFalseConstraint.create(); } - + // V <~> V => TRUE (every type is always comparable to itself) - if (left == right) { + if (first == second) { return AlwaysTrueConstraint.create(); } // otherwise => CREATE_REAL_COMPARABLE_CONSTRAINT - return new ComparableConstraint(operation, left, right, location); + return new ComparableConstraint(first, second, location); } @Override @@ -116,25 +63,27 @@ public T serialize(Serializer serializer) { return serializer.serialize(this); } - public ComparableOperationKind getOperation() { - return operation; + @Override + public Slot getFirst() { + return first; } - public Slot getLeft() { - return left; + @Override + public Slot getSecond() { + return second; } - public Slot getRight() { - return right; + @Override + public Constraint make(Slot first, Slot second) { + return new ComparableConstraint(first, second); } @Override public int hashCode() { - int code = 1; - code = code + ((left == null) ? 0 : left.hashCode()); - code = code + ((right == null) ? 0 : right.hashCode()); - code = code + ((operation == null) ? 0 : operation.hashCode()); - return code; + int result = 1; + result = result + ((first == null) ? 0 : first.hashCode()); + result = result + ((second == null) ? 0 : second.hashCode()); + return result; } @Override @@ -146,8 +95,8 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; ComparableConstraint other = (ComparableConstraint) obj; - if (left.equals(other.left) && right.equals(other.right) - && operation.equals(other.operation)) { + if ((first.equals(other.first) && second.equals(other.second)) + || (first.equals(other.second) && (second.equals(other.first)))) { return true; } else { return false; diff --git a/src/checkers/inference/model/ComparisonConstraint.java b/src/checkers/inference/model/ComparisonConstraint.java new file mode 100644 index 000000000..1afa5c0cd --- /dev/null +++ b/src/checkers/inference/model/ComparisonConstraint.java @@ -0,0 +1,140 @@ +package checkers.inference.model; + +import java.util.Arrays; + +import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.javacutil.BugInCF; + +import com.sun.source.tree.Tree.Kind; + +/** + * Represents a constraint that two slots must be comparable. + * + */ +public class ComparisonConstraint extends Constraint { + + private final ComparisonOperationKind operation; + private final Slot left; + private final Slot right; + private final ComparisonVariableSlot result; + + public enum ComparisonOperationKind { + EQUAL_TO("=="), + NOT_EQUAL_TO("!="), + GREATER_THAN(">"), + GREATER_THAN_EQUAL(">="), + LESS_THAN("<"), + LESS_THAN_EQUAL("<="); + + // stores the symbol of the operation + private final String opSymbol; + + private ComparisonOperationKind(String opSymbol) { + this.opSymbol = opSymbol; + } + + public static ComparisonOperationKind fromTreeKind(Kind kind) { + switch (kind) { + case EQUAL_TO: + return EQUAL_TO; + case NOT_EQUAL_TO: + return NOT_EQUAL_TO; + case GREATER_THAN: + return GREATER_THAN; + case GREATER_THAN_EQUAL: + return GREATER_THAN_EQUAL; + case LESS_THAN: + return LESS_THAN; + case LESS_THAN_EQUAL: + return LESS_THAN_EQUAL; + default: + throw new BugInCF("There are no defined ComparableOperationKind " + + "for the given com.sun.source.tree.Tree.Kind: " + kind); + } + } + + public String getSymbol() { + return opSymbol; + } + } + + private ComparisonConstraint(ComparisonOperationKind operation, Slot left, Slot right, + ComparisonVariableSlot result, AnnotationLocation location) { + super(Arrays.asList(left, right, result), location); + this.left = left; + this.right = right; + this.operation = operation; + this.result = result; + } + + private ComparisonConstraint(ComparisonOperationKind operation, Slot left, Slot right, + ComparisonVariableSlot result) { + super(Arrays.asList(left, right, result)); + this.left = left; + this.right = right; + this.operation = operation; + this.result = result; + } + + protected static Constraint create(ComparisonOperationKind operation, Slot left, Slot right, + ComparisonVariableSlot result, AnnotationLocation location, QualifierHierarchy realQualHierarchy) { + if (operation == null || left == null || right == null) { + throw new BugInCF("Create comparable constraint with null argument. " + + "Operation: " + operation + " Subtype: " + + left + " Supertype: " + right); + } + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "Cannot create an ComparisonConstraint with a missing annotation location."); + } + + return new ComparisonConstraint(operation, left, right, result, location); + } + + @Override + public T serialize(Serializer serializer) { + return serializer.serialize(this); + } + + public ComparisonOperationKind getOperation() { + return operation; + } + + public Slot getLeft() { + return left; + } + + public Slot getRight() { + return right; + } + + public ComparisonVariableSlot getResult() { + return result; + } + + @Override + public int hashCode() { + int code = 1; + code = code + ((left == null) ? 0 : left.hashCode()); + code = code + ((right == null) ? 0 : right.hashCode()); + code = code + ((operation == null) ? 0 : operation.hashCode()); + return code; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + ComparisonConstraint other = (ComparisonConstraint) obj; + if (left.equals(other.left) && right.equals(other.right) + && operation.equals(other.operation)) { + return true; + } else { + return false; + } + } +} \ No newline at end of file diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java new file mode 100644 index 000000000..78fe3937e --- /dev/null +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -0,0 +1,35 @@ +package checkers.inference.model; + +/** + * ComparisonVariableSlot represent the left side refinement of an comparison operation between two other + * {@link VariableSlot}s. + * e.g., for a comparison constraint c := x < y, the comparison variable slot c is the refined value of + * x where x < y is always when x = c. + * Note that this slot is serialized identically to a {@link VariableSlot}. + */ +public class ComparisonVariableSlot extends VariableSlot { + + public ComparisonVariableSlot(AnnotationLocation location, int id) { + super(location, id); + } + + @Override + public Kind getKind() { + return Kind.COMPARISON_VARIABLE; + } + + @Override + public S serialize(Serializer serializer) { + return serializer.serialize(this); + } + + /** + * ComparisonVariable should never be re-inserted into the source code. + * + * @return false + */ + @Override + public boolean isInsertable() { + return false; + } +} \ No newline at end of file diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index 1e20e0efa..e05a4ea40 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -10,7 +10,7 @@ import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.VariableAnnotator; import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; +import checkers.inference.model.ComparisonConstraint.ComparisonOperationKind; /** * Constraint manager holds constraints that are generated by InferenceVisitor. @@ -115,9 +115,16 @@ public Constraint createInequalityConstraint(Slot first, Slot second) { * Creates a {@link ComparableConstraint} between the two slots, which may be normalized to * {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}. */ - public Constraint createComparableConstraint(ComparableOperationKind operation, Slot first, - Slot second) { - return ComparableConstraint.create(operation, first, second, getCurrentLocation(), realQualHierarchy); + public Constraint createComparableConstraint(Slot first, Slot second) { + return ComparableConstraint.create(first, second, getCurrentLocation(), realQualHierarchy); + } + + /** + * Creates a {@link ComparisonConstraint} between the two slots. + */ + public Constraint createComparisonConstraint(ComparisonOperationKind operation, Slot first, + Slot second, ComparisonVariableSlot result) { + return ComparisonConstraint.create(operation, first, second, result, getCurrentLocation(), realQualHierarchy); } /** @@ -235,17 +242,25 @@ public void addInequalityConstraint(Slot first, Slot second) { /** * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set, - * which may be normalized to {@link AlwaysTrueConstraint} if kidn is a reference. - * An error is issued if the {@link ComparableConstraint} is always unsatisfiable. + * which may be normalized to {@link AlwaysTrueConstraint}. An error is issued if the + * {@link ComparableConstraint} is always unsatisfiable. */ - public void addComparableConstraint(ComparableOperationKind operation, Slot first, Slot second) { - Constraint constraint = createComparableConstraint(operation, first, second); + public void addComparableConstraint(Slot first, Slot second) { + Constraint constraint = createComparableConstraint(first, second); if (constraint instanceof AlwaysFalseConstraint) { checker.reportError(visitorState.getPath().getLeaf(), "comparable.constraint.unsatisfiable", first, second); } else { add(constraint); } } + + /** + * Creates and adds a {@link ComparisonConstraint} between the two slots to the constraint set. + */ + public void addComparableConstraint(ComparisonOperationKind operation, Slot left, Slot right, + ComparisonVariableSlot result) { + add(createComparisonConstraint(operation, left, right, result)); + } /** * Creates and adds a {@link CombineConstraint} to the constraint set. diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index 8fd10b6c2..d434458f1 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -39,6 +39,8 @@ public interface Serializer { S serialize(LubVariableSlot slot); T serialize(ComparableConstraint comparableConstraint); + + T serialize(ComparisonConstraint comparisonConstraint); T serialize(CombineConstraint combineConstraint); diff --git a/src/checkers/inference/model/Slot.java b/src/checkers/inference/model/Slot.java index de038b974..4c04bc3ce 100644 --- a/src/checkers/inference/model/Slot.java +++ b/src/checkers/inference/model/Slot.java @@ -51,6 +51,7 @@ public enum Kind { COMB_VARIABLE, ARITHMETIC_VARIABLE, COMPARABLE_VARIABLE, + COMPARISON_VARIABLE, LUB_VARIABLE } diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index e4802becd..0dad6a6a4 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -14,6 +14,7 @@ import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -255,6 +256,12 @@ public VecInt[] serialize(ComparableConstraint comparableConstraint) { // not sure what this means return emptyClauses; } + + @Override + public VecInt[] serialize(ComparisonConstraint comparisonConstraint) { + throw new UnsupportedOperationException( + "Serializing ComparisonConstraint is unsupported in CnfVecIntSerializer"); + } @Override public VecInt[] serialize(CombineConstraint combineConstraint) { diff --git a/src/checkers/inference/model/serialization/JsonDeserializer.java b/src/checkers/inference/model/serialization/JsonDeserializer.java index 3fe80888a..6425bbc7b 100644 --- a/src/checkers/inference/model/serialization/JsonDeserializer.java +++ b/src/checkers/inference/model/serialization/JsonDeserializer.java @@ -17,7 +17,6 @@ import org.json.simple.parser.ParseException; import checkers.inference.InferenceMain; -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.Constraint; import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; @@ -111,7 +110,7 @@ public List jsonArrayToConstraints(final JSONArray jsonConstraints) } else if (COMP_CONSTRAINT_KEY.equals(constraintType)) { Slot lhs = parseSlot((String) constraint.get(COMP_LHS)); Slot rhs = parseSlot((String) constraint.get(COMP_RHS)); - results.add(constraintManager.createComparableConstraint(ComparableOperationKind.OTHER, lhs, rhs)); + results.add(constraintManager.createComparableConstraint(lhs, rhs)); } else if (EXISTENTIAL_CONSTRAINT_KEY.equals(constraintType)) { Slot potential = parseSlot((String) constraint.get(EXISTENTIAL_ID)); List thenConstraints = diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index 9d0282890..5ad519d80 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -15,6 +15,7 @@ import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -122,6 +123,11 @@ public class JsonSerializer implements Serializer { protected static final String COMP_CONSTRAINT_KEY = "comparable"; protected static final String COMP_RHS = "rhs"; protected static final String COMP_LHS = "lhs"; + + protected static final String COMPARISON_CONSTRAINT_KEY = "comparison"; + protected static final String COMPARISON_RHS = "rhs"; + protected static final String COMPARISON_LHS = "lhs"; + protected static final String COMPARISON_RESULT = "result"; protected static final String COMB_CONSTRAINT_KEY = "combine"; protected static final String COMB_TARGET = "target"; @@ -300,14 +306,29 @@ public JSONObject serialize(InequalityConstraint constraint) { @SuppressWarnings("unchecked") @Override public JSONObject serialize(ComparableConstraint constraint) { - if (constraint.getLeft() == null || constraint.getRight() == null) { + if (constraint.getFirst() == null || constraint.getSecond() == null) { return null; } JSONObject obj = new JSONObject(); obj.put(CONSTRAINT_KEY, COMP_CONSTRAINT_KEY); - obj.put(COMP_LHS, constraint.getLeft().serialize(this)); - obj.put(COMP_RHS, constraint.getRight().serialize(this)); + obj.put(COMP_LHS, constraint.getFirst().serialize(this)); + obj.put(COMP_RHS, constraint.getSecond().serialize(this)); + return obj; + } + + @SuppressWarnings("unchecked") + @Override + public JSONObject serialize(ComparisonConstraint constraint) { + if (constraint.getLeft() == null || constraint.getRight() == null) { + return null; + } + + JSONObject obj = new JSONObject(); + obj.put(CONSTRAINT_KEY, COMPARISON_CONSTRAINT_KEY); + obj.put(COMPARISON_LHS, constraint.getLeft().serialize(this)); + obj.put(COMPARISON_RHS, constraint.getRight().serialize(this)); + obj.put(COMPARISON_RESULT, constraint.getResult().serialize(this)); return obj; } diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 60243f83c..47f98221b 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -15,6 +15,7 @@ import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -199,9 +200,29 @@ public String serialize(ComparableConstraint constraint) { showVerboseVars = false; final StringBuilder sb = new StringBuilder(); sb.append(getCurrentIndentString()) - .append(constraint.getLeft().serialize(this)) + .append(constraint.getFirst().serialize(this)) .append(" <~> ") - .append(constraint.getRight().serialize(this)); + .append(constraint.getSecond().serialize(this)); + showVerboseVars = prevShowVerboseVars; + return sb.toString(); + } + + @Override + public String serialize(ComparisonConstraint constraint) { + boolean prevShowVerboseVars = showVerboseVars; + showVerboseVars = false; + // format: result <= ( left comp right ) + final StringBuilder sb = new StringBuilder(); + sb.append(getCurrentIndentString()) + .append(constraint.getResult().serialize(this)) + .append(" <= ( ") + .append(constraint.getLeft().serialize(this)) + .append(" ") + .append(constraint.getOperation().getSymbol()) + .append(" ") + .append(constraint.getRight().serialize(this)) + .append(" )"); + optionallyFormatAstPath(constraint, sb); showVerboseVars = prevShowVerboseVars; return sb.toString(); } diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 8f7b312a4..fbf27a26a 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -4,6 +4,7 @@ import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; @@ -16,9 +17,10 @@ import checkers.inference.model.SubtypeConstraint; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; -import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; import checkers.inference.solver.backend.encoder.ConstraintEncoderCoordinator; import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; @@ -98,6 +100,11 @@ public abstract class AbstractFormatTranslator comparableConstraintEncoder; + + /** + * {@code ComparisonConstraintEncoder} to which encoding of {@link ComparableConstraint} is delegated. + */ + protected ComparisonConstraintEncoder comparisonConstraintEncoder; /** * {@code PreferenceConstraintEncoder} to which encoding of {@link PreferenceConstraint} is delegated. @@ -176,6 +183,12 @@ public ConstraintEncodingT serialize(ComparableConstraint constraint) { return comparableConstraintEncoder == null ? null : ConstraintEncoderCoordinator.dispatch(constraint, comparableConstraintEncoder); } + + @Override + public ConstraintEncodingT serialize(ComparisonConstraint constraint) { + return comparableConstraintEncoder == null ? null : + ConstraintEncoderCoordinator.dispatch(constraint, comparisonConstraintEncoder); + } @Override public ConstraintEncodingT serialize(PreferenceConstraint constraint) { diff --git a/src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java deleted file mode 100644 index 72c401e73..000000000 --- a/src/checkers/inference/solver/backend/encoder/ComparableConstraintEncoder.java +++ /dev/null @@ -1,28 +0,0 @@ -package checkers.inference.solver.backend.encoder; - -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; -import checkers.inference.solver.backend.encoder.binary.BinaryConstraintEncoder; -import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; - -/** - * A marker interface that all constraint encoders that support encoding {@link checkers.inference.model.ComparableConstraint} - * should implement. Otherwise, the encoder will be considered not supporting encoding comparable - * constraint and rejected by the {@link AbstractConstraintEncoderFactory#createComparableConstraintEncoder()} - * - * @see checkers.inference.model.ComparableConstraint - * @see AbstractConstraintEncoderFactory#createComparableConstraintEncoder() - */ -public interface ComparableConstraintEncoder { - ConstraintEncodingT encodeVariable_Variable(ComparableOperationKind operation, - VariableSlot left, VariableSlot right); - - ConstraintEncodingT encodeVariable_Constant(ComparableOperationKind operation, - VariableSlot left, ConstantSlot right); - - ConstraintEncodingT encodeConstant_Variable(ComparableOperationKind operation, - ConstantSlot left, VariableSlot right); - - ConstraintEncodingT encodeConstant_Constant(ComparableOperationKind operation, - ConstantSlot left, ConstantSlot right); -} diff --git a/src/checkers/inference/solver/backend/encoder/ComparisonConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/ComparisonConstraintEncoder.java new file mode 100644 index 000000000..b3b522e8a --- /dev/null +++ b/src/checkers/inference/solver/backend/encoder/ComparisonConstraintEncoder.java @@ -0,0 +1,28 @@ +package checkers.inference.solver.backend.encoder; + +import checkers.inference.model.ComparisonConstraint.ComparisonOperationKind; +import checkers.inference.model.ComparisonVariableSlot; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.VariableSlot; + +/** + * A marker interface that all constraint encoders that support encoding {@link checkers.inference.model.ComparisonConstraint} + * should implement. Otherwise, the encoder will be considered not supporting encoding comparable + * constraint and rejected by the {@link AbstractConstraintEncoderFactory#createComparisonConstraintEncoder()} + * + * @see checkers.inference.model.ComparisonConstraint + * @see AbstractConstraintEncoderFactory#createComparisonConstraintEncoder() + */ +public interface ComparisonConstraintEncoder { + ConstraintEncodingT encodeVariable_Variable(ComparisonOperationKind operation, + VariableSlot left, VariableSlot right, ComparisonVariableSlot result); + + ConstraintEncodingT encodeVariable_Constant(ComparisonOperationKind operation, + VariableSlot left, ConstantSlot right, ComparisonVariableSlot result); + + ConstraintEncodingT encodeConstant_Variable(ComparisonOperationKind operation, + ConstantSlot left, VariableSlot right, ComparisonVariableSlot result); + + ConstraintEncodingT encodeConstant_Constant(ComparisonOperationKind operation, + ConstantSlot left, ConstantSlot right, ComparisonVariableSlot result); +} diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java index a5c12702e..2146c773b 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java @@ -5,6 +5,8 @@ import checkers.inference.model.BinaryConstraint; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ImplicationConstraint; @@ -81,25 +83,25 @@ public static ConstraintEncodingT dispatch(CombineConstrai } public static ConstraintEncodingT dispatch( - ComparableConstraint constraint, - ComparableConstraintEncoder encoder) { + ComparisonConstraint constraint, + ComparisonConstraintEncoder encoder) { switch (SlotSlotCombo.valueOf(constraint.getLeft(), constraint.getRight())) { case VARIABLE_VARIABLE: return encoder.encodeVariable_Variable(constraint.getOperation(), (VariableSlot) constraint.getLeft(), - (VariableSlot) constraint.getRight()); + (VariableSlot) constraint.getRight(), constraint.getResult()); case VARIABLE_CONSTANT: return encoder.encodeVariable_Constant(constraint.getOperation(), (VariableSlot) constraint.getLeft(), - (ConstantSlot) constraint.getRight()); + (ConstantSlot) constraint.getRight(), constraint.getResult()); case CONSTANT_VARIABLE: return encoder.encodeConstant_Variable(constraint.getOperation(), (ConstantSlot) constraint.getLeft(), - (VariableSlot) constraint.getRight()); + (VariableSlot) constraint.getRight(), constraint.getResult()); case CONSTANT_CONSTANT: return encoder.encodeConstant_Constant(constraint.getOperation(), (ConstantSlot) constraint.getLeft(), - (ConstantSlot) constraint.getRight()); + (ConstantSlot) constraint.getRight(), constraint.getResult()); } return null; } diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java index d3bd1143d..3c28727e7 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java @@ -1,5 +1,6 @@ package checkers.inference.solver.backend.encoder; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; @@ -18,6 +19,7 @@ *
  • {@link EqualityConstraintEncoder}
    • *
  • {@link InequalityConstraintEncoder}
    • *
  • {@link ComparableConstraintEncoder}
    • + *
  • {@link ComparisonConstraintEncoder}
    • *
  • {@link PreferenceConstraintEncoder}
    • *
  • {@link CombineConstraintEncoder}
    • *
  • {@link ExistentialConstraintEncoder}
    • @@ -39,6 +41,8 @@ public interface ConstraintEncoderFactory { InequalityConstraintEncoder createInequalityConstraintEncoder(); ComparableConstraintEncoder createComparableConstraintEncoder(); + + ComparisonConstraintEncoder createComparisonConstraintEncoder(); PreferenceConstraintEncoder createPreferenceConstraintEncoder(); diff --git a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java new file mode 100644 index 000000000..ac3f44bec --- /dev/null +++ b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java @@ -0,0 +1,14 @@ +package checkers.inference.solver.backend.encoder.binary; + +import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; + +/** + * A marker interface that all constraint encoders that support encoding {@link checkers.inference.model.ComparableConstraint} + * should implement. Otherwise, the encoder will be considered not supporting encoding comparable + * constraint and rejected by the {@link AbstractConstraintEncoderFactory#createComparableConstraintEncoder()} + * + * @see checkers.inference.model.ComparableConstraint + * @see AbstractConstraintEncoderFactory#createComparableConstraintEncoder() + */ +public interface ComparableConstraintEncoder extends BinaryConstraintEncoder { +} \ No newline at end of file diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 7caf1998f..1873a627d 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -1,9 +1,8 @@ package checkers.inference.solver.backend.logiql.encoder; -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,37 +12,24 @@ public LogiQLComparableConstraintEncoder(Lattice lattice) { super(lattice); } - @Override - public String encodeVariable_Variable(ComparableOperationKind operation, VariableSlot fst, VariableSlot snd) { - String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + @Override + public String encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; return logiQLData; - } + } - @Override - public String encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { - String constantName = NameUtils.getSimpleName(snd.getValue()); - int variableId = fst.getId(); - String logiQLData = "+comparableConstraint(v, c), +variable(v), +hasvariableName[v] = \"" - + variableId + "\", +constant(c), +hasconstantName[c] = " + constantName + ".\n"; - return logiQLData; - } + @Override + public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + return encodeConstant_Variable(snd, fst); + } - @Override - public String encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { - String constantName = NameUtils.getSimpleName(fst.getValue()); + @Override + public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); - String logiQLData = "+comparableConstraint(c, v), +constant(c), +hasconstantName[c] = \"" + String logiQLData = "+equalityConstraintContainsConstant(c, v), +constant(c), +hasconstantName[c] = \"" + constantName + "\", +variable(v), +hasvariableName[v] = " + variableId + ".\n"; return logiQLData; - } - - @Override - public String encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd) { - String constantNamefst = NameUtils.getSimpleName(fst.getValue()); - String constantNamesnd = NameUtils.getSimpleName(snd.getValue()); - String logiQLData = "+comparableConstraint(c1, c2), +constant(c1), +hasconstantName[c1] = \"" - + constantNamefst + "\", +constant(c2), +hasconstantName[c2] = " + constantNamesnd + ".\n"; - return logiQLData; - } -} + } +} \ No newline at end of file diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java index 4c6c12116..e92e4a925 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java @@ -2,7 +2,8 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; -import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; @@ -43,6 +44,11 @@ public InequalityConstraintEncoder createInequalityConstraintEncoder() { public ComparableConstraintEncoder createComparableConstraintEncoder() { return new LogiQLComparableConstraintEncoder(lattice); } + + @Override + public ComparisonConstraintEncoder createComparisonConstraintEncoder() { + return null; + } @Override public PreferenceConstraintEncoder createPreferenceConstraintEncoder() { diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index 7574298d1..c97283f7a 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -1,9 +1,8 @@ package checkers.inference.solver.backend.maxsat.encoder; -import checkers.inference.model.ComparableConstraint.ComparableOperationKind; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; -import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; import checkers.inference.solver.frontend.Lattice; @@ -20,9 +19,9 @@ public MaxSATComparableConstraintEncoder(Lattice lattice, Map !b which is the same as (!a v !b) & (b v a) + @Override + public VecInt[] encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + // a <=> !b which is the same as (!a v !b) & (b v a) List list = new ArrayList(); for (AnnotationMirror type : lattice.allTypes) { if (lattice.incomparableType.keySet().contains(type)) { @@ -37,11 +36,11 @@ public VecInt[] encodeVariable_Variable(ComparableOperationKind operation, Varia } VecInt[] result = list.toArray(new VecInt[list.size()]); return result; - } + } - @Override - public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, VariableSlot fst, ConstantSlot snd) { - if (lattice.incomparableType.keySet().contains(snd.getValue())) { + @Override + public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + if (lattice.incomparableType.keySet().contains(snd.getValue())) { List resultList = new ArrayList<>(); for (AnnotationMirror incomparable : lattice.incomparableType.get(snd.getValue())) { // Should not be equal to incomparable @@ -54,15 +53,10 @@ public VecInt[] encodeVariable_Constant(ComparableOperationKind operation, Varia } else { return emptyValue; } - } - - @Override - public VecInt[] encodeConstant_Variable(ComparableOperationKind operation, ConstantSlot fst, VariableSlot snd) { - return encodeVariable_Constant(operation, snd, fst); - } + } - @Override - public VecInt[] encodeConstant_Constant(ComparableOperationKind operation, ConstantSlot fst, ConstantSlot snd) { - return null; - } -} + @Override + public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + return encodeVariable_Constant(snd, fst); + } +} \ No newline at end of file diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java index 4dcfaf12f..b9c026501 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java @@ -2,6 +2,7 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; @@ -46,6 +47,12 @@ public MaxSATInequalityConstraintEncoder createInequalityConstraintEncoder() { public MaxSATComparableConstraintEncoder createComparableConstraintEncoder() { return new MaxSATComparableConstraintEncoder(lattice, typeToInt); } + + @Override + public ComparisonConstraintEncoder createComparisonConstraintEncoder() { + return null; + } + @Override public MaxSATPreferenceConstraintEncoder createPreferenceConstraintEncoder() { diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java index f1d396379..9d42df3d9 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java @@ -2,7 +2,8 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; -import checkers.inference.solver.backend.encoder.ComparableConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; +import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; @@ -49,6 +50,11 @@ public InequalityConstraintEncoder createInequalityConstraintEncoder() public ComparableConstraintEncoder createComparableConstraintEncoder() { return null; } + + @Override + public ComparisonConstraintEncoder createComparisonConstraintEncoder() { + return null; + } @Override public PreferenceConstraintEncoder createPreferenceConstraintEncoder() { diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index e052c3c3e..68872d893 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -16,6 +16,7 @@ import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -246,8 +247,16 @@ public Void serialize(InequalityConstraint constraint) { @Override public Void serialize(ComparableConstraint constraint) { + constraint.getFirst().serialize(this); + constraint.getSecond().serialize(this); + return null; + } + + @Override + public Void serialize(ComparisonConstraint constraint) { constraint.getLeft().serialize(this); constraint.getRight().serialize(this); + constraint.getResult().serialize(this); return null; } From b6e269c4be750202fb281be13021da3278b38349 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Jun 2020 14:31:50 -0400 Subject: [PATCH 07/24] clean up --- src/checkers/inference/InferenceVisitor.java | 4 ++-- src/checkers/inference/model/ConstraintManager.java | 2 +- src/checkers/inference/model/Slot.java | 1 - .../backend/encoder/binary/ComparableConstraintEncoder.java | 2 +- .../logiql/encoder/LogiQLComparableConstraintEncoder.java | 2 +- .../maxsat/encoder/MaxSATComparableConstraintEncoder.java | 2 +- 6 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index 1d9b6d17c..bc66b918d 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/src/checkers/inference/InferenceVisitor.java @@ -38,7 +38,6 @@ import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceUtil; -import com.sun.source.tree.BinaryTree; import com.sun.source.tree.CatchTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodTree; @@ -317,6 +316,7 @@ private void annoIsNoneOf(AnnotatedTypeMirror sourceType, AnnotationMirror effec } } + public void areComparable(AnnotatedTypeMirror ty1, AnnotatedTypeMirror ty2, String msgkey, Tree node) { if (infer) { final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); @@ -329,7 +329,7 @@ public void areComparable(AnnotatedTypeMirror ty1, AnnotatedTypeMirror ty2, Stri } else { if (!InferenceMain.getInstance().isPerformingFlow()) { logger.fine("InferenceVisitor::areComparable: Comparable constraint constructor invocation."); - InferenceMain.getInstance().getConstraintManager().addComparableConstraint(el1, el2); + InferenceMain.getInstance().getConstraintManager().addComparableConstraint(el1, el2); } } } else { diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index e05a4ea40..045e4261f 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -239,7 +239,7 @@ public void addInequalityConstraint(Slot first, Slot second) { add(constraint); } } - + /** * Creates and adds a {@link ComparableConstraint} between the two slots to the constraint set, * which may be normalized to {@link AlwaysTrueConstraint}. An error is issued if the diff --git a/src/checkers/inference/model/Slot.java b/src/checkers/inference/model/Slot.java index 4c04bc3ce..4c7b4c6e8 100644 --- a/src/checkers/inference/model/Slot.java +++ b/src/checkers/inference/model/Slot.java @@ -50,7 +50,6 @@ public enum Kind { EXISTENTIAL_VARIABLE, COMB_VARIABLE, ARITHMETIC_VARIABLE, - COMPARABLE_VARIABLE, COMPARISON_VARIABLE, LUB_VARIABLE } diff --git a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java index ac3f44bec..4efb41b05 100644 --- a/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/binary/ComparableConstraintEncoder.java @@ -11,4 +11,4 @@ * @see AbstractConstraintEncoderFactory#createComparableConstraintEncoder() */ public interface ComparableConstraintEncoder extends BinaryConstraintEncoder { -} \ No newline at end of file +} diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 1873a627d..68a127f22 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -32,4 +32,4 @@ public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + constantName + "\", +variable(v), +hasvariableName[v] = " + variableId + ".\n"; return logiQLData; } -} \ No newline at end of file +} diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index c97283f7a..a9cb02d9a 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -59,4 +59,4 @@ public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encodeVariable_Constant(snd, fst); } -} \ No newline at end of file +} From 5b7df57fa93b3a6658b0ec16e2a76a3b8d4880d0 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Jun 2020 14:32:22 -0400 Subject: [PATCH 08/24] Update ComparisonVariableSlot.java --- src/checkers/inference/model/ComparisonVariableSlot.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java index 78fe3937e..96a980b11 100644 --- a/src/checkers/inference/model/ComparisonVariableSlot.java +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -32,4 +32,4 @@ public S serialize(Serializer serializer) { public boolean isInsertable() { return false; } -} \ No newline at end of file +} From 7cc964792e6bb7f4927489666c9e2844f9a99a47 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Jun 2020 14:32:37 -0400 Subject: [PATCH 09/24] Update ComparisonConstraint.java --- src/checkers/inference/model/ComparisonConstraint.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/checkers/inference/model/ComparisonConstraint.java b/src/checkers/inference/model/ComparisonConstraint.java index 1afa5c0cd..20181b303 100644 --- a/src/checkers/inference/model/ComparisonConstraint.java +++ b/src/checkers/inference/model/ComparisonConstraint.java @@ -137,4 +137,4 @@ public boolean equals(Object obj) { return false; } } -} \ No newline at end of file +} From d7f746f1cd0c1cfd0b9fdaea54ce2f737e255da9 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 3 Jun 2021 02:11:57 -0400 Subject: [PATCH 10/24] fix compile error --- .../inference/model/ComparisonVariableSlot.java | 4 ++-- src/checkers/inference/model/Serializer.java | 2 ++ .../model/serialization/CnfVecIntSerializer.java | 6 ++++++ .../model/serialization/JsonSerializer.java | 6 ++++++ .../model/serialization/ToStringSerializer.java | 12 ++++++++++++ .../solver/backend/AbstractFormatTranslator.java | 6 ++++++ src/checkers/inference/solver/util/PrintUtils.java | 7 +++++++ 7 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java index 96a980b11..817e5f47f 100644 --- a/src/checkers/inference/model/ComparisonVariableSlot.java +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -9,8 +9,8 @@ */ public class ComparisonVariableSlot extends VariableSlot { - public ComparisonVariableSlot(AnnotationLocation location, int id) { - super(location, id); + public ComparisonVariableSlot(int id, AnnotationLocation location) { + super(id, location); } @Override diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index cfe76d9a5..e687aec03 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -38,6 +38,8 @@ public interface Serializer { S serialize(LubVariableSlot slot); + S serialize(ComparisonVariableSlot slot); + S serialize(ArithmeticVariableSlot slot); T serialize(ComparableConstraint comparableConstraint); diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 77250a5be..620710a19 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -17,6 +17,7 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -253,6 +254,11 @@ public VecInt[] serialize(ArithmeticVariableSlot slot) { return null; } + @Override + public VecInt[] serialize(ComparisonVariableSlot slot) { + return null; + } + @Override public VecInt[] serialize(ExistentialVariableSlot slot) { // See checkers.inference.ConstraintNormalizer.normalize() diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index fbbe511c2..7713d9bec 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -17,6 +17,7 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -259,6 +260,11 @@ public String serialize(ArithmeticVariableSlot slot) { return serializeSlot(slot); } + @Override + public String serialize(ComparisonVariableSlot slot) { + return serializeSlot(slot); + } + @SuppressWarnings("unchecked") @Override public JSONObject serialize(SubtypeConstraint constraint) { diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index cc0b7fc68..bd849ad7a 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -17,6 +17,7 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -377,6 +378,17 @@ public String serialize(ArithmeticVariableSlot slot) { return sb.toString(); } + @Override + public String serialize(ComparisonVariableSlot slot) { + final StringBuilder sb = new StringBuilder(); + sb.append(slot.getId()); + if (showVerboseVars) { + // TODO: show more comparison-specific details + optionallyShowVerbose(slot, sb); + } + return sb.toString(); + } + /** * @return the indent string for the current indentation level as stored in * {@link #indentationLevel}. diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 0966cb488..454e8f5e5 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -6,6 +6,7 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; @@ -255,4 +256,9 @@ public SlotEncodingT serialize(LubVariableSlot slot) { public SlotEncodingT serialize(ArithmeticVariableSlot slot) { return null; } + + @Override + public SlotEncodingT serialize(ComparisonVariableSlot slot) { + return null; + } } diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index 6e30e5ca9..99eb5c889 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -18,6 +18,7 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; import checkers.inference.model.ComparisonConstraint; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; @@ -343,5 +344,11 @@ public Void serialize(ArithmeticVariableSlot slot) { addSlotIfNotAdded(slot); return null; } + + @Override + public Void serialize(ComparisonVariableSlot slot) { + addSlotIfNotAdded(slot); + return null; + } } } From 73c4ac9f85f499dd5a227e77ecee6c370ca5a3e5 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 3 Jun 2021 22:39:42 -0400 Subject: [PATCH 11/24] separate comparable and comparison --- .../inference/DefaultSlotManager.java | 67 +++++++++++ src/checkers/inference/SlotManager.java | 26 +++++ .../inference/dataflow/InferenceTransfer.java | 106 ++++++++++++++++-- .../model/ComparisonVariableSlot.java | 2 +- .../inference/model/ConstraintManager.java | 2 +- 5 files changed, 193 insertions(+), 10 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 5976d8778..85fe03dde 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -26,6 +26,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -97,6 +98,22 @@ public class DefaultSlotManager implements SlotManager { */ private final Map arithmeticSlotCache; + /** + * A map of {@link AnnotationLocation} to {@link Integer} for caching + * {@link ComparisonVariableSlot}s. The annotation location uniquely identifies an + * {@link ComparisonVariableSlot}. The {@link Integer} is the Id of the corresponding + * {@link ComparisonVariableSlot}. + */ + private final Map comparisonThenSlotCache; + + /** + * A map of {@link AnnotationLocation} to {@link Integer} for caching + * {@link ComparisonVariableSlot}s. The annotation location uniquely identifies an + * {@link ComparisonVariableSlot}. The {@link Integer} is the Id of the corresponding + * {@link ComparisonVariableSlot}. + */ + private final Map comparisonElseSlotCache; + private final Set> realQualifiers; private final ProcessingEnvironment processingEnvironment; @@ -119,6 +136,8 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment, combSlotPairCache = new LinkedHashMap<>(); lubSlotPairCache = new LinkedHashMap<>(); arithmeticSlotCache = new LinkedHashMap<>(); + comparisonThenSlotCache = new LinkedHashMap<>(); + comparisonElseSlotCache = new LinkedHashMap<>(); if (storeConstants) { for (Class annoClass : this.realQualifiers) { @@ -436,6 +455,54 @@ public ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation locat } } + @Override + public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch) { + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "Cannot create an ComparisonVariableSlot with a missing annotation location."); + } + + // create the comparison var slot if it doesn't exist for the given location + if (thenBranch && !comparisonThenSlotCache.containsKey(location)) { + ComparisonVariableSlot slot = new ComparisonVariableSlot(nextId(), location, refined); + addToSlots(slot); + comparisonThenSlotCache.put(location, slot.getId()); + return slot; + } + + // create the comparison var slot if it doesn't exist for the given location + if (!thenBranch && !comparisonElseSlotCache.containsKey(location)) { + ComparisonVariableSlot slot = new ComparisonVariableSlot(nextId(), location, refined); + addToSlots(slot); + comparisonElseSlotCache.put(location, slot.getId()); + return slot; + } + + return getComparisonVariableSlot(location, thenBranch); + } + + @Override + public ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch) { + if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { + throw new BugInCF( + "ComparisonVariableSlot are never created with a missing annotation location."); + } + if (thenBranch) { + if (!comparisonThenSlotCache.containsKey(location)) { + return null; + } else { + return (ComparisonVariableSlot) getSlot(comparisonThenSlotCache.get(location)); + } + } else { + if (!comparisonElseSlotCache.containsKey(location)) { + return null; + } else { + return (ComparisonVariableSlot) getSlot(comparisonElseSlotCache.get(location)); + } + } + } + + @Override public AnnotationMirror createEquivalentVarAnno(AnnotationMirror realQualifier) { ConstantSlot varSlot = createConstantSlot(realQualifier); diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 1f10f9b30..2cf954ef5 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -11,6 +11,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; @@ -151,6 +152,31 @@ public interface SlotManager { */ ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation location); + /** + * Create new ComparisonVariableSlot at the given location and return a reference to it if no + * ComparisonVariableSlot exists for the location. Otherwise, returns the existing + * ComparisonVariableSlot. + * + * @param location an AnnotationLocation used to locate this variable in code + * @param thenBranch true if is for the then store, false if is for the else store + * @return the ComparisonVariableSlot for the given location + */ + ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch); + + /** + * Retrieves the ComparisonVariableSlot created for the given location if it has been previously + * created, otherwise null is returned. + * + * This method allows faster retrieval of already created ComparisonVariableSlot during + * traversals of binary comparison trees in an InferenceTransfer subclass, which does not have direct access + * to the ATM containing this slot. + * + * @param location an AnnotationLocation used to locate this variable in code + * @param thenBranch true if is for the then store, false if is for the else store + * @return the ComparisonVariableSlot for the given location, or null if none exists + */ + ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch); + /** * Create a VarAnnot equivalent to the given realQualifier. * diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 7db32c673..83c0d0f19 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -1,12 +1,16 @@ package checkers.inference.dataflow; +import org.checkerframework.dataflow.analysis.ConditionalTransferResult; +import org.checkerframework.dataflow.analysis.FlowExpressions; import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.EqualToNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.NotEqualNode; import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode; import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; import org.checkerframework.framework.flow.CFStore; @@ -21,6 +25,7 @@ import java.util.Map; import java.util.logging.Logger; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; import com.sun.source.tree.CompoundAssignmentTree; @@ -33,6 +38,8 @@ import checkers.inference.SlotManager; import checkers.inference.VariableAnnotator; import checkers.inference.model.AnnotationLocation; +import checkers.inference.model.ComparisonVariableSlot; +import checkers.inference.model.ConstraintManager; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; @@ -63,8 +70,11 @@ public class InferenceTransfer extends CFTransfer { // case where the correct, inferred RHS has no primary annotation private Map> createdTypeVarRefinementVariables = new HashMap<>(); + private final InferenceAnnotatedTypeFactory typeFactory; + public InferenceTransfer(InferenceAnalysis analysis) { super(analysis); + typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory(); } private InferenceAnalysis getInferenceAnalysis() { @@ -92,7 +102,6 @@ public TransferResult visitAssignment(AssignmentNode assignmen Node lhs = assignmentNode.getTarget(); CFStore store = transferInput.getRegularStore(); - InferenceAnnotatedTypeFactory typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory(); // Target tree is null for field access's Tree targetTree = assignmentNode.getTarget().getTree(); @@ -137,7 +146,7 @@ public TransferResult visitAssignment(AssignmentNode assignmen assert false; } - return storeDeclaration(lhs, (VariableTree) assignmentNode.getTree(), store, typeFactory); + return storeDeclaration(lhs, (VariableTree) assignmentNode.getTree(), store); } else if (lhs.getTree().getKind() == Tree.Kind.IDENTIFIER || lhs.getTree().getKind() == Tree.Kind.MEMBER_SELECT) { @@ -179,7 +188,6 @@ public TransferResult visitAssignment(AssignmentNode assignmen public TransferResult visitStringConcatenateAssignment(StringConcatenateAssignmentNode assignmentNode, TransferInput transferInput) { // TODO: CompoundAssigment trees are not refined, see Issue 9 CFStore store = transferInput.getRegularStore(); - InferenceAnnotatedTypeFactory typeFactory = (InferenceAnnotatedTypeFactory) analysis.getTypeFactory(); Tree targetTree = assignmentNode.getLeftOperand().getTree(); @@ -225,7 +233,7 @@ private TransferResult createRefinementVar(Node lhs, refVar = createdRefinementVariables.get(assignmentTree); } else { AnnotationLocation location = VariableAnnotator.treeToLocation(analysis.getTypeFactory(), assignmentTree); - refVar = getInferenceAnalysis().getSlotManager().createRefinementVariableSlot(location, slotToRefine, refineTo); + refVar = slotManager.createRefinementVariableSlot(location, slotToRefine, refineTo); // Fields from library methods can be refined, but the slotToRefine is a ConstantSlot // which does not have a refined slots field. @@ -236,7 +244,7 @@ private TransferResult createRefinementVar(Node lhs, createdRefinementVariables.put(assignmentTree, refVar); } - atm.replaceAnnotation(getInferenceAnalysis().getSlotManager().getAnnotation(refVar)); + atm.replaceAnnotation(slotManager.getAnnotation(refVar)); // add refinement variable value to output CFValue result = analysis.createAbstractValue(atm); @@ -379,12 +387,10 @@ private TransferResult createTypeVarRefinementVars(Node lhs, T * @param lhs * @param assignmentTree * @param store - * @param typeFactory * @return */ private TransferResult storeDeclaration(Node lhs, - VariableTree assignmentTree, CFStore store, - InferenceAnnotatedTypeFactory typeFactory) { + VariableTree assignmentTree, CFStore store) { AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(assignmentTree); CFValue result = analysis.createAbstractValue(atm); @@ -395,4 +401,88 @@ private TransferResult storeDeclaration(Node lhs, private boolean isDeclarationWithInitializer(AssignmentNode assignmentNode) { return (assignmentNode.getTree().getKind() == Tree.Kind.VARIABLE); } + + + private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore elseStore) { + // Only create refinement comparison slot for variables + // TODO: deal with comparison between more complex expressions + Node var = node; + if (node instanceof AssignmentNode) { + AssignmentNode a = (AssignmentNode) node; + var = a.getTarget(); + } + if (!(var instanceof LocalVariableNode) && !(var instanceof FieldAccessNode)) { + return; + } + Tree tree = var.getTree(); + ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + SlotManager slotManager = getInferenceAnalysis().getSlotManager(); + + AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree); + Slot slotToRefine = slotManager.getSlot(atm); + + // TODO: Understand why there are null slots + if (InferenceMain.isHackMode(slotToRefine == null)) { + logger.fine("HackMode: slotToRefine is null !"); + return; + } + + if (slotToRefine instanceof RefinementVariableSlot) { + slotToRefine = ((RefinementVariableSlot) slotToRefine).getRefined(); + assert !(slotToRefine instanceof RefinementVariableSlot); + } + + AnnotationLocation location = + VariableAnnotator.treeToLocation(analysis.getTypeFactory(), tree); + // TODO: find out why there are missing location + if (InferenceMain.isHackMode(location == AnnotationLocation.MISSING_LOCATION)) { + logger.fine("HackMode: create ComparisonVariableSlot on MISSING_LOCATION !"); + return; + } + ComparisonVariableSlot thenSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, true); + constraintManager.addSubtypeConstraint(thenSlot, slotToRefine); + ComparisonVariableSlot elseSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, false); + constraintManager.addSubtypeConstraint(elseSlot, slotToRefine); + AnnotationMirror thenAm = slotManager.getAnnotation(thenSlot); + AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot); + + // If node is assignment, iterate over lhs; otherwise, just node. + FlowExpressions.Receiver rec; + rec = FlowExpressions.internalReprOf(getInferenceAnalysis().getTypeFactory(), var); + thenStore.clearValue(rec); + thenStore.insertValue(rec, thenAm); + elseStore.clearValue(rec); + elseStore.insertValue(rec, elseAm); + } + + @Override + public TransferResult visitEqualTo( + EqualToNode n, TransferInput in) { + TransferResult result = super.visitEqualTo(n, in); + CFStore thenStore = result.getThenStore(); + CFStore elseStore = result.getElseStore(); + + createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore); + createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore); + + CFValue newResultValue = + getInferenceAnalysis() + .createAbstractValue(typeFactory.getAnnotatedType(n.getTree())); + return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore); + } + + @Override + public TransferResult visitNotEqual( + NotEqualNode n, TransferInput in) { + TransferResult result = super.visitNotEqual(n, in); + CFStore thenStore = result.getThenStore(); + CFStore elseStore = result.getElseStore(); + + createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore); + createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore); + + CFValue newResultValue = + analysis.createAbstractValue(typeFactory.getAnnotatedType(n.getTree())); + return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore); + } } diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java index 817e5f47f..b1cf11526 100644 --- a/src/checkers/inference/model/ComparisonVariableSlot.java +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -9,7 +9,7 @@ */ public class ComparisonVariableSlot extends VariableSlot { - public ComparisonVariableSlot(int id, AnnotationLocation location) { + public ComparisonVariableSlot(int id, AnnotationLocation location, Slot refined) { super(id, location); } diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index 9ce090fb0..d8b1dfc27 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -257,7 +257,7 @@ public void addComparableConstraint(Slot first, Slot second) { /** * Creates and adds a {@link ComparisonConstraint} between the two slots to the constraint set. */ - public void addComparableConstraint(ComparisonOperationKind operation, Slot left, Slot right, + public void addComparsionConstraint(ComparisonOperationKind operation, Slot left, Slot right, ComparisonVariableSlot result) { add(createComparisonConstraint(operation, left, right, result)); } From 300e147d3f0b8651c9987e4fabfbdd2d13a05519 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 4 Jun 2021 13:56:41 -0400 Subject: [PATCH 12/24] bug-fix --- src/checkers/inference/dataflow/InferenceValue.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 8ac9b3aa0..36faf5daa 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/src/checkers/inference/dataflow/InferenceValue.java @@ -233,7 +233,7 @@ public String toString() { // TODO: improve output of ConstantSlot itself sb.append(slot.getClass().getSimpleName()); sb.append("("); - sb.append(((VariableSlot)slot).getId()); + sb.append(slot.getId()); sb.append(")"); sb.append(")"); From 45c9872038f199119417836368b78c5b6226fa33 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 4 Jun 2021 22:06:52 -0400 Subject: [PATCH 13/24] refine comparison operand with comparison variable slots --- .../inference/dataflow/InferenceTransfer.java | 7 +++ .../inference/dataflow/InferenceValue.java | 58 +++++++++++-------- .../model/ComparisonVariableSlot.java | 6 ++ .../inference/model/VariableSlot.java | 4 +- 4 files changed, 50 insertions(+), 25 deletions(-) diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 83c0d0f19..633335184 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -443,6 +443,13 @@ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore constraintManager.addSubtypeConstraint(thenSlot, slotToRefine); ComparisonVariableSlot elseSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, false); constraintManager.addSubtypeConstraint(elseSlot, slotToRefine); + + if (slotToRefine instanceof VariableSlot) { + // ComparisonVariableSlots stores the refined value after comparison, so add it to the "refinedTo" list + ((VariableSlot) slotToRefine).getRefinedToSlots().add(thenSlot); + ((VariableSlot) slotToRefine).getRefinedToSlots().add(elseSlot); + } + AnnotationMirror thenAm = slotManager.getAnnotation(thenSlot); AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot); diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 36faf5daa..bdbe4ef4c 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/src/checkers/inference/dataflow/InferenceValue.java @@ -1,5 +1,6 @@ package checkers.inference.dataflow; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.util.InferenceUtil; import javax.lang.model.type.TypeVariable; import org.checkerframework.framework.flow.CFValue; @@ -119,30 +120,41 @@ public CFValue mostSpecific(CFValue other, CFValue backup) { * */ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, final CFValue other, final CFValue backup) { - if (thisSlot.isVariable() && otherSlot.isVariable()) { - if (thisSlot.isMergedTo(otherSlot)) { - return other; - } else if (otherSlot.isMergedTo(thisSlot)) { - return this; - } else if (thisSlot instanceof RefinementVariableSlot - && ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) { - - return this; - } else if (otherSlot instanceof RefinementVariableSlot - && ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) { - - return other; - } else { - // Check if one of these has refinement variables that were merged to the other. - for (RefinementVariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) { - if (slot.isMergedTo(otherSlot)) { - return other; - } + if (thisSlot.isMergedTo(otherSlot)) { + return other; + } + if (otherSlot.isMergedTo(thisSlot)) { + return this; + } + if (thisSlot instanceof RefinementVariableSlot + && ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) { + return this; + } + if (otherSlot instanceof RefinementVariableSlot + && ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) { + return other; + } + if (thisSlot instanceof ComparisonVariableSlot + && ((ComparisonVariableSlot) thisSlot).getRefined().equals(otherSlot)) { + return this; + } + if (otherSlot instanceof ComparisonVariableSlot + && ((ComparisonVariableSlot) otherSlot).getRefined().equals(thisSlot)) { + return other; + } + + if (thisSlot.isVariable()) { + // Check if one of these has refinement variables that were merged to the other. + for (VariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) { + if (slot.isMergedTo(otherSlot)) { + return other; } - for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) { - if (slot.isMergedTo(thisSlot)) { - return this; - } + } + } + if (otherSlot.isVariable()) { + for (VariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) { + if (slot.isMergedTo(thisSlot)) { + return this; } } } diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java index b1cf11526..ba3a0b263 100644 --- a/src/checkers/inference/model/ComparisonVariableSlot.java +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -8,9 +8,15 @@ * Note that this slot is serialized identically to a {@link VariableSlot}. */ public class ComparisonVariableSlot extends VariableSlot { + private final Slot refined; public ComparisonVariableSlot(int id, AnnotationLocation location, Slot refined) { super(id, location); + this.refined = refined; + } + + public Slot getRefined() { + return refined; } @Override diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 5306e741e..4b4d4b653 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -31,7 +31,7 @@ public abstract class VariableSlot extends Slot { private AnnotationLocation location; /** Refinement variables that refine this slot. */ - private final Set refinedToSlots = new HashSet<>(); + private final Set refinedToSlots = new HashSet<>(); /** * Create a Slot with the given annotation location. @@ -53,7 +53,7 @@ public void setLocation(AnnotationLocation location) { this.location = location; } - public Set getRefinedToSlots() { + public Set getRefinedToSlots() { return refinedToSlots; } From 2e4ccc02c192592a850b20f345ec35986ace3ca0 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 4 Jun 2021 22:23:03 -0400 Subject: [PATCH 14/24] add test case --- .../ostrusted-inferrable-test/Comparison.java | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 testdata/ostrusted-inferrable-test/Comparison.java diff --git a/testdata/ostrusted-inferrable-test/Comparison.java b/testdata/ostrusted-inferrable-test/Comparison.java new file mode 100644 index 000000000..3168440a1 --- /dev/null +++ b/testdata/ostrusted-inferrable-test/Comparison.java @@ -0,0 +1,19 @@ +import ostrusted.qual.OsTrusted; +import ostrusted.qual.OsUntrusted; + +public class Comparison { + + void foo(@OsUntrusted Object o) { + if (o == null) { + bar(o); + } + } + + @OsTrusted + Object bar(Object o) { + // :: fixable-error: (return.type.incompatible) + return o; + } + +} + From 73690ea248239f04fec25ee17f3a82fb3cef8bb9 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 29 May 2021 21:40:03 -0400 Subject: [PATCH 15/24] add downstream value inference --- .ci-build.sh | 12 ++++++++++++ .github/workflows/main.yml | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/.ci-build.sh b/.ci-build.sh index fc000292e..aa49b9a4d 100755 --- a/.ci-build.sh +++ b/.ci-build.sh @@ -92,6 +92,18 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then clone_downstream $SECURITY_GIT $SECURITY_BRANCH test_downstream $SECURITY_GIT $SECURITY_COMMAND fi + + # Value inference test + if [[ "${GROUP}" == "downstream-value-inference" ]]; then + VALUE_GIT=value-inference + VALUE_BRANCH=master + VALUE_COMMAND="./gradlew build" + + ./gradlew testLibJar + + clone_downstream $VALUE_GIT $VALUE_BRANCH + test_downstream $VALUE_GIT $VALUE_COMMAND + fi fi echo Exiting "$(cd "$(dirname "$0")" && pwd -P)/$(basename "$0")" in `pwd` diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 358dfd47d..499026a7a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,7 @@ jobs: strategy: fail-fast: false matrix: - group: [ cfi-tests, downstream-ontology, downstream-security-demo ] + group: [ cfi-tests, downstream-value-inference ] jdk: [ 8, 11 ] runs-on: ubuntu-latest steps: From bb1653ca772af6f49c0f4717ef374c8ece92dfc6 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 4 Jun 2021 22:33:45 -0400 Subject: [PATCH 16/24] add units inference as downstreamOC --- .ci-build.sh | 12 ++++++++++++ .github/workflows/main.yml | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/.ci-build.sh b/.ci-build.sh index aa49b9a4d..b9260c775 100755 --- a/.ci-build.sh +++ b/.ci-build.sh @@ -104,6 +104,18 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then clone_downstream $VALUE_GIT $VALUE_BRANCH test_downstream $VALUE_GIT $VALUE_COMMAND fi + + # Unit inference test + if [[ "${GROUP}" == "downstream-units-inference" ]]; then + UNIT_GIT=units-inference + UNIT_BRANCH=master + UNIT_COMMAND="./gradlew build" + + ./gradlew testLibJar + + clone_downstream $UNIT_GIT $UNIT_BRANCH + test_downstream $UNIT_GIT $UNIT_COMMAND + fi fi echo Exiting "$(cd "$(dirname "$0")" && pwd -P)/$(basename "$0")" in `pwd` diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 499026a7a..b24ba2442 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,7 @@ jobs: strategy: fail-fast: false matrix: - group: [ cfi-tests, downstream-value-inference ] + group: [ cfi-tests, downstream-value-inference, downstream-units-inference ] jdk: [ 8, 11 ] runs-on: ubuntu-latest steps: From cfd51e90c4b58fed1a21a1f33d92404b419b7345 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 5 Jun 2021 23:41:31 -0400 Subject: [PATCH 17/24] some refactors about z3smt constraint encoder --- .../inference/model/ConstraintManager.java | 6 +- .../Z3SmtAbstractConstraintEncoder.java | 26 -------- .../encoder/Z3SmtSoftConstraintEncoder.java | 62 +++++++++++++------ 3 files changed, 47 insertions(+), 47 deletions(-) diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index d8b1dfc27..75d9f11bb 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -253,12 +253,12 @@ public void addComparableConstraint(Slot first, Slot second) { add(constraint); } } - + /** * Creates and adds a {@link ComparisonConstraint} between the two slots to the constraint set. */ - public void addComparsionConstraint(ComparisonOperationKind operation, Slot left, Slot right, - ComparisonVariableSlot result) { + public void addComparisonConstraint(ComparisonOperationKind operation, Slot left, Slot right, + ComparisonVariableSlot result) { add(createComparisonConstraint(operation, left, right, result)); } diff --git a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java index bedb79975..85cae0030 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java @@ -1,14 +1,5 @@ package checkers.inference.solver.backend.z3smt.encoder; -import checkers.inference.model.ArithmeticConstraint; -import checkers.inference.model.CombineConstraint; -import checkers.inference.model.ComparableConstraint; -import checkers.inference.model.EqualityConstraint; -import checkers.inference.model.ExistentialConstraint; -import checkers.inference.model.ImplicationConstraint; -import checkers.inference.model.InequalityConstraint; -import checkers.inference.model.PreferenceConstraint; -import checkers.inference.model.SubtypeConstraint; import checkers.inference.solver.backend.encoder.AbstractConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -39,21 +30,4 @@ public Z3SmtAbstractConstraintEncoder( this.z3SmtFormatTranslator = z3SmtFormatTranslator; } - protected abstract void encodeSubtypeConstraint(SubtypeConstraint constraint); - - protected abstract void encodeComparableConstraint(ComparableConstraint constraint); - - protected abstract void encodeArithmeticConstraint(ArithmeticConstraint constraint); - - protected abstract void encodeEqualityConstraint(EqualityConstraint constraint); - - protected abstract void encodeInequalityConstraint(InequalityConstraint constraint); - - protected abstract void encodeImplicationConstraint(ImplicationConstraint constraint); - - protected abstract void encodeExistentialConstraint(ExistentialConstraint constraint); - - protected abstract void encodeCombineConstraint(CombineConstraint constraint); - - protected abstract void encodePreferenceConstraint(PreferenceConstraint constraint); } diff --git a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java index f730b624f..444049445 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java @@ -2,6 +2,7 @@ import java.util.Collection; +import checkers.inference.model.ComparisonConstraint; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; @@ -34,44 +35,69 @@ public Z3SmtSoftConstraintEncoder( protected void addSoftConstraint(Expr serializedConstraint, int weight) { softConstraints.append("(assert-soft " + serializedConstraint + " :weight " + weight + ")\n"); } - + + + protected abstract void encodeSoftSubtypeConstraint(SubtypeConstraint constraint); + + protected abstract void encodeSoftComparableConstraint(ComparableConstraint constraint); + + protected abstract void encodeSoftComparisonConstraint(ComparisonConstraint constraint); + + protected abstract void encodeSoftArithmeticConstraint(ArithmeticConstraint constraint); + + protected abstract void encodeSoftEqualityConstraint(EqualityConstraint constraint); + + protected abstract void encodeSoftInequalityConstraint(InequalityConstraint constraint); + + protected abstract void encodeSoftImplicationConstraint(ImplicationConstraint constraint); + + protected abstract void encodeSoftExistentialConstraint(ExistentialConstraint constraint); + + protected abstract void encodeSoftCombineConstraint(CombineConstraint constraint); + + protected abstract void encodeSoftPreferenceConstraint(PreferenceConstraint constraint); + public String encodeAndGetSoftConstraints(Collection constraints) { for (Constraint constraint : constraints) { // Generate a soft constraint for subtype constraint if (constraint instanceof SubtypeConstraint) { - encodeSubtypeConstraint((SubtypeConstraint) constraint); + encodeSoftSubtypeConstraint((SubtypeConstraint) constraint); + } + // Generate soft constraint for comparable constraint + else if (constraint instanceof ComparableConstraint) { + encodeSoftComparableConstraint((ComparableConstraint) constraint); } // Generate soft constraint for comparison constraint - if (constraint instanceof ComparableConstraint) { - encodeComparableConstraint((ComparableConstraint) constraint); + else if (constraint instanceof ComparisonConstraint) { + encodeSoftComparisonConstraint((ComparisonConstraint) constraint); } // Generate soft constraint for arithmetic constraint - if (constraint instanceof ArithmeticConstraint) { - encodeArithmeticConstraint((ArithmeticConstraint) constraint); + else if (constraint instanceof ArithmeticConstraint) { + encodeSoftArithmeticConstraint((ArithmeticConstraint) constraint); } // Generate soft constraint for equality constraint - if (constraint instanceof EqualityConstraint) { - encodeEqualityConstraint((EqualityConstraint) constraint); + else if (constraint instanceof EqualityConstraint) { + encodeSoftEqualityConstraint((EqualityConstraint) constraint); } // Generate soft constraint for inequality constraint - if (constraint instanceof InequalityConstraint) { - encodeInequalityConstraint((InequalityConstraint) constraint); + else if (constraint instanceof InequalityConstraint) { + encodeSoftInequalityConstraint((InequalityConstraint) constraint); } // Generate soft constraint for implication constraint - if (constraint instanceof ImplicationConstraint) { - encodeImplicationConstraint((ImplicationConstraint) constraint); + else if (constraint instanceof ImplicationConstraint) { + encodeSoftImplicationConstraint((ImplicationConstraint) constraint); } // Generate soft constraint for existential constraint - if (constraint instanceof ExistentialConstraint) { - encodeExistentialConstraint((ExistentialConstraint) constraint); + else if (constraint instanceof ExistentialConstraint) { + encodeSoftExistentialConstraint((ExistentialConstraint) constraint); } // Generate soft constraint for combine constraint - if (constraint instanceof CombineConstraint) { - encodeCombineConstraint((CombineConstraint) constraint); + else if (constraint instanceof CombineConstraint) { + encodeSoftCombineConstraint((CombineConstraint) constraint); } // Generate soft constraint for preference constraint - if (constraint instanceof PreferenceConstraint) { - encodePreferenceConstraint((PreferenceConstraint) constraint); + else if (constraint instanceof PreferenceConstraint) { + encodeSoftPreferenceConstraint((PreferenceConstraint) constraint); } } return softConstraints.toString(); From 4bf14566321ef947ed58e806e4577d03b1312461 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 9 Jun 2021 22:58:45 -0400 Subject: [PATCH 18/24] fix bugs to pass value-inference --- .../solver/backend/AbstractFormatTranslator.java | 5 +++-- .../solver/backend/z3smt/Z3SmtFormatTranslator.java | 11 +++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 454e8f5e5..2443965dc 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -147,6 +147,7 @@ protected void finishInitializingEncoders() { equalityConstraintEncoder = encoderFactory.createEqualityConstraintEncoder(); inequalityConstraintEncoder = encoderFactory.createInequalityConstraintEncoder(); comparableConstraintEncoder = encoderFactory.createComparableConstraintEncoder(); + comparisonConstraintEncoder = encoderFactory.createComparisonConstraintEncoder(); preferenceConstraintEncoder = encoderFactory.createPreferenceConstraintEncoder(); combineConstraintEncoder = encoderFactory.createCombineConstraintEncoder(); existentialConstraintEncoder = encoderFactory.createExistentialConstraintEncoder(); @@ -188,7 +189,7 @@ public ConstraintEncodingT serialize(ComparableConstraint constraint) { @Override public ConstraintEncodingT serialize(ComparisonConstraint constraint) { - return comparableConstraintEncoder == null ? null : + return comparisonConstraintEncoder == null ? null : ConstraintEncoderCoordinator.dispatch(constraint, comparisonConstraintEncoder); } @@ -200,7 +201,7 @@ public ConstraintEncodingT serialize(PreferenceConstraint constraint) { @Override public ConstraintEncodingT serialize(CombineConstraint combineConstraint) { - return comparableConstraintEncoder == null ? null : + return combineConstraintEncoder == null ? null : ConstraintEncoderCoordinator.dispatch(combineConstraint, combineConstraintEncoder); } diff --git a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java index ac381799b..53c29204a 100644 --- a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java @@ -2,6 +2,7 @@ import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.LubVariableSlot; @@ -76,6 +77,16 @@ public SlotEncodingT serialize(LubVariableSlot slot) { return serializeVariableSlot(slot); } + @Override + public SlotEncodingT serialize(ArithmeticVariableSlot slot) { + return serializeVariableSlot(slot); + } + + @Override + public SlotEncodingT serialize(ComparisonVariableSlot slot) { + return serializeVariableSlot(slot); + } + /** * Subclasses can override this method to perform pre-analysis of slots for encoding * optimization From 26e89df1091049563476d129a0fb35949a659525 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 1 Sep 2021 16:44:10 -0400 Subject: [PATCH 19/24] fix compile-error --- src/checkers/inference/dataflow/InferenceTransfer.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 549d87682..04aa1b032 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -1,7 +1,6 @@ package checkers.inference.dataflow; import org.checkerframework.dataflow.analysis.ConditionalTransferResult; -import org.checkerframework.dataflow.analysis.FlowExpressions; import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; @@ -13,6 +12,7 @@ import org.checkerframework.dataflow.cfg.node.NotEqualNode; import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode; import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; +import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFTransfer; import org.checkerframework.framework.flow.CFValue; @@ -471,8 +471,8 @@ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot); // If node is assignment, iterate over lhs; otherwise, just node. - FlowExpressions.Receiver rec; - rec = FlowExpressions.internalReprOf(getInferenceAnalysis().getTypeFactory(), var); + JavaExpression rec; + rec = JavaExpression.fromNode(var); thenStore.clearValue(rec); thenStore.insertValue(rec, thenAm); elseStore.clearValue(rec); From 447ba2e01f4ba53a9528cda3146604a9023b387f Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 17 Dec 2021 07:41:01 -0500 Subject: [PATCH 20/24] config CI projects --- .ci-build.sh | 11 ----------- .github/workflows/main.yml | 2 +- 2 files changed, 1 insertion(+), 12 deletions(-) diff --git a/.ci-build.sh b/.ci-build.sh index b9260c775..049b0759b 100755 --- a/.ci-build.sh +++ b/.ci-build.sh @@ -105,17 +105,6 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then test_downstream $VALUE_GIT $VALUE_COMMAND fi - # Unit inference test - if [[ "${GROUP}" == "downstream-units-inference" ]]; then - UNIT_GIT=units-inference - UNIT_BRANCH=master - UNIT_COMMAND="./gradlew build" - - ./gradlew testLibJar - - clone_downstream $UNIT_GIT $UNIT_BRANCH - test_downstream $UNIT_GIT $UNIT_COMMAND - fi fi echo Exiting "$(cd "$(dirname "$0")" && pwd -P)/$(basename "$0")" in `pwd` diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b24ba2442..2f2b611b4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,7 @@ jobs: strategy: fail-fast: false matrix: - group: [ cfi-tests, downstream-value-inference, downstream-units-inference ] + group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-value-inference ] jdk: [ 8, 11 ] runs-on: ubuntu-latest steps: From 883eabc121fd5dbb8b072005c9ff75ffcacaa1c6 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 17 Dec 2021 11:16:31 -0500 Subject: [PATCH 21/24] encode ComparisonVariableSlot --- .../solver/backend/z3/Z3BitVectorFormatTranslator.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java index 68455c1f2..93fce04c5 100644 --- a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java @@ -7,6 +7,7 @@ import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; +import checkers.inference.model.ComparisonVariableSlot; import org.checkerframework.javacutil.BugInCF; import checkers.inference.solver.backend.AbstractFormatTranslator; @@ -153,6 +154,11 @@ public BitVecExpr serialize(ArithmeticVariableSlot slot) { return serializeVarSlot(slot); } + @Override + public BitVecExpr serialize(ComparisonVariableSlot slot) { + return serializeVarSlot(slot); + } + @Override public AnnotationMirror decodeSolution(BitVecNum solution, ProcessingEnvironment processingEnvironment) { return z3BitVectorCodec.decodeNumeralValue(solution.getBigInteger(), processingEnvironment); From 699c4f83d5a07b4778a84be76fc203bc0ba5d631 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 5 Feb 2022 22:41:57 -0500 Subject: [PATCH 22/24] add arithmetic kind for compound assignment --- .../inference/DefaultSlotManager.java | 9 +++----- src/checkers/inference/SlotManager.java | 2 +- .../inference/model/ArithmeticConstraint.java | 22 ++++++++++++++----- 3 files changed, 20 insertions(+), 13 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 4fc4b5290..f7eb38a3b 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -446,10 +446,7 @@ public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot, * @param rhsAtm atm of right operand * @return type kind of the arithmetic operation */ - private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) { - TypeMirror lhsType = lhsAtm.getUnderlyingType(); - TypeMirror rhsType = rhsAtm.getUnderlyingType(); - + private TypeKind getArithmeticResultKind(TypeMirror lhsType, TypeMirror rhsType) { assert (TypesUtils.isPrimitiveOrBoxed(lhsType) && TypesUtils.isPrimitiveOrBoxed(rhsType)); if (TypesUtils.isFloatingPoint(lhsType) || TypesUtils.isFloatingPoint(rhsType)) { @@ -466,7 +463,7 @@ private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTy @Override public ArithmeticVariableSlot createArithmeticVariableSlot( - AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) { + AnnotationLocation location, TypeMirror lhs, TypeMirror rhs) { if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { throw new BugInCF( "Cannot create an ArithmeticVariableSlot with a missing annotation location."); @@ -477,7 +474,7 @@ public ArithmeticVariableSlot createArithmeticVariableSlot( } // create the arithmetic var slot if it doesn't exist for the given location - TypeKind kind = getArithmeticResultKind(lhsAtm, rhsAtm); + TypeKind kind = getArithmeticResultKind(lhs, rhs); ArithmeticVariableSlot slot = new ArithmeticVariableSlot(nextId(), location, kind); addToSlots(slot); arithmeticSlotCache.put(location, slot.getId()); diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 629bf9af7..f6f4c217c 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -154,7 +154,7 @@ public interface SlotManager { * @return the ArithmeticVariableSlot for the given location */ ArithmeticVariableSlot createArithmeticVariableSlot( - AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm); + AnnotationLocation location, TypeMirror lhsType, TypeMirror rhsType); /** * Create new ComparisonVariableSlot at the given location and return a reference to it if no diff --git a/src/checkers/inference/model/ArithmeticConstraint.java b/src/checkers/inference/model/ArithmeticConstraint.java index 96fc6e3e5..d38c71794 100644 --- a/src/checkers/inference/model/ArithmeticConstraint.java +++ b/src/checkers/inference/model/ArithmeticConstraint.java @@ -46,17 +46,27 @@ public static ArithmeticOperationKind fromTreeKind(Kind kind) { case REMAINDER: return REMAINDER; case LEFT_SHIFT: - return LEFT_SHIFT; + return LEFT_SHIFT; case RIGHT_SHIFT: - return RIGHT_SHIFT; + return RIGHT_SHIFT; case UNSIGNED_RIGHT_SHIFT: - return UNSIGNED_RIGHT_SHIFT; + return UNSIGNED_RIGHT_SHIFT; case AND: - return AND; + return AND; case OR: - return OR; + return OR; case XOR: - return XOR; + return XOR; + case PLUS_ASSIGNMENT: + return PLUS; + case MINUS_ASSIGNMENT: + return MINUS; + case MULTIPLY_ASSIGNMENT: + return MULTIPLY; + case DIVIDE_ASSIGNMENT: + return DIVIDE; + case REMAINDER_ASSIGNMENT: + return REMAINDER; default: throw new BugInCF("There are no defined ArithmeticOperationKinds " + "for the given com.sun.source.tree.Tree.Kind: " + kind); From 898e2c245074e820fc5a301642891ecdae56f42d Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 6 Feb 2022 14:46:22 -0500 Subject: [PATCH 23/24] workaround for unsupported kinds of soft constraints --- .../z3smt/encoder/Z3SmtSoftConstraintEncoder.java | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java index 46a6ab525..9a9e64bc5 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java @@ -1,7 +1,9 @@ package checkers.inference.solver.backend.z3smt.encoder; import java.util.Collection; +import java.util.logging.Logger; +import checkers.inference.InferenceMain; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; @@ -16,6 +18,8 @@ public abstract class Z3SmtSoftConstraintEncoder extends Z3SmtAbstractConstraintEncoder { + private static final Logger logger = Logger.getLogger(Z3SmtSoftConstraintEncoder.class.getName()); + protected final StringBuilder softConstraints; public Z3SmtSoftConstraintEncoder( @@ -54,7 +58,11 @@ public String encodeAndGetSoftConstraints(Collection constraints) { encodeSoftInequalityConstraint((InequalityConstraint) constraint); } else { - throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + if (InferenceMain.isHackMode()) { + logger.warning("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + } else { + throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + } } } String res = softConstraints.toString(); From f224e14aab03f1b434b5fdf161efa335c933e6e1 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 6 Feb 2022 15:02:44 -0500 Subject: [PATCH 24/24] undo changes --- .../inference/DefaultSlotManager.java | 22 ------------------- src/checkers/inference/SlotManager.java | 14 ------------ src/checkers/inference/model/Serializer.java | 2 +- .../serialization/CnfVecIntSerializer.java | 2 +- .../serialization/ToStringSerializer.java | 2 +- .../backend/AbstractFormatTranslator.java | 4 ++-- .../encoder/ConstraintEncoderCoordinator.java | 2 +- .../encoder/ConstraintEncoderFactory.java | 2 +- .../LogiQLConstraintEncoderFactory.java | 2 +- .../MaxSATConstraintEncoderFactory.java | 2 +- .../Z3BitVectorConstraintEncoderFactory.java | 2 +- .../Z3SmtAbstractConstraintEncoder.java | 9 ++++++++ .../inference/solver/util/PrintUtils.java | 2 +- 13 files changed, 20 insertions(+), 47 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index f7eb38a3b..44e5df5b9 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -506,28 +506,6 @@ public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation lo return slot; } - @Override - public ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch) { - if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { - throw new BugInCF( - "ComparisonVariableSlot are never created with a missing annotation location."); - } - if (thenBranch) { - if (!comparisonThenSlotCache.containsKey(location)) { - return null; - } else { - return (ComparisonVariableSlot) getSlot(comparisonThenSlotCache.get(location)); - } - } else { - if (!comparisonElseSlotCache.containsKey(location)) { - return null; - } else { - return (ComparisonVariableSlot) getSlot(comparisonElseSlotCache.get(location)); - } - } - } - - @Override public AnnotationMirror createEquivalentVarAnno(AnnotationMirror realQualifier) { ConstantSlot varSlot = createConstantSlot(realQualifier); diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index f6f4c217c..e10e9e2fd 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -167,20 +167,6 @@ ArithmeticVariableSlot createArithmeticVariableSlot( */ ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch); - /** - * Retrieves the ComparisonVariableSlot created for the given location if it has been previously - * created, otherwise null is returned. - * - * This method allows faster retrieval of already created ComparisonVariableSlot during - * traversals of binary comparison trees in an InferenceTransfer subclass, which does not have direct access - * to the ATM containing this slot. - * - * @param location an AnnotationLocation used to locate this variable in code - * @param thenBranch true if is for the then store, false if is for the else store - * @return the ComparisonVariableSlot for the given location, or null if none exists - */ - ComparisonVariableSlot getComparisonVariableSlot(AnnotationLocation location, boolean thenBranch); - /** * Create a VarAnnot equivalent to the given realQualifier. * diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index e687aec03..4a318a198 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -43,7 +43,7 @@ public interface Serializer { S serialize(ArithmeticVariableSlot slot); T serialize(ComparableConstraint comparableConstraint); - + T serialize(ComparisonConstraint comparisonConstraint); T serialize(CombineConstraint combineConstraint); diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 50c273462..65ca0e6ae 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -271,7 +271,7 @@ public VecInt[] serialize(ComparableConstraint comparableConstraint) { // not sure what this means return emptyClauses; } - + @Override public VecInt[] serialize(ComparisonConstraint comparisonConstraint) { throw new UnsupportedOperationException( diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index c79111e0f..eddb8c6e2 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -196,7 +196,7 @@ public String serialize(ComparableConstraint constraint) { showVerboseVars = prevShowVerboseVars; return sb.toString(); } - + @Override public String serialize(ComparisonConstraint constraint) { boolean prevShowVerboseVars = showVerboseVars; diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 2cc9abde1..483bc55e4 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -102,7 +102,7 @@ public abstract class AbstractFormatTranslator comparableConstraintEncoder; - + /** * {@code ComparisonConstraintEncoder} to which encoding of {@link ComparableConstraint} is delegated. */ @@ -186,7 +186,7 @@ public ConstraintEncodingT serialize(ComparableConstraint constraint) { return comparableConstraintEncoder == null ? null : ConstraintEncoderCoordinator.dispatch(constraint, comparableConstraintEncoder); } - + @Override public ConstraintEncodingT serialize(ComparisonConstraint constraint) { return comparisonConstraintEncoder == null ? null : diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java index 075bb7341..9be1d5448 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java @@ -86,7 +86,7 @@ public static ConstraintEncodingT dispatch(CombineConstrai throw new BugInCF("Unsupported SlotSlotCombo enum."); } } - + public static ConstraintEncodingT dispatch( ComparisonConstraint constraint, ComparisonConstraintEncoder encoder) { diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java index 3c28727e7..1331348d4 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java @@ -41,7 +41,7 @@ public interface ConstraintEncoderFactory { InequalityConstraintEncoder createInequalityConstraintEncoder(); ComparableConstraintEncoder createComparableConstraintEncoder(); - + ComparisonConstraintEncoder createComparisonConstraintEncoder(); PreferenceConstraintEncoder createPreferenceConstraintEncoder(); diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java index e92e4a925..76990b819 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java @@ -44,7 +44,7 @@ public InequalityConstraintEncoder createInequalityConstraintEncoder() { public ComparableConstraintEncoder createComparableConstraintEncoder() { return new LogiQLComparableConstraintEncoder(lattice); } - + @Override public ComparisonConstraintEncoder createComparisonConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java index 09ff8b247..4564052cd 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java @@ -47,7 +47,7 @@ public MaxSATInequalityConstraintEncoder createInequalityConstraintEncoder() { public MaxSATComparableConstraintEncoder createComparableConstraintEncoder() { return new MaxSATComparableConstraintEncoder(lattice, typeToInt); } - + @Override public ComparisonConstraintEncoder createComparisonConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java index 9d42df3d9..03a494602 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java @@ -50,7 +50,7 @@ public InequalityConstraintEncoder createInequalityConstraintEncoder() public ComparableConstraintEncoder createComparableConstraintEncoder() { return null; } - + @Override public ComparisonConstraintEncoder createComparisonConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java index 85cae0030..49f226334 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java @@ -1,5 +1,14 @@ package checkers.inference.solver.backend.z3smt.encoder; +import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.CombineConstraint; +import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.EqualityConstraint; +import checkers.inference.model.ExistentialConstraint; +import checkers.inference.model.ImplicationConstraint; +import checkers.inference.model.InequalityConstraint; +import checkers.inference.model.PreferenceConstraint; +import checkers.inference.model.SubtypeConstraint; import checkers.inference.solver.backend.encoder.AbstractConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index 0558fd104..3c0aa7961 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -257,7 +257,7 @@ public Void serialize(ComparableConstraint constraint) { constraint.getSecond().serialize(this); return null; } - + @Override public Void serialize(ComparisonConstraint constraint) { constraint.getLeft().serialize(this);