00001 package edu.ksu.cis.bandera.abstraction;
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036 import ca.mcgill.sable.soot.grimp.*;
00037 import ca.mcgill.sable.soot.jimple.*;
00038 import edu.ksu.cis.bandera.jext.*;
00039 import edu.ksu.cis.bandera.abstraction.typeinference.*;
00040 import edu.ksu.cis.bandera.abstraction.util.*;
00041 import java.util.*;
00042 public class PredicateInterpreter extends AbstractBanderaValueSwitch {
00043 private TypeTable typeTable;
00044 private Vector variables;
00045 private int[] tokens;
00046 private int result;
00047 public void caseAddExpr(AddExpr v) {
00048 doOp(v, "add", false);
00049 }
00050 public void caseAndExpr(AndExpr v) {
00051 doOp(v, "and", false);
00052 }
00053 public void caseArrayRef(ArrayRef v) {
00054 result = tokens[variables.indexOf(v)];
00055 }
00056 public void caseDivExpr(DivExpr v) {
00057 doOp(v, "div", false);
00058 }
00059 public void caseDoubleConstant(DoubleConstant v) {
00060 String aName = typeTable.get(v).getClass().getName();
00061 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {double.class}, null, new Object[] {new Double(v.value)})).intValue();
00062 }
00063 public void caseEqExpr(EqExpr v) {
00064 doOp(v, "eq", true);
00065 }
00066 public void caseFloatConstant(FloatConstant v) {
00067 String aName = typeTable.get(v).getClass().getName();
00068 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {double.class}, null, new Object[] {new Double(v.value)})).intValue();
00069 }
00070 public void caseGeExpr(GeExpr v) {
00071 doOp(v, "ge", true);
00072 }
00073 public void caseGtExpr(GtExpr v) {
00074 doOp(v, "gt", true);
00075 }
00076 public void caseInstanceFieldRef(InstanceFieldRef v) {
00077 result = tokens[variables.indexOf(v)];
00078 }
00079 public void caseIntConstant(IntConstant v) {
00080 Abstraction a = typeTable.get(v);
00081 String aName = a.getClass().getName();
00082 if (a instanceof RealAbstraction) {
00083 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {double.class}, null, new Object[] {new Double(v.value)})).intValue();
00084 } else if (a instanceof IntegralAbstraction) {
00085 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {long.class}, null, new Object[] {new Long(v.value)})).intValue();
00086 } else {
00087 throw new RuntimeException("Error in predicate interpreter");
00088 }
00089 }
00090 public void caseLeExpr(LeExpr v) {
00091 doOp(v, "le", true);
00092 }
00093 public void caseLengthExpr(LengthExpr v) {
00094 result = tokens[variables.indexOf(v)];
00095 }
00096
00097
00098
00099
00100 public void caseLocalExpr(LocalExpr v) {
00101 result = tokens[variables.indexOf(v)];
00102 }
00103 public void caseLongConstant(LongConstant v) {
00104 Abstraction a = typeTable.get(v);
00105 String aName = a.getClass().getName();
00106 if (a instanceof RealAbstraction) {
00107 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {double.class}, null, new Object[] {new Double(v.value)})).intValue();
00108 } else if (a instanceof IntegralAbstraction) {
00109 result = 1 << ((Integer) AbstractionClassLoader.invokeMethod(aName, "abs", new Class[] {long.class}, null, new Object[] {new Long(v.value)})).intValue();
00110 } else {
00111 throw new RuntimeException("Error in predicate interpreter");
00112 }
00113 }
00114 public void caseLtExpr(LtExpr v) {
00115 doOp(v, "lt", true);
00116 }
00117 public void caseMulExpr(MulExpr v) {
00118 doOp(v, "mul", false);
00119 }
00120 public void caseNeExpr(NeExpr v) {
00121 doOp(v, "ne", true);
00122 }
00123 public void caseNegExpr(NegExpr v) {
00124 }
00125 public void caseOrExpr(OrExpr v) {
00126 doOp(v, "or", false);
00127 }
00128 public void caseRemExpr(RemExpr v) {
00129 doOp(v, "rem", false);
00130 }
00131 public void caseShlExpr(ShlExpr v) {
00132 doOp(v, "shl", false);
00133 }
00134 public void caseShrExpr(ShrExpr v) {
00135 doOp(v, "shr", false);
00136 }
00137 public void caseStaticFieldRef(StaticFieldRef v) {
00138 result = tokens[variables.indexOf(v)];
00139 }
00140 public void caseSubExpr(SubExpr v) {
00141 doOp(v, "sub", false);
00142 }
00143 public void caseUshrExpr(UshrExpr v) {
00144 doOp(v, "ushr", false);
00145 }
00146 public void caseXorExpr(XorExpr v) {
00147 doOp(v, "xor", false);
00148 }
00149
00150
00151
00152
00153 public void defaultCase(Object o) {
00154 throw new RuntimeException(o + " is not handled by the predicate interpreter");
00155 }
00156
00157
00158
00159
00160
00161 private void doOp(BinopExpr v, String methodName, boolean isTest) {
00162 Abstraction a = typeTable.get(v);
00163 v.getOp1().apply(this);
00164 int v1 = result;
00165 v.getOp2().apply(this);
00166 int v2 = result;
00167 try {
00168 if (isTest) {
00169 result = ((Byte) AbstractionClassLoader.invokeMethod(a.getClass().getName(), methodName + "Set", new Class[] {int.class, int.class}, null, new Object[] {new Integer(v1), new Integer(v2)})).intValue();
00170 } else {
00171 result = ((Integer) AbstractionClassLoader.invokeMethod(a.getClass().getName(), methodName + "Set", new Class[] {int.class, int.class}, null, new Object[] {new Integer(v1), new Integer(v2)})).intValue();
00172 }
00173 if (result == -1 || (!isTest && (result == 0))) {
00174 throw new Exception(v + " give result an invalid token set");
00175 }
00176 } catch (Exception e) {
00177 throw new RuntimeException(e.getMessage());
00178 }
00179 }
00180
00181
00182
00183
00184
00185
00186
00187
00188 public boolean isFalse(TypeTable typeTable, Vector variables, int[] tokens, Value v) {
00189 this.typeTable = typeTable;
00190 this.variables = variables;
00191 this.tokens = tokens;
00192 v.apply(this);
00193 return result == Abstraction.FALSE;
00194 }
00195
00196
00197
00198
00199
00200
00201
00202
00203 public boolean isTop(TypeTable typeTable, Vector variables, int[] tokens, Value v) {
00204 this.typeTable = typeTable;
00205 this.variables = variables;
00206 this.tokens = tokens;
00207 v.apply(this);
00208 return result == Abstraction.TRUE_OR_FALSE;
00209 }
00210
00211
00212
00213
00214
00215 public boolean isTrue(TypeTable typeTable, Vector variables, int[] tokens, Value v) {
00216 this.typeTable = typeTable;
00217 this.variables = variables;
00218 this.tokens = tokens;
00219 v.apply(this);
00220 return result == Abstraction.TRUE;
00221 }
00222 }