src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18
  19 package gov.nasa.jpf.vm.serialize;
  20
  21 import java.util.Iterator;
  22
  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;
  33
  34 /**
  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.
  38  *
  39  * Use this serializer if the Heap implementation does not provide
  40  * sufficient symmetry, i.e. reference values depend on the order of
  41  * thread scheduling.
  42  *
  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.
  51  */
  52 public class CFSerializer extends FilteringSerializer {
  53
  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   long initsidCount=0;
  59   long sidCount=1;
  60
  61   @Override
  62   protected void initReferenceQueue() {
  63     super.initReferenceQueue();
  64
  65     initsidCount = sidCount - 1;
  66   }
  67
  68   // might be overriden in subclasses to conditionally queue objects
  69   protected void queueReference(ElementInfo ei){
  70     refQueue.add(ei);
  71   }
  72
  73   @Override
  74   public void processReference(int objref) {
  75     if (objref == MJIEnv.NULL) {
  76       buf.add(MJIEnv.NULL);
  77     } else {
  78       ElementInfo ei = heap.get(objref);
  79       ClassInfo ci = ei.getClassInfo();
  80
  81       if (SmartThingsConfig.instance.ignoreClass(ci)) {
  82         ei.setSid(initsidCount);
  83         buf.add(0);
  84         return;
  85       }
  86       long sid = ei.getSid();
  87
  88       if (sid <= initsidCount){ // count sid upwards from 1
  89           sid = sidCount++;
  90           ei.setSid(sid);
  91           queueReference(ei);
  92       }
  93
  94       // note that we always add the absolute sid value
  95       buf.add((int)(sid - initsidCount));
  96     }
  97   }
  98
  99
 100   @Override
 101   protected void serializeStackFrames() {
 102     ThreadList tl = ks.getThreadList();
 103     for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
 104       serializeStackFrames(it.next());
 105     }
 106   }
 107
 108   //Don't think we actually have static fields...so this should be safe
 109   @Override
 110   protected void serializeClassLoaders(){
 111   }
 112
 113   protected void serializeClass (StaticElementInfo sei){
 114     // buf.add(sei.getStatus());
 115
 116     Fields fields = sei.getFields();
 117     ClassInfo ci = sei.getClassInfo();
 118     FinalBitSet filtered = getStaticFilterMask(ci);
 119     FinalBitSet refs = getStaticRefMask(ci);
 120     int max = ci.getStaticDataSize();
 121     if (SmartThingsConfig.instance.staticClass(ci))
 122       return;
 123     for (int i = 0; i < max; i++) {
 124       if (!filtered.get(i)) {
 125         int v = fields.getIntValue(i);
 126         if (refs.get(i)) {
 127           processReference(v);
 128         } else {
 129           buf.add(v);
 130         }
 131       }
 132     }
 133   }
 134
 135
 136   @Override
 137   protected void serializeFrame(StackFrame frame){
 138     FramePolicy fp = getFramePolicy(frame.getMethodInfo());
 139     Instruction pc = frame.getPC();
 140     int len = frame.getTopPos()+1;
 141
 142     if (fp == null || fp.includePC) {
 143       buf.add(frame.getMethodInfo().getGlobalId());
 144       buf.add( pc != null ? pc.getInstructionIndex() : -1);
 145     }
 146
 147     if (fp == null || fp.includeLocals) {
 148       buf.add(len);
 149
 150       // unfortunately we can't do this as a block operation because that
 151       // would use concrete reference values as hash data, i.e. break heap symmetry
 152       int thisslot = frame.getThis();
 153       processReference(thisslot);
 154       /*
 155       int[] slots = frame.getSlots();
 156       for (int i = 0; i < len; i++) {
 157         if (frame.isReferenceSlot(i)) {
 158           processReference(slots[i]);
 159         } else {
 160           buf.add(slots[i]);
 161         }
 162       }
 163       */
 164     }
 165   }
 166
 167   @Override
 168   protected void processReferenceQueue() {
 169     refQueue.process(this);
 170   }
 171
 172   @Override
 173   protected int getSerializedReferenceValue (ElementInfo ei){
 174     return (int)(ei.getSid()-initsidCount);
 175   }
 176 }