001 package daikon;
002
003 import daikon.derive.*;
004 import daikon.derive.unary.*;
005 import daikon.derive.binary.*;
006 import daikon.derive.ternary.*;
007 import daikon.VarInfoName.*;
008 import daikon.PrintInvariants;
009 import daikon.inv.*;
010 import daikon.inv.unary.scalar.*;
011 import daikon.inv.unary.sequence.*;
012 import daikon.inv.binary.twoScalar.*;
013 import daikon.Quantify;
014 import daikon.Quantify.QuantFlags;
015 import daikon.Quantify.QuantifyReturn;
016 import static daikon.FileIO.VarDefinition;
017
018 import utilMDE.*;
019
020 import java.util.*;
021 import java.util.logging.Logger;
022 import java.util.logging.Level;
023 import java.io.*;
024
025 /**
026 * Represents information about a particular variable for a program
027 * point. This object doesn't hold the value of the variable at a
028 * particular step of the program point, but can get the value it
029 * holds when given a ValueTuple using the getValue() method. VarInfo
030 * also includes info about the variable's name, its declared type, its
031 * file representation type, its internal type, and its comparability.
032 **/
033 @SuppressWarnings("nullness") // nullness properties in this file are hairy; save for later
034 public final /*@Interned*/ class VarInfo implements Cloneable, Serializable {
035 // We are Serializable, so we specify a version to allow changes to
036 // method signatures without breaking serialization. If you add or
037 // remove fields, you should change this number to the current date.
038 static final long serialVersionUID = 20060815L;
039
040 /**
041 * If true, then variables are only considered comparable if they
042 * are declared with the same type. For example, java.util.List
043 * is not comparable to java.util.ArrayList and float is not
044 * comparable to double. This may miss valid invariants, but
045 * significant time can be saved and many variables with
046 * different declared types are not comparable (e.g., java.util.Date
047 * and java.util.ArrayList).
048 */
049 public static boolean dkconfig_declared_type_comparability = true;
050
051 /**
052 * If true, the treat static constants (such as MapQuick.GeoPoint.FACTOR)
053 * as fields within an object rather than as a single name. Not correct,
054 * but used to obtain compatibility with VarInfoName.
055 */
056 public static boolean dkconfig_constant_fields_simplify = true;
057
058 /** Debug missing vals. **/
059 public static final Logger debugMissing =
060 Logger.getLogger("daikon.VarInfo.missing");
061
062 /** The program point this variable is in. **/
063 public PptTopLevel ppt;
064
065 /**
066 * Name. Do not compare names of invariants from different program
067 * points, because two different program points could contain unrelated
068 * variables named "x".
069 **/
070 private VarInfoName var_info_name; // interned
071
072 /**
073 * Name as specified in the program point declaration. VarInfoName
074 * sometimes changes this name as part of parsing so that
075 * VarInfoName.name() doesn't return the original name.
076 */
077 private /*@Interned*/ String str_name; // interned
078
079 /** returns the interned name of the variable **/
080 public /*@Interned*/ String name() {
081 if (FileIO.new_decl_format)
082 return str_name;
083 else
084 return (var_info_name.name().intern()); // vin ok
085 }
086
087 /** Returns the original name of the variable from the program point declaration. **/
088 public /*@Interned*/ String str_name() {
089 return str_name;
090 }
091
092 /**
093 * Type as declared in the target program. This is seldom used
094 * within Daikon as these types vary with program language and
095 * the like. It's here more for information than anything else.
096 **/
097 public ProglangType type; // interned (as are all ProglangType objects)
098
099 /**
100 * Type as written in the data trace file -- i.e., it is the
101 * source variable type mapped into the set of basic types
102 * recognized by Daikon. In particular, it includes boolean and
103 * hashcode (pointer). This is the type that is normally used
104 * when determining if an invariant is applicable to a variable.
105 * For example, the less-than invariant is not applicable to
106 * booleans or hashcodes, but is applicable to integers (of
107 * various sizes) and floats.
108 * (In the variable name, "rep" stands for "representation".)
109 **/
110 public ProglangType file_rep_type; // interned (as are all ProglangType objects)
111
112 /**
113 * Type as internally stored by Daikon. It contains less
114 * information than file_rep_type (for example, boolean and
115 * hashcode are both stored as integers).
116 * (In the variable name, "rep" stands for "representation".)
117 *
118 * @see ProglangType#fileTypeToRepType()
119 **/
120 public ProglangType rep_type; // interned (as are all ProglangType objects)
121
122 /** Comparability info. **/
123 public VarComparability comparability;
124
125 /** Auxiliary info. **/
126 public VarInfoAux aux;
127
128 /** The index in lists of VarInfo objects. **/
129 public int varinfo_index;
130
131 /**
132 * The index in a ValueTuple (more generally, in a list of values).
133 * It can differ from varinfo_index due to
134 * constants (and possibly other factors).
135 * It is -1 iff is_static_constant or not yet set.
136 **/
137 public int value_index;
138
139 /**
140 * is_static_constant iff (value_index == -1);
141 * is_static_constant == (static_constant_value != null).
142 **/
143 public boolean is_static_constant;
144
145 /** Null if not statically constant. **/
146 /*@Nullable*/ /*@Interned*/ Object static_constant_value;
147
148 /** Whether and how derived. Null if this is not derived. **/
149 public /*@LazyNonNull*/ Derivation derived;
150
151 // Various enums used for information about variables
152 public enum RefType {POINTER, OFFSET};
153 public enum LangFlags {PUBLIC, PRIVATE, PROTECTED, STATIC, FINAL,
154 SYNCHRONIZED, VOLATILE, TRANSIENT, ANNOTATION, ENUM};
155 // These enums are intentionally duplicated in Chicory and other
156 // front-ends. These values are written into decl files, and as
157 // such, should stay constant between front-ends. They should not be
158 // changed without good reason; if you do change them, make sure to
159 // also change the corresponding constants in Daikon front ends!
160 public enum VarKind {FIELD, FUNCTION, ARRAY, VARIABLE, RETURN};
161 public enum VarFlags {IS_PARAM, NO_DUPS, NOT_ORDERED, NO_SIZE, NOMOD,
162 SYNTHETIC, CLASSNAME, TO_STRING, NON_NULL};
163
164
165 public /*@Nullable*/ RefType ref_type;
166 public VarKind var_kind;
167 public EnumSet<VarFlags> var_flags = EnumSet.noneOf (VarFlags.class);
168 public EnumSet<LangFlags> lang_flags = EnumSet.noneOf (LangFlags.class);
169
170 public VarDefinition vardef;
171 // under what circumstances is this null?
172 public /*@Nullable*/ VarInfo enclosing_var;
173 public int arr_dims = 0;
174 public /*@Nullable*/ List<VarInfo> function_args = null;
175
176 /** Parent ppt for this variable (if any) **/
177 public /*@Nullable*/ String parent_ppt = null;
178
179 /** Parent variable (within parent_ppt) (if any) **/
180 public /*@Nullable*/ String parent_variable = null;
181
182 /** Parent ppt relation id **/
183 public int parent_relation_id = 0;
184
185 /**
186 * The relative name of this variable with respect to its enclosing
187 * variable. Field name for fields, method name for instance methods.
188 */
189 public /*@Nullable*/ String relative_name = null;
190
191 /**
192 * Returns whether or not we have encountered to date any missing values
193 * due to array indices being out of bounds. This can happen with both
194 * subscripts and subsequences. Note that this becomes true as we are
195 * running, it cannot be set in advance without a first pass.
196 *
197 * This is used as we are processing data to destroy any invariants
198 * that use this variable.
199 *
200 * @see Derivation#missingOutOfBounds()
201 **/
202 public boolean missingOutOfBounds() {
203 if ((derived != null) && derived.missingOutOfBounds())
204 return (true);
205 return (false);
206 }
207
208 /** True if this variable is ever missing **/
209 public boolean canBeMissing = false;
210
211 /**
212 * Which equality group this belongs to. Replaces equal_to. Never null
213 * after this is put inside equalitySet.
214 **/
215 public Equality equalitySet;
216
217 /** Cached value for sequenceSize() **/
218 private VarInfo sequenceSize;
219
220 /** non-null if this is an orig() variable.
221 * <b>Do not test equality! Only use its .name slot.</b>
222 **/
223 public /*@Nullable*/ VarInfo postState; //
224
225 /**
226 * @exception RuntimeException if representation invariant on this is broken
227 */
228 public void checkRep() {
229 assert ppt != null;
230 assert var_info_name != null; // vin ok
231 assert var_info_name == var_info_name.intern(); // vin ok
232 assert type != null;
233 assert file_rep_type != null;
234 assert rep_type != null;
235 assert comparability != null; // anything else ??
236 assert comparability.alwaysComparable()
237 || (((VarComparabilityImplicit)comparability).dimensions == file_rep_type.dimensions());
238 assert
239 0 <= varinfo_index && varinfo_index < ppt.var_infos.length;
240 assert -1 <= value_index && value_index < varinfo_index;
241 assert is_static_constant == (value_index == -1);
242 assert
243 is_static_constant || (static_constant_value == null);
244 }
245
246 /** Returns whether or not rep_type is a legal type **/
247 static boolean legalRepType(ProglangType rep_type) {
248 return (
249 (rep_type == ProglangType.INT)
250 || (rep_type == ProglangType.DOUBLE)
251 || (rep_type == ProglangType.STRING)
252 || (rep_type == ProglangType.INT_ARRAY)
253 || (rep_type == ProglangType.DOUBLE_ARRAY)
254 || (rep_type == ProglangType.STRING_ARRAY));
255 }
256
257 /** Returns whether or not constant_value is a legal constant **/
258 static boolean legalConstant (Object constant_value) {
259 return ((constant_value == null) || (constant_value instanceof Long)
260 || (constant_value instanceof Double));
261 }
262
263 /**
264 * Returns whether or not file_rep_type is a legal file_rep_type.
265 * The file_rep_type matches rep_type except that it also allows
266 * the more detailed scalar types (HASHCODE, BOOLEAN, etc).
267 */
268 static boolean legalFileRepType(ProglangType file_rep_type) {
269 return (legalRepType(file_rep_type)
270 // The below types are converted into one of the rep types
271 // by ProglangType.fileTypeToRepType().
272 || (file_rep_type == ProglangType.HASHCODE)
273 || (file_rep_type == ProglangType.HASHCODE_ARRAY)
274 || ((file_rep_type.dimensions() <= 1) && file_rep_type.baseIsPrimitive()));
275 }
276
277 /** Create VarInfo from VarDefinition **/
278 public VarInfo (VarDefinition vardef) {
279
280 // Basic checking for sensible input
281 assert vardef.name != null;
282 assert vardef.kind != null;
283 assert vardef.rep_type != null;
284 assert (vardef.arr_dims == 0) || (vardef.arr_dims == 1);
285 assert vardef.rep_type != null;
286 assert vardef.declared_type != null;
287 assert vardef.comparability != null;
288 if (vardef.kind != VarKind.FUNCTION)
289 assert vardef.function_args == null;
290
291 this.vardef = vardef;
292
293 // Create a VarInfoName from the external name. This probably gets
294 // removed in the long run.
295 try {
296 var_info_name = VarInfoName.parse (vardef.name); // vin ok
297 } catch (Exception e) {
298 @SuppressWarnings("nullness") // error case, likely to crash later anyway
299 /*@NonNull*/ VarInfoName vin = null;
300 var_info_name = vin;
301 System.out.printf ("Warning: Can't parse %s as a VarInfoName",
302 vardef.name);
303 }
304 str_name = vardef.name.intern();
305
306 // Copy info from vardef
307 var_kind = vardef.kind;
308 relative_name = vardef.relative_name;
309 ref_type = vardef.ref_type;
310 arr_dims = vardef.arr_dims;
311 comparability = vardef.comparability;
312 file_rep_type = vardef.rep_type;
313 type = vardef.declared_type;
314 var_flags = vardef.flags;
315 lang_flags = vardef.lang_flags;
316 parent_ppt = vardef.parent_ppt;
317 parent_variable = vardef.parent_variable;
318 parent_relation_id = vardef.parent_relation_id;
319
320 // If a static constant value was specified, set it
321 if (vardef.static_constant_value != null) {
322 is_static_constant = true;
323 static_constant_value = vardef.static_constant_value;
324 } else {
325 is_static_constant = false;
326 }
327
328 // Create the rep_type from the file rep type
329 rep_type = file_rep_type.fileTypeToRepType();
330
331 // Create the VarInfoAux information
332 String auxstr = "";
333 if (var_flags.contains (VarFlags.IS_PARAM)) {
334 if (auxstr.length() > 0)
335 auxstr += ", ";
336 auxstr += "isParam=true";
337 }
338 if (var_flags.contains (VarFlags.NON_NULL)) {
339 if (auxstr.length() > 0)
340 auxstr += ", ";
341 auxstr += "isStruct=true";
342 }
343 try {
344 aux = VarInfoAux.parse (auxstr);
345 } catch (Exception e) {
346 throw new RuntimeException ("unexpected aux error", e);
347 }
348 }
349
350 /**
351 * Finishes defining the variable by relating it to other variables.
352 * This cannot be done when creating the variable because the other variables
353 * it is related to, may not yet exist. Variables are related to their
354 * enclosing variables (for fields, arrays, and functions) and to their
355 * parent variables in the PptHierarchy. RuntimeExceptions are thrown if
356 * any related variables do not exist.
357 */
358 public void relate_var() {
359
360 if (vardef == null)
361 return;
362
363 // System.out.printf ("enclosing var for %s is %s%n", str_name,
364 // vardef.enclosing_var);
365
366 // Find and set the enclosing variable (if any)
367 if (vardef.enclosing_var != null) {
368 enclosing_var = ppt.find_var_by_name (vardef.enclosing_var);
369 if (enclosing_var == null) {
370 for (int i = 0; i < ppt.var_infos.length; i++)
371 System.out.printf ("var = '%s'%n", ppt.var_infos[i]);
372 throw new RuntimeException
373 (String.format("enclosing variable '%s' for variable '%s' "
374 + "in ppt '%s' cannot be found",
375 vardef.enclosing_var, vardef.name, ppt.name));
376 }
377 }
378
379 // Find all function arguments (if any)
380 if (vardef.function_args != null) {
381 function_args = new ArrayList<VarInfo>(vardef.function_args.size());
382 for (String varname : vardef.function_args) {
383 VarInfo vi = ppt.find_var_by_name (varname);
384 if (vi == null) {
385 throw new RuntimeException
386 (String.format ("function argument '%s' for variable '%s' "
387 +" in ppt '%s' cannot be found",
388 varname, vardef.name, ppt.name));
389 }
390 function_args.add (vi);
391 }
392 }
393
394 // do something appropriate with the ppt/var hierarchy. It may be
395 // that this is better done within PptRelation
396 }
397
398 /**
399 * Setup information normally specified in the declaration record
400 * for derived variables where the new variable is the result of
401 * applying a function to the other variables. Much of the
402 * information is inferred from (arbitrarily) the first argument to
403 * the function.
404 *
405 * The parent_ppt field is set if each VarInfo in the derivation has
406 * the same parent. The parent_variable field is set if there is a
407 * parent_ppt and one or more of the bases has a non-default parent
408 * variable. The parent variable name is formed as
409 * function_name(arg1,arg2,...) where arg1, arg2, etc are the
410 * parent variable names of each of the arguments.
411 */
412 public void setup_derived_function (String name, VarInfo... bases) {
413
414 // Copy variable info from the first base
415 VarInfo base = bases[0];
416 ref_type = null;
417 var_flags = base.var_flags.clone();
418 lang_flags = base.lang_flags.clone();
419 for (int ii = 1; ii < bases.length; ii++) {
420 var_flags.retainAll (bases[ii].var_flags);
421 lang_flags.retainAll (bases[ii].lang_flags);
422 }
423 enclosing_var = null;
424 arr_dims = base.arr_dims;
425 var_kind = VarKind.FUNCTION;
426 function_args = Arrays.asList (bases);
427
428 // Build the string name
429 List<String> arg_names = new ArrayList<String>();
430 for (VarInfo vi : bases)
431 arg_names.add (vi.name());
432 str_name
433 = String.format ("%s(%s)", name, UtilMDE.join (arg_names, ",")).intern();
434
435 // The parent ppt is the same as the base if each varinfo in the
436 // derivation has the same parent
437 parent_relation_id = base.parent_relation_id;
438 parent_ppt = base.parent_ppt;
439 if (parent_relation_id != 0) {
440 for (int ii = 1; ii < bases.length; ii++) {
441 if (parent_relation_id != bases[ii].parent_relation_id) {
442 parent_relation_id = 0;
443 parent_ppt = null;
444 break;
445 }
446 }
447 }
448
449 // If there is a parent_ppt, determine the parent_variable name.
450 // If all of the argument names are the default, then the parent_variable
451 // is the default as well. Otherwise, build up the name from the
452 // function name and the name of each arguments parent variable name.
453 if (parent_ppt != null) {
454 boolean parent_vars_specified = false;
455 for (VarInfo vi : bases) {
456 if (vi.parent_variable != null)
457 parent_vars_specified = true;
458 }
459 if (!parent_vars_specified)
460 parent_variable = null;
461 else { // one of the arguments has a different parent variable name
462 StringBuilderDelimited args = new StringBuilderDelimited(",");
463 for (VarInfo vi : bases) {
464 args.append(vi.parent_variable);
465 }
466 parent_variable = String.format ("%s(%s)", name, args.toString());
467 }
468 }
469 }
470
471 /**
472 * Setup information normally specified in the declaration record
473 * for derived variables where one of the variables is the base of
474 * the derivation. In general this information is inferred
475 * from the base variable of the derived variables. Note that
476 * parent_ppt is set if each VarInfo in the derivation has the same
477 * parent, but parent_variable is not set. This has to be set based
478 * on the particular derivation.
479 */
480 public void setup_derived_base (VarInfo base, VarInfo... others) {
481
482 // Copy variable info from the base
483 ref_type = base.ref_type;
484 var_kind = base.var_kind;
485 var_flags = base.var_flags.clone();
486 lang_flags = base.lang_flags.clone();
487 enclosing_var = base.enclosing_var;
488 arr_dims = base.arr_dims;
489 function_args = base.function_args;
490
491 // The parent ppt is the same as the base if each varinfo in the
492 // derivation has the same parent
493 parent_relation_id = base.parent_relation_id;
494 parent_ppt = base.parent_ppt;
495 if (parent_relation_id != 0) {
496 for (VarInfo other : others) {
497 if (other == null)
498 continue;
499 if (parent_relation_id != other.parent_relation_id) {
500 parent_relation_id = 0;
501 parent_ppt = null;
502 break;
503 }
504 }
505 }
506
507 }
508
509 /** Create the specified VarInfo **/
510 private VarInfo (VarInfoName name, ProglangType type,
511 ProglangType file_rep_type, VarComparability comparability,
512 boolean is_static_constant, /*@Nullable*/ /*@Interned*/ Object static_constant_value,
513 VarInfoAux aux) {
514
515 assert name != null;
516 assert file_rep_type != null;
517 assert legalFileRepType(file_rep_type) : "Unsupported representation type "
518 + file_rep_type.format() + "/" + file_rep_type.getClass() + " "
519 + ProglangType.HASHCODE.getClass() + " for variable " + name;
520 assert type != null;
521 assert comparability != null;
522 // COMPARABILITY TEST
523 // assert
524 // comparability.alwaysComparable() || ((VarComparabilityImplicit)comparability).dimensions == file_rep_type.dimensions()
525 // : "Types dimensions incompatibility: "
526 // + type
527 // + " vs. "
528 // + file_rep_type;
529 assert aux != null;
530 assert legalConstant (static_constant_value)
531 : "unexpected constant class " + static_constant_value.getClass();
532
533 // Possibly the call to intern() isn't necessary; but it's safest to
534 // make the call to intern() rather than running the risk that a caller
535 // didn't.
536 this.var_info_name = name.intern(); // vin ok
537 this.type = type;
538 this.file_rep_type = file_rep_type;
539 this.rep_type = file_rep_type.fileTypeToRepType();
540 this.comparability = comparability;
541 this.is_static_constant = is_static_constant;
542 this.static_constant_value = static_constant_value;
543 this.aux = aux;
544
545 if (debug.isLoggable(Level.FINE)) {
546 debug.fine("Var " + name + " aux: " + aux);
547 }
548
549 // Indicates that these haven't yet been set to reasonable values.
550 value_index = -1;
551 varinfo_index = -1;
552
553 canBeMissing = false;
554 }
555
556 /** Create the specified VarInfo **/
557 public VarInfo (String name, ProglangType type,
558 ProglangType file_rep_type, VarComparability comparability,
559 boolean is_static_constant, /*@Nullable*/ /*@Interned*/ Object static_constant_value,
560 VarInfoAux aux) {
561 this (VarInfoName.parse(name), type, file_rep_type, comparability,
562 is_static_constant, static_constant_value, aux);
563 assert name != null;
564 this.str_name = name.intern();
565 }
566
567 /** Create the specified non-static VarInfo **/
568 private VarInfo (VarInfoName name, ProglangType type,
569 ProglangType file_rep_type, VarComparability comparability,
570 VarInfoAux aux) {
571 this(name, type, file_rep_type, comparability, false, null, aux);
572 }
573
574 /** Create the specified non-static VarInfo **/
575 public VarInfo (String name, ProglangType type,
576 ProglangType file_rep_type, VarComparability comparability,
577 VarInfoAux aux) {
578 this(name, type, file_rep_type, comparability, false, null, aux);
579 assert name != null;
580 this.str_name = name.intern();
581 }
582
583 /** Create a VarInfo with the same values as vi **/
584 public VarInfo (VarInfo vi) {
585 this (vi.name(), vi.type, vi.file_rep_type, vi.comparability,
586 vi.is_static_constant, vi.static_constant_value, vi.aux);
587 str_name = vi.str_name;
588 canBeMissing = vi.canBeMissing;
589 postState = vi.postState;
590 equalitySet = vi.equalitySet;
591 ref_type = vi.ref_type;
592 var_kind = vi.var_kind;
593 var_flags = vi.var_flags.clone();
594 lang_flags = vi.lang_flags.clone();
595 vardef = vi.vardef;
596 enclosing_var = vi.enclosing_var;
597 arr_dims = vi.arr_dims;
598 function_args = vi.function_args;
599 parent_ppt = vi.parent_ppt;
600 parent_variable = vi.parent_variable;
601 parent_relation_id = vi.parent_relation_id;
602 relative_name = vi.relative_name;
603 }
604
605 /** Creates and returns a copy of this. **/
606 // Default implementation to quiet Findbugs.
607 @SuppressWarnings("interning") // temporary?
608 public VarInfo clone() throws CloneNotSupportedException {
609 return (VarInfo) super.clone();
610 }
611
612 /** Create the prestate, or "orig()", version of the variable. **/
613 public static VarInfo origVarInfo(VarInfo vi) {
614 // At an exit point, parameters are uninteresting, but orig(param) is not.
615 // So don't call orig(param) a parameter.
616 // VIN (below should be removed)
617 // VarInfoAux aux_nonparam =
618 // vi.aux.setValue(VarInfoAux.IS_PARAM, VarInfoAux.FALSE);
619
620 VarInfo result;
621 if (FileIO.new_decl_format) {
622
623 // Build a Variable Definition from the poststate vardef
624 VarDefinition result_vardef = vi.vardef.copy();
625 result_vardef.name = vi.prestate_name();
626
627 // The only hierarchy relation for orig variables is to the enter
628 // ppt. Remove any specified relations.
629 result_vardef.clear_parent_relation();
630
631 // Fix the enclosing variable to point to the prestate version
632 if (result_vardef.enclosing_var != null)
633 result_vardef.enclosing_var = vi.enclosing_var.prestate_name();
634
635 // Build a the prestate VarInfo from the VarDefinition.
636 result = new VarInfo (result_vardef);
637
638 // Copy the missing flag from the original variable. This is necessary
639 // for combined exit points which are built after processing is
640 // complete. In most cases the missing flag will be set correctly
641 // by merging the missing flag from the numbered exit points. But
642 // this will fail if the method terminates early each time the variable
643 // is missing. A better fix would be to instrument early exits and
644 // merge them in as well, but this matches what we did previously.
645 result.canBeMissing = vi.canBeMissing;
646
647 } else {
648 VarInfoName newname = vi.var_info_name.applyPrestate(); // vin ok
649 result =
650 new VarInfo(newname,
651 vi.type,
652 vi.file_rep_type,
653 vi.comparability.makeAlias(),
654 vi.aux);
655 result.canBeMissing = vi.canBeMissing;
656 result.postState = vi;
657 result.equalitySet = vi.equalitySet;
658 result.arr_dims = vi.arr_dims;
659 result.str_name = vi.prestate_name();
660 }
661
662 // At an exit point, parameters are uninteresting, but orig(param) is not.
663 // So don't call orig(param) a parameter.
664 result.set_is_param (false);
665 return result;
666 }
667
668 /**
669 * Given an array of VarInfo objects, return an array of clones, where
670 * references to the originals have been modified into references to the
671 * new ones (so that the new set is self-consistent). The originals
672 * should not be modified by this operation.
673 **/
674 public static VarInfo[] arrayclone_simple(VarInfo[] a_old) {
675 int len = a_old.length;
676 VarInfo[] a_new = new VarInfo[len];
677 for (int i = 0; i < len; i++) {
678 a_new[i] = new VarInfo(a_old[i]);
679 if (a_old[i].derived != null)
680 assert a_new[i].derived != null;
681 a_new[i].varinfo_index = a_old[i].varinfo_index;
682 a_new[i].value_index = a_old[i].value_index;
683 }
684 return a_new;
685 }
686
687
688 /** Trims the collections used by this VarInfo. */
689 public void trimToSize() {
690 // if (derivees != null) { derivees.trimToSize(); }
691 // Derivation derived; probably can't be trimmed
692 }
693
694 /** Returns the name of the variable. For more info see repr() **/
695 public String toString() {
696 return name();
697 }
698
699 /** Helper function for repr(). **/
700 private Object checkNull(Object o) {
701 return (o == null) ? "null" : o;
702 }
703
704 /** Returns a complete string description of the variable **/
705 public String repr() {
706 return "<VarInfo "
707 + var_info_name // vin ok
708 + ": "
709 + "type="
710 + type
711 + ",file_rep_type="
712 + file_rep_type
713 + ",rep_type="
714 + rep_type
715 + ",comparability="
716 + comparability
717 + ",value_index="
718 + value_index
719 + ",varinfo_index="
720 + varinfo_index
721 + ",is_static_constant="
722 + is_static_constant
723 + ",static_constant_value="
724 + static_constant_value
725 + ",derived="
726 + checkNull(derived)
727 + ",derivees="
728 + derivees()
729 + ",ppt="
730 + ppt.name()
731 + ",canBeMissing="
732 + canBeMissing
733 + (",equal_to="
734 + (equalitySet == null ? "null" : equalitySet.toString()))
735 + ",isCanonical()="
736 + isCanonical()
737 + ">";
738 }
739
740 /** Returns whether or not this variable is a static constant **/
741 public boolean isStaticConstant() {
742 return is_static_constant;
743 }
744
745 /**
746 * Returns the static constant value of this variable. The variable
747 * must be a static constant.
748 */
749 public Object constantValue() {
750 if (isStaticConstant()) {
751 return static_constant_value;
752 } else {
753 throw new Error("Variable " + name() + " is not constant");
754 }
755 }
756
757 /** Returns true if this is an "orig()" variable **/
758 /*@AssertNonNullIfTrue("postState")*/
759 public boolean isPrestate() {
760 return postState != null;
761 }
762
763 /** Returns true if this variable is derived from prestate variables **/
764 public boolean isPrestateDerived() {
765 if (postState != null)
766 return true;
767 if (isDerived()) {
768 for (VarInfo vi : derived.getBases()) {
769 if (!vi.isPrestate())
770 return false;
771 }
772 return true;
773 } else {
774 return isPrestate();
775 }
776
777 // return name.isAllPrestate();
778 }
779
780 /** Returns true if this variable is a derived variable **/
781 public boolean isDerived() {
782 return (derived != null);
783 }
784
785 /** returns the depth of derivation **/
786 public int derivedDepth() {
787 if (derived == null)
788 return 0;
789 else
790 return derived.derivedDepth();
791 }
792
793 /** Return all derived variables that build off this one. **/
794 public List<Derivation> derivees() {
795 ArrayList<Derivation> result = new ArrayList<Derivation>();
796 VarInfo[] vis = ppt.var_infos;
797 for (int i = 0; i < vis.length; i++) {
798 VarInfo vi = vis[i];
799 Derivation der = vi.derived;
800 if (der == null)
801 continue;
802 if (ArraysMDE.indexOf(der.getBases(), this) >= 0) {
803 result.add(der);
804 }
805 }
806 return result;
807 }
808
809 /**
810 * Returns a list of all of the basic (non-derived) variables that
811 * are used to make up this variable. If this variable is not
812 * derived, it is just this variable. Otherwise it is all of the
813 * the bases of this derivation
814 */
815 public List<VarInfo> get_all_constituent_vars() {
816 List<VarInfo> vars = new ArrayList<VarInfo>();
817 if (isDerived()) {
818 for (VarInfo vi : derived.getBases()) {
819 vars.addAll (vi.get_all_constituent_vars());
820 }
821 } else {
822 vars.add (this);
823 }
824 return (vars);
825 }
826
827 /**
828 * Returns a list of all of the simple names that make up this variable.
829 * this includes each field and function name in the variable. If this
830 * variable is derived it includes the simple names from each of its bases.
831 * For example, 'this.item.a' would return a list with 'this', 'item', and
832 * 'a' and 'this.theArray[i]' would return 'this', 'theArray' and 'i'.
833 **/
834 public List<String> get_all_simple_names() {
835 assert FileIO.new_decl_format;
836 List<String> names = new ArrayList<String>();
837 if (isDerived()) {
838 for (VarInfo vi : derived.getBases()) {
839 names.addAll (vi.get_all_simple_names());
840 }
841 } else {
842 VarInfo start = (isPrestate() ? postState : this);
843 for (VarInfo vi = start; vi != null; vi = vi.enclosing_var) {
844 if (relative_name == null)
845 names.add (vi.name());
846 else
847 names.add (vi.relative_name);
848 }
849 }
850 return (names);
851
852 }
853
854 public boolean isClosure() {
855 // This should eventually turn into
856 // return name.indexOf("closure(") != -1;
857 // when I rename those variables to "closure(...)".
858 return name().indexOf("~") != -1; // XXX
859 }
860
861 /** Cached value for getDerivedParam(). **/
862 public VarInfo derivedParamCached = null;
863
864 /** Cached value for isDerivedParam(). **/
865 // Boolean rather than boolean so we can use "null" to indicate "not yet set".
866 public Boolean isDerivedParamCached = null;
867
868 /**
869 * Returns true if this is a param according to aux info, or this is
870 * a front end derivation such that one of its bases is a param. To
871 * figure this out, what we do is get all the param variables at
872 * this's program point. Then we search in this's name to see if
873 * the name contains any of the variables. We have to do this
874 * because we only have name info, and we assume that x and x.a are
875 * related from the names alone.
876 * Effects: Sets isDerivedParamCached and derivedParamCached to
877 * values the first time this method is called. Subsequent calls
878 * use these cached values.
879 **/
880 public boolean isDerivedParam() {
881 if (isDerivedParamCached != null) {
882 // System.out.printf ("var %s is-derived-param = %b\n", name(),
883 // isDerivedParamCached);
884 return isDerivedParamCached.booleanValue();
885 }
886
887 boolean result = false;
888 if (isParam() && !isPrestate())
889 result = true;
890
891
892 if (!FileIO.new_decl_format) {
893 // Determine the result from VarInfoName
894 Set<VarInfo> paramVars = ppt.getParamVars();
895 Set<VarInfoName> param_names = new LinkedHashSet<VarInfoName>();
896 for (VarInfo vi : paramVars)
897 param_names.add (vi.var_info_name); // vin ok
898
899 String param = "";
900 VarInfoName.Finder finder = new VarInfoName.Finder(param_names);
901 Object baseMaybe = finder.getPart(var_info_name); // vin ok
902 if (baseMaybe != null) {
903 VarInfoName base = (VarInfoName) baseMaybe;
904 derivedParamCached = this.ppt.find_var_by_name (base.name());
905 if (Global.debugSuppressParam.isLoggable(Level.FINE)) {
906 Global.debugSuppressParam.fine(
907 name() + " is a derived param");
908 Global.debugSuppressParam.fine("derived from " + base.name());
909 Global.debugSuppressParam.fine(paramVars.toString());
910 }
911 param = "derived from " + base.name();
912 result = true;
913 }
914 } else { // new format
915 derivedParamCached = enclosing_param();
916 if (derivedParamCached != null)
917 result = true;
918 else if (derived != null) {
919 for (VarInfo vi : derived.getBases()) {
920 derivedParamCached = vi.enclosing_param();
921 if (derivedParamCached != null) {
922 result = true;
923 break;
924 }
925 }
926 }
927 }
928
929 // System.out.printf ("var %s is-derived-param = %b\n", name(), result);
930 isDerivedParamCached = result ? Boolean.TRUE : Boolean.FALSE;
931 return result;
932 }
933
934 /**
935 * Returns the param variable that encloses this variable (if any).
936 * Returns null otherwise. Only valid in the new decl format.
937 **/
938 private /*@Nullable*/ VarInfo enclosing_param () {
939 // System.out.printf ("Considering %s\n", this);
940 assert FileIO.new_decl_format;
941 if (isPrestate())
942 return postState.enclosing_param();
943 for (VarInfo evi = this; evi != null; evi = evi.enclosing_var) {
944 // System.out.printf ("%s isParam=%b\n", evi, evi.isParam());
945 if (evi.isParam()) {
946 return (evi);
947 }
948 }
949 return (null);
950 }
951
952 /**
953 * Return a VarInfo that has two properties: this is a derivation of
954 * it, and it is a parameter variable. If this is a parameter, then
955 * this is returned. For example, "this" is always a parameter.
956 * The return value of getDerivedParam for "this.a" (which is not a
957 * parameter) is "this".
958 * Effects: Sets isDerivedParamCached and derivedParamCached to
959 * values the first time this method is called. Subsequent calls
960 * use these cached values.
961 * @return null if the above condition doesn't hold.
962 **/
963 public /*@Nullable*/ VarInfo getDerivedParam() {
964 if (isDerivedParamCached == null) {
965 isDerivedParam();
966 }
967 return derivedParamCached;
968 }
969
970 private Boolean isDerivedParamAndUninterestingCached = null;
971
972 /**
973 * Returns true if a given VarInfo is a parameter or derived from
974 * one in such a way that changes to it wouldn't be visible to the
975 * method's caller. There are 3 such cases:
976 *
977 * <li> The variable is a pass-by-value parameter "p".
978 * <li> The variable is of the form "p.prop" where "prop" is an
979 * immutable property of an object, like its type, or (for a Java
980 * array) its size.
981 * <li> The variable is of the form "p.prop", and "p" has been
982 * modified to point to a different object. We assume "p" has been
983 * modified if we don't have an invariant "orig(p) == p".
984 *
985 * In any case, the variable must have a postState VarInfoName, and
986 * equality invariants need to have already been computed.
987 **/
988 public boolean isDerivedParamAndUninteresting() {
989 if (isDerivedParamAndUninterestingCached != null) {
990 return isDerivedParamAndUninterestingCached.booleanValue();
991 } else {
992 isDerivedParamAndUninterestingCached =
993 _isDerivedParamAndUninteresting()
994 ? Boolean.TRUE
995 : Boolean.FALSE;
996 return isDerivedParamAndUninterestingCached.booleanValue();
997 }
998 }
999
1000 private boolean _isDerivedParamAndUninteresting() {
1001 if (PrintInvariants.debugFiltering.isLoggable(Level.FINE)) {
1002 PrintInvariants.debugFiltering.fine(
1003 "isDPAU: name is " + name());
1004 PrintInvariants.debugFiltering.fine(
1005 " isPrestate is " + String.valueOf(isPrestate()));
1006 }
1007
1008 // Orig variables are not considered parameters. We only check the
1009 // first variable in a derivation because that is the sequence in
1010 // sequence-subscript or sequence-subsequence derivations and we don't
1011 // care if the index into the sequence is prestate or not.
1012 if (isPrestate() || (isDerived() && derived.getBases()[0].isPrestate())) {
1013 return false;
1014 }
1015
1016 if (isParam()) {
1017 PrintInvariants.debugFiltering.fine(
1018 " not interesting, IS_PARAM == true for "
1019 + name());
1020 return true;
1021 }
1022 if (Global.debugSuppressParam.isLoggable(Level.FINE)) {
1023 Global.debugSuppressParam.fine(
1024 "Testing isDerivedParamAndUninteresting for: " + name());
1025 Global.debugSuppressParam.fine(aux.toString());
1026 Global.debugSuppressParam.fine("At ppt " + ppt.name());
1027 }
1028 if (isDerivedParam()) {
1029 // I am uninteresting if I'm a derived param from X and X's
1030 // type or X's size, because these things are boring if X
1031 // changes (the default for the rest of the code here), and
1032 // boring if X stays the same (because it's obviously true).
1033 if (!FileIO.new_decl_format) {
1034 if (var_info_name instanceof VarInfoName.TypeOf) { // vin ok
1035 VarInfoName base = ((VarInfoName.TypeOf) var_info_name).term; // vin ok
1036 VarInfo baseVar = ppt.find_var_by_name (base.name());
1037 if ((baseVar != null) && baseVar.isParam()) {
1038 Global.debugSuppressParam.fine("TypeOf returning true");
1039 PrintInvariants.debugFiltering.fine(
1040 " not interesting, first dpf case");
1041 return true;
1042 }
1043 }
1044 if (var_info_name instanceof VarInfoName.SizeOf) { // vin ok
1045 VarInfoName base = ((VarInfoName.SizeOf) var_info_name).get_term(); // vin ok
1046 VarInfo baseVar = ppt.find_var_by_name (base.name());
1047 if (baseVar != null && baseVar.isParam()) {
1048 Global.debugSuppressParam.fine("SizeOf returning true");
1049 PrintInvariants.debugFiltering.fine(
1050 " not interesting, second dpf case");
1051 return true;
1052 }
1053 }
1054 } else { // new decl format
1055 assert enclosing_var != null : this;
1056
1057 // The class of a parameter can't change in the caller
1058 if (var_flags.contains (VarFlags.CLASSNAME) && enclosing_var.isParam())
1059 return true;
1060
1061 // The size of a parameter can't change in the caller. We shouldn't
1062 // have the shift==0 test, but need it to match the old code
1063 if (is_size() && (enclosing_var.get_base_array_hashcode().isParam())) {
1064 if (((SequenceLength) derived).shift == 0)
1065 return true;
1066 }
1067 }
1068
1069 VarInfo base = getDerivedParam();
1070 assert base != null : "can't find base for " + name();
1071 // Actually we should be getting all the derivations that could
1072 // be params, and if any of them are uninteresting, this is
1073 // uninteresting.
1074
1075 // Remember that if this is derived from a true param, then this
1076 // is a param too, so we don't need to worry. However, if this
1077 // is derived from a derivedParam, then we need to find all
1078 // derivation parents that could possibly fail under these
1079 // rules. Right now, we just get the first one.
1080
1081 // So if x = Foo(this.y, p.y) and this hasn't changed then we
1082 // will be ignoring the fact that y has changed.
1083
1084 // Henceforth only interesting if it's true that base = orig(base)
1085 if (base.name().equals("this"))
1086 return false;
1087 Global.debugSuppressParam.fine("Base is " + base.name());
1088 VarInfo origBase = ppt.find_var_by_name (base.prestate_name());
1089 if (origBase == null) {
1090 Global.debugSuppressParam.fine(
1091 "No orig variable for base, returning true ");
1092 PrintInvariants.debugFiltering.fine(
1093 " not interesting, no orig variable for base");
1094 return true; // There can't be an equal invariant without orig
1095 }
1096 if (base.isEqualTo(origBase)) {
1097 Global.debugSuppressParam.fine(
1098 "Saw equality. Derived worth printing.");
1099 return false;
1100 } else {
1101 Global.debugSuppressParam.fine(
1102 "Didn't see equality in base, so uninteresting");
1103 PrintInvariants.debugFiltering.fine(
1104 " didn't see equality in base");
1105 return true;
1106 }
1107
1108 } else {
1109 Global.debugSuppressParam.fine(" Not a derived param.");
1110 }
1111 return false;
1112 }
1113
1114 /** Convenience methods that return information from the ValueTuple. **/
1115 public int getModified(ValueTuple vt) {
1116 if (is_static_constant)
1117 // return ValueTuple.STATIC_CONSTANT;
1118 return ValueTuple.MODIFIED;
1119 else
1120 return vt.getModified(value_index);
1121 }
1122 public boolean isUnmodified(ValueTuple vt) {
1123 return ValueTuple.modIsUnmodified(getModified(vt));
1124 }
1125 public boolean isModified(ValueTuple vt) {
1126 return ValueTuple.modIsModified(getModified(vt));
1127 }
1128 public boolean isMissingNonsensical(ValueTuple vt) {
1129 return ValueTuple.modIsMissingNonsensical(getModified(vt));
1130 }
1131 public boolean isMissingFlow(ValueTuple vt) {
1132 return ValueTuple.modIsMissingFlow(getModified(vt));
1133 }
1134 public boolean isMissing(ValueTuple vt) {
1135 return isMissingNonsensical(vt) || isMissingFlow(vt);
1136 }
1137
1138 /**
1139 * Get the value of this variable from a particular sample (ValueTuple).
1140 * @param vt the ValueTuple from which to extract the value
1141 **/
1142 public /*@Interned*/ Object getValue(ValueTuple vt) {
1143 if (is_static_constant)
1144 return static_constant_value;
1145 else
1146 return vt.getValue(value_index);
1147 }
1148
1149 /** Use of this method is discouraged. */
1150 public /*@Nullable*/ /*@Interned*/ Object getValueOrNull(ValueTuple vt) {
1151 if (is_static_constant)
1152 return static_constant_value;
1153 else
1154 return vt.getValueOrNull(value_index);
1155 }
1156
1157 /** Return the value of this long variable (as an integer) **/
1158 public int getIndexValue(ValueTuple vt) {
1159 Object raw = getValue(vt);
1160 if (raw == null) {
1161 throw new Error(
1162 "getIndexValue: getValue returned null "
1163 + this.name()
1164 + " index="
1165 + this.varinfo_index
1166 + " vt="
1167 + vt);
1168 }
1169 return ((Long) raw).intValue();
1170 }
1171
1172 /** Return the value of this long variable (as a long) **/
1173 public long getIntValue(ValueTuple vt) {
1174 Object raw = getValue(vt);
1175 if (raw == null) {
1176 throw new Error(
1177 "getIntValue: getValue returned null "
1178 + this.name()
1179 + " index="
1180 + this.varinfo_index
1181 + " vt="
1182 + vt);
1183 }
1184 return ((Long) raw).longValue();
1185 }
1186
1187 /** Return the value of an long[] variable **/
1188 public long[] getIntArrayValue(ValueTuple vt) {
1189 Object raw = getValue(vt);
1190 if (raw == null) {
1191 throw new Error(
1192 "getIntArrayValue: getValue returned null "
1193 + this.name()
1194 + " index="
1195 + this.varinfo_index
1196 + " vt="
1197 + vt);
1198 }
1199 return (long[]) raw;
1200 }
1201
1202 /** Return the value of a double variable **/
1203 public double getDoubleValue(ValueTuple vt) {
1204 Object raw = getValue(vt);
1205 if (raw == null) {
1206 throw new Error(
1207 "getDoubleValue: getValue returned null "
1208 + this.name()
1209 + " index="
1210 + this.varinfo_index
1211 + " vt="
1212 + vt);
1213 }
1214 return ((Double) raw).doubleValue();
1215 }
1216
1217 /** Return the value of a double[] variable **/
1218 public double[] getDoubleArrayValue(ValueTuple vt) {
1219 Object raw = getValue(vt);
1220 if (raw == null) {
1221 throw new Error(
1222 "getDoubleArrayValue: getValue returned null "
1223 + this.name()
1224 + " index="
1225 + this.varinfo_index
1226 + " vt="
1227 + vt);
1228 }
1229 return (double[]) raw;
1230 }
1231
1232 /** Return the value of a String variable **/
1233 public String getStringValue(ValueTuple vt) {
1234 return (String) getValue(vt);
1235 }
1236
1237 /** Reteurn the value of a String[] array variable **/
1238 public String[] getStringArrayValue(ValueTuple vt) {
1239 Object raw = getValue(vt);
1240 if (raw == null) {
1241 throw new Error(
1242 "getDoubleArrayValue: getValue returned null "
1243 + this.name()
1244 + " index="
1245 + this.varinfo_index
1246 + " vt="
1247 + vt);
1248 }
1249 return (String[]) raw;
1250 }
1251
1252 static final class UsesVarFilter implements Filter<Invariant> {
1253 VarInfo var;
1254 public UsesVarFilter(VarInfo var) {
1255 this.var = var;
1256 }
1257 public boolean accept(Invariant inv) {
1258 return inv.usesVar(var);
1259 }
1260 }
1261
1262 /**
1263 * Whether this VarInfo is the leader of its equality set.
1264 **/
1265 public boolean isCanonical() {
1266 if (equalitySet == null)
1267 return true;
1268 return (equalitySet.leader() == this);
1269 }
1270
1271 /**
1272 * Canonical representative that's equal to this variable.
1273 **/
1274 public VarInfo canonicalRep() {
1275 if (equalitySet == null) {
1276 System.out.println("equality sets = " + ppt.equality_sets_txt());
1277 assert
1278 equalitySet != null
1279 : "Variable "
1280 + name()
1281 + " in ppt "
1282 + ppt.name()
1283 + " index = "
1284 + varinfo_index;
1285 }
1286 return equalitySet.leader();
1287 }
1288
1289 /**
1290 * Return true if this is a pointer or reference to another object.
1291 **/
1292 public boolean is_reference() {
1293
1294 // This used to check to see if the item was a list and some other
1295 // odd things, but hashcode seems like the right check.
1296 return rep_type.isHashcode();
1297 }
1298
1299 /**
1300 * Returns the VarInfo for the sequence from which this was derived,
1301 * or null if this wasn't derived from a sequence.
1302 * Only works for scalars.
1303 **/
1304 public /*@Nullable*/ VarInfo isDerivedSequenceMember() {
1305 if (derived == null)
1306 return null;
1307
1308 if (derived instanceof SequenceScalarSubscript) {
1309 SequenceScalarSubscript sss = (SequenceScalarSubscript) derived;
1310 return sss.seqvar();
1311 } else if (derived instanceof SequenceInitial) {
1312 SequenceInitial se = (SequenceInitial) derived;
1313 return se.seqvar();
1314 } else if (derived instanceof SequenceMax) {
1315 SequenceMax sm = (SequenceMax) derived;
1316 return sm.base;
1317 } else if (derived instanceof SequenceMin) {
1318 SequenceMin sm = (SequenceMin) derived;
1319 return sm.base;
1320 } else {
1321 return null;
1322 }
1323 }
1324
1325 public boolean isDerivedSequenceMinMaxSum() {
1326 return (
1327 (derived != null)
1328 && ((derived instanceof SequenceMax)
1329 || (derived instanceof SequenceMin)
1330 || (derived instanceof SequenceSum)));
1331 }
1332
1333 /**
1334 * Return the original sequence variable from which this derived sequence
1335 * was derived.
1336 * Only works for sequences.
1337 **/
1338 public /*@Nullable*/ VarInfo isDerivedSubSequenceOf() {
1339
1340 if (derived == null)
1341 return null;
1342
1343 if (derived instanceof SequenceScalarSubsequence) {
1344 SequenceScalarSubsequence sss = (SequenceScalarSubsequence) derived;
1345 return sss.seqvar();
1346 } else if (derived instanceof SequenceScalarArbitrarySubsequence) {
1347 SequenceScalarArbitrarySubsequence ssas =
1348 (SequenceScalarArbitrarySubsequence) derived;
1349 return ssas.seqvar();
1350 } else {
1351 return null;
1352 }
1353 }
1354
1355 /** Returns the variable (if any) that represents the size of this sequence **/
1356 public /*@Nullable*/ VarInfo sequenceSize() {
1357 if (sequenceSize != null)
1358 return sequenceSize;
1359 assert rep_type.isArray();
1360 // we know the size follows the variable itself in the list
1361 VarInfo[] vis = ppt.var_infos;
1362 for (int i = varinfo_index + 1; i < vis.length; i++) {
1363 VarInfo vi = vis[i];
1364 if ((vi.derived instanceof SequenceLength)
1365 && (((SequenceLength) vi.derived).base == this)) {
1366 sequenceSize = vi;
1367 return sequenceSize;
1368 }
1369 }
1370 // It is possible that this VarInfo never had its size derived,
1371 // since it looked something like this.ary[].field. In this case,
1372 // we should return size(this.ary[]), since it was derived and
1373 // must be the same values.
1374 if (FileIO.new_decl_format) {
1375 VarInfo base = get_base_array();
1376 VarInfo size = ppt.find_var_by_name ("size(" + base.name() + ")");
1377 return size;
1378 } else {
1379 VarInfoName search = this.var_info_name; // vin ok
1380 boolean pre = false;
1381 if (search instanceof VarInfoName.Prestate) {
1382 search = ((VarInfoName.Prestate) search).term;
1383 pre = true;
1384 }
1385 while (search instanceof VarInfoName.Field) {
1386 search = ((VarInfoName.Field) search).term;
1387 }
1388 if (pre) {
1389 search = search.applyPrestate();
1390 }
1391 search = search.applySize();
1392 VarInfo result = ppt.find_var_by_name (search.name());
1393 if (result != null) {
1394 return result;
1395 // } else {
1396 // System.out.println("Warning: Size variable " + search + " not found.");
1397 // System.out.print("Variables: ");
1398 // for (int i=0; i<ppt.var_infos.length; i++) {
1399 // VarInfo vi = ppt.var_infos[i];
1400 // System.out.print(vi.name + " ");
1401 // }
1402 // System.out.println();
1403 }
1404 }
1405 // throw new Error("Couldn't find size of " + name);
1406 return null;
1407 }
1408
1409 /**
1410 * Returns true if the type in the original program is integer.
1411 * Should perhaps check Daikon.check_program_types and behave differently
1412 * depending on that.
1413 */
1414 public boolean isIndex() {
1415 return ((file_rep_type == ProglangType.INT) && type.isIndex());
1416 }
1417
1418 public boolean is_array() {
1419 if (FileIO.new_decl_format)
1420 return (arr_dims > 0);
1421 else
1422 return rep_type.isArray();
1423 }
1424
1425 /**
1426 * @return false if this variable expression is not legal ESC
1427 * syntax, except for any necessary quantifications (subscripting).
1428 * We err on the side of returning true, for now.
1429 **/
1430 public boolean isValidEscExpression() {
1431 // "myVector.length" is invalid
1432 boolean is_length = (derived instanceof SequenceLength);
1433 boolean is_array_length =
1434 is_length && ((SequenceLength) derived).base.type.isArray();
1435 if (is_length && (!is_array_length)) {
1436 return false;
1437 }
1438
1439 // "myVector[]" is invalid, as is myVector[foo] (when myVector is a list
1440 // of some sort and not an array)
1441 if (FileIO.new_decl_format) {
1442 for (VarInfo vi = this; vi != null; vi = vi.enclosing_var) {
1443 if (vi.file_rep_type.isArray() && !vi.type.isArray())
1444 return false;
1445 if (vi.isDerived()) {
1446 VarInfo base = vi.derived.getBases()[0];
1447 if (base.file_rep_type.isArray() && !base.type.isArray())
1448 return false;
1449 }
1450 }
1451 } else {
1452 for (VarInfoName next : var_info_name.inOrderTraversal()) { // vin ok
1453 if (next instanceof VarInfoName.Elements) {
1454 VarInfoName.Elements elems = (VarInfoName.Elements) next;
1455 VarInfo seq = ppt.find_var_by_name (elems.term.name());
1456 if (!seq.type.isArray()) {
1457 return false;
1458 }
1459 }
1460 }
1461 }
1462
1463 return true;
1464 }
1465
1466 /**
1467 * Return true if invariants about this quantity are really
1468 * properties of a pointer, but derived variables can refer to
1469 * properties of the thing pointed to. This distinction is important
1470 * when making logical statements about the object, because in the
1471 * presence of side effects, the pointed-to object can change even
1472 * when the pointer doesn't. For instance, we might have "obj ==
1473 * orig(obj)", but "obj.color != orig(obj.color)". In such a case,
1474 * isPointer() would be true of obj, and for some forms of output
1475 * we'd need to translate "obj == orig(obj)" into something like
1476 * "location(obj) == location(orig(obj))".
1477 */
1478 public boolean isPointer() {
1479 // This used to check whether the program type had a higher
1480 // dimension than the rep type, or if the rep type was integral
1481 // but the program type wasn't primitive. These rules worked
1482 // pretty well for Java, but not so well for C, where for instance
1483 // you might have rep_type = int and type = size_t.
1484
1485 return file_rep_type.isPointerFileRep();
1486 }
1487
1488 /**
1489 * A wrapper around VarInfoName.simplify_name() that also uses
1490 * VarInfo information to guess whether "obj" should logically be
1491 * treated as just the hash code of "obj", rather than the whole
1492 * object.
1493 **/
1494 public String simplifyFixup(String str) {
1495 if (isPointer()) {
1496 str = "(hash " + str + ")";
1497 }
1498 return str;
1499 }
1500
1501 public String simplifyFixedupName() {
1502 return simplifyFixup(simplify_name());
1503 }
1504
1505 ///////////////////////////////////////////////////////////////////////////
1506 /// Utility functions
1507 ///
1508
1509 // Where do these really belong?
1510
1511 /**
1512 * Given two variables I and J, indicate whether it is necessarily the
1513 * case that i<=j or i>=j. The variables also each have a shift, so the
1514 * test can really be something like (i+1)<=(j-1).
1515 * The test is either: i + i_shift <= j + j_shift (if test_lessequal)
1516 * i + i_shift >= j + j_shift (if !test_lessequal)
1517 * This is a dynamic check, and so must not be called while Daikon is
1518 * inferencing.
1519 **/
1520 public static boolean compare_vars(
1521 VarInfo vari,
1522 int vari_shift,
1523 VarInfo varj,
1524 int varj_shift,
1525 boolean test_lessequal) {
1526
1527 // System.out.printf ("comparing variables %s and %s in ppt %s%n",
1528 // vari.name(), varj.name(), vari.ppt.name());
1529 // Throwable stack = new Throwable("debug traceback");
1530 // stack.fillInStackTrace();
1531 // stack.printStackTrace();
1532
1533 assert !Daikon.isInferencing;
1534 // System.out.println("compare_vars(" + vari.name + ", " + vari_shift + ", "+ varj.name + ", " + varj_shift + ", " + (test_lessequal?"<=":">=") + ")");
1535 if (vari == varj) {
1536 // same variable
1537 return (
1538 test_lessequal
1539 ? (vari_shift <= varj_shift)
1540 : (vari_shift >= varj_shift));
1541 }
1542 // different variables
1543 @SuppressWarnings("interning") // assertion (PptTopLevel)
1544 boolean samePpt = (vari.ppt == varj.ppt);
1545 assert samePpt;
1546 PptSlice indices_ppt = vari.ppt.findSlice_unordered(vari, varj);
1547 if (indices_ppt == null)
1548 return false;
1549
1550 boolean vari_is_var1 = (vari == indices_ppt.var_infos[0]);
1551 LinearBinary lb = LinearBinary.find(indices_ppt);
1552 long index_vari_minus_seq = -2222; // valid only if lb != null
1553 if (lb != null) {
1554 if (!lb.enoughSamples()) {
1555 lb = null;
1556 } else if (lb.core.a != 1 || lb.core.b != -1 ) {
1557 // Do not attempt to deal with anything but y=x+b, aka x-y+b=0.
1558 lb = null;
1559 } else {
1560 // System.out.println("justified LinearBinary: " + lb.format());
1561 // lb.b is var2()-var1().
1562
1563 // a is 1 or -1, and the values are integers, so c must be an integer
1564 long c_int = (long) lb.core.c;
1565 assert lb.core.c == c_int;
1566 index_vari_minus_seq = (vari_is_var1 ? -c_int : c_int);
1567 index_vari_minus_seq += vari_shift - varj_shift;
1568 }
1569 }
1570
1571 boolean vari_lt = false;
1572 boolean vari_le = false;
1573 boolean vari_gt = false;
1574 boolean vari_ge = false;
1575 {
1576 IntLessEqual ile = IntLessEqual.find(indices_ppt);
1577 IntLessThan ilt = IntLessThan.find(indices_ppt);
1578 IntGreaterEqual ige = IntGreaterEqual.find(indices_ppt);
1579 IntGreaterThan igt = IntGreaterThan.find(indices_ppt);
1580 if (ile != null && !ile.enoughSamples()) {
1581 ile = null;
1582 }
1583 if (ilt != null && !ilt.enoughSamples()) {
1584 ilt = null;
1585 }
1586 if (ige != null && !ige.enoughSamples()) {
1587 ige = null;
1588 }
1589 if (igt != null && !igt.enoughSamples()) {
1590 igt = null;
1591 }
1592
1593 if (vari_is_var1) {
1594 vari_lt = ilt != null;
1595 vari_le = ile != null;
1596 vari_gt = igt != null;
1597 vari_ge = ige != null;
1598 } else {
1599 vari_lt = igt != null;
1600 vari_le = ige != null;
1601 vari_gt = ilt != null;
1602 vari_ge = ile != null;
1603 }
1604 }
1605
1606 // System.out.println("test_lessequal=" + test_lessequal
1607 // + ", vari_can_be_lt=" + vari_can_be_lt
1608 // + ", vari_can_be_eq=" + vari_can_be_eq
1609 // + ", vari_can_be_gt=" + vari_can_be_gt);
1610
1611 if (test_lessequal) {
1612 if (lb != null) {
1613 return (index_vari_minus_seq <= 0);
1614 } else {
1615 return (
1616 (vari_le && (vari_shift <= varj_shift))
1617 || (vari_lt && (vari_shift - 1 <= varj_shift)));
1618 }
1619 } else {
1620 if (lb != null) {
1621 return (index_vari_minus_seq >= 0);
1622 } else {
1623 return (
1624 (vari_ge && (vari_shift >= varj_shift))
1625 || (vari_gt && (vari_shift + 1 >= varj_shift)));
1626 }
1627 }
1628 }
1629
1630 // // takes an "orig()" var and gives a VarInfoName for a variable or
1631 // // expression in the post-state which is equal to this one.
1632 // public VarInfoName postStateEquivalent() {
1633 // return otherStateEquivalent(true);
1634 // }
1635
1636 // takes a non-"orig()" var and gives a VarInfoName for a variable
1637 // or expression in the pre-state which is equal to this one.
1638 public VarInfoName preStateEquivalent() {
1639 return otherStateEquivalent(false);
1640 }
1641
1642 /**
1643 * Return some variable in the other state (pre-state if this is
1644 * post-state, or vice versa) that equals this one, or null if no equal
1645 * variable exists.
1646 **/
1647 // This does *not* try the obvious thing of converting "foo" to
1648 // "orig(foo)"; it creates something new. I need to clarify the
1649 // documentation.
1650 public /*@Nullable*/ VarInfoName otherStateEquivalent(boolean post) {
1651
1652 assert !FileIO.new_decl_format;
1653
1654 // Below is equivalent to:
1655 // assert post == isPrestate();
1656 if (post != isPrestate()) {
1657 throw new Error("Shouldn't happen (should it?): "
1658 + (post ? "post" : "pre") + "StateEquivalent("
1659 + name() + ")");
1660 }
1661
1662 {
1663 Vector<LinearBinary> lbs = LinearBinary.findAll(this);
1664 for (LinearBinary lb : lbs) {
1665 if (this.equals(lb.var2())
1666 && (post != lb.var1().isPrestate())) {
1667
1668 // a * v1 + b * this + c = 0 or this == (-a/b) * v1 - c/b
1669 double a = lb.core.a, b = lb.core.b, c = lb.core.c;
1670 // if (a == 1) {
1671 if (-a/b == 1) {
1672 // this = v1 - c/b
1673 // int add = (int) b;
1674 int add = (int) -c/(int)b;
1675 return lb.var1().var_info_name.applyAdd(add); // vin ok
1676 }
1677 }
1678
1679 if (this.equals(lb.var1())
1680 && (post != lb.var2().isPrestate())) {
1681 // v2 = a * this + b <-- not true anymore
1682 // a * this + b * v2 + c == 0 or v2 == (-a/b) * this - c/b
1683 double a = lb.core.a, b = lb.core.b, c = lb.core.c;
1684 //if (a == 1) {
1685 if (-a/b == 1) {
1686 // this = v2 + c/b
1687 //int add = - ((int) b);
1688 int add = (int) c/(int) b;
1689 return lb.var2().var_info_name.applyAdd(add); // vin ok
1690 }
1691 }
1692 }
1693
1694
1695 // Should also try other exact invariants...
1696 }
1697
1698 // Can't find post-state equivalent.
1699 return null;
1700 }
1701
1702 /**
1703 * Check if two VarInfos are truly (non guarded) equal to each other
1704 * right now.
1705 **/
1706 @SuppressWarnings("interning") // Equality
1707 public boolean isEqualTo(VarInfo other) {
1708 assert equalitySet != null;
1709 return this.equalitySet == other.equalitySet;
1710 }
1711
1712 /** Debug tracer. **/
1713 private static final Logger debug = Logger.getLogger("daikon.VarInfo");
1714
1715 /** Debug tracer for simplifying expressions. **/
1716 private static final Logger debugSimplifyExpression =
1717 Logger.getLogger("daikon.VarInfo.simplifyExpression");
1718
1719 /**
1720 * Change the name of this VarInfo by side effect into a more simplified
1721 * form, which is easier to read on display. Don't call this during
1722 * processing, as I think the system assumes that names don't change
1723 * over time (?).
1724 **/
1725 public void simplify_expression() {
1726 if (debugSimplifyExpression.isLoggable(Level.FINE))
1727 debugSimplifyExpression.fine("** Simplify: " + name());
1728
1729 if (!isDerived()) {
1730 if (debugSimplifyExpression.isLoggable(Level.FINE))
1731 debugSimplifyExpression.fine(
1732 "** Punt because not derived variable");
1733 return;
1734 }
1735
1736 // find a ...post(...)... expression to simplify
1737 VarInfoName.Poststate postexpr = null;
1738 for (VarInfoName node : (new VarInfoName.InorderFlattener(var_info_name)).nodes()) { // vin ok
1739 if (node instanceof VarInfoName.Poststate) {
1740 // Remove temporary var when bug is fixed.
1741 VarInfoName.Poststate tempNode = (VarInfoName.Poststate) node;
1742 postexpr = tempNode;
1743 // old code; reinstate when bug is fixed
1744 // postexpr = (VarInfoName.Poststate) node;
1745 break;
1746 }
1747 }
1748 if (postexpr == null) {
1749 if (debugSimplifyExpression.isLoggable(Level.FINE))
1750 debugSimplifyExpression.fine("** Punt because no post()");
1751 return;
1752 }
1753
1754 // if we have post(...+k) rewrite as post(...)+k
1755 if (postexpr.term instanceof VarInfoName.Add) {
1756 VarInfoName.Add add = (VarInfoName.Add) postexpr.term;
1757 VarInfoName swapped =
1758 add.term.applyPoststate().applyAdd(add.amount);
1759 var_info_name = (new VarInfoName.Replacer(postexpr, swapped)).replace(var_info_name).intern(); // vin ok // interning bugfix
1760 // start over
1761 simplify_expression();
1762 return;
1763 }
1764
1765 // Stop now if we don't want to replace post vars with equivalent orig
1766 // vars
1767 if (!PrintInvariants.dkconfig_remove_post_vars)
1768 return;
1769
1770 // [[ find the ppt context for the post() term ]] (I used to
1771 // search the expression for this, but upon further reflection,
1772 // there is only one EXIT point which could possibly be associated
1773 // with this VarInfo, so "this.ppt" must be correct.
1774 PptTopLevel post_context = this.ppt;
1775
1776 // see if the contents of the post(...) have an equivalent orig()
1777 // expression.
1778 VarInfo postvar = post_context.find_var_by_name (postexpr.term.name());
1779 if (postvar == null) {
1780 if (debugSimplifyExpression.isLoggable(Level.FINE))
1781 debugSimplifyExpression.fine(
1782 "** Punt because no VarInfo for postvar " + postexpr.term);
1783 return;
1784 }
1785 VarInfoName pre_expr = postvar.preStateEquivalent();
1786 if (pre_expr != null) {
1787 // strip off any orig() so we don't get orig(a[orig(i)])
1788 if (pre_expr instanceof VarInfoName.Prestate) {
1789 pre_expr = ((VarInfoName.Prestate) pre_expr).term;
1790 } else if (pre_expr instanceof VarInfoName.Add) {
1791 VarInfoName.Add add = (VarInfoName.Add) pre_expr;
1792 if (add.term instanceof VarInfoName.Prestate) {
1793 pre_expr =
1794 ((VarInfoName.Prestate) add.term).term.applyAdd(
1795 add.amount);
1796 }
1797 }
1798 var_info_name = (new VarInfoName.Replacer(postexpr, pre_expr)).replace(var_info_name).intern(); // vin ok // interning bugfix
1799 if (debugSimplifyExpression.isLoggable(Level.FINE))
1800 debugSimplifyExpression.fine("** Replaced with: " + var_info_name); // vin ok
1801 }
1802
1803 if (debugSimplifyExpression.isLoggable(Level.FINE))
1804 debugSimplifyExpression.fine(
1805 "** Nothing to do (no state equlivalent)");
1806 }
1807
1808 /**
1809 * Two variables are "compatible" if their declared types are
1810 * castable and their comparabilities are comparable. This is a
1811 * reflexive relationship, because it calls
1812 * ProglangType.comparableOrSuperclassEitherWay. However, it is not
1813 * transitive because it might not hold for two children of a
1814 * superclass, even though it would for each child and the superclass.
1815 **/
1816 public boolean compatible(VarInfo var2) {
1817 VarInfo var1 = this;
1818 // Can only compare in the same ppt because otherwise
1819 // comparability info may not make sense.
1820 @SuppressWarnings("interning") // assertion (PptTopLevel)
1821 boolean samePpt = (var1.ppt == var2.ppt);
1822 assert samePpt;
1823
1824 if (!comparableByType(var2)) {
1825 return false;
1826 }
1827
1828 if ((!Daikon.ignore_comparability)
1829 && (!VarComparability.comparable(var1, var2))) {
1830 return false;
1831 }
1832
1833 return true;
1834 }
1835
1836 /**
1837 * Return true if this sequence variable's element type is compatible
1838 * with the scalar variable.
1839 **/
1840 public boolean eltsCompatible(VarInfo sclvar) {
1841 VarInfo seqvar = this;
1842 if (Daikon.check_program_types) {
1843 ProglangType elttype = seqvar.type.elementType();
1844 if (!elttype.comparableOrSuperclassEitherWay(sclvar.type)) {
1845 // System.out.printf("eltsCompatible: bad program types; elttype(%s)=%s, scltype(%s)=%s%n",
1846 // seqvar, elttype, sclvar, sclvar.type);
1847 return false;
1848 }
1849 }
1850 if (!Daikon.ignore_comparability) {
1851 if (!VarComparability.comparable(seqvar.comparability.elementType(),
1852 sclvar.comparability)) {
1853 // System.out.printf("eltsCompatible: eltcomp(%s;%s)=%s, sclcomp(%s)=%s%n",
1854 // seqvar, seqvar.comparability.elementType(), seqvar.comparability.elementType(), sclvar, sclvar.comparability);
1855 return false;
1856 }
1857 }
1858 return true;
1859 }
1860
1861 /**
1862 * Without using comparability info, check that this is comparable
1863 * to var2. This is a reflexive relationship, because it calls
1864 * ProglangType.comparableOrSuperclassEitherWay. However, it is not
1865 * transitive because it might not hold for two children of a
1866 * superclass, even though it would for each child and the
1867 * superclass. Does not check comparabilities.
1868 **/
1869 public boolean comparableByType(VarInfo var2) {
1870 VarInfo var1 = this;
1871
1872 // System.out.printf("comparableByType(%s, %s)%n", var1, var2);
1873
1874 // the check ensures that a scalar or string and elements of an array of the same type are
1875 // labelled as comparable
1876 if (Daikon.check_program_types && (var1.file_rep_type.isArray() && !var2.file_rep_type.isArray())) {
1877
1878 // System.out.printf("comparableByType: case 1 %s%n", var1.eltsCompatible(var2));
1879 if (var1.eltsCompatible(var2))
1880 return true;
1881 }
1882
1883 // the check ensures that a scalar or string and elements of an array of the same type are
1884 // labelled as comparable
1885 if (Daikon.check_program_types && (!var1.file_rep_type.isArray() && var2.file_rep_type.isArray())) {
1886
1887 // System.out.printf("comparableByType: case 2 %s%n", var2.eltsCompatible(var1));
1888 if (var2.eltsCompatible(var1))
1889 return true;
1890
1891 }
1892
1893 if (Daikon.check_program_types
1894 && (var1.file_rep_type != var2.file_rep_type)) {
1895 // System.out.printf("comparableByType: case 4 return false%n");
1896 return false;
1897 }
1898
1899 // If the file rep types match then the variables are comparable unless
1900 // their dimensions are different.
1901 if (!dkconfig_declared_type_comparability) {
1902 if (var1.type.dimensions() != var2.type.dimensions()) {
1903 // debug_print_once ("types %s and %s are not comparable",
1904 // var1.type, var2.type);
1905 return (false);
1906 }
1907 return (true);
1908 }
1909
1910
1911 if (Daikon.check_program_types
1912 && (!var1.type.comparableOrSuperclassEitherWay(var2.type))) {
1913 // debug_print_once ("types %s and %s are not comparable",
1914 // var1.type, var2.type);
1915 return false;
1916 }
1917 // debug_print_once ("types %s and %s are comparable",
1918 // var1.type, var2.type);
1919
1920 // System.out.printf("comparableByType: fallthough return true%n");
1921 return true;
1922 }
1923
1924 /**
1925 * Without using comparability info, check that this is comparable
1926 * to var2. This is a reflexive and transitive relationship. Does
1927 * not check comparabilities.
1928 **/
1929 public boolean comparableNWay(VarInfo var2) {
1930 VarInfo var1 = this;
1931 if (Daikon.check_program_types
1932 && (!var1.type.comparableOrSuperclassOf(var2.type))) {
1933 return false;
1934 }
1935 if (Daikon.check_program_types
1936 && (!var2.type.comparableOrSuperclassOf(var1.type))) {
1937 return false;
1938 }
1939 if (Daikon.check_program_types
1940 && (var1.file_rep_type != var2.file_rep_type)) {
1941 return false;
1942 }
1943 return true;
1944 }
1945
1946 /**
1947 * Return true if this sequence's first index type is compatible
1948 * with the scalar variable.
1949 **/
1950 public boolean indexCompatible(VarInfo sclvar) {
1951 VarInfo seqvar = this;
1952 if (Daikon.check_program_types) {
1953 if (!seqvar.is_array() || !sclvar.isIndex()) {
1954 return false;
1955 }
1956 }
1957 if (!Daikon.ignore_comparability) {
1958 if (!VarComparability
1959 .comparable(
1960 seqvar.comparability.indexType(0),
1961 sclvar.comparability)) {
1962 return false;
1963 }
1964 }
1965 return true;
1966 }
1967
1968 // Interning is lost when an object is serialized and deserialized.
1969 // Manually re-intern any interned fields upon deserialization.
1970 private void readObject(ObjectInputStream in)
1971 throws IOException, ClassNotFoundException {
1972 in.defaultReadObject();
1973 var_info_name = var_info_name.intern(); // vin ok
1974 str_name = str_name.intern();
1975 }
1976
1977 // /**
1978 // * It is <b>not</b> safe in general to compare based on VarInfoName
1979 // * alone, because it is possible for two different program points to have
1980 // * unrelated variables of the same name.
1981 // **/
1982 // public static class LexicalComparator implements Comparator<VarInfo> {
1983 // public int compare(VarInfo vi1, VarInfo vi2) {
1984 // VarInfoName name1 = vi1.name;
1985 // VarInfoName name2 = vi2.name;
1986 // return name1.compareTo(name2);
1987 // }
1988 // }
1989
1990 /**
1991 * Create a guarding predicate for this VarInfo, that is, an
1992 * invariant that ensures that this object is available for access
1993 * to variables that reference it, such as fields.
1994 * (The invariant is placed in the appropriate slice.)
1995 * Returns null if no guarding is needed.
1996 **/
1997 // Adding a test against null is not quite right for C programs, where *p
1998 // could be nonsensical (uninitialized or freed) even when p is non-null.
1999 // But this is a decent approximation to start with.
2000 public /*@Nullable*/ Invariant createGuardingPredicate(boolean install) {
2001 // Later for the array, make sure index in bounds
2002 if (! (type.isArray() || type.isObject())) {
2003 String message = String.format
2004 ("Unexpected guarding based on %s with type %s%n", name(), type);
2005 System.err.printf(message);
2006 throw new Error(message);
2007 }
2008
2009 // For now associating with the variable's PptSlice
2010 PptSlice slice = ppt.get_or_instantiate_slice(this);
2011
2012 Invariant result;
2013 Class<NonZero> NonZero_class;
2014 try {
2015 @SuppressWarnings("unchecked")
2016 Class<NonZero> NonZero_class_tmp = (Class<NonZero>) Class.forName("daikon.inv.unary.scalar.NonZero");
2017 NonZero_class = NonZero_class_tmp;
2018 } catch (ClassNotFoundException e) {
2019 throw new Error("Could not locate class object for daikon.inv.unary.scalar.NonZero");
2020 }
2021 // result = Invariant.find(NonZero_class, slice);
2022 result = Invariant.find(NonZero.class, slice);
2023
2024 // Check whether the predicate already exists
2025 if (result == null) {
2026 // If it doesn't, create a "fake" invariant, which should
2027 // never be printed. Is it a good idea even to set
2028 // result.falsified to true? We know it's true because
2029 // result's children were missing. However, some forms of
2030 // filtering might remove it from slice.
2031 VarInfo[] vis = slice.var_infos;
2032 if (SingleScalar.valid_types_static(vis)) {
2033 result = NonZero.get_proto().instantiate(slice);
2034 } else if (SingleScalarSequence.valid_types_static(vis)) {
2035 result = EltNonZero.get_proto().instantiate(slice);
2036 } else {
2037 throw new Error("Bad VarInfos");
2038 }
2039 if (result == null)
2040 // Return null if NonZero invariant is not applicable to this variable.
2041 return null;
2042 result.isGuardingPredicate = true;
2043 // System.out.printf("Created a guarding predicate: %s at %s%n", result, slice);
2044 // new Error().printStackTrace(System.out);
2045 if (install) {
2046 slice.addInvariant(result);
2047 }
2048 }
2049
2050 return result;
2051 }
2052
2053
2054 static Set<String> addVarMessages = new HashSet<String>();
2055
2056 /**
2057 * Finds a list of variables that must be guarded for a VarInfo to be
2058 * guaranteed to not be missing. This list never includes "this", as it
2059 * can never be null. The variables are returned in the order in which
2060 * their guarding prefixes are supposed to print.
2061 **/
2062 public List<VarInfo> getGuardingList() {
2063
2064 /**
2065 * The list returned by this visitor always includes the argument
2066 * itself (if it is testable against null; for example, derived
2067 * variables are not).
2068 * If the caller does not want the argument to be in the list, the
2069 * caller must must remove the argument.
2070 **/
2071 // Inner class because it uses the "ppt" variable.
2072 // Basic structure of each visitor:
2073 // If the argument should be guarded, recurse.
2074 // If the argument is testable against null, add it to the result.
2075 // Recursing first arranges that the argument goes at the end,
2076 // after its subparts that need to be guarded.
2077
2078 class GuardingVisitor implements Visitor<List<VarInfo>> {
2079 boolean inPre = false;
2080
2081 private boolean shouldBeGuarded(VarInfo vi) {
2082 assert vi != null;
2083 boolean result
2084 = (vi != null
2085 && (Daikon.dkconfig_guardNulls == "always" // interned
2086 || (Daikon.dkconfig_guardNulls == "missing" // interned
2087 && vi.canBeMissing)));
2088 if (Invariant.debugGuarding.isLoggable(Level.FINE))
2089 Invariant.debugGuarding.fine
2090 (String.format("shouldBeGuarded(%s) %b %b", vi, result,
2091 vi.canBeMissing));
2092 return result;
2093 }
2094 private boolean shouldBeGuarded(VarInfoName viname) {
2095 // Not "shouldBeGuarded(ppt.findVar(viname))" because that
2096 // unnecessarily computes ppt.findVar(viname), if
2097 // dkconfig_guardNulls is "always".
2098 //System.out.printf ("viname = %s, applyPreMaybe=%s, findvar=%s%n",
2099 // viname, applyPreMaybe(viname),
2100 // ppt.findVar(applyPreMaybe(viname)));
2101 if (Daikon.dkconfig_guardNulls == "always") // interned
2102 return (true);
2103 if (Daikon.dkconfig_guardNulls == "missing") { // interned
2104 VarInfo vi = ppt.find_var_by_name(applyPreMaybe(viname).name());
2105 // Don't guard variables that don't exist. This happends when
2106 // we incorrectly parse static variable package names as field names
2107 if (Invariant.debugGuarding.isLoggable(Level.FINE))
2108 Invariant.debugGuarding.fine
2109 (String.format("shouldBeGuarded(%s) [%s] %s %b", viname,
2110 applyPreMaybe(viname), vi,
2111 ((vi == null) ? false :vi.canBeMissing)));
2112 if (vi == null)
2113 return false;
2114 return (vi.canBeMissing);
2115 }
2116 return false;
2117
2118 }
2119 public List<VarInfo> visitSimple(Simple o) {
2120 List<VarInfo> result = new ArrayList<VarInfo>();
2121 // No recursion: no children
2122 if (! o.name.equals("this")) {
2123 result = addVar(result, o);
2124 }
2125 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2126 Invariant.debugGuarding.fine(String.format("visitSimple(%s) => %s", o.name(), result));
2127 }
2128 return result;
2129 }
2130 public List<VarInfo> visitSizeOf(SizeOf o) {
2131 List<VarInfo> result = new ArrayList<VarInfo>();
2132 if (shouldBeGuarded(o)) {
2133 result.addAll(o.sequence.accept(this));
2134 }
2135 // No call to addVar: derived variable
2136 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2137 Invariant.debugGuarding.fine(String.format("visitSizeOf(%s) => %s", o.name(), result));
2138 }
2139 return result;
2140 }
2141 public List<VarInfo> visitFunctionOf(FunctionOf o) {
2142 List<VarInfo> result = new ArrayList<VarInfo>();
2143 if (shouldBeGuarded(o)) {
2144 result.addAll(o.argument.accept(this));
2145 }
2146 result = addVar(result, o);
2147 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2148 Invariant.debugGuarding.fine(String.format("visitFunctionOf(%s) => %s", o.name(), result));
2149 }
2150 return result;
2151 }
2152 public List<VarInfo> visitFunctionOfN(FunctionOfN o) {
2153 List<VarInfo> result = new ArrayList<VarInfo>();
2154 if (shouldBeGuarded(o)) {
2155 for (VarInfoName arg : o.args) {
2156 result.addAll(arg.accept(this));
2157 }
2158 }
2159 result = addVar(result, o);
2160 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2161 Invariant.debugGuarding.fine(String.format("visitFunctionOfN(%s) => %s", o.name(), result));
2162 }
2163 return result;
2164 }
2165 public List<VarInfo> visitField(Field o) {
2166 List<VarInfo> result = new ArrayList<VarInfo>();
2167 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2168 Invariant.debugGuarding.fine(String.format("visitField: shouldBeGuarded(%s) => %s", o.name(), shouldBeGuarded(o)));
2169 }
2170 if (shouldBeGuarded(o)) {
2171 result.addAll(o.term.accept(this));
2172 }
2173 result = addVar(result, o);
2174 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2175 Invariant.debugGuarding.fine(String.format("visitField(%s) => %s", o.name(), result));
2176 }
2177 return result;
2178 }
2179 public List<VarInfo> visitTypeOf(TypeOf o) {
2180 List<VarInfo> result = new ArrayList<VarInfo>();
2181 if (shouldBeGuarded(o)) {
2182 result.addAll(o.term.accept(this));
2183 }
2184 // No call to addVar: derived variable
2185 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2186 Invariant.debugGuarding.fine(String.format("visitTypeOf(%s) => %s", o.name(), result));
2187 }
2188 return result;
2189 }
2190 public List<VarInfo> visitPrestate(Prestate o) {
2191 assert inPre == false;
2192 inPre = true;
2193 List<VarInfo> result = o.term.accept(this);
2194 assert inPre == true;
2195 inPre = false;
2196 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2197 Invariant.debugGuarding.fine(String.format("visitPrestate(%s) => %s", o.name(), result));
2198 }
2199 return result;
2200 }
2201 public List<VarInfo> visitPoststate(Poststate o) {
2202 assert inPre == true;
2203 inPre = false;
2204 List<VarInfo> result = o.term.accept(this);
2205 assert inPre == false;
2206 inPre = true;
2207 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2208 Invariant.debugGuarding.fine(String.format("visitPostState(%s) => %s", o.name(), result));
2209 }
2210 return result;
2211 }
2212 public List<VarInfo> visitAdd(Add o) {
2213 List<VarInfo> result = new ArrayList<VarInfo>();
2214 if (shouldBeGuarded(o)) {
2215 result.addAll(o.term.accept(this));
2216 }
2217 // No call to addVar: derived variable
2218 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2219 Invariant.debugGuarding.fine(String.format("visitAdd(%s) => %s", o.name(), result));
2220 }
2221 return result;
2222 }
2223 public List<VarInfo> visitElements(Elements o) {
2224 List<VarInfo> result = new ArrayList<VarInfo>();
2225 if (shouldBeGuarded(o)) {
2226 result.addAll(o.term.accept(this));
2227 }
2228 // No call to addVar: derived variable
2229 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2230 Invariant.debugGuarding.fine(String.format("visitElements(%s) => %s", o.name(), result));
2231 }
2232 return result;
2233 }
2234 public List<VarInfo> visitSubscript(Subscript o) {
2235 List<VarInfo> result = new ArrayList<VarInfo>();
2236 if (shouldBeGuarded(o)) {
2237 result.addAll(o.sequence.accept(this));
2238 result.addAll(o.index.accept(this));
2239 }
2240 result = addVar(result, o);
2241 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2242 Invariant.debugGuarding.fine(String.format("visitSubscript(%s) => %s", o.name(), result));
2243 }
2244 return result;
2245 }
2246 public List<VarInfo> visitSlice(Slice o) {
2247 List<VarInfo> result = new ArrayList<VarInfo>();
2248 if (shouldBeGuarded(o)) {
2249 result.addAll(o.sequence.accept(this));
2250 if (o.i != null)
2251 result.addAll(o.i.accept(this));
2252 if (o.j != null)
2253 result.addAll(o.j.accept(this));
2254 }
2255 // No call to addVar: derived variable
2256 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2257 Invariant.debugGuarding.fine(String.format("visitSlice(%s) => %s", o.name(), result));
2258 }
2259 return result;
2260 }
2261
2262 // Convert to prestate variable name if appropriate
2263 VarInfoName applyPreMaybe(VarInfoName vin) {
2264 if (inPre)
2265 return vin.applyPrestate();
2266 else
2267 return vin;
2268 }
2269
2270 private VarInfo convertToPre(VarInfo vi) {
2271 // 1. "ppt.findVar("orig(" + vi.name() + ")")" does not work:
2272 // "Error: orig() variables shouldn't appear in .decls files"
2273
2274 VarInfoName viPreName = vi.var_info_name.applyPrestate(); // vin ok
2275 VarInfo viPre = ppt.find_var_by_name (vi.prestate_name());
2276 if (viPre == null) {
2277 System.out.printf("Can't find pre var %s (%s) at %s%n", viPreName.name(), viPreName, ppt);
2278 for (VarInfo v : ppt.var_infos) {
2279 System.out.printf(" %s%n", v);
2280 }
2281 throw new Error();
2282 }
2283 return viPre;
2284 }
2285
2286 private List<VarInfo> addVar(List<VarInfo> result, VarInfoName vin) {
2287 VarInfo vi = ppt.find_var_by_name(applyPreMaybe(vin).name());
2288 // vi could be null because some variable's prefix is not a
2289 // variable. Example: for static variable "Class.staticvar",
2290 // "Class" is not a varible, even though for variable "a.b.c",
2291 // typically "a" and "a.b" are also variables.
2292 if (vi == null) {
2293 String message
2294 = String.format("getGuardingList(%s, %s): did not find variable %s [inpre=%s]", name(), ppt.name(), vin.name(), inPre);
2295 // Only print the error message at most once per variable.
2296 if (addVarMessages.add(vin.name())) {
2297 // For now, don't print at all: it's generally innocuous
2298 // (class prefix of a static variable).
2299 // System.err.println(message);
2300 }
2301 // System.out.println("vars: " + ppt.varNames());
2302 // System.out.flush();
2303 // throw new Error(String.format(message));
2304 return result;
2305 } else {
2306 return addVarInfo(result, vi);
2307 }
2308 }
2309
2310 /**
2311 * Add the given variable to the result list.
2312 * Does nothing if the variable is of primitive type.
2313 **/
2314 // Should this operate by side effect on a global variable?
2315 // (Then what is the type of the visitor; what does everything return?)
2316 private List<VarInfo> addVarInfo(List<VarInfo> result, VarInfo vi) {
2317 assert vi != null;
2318 assert ((! vi.isDerived()) || vi.isDerived())
2319 : "addVar on derived variable: " + vi;
2320 // Don't guard primitives
2321 if (// TODO: ***** make changes here *****
2322 // vi.file_rep_type.isScalar() &&
2323 ! vi.type.isScalar()
2324 // (vi.type.isArray() || vi.type.isObject())
2325 ) {
2326 result.add(vi);
2327 } else {
2328 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2329 Invariant.debugGuarding.fine(String.format("addVarInfo did not add %s: %s (%s) %s (%s)", vi, vi.file_rep_type.isScalar(), vi.file_rep_type, vi.type.isScalar(), vi.type));
2330 }
2331 }
2332 if (Invariant.debugGuarding.isLoggable(Level.FINE)) {
2333 Invariant.debugGuarding.fine(String.format("addVarInfo(%s) => %s", vi, result));
2334 }
2335 return result;
2336 }
2337
2338 } // end of class GuardingVisitor
2339
2340 if (!FileIO.new_decl_format) {
2341 List<VarInfo> result = var_info_name.accept(new GuardingVisitor()); // vin ok
2342 result.remove(ppt.find_var_by_name (var_info_name.name())); // vin ok
2343 assert ! ArraysMDE.any_null(result);
2344 return result;
2345 } else { // new format
2346 List<VarInfo> result = new ArrayList<VarInfo>();
2347
2348 if (Daikon.dkconfig_guardNulls == "never") // interned
2349 return result;
2350
2351 // If this is never missing, nothing to guard
2352 if ((Daikon.dkconfig_guardNulls == "missing") // interned
2353 && !canBeMissing)
2354 return result;
2355
2356 // Create a list of variables to be guarded from the list of all
2357 // enclosing variables.
2358 for (VarInfo vi : get_all_enclosing_vars()) {
2359 if (false && var_flags.contains (VarFlags.CLASSNAME)) {
2360 System.err.printf ("%s filerep type = %s, canbemissing = %b\n",
2361 vi, vi.file_rep_type, vi.canBeMissing);
2362 }
2363 if (!vi.file_rep_type.isHashcode())
2364 continue;
2365 result.add (0, vi);
2366 if ((Daikon.dkconfig_guardNulls == "missing") // interned
2367 && !vi.canBeMissing)
2368 break;
2369 }
2370 return (result);
2371 }
2372 }
2373
2374
2375 /**
2376 * Returns a list of all of the variables that enclose this one. If
2377 * this is derived, this includes all of the enclosing variables of all
2378 * of the bases
2379 */
2380 public List<VarInfo> get_all_enclosing_vars() {
2381 List<VarInfo> result = new ArrayList<VarInfo>();
2382 if (isDerived()) {
2383 for (VarInfo base : derived.getBases()) {
2384 result.addAll (base.get_all_enclosing_vars());
2385 }
2386 } else { // not derived
2387 for (VarInfo vi = this.enclosing_var; vi != null; vi = vi.enclosing_var)
2388 result.add (vi);
2389 }
2390 return result;
2391 }
2392
2393 /**
2394 * Compare names by index.
2395 **/
2396 public static final class IndexComparator
2397 implements Comparator<VarInfo>, Serializable {
2398 // This needs to be serializable because Equality invariants keep
2399 // a TreeSet of variables sorted by theInstance.
2400
2401 // We are Serializable, so we specify a version to allow changes to
2402 // method signatures without breaking serialization. If you add or
2403 // remove fields, you should change this number to the current date.
2404 static final long serialVersionUID = 20050923L;
2405
2406 private IndexComparator() {
2407 }
2408
2409 public int compare(VarInfo vi1, VarInfo vi2) {
2410 if (vi1.varinfo_index < vi2.varinfo_index) {
2411 return -1;
2412 } else if (vi1.varinfo_index == vi2.varinfo_index) {
2413 return 0;
2414 } else {
2415 return 1;
2416 }
2417 }
2418
2419 public static IndexComparator getInstance() {
2420 return theInstance;
2421 }
2422
2423 public static final IndexComparator theInstance = new IndexComparator();
2424 }
2425
2426 /**
2427 * Looks for an OBJECT ppt that corresponds to the type of this
2428 * variable. Returns null if such a point is not found.
2429 *
2430 * @param all_ppts map of all program points
2431 */
2432 public /*@Nullable*/ PptTopLevel find_object_ppt(PptMap all_ppts) {
2433
2434 // Arrays don't have types
2435 if (is_array())
2436 return (null);
2437
2438 // build the name of the object ppt based on the variable type
2439 String type_str = type.base().replaceFirst("\\$", ".");
2440 PptName objname = new PptName(type_str, null, FileIO.object_suffix);
2441 return (all_ppts.get(objname));
2442 }
2443
2444 /**
2445 * Class used to contain a pair of VarInfos and their sample count.
2446 * Currently used for equality set merging as a way to store pairs
2447 * of equal variables. The variable with the smaller index is
2448 * always stored first.
2449 *
2450 * Pairs are equal if both of their VarInfos are identical. Note
2451 * that the content of the VarInfos are not compared, only their
2452 * pointer values.
2453 */
2454 public static class Pair {
2455
2456 public VarInfo v1;
2457 public VarInfo v2;
2458 public int samples;
2459
2460 public Pair(VarInfo v1, VarInfo v2, int samples) {
2461 if (v1.varinfo_index < v2.varinfo_index) {
2462 this.v1 = v1;
2463 this.v2 = v2;
2464 } else {
2465 this.v1 = v2;
2466 this.v2 = v1;
2467 }
2468 this.samples = samples;
2469 }
2470
2471 public boolean equals(/*@Nullable*/ Object obj) {
2472 if (!(obj instanceof Pair))
2473 return (false);
2474
2475 Pair o = (Pair) obj;
2476 return ((o.v1 == v1) && (o.v2 == v2));
2477 }
2478
2479 public int hashCode() {
2480 return (v1.hashCode() + v2.hashCode());
2481 }
2482
2483 public String toString() {
2484 return (v1.name() + " = " + v2.name());
2485 }
2486 }
2487
2488 /** Returns a string containing the names of the vars in the array. **/
2489 public static String toString(VarInfo[] vis) {
2490
2491 if (vis == null)
2492 return ("null");
2493 ArrayList<String> vars = new ArrayList<String>(vis.length);
2494 for (int i = 0; i < vis.length; i++) {
2495 if (vis[i] == null)
2496 vars.add("null");
2497 else
2498 vars.add(vis[i].name());
2499 }
2500 return UtilMDE.join(vars, ", ");
2501 }
2502
2503 /** Returns a string containing the names of the vars in the list. **/
2504 public static String toString(List<VarInfo> vlist) {
2505
2506 if (vlist == null)
2507 return ("null");
2508 ArrayList<String> vars = new ArrayList<String>(vlist.size());
2509 for (VarInfo v : vlist) {
2510 if (v == null)
2511 vars.add("null");
2512 else
2513 vars.add(v.name());
2514 }
2515 return UtilMDE.join(vars, ", ");
2516 }
2517
2518 public ValueSet get_value_set() {
2519
2520 // Static constants don't have value sets, so we must make one
2521 if (is_static_constant) {
2522 ValueSet vs = ValueSet.factory(this);
2523 vs.add(static_constant_value);
2524 return (vs);
2525 }
2526
2527 return (ppt.value_sets[value_index]);
2528 }
2529
2530 public String get_value_info() {
2531 return name() + "- " + get_value_set().repr_short();
2532 }
2533
2534 /**
2535 * Returns the number of elements in the variable's equality set.
2536 * Returns 1 if the equality optimization is turned off
2537 */
2538 public int get_equalitySet_size() {
2539 if (equalitySet == null)
2540 return 1;
2541 else
2542 return equalitySet.size();
2543 }
2544
2545 /**
2546 * Returns the vars_info in the variable's equality set.
2547 * Returns a set with just itself if the equality optimization is turned off
2548 */
2549 public Set<VarInfo> get_equalitySet_vars() {
2550 if (equalitySet == null) {
2551 HashSet<VarInfo> set = new HashSet<VarInfo>();
2552 set.add(this);
2553 return set;
2554 } else
2555 return equalitySet.getVars();
2556 }
2557
2558 /**
2559 * Returns the leader in the variable's equality set.
2560 * Returns itself if the equality optimization is turned off
2561 */
2562 public VarInfo get_equalitySet_leader() {
2563 // if (equalitySet == null && VarInfo.use_equality_optimization == false) {
2564 if (equalitySet == null) {
2565 return this;
2566 } else
2567 return equalitySet.leader();
2568 }
2569
2570
2571 private static Set<String> out_strings = new LinkedHashSet<String>();
2572
2573 /** If the message is new print it, otherwise discard it **/
2574 static void debug_print_once (String format, /*@Nullable*/ Object... args) {
2575 String msg = String.format (format, args);
2576 if (!out_strings.contains (msg)) {
2577 System.out.println (msg);
2578 out_strings.add (msg);
2579 }
2580 }
2581
2582 /** Returns whether or not this variable is a parameter **/
2583 public boolean isParam() {
2584 if (FileIO.new_decl_format) {
2585 return var_flags.contains (VarFlags.IS_PARAM);
2586 } else {
2587 return aux.isParam(); // VIN
2588 }
2589 }
2590
2591 /** Set this variable as a parameter **/
2592 public void set_is_param() {
2593 // System.out.printf ("setting is_param for %s %n", name());
2594 if (FileIO.new_decl_format)
2595 var_flags.add (VarFlags.IS_PARAM);
2596 aux = aux.setValue (VarInfoAux.IS_PARAM, VarInfoAux.TRUE); // VIN
2597 }
2598
2599 /** Set whether or not this variable is a parameter **/
2600 public void set_is_param (boolean set) {
2601 if (set)
2602 set_is_param();
2603 else {
2604 if (FileIO.new_decl_format)
2605 var_flags.remove (VarFlags.IS_PARAM);
2606 aux = aux.setValue (VarInfoAux.IS_PARAM, VarInfoAux.FALSE); // VIN
2607 }
2608 }
2609
2610 /**
2611 * Returns the name of the parent variable in the ppt/var hierarchy.
2612 * If no parent name is specified, it is presume to be the same name
2613 * as the variable.
2614 */
2615 public String parent_var_name() {
2616 if (parent_variable == null)
2617 return name();
2618 else
2619 return parent_variable;
2620 }
2621
2622 /**
2623 * Adds a subscript (or sequence) to an array variable. This should
2624 * really just just substitute for '..', but the dots are currently
2625 * removed for back compatability.
2626 */
2627 public String apply_subscript (String subscript) {
2628 if (FileIO.new_decl_format) {
2629 assert arr_dims == 1 : "Can't apply subscript to " + name();
2630 return name().replace ("..", subscript);
2631 } else {
2632 assert name().contains ("[]") : "Can't apply subscript to " + name();
2633 return apply_subscript (name(), subscript);
2634 }
2635 }
2636
2637 /**
2638 * Adds a subscript (or subsequence) to an array name. This should
2639 * really just substitute for '..', but the dots are currently removed
2640 * for back compatibility.
2641 */
2642 public static String apply_subscript (String sequence, String subscript) {
2643 if (FileIO.new_decl_format) {
2644 return sequence.replace ("[..]", "[" + subscript + "]");
2645 } else {
2646 return sequence.replace ("[]", "[" + subscript + "]");
2647 }
2648 }
2649
2650 /**
2651 * For array variables, returns the variable that is a simple array.
2652 * If this variable is a slice, it returns the array variable that is being
2653 * sliced. If this variable is a simple array itself, returns this.
2654 */
2655 public VarInfo get_array_var() {
2656 assert file_rep_type.isArray();
2657 if (isDerived())
2658 return derived.get_array_var();
2659 else
2660 return this;
2661 }
2662
2663 /**
2664 * Returns the VarInfo that represents the base array of this
2665 * array. For example, if the array is a[].b.c, returns a[]
2666 */
2667 public VarInfo get_base_array() {
2668 assert file_rep_type.isArray() : this;
2669 if (FileIO.new_decl_format) {
2670 VarInfo var = this;
2671 while (var.var_kind != VarKind.ARRAY) {
2672 if (var.enclosing_var == null) {
2673 for (VarInfo vi = this; vi != null; vi = vi.enclosing_var)
2674 System.out.printf ("%s %s%n", vi, vi.var_kind);
2675 assert var.enclosing_var != null : this + " " + var;
2676 }
2677 var = var.enclosing_var;
2678 }
2679 return var;
2680 } else {
2681 Elements elems = (new ElementsFinder(var_info_name)).elems(); // vin ok
2682 return ppt.find_var_by_name (elems.name());
2683 }
2684 }
2685
2686 /**
2687 * Returns the VarInfo that represents the hashcode of the base array
2688 * of this array. For example, if the array is a[].b.c, returns a.
2689 * Returns null if there is no such variable.
2690 */
2691 public /*@Nullable*/ VarInfo get_base_array_hashcode() {
2692 if (FileIO.new_decl_format)
2693 return get_base_array().enclosing_var;
2694 else {
2695 Elements elems = (new ElementsFinder(var_info_name)).elems(); // vin ok
2696 // System.out.printf ("term.name() = %s\n", elems.term.name());
2697 return ppt.find_var_by_name (elems.term.name());
2698 }
2699 }
2700
2701 /**
2702 * Returns the lower bound of the array or slice.
2703 */
2704 public Quantify.Term get_lower_bound() {
2705 assert file_rep_type.isArray() : "var " + name() + " rep " + file_rep_type;
2706 if (isDerived()) {
2707 return derived.get_lower_bound();
2708 } else {
2709 return new Quantify.Constant (0);
2710 }
2711 }
2712
2713 /**
2714 * Returns the upper bound of the array or slice.
2715 */
2716 public Quantify.Term get_upper_bound() {
2717 assert file_rep_type.isArray();
2718 if (isDerived()) {
2719 return derived.get_upper_bound();
2720 } else {
2721 return new Quantify.Length (this, -1);
2722 }
2723 }
2724
2725 /**
2726 * Returns the length of this array. The array can be an array or
2727 * a list. It cannot be a slice.
2728 */
2729 public Quantify.Term get_length() {
2730 assert file_rep_type.isArray() && !isDerived() : this;
2731 return new Quantify.Length (this, 0);
2732 }
2733
2734 /**
2735 * Updates any references to other variables that should be within this
2736 * ppt by looking them up within the ppt. Necessary if a variable is
2737 * moved to a different program point or if cloned variable is placed
2738 * in a new program point (such as is done when combined exits are
2739 * created)
2740 **/
2741 public void new_ppt() {
2742 if (enclosing_var != null) {
2743 enclosing_var = ppt.find_var_by_name (enclosing_var.name());
2744 assert enclosing_var != null;
2745 }
2746 }
2747
2748 /**
2749 * Temporary to let things compile now that name is private. Eventually
2750 * this should be removed.
2751 */
2752 public VarInfoName get_VarInfoName() {
2753 return (var_info_name); // vin ok
2754 }
2755
2756 /**
2757 * Returns the name of this variable in the specified format
2758 */
2759 public String name_using (OutputFormat format) {
2760 if (format == OutputFormat.DAIKON) return name();
2761 if (format == OutputFormat.SIMPLIFY) return simplify_name();
2762 if (format == OutputFormat.ESCJAVA) return esc_name();
2763 if (format == OutputFormat.JAVA) return java_name();
2764 if (format == OutputFormat.JML) return jml_name();
2765 if (format == OutputFormat.DBCJAVA) return dbc_name();
2766 throw new UnsupportedOperationException
2767 ("Unknown format requested: " + format);
2768 }
2769
2770 /** Returns the name in java format. This is the same as JML **/
2771 public String java_name() {
2772 if (!FileIO.new_decl_format)
2773 return var_info_name.java_name (this); // vin ok
2774
2775 return jml_name();
2776 }
2777
2778 /** Returns the name in DBC format. This is the same as JML **/
2779 public String dbc_name() {
2780 if (!FileIO.new_decl_format)
2781 return var_info_name.dbc_name (this); // vin ok
2782
2783 return jml_name();
2784 }
2785
2786 /**
2787 * Returns the name of this variable in ESC format.
2788 **/
2789 public String esc_name() {
2790 if (!FileIO.new_decl_format)
2791 return var_info_name.esc_name(); // vin ok
2792
2793 return (esc_name (null));
2794
2795 }
2796
2797 /**
2798 * Returns the name of this variable in ESC format. If an index
2799 * is specified, it is used as an array index. It is an error to
2800 * specify an index on a non-array variable
2801 */
2802 public String esc_name (String index) {
2803
2804 // System.out.printf ("esc_name for %s, flags %s, enclosing-var %s "
2805 // + " poststate %s index %s rname %s ppt %s%n", str_name,
2806 // var_flags, enclosing_var, postState, index,
2807 // relative_name, ppt.name());
2808 if (index != null)
2809 assert file_rep_type.isArray();
2810
2811 // If this is an orig variable, use the post version to generate the name
2812 if (postState != null)
2813 return "\\old(" + postState.esc_name(index) + ")";
2814
2815 // If this is a derived variable, the derivations builds the name
2816 if (derived != null)
2817 return derived.esc_name (index);
2818
2819 // Build the name by processing back through all of the enclosing variables
2820 switch (var_kind) {
2821 case FIELD:
2822 assert relative_name != null : this;
2823 if (enclosing_var != null)
2824 return enclosing_var.esc_name (index) + "." + relative_name;
2825 return str_name;
2826 case FUNCTION:
2827 assert function_args == null : "function args not implemented";
2828 if (var_flags.contains (VarFlags.CLASSNAME))
2829 return ("\\typeof(" + enclosing_var.esc_name(index) +")");
2830 if (var_flags.contains (VarFlags.TO_STRING))
2831 return enclosing_var.esc_name(index) + ".toString";
2832 if (enclosing_var != null)
2833 return enclosing_var.esc_name(index) + "." + relative_name + "()";
2834 return str_name;
2835 case ARRAY:
2836 if (index == null)
2837 return enclosing_var.esc_name(null) + "[]";
2838 return enclosing_var.esc_name(null) + "[" + index + "]";
2839 case VARIABLE:
2840 assert enclosing_var == null;
2841 return str_name;
2842 case RETURN:
2843 return ("\\result");
2844 default:
2845 throw new Error("can't drop through switch statement");
2846 }
2847 }
2848
2849 /**
2850 * Returns the name of this variable in JML format.
2851 **/
2852 public String jml_name() {
2853 if (!FileIO.new_decl_format)
2854 return var_info_name.jml_name(this); // vin ok
2855
2856 return (jml_name (null));
2857 }
2858
2859 /**
2860 * Returns the name of this variable in JML format. If an index
2861 * is specified, it is used as an array index. It is an error to
2862 * specify an index on a non-array variable
2863 */
2864 public String jml_name (String index) {
2865
2866 if (index != null)
2867 assert file_rep_type.isArray();
2868
2869 // If this is an orig variable, use the post version to generate the name
2870 if (postState != null)
2871 return "\\old(" + postState.jml_name(index) + ")";
2872
2873 // If this is a derived variable, the derivations builds the name
2874 if (derived != null)
2875 return derived.jml_name (index);
2876
2877 // If this is an array of fields, collect the fields into a collection
2878 if ((arr_dims > 0) && (var_kind != VarKind.ARRAY)
2879 && !var_flags.contains (VarFlags.CLASSNAME)) {
2880 String field_name = relative_name;;
2881 VarInfo vi = this.enclosing_var;
2882 for (; vi.var_kind != VarKind.ARRAY; vi = vi.enclosing_var) {
2883 field_name = vi.relative_name + "." + field_name;
2884 }
2885 return String.format ("daikon.Quant.collectObject(%s, \"%s\")",
2886 vi.jml_name(), field_name);
2887 }
2888
2889 // Build the name by processing back through all of the enclosing variables
2890 switch (var_kind) {
2891 case FIELD:
2892 assert relative_name != null : this;
2893 if (enclosing_var != null)
2894 return enclosing_var.jml_name (index) + "." + relative_name;
2895 return str_name;
2896 case FUNCTION:
2897 assert function_args == null : "function args not implemented";
2898 if (var_flags.contains (VarFlags.CLASSNAME)) {
2899 if (arr_dims > 0)
2900 return String.format ("daikon.Quant.typeArray(%s)",
2901 enclosing_var.jml_name(index));
2902 else
2903 return enclosing_var.jml_name(index) + ".getClass()";
2904 }
2905 if (var_flags.contains (VarFlags.TO_STRING))
2906 return enclosing_var.jml_name(index) + ".toString()";
2907 if (enclosing_var != null)
2908 return enclosing_var.jml_name(index) + "." + relative_name + "()";
2909 return str_name;
2910 case ARRAY:
2911 if (index == null)
2912 return enclosing_var.jml_name(null);
2913 return enclosing_var.jml_name(null) + "[" + index + "]";
2914 case VARIABLE:
2915 assert enclosing_var == null;
2916 return str_name;
2917 case RETURN:
2918 return ("\\result");
2919 default:
2920 throw new Error("can't drop through switch statement");
2921 }
2922 }
2923
2924 /** Returns the name of this variable in simplify format **/
2925 public String simplify_name() {
2926 return simplify_name (null);
2927 }
2928
2929 /**
2930 * Returns the name of this variable in simplify format. If an index
2931 * is specified, it is used as an array index. It is an error to specify
2932 * an index on a non-array variable
2933 **/
2934 public String simplify_name (String index) {
2935 if (!FileIO.new_decl_format)
2936 return var_info_name.simplify_name(); // vin ok
2937
2938 assert (index == null) || file_rep_type.isArray() : index + " " + name();
2939
2940 // If this is a derived variable, the derivations builds the name
2941 if (derived != null)
2942 return derived.simplify_name ();
2943
2944 // Build the name by processing back through all of the enclosing variables
2945 switch (var_kind) {
2946 case FIELD:
2947 assert relative_name != null : this;
2948 return String.format ("(select |%s| %s)", relative_name,
2949 enclosing_var.simplify_name(index));
2950 case FUNCTION:
2951 assert function_args == null : "function args not implemented";
2952 if (var_flags.contains (VarFlags.CLASSNAME))
2953 return ("(typeof " + enclosing_var.simplify_name(index) +")");
2954 if (var_flags.contains (VarFlags.TO_STRING))
2955 return String.format ("(select |toString| %s)",
2956 enclosing_var.simplify_name(index));
2957 if (enclosing_var != null)
2958 return enclosing_var.simplify_name(index) + "." + relative_name + "()";
2959 return str_name;
2960 case ARRAY:
2961 if (index == null)
2962 return String.format("(select elems %s)",
2963 enclosing_var.simplify_name());
2964 if (false && index.equals("|0|")) {
2965 System.err.printf ("index = %s\n", index);
2966 Throwable t = new Throwable();
2967 t.printStackTrace();
2968 }
2969 return String.format ("(select (select elems %s) %s)",
2970 enclosing_var.simplify_name(), index);
2971 case VARIABLE:
2972 if (dkconfig_constant_fields_simplify && str_name.contains(".")) {
2973 String sel = null;
2974 String[] fields = null;
2975 if (postState != null) {
2976 fields = postState.name().split ("\\.");
2977 sel = String.format ("(select |%s| |__orig__%s|)", fields[1],
2978 fields[0]);
2979 } else { // not orig variable
2980 fields = str_name.split ("\\.");
2981 sel = String.format ("(select |%s| |%s|)", fields[1], fields[0]);
2982 }
2983 for (int ii = 2; ii < fields.length; ii++) {
2984 sel = String.format ("(select |%s| %s)", fields[ii], sel);
2985 }
2986 return sel;
2987 }
2988
2989 assert enclosing_var == null;
2990 if (postState != null)
2991 return "|__orig__" + postState.name() + "|";
2992 return "|" + str_name + "|";
2993 case RETURN:
2994 return ("|return|");
2995 default:
2996 throw new Error("can't drop through switch statement");
2997 }
2998 }
2999
3000 /**
3001 * Return the name of this variable in its prestate (orig)
3002 */
3003 public /*@Interned*/ String prestate_name() {
3004 return ("orig(" + name() + ")").intern();
3005 }
3006
3007 /**
3008 * Returns the name of the size variable that correponds to this
3009 * array variable in simplify format. Returns null if this variable
3010 * is not an array or the size name can't be constructed for other
3011 * reasons. Note that isArray seems to distinguish between actual
3012 * arrays and other sequences (such as java.util.list). Simplify uses
3013 * (it seems) the same length approach for both, so we don't check isArray()
3014 */
3015 public /*@Nullable*/ String get_simplify_size_name() {
3016 /*@Interned*/ String result = null;
3017 if (!file_rep_type.isArray() || isDerived())
3018 result = null;
3019 else {
3020 // System.out.printf ("Getting size name for %s [%s]\n", name(),
3021 // get_length());
3022 result = get_length().simplify_name().intern();
3023 }
3024
3025 /*@Interned*/ String old_result = null;
3026 if (!var_info_name.isApplySizeSafe()) // vin ok
3027 old_result = null;
3028 else
3029 old_result = var_info_name.applySize().simplify_name().intern(); // vin ok
3030 if (FileIO.new_decl_format && (old_result != result)) {
3031 throw new Error(String.format("%s: '%s' '%s'%n basehashcode = %s%n", this, result, old_result, get_base_array_hashcode()));
3032 }
3033
3034 return old_result;
3035 }
3036
3037 /**
3038 * Returns whether or not this variable is the 'this' variable
3039 */
3040 public boolean is_this() {
3041 return name().equals ("this");
3042 // return (get_VarInfoName().equals (VarInfoName.THIS));
3043 }
3044
3045 /**
3046 * Returns true if this variable contains a simple variable whose
3047 * name is varname
3048 */
3049 public boolean includes_simple_name (String varname) {
3050 if (!FileIO.new_decl_format)
3051 return var_info_name.includesSimpleName (varname); // vin ok
3052
3053 if (isDerived()) {
3054 for (VarInfo base : derived.getBases()) {
3055 if (base.includes_simple_name (varname))
3056 return true;
3057 }
3058 } else {
3059 for (VarInfo vi = this; vi != null; vi = vi.enclosing_var)
3060 if ((vi.var_kind == VarKind.VARIABLE) && vi.name().equals (varname))
3061 return true;
3062 }
3063 return (false);
3064 }
3065
3066 /**
3067 * Quantifies over the specified array variables in ESC format.
3068 * Returns a 4 element string array. Element 0 is the
3069 * quantification, Element 1 is the indexed form of variable 1,
3070 * Element 2 is the indexed form of variable 3. and Element 4 is
3071 * unknown.
3072 */
3073 public static String[] esc_quantify(VarInfo... vars) {
3074 return esc_quantify (true, vars);
3075 }
3076
3077 /**
3078 * Quantifies over the specified array variables in ESC format.
3079 * Returns a 4 element string array. Element 0 is the
3080 * quantification, Element 1 is the indexed form of variable 1,
3081 * Element 2 is the indexed form of variable 3. and Element 4 is
3082 * unknown.
3083 */
3084 public static String[] esc_quantify(boolean elementwise, VarInfo... vars) {
3085
3086 if (FileIO.new_decl_format) {
3087 Quantify.ESCQuantification quant = new Quantify.ESCQuantification
3088 (Quantify.get_flags(elementwise), vars);
3089 if (vars.length == 1)
3090 return new String[] {quant.get_quantification(),
3091 quant.get_arr_vars_indexed(0), ")"};
3092 else if ((vars.length == 2) && vars[1].file_rep_type.isArray())
3093 return new String[] {quant.get_quantification(),
3094 quant.get_arr_vars_indexed(0), quant.get_arr_vars_indexed(1), ")"};
3095 else
3096 return new String[] {quant.get_quantification(),
3097 quant.get_arr_vars_indexed(0), vars[1].esc_name(), ")"};
3098 } else {
3099 VarInfoName vin[] = new VarInfoName[vars.length];
3100 for (int ii = 0; ii < vars.length; ii++)
3101 vin[ii] = vars[ii].var_info_name; // vin ok
3102 return VarInfoName.QuantHelper.format_esc (vin, elementwise);
3103 }
3104
3105 }
3106
3107
3108 /**
3109 * Returns a string array with 3 elements. The first element is
3110 * the sequence, the second element is the lower bound, and the third
3111 * element is the upper bound. Returns null if this is not a direct
3112 * array or slice.
3113 */
3114 public String /*@Nullable*/ [] simplifyNameAndBounds() {
3115 if (!FileIO.new_decl_format)
3116 return VarInfoName.QuantHelper.simplifyNameAndBounds (var_info_name); // vin ok
3117
3118 String[] results = new String[3];
3119 if (is_direct_non_slice_array()
3120 || (derived instanceof SequenceSubsequence)) {
3121 results[0] = get_base_array_hashcode().simplify_name();
3122 results[1] = get_lower_bound().simplify_name();
3123 results[2] = get_upper_bound().simplify_name();
3124 return results;
3125 }
3126
3127 return null;
3128
3129 }
3130
3131 /**
3132 * Returns the upper and lower bounds of the slice in simplify format.
3133 * The implementation is somewhat different that simplifyNameAndBounds
3134 * (I don't know why).
3135 */
3136 public String /*@Nullable*/ [] get_simplify_slice_bounds() {
3137 if (!FileIO.new_decl_format) {
3138 /*@Interned*/ VarInfoName[] bounds = var_info_name.getSliceBounds(); // vin ok
3139 if (bounds == null)
3140 return null;
3141 String[] str_bounds = new String[2];
3142 str_bounds[0] = bounds[0].simplify_name();
3143 str_bounds[1] = bounds[1].simplify_name();
3144 return str_bounds;
3145 }
3146
3147 String[] results = new String[2];
3148 if (derived instanceof SequenceSubsequence) {
3149 results[0] = get_lower_bound().simplify_name().intern();
3150 results[1] = get_upper_bound().simplify_name().intern();
3151 } else {
3152 results = null;
3153 }
3154
3155 return results;
3156
3157 }
3158
3159 /**
3160 * Return a string in simplify format that will seclect the
3161 * (index_base + index_off)-th element of the sequence specified by
3162 * this variable.
3163 *
3164 * @param simplify_index_name name of the index. If free is false, this
3165 * must be a number or null (null implies an index of 0)
3166 * @param free true of simplify_index_name is variable name
3167 * @param index_off offset from the index
3168 */
3169 public String get_simplify_selectNth (String simplify_index_name,
3170 boolean free, int index_off) {
3171
3172 // Remove the simplify bars if present from the index name
3173 if ((simplify_index_name != null) && simplify_index_name.startsWith ("|")
3174 && simplify_index_name.endsWith ("|"))
3175 simplify_index_name
3176 = simplify_index_name.substring (1, simplify_index_name.length()-1);
3177
3178 // Use VarInfoName to handle the old format
3179 if (!FileIO.new_decl_format) {
3180 VarInfoName select
3181 = VarInfoName.QuantHelper.selectNth (this.var_info_name, // vin ok
3182 simplify_index_name, free, index_off);
3183 // System.out.printf ("sNth: index %s, free %b, off %d, result '%s'\n",
3184 // simplify_index_name, free, index_off,
3185 // select.simplify_name());
3186 return select.simplify_name();
3187 }
3188
3189 // Calculate the index (including the offset if non-zero)
3190 String complete_index = null;
3191 if (!free) {
3192 int index = 0;
3193 if (simplify_index_name != null)
3194 index = Integer.decode (simplify_index_name);
3195 index += index_off;
3196 complete_index = String.format ("%d", index);
3197 } else {
3198 if (index_off != 0)
3199 complete_index = String.format ("(+ |%s| %d)", simplify_index_name,
3200 index_off);
3201 else
3202 complete_index = String.format ("|%s|", simplify_index_name);
3203 }
3204
3205 // Return the array properly indexed
3206 return simplify_name (complete_index);
3207 }
3208
3209 /**
3210 * Return a string in simplify format that will seclect the
3211 * index_off element in a sequence that has a lower bound.
3212 *
3213 * @param index_off offset from the index
3214 */
3215 public String get_simplify_selectNth_lower (int index_off) {
3216
3217 // Use VarInfoName to handle the old format
3218 if (!FileIO.new_decl_format) {
3219 /*@Interned*/ VarInfoName[] bounds = var_info_name.getSliceBounds();
3220 VarInfoName lower = null;
3221 if (bounds != null)
3222 lower = bounds[0];
3223 VarInfoName select
3224 = VarInfoName.QuantHelper.selectNth (var_info_name, // vin ok
3225 lower, index_off);
3226 return select.simplify_name();
3227 }
3228
3229 // Calculate the index (including the offset if non-zero)
3230 String complete_index = null;
3231 Quantify.Term lower = get_lower_bound();
3232 String lower_name = lower.simplify_name();
3233 if (!(lower instanceof Quantify.Constant))
3234 lower_name = String.format ("|%s|", lower_name);
3235 if (index_off != 0) {
3236 if (lower instanceof Quantify.Constant)
3237 complete_index = String.format ("%d",
3238 ((Quantify.Constant) lower).get_value() + index_off);
3239 else
3240 complete_index = String.format ("(+ %s %d)", lower_name, index_off);
3241 } else
3242 complete_index = String.format ("%s", lower_name);
3243
3244 // Return the array properly indexed
3245 // System.err.printf ("lower bound type = %s [%s] %s\n", lower,
3246 // lower.getClass(), complete_index);
3247 return simplify_name (complete_index);
3248 }
3249
3250 /**
3251 * Get a fresh variable name that doesn't appear in the given
3252 * variable in simplify format
3253 */
3254 public static String get_simplify_free_index (VarInfo... vars) {
3255 if (!FileIO.new_decl_format) {
3256 VarInfoName[] vins = new VarInfoName[vars.length];
3257 for (int ii = 0; ii < vars.length; ii++) {
3258 vins[ii] = vars[ii].var_info_name; // vin ok
3259 }
3260 return VarInfoName.QuantHelper.getFreeIndex (vins).simplify_name();
3261 }
3262
3263 // Get a free variable for each variable and return the first one
3264 QuantifyReturn qret[] = Quantify.quantify (vars);
3265 return qret[0].index.simplify_name();
3266 }
3267
3268 /**
3269 * Get a 2 fresh variable names that doesn't appear in the given
3270 * variable in simplify format
3271 */
3272 public static String[] get_simplify_free_indices (VarInfo... vars) {
3273 if (!FileIO.new_decl_format) {
3274 if (vars.length == 1) {
3275 VarInfoName index1_vin
3276 = VarInfoName.QuantHelper.getFreeIndex (vars[0].var_info_name); // vin ok
3277 String index2 = VarInfoName.QuantHelper.getFreeIndex
3278 (vars[0].var_info_name, index1_vin).simplify_name(); // vin ok
3279 return new String[] {index1_vin.name(), index2};
3280 } else if (vars.length == 2) {
3281 VarInfoName index1_vin = VarInfoName.QuantHelper.getFreeIndex
3282 (vars[0].var_info_name, vars[1].var_info_name); // vin ok
3283 String index2 = VarInfoName.QuantHelper.getFreeIndex
3284 (vars[0].var_info_name, vars[2].var_info_name, index1_vin) // vin ok
3285 .simplify_name();
3286 return new String[] {index1_vin.name(), index2};
3287 } else
3288 throw new Error ("unexpected length " + vars.length);
3289 }
3290
3291 // Get a free variable for each variable
3292 if (vars.length == 1)
3293 vars = new VarInfo[] {vars[0], vars[0]};
3294 QuantifyReturn qret[] = Quantify.quantify (vars);
3295 return new String[] {qret[0].index.simplify_name(),
3296 qret[1].index.simplify_name()};
3297 }
3298
3299 /**
3300 * Quantifies over the specified array variables in Simplify format.
3301 * Returns a string array that contains the quantification, indexed
3302 * form of each variable, optionally the index itself, and the closer.
3303 *
3304 * If elementwise is true, include the additional contraint that
3305 * the indices (there must be exactly two in this case) refer to
3306 * corresponding positions. If adjacent is true, include the
3307 * additional constraint that the second index be one more than
3308 * the first. If distinct is true, include the constraint that the
3309 * two indices are different. If includeIndex is true, return
3310 * additional strings, after the roots but before the closer, with
3311 * the names of the index variables.
3312 */
3313 public static String[] simplify_quantify (EnumSet<QuantFlags> flags,
3314 VarInfo ...vars) {
3315
3316 if (!FileIO.new_decl_format) {
3317 // Get the names for each variable.
3318 VarInfoName vin[] = new VarInfoName[vars.length];
3319 for (int ii = 0; ii < vars.length; ii++)
3320 vin[ii] = vars[ii].var_info_name; // vin ok
3321
3322 return VarInfoName.QuantHelper.format_simplify
3323 (vin, flags.contains (QuantFlags.ELEMENT_WISE),
3324 flags.contains (QuantFlags.ADJACENT),
3325 flags.contains (QuantFlags.DISTINCT),
3326 flags.contains (QuantFlags.INCLUDE_INDEX));
3327 }
3328
3329 Quantify.SimplifyQuantification quant
3330 = new Quantify.SimplifyQuantification (flags, vars);
3331 boolean include_index = flags.contains (QuantFlags.INCLUDE_INDEX);
3332 if ((vars.length == 1) && include_index)
3333 return new String[] {quant.get_quantification(),
3334 quant.get_arr_vars_indexed(0),
3335 quant.get_index(0), quant.get_closer()};
3336 else if (vars.length == 1)
3337 return new String[] {quant.get_quantification(),
3338 quant.get_arr_vars_indexed(0),
3339 quant.get_closer()};
3340 else if ((vars.length == 2) && include_index)
3341 return new String[] {quant.get_quantification(),
3342 quant.get_arr_vars_indexed(0),
3343 quant.get_arr_vars_indexed(1),
3344 quant.get_index(0), quant.get_index(1),
3345 quant.get_closer()};
3346 else // must be length 2 and no index
3347 return new String[] {quant.get_quantification(),
3348 quant.get_arr_vars_indexed(0),
3349 quant.get_arr_vars_indexed(1),
3350 quant.get_closer()};
3351
3352 }
3353
3354 /** see simplify_quantify (EnumSet<QuantFlags>, VarInfo ...) **/
3355 public static String[] simplify_quantify (VarInfo ...vars) {
3356 return simplify_quantify (EnumSet.noneOf (QuantFlags.class), vars);
3357 }
3358
3359 /**
3360 * Returns a rough indication of the complexity of the variable. Higher
3361 * numbers indicate more complexity.
3362 */
3363 public int complexity() {
3364 if (!FileIO.new_decl_format) {
3365 // System.out.printf ("%s - %s\n", this, var_info_name.repr());
3366 return var_info_name.inOrderTraversal().size(); // vin ok
3367 }
3368
3369 int cnt = 0;
3370 if (isDerived()) {
3371 cnt += derived.complexity();
3372 VarInfo[] bases = derived.getBases();
3373 for (VarInfo vi : bases) {
3374 cnt += vi.complexity();
3375 }
3376 // Adjust for the complexity change when a prestate is nested in
3377 // another prestate. This is just done to match the old version
3378 if ((bases.length == 2) && bases[0].isPrestate()) {
3379 if (bases[1].isPrestate())
3380 cnt--;
3381 else
3382 cnt++;
3383 }
3384 } else {
3385 if (isPrestate())
3386 cnt++;
3387 for (VarInfo vi = this; vi != null; vi = vi.enclosing_var) {
3388 cnt++;
3389 }
3390 }
3391
3392 // int old_cnt = var_info_name.inOrderTraversal().size();
3393 // if (cnt != old_cnt)
3394 // System.out.printf ("var %s, new cnt = %d, old cnt = %d [%s]\n",
3395 // name(), cnt, old_cnt, var_info_name.inOrderTraversal());
3396 return cnt;
3397
3398 }
3399
3400 /**
3401 * Returns true if this variable can be assigned to. Currently this is
3402 * presumed true of all variable except the special variable for the type
3403 * of a variable and the size of a sequence. It should include pure
3404 * functions as well
3405 */
3406 public boolean is_assignable_var() {
3407 if (!FileIO.new_decl_format)
3408 return !((var_info_name instanceof VarInfoName.TypeOf) // vin ok
3409 || (var_info_name instanceof VarInfoName.SizeOf)); // vin ok
3410
3411 return !(is_typeof() || is_size());
3412 }
3413
3414 /**
3415 * Returns whether or not this variable represents the type of a variable
3416 * (eg, a.getClass()). Note that this will miss prestate variables such
3417 * as 'orig(a.getClass())'.
3418 */
3419 public boolean is_typeof() {
3420 if (!FileIO.new_decl_format)
3421 return (var_info_name instanceof VarInfoName.TypeOf); // vin ok
3422
3423 // The isPrestate check doesn't seem necessary, but is required to
3424 // match old behavior.
3425 return !isPrestate() && var_flags.contains (VarFlags.CLASSNAME);
3426 }
3427
3428 /**
3429 * Returns whether or not this variable represents the type of a variable
3430 * (eg, a.getClass()). This version finds prestate variable such as
3431 * 'org(a.getClass())'.
3432 */
3433 public boolean has_typeof() {
3434 if (!FileIO.new_decl_format)
3435 return var_info_name.hasTypeOf(); // vin ok
3436
3437 if (isPrestate())
3438 return postState.has_typeof();
3439 return is_typeof();
3440 }
3441
3442 /**
3443 * Returns whether or not this name refers to the 'this' variable
3444 * of a class. True for both normal and prestate versions of the
3445 * variable
3446 */
3447 public boolean isThis() {
3448 return var_info_name.isThis();
3449 }
3450
3451 /** Returns whether this is a size of an array or a prestate thereof **/
3452 public boolean is_size() {
3453 return (derived instanceof SequenceLength);
3454 }
3455
3456 /** Returns wehther or not this variable is a field **/
3457 public boolean is_field() {
3458 return (var_info_name instanceof VarInfoName.Field);
3459 }
3460
3461 /** Returns whether or not this variable has an integer offset (eg, a+2) **/
3462 public boolean is_add() {
3463 return (var_info_name instanceof VarInfoName.Add);
3464 }
3465
3466 /**
3467 * Returns the integer offset if this variable is an addition such
3468 * as a+2. Throws an exception of this variable is not an addition.
3469 * see #is_add()
3470 */
3471 public int get_add_amount() {
3472 return ((VarInfoName.Add)var_info_name).amount;
3473 }
3474
3475 /**
3476 * Returns whether or not this variable is an actual array as opposed
3477 * to an array that is created over fields/methods of an array. For
3478 * example, 'a[]' is a direct array, but 'a[].b' is not.
3479 */
3480 public boolean is_direct_array() {
3481 // Must be an array to be a direct array
3482 if (!rep_type.isArray())
3483 return false;
3484
3485 // If $Field or $Type appears before $Elements, false.
3486 // System.out.printf ("%s flatten %s%n", name(), name);
3487 for (VarInfoName node : (new VarInfoName.InorderFlattener(var_info_name)).nodes()) {
3488 if (node instanceof VarInfoName.Field) {
3489 return false;
3490 }
3491 if (node instanceof VarInfoName.TypeOf) {
3492 return false;
3493 }
3494 if (node instanceof VarInfoName.Elements) {
3495 break;
3496 }
3497 }
3498
3499 return (true);
3500 }
3501
3502 /**
3503 * Returns whether or not this variable is an actual array as opposed
3504 * to an array that is created over fields/methods of an array or a
3505 * slice. For example, 'a[]' is a direct array, but 'a[].b' and 'a[i..]'
3506 * are not.
3507 */
3508 public boolean is_direct_non_slice_array() {
3509 return (var_info_name instanceof VarInfoName.Elements);
3510 }
3511
3512 /**
3513 * Returns whether or not two variables have the same enclosing variable.
3514 * If either variable is not a field, returns false
3515 */
3516 public boolean has_same_parent (VarInfo other) {
3517 if (!is_field() || !other.is_field())
3518 return (false);
3519
3520 VarInfoName.Field name1 = (VarInfoName.Field) var_info_name;
3521 VarInfoName.Field name2 = (VarInfoName.Field) other.var_info_name;
3522
3523 return (name1.term.equals(name2.term));
3524 }
3525
3526 /**
3527 * Returns the variable that encloses this one. For example if
3528 * this variable is 'x.a.b', the enclosing variable is 'x.a'.
3529 */
3530 public VarInfo get_enclosing_var() {
3531 if (FileIO.new_decl_format)
3532 return enclosing_var;
3533 else {
3534 List<VarInfoName> traversal
3535 = new VarInfoName.InorderFlattener(var_info_name).nodes();
3536 if (traversal.size() <= 1) {
3537 // System.out.printf ("size <= 1, traversal = %s%n", traversal);
3538 return (null);
3539 } else {
3540 VarInfo enclosing_vi = ppt.find_var_by_name(traversal.get(1).name());
3541 // if (enclosing_vi == null)
3542 // System.out.printf ("Can't find '%s' in %s%n",
3543 // traversal.get(1).name(), ppt.varNames());
3544 return (enclosing_vi);
3545 }
3546 }
3547 }
3548
3549 /**
3550 * Replaces all instances of 'this' in the variable with the
3551 * name of arg. Used to match up enter/exit variables with object variables
3552 **/
3553 public String replace_this (VarInfo arg) {
3554 VarInfoName parent_name = var_info_name.replaceAll (VarInfoName.THIS, arg.var_info_name);
3555 return parent_name.name();
3556 }
3557
3558 /**
3559 * Creates a VarInfo that is a subsequence that begins at begin and
3560 * ends at end with the specified shifts. The begin or the end can be
3561 * null. Shifts are only allowed with non-null variables
3562 */
3563 public static VarInfo make_subsequence (VarInfo seq,
3564 /*@Nullable*/ VarInfo begin, int begin_shift,
3565 /*@Nullable*/ VarInfo end, int end_shift) {
3566
3567 String begin_str = inside_name (begin, seq.isPrestate(), begin_shift);
3568 if (begin_str.equals("")) // interned if the null string, not interned otherwise
3569 begin_str = "0";
3570 String end_str = inside_name (end, seq.isPrestate(), end_shift);
3571
3572 VarInfoName begin_name = (begin != null) ? begin.var_info_name : null;
3573 String parent_format = "%s..";
3574 if (begin_shift == -1) {
3575 begin_name = begin_name.applyDecrement();
3576 parent_format = "%s-1..";
3577 } else if (begin_shift == 1) {
3578 begin_name = begin_name.applyIncrement();
3579 parent_format = "%s+1..";
3580 } else {
3581 assert begin_shift == 0;
3582 }
3583
3584 VarInfoName end_name = (end != null) ? end.var_info_name : null;
3585 if (end_shift == -1) {
3586 end_name = end_name.applyDecrement();
3587 parent_format += "%s-1";
3588 } else if (end_shift == 1) {
3589 end_name = end_name.applyIncrement();
3590 parent_format += "%s+1";
3591 } else {
3592 assert end_shift == 0;
3593 parent_format += "%s";
3594 }
3595
3596 VarInfoName new_name = seq.var_info_name.applySlice (begin_name, end_name);
3597
3598 VarInfo vi = new VarInfo (new_name, seq.type, seq.file_rep_type,
3599 seq.comparability, seq.aux);
3600 vi.setup_derived_base (seq, begin, end);
3601 vi.str_name = seq.apply_subscript (String.format ("%s..%s", begin_str,
3602 end_str)).intern(); // interning bugfix
3603
3604 // If there is a parent ppt (set in setup_derived_base), set the
3605 // parent variable accordingly. If all of the original variables, used
3606 // the default name, this can as well. Otherwise, build the parent
3607 // name.
3608 if (vi.parent_ppt != null) {
3609 if ((seq.parent_variable == null)
3610 && ((begin == null) || (begin.parent_variable == null))
3611 && ((end == null) || (end.parent_variable == null)))
3612 vi.parent_variable = null;
3613 else {
3614 String begin_pname = (begin == null) ? "0" : begin.parent_var_name();
3615 String end_pname = (end == null) ? "" : end.parent_var_name();
3616 vi.parent_variable = apply_subscript (seq.parent_var_name(),
3617 String.format (parent_format, begin_pname, end_pname));
3618 // System.out.printf ("-- set parent var from '%s' '%s' '%s' '%s'%n",
3619 // seq.parent_var_name(), parent_format, begin_pname, end_pname);
3620 }
3621
3622 }
3623 // System.out.printf ("Parent for %s:%s is %s:%s%n",
3624 // ((seq.ppt != null)? seq.ppt.name() : "none"), vi.name(),
3625 // vi.parent_ppt, vi.parent_variable);
3626
3627 return (vi);
3628 }
3629
3630 /**
3631 * Returns the name to use for vi inside of a array reference.
3632 * If the array reference is orig, then orig is implied. This removes
3633 * orig from orig variales and adds post to post variables.
3634 */
3635 private static String inside_name (/*@Nullable*/ VarInfo vi, boolean in_orig, int shift) {
3636 if (vi == null)
3637 return "";
3638
3639 String shift_str = "";
3640 if (shift != 0)
3641 shift_str = String.format ("%+d", shift);
3642
3643 if (in_orig) {
3644 if (vi.isPrestate())
3645 return vi.postState.name() + shift_str;
3646 else
3647 return String.format ("post(%s)%s", vi.name(), shift_str);
3648 } else
3649 return vi.name() + shift_str;
3650 }
3651
3652 /**
3653 * Creates a VarInfo that is an index into a sequence. The type,
3654 * file_rep_type, etc are taken from the element type of the sequence.
3655 */
3656 public static VarInfo make_subscript (VarInfo seq, VarInfo index,
3657 int index_shift) {
3658
3659 String index_str = inside_name (index, seq.isPrestate(), index_shift);
3660
3661 VarInfoName index_name = null;
3662 if (index == null)
3663 index_name = VarInfoName.parse (String.valueOf (index_shift));
3664 else {
3665 index_name = index.var_info_name;
3666 if (index_shift == -1)
3667 index_name = index_name.applyDecrement();
3668 else
3669 assert index_shift == 0 : "bad shift " + index_shift + " for " + index;
3670 }
3671
3672 VarInfoName new_name = seq.var_info_name.applySubscript (index_name);
3673 VarInfo vi = new VarInfo (new_name, seq.type.elementType(),
3674 seq.file_rep_type.elementType(),
3675 seq.comparability.elementType(),
3676 VarInfoAux.getDefault());
3677 vi.setup_derived_base (seq, index);
3678 vi.var_kind = VarInfo.VarKind.FIELD;
3679 vi.str_name = seq.apply_subscript (index_str).intern(); // interning bugfix
3680 if (vi.parent_ppt != null) {
3681 if ((seq.parent_variable == null) &&
3682 ((index == null) || (index.parent_variable == null)))
3683 vi.parent_variable = null;
3684 else { // one of the two bases has a different parent variable name
3685 String subscript_parent = String.valueOf (index_shift);
3686 if (index != null) {
3687 subscript_parent = index.parent_var_name();
3688 if (index_shift == -1)
3689 subscript_parent = subscript_parent + "-1";
3690 }
3691 vi.parent_variable = apply_subscript (seq.parent_var_name(),
3692 subscript_parent);
3693 }
3694 }
3695 return (vi);
3696 }
3697
3698
3699 /**
3700 * Create a VarInfo that is a function over one or more other variables.
3701 * the type, rep_type, etc of the new function are taken from the first
3702 * variable.
3703 */
3704 public static VarInfo make_function (String function_name, VarInfo... vars) {
3705
3706 VarInfoName[] vin = new VarInfoName[vars.length];
3707 for (int ii = 0; ii < vars.length; ii++)
3708 vin[ii] = vars[ii].var_info_name;
3709
3710 VarInfo vi = new VarInfo(VarInfoName.applyFunctionOfN(function_name, vin),
3711 vars[0].type, vars[0].file_rep_type,
3712 vars[0].comparability, vars[0].aux);
3713 vi.setup_derived_function (function_name, vars);
3714 return (vi);
3715 }
3716
3717 /*
3718 * Creates the derived variable func(seq) from seq.
3719 *
3720 * @param func_name Name of the function
3721 * @param type Return type of the function. If null, the return type is
3722 * the element type of the sequence
3723 * @param seq Sequence variable
3724 * @param shift value to add or subtract from the function. Legal values
3725 * are -1, 0, and 1.
3726 */
3727 public static VarInfo make_scalar_seq_func (String func_name,
3728 ProglangType type, VarInfo seq, int shift) {
3729
3730 VarInfoName viname = seq.var_info_name.applyFunction (func_name);
3731 if (func_name.equals ("size"))
3732 viname = seq.var_info_name.applySize();
3733 String shift_name = "";
3734 if (shift == -1) {
3735 viname = viname.applyDecrement();
3736 shift_name = "_minus1";
3737 } else if (shift == 1) {
3738 viname = viname.applyIncrement();
3739 shift_name = "_plus1";
3740 } else
3741 assert shift == 0;
3742
3743 ProglangType ptype = type;
3744 ProglangType frtype = type;
3745 VarComparability comp = seq.comparability.indexType(0);
3746 VarInfoAux aux = VarInfoAux.getDefault();
3747 if (type == null) {
3748 ptype = seq.type.elementType();
3749 frtype = seq.file_rep_type.elementType();
3750 comp = seq.comparability.elementType();
3751 aux = seq.aux;
3752 }
3753 VarInfo vi = new VarInfo(viname, ptype, frtype, comp, aux);
3754 vi.setup_derived_base (seq);
3755 vi.var_kind = VarInfo.VarKind.FUNCTION;
3756 vi.enclosing_var = seq;
3757 vi.arr_dims = 0;
3758 vi.function_args = null;
3759 vi.relative_name = func_name + shift_name;
3760
3761 // Calculate the string to add for the shift.
3762 String shift_str = "";
3763 if (shift != 0)
3764 shift_str = String.format ("%+d", shift);
3765
3766 // Determine whether orig should be swapped with the function.
3767 // The original VarInfoName code did this only for the size
3768 // function (though it makes the same sense for all functions over
3769 // sequences).
3770 boolean swap_orig = func_name.equals ("size") && seq.isPrestate();
3771
3772 // Force orig to the outside if specified.
3773 if (swap_orig) {
3774 vi.str_name = String.format ("orig(%s(%s))%s", func_name,
3775 seq.postState.name(), shift_str).intern(); // interning bugfix
3776 } else {
3777 vi.str_name = String.format ("%s(%s)%s", func_name, seq.name(),
3778 shift_str).intern(); // interning bugfix
3779 }
3780
3781 if (vi.parent_ppt != null) {
3782 if (seq.parent_variable == null)
3783 vi.parent_variable = null;
3784 else {
3785 assert !swap_orig : "swap orig with parent " + vi;
3786 vi.parent_variable = String.format ("%s(%s)%s", func_name,
3787 seq.parent_variable, shift_str);
3788 }
3789 }
3790 return (vi);
3791 }
3792
3793 /*
3794 * Creates the derived variable func(str) from string.
3795 *
3796 * @param func_name Name of the function
3797 * @param type Return type of the function.
3798 * @param str Sequence variable
3799 */
3800 public static VarInfo make_scalar_str_func (String func_name,
3801 ProglangType type, VarInfo str) {
3802
3803 VarInfoName viname = str.var_info_name.applyFunction (func_name);
3804
3805 ProglangType ptype = type;
3806 ProglangType frtype = type;
3807 VarComparability comp = str.comparability.string_length_type();
3808 VarInfoAux aux = VarInfoAux.getDefault();
3809 VarInfo vi = new VarInfo(viname, ptype, frtype, comp, aux);
3810 vi.setup_derived_base (str);
3811 vi.var_kind = VarInfo.VarKind.FUNCTION;
3812 vi.enclosing_var = str;
3813 vi.arr_dims = 0;
3814 vi.function_args = null;
3815 vi.relative_name = func_name;
3816
3817 vi.str_name = String.format ("%s.%s()", str.name(), func_name).intern(); // interning bugfix
3818
3819 if (vi.parent_ppt != null) {
3820 if (str.parent_variable == null)
3821 vi.parent_variable = null;
3822 else {
3823 vi.parent_variable = String.format ("%s.%s()", str.parent_variable,
3824 func_name);
3825 }
3826 }
3827 return (vi);
3828 }
3829
3830 /**
3831 * Returns true if vi is the prestate version of this. If this is a
3832 * derived variable, vi must be the same derivation using prestate
3833 * versions of each base variable.
3834 */
3835 public boolean is_prestate_version (VarInfo vi) {
3836
3837 // If both variables are not derived
3838 if ((derived == null) && (vi.derived == null)) {
3839
3840 // true if vi is the prestate version of this
3841 return (!isPrestate() && vi.isPrestate() &&
3842 name().equals (vi.postState.name()));
3843
3844 // else if both variables are derived
3845 } else if ((derived != null) && (vi.derived != null)) {
3846
3847 return (derived.is_prestate_version (vi.derived));
3848
3849 // one is derived and the other isn't
3850 } else {
3851 return false;
3852 }
3853 }
3854
3855 /** Returns true if this is an array or a slice **/
3856 public boolean isArray() {
3857 return type.isArray();
3858 }
3859
3860 /** Returns true if this is a slice **/
3861 public boolean isSlice() {
3862 return isArray() && isDerived();
3863 }
3864
3865 /**
3866 * Converts a variable name or expression to the old style of names
3867 */
3868 public static String old_var_names (String name) {
3869 if (PrintInvariants.dkconfig_old_array_names && FileIO.new_decl_format)
3870 return name.replace ("[..]", "[]");
3871 else
3872 return name;
3873 }
3874
3875 /**
3876 * Returns the old style variable name for this name
3877 */
3878 public String old_var_name() {
3879 return old_var_names (name());
3880 }
3881
3882 /**
3883 * Rough check to ensure that the variable name and derivation match
3884 * up
3885 */
3886 public void var_check() {
3887
3888 if (false) {
3889 if ((derived != null) && (derived instanceof SequenceSubsequence)) {
3890 if (name().contains ("-1")) {
3891 SequenceSubsequence ss = (SequenceSubsequence) derived;
3892 // System.out.printf ("checking %s[%08X] with derived %s[%08X]%n",
3893 // this, System.identityHashCode (this), derived,
3894 // System.identityHashCode (derived));
3895 assert ss.index_shift == -1
3896 : "bad var " + this + " derived " + derived + " shift "
3897 + ss.index_shift + " in ppt " + ppt.name();
3898 }
3899 }
3900 }
3901
3902
3903 }
3904 }