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}