From 564ad9103d56228149eaeea0b978de4f7bd73c59 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 25 Sep 2019 10:58:25 -0700 Subject: [PATCH] First version of the StateReducer class. --- .../gov/nasa/jpf/listener/StateReducer.java | 177 ++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 src/main/gov/nasa/jpf/listener/StateReducer.java diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java new file mode 100644 index 0000000..5dbe79d --- /dev/null +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -0,0 +1,177 @@ +/* + * 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.listener; + +import gov.nasa.jpf.Config; +import gov.nasa.jpf.JPF; +import gov.nasa.jpf.ListenerAdapter; +import gov.nasa.jpf.search.Search; +import gov.nasa.jpf.jvm.bytecode.*; +import gov.nasa.jpf.vm.*; +import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction; +import gov.nasa.jpf.vm.bytecode.ReadInstruction; +import gov.nasa.jpf.vm.bytecode.StoreInstruction; +import gov.nasa.jpf.vm.bytecode.WriteInstruction; +import gov.nasa.jpf.vm.choice.IntIntervalGenerator; + +import java.io.PrintWriter; + +import java.util.*; + +/** + * simple tool to log state changes + */ +public class StateReducer extends ListenerAdapter { + + private final PrintWriter out; + volatile private String valueVarLock = ""; + volatile private String valueVarContact = ""; + volatile private String operation; + volatile private String detail; + volatile private int depth; + volatile private int id; + Transition transition; + Object annotation; + String label; + String output; + int stateId; + + + public StateReducer (Config conf, JPF jpf) { + out = new PrintWriter(System.out, true); + } + + @Override + public void stateRestored(Search search) { + id = search.getStateId(); + depth = search.getDepth(); + operation = "restored"; + transition = search.getTransition(); + if (transition != null) { + annotation = transition.getAnnotation(); + label = transition.getLabel(); + output = transition.getOutput(); + stateId = transition.getStateId(); + } + detail = null; + + out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n"); + } + + //--- the ones we are interested in + @Override + public void searchStarted(Search search) { + out.println("----------------------------------- search started"); + } + + // Holds values that have appeared during CG advances + private HashSet cgChoiceSet = new HashSet<>(); + private Integer choiceUpperBound = 0; + private boolean isInitialized = false; + + @Override + public void choiceGeneratorSet (VM vm, ChoiceGenerator newCG) { + + // Initialize with necessary information from the CG + if (newCG instanceof IntIntervalGenerator) { + IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG; + // Check if CG has been initialized, otherwise initialize it + if (!isInitialized) { + Integer[] choices = iigCG.getChoices(); + // Get the upper bound from the last element of the choices + choiceUpperBound = choices[choices.length - 1]; + isInitialized = true; + } else { + newCG.setDone(); + } + } + } + + @Override + public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator currentCG) { + // Check every choice generated and make sure that all the available choices + // are chosen first before repeating the same choice of value twice! + if (currentCG instanceof IntIntervalGenerator) { + IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG; + Integer nextChoice = iigCG.getNextChoice(); + if (!cgChoiceSet.contains(nextChoice)) { + cgChoiceSet.add(nextChoice); + } + // Allow reinitialization after an upper bound is hit + // This means all available choices have been explored once during this iteration + if (cgChoiceSet.contains(choiceUpperBound)) { + isInitialized = false; + cgChoiceSet.clear(); + } + } + } + + @Override + public void stateAdvanced(Search search) { + String theEnd = null; + id = search.getStateId(); + depth = search.getDepth(); + operation = "forward"; + transition = search.getTransition(); + if (transition != null) { + annotation = transition.getAnnotation(); + label = transition.getLabel(); + output = transition.getOutput(); + stateId = transition.getStateId(); + } + if (search.isNewState()) { + detail = "new"; + } else { + detail = "visited"; + } + + if (search.isEndState()) { + out.println("This is the last state!"); + theEnd = "end"; + } + + //out.println("stateId: "+stateId+", output: "+output+", label: "+label); + 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"); + + if (search.isEndState()) { + detail += " end"; + } + } + + @Override + public void stateBacktracked(Search search) { + id = search.getStateId(); + depth = search.getDepth(); + operation = "backtrack"; + transition = search.getTransition(); + if (transition != null) { + annotation = transition.getAnnotation(); + label = transition.getLabel(); + output = transition.getOutput(); + stateId = transition.getStateId(); + } + detail = null; + + out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n"); + } + + @Override + public void searchFinished(Search search) { + out.println("----------------------------------- search finished"); + } +} \ No newline at end of file -- 2.34.1