001// ***** This file is automatically generated from SequenceScalar.java.jpp 002 003package daikon.inv.binary.sequenceString; 004 005import daikon.*; 006import daikon.inv.*; 007import daikon.inv.binary.BinaryInvariant; 008import org.checkerframework.checker.interning.qual.Interned; 009import org.checkerframework.checker.lock.qual.GuardSatisfied; 010import org.checkerframework.dataflow.qual.Pure; 011import org.plumelib.util.ArraysPlume; 012import org.plumelib.util.Intern; 013import typequals.prototype.qual.NonPrototype; 014import typequals.prototype.qual.Prototype; 015 016/** 017 * Abstract base class for comparing String sequences to String variables. Note that the sequence 018 * must always be passed in first. An example is {@code x is a member of a[]}. 019 */ 020public abstract class SequenceString extends BinaryInvariant { 021 022 static final long serialVersionUID = 20040113L; 023 024 protected SequenceString(PptSlice ppt) { 025 super(ppt); 026 } 027 028 protected @Prototype SequenceString() { 029 super(); 030 } 031 032 /** 033 * Returns whether or not the specified types are valid. All subclasses accept a scalar in one 034 * parameter and an array over the same scalar type in the other. 035 */ 036 @Override 037 public boolean valid_types(VarInfo[] vis) { 038 039 if (vis.length != 2) { 040 return false; 041 } 042 043 if (!vis[0].file_rep_type.baseIsString() || !vis[1].file_rep_type.baseIsString()) { 044 return false; 045 } 046 047 return vis[0].file_rep_type.isArray() ^ vis[1].file_rep_type.isArray(); 048 } 049 050 /** 051 * Since the order is determined from the vars and the sequence is always first, no permute is 052 * necesesary. Subclasses can override if necessary. 053 */ 054 protected Invariant resurrect_done_swapped() { 055 return this; 056 } 057 058 /** 059 * Since the order is determined from the vars and the sequence is always first, this is 060 * essentially symmetric. Subclasses can override if necessary. 061 */ 062 @Pure 063 @Override 064 public boolean is_symmetric() { 065 return true; 066 } 067 068 // Check if swap occurred and call one of the other two methods 069 @Override 070 protected Invariant resurrect_done(int[] permutation) { 071 assert permutation.length == 2; 072 // assert ArraysPlume.fnIsPermutation(permutation); 073 if (permutation[0] == 1) { 074 return resurrect_done_swapped(); 075 } else { 076 return resurrect_done_unswapped(); 077 } 078 } 079 080 /** Subclasses can override in the rare cases they need to fix things even when not swapped. */ 081 protected Invariant resurrect_done_unswapped() { 082 // do nothing 083 return this; 084 } 085 086 protected final boolean seq_first(@GuardSatisfied SequenceString this) { 087 return ppt.var_infos[0].rep_type == ProglangType.STRING_ARRAY; 088 } 089 090 protected final int seq_index(@GuardSatisfied SequenceString this) { 091 return seq_first() ? 0 : 1; 092 } 093 094 protected final int scl_index(@GuardSatisfied SequenceString this) { 095 return seq_first() ? 1 : 0; 096 } 097 098 public VarInfo seqvar(@GuardSatisfied SequenceString this) { 099 return ppt.var_infos[seq_index()]; 100 } 101 102 public VarInfo sclvar(@GuardSatisfied SequenceString this) { 103 return ppt.var_infos[scl_index()]; 104 } 105 106 /** 107 * Return the sequence variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos. 108 */ 109 public VarInfo seqvar(VarInfo[] vis) { 110 return vis[seq_index()]; 111 } 112 113 /** 114 * Return the scalar variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos. 115 */ 116 public VarInfo sclvar(VarInfo[] vis) { 117 return vis[scl_index()]; 118 } 119 120 @Override 121 public InvariantStatus check( 122 @Interned Object val1, @Interned Object val2, int mod_index, int count) { 123 assert !falsified; 124 assert (mod_index >= 0) && (mod_index < 4); 125 String[] v1 = (String[]) val1; 126 String v2 = ((String) val2); 127 if (v1 == null) { 128 } else if (mod_index == 0) { 129 return check_unmodified(v1, v2, count); 130 } else { 131 return check_modified(v1, v2, count); 132 } 133 return InvariantStatus.NO_CHANGE; 134 } 135 136 @Override 137 public InvariantStatus add( 138 @Interned Object val1, @Interned Object val2, int mod_index, int count) { 139 assert !falsified; 140 assert (mod_index >= 0) && (mod_index < 4); 141 String[] v1 = (String[]) val1; 142 String v2 = ((String) val2); 143 if (v1 == null) { 144 } else if (mod_index == 0) { 145 return add_unmodified(v1, v2, count); 146 } else { 147 return add_modified(v1, v2, count); 148 } 149 return InvariantStatus.NO_CHANGE; 150 } 151 152 /** 153 * Presents a sample to the invariant. Returns whether the sample is consistent with the 154 * invariant. Does not change the state of the invariant. 155 * 156 * @param count how many identical samples were observed in a row. For example, three calls to 157 * check_modified with a count parameter of 1 is equivalent to one call to check_modified with 158 * a count parameter of 3. 159 * @return whether or not the sample is consistent with the invariant 160 */ 161 public abstract InvariantStatus check_modified(String @Interned [] v1, String v2, int count); 162 163 public InvariantStatus check_unmodified(String @Interned [] v1, String v2, int count) { 164 return InvariantStatus.NO_CHANGE; 165 } 166 167 /** 168 * Similar to {@link #check_modified} except that it can change the state of the invariant if 169 * necessary. If the invariant doesn't have any state, then the implementation should simply call 170 * {@link #check_modified}. This method need not check for falsification; that is done by the 171 * caller. 172 */ 173 public abstract InvariantStatus add_modified(String @Interned [] v1, String v2, int count); 174 175 /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */ 176 public InvariantStatus add_unmodified(String @Interned [] v1, String v2, int count) { 177 return InvariantStatus.NO_CHANGE; 178 } 179}