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