001package daikon.inv.binary; 002 003import static daikon.inv.Invariant.asInvClass; 004 005import daikon.PptSlice; 006import daikon.VarInfo; 007import daikon.inv.Invariant; 008import daikon.inv.InvariantStatus; 009import java.lang.reflect.Method; 010import org.checkerframework.checker.interning.qual.Interned; 011import org.checkerframework.checker.nullness.qual.Nullable; 012import org.checkerframework.dataflow.qual.Pure; 013import typequals.prototype.qual.Prototype; 014 015/** Provides a class that defines the functions that must exist for each two variable invariant. */ 016public abstract class BinaryInvariant extends Invariant { 017 // We are Serializable, so we specify a version to allow changes to 018 // method signatures without breaking serialization. If you add or 019 // remove fields, you should change this number to the current date. 020 static final long serialVersionUID = 20130808L; 021 022 protected BinaryInvariant(PptSlice ppt) { 023 super(ppt); 024 } 025 026 protected @Prototype BinaryInvariant() { 027 super(); 028 } 029 030 public abstract InvariantStatus check( 031 @Interned Object val1, @Interned Object val2, int mod_index, int count); 032 033 public abstract InvariantStatus add( 034 @Interned Object val1, @Interned Object val2, int mod_index, int count); 035 036 /** 037 * Applies the variables in the correct order. If the second variable is an array and the first 038 * variable is not, the order of the values is reversed (so that the array is always the first 039 * argument). 040 */ 041 public InvariantStatus add_unordered( 042 @Interned Object val1, @Interned Object val2, int mod_index, int count) { 043 044 VarInfo v1 = ppt.var_infos[0]; 045 VarInfo v2 = ppt.var_infos[1]; 046 047 // If one argument is scalar and the other an array, put the scalar first. 048 if (v2.rep_type.isArray() && !v1.rep_type.isArray()) { 049 return add(val2, val1, mod_index, count); 050 } else { 051 return add(val1, val2, mod_index, count); 052 } 053 } 054 055 /** 056 * Checks the specified values in the correct order. If the second value is an array and the first 057 * value is not, the order of the values is reversed (so that the array is always the first 058 * argument). 059 * 060 * <p>The values are checked rather than the variables because this is sometimes called on 061 * prototype invariants. 062 */ 063 public InvariantStatus check_unordered( 064 @Prototype BinaryInvariant this, 065 @Interned Object val1, 066 @Interned Object val2, 067 int mod_index, 068 int count) { 069 070 // If one argument is scalar and the other an array, put the scalar first. 071 if (((val2 instanceof long[]) || (val2 instanceof double[]) || (val2 instanceof String[])) 072 && !((val1 instanceof long[]) 073 || (val1 instanceof String[]) 074 || (val1 instanceof double[]))) { 075 return check(val2, val1, mod_index, count); 076 } else { 077 return check(val1, val2, mod_index, count); 078 } 079 } 080 081 /** 082 * Returns true if the binary function is symmetric (x,y ⇒ y,x). Subclasses that are 083 * symmetric should override. 084 */ 085 @Pure 086 public boolean is_symmetric() { 087 return false; 088 } 089 090 /** 091 * Returns the swap setting for invariants that support a swap boolean to handle different 092 * permutations. This version should never be called. 093 */ 094 public boolean get_swap() { 095 throw new Error("swap called in BinaryInvariant"); 096 } 097 098 /** 099 * Searches for the specified binary invariant (by class) in the specified slice. Returns null if 100 * the invariant is not found. 101 */ 102 protected @Nullable Invariant find(Class<? extends Invariant> cls, VarInfo v1, VarInfo v2) { 103 104 // find the slice containing v1 and v2 105 boolean fswap = false; 106 PptSlice ppt; 107 if (v1.varinfo_index > v2.varinfo_index) { 108 fswap = true; 109 ppt = this.ppt.parent.findSlice(v2, v1); 110 } else { 111 ppt = this.ppt.parent.findSlice(v1, v2); 112 } 113 if (ppt == null) { 114 return null; 115 } 116 117 // The following is complicated because we are inconsistent in 118 // how we handle permutations in binary invariants. Some 119 // invariants (notably the comparison invariants <=, >=, >, etc) 120 // use only one permutation, but have two different invariants (eg, 121 // < and >) to account for both orders. Other invariants (notably 122 // most of those in Numeric.java.jpp) keep a swap boolean that indicates 123 // the order of their arguments. Still others (such as == and 124 // BitwiseComplement) are symmetric and need only track one invariant 125 // for each argument pair. 126 // 127 // The classes with multiple invariants, must provide a static 128 // method named swap_class that provides the converse invariant. 129 // Symmetric invariants return true from is_symmetric(). Others 130 // must support the get_swap() method that returns the current 131 // swap setting. 132 133 // If the specified invariant has a different class when swapped 134 // find that class. 135 boolean swap_class = true; 136 try { 137 Method swap_method = cls.getMethod("swap_class", (Class<?>[]) null); 138 if (fswap) { 139 @SuppressWarnings("nullness") // static method, so null first arg is OK: swap_class() 140 Class<? extends Invariant> tmp_cls = 141 asInvClass(swap_method.invoke(null, (Object @Nullable []) null)); 142 cls = tmp_cls; 143 } 144 } catch (Exception e) { 145 swap_class = false; 146 } 147 148 // Loop through each invariant, looking for the matching class 149 for (Invariant inv : ppt.invs) { 150 BinaryInvariant bi = (BinaryInvariant) inv; 151 if (bi.getClass() == cls) { 152 if (bi.is_symmetric() || swap_class) { 153 return bi; 154 } else { 155 if (bi.get_swap() == fswap) { 156 return bi; 157 } 158 } 159 } 160 } 161 162 return null; 163 } 164}