| package org.checkerframework.checker.nullness; |
| |
| import java.util.concurrent.atomic.AtomicLong; |
| import org.checkerframework.checker.initialization.InitializationStore; |
| import org.checkerframework.checker.nullness.qual.NonNull; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.checkerframework.checker.nullness.qual.PolyNull; |
| import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; |
| import org.checkerframework.framework.flow.CFAbstractAnalysis; |
| import org.checkerframework.framework.flow.CFAbstractStore; |
| import org.plumelib.util.UniqueId; |
| |
| /** |
| * Behaves like {@link InitializationStore}, but additionally tracks whether {@link PolyNull} is |
| * known to be {@link NonNull} or {@link Nullable} (or not known to be either). |
| */ |
| public class NullnessStore extends InitializationStore<NullnessValue, NullnessStore> |
| implements UniqueId { |
| |
| /** True if, at this point, {@link PolyNull} is known to be {@link NonNull}. */ |
| protected boolean isPolyNullNonNull; |
| |
| /** True if, at this point, {@link PolyNull} is known to be {@link Nullable}. */ |
| protected boolean isPolyNullNull; |
| |
| /** The unique ID for the next-created object. */ |
| static final AtomicLong nextUid = new AtomicLong(0); |
| /** The unique ID of this object. */ |
| final long uid = nextUid.getAndIncrement(); |
| /** |
| * Returns the unique ID of this object. |
| * |
| * @return the unique ID of this object |
| */ |
| @Override |
| public long getUid() { |
| return uid; |
| } |
| |
| /** |
| * Create a NullnessStore. |
| * |
| * @param analysis the analysis class this store belongs to |
| * @param sequentialSemantics should the analysis use sequential Java semantics (i.e., assume that |
| * only one thread is running at all times)? |
| */ |
| public NullnessStore( |
| CFAbstractAnalysis<NullnessValue, NullnessStore, ?> analysis, boolean sequentialSemantics) { |
| super(analysis, sequentialSemantics); |
| isPolyNullNonNull = false; |
| isPolyNullNull = false; |
| } |
| |
| /** |
| * Create a NullnessStore (copy constructor). |
| * |
| * @param s a store to copy |
| */ |
| public NullnessStore(NullnessStore s) { |
| super(s); |
| isPolyNullNonNull = s.isPolyNullNonNull; |
| isPolyNullNull = s.isPolyNullNull; |
| } |
| |
| @Override |
| public NullnessStore leastUpperBound(NullnessStore other) { |
| NullnessStore lub = super.leastUpperBound(other); |
| lub.isPolyNullNonNull = isPolyNullNonNull && other.isPolyNullNonNull; |
| lub.isPolyNullNull = isPolyNullNull && other.isPolyNullNull; |
| return lub; |
| } |
| |
| @Override |
| protected boolean supersetOf(CFAbstractStore<NullnessValue, NullnessStore> o) { |
| if (!(o instanceof InitializationStore)) { |
| return false; |
| } |
| NullnessStore other = (NullnessStore) o; |
| if ((other.isPolyNullNonNull != isPolyNullNonNull) |
| || (other.isPolyNullNull != isPolyNullNull)) { |
| return false; |
| } |
| return super.supersetOf(other); |
| } |
| |
| @Override |
| protected String internalVisualize(CFGVisualizer<NullnessValue, NullnessStore, ?> viz) { |
| return super.internalVisualize(viz) |
| + viz.getSeparator() |
| + viz.visualizeStoreKeyVal("isPolyNullNonNull", isPolyNullNonNull) |
| + viz.getSeparator() |
| + viz.visualizeStoreKeyVal("isPolyNullNull", isPolyNullNull); |
| } |
| |
| /** |
| * Returns true if, at this point, {@link PolyNull} is known to be {@link NonNull}. |
| * |
| * @return true if, at this point, {@link PolyNull} is known to be {@link NonNull} |
| */ |
| public boolean isPolyNullNonNull() { |
| return isPolyNullNonNull; |
| } |
| |
| /** |
| * Set the value of whether, at this point, {@link PolyNull} is known to be {@link NonNull}. |
| * |
| * @param isPolyNullNonNull whether, at this point, {@link PolyNull} is known to be {@link |
| * NonNull} |
| */ |
| public void setPolyNullNonNull(boolean isPolyNullNonNull) { |
| this.isPolyNullNonNull = isPolyNullNonNull; |
| } |
| |
| /** |
| * Returns true if, at this point, {@link PolyNull} is known to be {@link Nullable}. |
| * |
| * @return true if, at this point, {@link PolyNull} is known to be {@link Nullable} |
| */ |
| public boolean isPolyNullNull() { |
| return isPolyNullNull; |
| } |
| |
| /** |
| * Set the value of whether, at this point, {@link PolyNull} is known to be {@link Nullable}. |
| * |
| * @param isPolyNullNull whether, at this point, {@link PolyNull} is known to be {@link Nullable} |
| */ |
| public void setPolyNullNull(boolean isPolyNullNull) { |
| this.isPolyNullNull = isPolyNullNull; |
| } |
| } |