From: rtrimana <rtrimana@uci.edu>
Date: Wed, 6 Nov 2019 19:41:20 +0000 (-0800)
Subject: Fixing a bug: wrong CGs were reset when recursing into a sub-graph.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=5eea2985e05aeba96e036ba96f1a8e7beb9bc99a

Fixing a bug: wrong CGs were reset when recursing into a sub-graph.
---

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 957940f..08b27b1 100644
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -23,18 +23,13 @@ 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.IntChoiceFromSet;
-import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
-import java.awt.*;
 import java.io.PrintWriter;
 
 import java.util.*;
-import java.util.List;
 
 // TODO: Fix for Groovy's model-checking
 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
@@ -54,6 +49,7 @@ public class StateReducer extends ListenerAdapter {
 
   // State reduction fields
   private Integer[] choices;
+  private IntChoiceFromSet currCG;
   private int choiceCounter;
   private Integer choiceUpperBound;
   private boolean isInitialized;
@@ -88,6 +84,7 @@ public class StateReducer extends ListenerAdapter {
   private void initializeStateReduction() {
     if (stateReductionMode) {
       choices = null;
+      currCG = null;
       choiceCounter = 0;
       choiceUpperBound = 0;
       isInitialized = false;
@@ -130,7 +127,7 @@ public class StateReducer extends ListenerAdapter {
         Integer[] cgChoices = icsCG.getAllChoices();
         if (!isInitialized) {
           // Get the upper bound from the last element of the choices
-          choiceUpperBound = (Integer) cgChoices[cgChoices.length - 1];
+          choiceUpperBound = cgChoices[cgChoices.length - 1];
           isInitialized = true;
         }
         // Record the subsequent Integer CGs only until we hit the upper bound
@@ -199,6 +196,7 @@ public class StateReducer extends ListenerAdapter {
         // Update the current pointer to the current set of choices
         if (choices == null || choices != icsCG.getAllChoices()) {
           choiceListStartIndexMap.remove(choices);
+          currCG = icsCG;
           choices = icsCG.getAllChoices();
           // Reset a few things for the sub-graph
           conflictPairMap = new HashMap<>();
@@ -357,19 +355,19 @@ public class StateReducer extends ListenerAdapter {
   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 
     LinkedList<Integer[]> backtrackChoiceLists;
-    // Check if we have a list for this choice number
-    // If not we create a new one for it
-    if (!backtrackMap.containsKey(conflictEventNumber)) {
-      backtrackChoiceLists = new LinkedList<>();
-      backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
-    } else {
-      backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
-    }
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
     // (originally of length 6) since we don't start from event number 0
     if (!isResetAfterAnalysis) {
+      // Check if we have a list for this choice number
+      // If not we create a new one for it
+      if (!backtrackMap.containsKey(conflictEventNumber)) {
+        backtrackChoiceLists = new LinkedList<>();
+        backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
+      } else {
+        backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
+      }
       int maxListLength = choiceUpperBound + 1;
       int listLength = maxListLength - conflictEventNumber;
       Integer[] newChoiceList = new Integer[listLength + 1];
@@ -389,6 +387,8 @@ public class StateReducer extends ListenerAdapter {
       // The start index for the recursion is always 1 (from the main branch)
       choiceListStartIndexMap.put(newChoiceList, 1);
     } else { // This is a sub-graph
+      int backtrackListIndex = cgMap.get(currCG);
+      backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
       int listLength = choices.length;
       Integer[] newChoiceList = new Integer[listLength];
       // Copy everything before the conflict number