src/main/gov/nasa/jpf/listener/StateReducer.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 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.ListenerAdapter;
  23 import gov.nasa.jpf.search.Search;
  24 import gov.nasa.jpf.jvm.bytecode.*;
  25 import gov.nasa.jpf.vm.*;
  26 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
  27 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  28 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
  29 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  30 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  31
  32 import java.io.PrintWriter;
  33
  34 import java.util.*;
  35
  36 /**
  37  * simple tool to log state changes
  38  */
  39 public class StateReducer extends ListenerAdapter {
  40
  41   private final PrintWriter out;
  42   volatile private String valueVarLock = "";
  43   volatile private String valueVarContact = "";
  44   volatile private String operation;
  45   volatile private String detail;
  46   volatile private int depth;
  47   volatile private int id;
  48   Transition transition;
  49   Object annotation;
  50   String label;
  51   String output;
  52   int stateId;
  53
  54
  55   public StateReducer (Config conf, JPF jpf) {
  56     out = new PrintWriter(System.out, true);
  57   }
  58
  59   @Override
  60   public void stateRestored(Search search) {
  61     id = search.getStateId();
  62     depth = search.getDepth();
  63     operation = "restored";
  64     transition = search.getTransition();
  65     if (transition != null) {
  66       annotation = transition.getAnnotation();
  67       label = transition.getLabel();
  68       output = transition.getOutput();
  69       stateId = transition.getStateId();
  70     }
  71     detail = null;
  72
  73     out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
  74   }
  75
  76   //--- the ones we are interested in
  77   @Override
  78   public void searchStarted(Search search) {
  79     out.println("----------------------------------- search started");
  80   }
  81
  82   // Holds values that have appeared during CG advances
  83   private HashSet<Integer> cgChoiceSet = new HashSet<>();
  84   private Integer choiceUpperBound = 0;
  85   private boolean isInitialized = false;
  86
  87   @Override
  88   public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
  89
  90     // Initialize with necessary information from the CG
  91     if (newCG instanceof IntIntervalGenerator) {
  92       IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
  93       // Check if CG has been initialized, otherwise initialize it
  94       if (!isInitialized) {
  95         Integer[] choices = iigCG.getChoices();
  96         // Get the upper bound from the last element of the choices
  97         choiceUpperBound = choices[choices.length - 1];
  98         isInitialized = true;
  99       } else {
 100         newCG.setDone();
 101       }
 102     }
 103   }
 104
 105   @Override
 106   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
 107     // Check every choice generated and make sure that all the available choices
 108     // are chosen first before repeating the same choice of value twice!
 109     if (currentCG instanceof IntIntervalGenerator) {
 110       IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
 111       Integer nextChoice = iigCG.getNextChoice();
 112       if (!cgChoiceSet.contains(nextChoice)) {
 113         cgChoiceSet.add(nextChoice);
 114       }
 115       // Allow reinitialization after an upper bound is hit
 116       // This means all available choices have been explored once during this iteration
 117       if (cgChoiceSet.contains(choiceUpperBound)) {
 118         isInitialized = false;
 119         cgChoiceSet.clear();
 120       }
 121     }
 122   }
 123
 124   @Override
 125   public void stateAdvanced(Search search) {
 126     String theEnd = null;
 127     id = search.getStateId();
 128     depth = search.getDepth();
 129     operation = "forward";
 130     transition = search.getTransition();
 131     if (transition != null) {
 132       annotation = transition.getAnnotation();
 133       label = transition.getLabel();
 134       output = transition.getOutput();
 135       stateId = transition.getStateId();
 136     }
 137     if (search.isNewState()) {
 138       detail = "new";
 139     } else {
 140       detail = "visited";
 141     }
 142
 143     if (search.isEndState()) {
 144       out.println("This is the last state!");
 145       theEnd = "end";
 146     }
 147
 148     //out.println("stateId: "+stateId+", output: "+output+", label: "+label);
 149     out.println("\nThe state is forwarded to state with id: "+id+", with depth: "+depth+" which is "+detail+" Transition: "+transition+" state: "+"% "+theEnd+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
 150
 151     if (search.isEndState()) {
 152       detail += " end";
 153     }
 154   }
 155
 156   @Override
 157   public void stateBacktracked(Search search) {
 158     id = search.getStateId();
 159     depth = search.getDepth();
 160     operation = "backtrack";
 161     transition = search.getTransition();
 162     if (transition != null) {
 163       annotation = transition.getAnnotation();
 164       label = transition.getLabel();
 165       output = transition.getOutput();
 166       stateId = transition.getStateId();
 167     }
 168     detail = null;
 169
 170     out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
 171   }
 172
 173   @Override
 174   public void searchFinished(Search search) {
 175     out.println("----------------------------------- search finished");
 176   }
 177 }