01: //
02: // Copyright (C) 2005 United States Government as represented by the
03: // Administrator of the National Aeronautics and Space Administration
04: // (NASA). All Rights Reserved.
05: //
06: // This software is distributed under the NASA Open Source Agreement
07: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
08: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: // directory tree for the complete NOSA document.
10: //
11: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18: //
19: package gov.nasa.jpf.jvm;
20:
21: import gov.nasa.jpf.util.Md5Set;
22: import com.twmacinta.util.MD5;
23:
24: /**
25: * class that implements StateSets based on MD5 hashes
26: * (this is the interface to the MD5 library)
27: */
28: public class Md5StateSet implements StateSet {
29:
30: MD5 md5 = new MD5();
31: Md5Set set = new Md5Set();
32:
33: byte[] buf = new byte[4]; // just for Update call optimizations
34:
35: int lastStateId;
36: boolean isNewState;
37:
38: public boolean isNewState(int stateId) {
39: if (lastStateId == stateId) {
40: return isNewState;
41: } else {
42: return false; // otherwise we've had a subsequent forward() or backtrack
43: }
44: }
45:
46: public int size() {
47: return set.size();
48: }
49:
50: /**
51: * that's called by the VM, i.e. just once, and answers the corresponding id
52: * (so that we subsequently can refer to this id to get additional info)
53: */
54: public int add(SystemState ss) {
55: int[] sd = ss.getStoringData();
56:
57: md5.Init();
58: for (int i = 0; i < sd.length; i++) {
59: int n = sd[i];
60:
61: // this is optimized for the current implementation of MD5
62: // since MD5.Update() calls are a hotspot, and Update(byte) happens
63: // to convert back into a dynamically allocated byte[], then indirectly
64: // calling the Update(byte[],int,int). We can save the number of
65: // Update invokes, dyn arrays and call indirections
66: buf[0] = (byte) n;
67: buf[1] = (byte) (n >> 8);
68: buf[2] = (byte) (n >> 16);
69: buf[3] = (byte) (n >> 24);
70: md5.Update(buf, 0, 4);
71: // end optimization
72: }
73: byte[] hash = md5.Final();
74:
75: isNewState = set.add(hash);
76: lastStateId = set.getId(hash);
77:
78: return lastStateId;
79: }
80:
81: }
|