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   // 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
  60   long initsidCount=0;
  61   long sidCount=1;
  62
  63   @Override
  64   protected void initReferenceQueue() {
  65     super.initReferenceQueue();
  66
  67     initsidCount = sidCount - 1;
  68   }
  69
  70   // might be overriden in subclasses to conditionally queue objects
  71   protected void queueReference(ElementInfo ei){
  72     refQueue.add(ei);
  73   }
  74
  75   @Override
  76   public void processReference(int objref) {
  77     if (objref == MJIEnv.NULL) {
  78       buf.add(MJIEnv.NULL);
  79     } else {
  80       ElementInfo ei = heap.get(objref);
  81       ClassInfo ci = ei.getClassInfo();
  82
  83       if (SmartThingsConfig.instance.ignoreClass(ci)) {
  84         ei.setSid(initsidCount);
  85         buf.add(0);
  86         return;
  87       }
  88       long sid = ei.getSid();
  89
  90       if (sid <= initsidCount){ // count sid upwards from 1
  91           sid = sidCount++;
  92           ei.setSid(sid);
  93           queueReference(ei);
  94       }
  95
  96       // note that we always add the absolute sid value
  97       buf.add((int)(sid - initsidCount));
  98     }
  99   }
 100
 101
 102   @Override
 103   protected void serializeStackFrames() {
 104     ThreadList tl = ks.getThreadList();
 105     for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
 106       serializeStackFrames(it.next());
 107     }
 108   }
 109
 110   //Don't think we actually have static fields...so this should be safe
 111   @Override
 112   protected void serializeClassLoaders(){
 113   }
 114
 115   protected void serializeClass (StaticElementInfo sei){
 116     // buf.add(sei.getStatus());
 117
 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))
 124       return;
 125     for (int i = 0; i < max; i++) {
 126       if (!filtered.get(i)) {
 127         int v = fields.getIntValue(i);
 128         if (refs.get(i)) {
 129           processReference(v);
 130         } else {
 131           buf.add(v);
 132         }
 133       }
 134     }
 135   }
 136
 137
 138   @Override
 139   protected void serializeFrame(StackFrame frame){
 140     FramePolicy fp = getFramePolicy(frame.getMethodInfo());
 141     Instruction pc = frame.getPC();
 142     int len = frame.getTopPos()+1;
 143
 144     if (fp == null || fp.includePC) {
 145       buf.add(frame.getMethodInfo().getGlobalId());
 146       buf.add( pc != null ? pc.getInstructionIndex() : -1);
 147     }
 148
 149     if (fp == null || fp.includeLocals) {
 150       buf.add(len);
 151
 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);
 156       /*
 157       int[] slots = frame.getSlots();
 158       for (int i = 0; i < len; i++) {
 159         if (frame.isReferenceSlot(i)) {
 160           processReference(slots[i]);
 161         } else {
 162           buf.add(slots[i]);
 163         }
 164       }
 165       */
 166     }
 167   }
 168
 169   @Override
 170   protected void processReferenceQueue() {
 171     refQueue.process(this);
 172   }
 173
 174   @Override
 175   protected int getSerializedReferenceValue (ElementInfo ei){
 176     return (int)(ei.getSid()-initsidCount);
 177   }
 178 }