Detecting location mode read/write using the old method.
[jpf-core.git] / 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 com.sun.org.apache.xpath.internal.operations.Bool;
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.JPF;
23 import gov.nasa.jpf.ListenerAdapter;
24 import gov.nasa.jpf.search.Search;
25 import gov.nasa.jpf.jvm.bytecode.*;
26 import gov.nasa.jpf.vm.*;
27 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
28 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
29 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
30 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
31 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
32 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
33
34 import java.awt.*;
35 import java.io.PrintWriter;
36
37 import java.util.*;
38 import java.util.List;
39
40 // TODO: Fix for Groovy's model-checking
41 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
42 /**
43  * simple tool to log state changes
44  */
45 public class StateReducer extends ListenerAdapter {
46
47   // Debug info fields
48   private boolean debugMode;
49   private boolean stateReductionMode;
50   private final PrintWriter out;
51   volatile private String detail;
52   volatile private int depth;
53   volatile private int id;
54   Transition transition;
55
56   // State reduction fields
57   private int choiceCounter;
58   private Integer choiceUpperBound;
59   private boolean isInitialized;
60   private boolean isResetAfterAnalysis;
61   private boolean isBooleanCGFlipped;
62   private HashMap<IntChoiceFromSet,Integer> cgMap;
63   // Record the mapping between event number and field accesses (Read and Write)
64   private HashMap<Integer,ReadWriteSet> readWriteFieldsMap;
65   // The following is the backtrack map (set) that stores all the backtrack information
66   // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...}
67   private HashMap<Integer,LinkedList<Integer[]>> backtrackMap;
68   private HashMap<Integer,HashSet<Integer>> conflictPairMap;
69
70   public StateReducer (Config config, JPF jpf) {
71     debugMode = config.getBoolean("debug_state_transition", false);
72     stateReductionMode = config.getBoolean("activate_state_reduction", true);
73     if (debugMode) {
74       out = new PrintWriter(System.out, true);
75     } else {
76       out = null;
77     }
78     detail = null;
79     depth = 0;
80     id = 0;
81     transition = null;
82     isBooleanCGFlipped = false;
83     initializeStateReduction();
84   }
85
86   private void initializeStateReduction() {
87     if (stateReductionMode) {
88       choiceCounter = 0;
89       choiceUpperBound = 0;
90       isInitialized = false;
91       isResetAfterAnalysis = false;
92       cgMap = new HashMap<>();
93       readWriteFieldsMap = new HashMap<>();
94       backtrackMap = new HashMap<>();
95       conflictPairMap = new HashMap<>();
96     }
97   }
98
99   @Override
100   public void stateRestored(Search search) {
101     if (debugMode) {
102       id = search.getStateId();
103       depth = search.getDepth();
104       transition = search.getTransition();
105       detail = null;
106       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
107               " and depth: " + depth + "\n");
108     }
109   }
110
111   //--- the ones we are interested in
112   @Override
113   public void searchStarted(Search search) {
114     if (debugMode) {
115       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
116     }
117   }
118
119   @Override
120   public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
121     if (stateReductionMode) {
122       // Initialize with necessary information from the CG
123       if (nextCG instanceof IntChoiceFromSet) {
124         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
125         // Check if CG has been initialized, otherwise initialize it
126         Object[] choices = icsCG.getAllChoices();
127         if (!isInitialized) {
128           // Get the upper bound from the last element of the choices
129           choiceUpperBound = (Integer) choices[choices.length - 1];
130           isInitialized = true;
131         }
132         // Record the subsequent Integer CGs only until we hit the upper bound
133         if (choiceCounter < choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
134           // Update the choices of the first CG and add '-1'
135           Integer[] newChoices = new Integer[choices.length + 1];
136           System.arraycopy(choices, 0, newChoices, 0, choices.length);
137           newChoices[newChoices.length - 1] = -1;
138           icsCG.setNewValues(newChoices);
139           icsCG.reset();
140           // Advance the current Integer CG
141           // This way we explore all the event numbers in the first pass
142           icsCG.advance(choiceCounter);
143           cgMap.put(icsCG, choiceCounter);
144           choiceCounter++;
145         } else {
146           // Set done the subsequent CGs
147           // We only need n CGs (n is event numbers)
148           icsCG.setDone();
149         }
150       }
151     }
152   }
153
154   private void resetAllCGs() {
155     // Extract the event numbers that have backtrack lists
156     Set<Integer> eventSet = backtrackMap.keySet();
157     // Return if there is no conflict at all (highly unlikely)
158     if (eventSet.isEmpty()) {
159       return;
160     }
161     // Reset every CG with the first backtrack lists
162     for(IntChoiceFromSet cg : cgMap.keySet()) {
163       int event = cgMap.get(cg);
164       LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
165       if (choiceLists != null && choiceLists.peekFirst() != null) {
166         Integer[] choiceList = choiceLists.removeFirst();
167         // Deploy the new choice list for this CG
168         cg.setNewValues(choiceList);
169         cg.reset();
170       }
171     }
172   }
173
174   @Override
175   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
176                 
177     if(stateReductionMode) {
178       // Check the boolean CG and if it is flipped, we are resetting the analysis
179       if (currentCG instanceof BooleanChoiceGenerator) {
180         if (!isBooleanCGFlipped) {
181           isBooleanCGFlipped = true;
182         } else {
183           initializeStateReduction();
184         }
185       }
186       // Check every choice generated and make sure that all the available choices
187       // are chosen first before repeating the same choice of value twice!
188       if (currentCG instanceof IntChoiceFromSet) {
189         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
190         // Update and reset the CG if needed (do this for the first time after the analysis)
191         if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
192           resetAllCGs();
193           isResetAfterAnalysis = true;
194         }
195         // Do this for every CG after finishing each backtrack list
196         if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
197           int event = cgMap.get(icsCG);
198           LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
199           if (choiceLists.peekFirst() != null) {
200             Integer[] choiceList = choiceLists.removeFirst();
201             // Deploy the new choice list for this CG
202             icsCG.setNewValues(choiceList);
203             icsCG.reset();
204           } else {
205             // Set done if this was the last backtrack list
206             icsCG.setDone();
207           }
208         }
209       }
210     }
211   }
212
213   @Override
214   public void stateAdvanced(Search search) {
215     if (debugMode) {
216       id = search.getStateId();
217       depth = search.getDepth();
218       transition = search.getTransition();
219       if (search.isNewState()) {
220         detail = "new";
221       } else {
222         detail = "visited";
223       }
224
225       if (search.isEndState()) {
226         out.println("\n==> DEBUG: This is the last state!\n");
227         detail += " end";
228       }
229       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
230               " which is " + detail + " Transition: " + transition + "\n");
231     }
232   }
233
234   @Override
235   public void stateBacktracked(Search search) {
236     if (debugMode) {
237       id = search.getStateId();
238       depth = search.getDepth();
239       transition = search.getTransition();
240       detail = null;
241
242       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
243               " and depth: " + depth + "\n");
244     }
245   }
246
247   @Override
248   public void searchFinished(Search search) {
249     if (debugMode) {
250       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
251     }
252   }
253
254   // This class compactly stores Read and Write field sets
255   private class ReadWriteSet {
256     private HashSet<String> readSet;
257     private HashSet<String> writeSet;
258
259     public ReadWriteSet() {
260       readSet = new HashSet<>();
261       writeSet = new HashSet<>();
262     }
263
264     public void addReadField(String field) {
265       readSet.add(field);
266     }
267
268     public void addWriteField(String field) {
269       writeSet.add(field);
270     }
271
272     public boolean readFieldExists(String field) {
273       return readSet.contains(field);
274     }
275
276     public boolean writeFieldExists(String field) {
277       return writeSet.contains(field);
278     }
279   }
280
281   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass) {
282     // Do the analysis to get Read and Write accesses to fields
283     ReadWriteSet rwSet;
284     // We already have an entry
285     if (readWriteFieldsMap.containsKey(choiceCounter)) {
286       rwSet = readWriteFieldsMap.get(choiceCounter);
287     } else { // We need to create a new entry
288       rwSet = new ReadWriteSet();
289       readWriteFieldsMap.put(choiceCounter, rwSet);
290     }
291     // Record the field in the map
292     if (executedInsn instanceof WriteInstruction) {
293       rwSet.addWriteField(fieldClass);
294     }
295     if (executedInsn instanceof ReadInstruction) {
296       rwSet.addReadField(fieldClass);
297     }
298   }
299
300   private boolean recordConflictPair(int currentEvent, int eventNumber) {
301     HashSet<Integer> conflictSet;
302     if (!conflictPairMap.containsKey(currentEvent)) {
303       conflictSet = new HashSet<>();
304       conflictPairMap.put(currentEvent, conflictSet);
305     } else {
306       conflictSet = conflictPairMap.get(currentEvent);
307     }
308     // If this conflict has been recorded before, we return false because
309     // we don't want to service this backtrack point twice
310     if (conflictSet.contains(eventNumber)) {
311       return false;
312     }
313     // If it hasn't been recorded, then do otherwise
314     conflictSet.add(eventNumber);
315     return true;
316   }
317
318   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
319
320     int minChoice = Math.min(currentChoice, conflictEventNumber);
321     int maxChoice = Math.max(currentChoice, conflictEventNumber);
322     LinkedList<Integer[]> backtrackChoiceLists;
323     // Check if we have a list for this choice number
324     // If not we create a new one for it
325     if (!backtrackMap.containsKey(minChoice)) {
326       backtrackChoiceLists = new LinkedList<>();
327       backtrackMap.put(minChoice, backtrackChoiceLists);
328     } else {
329       backtrackChoiceLists = backtrackMap.get(minChoice);
330     }
331     // TODO: The following might change depending on the POR implementation detail
332     // Create a new list of choices for backtrack based on the current choice and conflicting event number
333     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
334     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
335     // (originally of length 6) since we don't start from event number 0
336     int maxListLength = choiceUpperBound + 1;
337     int listLength = maxListLength - minChoice;
338     Integer[] choiceList = new Integer[listLength+1];
339     // Put the conflicting event numbers first and reverse the order
340     choiceList[0] = maxChoice;
341     choiceList[1] = minChoice;
342     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
343     for(int i = minChoice + 1, j = 2; j < listLength; i++) {
344       if (i != maxChoice) {
345         choiceList[j] = i;
346         j++;
347       }
348     }
349     // Set the last element to '-1' as the end of the sequence
350     choiceList[choiceList.length - 1] = -1;
351     backtrackChoiceLists.addLast(choiceList);
352   }
353
354   @Override
355   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
356     if (stateReductionMode) {
357       // Record accesses from executed instructions
358       if (executedInsn instanceof JVMFieldInstruction) {
359         String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
360         // We don't care about libraries
361         if (!fieldClass.startsWith("java") &&
362             !fieldClass.startsWith("org") &&
363             !fieldClass.startsWith("sun") &&
364             !fieldClass.startsWith("com") &&
365             !fieldClass.startsWith("gov") &&
366             !fieldClass.startsWith("groovy")) {
367           analyzeReadWriteAccesses(executedInsn, fieldClass);
368         }
369       }
370       // Analyze conflicts from next instructions
371       if (nextInsn instanceof JVMFieldInstruction) {
372         String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
373         // We don't care about libraries
374         if (!fieldClass.startsWith("java") &&
375             !fieldClass.startsWith("org") &&
376             !fieldClass.startsWith("sun") &&
377             !fieldClass.startsWith("com") &&
378             !fieldClass.startsWith("gov") &&
379             !fieldClass.startsWith("groovy")) {
380           // Check for conflict (go backward from currentChoice and get the first conflict)
381           // If the current event has conflicts with multiple events, then these will be detected
382           // one by one as this recursively checks backward when backtrack set is revisited and executed.
383           for(int eventNumber=choiceCounter-1; eventNumber>=0; eventNumber--) {
384             // Skip if this event number does not have any Read/Write set
385             if (!readWriteFieldsMap.containsKey(eventNumber)) {
386               continue;
387             }
388             ReadWriteSet rwSet = readWriteFieldsMap.get(eventNumber);
389             // 1) Check for conflicts with Write fields for both Read and Write instructions
390             // 2) Check for conflicts with Read fields for Write instructions
391             if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
392                   rwSet.writeFieldExists(fieldClass)) ||
393                  (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass)))   {
394               // We do not record and service the same backtrack pair/point twice!
395               // If it has been serviced before, we just skip this
396               if (recordConflictPair(choiceCounter, eventNumber)) {
397                 createBacktrackChoiceList(choiceCounter, eventNumber);
398                 // Break if a conflict is found!
399                 break;
400               }
401             }
402           }
403         }
404       }
405     }
406   }
407 }