2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
19 package gov.nasa.jpf.vm.serialize;
21 import java.util.Iterator;
23 import gov.nasa.jpf.vm.ElementInfo;
24 import gov.nasa.jpf.vm.StaticElementInfo;
25 import gov.nasa.jpf.vm.Fields;
26 import gov.nasa.jpf.util.FinalBitSet;
27 import gov.nasa.jpf.vm.ClassInfo;
28 import gov.nasa.jpf.vm.Instruction;
29 import gov.nasa.jpf.vm.MJIEnv;
30 import gov.nasa.jpf.vm.StackFrame;
31 import gov.nasa.jpf.vm.ThreadInfo;
32 import gov.nasa.jpf.vm.ThreadList;
35 * a FilteringSerializer that performs on-the-fly heap canonicalization to
36 * achieve heap symmetry. It does so by storing the order in which
37 * objects are referenced, not the reference values themselves.
39 * Use this serializer if the Heap implementation does not provide
40 * sufficient symmetry, i.e. reference values depend on the order of
43 * Ad hoc heap symmetry is hard to achieve in the heap because of static initialization.
44 * Each time a thread loads a class all the static init (at least the class object and
45 * its fields) are associated with this thread, hence thread reference
46 * values depend on which classes are already loaded by other threads. Associating
47 * all allocations from inside of clinits to one address range doesn't help either
48 * because then this range will experience scheduling dependent orders. A hybrid
49 * approach in which only this segment is canonicalized might work, but it is
50 * questionable if the overhead is worth the effort.
52 public class CFSerializer extends FilteringSerializer {
54 // we flip this on every serialization, which helps us to avoid passes
55 // over the serialized objects to reset their sids. This works by resetting
56 // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
57 // from -1, but store the absolute value in the serialization stream
58 // TODO: Fix for Groovy's model-checking
59 // TODO: Change of sid assignment strategy since the previous one caused a bug with SmartThings object filtering
64 protected void initReferenceQueue() {
65 super.initReferenceQueue();
67 initsidCount = sidCount - 1;
70 // might be overriden in subclasses to conditionally queue objects
71 protected void queueReference(ElementInfo ei){
76 public void processReference(int objref) {
77 if (objref == MJIEnv.NULL) {
80 ElementInfo ei = heap.get(objref);
81 ClassInfo ci = ei.getClassInfo();
83 if (SmartThingsConfig.instance.ignoreClass(ci)) {
84 ei.setSid(initsidCount);
88 long sid = ei.getSid();
90 if (sid <= initsidCount){ // count sid upwards from 1
96 // note that we always add the absolute sid value
97 buf.add((int)(sid - initsidCount));
103 protected void serializeStackFrames() {
104 ThreadList tl = ks.getThreadList();
105 for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
106 serializeStackFrames(it.next());
110 //Don't think we actually have static fields...so this should be safe
112 protected void serializeClassLoaders(){
115 protected void serializeClass (StaticElementInfo sei){
116 // buf.add(sei.getStatus());
118 Fields fields = sei.getFields();
119 ClassInfo ci = sei.getClassInfo();
120 FinalBitSet filtered = getStaticFilterMask(ci);
121 FinalBitSet refs = getStaticRefMask(ci);
122 int max = ci.getStaticDataSize();
123 if (SmartThingsConfig.instance.staticClass(ci))
125 for (int i = 0; i < max; i++) {
126 if (!filtered.get(i)) {
127 int v = fields.getIntValue(i);
139 protected void serializeFrame(StackFrame frame){
140 FramePolicy fp = getFramePolicy(frame.getMethodInfo());
141 Instruction pc = frame.getPC();
142 int len = frame.getTopPos()+1;
144 if (fp == null || fp.includePC) {
145 buf.add(frame.getMethodInfo().getGlobalId());
146 buf.add( pc != null ? pc.getInstructionIndex() : -1);
149 if (fp == null || fp.includeLocals) {
152 // unfortunately we can't do this as a block operation because that
153 // would use concrete reference values as hash data, i.e. break heap symmetry
154 int thisslot = frame.getThis();
155 processReference(thisslot);
157 int[] slots = frame.getSlots();
158 for (int i = 0; i < len; i++) {
159 if (frame.isReferenceSlot(i)) {
160 processReference(slots[i]);
170 protected void processReferenceQueue() {
171 refQueue.process(this);
175 protected int getSerializedReferenceValue (ElementInfo ei){
176 return (int)(ei.getSid()-initsidCount);