KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > jvm > Md5StateSet


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // 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 }
82
83
Popular Tags