001// ***** This file is automatically generated from LinearBinary.java.jpp 002 003package daikon.inv.binary.twoScalar; 004 005import daikon.*; 006import daikon.derive.unary.SequenceLength; 007import daikon.inv.*; 008import java.util.*; 009import org.checkerframework.checker.lock.qual.GuardSatisfied; 010import org.checkerframework.checker.nullness.qual.NonNull; 011import org.checkerframework.checker.nullness.qual.Nullable; 012import org.checkerframework.checker.nullness.qual.Nullable; 013import org.checkerframework.dataflow.qual.Pure; 014import org.checkerframework.dataflow.qual.SideEffectFree; 015import typequals.prototype.qual.NonPrototype; 016import typequals.prototype.qual.Prototype; 017 018/** 019 * Represents a Linear invariant between two long scalars {@code x} and {@code y}, of 020 * the form {@code ax + by + c = 0}. The constants {@code a}, {@code b} and 021 * {@code c} are mutually relatively prime, and the constant {@code a} is always positive. 022 */ 023public class LinearBinary extends TwoScalar { 024 static final long serialVersionUID = 20030822L; 025 026 // Variables starting with dkconfig_ should only be set via the 027 // daikon.config.Configuration interface. 028 /** Boolean. True iff LinearBinary invariants should be considered. */ 029 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 030 031 public LinearBinaryCore core; 032 033 @SuppressWarnings("nullness") // circular initialization 034 protected LinearBinary(PptSlice ppt) { 035 super(ppt); 036 core = new LinearBinaryCore(this); 037 } 038 039 @SuppressWarnings("nullness") // circular initialization 040 protected @Prototype LinearBinary() { 041 super(); 042 // Do we need core to be set for a prototype invariant? 043 core = new LinearBinaryCore(this); 044 } 045 046 private static @Prototype LinearBinary proto = new @Prototype LinearBinary(); 047 048 /** Returns a prototype LinearBinary invariant. */ 049 public static @Prototype LinearBinary get_proto() { 050 return proto; 051 } 052 053 @Override 054 public boolean enabled() { 055 return dkconfig_enabled; 056 } 057 058 @Override 059 public boolean instantiate_ok(VarInfo[] vis) { 060 061 if (!valid_types(vis)) { 062 return false; 063 } 064 065 // Don't look for linearbinary over hashcodes and booleans 066 if (!vis[0].file_rep_type.isIntegral() 067 || !vis[1].file_rep_type.isIntegral()) 068 return false; 069 070 return true; 071 } 072 073 @Override 074 protected LinearBinary instantiate_dyn(@Prototype LinearBinary this, PptSlice slice) { 075 return new LinearBinary(slice); 076 } 077 078 @SideEffectFree 079 @Override 080 public LinearBinary clone(@GuardSatisfied LinearBinary this) { 081 LinearBinary result = (LinearBinary) super.clone(); 082 result.core = core.clone(); 083 result.core.wrapper = result; 084 return result; 085 } 086 087 @Override 088 protected Invariant resurrect_done_swapped() { 089 core.swap(); 090 return this; 091 } 092 093 @Override 094 public String repr(@GuardSatisfied LinearBinary this) { 095 return "LinearBinary" + varNames() + ": falsified=" + falsified 096 + "; " + core.repr(); 097 } 098 099 @SideEffectFree 100 @Override 101 public String format_using(@GuardSatisfied LinearBinary this, OutputFormat format) { 102 return core.format_using(format, var1().name_using(format), 103 var2().name_using(format)); 104 } 105 106 @Pure 107 @Override 108 public boolean isActive() { 109 return core.isActive(); 110 } 111 112 @Override 113 public boolean mergeFormulasOk() { 114 return core.mergeFormulasOk(); 115 } 116 117 /** 118 * Merge the invariants in invs to form a new invariant. Each must be a LinearBinary invariant. The 119 * work is done by the LinearBinary core 120 * 121 * @param invs list of invariants to merge. They should all be permuted to match the variable 122 * order in parent_ppt. 123 * @param parent_ppt slice that will contain the new invariant 124 */ 125 @Override 126 public @Nullable LinearBinary merge(List<Invariant> invs, PptSlice parent_ppt) { 127 128 // Create a matching list of cores 129 List<LinearBinaryCore> cores = new ArrayList<>(); 130 for (Invariant inv : invs) { 131 cores.add(((LinearBinary) inv).core); 132 } 133 134 // Merge the cores and build a new invariant containing the merged core 135 LinearBinary result = new LinearBinary(parent_ppt); 136 LinearBinaryCore newcore = core.merge(cores, result); 137 if (newcore == null) { 138 return null; 139 } 140 result.core = newcore; 141 return result; 142 } 143 144 @Override 145 public InvariantStatus check_modified(long x, long y, int count) { 146 return clone().add_modified(x, y, count); 147 } 148 149 @Override 150 public InvariantStatus add_modified(long x, long y, int count) { 151 return core.add_modified(x, y, count); 152 } 153 154 @Override 155 public boolean enoughSamples(@GuardSatisfied LinearBinary this) { 156 return core.enoughSamples(); 157 } 158 159 @Override 160 protected double computeConfidence() { 161 return core.computeConfidence(); 162 } 163 164 @Pure 165 @Override 166 public boolean isExact() { 167 return true; 168 } 169 170 @Pure 171 @Override 172 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 173 // Obvious derived 174 VarInfo var1 = vis[0]; 175 VarInfo var2 = vis[1]; 176 // avoid comparing "size(a)" to "size(a)-1"; yields "size(a)-1 = size(a) - 1" 177 if (var1.isDerived() 178 && (var1.derived instanceof SequenceLength) 179 && var2.isDerived() 180 && (var2.derived instanceof SequenceLength)) { 181 @NonNull SequenceLength sl1 = (SequenceLength) var1.derived; 182 @NonNull SequenceLength sl2 = (SequenceLength) var2.derived; 183 if (sl1.base == sl2.base) { 184 String discardString = var1.name()+" and "+var2.name()+" derived from "+ 185 "same sequence: "+sl1.base.name(); 186 return new DiscardInfo(this, DiscardCode.obvious, discardString); 187 } 188 } 189 // avoid comparing "size(a)-1" to anything; should compare "size(a)" instead 190 if (var1.isDerived() 191 && (var1.derived instanceof SequenceLength) 192 && ((SequenceLength) var1.derived).shift != 0) { 193 String discardString = "Variables of the form 'size(a)-1' are not compared since 'size(a)' "+ 194 "will be compared"; 195 return new DiscardInfo(this, DiscardCode.obvious, discardString); 196 } 197 if (var2.isDerived() 198 && (var2.derived instanceof SequenceLength) 199 && ((SequenceLength) var2.derived).shift != 0) { 200 String discardString = "Variables of the form 'size(a)-1' are not compared since 'size(a)' "+ 201 "will be compared"; 202 return new DiscardInfo(this, DiscardCode.obvious, discardString); 203 } 204 205 return super.isObviousStatically(vis); 206 } 207 208 @Pure 209 @Override 210 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 211 DiscardInfo super_result = super.isObviousDynamically(vis); 212 if (super_result != null) { 213 return super_result; 214 } 215 216 if (core.a == 0) { 217 return new DiscardInfo(this, DiscardCode.obvious, var2().name() + " is constant"); 218 } 219 if (core.b == 0) { 220 return new DiscardInfo(this, DiscardCode.obvious, var1().name() + " is constant"); 221 } 222// if (core.a == 1 && core.b == 0) { 223// return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal"); 224// } 225 if (core.a == -core.b && core.c == 0) { 226 return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal"); 227 } 228 return null; 229 } 230 231 @Pure 232 @Override 233 public boolean isSameFormula(Invariant other) { 234 return core.isSameFormula(((LinearBinary) other).core); 235 } 236 237 @Pure 238 @Override 239 public boolean isExclusiveFormula(Invariant other) { 240 if (other instanceof LinearBinary) { 241 return core.isExclusiveFormula(((LinearBinary) other).core); 242 } 243 return false; 244 } 245 246 // Look up a previously instantiated invariant. 247 public static @Nullable LinearBinary find(PptSlice ppt) { 248 assert ppt.arity() == 2; 249 for (Invariant inv : ppt.invs) { 250 if (inv instanceof LinearBinary) { 251 return (LinearBinary) inv; 252 } 253 } 254 return null; 255 } 256 257 // Returns a vector of LinearBinary objects. 258 // This ought to produce an iterator instead. 259 public static List<LinearBinary> findAll(VarInfo vi) { 260 List<LinearBinary> result = new ArrayList<>(); 261 for (PptSlice view : vi.ppt.views_iterable()) { 262 if ((view.arity() == 2) && view.usesVar(vi)) { 263 LinearBinary lb = LinearBinary.find(view); 264 if (lb != null) { 265 result.add(lb); 266 } 267 } 268 } 269 return result; 270 } 271}