001package daikon.inv; 002 003import daikon.PptSlice; 004import daikon.PptSlice1; 005import daikon.PptSlice2; 006import daikon.PptSlice3; 007import daikon.PptTopLevel; 008import daikon.VarInfo; 009import java.util.HashSet; 010import java.util.Iterator; 011import java.util.List; 012import org.checkerframework.checker.lock.qual.GuardSatisfied; 013import org.checkerframework.checker.nullness.qual.Nullable; 014import org.checkerframework.dataflow.qual.SideEffectFree; 015import typequals.prototype.qual.NonPrototype; 016import typequals.prototype.qual.Prototype; 017 018/** 019 * This is a special invariant used internally by Daikon to represent invariants whose meaning 020 * Daikon doesn't understand. The only operation that can be performed on a DummyInvariant is to 021 * print it. In particular, the invariant cannot be tested against a sample: the invariant is always 022 * assumed to hold and is always considered to be statistically justified. 023 * 024 * <p>The main use for a dummy invariant is to represent a splitting condition that appears in a 025 * {@code .spinfo} file. The {@code .spinfo} file can indicate an arbitrary Java expression, which 026 * might not be equivalent to any invariant in Daikon's grammar. 027 * 028 * <p>Ordinarily, Daikon uses splitting conditions to split data, then seeks to use that split data 029 * to form conditional invariants out of its standard built-in invariants. If you wish the 030 * expression in the .spinfo file to be printed as an invariant, whether or not it is itself 031 * discovered by Daikon during invariant detection, then the configuration option {@code 032 * daikon.split.PptSplitter.dummy_invariant_level} must be set, and formatting information must be 033 * supplied in the splitter info file. 034 */ 035public class DummyInvariant extends Invariant { 036 static final long serialVersionUID = 20030220L; 037 038 private @Nullable String daikonFormat; 039 private @Nullable String javaFormat; 040 private @Nullable String escFormat; 041 private @Nullable String simplifyFormat; 042 private @Nullable String jmlFormat; 043 private @Nullable String dbcFormat; 044 private @Nullable String csharpFormat; 045 046 private boolean negated = false; 047 048 // Pre-instatiate(), set to true if we have reason to believe the user 049 // explicitly wanted this invariant to appear in the output. 050 // [What evidence is required, and when does the evidence show the user 051 // didn't want it? Does the fact that this is a DummyInvariant indicate 052 // the user explicitly cares?] 053 // After instantiation, also requires that we've found an appropriate 054 // slice for the invariant to live in. 055 public boolean valid = false; 056 057 public DummyInvariant( 058 PptSlice ppt, 059 @Nullable String daikonStr, 060 @Nullable String java, 061 @Nullable String esc, 062 @Nullable String simplify, 063 @Nullable String jml, 064 @Nullable String dbc, 065 @Nullable String csharp, 066 boolean valid) { 067 super(ppt); 068 daikonFormat = daikonStr; 069 javaFormat = java; 070 escFormat = esc; 071 simplifyFormat = simplify; 072 jmlFormat = jml; 073 dbcFormat = dbc; 074 csharpFormat = csharp; 075 this.valid = valid; 076 } 077 078 public @Prototype DummyInvariant( 079 @Nullable String daikonStr, 080 @Nullable String java, 081 @Nullable String esc, 082 @Nullable String simplify, 083 @Nullable String jml, 084 @Nullable String dbc, 085 @Nullable String csharp, 086 boolean valid) { 087 super(); 088 daikonFormat = daikonStr; 089 javaFormat = java; 090 escFormat = esc; 091 simplifyFormat = simplify; 092 jmlFormat = jml; 093 dbcFormat = dbc; 094 csharpFormat = csharp; 095 this.valid = valid; 096 } 097 098 public DummyInvariant instantiate(PptTopLevel parent, VarInfo[] vars) { 099 assert !this.negated : "Only instantiated invariants should be negated"; 100 DummyInvariant inv = 101 new DummyInvariant( 102 ppt, 103 daikonFormat, 104 javaFormat, 105 escFormat, 106 simplifyFormat, 107 jmlFormat, 108 dbcFormat, 109 csharpFormat, 110 // Not valid until we find a slice for it 111 /* valid= */ false); 112 113 // Find between 1 and 3 unique variables, to pick a slice to put 114 // this in. 115 HashSet<VarInfo> uniqVarsSet = new HashSet<>(); 116 for (int i = 0; i < vars.length; i++) { 117 uniqVarsSet.add(vars[i].canonicalRep()); 118 } 119 int sliceSize = uniqVarsSet.size(); 120 if (sliceSize > 3) { 121 sliceSize = 3; 122 } 123 /*NNC:@MonotonicNonNull*/ VarInfo[] newVars = new VarInfo[sliceSize]; 124 { 125 Iterator<VarInfo> it = uniqVarsSet.iterator(); 126 int i = 0; 127 while (it.hasNext()) { 128 newVars[i++] = it.next(); 129 if (i == sliceSize) { 130 break; 131 } 132 } 133 } 134 vars = newVars; 135 assert vars.length >= 1 && vars.length <= 3; 136 if (vars.length == 1) { 137 PptSlice1 slice = parent.findSlice(vars[0]); 138 if (slice == null) { 139 slice = new PptSlice1(parent, vars); 140 parent.addSlice(slice); 141 } 142 inv.ppt = slice; 143 } else if (vars.length == 2) { 144 if (vars[0] == vars[1]) { 145 return inv; 146 } else if (vars[0].varinfo_index > vars[1].varinfo_index) { 147 VarInfo tmp = vars[0]; 148 vars[0] = vars[1]; 149 vars[1] = tmp; 150 } 151 PptSlice2 slice = parent.findSlice(vars[0], vars[1]); 152 if (slice == null) { 153 slice = new PptSlice2(parent, vars); 154 parent.addSlice(slice); 155 } 156 inv.ppt = slice; 157 } else if (vars.length == 3) { 158 if (vars[0] == vars[1] || vars[1] == vars[2] || vars[0] == vars[2]) { 159 return inv; 160 } 161 // bubble sort 162 VarInfo tmp; 163 if (vars[0].varinfo_index > vars[1].varinfo_index) { 164 tmp = vars[0]; 165 vars[0] = vars[1]; 166 vars[1] = tmp; 167 } 168 if (vars[1].varinfo_index > vars[2].varinfo_index) { 169 tmp = vars[1]; 170 vars[1] = vars[2]; 171 vars[2] = tmp; 172 } 173 if (vars[0].varinfo_index > vars[1].varinfo_index) { 174 tmp = vars[0]; 175 vars[0] = vars[1]; 176 vars[1] = tmp; 177 } 178 PptSlice3 slice = parent.findSlice(vars[0], vars[1], vars[2]); 179 if (slice == null) { 180 slice = new PptSlice3(parent, vars); 181 parent.addSlice(slice); 182 } 183 inv.ppt = slice; 184 } 185 // We found a slice, so set the DummyInvariant to valid. 186 inv.valid = true; 187 return inv; 188 } 189 190 @Override 191 protected double computeConfidence() { 192 return Invariant.CONFIDENCE_JUSTIFIED; 193 } 194 195 public void negate() { 196 negated = !negated; 197 } 198 199 @SideEffectFree 200 @Override 201 public String format_using(@GuardSatisfied DummyInvariant this, OutputFormat format) { 202 if (format == OutputFormat.DAIKON) { 203 return format_daikon(); 204 } 205 if (format == OutputFormat.JAVA) { 206 return format_java(); 207 } 208 if (format == OutputFormat.ESCJAVA) { 209 return format_esc(); 210 } 211 if (format == OutputFormat.SIMPLIFY) { 212 return format_simplify(); 213 } 214 if (format == OutputFormat.JML) { 215 return format_jml(); 216 } 217 if (format == OutputFormat.DBCJAVA) { 218 return format_dbc(); 219 } 220 if (format == OutputFormat.CSHARPCONTRACT) { 221 return format_csharp(); 222 } 223 224 return format_unimplemented(format); 225 } 226 227 public String format_daikon(@GuardSatisfied DummyInvariant this) { 228 String df; 229 if (daikonFormat == null) { 230 df = "<dummy>"; 231 } else { 232 df = daikonFormat; 233 } 234 if (negated) { 235 return "not(" + df + ")"; 236 } else { 237 return df; 238 } 239 } 240 241 public String format_java(@GuardSatisfied DummyInvariant this) { 242 if (javaFormat == null) { 243 return "format_java not implemented for dummy invariant"; 244 } 245 if (negated) { 246 return "!(" + javaFormat + ")"; 247 } else { 248 return javaFormat; 249 } 250 } 251 252 public String format_esc(@GuardSatisfied DummyInvariant this) { 253 if (escFormat == null) { 254 return "format_esc not implemented for dummy invariant"; 255 } 256 if (negated) { 257 return "!(" + escFormat + ")"; 258 } else { 259 return escFormat; 260 } 261 } 262 263 public String format_simplify(@GuardSatisfied DummyInvariant this) { 264 if (simplifyFormat == null) { 265 return "format_simplify not implemented for dummy invariant"; 266 } 267 if (negated) { 268 return "(NOT " + simplifyFormat + ")"; 269 } else { 270 return simplifyFormat; 271 } 272 } 273 274 public String format_jml(@GuardSatisfied DummyInvariant this) { 275 if (jmlFormat == null) { 276 return "format_jml not implemented for dummy invariant"; 277 } 278 if (negated) { 279 return "!(" + jmlFormat + ")"; 280 } else { 281 return jmlFormat; 282 } 283 } 284 285 public String format_dbc(@GuardSatisfied DummyInvariant this) { 286 if (dbcFormat == null) { 287 return "format_dbc not implemented for dummy invariant"; 288 } 289 if (negated) { 290 return "!(" + dbcFormat + ")"; 291 } else { 292 return dbcFormat; 293 } 294 } 295 296 public String format_csharp(@GuardSatisfied DummyInvariant this) { 297 if (csharpFormat == null) { 298 return "format_csharp not implemented for dummy invariant"; 299 } 300 if (negated) { 301 return "!(" + csharpFormat + ")"; 302 } else { 303 return csharpFormat; 304 } 305 } 306 307 @Override 308 protected Invariant resurrect_done(int[] permutation) { 309 throw new Error("Not implemented"); 310 } 311 312 @Override 313 public boolean isSameFormula(Invariant other) { 314 throw new Error("Not implemented"); 315 } 316 317 @Override 318 public boolean enabled(@Prototype DummyInvariant this) { 319 throw new Error("do not invoke " + getClass() + ".enabled()"); 320 } 321 322 @Override 323 public boolean valid_types(@Prototype DummyInvariant this, VarInfo[] vis) { 324 throw new Error("do not invoke " + getClass() + ".valid_types()"); 325 } 326 327 @Override 328 protected @NonPrototype DummyInvariant instantiate_dyn( 329 @Prototype DummyInvariant this, PptSlice slice) { 330 throw new Error("do not invoke " + getClass() + ".instantiate_dyn()"); 331 } 332 333 @Override 334 public @Nullable @NonPrototype DummyInvariant merge( 335 @Prototype DummyInvariant this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) { 336 throw new Error("Don't merge DummyInvariant invariants"); 337 } 338}