2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.listener;
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;
32 import java.io.PrintWriter;
36 // TODO: Fix for Groovy's model-checking
37 // TODO: This is a listener created to detect device conflicts and global variable conflicts
39 * Simple listener tool to track remove unwanted ChoiceGenerators that are registered
40 * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same
41 * type could be registered spuriously during a while(true) loop.
43 public class StateReducer extends ListenerAdapter {
45 private boolean debugMode;
46 private boolean stateReductionMode;
47 private final PrintWriter out;
48 private String detail;
51 private Transition transition;
52 private HashSet<String> conflictSet;
53 private HashSet<String> appSet;
54 // Holds the event value numbers that execute write instructions
55 private HashSet<Integer> writeEventNumberSet;
56 // Holds values that have appeared during CG advances
57 private HashSet<Integer> cgChoiceSet;
58 private Integer choiceUpperBound;
59 private boolean isInitialized;
60 private int currentChoice;
61 // Records how many times BooleanChoiceGenerator has been advanced
62 private int bCGIsAdvanced;
63 // Records how many times we have looped through all the event numbers (IntIntervalGenerator)
64 private int iiCGIsLooped;
66 // Constants to determine when to start reducing states
67 private final int BOOLEAN_CG_ADVANCED_THRESHOLD = 2;
68 private final int INTEGER_CG_ADVANCED_THRESHOLD = 50;
70 public StateReducer (Config config) {
71 debugMode = config.getBoolean("debug_state_transition", false);
72 stateReductionMode = config.getBoolean("activate_state_reduction", true);
74 out = new PrintWriter(System.out, true);
82 cgChoiceSet = new HashSet<>();
84 isInitialized = false;
85 conflictSet = new HashSet<>();
86 String[] conflictVars = config.getStringArray("variables");
87 // We are not tracking anything if it is null
88 if (conflictVars != null) {
89 for (String var : conflictVars) {
93 appSet = new HashSet<>();
94 String[] apps = config.getStringArray("apps");
95 // We are not tracking anything if it is null
97 for (String var : apps) {
102 writeEventNumberSet = new HashSet<>();
108 public void stateRestored(Search search) {
110 id = search.getStateId();
111 depth = search.getDepth();
112 transition = search.getTransition();
114 out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
115 " and depth: " + depth + "\n");
119 //--- the ones we are interested in
121 public void searchStarted(Search search) {
123 out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
128 public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
129 if (stateReductionMode) {
130 // Initialize with necessary information from the CG
131 if (newCG instanceof IntIntervalGenerator) {
132 IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
133 // Check if CG has been initialized, otherwise initialize it
134 if (!isInitialized) {
135 Integer[] choices = iigCG.getChoices();
136 // Get the upper bound from the last element of the choices
137 choiceUpperBound = choices[choices.length - 1];
138 isInitialized = true;
147 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
148 if (stateReductionMode) {
149 // Check for BooleanChoiceGenerator
150 if (currentCG instanceof BooleanChoiceGenerator) {
153 // Check every choice generated and make sure that all the available choices
154 // are chosen first before repeating the same choice of value twice!
155 if (currentCG instanceof IntIntervalGenerator) {
156 IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
157 Integer nextChoice = iigCG.getNextChoice();
158 if (!cgChoiceSet.contains(nextChoice)) {
159 cgChoiceSet.add(nextChoice);
161 // Allow reinitialization after an upper bound is hit
162 // This means all available choices have been explored once during this iteration
163 if (cgChoiceSet.contains(choiceUpperBound)) {
164 isInitialized = false;
168 // Record the current choice
169 currentChoice = iigCG.getNextChoice();
170 // Start reducing (advancing) if the thresholds are passed
171 if (iiCGIsLooped >= INTEGER_CG_ADVANCED_THRESHOLD &&
172 bCGIsAdvanced >= BOOLEAN_CG_ADVANCED_THRESHOLD) {
173 if (!writeEventNumberSet.contains(currentChoice)) {
182 public void stateAdvanced(Search search) {
184 id = search.getStateId();
185 depth = search.getDepth();
186 transition = search.getTransition();
187 if (search.isNewState()) {
193 if (search.isEndState()) {
194 out.println("\n==> DEBUG: This is the last state!\n");
197 out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
198 " which is " + detail + " Transition: " + transition + "\n");
203 public void stateBacktracked(Search search) {
205 id = search.getStateId();
206 depth = search.getDepth();
207 transition = search.getTransition();
210 out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
211 " and depth: " + depth + "\n");
216 public void searchFinished(Search search) {
218 out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
223 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
224 // CASE #1: Detecting variable write-after-write conflict
225 if (executedInsn instanceof WriteInstruction) {
226 // Check for write-after-write conflict
227 String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
228 for(String var : conflictSet) {
229 if (varId.contains(var)) {
230 String writer = getWriter(ti.getStack());
231 // Just return if the writer is not one of the listed apps in the .jpf file
235 // Stores event number that executes WriteInstruction
236 if (!writeEventNumberSet.contains(currentChoice)) {
237 writeEventNumberSet.add(currentChoice);
244 // Find the variable writer
245 // It should be one of the apps listed in the .jpf file
246 private String getWriter(List<StackFrame> sfList) {
247 // Start looking from the top of the stack backward
248 for(int i=sfList.size()-1; i>=0; i--) {
249 MethodInfo mi = sfList.get(i).getMethodInfo();
250 if(!mi.isJPFInternal()) {
251 String method = mi.getStackTraceName();
252 // Check against the apps in the appSet
253 for(String app : appSet) {
254 // There is only one writer at a time but we need to always
255 // check all the potential writers in the list
256 if (method.contains(app)) {