From 0b14f9114177033656f5f4c84624ea1a1664a48d Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Wed, 19 Aug 2020 07:15:39 -0400 Subject: [PATCH 1/5] fixed problems with the comparison constraints --- src/checkers/inference/DefaultSlotManager.java | 6 +++--- src/checkers/inference/SlotManager.java | 2 +- src/checkers/inference/dataflow/InferenceTransfer.java | 6 ++++++ src/checkers/inference/model/ComparisonVariableSlot.java | 9 ++++++++- .../solver/backend/AbstractFormatTranslator.java | 1 + .../solver/backend/z3/Z3BitVectorFormatTranslator.java | 6 ++++++ .../solver/backend/z3smt/Z3SmtFormatTranslator.java | 6 ++++++ .../z3smt/encoder/Z3SmtSoftConstraintEncoder.java | 9 ++++++++- 8 files changed, 39 insertions(+), 6 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 10ac4c9f3..0b7993010 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -451,7 +451,7 @@ public ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation locat } @Override - public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, boolean thenBranch) { + 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."); @@ -459,7 +459,7 @@ public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation lo // create the comparison var slot if it doesn't exist for the given location if (thenBranch && !comparisonThenSlotCache.containsKey(location)) { - ComparisonVariableSlot slot = new ComparisonVariableSlot(location, nextId()); + ComparisonVariableSlot slot = new ComparisonVariableSlot(location, nextId(), refined); addToSlots(slot); comparisonThenSlotCache.put(location, slot.getId()); return slot; @@ -467,7 +467,7 @@ public ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation lo // create the comparison var slot if it doesn't exist for the given location if (!thenBranch && !comparisonElseSlotCache.containsKey(location)) { - ComparisonVariableSlot slot = new ComparisonVariableSlot(location, nextId()); + ComparisonVariableSlot slot = new ComparisonVariableSlot(location, nextId(), refined); addToSlots(slot); comparisonElseSlotCache.put(location, slot.getId()); return slot; diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 726969cf7..b7dc497cf 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -153,7 +153,7 @@ public interface SlotManager { * @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, boolean thenBranch); + ComparisonVariableSlot createComparisonVariableSlot(AnnotationLocation location, Slot refined, boolean thenBranch); /** * Retrieves the ComparisonVariableSlot created for the given location if it has been previously diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 4c60102c0..892f0cd20 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -1,8 +1,10 @@ package checkers.inference.dataflow; +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.analysis.FlowExpressions.Receiver; import org.checkerframework.dataflow.cfg.node.AssignmentNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; @@ -14,13 +16,16 @@ import org.checkerframework.framework.flow.CFValue; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.Pair; import java.util.HashMap; import java.util.Map; +import java.util.Set; import java.util.logging.Logger; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; import com.sun.source.tree.CompoundAssignmentTree; @@ -36,6 +41,7 @@ import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; +import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceUtil; /** diff --git a/src/checkers/inference/model/ComparisonVariableSlot.java b/src/checkers/inference/model/ComparisonVariableSlot.java index d8c5f22d8..a0c9b54e6 100644 --- a/src/checkers/inference/model/ComparisonVariableSlot.java +++ b/src/checkers/inference/model/ComparisonVariableSlot.java @@ -9,8 +9,15 @@ */ public class ComparisonVariableSlot extends Slot { - public ComparisonVariableSlot(AnnotationLocation location, int id) { + private final Slot refined; + + public ComparisonVariableSlot(AnnotationLocation location, int id, Slot refined) { super(id, location); + this.refined = refined; + } + + public Slot getRefined() { + return refined; } @Override diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index d2af1b47f..f4f64736c 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -148,6 +148,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(); diff --git a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java index 30d09dde1..05aabe460 100644 --- a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java @@ -20,6 +20,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; @@ -156,6 +157,11 @@ public BitVecExpr serialize(LubVariableSlot slot) { 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) { diff --git a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java index badd15495..a3d7c2923 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; @@ -77,6 +78,11 @@ public SlotEncodingT serialize(LubVariableSlot slot) { public SlotEncodingT serialize(ArithmeticVariableSlot slot) { return serializeVarSlot(slot); } + + @Override + public SlotEncodingT serialize(ComparisonVariableSlot slot) { + return serializeVarSlot(slot); + } /** * Subclasses can override this method to perform pre-analysis of slots for encoding diff --git a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java index 96f215cba..6714933f9 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java @@ -8,6 +8,7 @@ import checkers.inference.model.ArithmeticConstraint; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.ComparisonConstraint; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; @@ -52,6 +53,8 @@ public Z3SmtSoftConstraintEncoder( protected abstract void encodeSoftComparableConstraint(ComparableConstraint constraint); + protected abstract void encodeSoftComparisonConstraint(ComparisonConstraint constraint); + protected abstract void encodeSoftArithmeticConstraint(ArithmeticConstraint constraint); protected abstract void encodeSoftEqualityConstraint(EqualityConstraint constraint); @@ -76,10 +79,14 @@ public String encodeAndGetSoftConstraints(Collection constraints) { if (constraint instanceof SubtypeConstraint) { encodeSoftSubtypeConstraint((SubtypeConstraint) constraint); } - // Generate soft constraint for comparison constraint + // Generate soft constraint for comparable constraint if (constraint instanceof ComparableConstraint) { encodeSoftComparableConstraint((ComparableConstraint) constraint); } + // Generate soft constraint for comparison constraint + if (constraint instanceof ComparisonConstraint) { + encodeSoftComparisonConstraint((ComparisonConstraint) constraint); + } // Generate soft constraint for arithmetic constraint if (constraint instanceof ArithmeticConstraint) { encodeSoftArithmeticConstraint((ArithmeticConstraint) constraint); From 0191dd17b021c71f4833b88be77544db8555ddb8 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 25 Aug 2020 14:24:25 -0400 Subject: [PATCH 2/5] hacks --- src/checkers/inference/InferenceVisitor.java | 7 ++++--- src/checkers/inference/VariableAnnotator.java | 3 +++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index 2914c6f01..0ddeed9ba 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/src/checkers/inference/InferenceVisitor.java @@ -658,9 +658,10 @@ public boolean maybeAddRefinementVariableConstraints(final AnnotatedTypeMirror v Slot sub = slotManager.getVariableSlot(upperBound); logger.fine("InferenceVisitor::commonAssignmentCheck: Equality constraint for qualifiers sub: " + sub + " sup: " + sup); - - // Equality between the refvar and the value - constraintManager.addEqualityConstraint(sup, sub); + if (sub != null) { + // Equality between the refvar and the value + constraintManager.addEqualityConstraint(sup, sub); + } // Refinement variable still needs to be a subtype of its declared type value constraintManager.addSubtypeConstraint(sup, ((RefinementVariableSlot) sup).getRefined()); diff --git a/src/checkers/inference/VariableAnnotator.java b/src/checkers/inference/VariableAnnotator.java index 4a19a51fc..a408d88f5 100644 --- a/src/checkers/inference/VariableAnnotator.java +++ b/src/checkers/inference/VariableAnnotator.java @@ -1017,6 +1017,9 @@ public boolean enclosedByAnnotation(TreePath path) { treeKinds.add(Kind.METHOD); treeKinds.add(Kind.CLASS); Tree enclosure = TreeUtils.enclosingOfKind(path, treeKinds); + if (enclosure == null) { + return false; + } return enclosure.getKind() == Kind.ANNOTATION || enclosure.getKind() == Kind.ANNOTATION_TYPE || enclosure.getKind() == Kind.TYPE_ANNOTATION; From 5132e8778894a6230c70bc7dab4727981772f157 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 1 Sep 2020 00:48:45 -0400 Subject: [PATCH 3/5] add hacks to fix poly problem --- src/checkers/inference/DefaultSlotManager.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 0b7993010..009cd25f5 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -349,7 +349,12 @@ public RefinementVariableSlot createRefinementVariableSlot(AnnotationLocation lo addToSlots(refinementVariableSlot); } else if (locationCache.containsKey(location)) { int id = locationCache.get(location); - refinementVariableSlot = (RefinementVariableSlot) getSlot(id); + if (getSlot(id) instanceof RefinementVariableSlot) { + refinementVariableSlot = (RefinementVariableSlot) getSlot(id); + } else { + refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined); + addToSlots(refinementVariableSlot); + } } else { refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined); addToSlots(refinementVariableSlot); From 162066fca2892c6e6b141fb97570d18d6a5a481d Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Wed, 2 Sep 2020 11:23:05 -0400 Subject: [PATCH 4/5] add hacks to avoid null pointer exceptions --- src/checkers/inference/InferenceQualifierHierarchy.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/checkers/inference/InferenceQualifierHierarchy.java b/src/checkers/inference/InferenceQualifierHierarchy.java index 5d0f535bd..1a46fb90d 100644 --- a/src/checkers/inference/InferenceQualifierHierarchy.java +++ b/src/checkers/inference/InferenceQualifierHierarchy.java @@ -221,6 +221,11 @@ public boolean isSubtype(final AnnotationMirror subtype, final AnnotationMirror final Slot subSlot = slotMgr.getSlot(subtype); final Slot superSlot = slotMgr.getSlot(supertype); + + // TODO: remove hack + if (subSlot == null || superSlot == null) { + return true; + } return constraintMgr.addSubtypeConstraintNoErrorMsg(subSlot, superSlot); } From 87514a1ff81bf95c7200787234779eb4a3c6cced Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Thu, 10 Sep 2020 06:23:06 -0400 Subject: [PATCH 5/5] fix refinement to get declared instead of comparison slot --- src/checkers/inference/DefaultSlotManager.java | 3 +++ src/checkers/inference/dataflow/InferenceTransfer.java | 10 ++++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 009cd25f5..c9017d271 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -245,6 +245,9 @@ public Slot getVariableSlot( final AnnotatedTypeMirror atm ) { */ @Override public Slot getSlot( final AnnotationMirror annotationMirror ) { + if (annotationMirror == null) { + return null; + } final int id; if (InferenceQualifierHierarchy.isVarAnnot(annotationMirror)) { diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 892f0cd20..0f1d8b5c3 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -38,6 +38,7 @@ import checkers.inference.SlotManager; import checkers.inference.VariableAnnotator; import checkers.inference.model.AnnotationLocation; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; @@ -207,8 +208,13 @@ private TransferResult createRefinementVar(Node lhs, AnnotatedTypeMirror atm) { Slot slotToRefine = getInferenceAnalysis().getSlotManager().getVariableSlot(atm); - while (slotToRefine instanceof RefinementVariableSlot) { - slotToRefine = ((RefinementVariableSlot)slotToRefine).getRefined(); + while (slotToRefine instanceof RefinementVariableSlot + || slotToRefine instanceof ComparisonVariableSlot) { + if (slotToRefine instanceof RefinementVariableSlot) { + slotToRefine = ((RefinementVariableSlot)slotToRefine).getRefined(); + } else if (slotToRefine instanceof ComparisonVariableSlot) { + slotToRefine = ((ComparisonVariableSlot)slotToRefine).getRefined(); + } } logger.fine("Creating refinement variable for tree: " + assignmentTree);