001 package daikon.inv;
002
003 import daikon.*;
004 import java.util.HashSet;
005 import java.util.Iterator;
006
007 /**
008 * This is a special invariant used internally by Daikon to represent
009 * invariants whose meaning Daikon doesn't understand. The only
010 * operation that can be performed on a DummyInvariant is to print it.
011 * For instance, dummy invariants can be created to correspond to
012 * splitting conditions, when no other invariant in Daikon's grammar
013 * is equivalent to the condition.
014 *
015 * To use dummy invariants for splitting conditions, the configuration
016 * option <samp>daikon.PptTopLevel.dummy_invariant_level</samp> must be set,
017 * and formatting information must be supplied in the splitter info file.
018 **/
019 public class DummyInvariant
020 extends Invariant
021 {
022 // We are Serializable, so we specify a version to allow changes to
023 // method signatures without breaking serialization. If you add or
024 // remove fields, you should change this number to the current date.
025 static final long serialVersionUID = 20030220L;
026
027 private String daikonFormat;
028 private String javaFormat;
029 private String escFormat;
030 private String simplifyFormat;
031 private String jmlFormat;
032 private String dbcFormat;
033
034 private boolean negated = false;
035
036 // Pre-instatiate(), set to true if we have reason to believe the user
037 // explicitly wanted this invariant to appear in the output.
038 // After instantiation, also requires that we've found an appropriate
039 // slice for the invariant to live in.
040 public boolean valid = false;
041
042 public DummyInvariant(/*@Dependent(result=Nullable.class, when=Prototype.class)*/ PptSlice ppt) {
043 super(ppt);
044 }
045
046 public void setFormats(/*@Nullable*/ String daikonStr, /*@Nullable*/ String java, /*@Nullable*/ String esc,
047 /*@Nullable*/ String simplify, /*@Nullable*/ String jml,
048 /*@Nullable*/ String dbc, boolean desired) {
049 if (daikonStr != null)
050 daikonFormat = daikonStr;
051 if (java != null)
052 javaFormat = java;
053 if (esc != null)
054 escFormat = esc;
055 if (simplify != null)
056 simplifyFormat = simplify;
057 if (jml != null)
058 jmlFormat = jml;
059 if (dbc != null)
060 dbcFormat = dbc;
061
062 valid |= desired;
063 }
064
065 public DummyInvariant instantiate(PptTopLevel parent, VarInfo[] vars) {
066 DummyInvariant inv = new DummyInvariant(ppt);
067 inv.daikonFormat = this.daikonFormat;
068 inv.javaFormat = this.javaFormat;
069 inv.escFormat = this.escFormat;
070 inv.simplifyFormat = this.simplifyFormat;
071 inv.valid = false; // Not valid until we find a slice for it
072 assert !this.negated
073 : "Only instantiated invariants should be negated";
074
075 // Find between 1 and 3 unique variables, to pick a slice to put
076 // this in.
077 HashSet<VarInfo> uniqVarsSet = new HashSet<VarInfo>();
078 for (int i = 0; i < vars.length; i++)
079 uniqVarsSet.add(vars[i].canonicalRep());
080 int sliceSize = uniqVarsSet.size();
081 if (sliceSize > 3)
082 sliceSize = 3;
083 VarInfo[] newVars = new VarInfo[sliceSize];
084 {
085 Iterator<VarInfo> it = uniqVarsSet.iterator();
086 int i = 0;
087 while (it.hasNext()) {
088 newVars[i++] = it.next();
089 if (i == sliceSize)
090 break;
091 }
092 }
093 vars = newVars;
094 assert vars.length >= 1 && vars.length <= 3;
095 if (vars.length == 1) {
096 PptSlice1 slice = parent.findSlice(vars[0]);
097 if (slice == null) {
098 slice = new PptSlice1(parent, vars);
099 parent.addSlice(slice);
100 }
101 inv.ppt = slice;
102 } else if (vars.length == 2) {
103 if (vars[0] == vars[1])
104 return inv;
105 else if (vars[0].varinfo_index > vars[1].varinfo_index) {
106 VarInfo tmp = vars[0];
107 vars[0] = vars[1];
108 vars[1] = tmp;
109 }
110 PptSlice2 slice = parent.findSlice(vars[0], vars[1]);
111 if (slice == null) {
112 slice = new PptSlice2(parent, vars);
113 parent.addSlice(slice);
114 }
115 inv.ppt = slice;
116 } else if (vars.length == 3) {
117 if (vars[0] == vars[1] || vars[1] == vars[2] || vars[0] == vars[2])
118 return inv;
119 // bubble sort
120 VarInfo tmp;
121 if (vars[0].varinfo_index > vars[1].varinfo_index) {
122 tmp = vars[0]; vars[0] = vars[1]; vars[1] = tmp;
123 }
124 if (vars[1].varinfo_index > vars[2].varinfo_index) {
125 tmp = vars[1]; vars[1] = vars[2]; vars[2] = tmp;
126 }
127 if (vars[0].varinfo_index > vars[1].varinfo_index) {
128 tmp = vars[0]; vars[0] = vars[1]; vars[1] = tmp;
129 }
130 PptSlice3 slice = parent.findSlice(vars[0], vars[1], vars[2]);
131 if (slice == null) {
132 slice = new PptSlice3(parent, vars);
133 parent.addSlice(slice);
134 }
135 inv.ppt = slice;
136 }
137 inv.valid = this.valid;
138 return inv;
139 }
140
141 protected double computeConfidence() {
142 return Invariant.CONFIDENCE_JUSTIFIED;
143 }
144
145 public void negate() {
146 negated = !negated;
147 }
148
149 public String format_using(OutputFormat format) {
150 if (format == OutputFormat.DAIKON) return format_daikon();
151 if (format == OutputFormat.JAVA) return format_java();
152 if (format == OutputFormat.ESCJAVA) return format_esc();
153 if (format == OutputFormat.SIMPLIFY) return format_simplify();
154 if (format == OutputFormat.JML) return format_jml();
155 if (format == OutputFormat.DBCJAVA) return format_dbc();
156
157 return format_unimplemented(format);
158 }
159
160 public String format_daikon() {
161 String df;
162 if (daikonFormat == null)
163 df = "<dummy>";
164 else
165 df = daikonFormat;
166 if (negated)
167 return "not " + df;
168 else
169 return df;
170 }
171
172 public String format_java() {
173 if (javaFormat == null)
174 return "format_java not implemented for dummy invariant";
175 if (negated)
176 return "!(" + javaFormat + ")";
177 else
178 return javaFormat;
179 }
180
181 public String format_esc() {
182 if (escFormat == null)
183 return "format_esc not implemented for dummy invariant";
184 if (negated)
185 return "!(" + escFormat + ")";
186 else
187 return escFormat;
188 }
189
190 public String format_simplify() {
191 if (simplifyFormat == null)
192 return "format_simplify not implemented for dummy invariant";
193 if (negated)
194 return "(NOT " + simplifyFormat + ")";
195 else
196 return simplifyFormat;
197 }
198
199 public String format_jml() {
200 if (jmlFormat == null)
201 return "format_jml not implemented for dummy invariant";
202 if (negated)
203 return "!(" + jmlFormat + ")";
204 else
205 return jmlFormat;
206 }
207
208 public String format_dbc() {
209 if (dbcFormat == null)
210 return "format_dbc not implemented for dummy invariant";
211 if (negated)
212 return "!(" + dbcFormat + ")";
213 else
214 return dbcFormat;
215 }
216
217 protected Invariant resurrect_done(int[] permutation) {
218 throw new Error("Not implemented");
219 }
220 }