001: package javacard.framework;
002:
003: import de.uka.ilkd.key.javacard.*;
004:
005: /** Some of the methods in this class do not have any spec. This
006: * is because it is better to execute them symbolically (inline the
007: * implementation) in a KeY proof and let dedicated taclets for jvm*
008: * methods take care of the rest. Such no spec methods are marked
009: * with "no spec"
010: */
011: public class Util {
012:
013: // In principle this method could have a spec, but it would be
014: // very elaborate and very difficult for the src == dest case, so:
015: //
016: // no spec
017: public static short arrayCopy(byte[] src, short srcOff,
018: byte[] dest, short destOff, short length)
019: throws TransactionException {
020: if (src == null || dest == null)
021: throw new NullPointerException();
022: if (length < 0 || srcOff < 0 || destOff < 0
023: || (short) (srcOff + length) > src.length
024: || (short) (destOff + length) > dest.length)
025: throw new ArrayIndexOutOfBoundsException();
026: // arrayCopy is supposed to be atomic if the destination is
027: // persistent, start a transaction, unless there is one
028: // already
029: final boolean doTransaction = JCSystem.isTransient(dest) == JCSystem.NOT_A_TRANSIENT_OBJECT
030: && JCSystem.getTransactionDepth() == (byte) 0;
031: if (doTransaction)
032: KeYJCSystem.jvmBeginTransaction();
033: // From now on we use jvmArrayCopy, which should be "well formed", i.e.
034: // it will not throw any exception. In a KeY proof
035: // it will be treated by a dedicated taclet.
036: if (src == dest) {
037: byte[] _tempArray = new byte[length];
038: KeYJCSystem.jvmArrayCopy(src, srcOff, _tempArray,
039: (short) 0, length);
040: KeYJCSystem.jvmArrayCopy(_tempArray, (short) 0, dest,
041: destOff, length);
042: } else {
043: KeYJCSystem
044: .jvmArrayCopy(src, srcOff, dest, destOff, length);
045: }
046: if (doTransaction)
047: KeYJCSystem.jvmCommitTransaction();
048: return (short) (destOff + length);
049: }
050:
051: // Same as above: no spec
052: public static short arrayCopyNonAtomic(byte[] src, short srcOff,
053: byte[] dest, short destOff, short length) {
054:
055: if (src == null || dest == null)
056: throw new NullPointerException();
057: if (length < 0 || srcOff < 0 || destOff < 0
058: || srcOff + length > src.length
059: || destOff + length > dest.length)
060: throw new ArrayIndexOutOfBoundsException();
061: // From now on we use jvmArrayCopy and jvmArrayCopyNonAtomic,
062: // which should be "well formed", i.e. they will not throw any exception.
063: // In a KeY proof they will be treated by dedicated taclets.
064: if (src == dest) {
065: byte[] _tempArray = new byte[length];
066: KeYJCSystem.jvmArrayCopy(src, srcOff, _tempArray,
067: (short) 0, length);
068: KeYJCSystem.jvmArrayCopyNonAtomic(_tempArray, (short) 0,
069: dest, destOff, length);
070: } else {
071: KeYJCSystem.jvmArrayCopyNonAtomic(src, srcOff, dest,
072: destOff, length);
073: }
074: return (short) (destOff + length);
075: }
076:
077: // Same as above: no spec
078: public static short arrayFillNonAtomic(byte[] bArray, short bOff,
079: short bLen, byte bValue) {
080: if (bArray == null)
081: throw new NullPointerException();
082: if (bLen < 0 || bOff < 0
083: || (short) (bOff + bLen) > bArray.length)
084: throw new ArrayIndexOutOfBoundsException();
085: // From now on we use jvmArrayFillNonAtomic, which should be
086: // "well formed", i.e. it will not throw any exception.
087: // In a KeY proof it will be treated by a dedicated taclet.
088: KeYJCSystem.jvmArrayFillNonAtomic(bArray, bOff, bLen, bValue);
089: return (short) (bOff + bLen);
090: }
091:
092: /*@ normal_behavior
093: requires src != null;
094: requires dest != null;
095: requires srcOff >= 0 ;
096: requires destOff >= 0 ;
097: requires length >=0;
098: requires (short)(srcOff + length) <= src.length;
099: requires (short)(destOff + length) <= dest.length;
100: ensures \result == 0 || \result == 1 || \result == -1;
101: assignable \nothing;
102: @*/
103: public static byte arrayCompare(byte[] src, short srcOff,
104: byte[] dest, short destOff, short length) {
105: if (src == null || dest == null)
106: throw new NullPointerException();
107: if (length < 0 || srcOff < 0 || destOff < 0
108: || (short) (srcOff + length) > src.length
109: || (short) (destOff + length) > dest.length)
110: throw new ArrayIndexOutOfBoundsException();
111: return KeYJCSystem.jvmArrayCompare(src, srcOff, dest, destOff,
112: length);
113: }
114:
115: // no spec
116: public static short makeShort(byte b1, byte b2) {
117: return KeYJCSystem.jvmMakeShort(b1, b2);
118: }
119:
120: // Could be specified, but KeY does not handle byte and short
121: // args. in query methods very well, see bug #638
122: //
123: // no spec
124: public static short getShort(byte[] bArray, short bOff) {
125: if (bArray == null)
126: throw new NullPointerException();
127: if (bOff < 0 || (short) (bOff + 1) >= bArray.length)
128: throw new ArrayIndexOutOfBoundsException();
129: return KeYJCSystem.jvmMakeShort(bArray[bOff], bArray[bOff + 1]);
130: }
131:
132: // no spec
133: public static short setShort(byte[] bArray, short bOff, short sValue)
134: throws TransactionException {
135: if (bArray == null)
136: throw new NullPointerException();
137: if (bOff < 0 || (short) (bOff + 1) >= bArray.length)
138: throw new ArrayIndexOutOfBoundsException();
139: final boolean doTransaction = JCSystem.isTransient(bArray) == JCSystem.NOT_A_TRANSIENT_OBJECT
140: && JCSystem.getTransactionDepth() == (byte) 0;
141: if (doTransaction)
142: KeYJCSystem.jvmBeginTransaction();
143: KeYJCSystem.jvmSetShort(bArray, bOff, sValue);
144: if (doTransaction)
145: KeYJCSystem.jvmCommitTransaction();
146: return (short) (bOff + 2);
147: }
148:
149: }
|