| package org.checkerframework.dataflow.constantpropagation; |
| |
| import java.util.Objects; |
| import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.checkerframework.dataflow.analysis.AbstractValue; |
| |
| public class Constant implements AbstractValue<Constant> { |
| |
| /** What kind of abstract value is this? */ |
| protected Type type; |
| |
| /** The value of this abstract value (or null). */ |
| protected @Nullable Integer value; |
| |
| public enum Type { |
| CONSTANT, |
| TOP, |
| BOTTOM, |
| } |
| |
| /** Create a constant for {@code type}. */ |
| public Constant(Type type) { |
| assert type != Type.CONSTANT; |
| this.type = type; |
| } |
| |
| /** Create a constant for {@code value}. */ |
| public Constant(Integer value) { |
| this.type = Type.CONSTANT; |
| this.value = value; |
| } |
| |
| /** |
| * Returns whether or not the constant is TOP. |
| * |
| * @return whether or not the constant is TOP |
| */ |
| public boolean isTop() { |
| return type == Type.TOP; |
| } |
| |
| /** |
| * Returns whether or not the constant is BOTTOM. |
| * |
| * @return whether or not the constant is BOTTOM |
| */ |
| public boolean isBottom() { |
| return type == Type.BOTTOM; |
| } |
| |
| /** |
| * Returns whether or not the constant is CONSTANT. |
| * |
| * @return whether or not the constant is CONSTANT |
| */ |
| @EnsuresNonNullIf(result = true, expression = "value") |
| public boolean isConstant() { |
| return type == Type.CONSTANT && value != null; |
| } |
| |
| /** |
| * Returns the value. |
| * |
| * @return the value |
| */ |
| public Integer getValue() { |
| assert isConstant() : "@AssumeAssertion(nullness): inspection"; |
| return value; |
| } |
| |
| public Constant copy() { |
| if (isConstant()) { |
| return new Constant(value); |
| } |
| return new Constant(type); |
| } |
| |
| @Override |
| public Constant leastUpperBound(Constant other) { |
| if (other.isBottom()) { |
| return this.copy(); |
| } |
| if (this.isBottom()) { |
| return other.copy(); |
| } |
| if (other.isTop() || this.isTop()) { |
| return new Constant(Type.TOP); |
| } |
| if (other.getValue().equals(getValue())) { |
| return this.copy(); |
| } |
| return new Constant(Type.TOP); |
| } |
| |
| @Override |
| public boolean equals(@Nullable Object obj) { |
| if (!(obj instanceof Constant)) { |
| return false; |
| } |
| Constant other = (Constant) obj; |
| return type == other.type && Objects.equals(value, other.value); |
| } |
| |
| @Override |
| public int hashCode() { |
| return Objects.hash(type, value); |
| } |
| |
| @Override |
| public String toString() { |
| switch (type) { |
| case TOP: |
| return "T"; |
| case BOTTOM: |
| return "-"; |
| case CONSTANT: |
| assert isConstant() : "@AssumeAssertion(nullness)"; |
| return value.toString(); |
| default: |
| throw new Error("Unexpected type"); |
| } |
| } |
| } |