0001: package U2.T2;
0002:
0003: import U2.T2.Obj.*;
0004: import U2.T2.Msg.*;
0005: import java.util.*;
0006: import java.lang.reflect.*;
0007: import java.io.*;
0008: import java.util.logging.*;
0009:
0010: /**
0011: * This class provides a meta representation of execution. An instance
0012: * of this class is called an execution trace. It is a meta
0013: * representation of an actual execution. For the big picture, see the
0014: * doc of the {@link U2.T2 U2.T2 package}. The important thing is that
0015: * from an execution trace we can reproduce the actual execution. It
0016: * can also be saved and reloaded; thus allowing us to later on replay
0017: * the actual execution.
0018: *
0019: * <p>A trace consists of a <u>creation step</u>, that creates the
0020: * target object, and a sequence of subsequent {@link
0021: * U2.T2.Trace.TraceStep trace steps}, each doing something on the
0022: * target object, e.g. calling a method on it. The creation step is an
0023: * instance of so called a {@link U2.T2.Trace.MkValStep MkVal} step. A
0024: * MkVal step is used to create an object, whereas a trace step is
0025: * used to apply side effect on the target object. A trace step may
0026: * also consist of MkVal steps, e.g. when it needs to create objects
0027: * to pass as parameters to a method.
0028: */
0029:
0030: public class Trace implements Serializable {
0031:
0032: // ---------------------------------------------------------------
0033: // The fields of a trace:
0034:
0035: /**
0036: * The creation step that starts this execution trace.
0037: */
0038: MkValStep creation = null;
0039:
0040: /**
0041: * The sequence of trace steps belonging to this execution trace.
0042: */
0043: LinkedList<TraceStep> trace;
0044:
0045: /**
0046: * The target object of this execution trace.
0047: */
0048: int indexOfTargetObj;
0049:
0050: /**
0051: * Used to classify different kind of traces, e.g. to distinguish
0052: * violating and non-violating traces. The purpose of this field is
0053: * mainly to quickly filter traces without having to execute them.
0054: */
0055: String classification = null;
0056:
0057: /**
0058: * Currently this is the only classification :)
0059: */
0060: static public String VIOLATING_TRACE = "VIOLATING TRACE";
0061:
0062: // Some variables to control the verbosity of the report:
0063: boolean printMethodParamsOption = true;
0064: boolean printIntermediateStepsOption = true;
0065: int showDepth = 6;
0066:
0067: // Logger:
0068: private static Logger logger = Logger.getLogger("U2.T2");
0069:
0070: /**
0071: * Create an empty execution trace.
0072: */
0073: public Trace() {
0074: trace = new LinkedList<TraceStep>();
0075: indexOfTargetObj = -1;
0076: }
0077:
0078: // ---------------------------------------------------------------
0079: // Nested class to construct the elements of a trace:
0080:
0081: /**
0082: * Representing a MkVal step.
0083: */
0084: public static abstract class MkValStep implements Serializable {
0085: }
0086:
0087: /**
0088: * A MkVal step in which an object is 'created' by picking it from
0089: * the {@link U2.T2.Pool object pool}. The Pool-ID of the picked
0090: * object will be remebered in this step.
0091: */
0092: public static class REF extends MkValStep {
0093: private int index;
0094:
0095: /**
0096: * @param i The Pool-ID of the object supplied by this step.
0097: */
0098: public REF(int i) {
0099: index = i;
0100: }
0101:
0102: public int getIndex() {
0103: return index;
0104: }
0105: }
0106:
0107: /**
0108: * A MkVal step in which an object is 'created' by picking a
0109: * 'constant', e.g. from the {@link U2.T2.BaseDomain base domain}.
0110: * The object used as 'constant' is remembered in this step.
0111: *
0112: */
0113: public static class CONST extends MkValStep {
0114: private Object val;
0115: // When val is null, then we can't ask via reflection what it
0116: // class was; so we'll also keep track the class as well. This
0117: // field is only setup when val is null:
0118: private Class C;
0119:
0120: /**
0121: * @param v The object used as the constant supplied by this step.
0122: */
0123: public CONST(Object v, Class E) {
0124: val = v;
0125: C = E;
0126: }
0127:
0128: public boolean isNull() {
0129: return val == null;
0130: }
0131:
0132: /**
0133: * For serialization.
0134: */
0135: private void writeObject(java.io.ObjectOutputStream stream)
0136: throws IOException {
0137: try {
0138: if (val == null) {
0139: stream.writeObject(C.getName());
0140: stream.writeObject("null");
0141: } else {
0142: stream.writeObject(val.getClass().getName());
0143: stream.writeObject("not null");
0144: stream.writeObject(val);
0145: }
0146: } catch (Exception e) {
0147: throw new IOException();
0148: }
0149: }
0150:
0151: /**
0152: * For serialization.
0153: */
0154: private void readObject(java.io.ObjectInputStream stream)
0155: throws IOException, ClassNotFoundException {
0156: try {
0157: C = classOf((String) stream.readObject());
0158: String isNull = (String) stream.readObject();
0159: if (isNull.equals("null"))
0160: val = null;
0161: else
0162: val = stream.readObject();
0163: } catch (ClassNotFoundException e) {
0164: throw e;
0165: } catch (Exception e) {
0166: throw new IOException();
0167: }
0168: }
0169: }
0170:
0171: /**
0172: * A MkVal step in which an object is created by calling a
0173: * constructor P. The constructor will be remembered in this step.
0174: * We also keep track of the MkVal steps needed to create the
0175: * objects needed as the parameters for P.
0176: */
0177: public static class CREATE_TARGET_OBJECT extends MkValStep {
0178: private Constructor con;
0179: private MkValStep[] params;
0180: /**
0181: * Set this to -1 if the index is still unknown.
0182: */
0183: int indexOfNewObject;
0184:
0185: /**
0186: * @param c The constructor used in this step.
0187: * @param ps MkVal steps needed to generate parameters for c.
0188: * @param index The Pool-ID of the newly created object.
0189: */
0190: public CREATE_TARGET_OBJECT(Constructor c, MkValStep[] ps,
0191: int index) {
0192: con = c;
0193: params = ps;
0194: indexOfNewObject = index;
0195: }
0196:
0197: /**
0198: * For serialization.
0199: */
0200: private void writeObject(java.io.ObjectOutputStream stream)
0201: throws IOException {
0202: try {
0203: stream.writeObject(con.getDeclaringClass().getName());
0204: Class[] paramTypes = con.getParameterTypes();
0205: String[] paramTypes_ = new String[paramTypes.length];
0206: for (int i = 0; i < paramTypes.length; i++)
0207: paramTypes_[i] = paramTypes[i].getName();
0208: stream.writeObject(paramTypes_);
0209: stream.writeObject(params);
0210: stream.writeInt(indexOfNewObject);
0211: } catch (Exception e) {
0212: throw new IOException();
0213: }
0214: }
0215:
0216: /**
0217: * For serialization.
0218: */
0219: private void readObject(java.io.ObjectInputStream stream)
0220: throws IOException, ClassNotFoundException {
0221: try {
0222: Class C = classOf((String) stream.readObject());
0223: String[] paramTypes_ = (String[]) stream.readObject();
0224: Class[] paramTypes = new Class[paramTypes_.length];
0225: for (int i = 0; i < paramTypes_.length; i++)
0226: paramTypes[i] = classOf(paramTypes_[i]);
0227: con = C.getConstructor(paramTypes);
0228: params = (MkValStep[]) stream.readObject();
0229: indexOfNewObject = stream.readInt();
0230: } catch (ClassNotFoundException e) {
0231: throw e;
0232: } catch (Exception e) {
0233: throw new IOException();
0234: }
0235: }
0236: }
0237:
0238: /**
0239: * Code.
0240: */
0241: public static final String ARRAY = "ARRAY";
0242:
0243: /**
0244: * A MkVal step where a collection like object is constructed. Set
0245: * collectionType to "ARRAY" to create an array, and else the name
0246: * of the class implementing Collection to make a collection.
0247: */
0248: public static class CREATE_COLLECTION_LIKE extends MkValStep {
0249: private String collectionType;
0250: private Class elementType;
0251: private int size;
0252: private MkValStep[] elements;
0253:
0254: public CREATE_COLLECTION_LIKE(String Ctype, Class ElemTy,
0255: int n, MkValStep[] elems) {
0256: collectionType = Ctype;
0257: elementType = ElemTy;
0258: size = n;
0259: elements = elems;
0260: }
0261:
0262: /**
0263: * For serialization.
0264: */
0265: private void writeObject(java.io.ObjectOutputStream stream)
0266: throws IOException {
0267: try {
0268: stream.writeObject(collectionType);
0269: stream.writeObject(elementType.getName());
0270: stream.writeInt(size);
0271: stream.writeObject(elements);
0272: } catch (Exception e) {
0273: throw new IOException();
0274: }
0275: }
0276:
0277: /**
0278: * For serialization.
0279: */
0280: private void readObject(java.io.ObjectInputStream stream)
0281: throws IOException, ClassNotFoundException {
0282: try {
0283: collectionType = (String) stream.readObject();
0284: String elementType_ = (String) stream.readObject();
0285: elementType = classOf(elementType_);
0286: size = stream.readInt();
0287: elements = (MkValStep[]) stream.readObject();
0288: } catch (ClassNotFoundException e) {
0289: throw e;
0290: } catch (Exception e) {
0291: throw new IOException();
0292: }
0293: }
0294: }
0295:
0296: private static Class classOf(String cname)
0297: throws ClassNotFoundException {
0298: if (cname.equals("boolean"))
0299: return Boolean.TYPE;
0300: if (cname.equals("byte"))
0301: return Byte.TYPE;
0302: if (cname.equals("int"))
0303: return Integer.TYPE;
0304: if (cname.equals("long"))
0305: return Long.TYPE;
0306: if (cname.equals("character"))
0307: return Character.TYPE;
0308: if (cname.equals("float"))
0309: return Float.TYPE;
0310: if (cname.equals("double"))
0311: return Double.TYPE;
0312: return Class.forName(cname);
0313: }
0314:
0315: /**
0316: * Representing trace steps.
0317: */
0318: public static abstract class TraceStep implements Serializable {
0319:
0320: abstract public String getName();
0321: }
0322:
0323: /**
0324: * A trace step where we update a field of the target object.
0325: */
0326: public static class UPDATE_FIELD extends TraceStep {
0327: private Field field;
0328: private MkValStep val;
0329:
0330: /**
0331: * @param f The field to update.
0332: * @param v A MkVal step producing a new value for the field f.
0333: */
0334: public UPDATE_FIELD(Field f, MkValStep v) {
0335: field = f;
0336: val = v;
0337: }
0338:
0339: public String getName() {
0340: return field.getName();
0341: }
0342:
0343: /**
0344: * For serialization.
0345: */
0346: private void writeObject(java.io.ObjectOutputStream stream)
0347: throws IOException {
0348: try {
0349: stream.writeObject(field.getDeclaringClass().getName());
0350: stream.writeObject(field.getName());
0351: stream.writeObject(val);
0352: } catch (Exception e) {
0353: throw new IOException();
0354: }
0355: }
0356:
0357: /**
0358: * For serialization.
0359: */
0360: private void readObject(java.io.ObjectInputStream stream)
0361: throws IOException, ClassNotFoundException {
0362: try {
0363: Class C = classOf((String) stream.readObject());
0364: String fieldName = (String) stream.readObject();
0365: field = C.getField(fieldName);
0366: val = (MkValStep) stream.readObject();
0367: } catch (ClassNotFoundException e) {
0368: throw e;
0369: } catch (Exception e) {
0370: throw new IOException();
0371: }
0372: }
0373:
0374: }
0375:
0376: /**
0377: * A trace step where we call a method.
0378: */
0379: public static class CALL_METHOD extends TraceStep {
0380: private Method method;
0381: // When it is null then the method is static. Else it is
0382: // the receiver of the call.
0383: private MkValStep receiver;
0384: private MkValStep[] params;
0385:
0386: /**
0387: * @param m The method to call. If the method is static, set r to null.
0388: * @param r MkVal step producing the receiver object.
0389: * @param ps MkVal steps produducing the arguments for r.
0390: */
0391: public CALL_METHOD(Method m, MkValStep r, MkValStep[] ps) {
0392: method = m;
0393: receiver = r;
0394: params = ps;
0395: }
0396:
0397: public String getName() {
0398: return method.getName();
0399: }
0400:
0401: /**
0402: * For serialization.
0403: */
0404: private void writeObject(java.io.ObjectOutputStream stream)
0405: throws IOException {
0406: try {
0407: stream
0408: .writeObject(method.getDeclaringClass()
0409: .getName());
0410: stream.writeObject(method.getName());
0411: Class[] paramTypes = method.getParameterTypes();
0412: String[] paramTypes_ = new String[paramTypes.length];
0413: for (int i = 0; i < paramTypes.length; i++)
0414: paramTypes_[i] = paramTypes[i].getName();
0415: stream.writeObject(paramTypes_);
0416: stream.writeObject(receiver);
0417: stream.writeObject(params);
0418: } catch (Exception e) {
0419: throw new IOException();
0420: }
0421: }
0422:
0423: /**
0424: * For serialization.
0425: */
0426: private void readObject(java.io.ObjectInputStream stream)
0427: throws IOException, ClassNotFoundException {
0428: try {
0429: Class C = classOf((String) stream.readObject());
0430: String methodName = (String) stream.readObject();
0431: String[] paramTypes_ = (String[]) stream.readObject();
0432: Class[] paramTypes = new Class[paramTypes_.length];
0433: for (int i = 0; i < paramTypes_.length; i++)
0434: paramTypes[i] = classOf(paramTypes_[i]);
0435: method = C.getMethod(methodName, paramTypes);
0436: receiver = (MkValStep) stream.readObject();
0437: params = (MkValStep[]) stream.readObject();
0438: } catch (ClassNotFoundException e) {
0439: throw e;
0440: } catch (Exception e) {
0441: throw new IOException();
0442: }
0443: }
0444: }
0445:
0446: // ---------------------------------------------------------------
0447:
0448: /**
0449: * Execute a given MkVal step to construct an object.
0450: */
0451: public static Object MkVal(Pool pool, MkValStep step)
0452:
0453: throws InvocationTargetException
0454:
0455: {
0456:
0457: // System.out.println(">" + step.getClass() . getName()) ;
0458: // System.out.print("@ " + Show.show(step)) ;
0459:
0460: // note the cloning in CONST-case:
0461:
0462: if (step instanceof CONST) {
0463:
0464: if (((CONST) step).val == null)
0465: return null;
0466:
0467: try {
0468: return Cloner.clone(((CONST) step).val);
0469: }
0470:
0471: catch (Exception e) {
0472:
0473: Message
0474: .throwT2Error(
0475: T2Error.ABORT,
0476: "Fail to clone. Perhaps because Base Domain contains unclonable objects.",
0477: e);
0478: }
0479: }
0480: if (step instanceof REF)
0481: return pool.get(((REF) step).index);
0482: if (step instanceof CREATE_TARGET_OBJECT) {
0483: CREATE_TARGET_OBJECT step_ = (CREATE_TARGET_OBJECT) step;
0484: Object[] args = new Object[step_.params.length];
0485: for (int i = 0; i < step_.params.length; i++)
0486: args[i] = MkVal(pool, step_.params[i]);
0487: Object newobject = null;
0488:
0489: try {
0490: newobject = step_.con.newInstance(args);
0491: }
0492:
0493: // handles InstantiationException too. INCOMPLETE
0494:
0495: catch (InvocationTargetException e) {
0496: throw e;
0497: }
0498:
0499: catch (Exception e) {
0500:
0501: // System.out.println("## " + step_.con.getName()) ;
0502: // System.out.println("## " + Show.show(e)) ;
0503:
0504: Message.throwT2Error(T2Error.BUG,
0505: "Failure to create object via "
0506: + step_.con.getName(), e);
0507: }
0508: int index = pool.put(newobject);
0509: if (step_.indexOfNewObject == -1)
0510: step_.indexOfNewObject = index;
0511: assert (index == step_.indexOfNewObject);
0512: return newobject;
0513: }
0514:
0515: if (step instanceof CREATE_COLLECTION_LIKE) {
0516: CREATE_COLLECTION_LIKE step_ = (CREATE_COLLECTION_LIKE) step;
0517:
0518: if (step_.collectionType.equals(ARRAY)) {
0519: Object array = Array.newInstance(step_.elementType,
0520: step_.size);
0521: for (int i = 0; i < step_.size; i++)
0522: Array.set(array, i, MkVal(pool, step_.elements[i]));
0523: return array;
0524: }
0525: // ELSE:
0526: Collection col = null;
0527: try {
0528: col = (Collection) Class.forName(step_.collectionType)
0529: .newInstance();
0530: } catch (Exception e) {
0531: }
0532: // if (step_.collectionType == LINKEDLIST) col = new LinkedList() ;
0533: // if (step_.collectionType == HASHSET) col = new HashSet() ;
0534: if (col != null) {
0535: for (int i = 0; i < step_.size; i++)
0536: col.add(MkVal(pool, step_.elements[i]));
0537: return col;
0538: }
0539: }
0540:
0541: // System.out.println("# " + Show.show(step)) ;
0542:
0543: Message.throwT2Error(T2Error.BUG, Message.ILLEGAL_STATE);
0544: return null;
0545: }
0546:
0547: /**
0548: * As the other MkVal, but this one executes multiple steps.
0549: */
0550: public static Object[] MkVal(Pool pool, MkValStep[] steps)
0551:
0552: throws InvocationTargetException
0553:
0554: {
0555: Object[] objs = new Object[steps.length];
0556: for (int i = 0; i < steps.length; i++)
0557: objs[i] = MkVal(pool, steps[i]);
0558: return objs;
0559: }
0560:
0561: /**
0562: * As MkVal, but especially for constructing a target object. It will
0563: * also execute the classinvariant.
0564: */
0565: public static ExecResult MkTargetObject(Pool pool, MkValStep step,
0566: Method classinv) throws InvocationTargetException {
0567: Object targetObj = MkVal(pool, step);
0568: update_aux_laststep(targetObj, targetObj.getClass().getName());
0569: ExecResult result = new ExecResult();
0570: execClassInv(classinv, targetObj, result);
0571: result.returnedObj = targetObj;
0572: return result;
0573: }
0574:
0575: public static class ExecResult {
0576:
0577: protected Object returnedObj = null;
0578: /**
0579: * Exception thrown but not unexpected.
0580: */
0581: protected Exception returnedException = null;
0582: protected AssertionError precViolation = null;
0583: /**
0584: * Violation to postcodition or other non-precond. assertion.
0585: */
0586: protected AssertionError postcViolation = null;
0587: /**
0588: * Internal error or (unexpected) runtime exception thrown.
0589: */
0590: protected Throwable internalError = null;
0591: protected AssertionError appmodViolation = null;
0592: protected Throwable classinvExecptionalViolation = null;
0593: protected boolean classinvViolation = false;
0594:
0595: /**
0596: * Return true if the result indicates a violation to either pre-cond
0597: * or app. model.
0598: */
0599: public boolean isAsmViolating() {
0600: return (precViolation != null) || (appmodViolation != null);
0601: }
0602:
0603: /**
0604: * Return true if the result indicates a violation to either post-cond
0605: * or classinv.
0606: */
0607: public boolean isReqViolating() {
0608: return classinvViolation || (postcViolation != null)
0609: || (internalError != null);
0610: }
0611:
0612: /**
0613: * True if either isAsmViolating or isReqViolating.
0614: */
0615: public boolean isViolating() {
0616: return isAsmViolating() || isReqViolating();
0617: }
0618:
0619: /**
0620: * For reporting this result.
0621: */
0622: public void report(Show Shower, PrintStream out) {
0623:
0624: if (returnedObj != null) {
0625: out.println(" ** Return value:");
0626: out.println(Shower.showWithContNum(returnedObj));
0627: }
0628: if (returnedException != null)
0629: out.println(" ** Throwing (expected) "
0630: + returnedException);
0631:
0632: if (precViolation != null)
0633: out.println(" xx Pre-condition VIOLATED!");
0634:
0635: if (appmodViolation != null)
0636: out.println(" xx Application model VIOLATED!");
0637:
0638: if (postcViolation != null)
0639: out.println(" xx Assertion VIOLATED!");
0640:
0641: if (classinvViolation)
0642: out.println(" xx Class invariant VIOLATED!");
0643:
0644: if (classinvExecptionalViolation != null) {
0645: out.println(" xx Class invariant throws (UNEXPECTED) "
0646: + classinvExecptionalViolation);
0647: out.println(" ** Strack trace: ");
0648: classinvExecptionalViolation.printStackTrace(out);
0649: }
0650:
0651: if (internalError != null) {
0652: out.println(" xx INTERNAL ERROR!");
0653: out.println(" ** Strack trace: ");
0654: internalError.printStackTrace(out);
0655: }
0656:
0657: }
0658: }
0659:
0660: /**
0661: * Execute (and check) the given class invariant.
0662: *
0663: * @param classinv The method specifying the class invariant.
0664: * @param result Information about violations found will be put in here.
0665: */
0666: public static void execClassInv(Method classinv, Object targetObj,
0667: ExecResult result) {
0668:
0669: if (classinv == null)
0670: return;
0671:
0672: result.classinvViolation = false;
0673: try {
0674: result.classinvViolation = !(Boolean) (classinv.invoke(
0675: targetObj, (Object[]) null));
0676: }
0677:
0678: catch (InvocationTargetException e) {
0679: Throwable c = e.getCause();
0680: // This is to handle application model, encoded as pre-cond of
0681: // class invariant:
0682: if (c instanceof AssertionError
0683: && c.getMessage().startsWith("APPMODEL"))
0684:
0685: result.appmodViolation = (AssertionError) c;
0686: // Note that ANY exception in classinv, even from appmodel will be
0687: // considered as classinv violation. The exception will later
0688: // be reported.
0689: else
0690: result.classinvExecptionalViolation = c;
0691: } catch (Exception e) {
0692: Message.throwT2Error(T2Error.BUG,
0693: "Fail to invoke the classinvariant.");
0694: }
0695: }
0696:
0697: /**
0698: * Method to fill-in the aux_laststep hook.
0699: */
0700: static protected void update_aux_laststep(Object targetObj,
0701: String step) {
0702: try {
0703: Field laststep_hook = targetObj.getClass()
0704: .getDeclaredField("aux_laststep");
0705: String step_ = step;
0706: if (step_.endsWith("_spec"))
0707: step_ = step.substring(0, step.length() - 5);
0708: laststep_hook.set(targetObj, step_);
0709: } catch (Exception e) {
0710: }
0711: }
0712:
0713: /**
0714: * Execute a given trace step. If a printstream is also given, this
0715: * methdo will also report the execution to the stream.
0716: *
0717: * @param out If not null will cause objects involed in this step to be
0718: * textually reported to this print stream.
0719: *
0720: * @param printMethodParamsOption If true, and if this step is a method
0721: * calls, the parameters to the call will be printed
0722: * in the report.
0723: *
0724: * @param Shower A shower object need to be passed; it is used to
0725: * show (print) an object, but we also need to maintain object
0726: * numbering across different the entire execution; the show
0727: * object internally maintains this numbering.
0728: *
0729: */
0730: public static ExecResult exec(Pool pool, Object targetObj,
0731: TraceStep step, Method classinv, PrintStream out,
0732: boolean printMethodParamsOption, Show Shower) {
0733: ExecResult result = new ExecResult();
0734:
0735: update_aux_laststep(targetObj, step.getName());
0736:
0737: if (step instanceof UPDATE_FIELD) {
0738: UPDATE_FIELD step_ = (UPDATE_FIELD) step;
0739:
0740: // System.out.println(">" + step_.field.getName()) ;
0741: // System.out.println(">" + MkVal(pool,step_.val)) ;
0742: // System.out.println("+" + targetObj) ;
0743:
0744: try {
0745: Object newFieldVal = MkVal(pool, step_.val);
0746: step_.field.set(targetObj, newFieldVal);
0747: if (out != null) {
0748: out.println(" ** Update on "
0749: + step_.field.getName() + " with:");
0750: out.println(Shower.showWithContNum(newFieldVal));
0751: }
0752: } catch (Exception e) {
0753: Message.throwT2Error(T2Error.BUG,
0754: "Failure to update field "
0755: + step_.field.getName(), e);
0756: }
0757: // now goto the END
0758: } else if (step instanceof CALL_METHOD) {
0759: CALL_METHOD step_ = (CALL_METHOD) step;
0760: Object receiver = null;
0761: Object[] args = null;
0762:
0763: try {
0764: // receiver is null if the method is static
0765: if (step_.receiver != null)
0766: receiver = MkVal(pool, step_.receiver);
0767: args = MkVal(pool, step_.params);
0768: } catch (InvocationTargetException e) {
0769: if (out != null)
0770: out
0771: .println(" ** Cancelling call to "
0772: + step_.method.getName()
0773: + ", because failing to construct its arguments!");
0774: return result;
0775: }
0776: // System.out.println("@" + step_ . method . getName()) ;
0777: // Reporting actual arguments:
0778: if (out != null) {
0779: out.println(" ** Calling method "
0780: + step_.method.getName() + " with:");
0781: if (receiver != null) {
0782: out.print(" ** Receiver: ");
0783: if (targetObj == receiver)
0784: out.println("target-obj");
0785: else {
0786: out.println("");
0787: out.println(Shower.showWithContNum(receiver));
0788: }
0789: }
0790: if (printMethodParamsOption) {
0791: for (int i = 0; i < args.length; i++) {
0792: out.print(" ** Arg [" + i + ":]");
0793: if (args[i] == targetObj)
0794: out.println("target-obj");
0795: else {
0796: out.println("");
0797: out
0798: .println(Shower
0799: .showWithContNum(args[i]));
0800: }
0801: }
0802: }
0803: }
0804:
0805: try {
0806: result.returnedObj = step_.method
0807: .invoke(receiver, args);
0808: }
0809:
0810: catch (InvocationTargetException e) {
0811: Throwable exc = e.getCause();
0812:
0813: // could be spec violation:
0814: if (exc instanceof AssertionError) {
0815: AssertionError assErr = (AssertionError) exc;
0816: if (assErr.getMessage().startsWith("PRE"))
0817: result.precViolation = assErr;
0818: else
0819: result.postcViolation = assErr;
0820: }
0821: // or internal error or runtime exception:
0822: else if (exc instanceof Error
0823: || exc instanceof RuntimeException)
0824: result.internalError = exc;
0825: // else it is considered an expected exception:
0826: else
0827: result.returnedException = (Exception) exc;
0828:
0829: } catch (Exception e) {
0830: // System.out.println(Show.show(receiver)) ;
0831: // e.printStackTrace() ;
0832: Message.throwT2Error(T2Error.BUG,
0833: "Failure to invoke method "
0834: + step_.method.getName(), e);
0835: }
0836: // proceed to END
0837: }
0838: // END:
0839: execClassInv(classinv, targetObj, result);
0840: // reporting the step result:
0841: if (out != null) {
0842: out.println(" ** Target object after the step:");
0843: out.println(Shower.showWithContNum(targetObj));
0844: }
0845: return result;
0846: }
0847:
0848: /**
0849: * As the other exec, but this does not produce report.
0850: */
0851: public static ExecResult exec(Pool pool, Object targetObj,
0852: TraceStep step, Method classinv)
0853:
0854: {
0855: return exec(pool, targetObj, step, classinv, null, false, null);
0856: }
0857:
0858: private static final String lineHsep1 = " -----------------------------------";
0859: private static final String lineHsep2 = " --------";
0860:
0861: /**
0862: * This method is used to report the states, methods called,
0863: * parameters passed along an execution induced by a trace. Note
0864: * that to be able to do so, the execution has to be
0865: * reconstructed. Violations will not be checked. This is assumed
0866: * to has been done by whatever phases that preceed reporting.
0867: *
0868: * @param pool Pass here the same pool as used to produce this
0869: * execution trace.
0870: * @param out The steam to which the report will be printed;
0871: * should not be null.
0872: */
0873: public void report(Pool pool, Method classinv, PrintStream out)
0874:
0875: {
0876: Show Shower = new Show(showDepth, 6);
0877:
0878: pool.reset();
0879: Object targetObj = null;
0880: ExecResult result = null;
0881:
0882: try {
0883: result = MkTargetObject(pool, creation, classinv);
0884: } catch (InvocationTargetException e) {
0885: Throwable cause = e.getCause();
0886: out.println(" ** FAIL CREATING target object! Throwing "
0887: + cause + " . Stack trace:");
0888: cause.printStackTrace(out);
0889: return;
0890: }
0891: int count = 0;
0892: targetObj = pool.get(indexOfTargetObj);
0893:
0894: out.println(" ** CREATING target object.");
0895: // out.println(Shower.showWithContNum(targetObj)) ;
0896: result.report(Shower, out);
0897: if (result.isViolating())
0898: return;
0899:
0900: for (TraceStep step : trace) {
0901: count++;
0902: if (!printIntermediateStepsOption
0903: && count < trace.size() - 2) {
0904: result = exec(pool, targetObj, step, classinv, null,
0905: false, Shower);
0906: if (result.isViolating())
0907: result.report(Shower, out);
0908: } else {
0909: out.println(" ** STEP " + count + ".");
0910: result = exec(pool, targetObj, step, classinv, out,
0911: printMethodParamsOption, Shower);
0912: result.report(Shower, out);
0913: }
0914: if (result.isViolating())
0915: break;
0916: }
0917: // out.println(lineHsep2) ;
0918: // out.println(" ** Final state of target object:") ;
0919: // out.println(Shower.showWithContNum(targetObj)) ;
0920: out.println(lineHsep1);
0921: }
0922:
0923: /**
0924: * For saving execution traces. They will be saved in the file
0925: * name.tr where name is CUT's simple name.
0926: *
0927: * @param CUT The target class to which the traces belong.
0928: */
0929: public static void save(Class CUT, LinkedList<Trace> traces)
0930: throws T2Exception {
0931: try {
0932: String fname = CUT.getSimpleName() + ".tr";
0933: ObjectOutputStream oos = new ObjectOutputStream(
0934: new FileOutputStream(fname));
0935: oos.writeObject(CUT.getName());
0936: // System.out.println("### " + CUT.getName()) ;
0937: oos.writeObject(traces);
0938: oos.close();
0939: } catch (NotSerializableException e) {
0940: Message
0941: .throwT2Error(
0942: T2Error.ABORT,
0943: "A part of execution trace turns out to be unserializable.",
0944: e);
0945: } catch (InvalidClassException e) {
0946: Message
0947: .throwT2Error(
0948: T2Error.ABORT,
0949: "A part of execution trace turns out to be unserializable.",
0950: e);
0951: } catch (Exception e) {
0952: throw new T2Exception(Message.mk(Message.PROBLEM,
0953: "Fail to save execution traces.", e));
0954: }
0955: }
0956:
0957: /**
0958: * For loading execution traces from a single save-file. The file
0959: * is assumed to be called name.tr where name is CUT's simple name.
0960: *
0961: * @param CUT The target class to which the traces belong.
0962: */
0963: public static LinkedList<Trace> load(Class CUT) throws T2Exception {
0964:
0965: LinkedList<Trace> traces = null;
0966: String fname = CUT.getSimpleName() + ".tr";
0967: try {
0968: ObjectInputStream ois = new ObjectInputStream(
0969: new FileInputStream(fname));
0970: String className = (String) ois.readObject();
0971: if (!className.equals(CUT.getName())) {
0972: String msg = Message.mk(Message.PROBLEM, "The file "
0973: + fname + " does not contain traces for class "
0974: + CUT.getSimpleName() + ".");
0975: throw new IOException(msg);
0976: } else
0977: traces = (LinkedList<Trace>) ois.readObject();
0978: ois.close();
0979: } catch (Exception e) {
0980: throw new T2Exception(Message.mk(Message.PROBLEM,
0981: "Fail to load execution traces.", e));
0982: }
0983:
0984: return traces;
0985: }
0986:
0987: // test, comment off the rest in simulate first!!
0988: public static void main(String[] args) {
0989: A a1 = new A("Alice");
0990: A a2 = new A("Bob");
0991: A2 a3 = new A2("Vilain", 100);
0992: A2 a4 = new A2("Vilain", 999);
0993:
0994: Pool p = new Pool();
0995: p.put(a1);
0996: p.put(a2);
0997: p.put(a3);
0998: p.put(a4);
0999:
1000: Trace tau = new Trace();
1001: tau.creation = new REF(2); // index of a3
1002: tau.indexOfTargetObj = 2;
1003:
1004: try {
1005: tau.trace.add(new UPDATE_FIELD(a3.getClass().getField("n"),
1006: new CONST("Good guy", null)));
1007:
1008: tau.trace.add(new UPDATE_FIELD(a3.getClass().getField("x"),
1009: new CONST(new Integer(111), null)));
1010: } catch (Exception e) {
1011: System.out.println("!!!");
1012: }
1013: tau.report(p, null, System.out);
1014:
1015: }
1016:
1017: }
|