001package daikon.inv;
002
003import daikon.Global;
004import daikon.PptSlice;
005import daikon.PptTopLevel;
006import daikon.VarInfo;
007import java.util.ArrayList;
008import java.util.List;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import org.checkerframework.checker.nullness.qual.Nullable;
011import org.checkerframework.dataflow.qual.Pure;
012import org.checkerframework.dataflow.qual.SideEffectFree;
013import typequals.prototype.qual.NonPrototype;
014import typequals.prototype.qual.Prototype;
015
016/**
017 * This is a special invariant used internally by Daikon to represent an antecedent invariant in an
018 * implication where that antecedent consists of two invariants anded together.
019 */
020public class AndJoiner extends Joiner {
021  static final long serialVersionUID = 20030822L;
022
023  public AndJoiner(PptTopLevel ppt, Invariant left, Invariant right) {
024    super(ppt, left, right);
025  }
026
027  @Override
028  protected double computeConfidence() {
029    return Invariant.confidence_and(left.computeConfidence(), right.computeConfidence());
030  }
031
032  @Override
033  public String repr(@GuardSatisfied AndJoiner this) {
034    return "[" + left.repr() + " and " + right.repr() + "]";
035  }
036
037  @SideEffectFree
038  @Override
039  public String format_using(@GuardSatisfied AndJoiner this, OutputFormat format) {
040    List<Invariant> invs = conjuncts();
041    List<String> invStrings = new ArrayList<>(invs.size());
042    for (Invariant inv : invs) {
043      invStrings.add(inv.format_using(format));
044    }
045    if (format == OutputFormat.DAIKON) {
046      return String.join(" and ", invStrings);
047    } else if (format == OutputFormat.ESCJAVA
048        || format.isJavaFamily()
049        || format == OutputFormat.CSHARPCONTRACT) {
050      // Forrest
051      return "(" + String.join(") && (", invStrings) + ")";
052    } else if (format == OutputFormat.SIMPLIFY) {
053      return "(AND" + String.join(" ", invStrings) + ")";
054    } else {
055      return format_unimplemented(format);
056    }
057  }
058
059  public List<Invariant> conjuncts(@GuardSatisfied AndJoiner this) {
060    List<Invariant> result = new ArrayList<>(2);
061    if (left instanceof AndJoiner) {
062      result.addAll(((AndJoiner) left).conjuncts());
063    } else {
064      result.add(left);
065    }
066    if (right instanceof AndJoiner) {
067      result.addAll(((AndJoiner) right).conjuncts());
068    } else {
069      result.add(right);
070    }
071    return result;
072  }
073
074  @Pure
075  @Override
076  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
077    // Don't call super.isObviousDynamically(vis);
078
079    DiscardInfo leftObvious = left.isObviousDynamically(vis);
080    DiscardInfo rightObvious = right.isObviousDynamically(vis);
081    if (leftObvious != null && rightObvious != null) {
082      return new DiscardInfo(
083          this,
084          DiscardCode.obvious,
085          "Left obvious: "
086              + leftObvious.discardString()
087              + Global.lineSep
088              + "Right obvious: "
089              + rightObvious.discardString());
090    }
091    return null;
092  }
093
094  @Pure
095  @Override
096  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
097    DiscardInfo leftObvious = left.isObviousStatically(vis);
098    DiscardInfo rightObvious = right.isObviousStatically(vis);
099    if (leftObvious != null && rightObvious != null) {
100      DiscardInfo result =
101          new DiscardInfo(
102              this,
103              DiscardCode.obvious,
104              "Left obvious: "
105                  + leftObvious.discardString()
106                  + Global.lineSep
107                  + "Right obvious: "
108                  + rightObvious.discardString());
109      return result;
110    } else {
111      return null;
112    }
113  }
114
115  @Pure
116  @Override
117  public boolean isSameInvariant(Invariant other) {
118    return super.isSameInvariant(other);
119  }
120
121  @Override
122  public boolean enabled(@Prototype AndJoiner this) {
123    throw new Error("do not invoke " + getClass() + ".enabled()");
124  }
125
126  @Override
127  public boolean valid_types(@Prototype AndJoiner this, VarInfo[] vis) {
128    throw new Error("do not invoke " + getClass() + ".valid_types()");
129  }
130
131  @Override
132  protected @NonPrototype AndJoiner instantiate_dyn(@Prototype AndJoiner this, PptSlice slice) {
133    throw new Error("do not invoke " + getClass() + ".instantiate_dyn()");
134  }
135}