view src/main/gov/nasa/jpf/vm/serialize/AdaptiveSerializer.java @ 3:fdc263e5806b

added inverse matching in StringSetMatcher. Since this is not easy to do in regexes, it's at the next hight level in StringSetMatcher added a optional CG accessor interface (geChoice(i), getAllChoices(), getProcessedChoices() getUnprocessedChoices()) that can be used from listeners and peers to enumerate/analyse choice sets. Note that not all CGs have to support this as there is no requirement that CGs actually use pre-computed choice sets. The low level accessor is getChoice(i), ChoiceGeneratorBase provides generic (not very efficient) set accessor implementations. Note that ChoiceGeneratorBase.getChoice() has to be overridden in subclasses in order to support choice enumeration, the default impl is just there so that we don't break subclass compilation
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Tue, 03 Feb 2015 08:49:33 -0800
parents 61d41facf527
children
line wrap: on
line source

/*
 * Copyright (C) 2014, United States Government, as represented by the
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * The Java Pathfinder core (jpf-core) platform is licensed under the
 * Apache License, Version 2.0 (the "License"); you may not use this file except
 * in compliance with the License. You may obtain a copy of the License at
 * 
 *        http://www.apache.org/licenses/LICENSE-2.0. 
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and 
 * limitations under the License.
 */

package gov.nasa.jpf.vm.serialize;

import gov.nasa.jpf.vm.ChoiceGenerator;
import gov.nasa.jpf.vm.ElementInfo;

/**
 * a CG type adaptive, canonicalizing & filtering serializer that is an
 * under-approximation mostly aimed at finding data races and deadlocks in programs
 * with a large number of scheduling points (= thread choices)
 *
 * This came to bear by accidentally discovering that JPF often seems to finds
 * concurrency defects by just serializing the thread states, their topmost stack
 * frames and the objects directly referenced from there.
 * For non-scheduling points, we just fall back to serializing statics, all thread
 * stacks and all the data reachable from there
 */
public class AdaptiveSerializer extends CFSerializer {

  boolean traverseObjects;
  boolean isSchedulingPoint;

  @Override
  protected void initReferenceQueue() {
    super.initReferenceQueue();
    traverseObjects = true;

    ChoiceGenerator<?> nextCg = vm.getNextChoiceGenerator();
    isSchedulingPoint = (nextCg != null) && nextCg.isSchedulingPoint();
  }

  @Override
  protected void queueReference(ElementInfo ei){
    if (traverseObjects){
      refQueue.add(ei);
    }
  }

  @Override
  protected void processReferenceQueue() {
    if (isSchedulingPoint){
      traverseObjects = false;
    }
    refQueue.process(this);
  }

  //@Override
  @Override
  protected void serializeClassLoaders(){
    // for thread CGs we skip this - assuming that this is only relevant if there is
    // a class object lock, which is covered by the thread lock info
    if (!isSchedulingPoint){
      // <2do> this seems too conservative - we should only serialize what is
      // used from this thread, which can be collected at class load time
      // by looking at GET/PUTSTATIC targets (and their superclasses)
      super.serializeClassLoaders();
    }
  }
}