From: rtrimana <rtrimana@uci.edu>
Date: Fri, 27 Sep 2019 22:04:28 +0000 (-0700)
Subject: Adding more state reduction analysis.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=1418a055d0a3e09ae21b101195659f04be39c882;hp=1f6b0f10f6cbe063b5e3bb9c281ad8cf9444dd6b

Adding more state reduction analysis.
---

diff --git a/main.jpf b/main.jpf
index da1b57f..9ef7754 100644
--- a/main.jpf
+++ b/main.jpf
@@ -2,8 +2,8 @@ target = main
 
 # This is the listener that can detect variable write-after-write conflicts
 #listener=gov.nasa.jpf.listener.VariableConflictTracker
-#listener=gov.nasa.jpf.listener.StateReducer
-listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
+listener=gov.nasa.jpf.listener.StateReducer
+#listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 
 # Potentially conflicting variables
 # Alarms
diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 7d57f1d..67446f3 100644
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -49,13 +49,25 @@ public class StateReducer extends ListenerAdapter {
   private int depth;
   private int id;
   private Transition transition;
-
+  private HashSet<String> conflictSet;
+  private HashSet<String> appSet;
+  // Holds the event value numbers that execute write instructions
+  private HashSet<Integer> writeEventNumberSet;
   // Holds values that have appeared during CG advances
   private HashSet<Integer> cgChoiceSet;
   private Integer choiceUpperBound;
   private boolean isInitialized;
+  private int currentChoice;
+  // Records how many times BooleanChoiceGenerator has been advanced
+  private int bCGIsAdvanced;
+  // Records how many times we have looped through all the event numbers (IntIntervalGenerator)
+  private int iiCGIsLooped;
+
+  // Constants to determine when to start reducing states
+  private final int BOOLEAN_CG_ADVANCED_THRESHOLD = 2;
+  private final int INTEGER_CG_ADVANCED_THRESHOLD = 50;
 
-  public StateReducer (Config config, JPF jpf) {
+  public StateReducer (Config config) {
     debugMode = config.getBoolean("debug_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);
     if (debugMode) {
@@ -70,6 +82,26 @@ public class StateReducer extends ListenerAdapter {
     cgChoiceSet = new HashSet<>();
     choiceUpperBound = 0;
     isInitialized = false;
+    conflictSet = new HashSet<>();
+    String[] conflictVars = config.getStringArray("variables");
+    // We are not tracking anything if it is null
+    if (conflictVars != null) {
+      for (String var : conflictVars) {
+        conflictSet.add(var);
+      }
+    }
+    appSet = new HashSet<>();
+    String[] apps = config.getStringArray("apps");
+    // We are not tracking anything if it is null
+    if (apps != null) {
+      for (String var : apps) {
+        appSet.add(var);
+      }
+    }
+    currentChoice = 0;
+    writeEventNumberSet = new HashSet<>();
+    bCGIsAdvanced = 0;
+    iiCGIsLooped = 0;
   }
 
   @Override
@@ -114,6 +146,10 @@ public class StateReducer extends ListenerAdapter {
   @Override
   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
     if (stateReductionMode) {
+      // Check for BooleanChoiceGenerator
+      if (currentCG instanceof BooleanChoiceGenerator) {
+        bCGIsAdvanced++;
+      }
       // 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) {
@@ -127,6 +163,16 @@ public class StateReducer extends ListenerAdapter {
         if (cgChoiceSet.contains(choiceUpperBound)) {
           isInitialized = false;
           cgChoiceSet.clear();
+          iiCGIsLooped++;
+        }
+        // Record the current choice
+        currentChoice = iigCG.getNextChoice();
+        // Start reducing (advancing) if the thresholds are passed
+        if (iiCGIsLooped >= INTEGER_CG_ADVANCED_THRESHOLD &&
+            bCGIsAdvanced >= BOOLEAN_CG_ADVANCED_THRESHOLD) {
+          if (!writeEventNumberSet.contains(currentChoice)) {
+            iigCG.advance();
+          }
         }
       }
     }
@@ -172,4 +218,48 @@ public class StateReducer extends ListenerAdapter {
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
     }
   }
+
+  @Override
+  public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+    // CASE #1: Detecting variable write-after-write conflict
+    if (executedInsn instanceof WriteInstruction) {
+      // Check for write-after-write conflict
+      String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+      for(String var : conflictSet) {
+        if (varId.contains(var)) {
+          String writer = getWriter(ti.getStack());
+          // Just return if the writer is not one of the listed apps in the .jpf file
+          if (writer == null)
+            return;
+
+          // Stores event number that executes WriteInstruction
+          if (!writeEventNumberSet.contains(currentChoice)) {
+            writeEventNumberSet.add(currentChoice);
+          }
+        }
+      }
+    }
+  }
+
+  // Find the variable writer
+  // It should be one of the apps listed in the .jpf file
+  private String getWriter(List<StackFrame> sfList) {
+    // Start looking from the top of the stack backward
+    for(int i=sfList.size()-1; i>=0; i--) {
+      MethodInfo mi = sfList.get(i).getMethodInfo();
+      if(!mi.isJPFInternal()) {
+        String method = mi.getStackTraceName();
+        // Check against the apps in the appSet
+        for(String app : appSet) {
+          // There is only one writer at a time but we need to always
+          // check all the potential writers in the list
+          if (method.contains(app)) {
+            return app;
+          }
+        }
+      }
+    }
+
+    return null;
+  }
 }
\ No newline at end of file