001 package daikon.inv;
002
003 import daikon.*;
004
005 import java.util.logging.Logger;
006 import java.util.logging.Level;
007
008 import utilMDE.*;
009
010 // Here Implication is reimplemented as an extension of the new general
011 // Joiner class
012
013 /**
014 * The Implication invariant class is used internally within Daikon to
015 * handle invariants that are only true when certain other conditions are
016 * also true (splitting).
017 **/
018 public class Implication
019 extends Joiner
020 {
021 // We are Serializable, so we specify a version to allow changes to
022 // method signatures without breaking serialization. If you add or
023 // remove fields, you should change this number to the current date.
024 static final long serialVersionUID = 20030822L;
025
026 // These can be null (for instance, for GuardingImplication). What
027 // exactly is the representation invariant: should they never be null?
028 /** The original predicate invariant from its original conditional ppt. */
029 private Invariant orig_left;
030 /** The original consequent invariant from its original conditional ppt. */
031 private Invariant orig_right;
032
033 public Invariant predicate() { return left; }
034 public Invariant consequent() { return right; }
035 public boolean iff;
036
037 protected Implication(PptSlice ppt, Invariant predicate, Invariant consequent,
038 boolean iff, Invariant orig_predicate, Invariant orig_consequent) {
039 super(ppt, predicate, consequent);
040 assert(predicate != null);
041 assert(consequent != null);
042 this.iff = iff;
043 this.orig_left = orig_predicate;
044 this.orig_right = orig_consequent;
045 }
046
047 /**
048 * Creates a new Implication Invariant from the predicate,
049 * consequent and the boolean iff and adds it to the PptTopLevel.
050 *
051 * @return null if predicate and the consequent are the same, or if
052 * the PptTopLevel already contains this Implication.
053 **/
054 public static /*@Nullable*/ Implication makeImplication(PptTopLevel ppt,
055 Invariant predicate,
056 Invariant consequent,
057 boolean iff,
058 Invariant orig_predicate,
059 Invariant orig_consequent) {
060 if (predicate.isSameInvariant(consequent)) {
061 PptSplitter.debug.fine ("Not creating implication (pred==conseq): " + predicate +
062 " ==> " + consequent);
063 return null;
064 }
065
066 Implication result = new Implication(ppt.joiner_view, predicate, consequent, iff,
067 orig_predicate, orig_consequent);
068
069 // Don't add this Implication to the program point if the program
070 // point already has this implication.
071 if (ppt.joiner_view.hasImplication(result)) {
072 return null;
073 }
074
075 if (PptSplitter.debug.isLoggable (Level.FINE))
076 PptSplitter.debug.fine ("Creating implication " + predicate + " ==> "
077 + consequent);
078 return result;
079 }
080
081 protected double computeConfidence() {
082 double pred_conf = orig_left.computeConfidence();
083 double cons_conf = orig_right.computeConfidence();
084 if ((pred_conf == CONFIDENCE_NEVER)
085 || (cons_conf == CONFIDENCE_NEVER)) {
086 return CONFIDENCE_NEVER;
087 }
088 double result = confidence_and(pred_conf, cons_conf);
089 log ("Confidence " + result + " " + pred_conf + "/"
090 + cons_conf + " for " + format());
091 return result;
092 }
093
094 public String repr() {
095 return "[Implication: " + left.repr()
096 + " => " + right.repr() + "]";
097 }
098
099 public String format_using(OutputFormat format) {
100 String pred_fmt = left.format_using(format);
101 String consq_fmt = right.format_using(format);
102 if (format == OutputFormat.DAIKON || format == OutputFormat.JML) {
103 String arrow = (iff ? " <==> " : " ==> "); // "interned"
104 return "(" + pred_fmt + ")" + arrow + "(" + consq_fmt + ")";
105 } else if (format == OutputFormat.ESCJAVA) {
106 String arrow = (iff ? " == " : " ==> "); // "interned"
107 return "(" + pred_fmt + ")" + arrow + "(" + consq_fmt + ")";
108 } else if (format == OutputFormat.JAVA) {
109 String mid = (iff ? " == " : " || !"); // "interned"
110 return "(" + consq_fmt + ")" + mid + "(" + pred_fmt + ")";
111 } else if (format == OutputFormat.SIMPLIFY) {
112 String cmp = (iff ? "IFF" : "IMPLIES");
113 return "(" + cmp + " " + pred_fmt + " " + consq_fmt + ")";
114 } else if (format == OutputFormat.DBCJAVA) {
115 if ( iff )
116 return "((" + pred_fmt + ") == (" + consq_fmt + "))";
117 else
118 return "(" + pred_fmt + " $implies " + consq_fmt + ")";
119 } else {
120 return format_unimplemented(format);
121 }
122 }
123
124 public /*@Nullable*/ DiscardInfo isObviousStatically(VarInfo[] vis) {
125 assert vis.length > 0;
126 for (int ii = 0; ii < vis.length; ii++ )
127 assert vis[ii] != null;
128 return orig_right.isObviousStatically(vis);
129 }
130
131 public /*@Nullable*/ DiscardInfo isObviousDynamically (VarInfo[] vis) {
132 assert vis.length > 0;
133 for (int ii = 0; ii < vis.length; ii++ )
134 assert vis[ii] != null;
135 DiscardInfo di = orig_right.isObviousDynamically (vis);
136 if (di != null) {
137 log ("failed isObviousDynamically with vis = " + VarInfo.toString (vis));
138 return (di);
139 }
140
141 return (null);
142 }
143
144
145 /**
146 * Return true if the right side of the implication and some
147 * equality combinations of its member variables are statically
148 * obvious. For example, if a == b, and f(a) is obvious, then so is
149 * f(b). We use the someInEquality (or least interesting) method
150 * during printing so we only print an invariant if all its
151 * variables are interesting, since a single, static, non
152 * interesting occurance means all the equality combinations aren't
153 * interesting.
154 *
155 * This must be overridden for Implication because the right side is
156 * the invariant of interest. The standard version passes the vis
157 * from the slice containing the implication itself (slice 0).
158 **/
159 public /*@Nullable*/ DiscardInfo isObviousStatically_SomeInEquality() {
160 return orig_right.isObviousStatically_SomeInEquality();
161 // DiscardInfo result = isObviousStatically (orig_right.ppt.var_infos);
162 // if (result != null) return result;
163 // assert orig_right.ppt.var_infos.length > 0;
164 // for (int ii = 0; ii < orig_right.ppt.var_infos.length; ii++ )
165 // assert orig_right.ppt.var_infos[ii] != null;
166 // return isObviousStatically_SomeInEqualityHelper (orig_right.ppt.var_infos,
167 // new VarInfo[orig_right.ppt.var_infos.length], 0);
168 }
169
170 /**
171 * Return true if the rightr side of the implication some equality
172 * combinations of its member variables are dynamically obvious.
173 * For example, a == b, and f(a) is obvious, so is f(b). We use the
174 * someInEquality (or least interesting) method during printing so
175 * we only print an invariant if all its variables are interesting,
176 * since a single, dynamic, non interesting occurance means all the
177 * equality combinations aren't interesting.
178 *
179 * This must be overridden for Implication because the right side is
180 * the invariant of interest. The standard version passes the vis
181 * from the slice containing the implication itself (slice 0).
182 **/
183 public /*@Nullable*/ DiscardInfo isObviousDynamically_SomeInEquality() {
184
185 // If the consequent is ni-suppressed in its original program point,
186 // then it is obvious from some set of other invariants. Those invariants
187 // could be other implications or they could be true at both conditional
188 // points.
189 // JHP: Seemingly it would be better if this invariant was never
190 // created, but somehow that creates other implications. See the
191 // disabled code in PptSplitter.add_implication()
192 if (orig_right.is_ni_suppressed())
193 return (new DiscardInfo (this, DiscardCode.obvious, "consequent "
194 + orig_right.format() + " is ni suppressed"));
195
196 return orig_right.isObviousDynamically_SomeInEquality();
197 // DiscardInfo result = isObviousDynamically (orig_right.ppt.var_infos);
198 // if (result != null)
199 // return result;
200 // return isObviousDynamically_SomeInEqualityHelper (orig_right.ppt.var_infos,
201 // new VarInfo[right.ppt.var_infos.length], 0);
202 }
203
204 public boolean isSameFormula(Invariant other) {
205 Implication other_implic = (Implication)other;
206 return ((iff == other_implic.iff)
207 && super.isSameFormula(other_implic));
208 }
209
210 public boolean isSameInvariant(Invariant other) {
211 if (other == null)
212 return false;
213 if (! (other instanceof Implication))
214 return false;
215 if (iff != ((Implication)other).iff)
216 return false;
217 return super.isSameInvariant(other);
218 }
219
220 // An implication is only interesting if both the predicate and
221 // consequent are interesting
222 public boolean isInteresting() {
223 return (predicate().isInteresting() && consequent().isInteresting());
224 }
225
226 // If a constant managed to appear in a predicate, that's
227 // interesting enough for us.
228 public boolean hasUninterestingConstant() {
229 return consequent().hasUninterestingConstant();
230 }
231
232 public boolean isAllPrestate() {
233 return predicate().isAllPrestate() && consequent().isAllPrestate();
234 }
235
236 /**
237 * Logs a description of the invariant and the specified msg via the
238 * logger as described in {@link daikon.Debug#log(Logger, Class, Ppt,
239 * VarInfo[], String)}. Uses the consequent as the logger
240 */
241
242 public void log (Logger log, String msg) {
243
244 right.log (log, msg + "[for implication " + format() + " ("
245 + (orig_right == null ? "null" : orig_right.format()) + ")]");
246 }
247
248
249 /**
250 * Logs a description of the invariant and the specified msg via the
251 * logger as described in {@link daikon.Debug#log(Logger, Class, Ppt,
252 * VarInfo[], String)}. Uses the consequent as the logger
253 *
254 * @return whether or not it logged anything
255 */
256
257 public boolean log (String msg) {
258
259 return (right.log (msg + "[for implication " + format() + " ("
260 + (orig_right == null ? "null" : orig_right.format()) + ")]"));
261 }
262
263
264 }