From 89c50363b6c404c37f8c33eb3fc162eb61b80816 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Wed, 31 Jul 2019 12:09:09 -0700
Subject: [PATCH] Fixing a bug in the tracker.

---
 .../jpf/listener/VariableConflictTracker.java | 79 +++++++++++++++++--
 1 file changed, 74 insertions(+), 5 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
index 4a2c4f1..80bc940 100644
--- a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
@@ -69,7 +69,6 @@ public class VariableConflictTracker extends ListenerAdapter {
 
   @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
@@ -111,7 +110,7 @@ public class VariableConflictTracker extends ListenerAdapter {
   }
   
   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
-    
+
     if (writeMap.containsKey(var)) {
       // Subsequent writes to the variable
       VarChange current = writeMap.get(var);
@@ -154,13 +153,15 @@ public class VariableConflictTracker extends ListenerAdapter {
   // Find the variable writer
   // It should be one of the apps listed in the .jpf file
   private String getWriter(List<StackFrame> sfList) {
-
-    for(StackFrame sf : sfList) {
-      MethodInfo mi = sf.getMethodInfo();
+    // 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;
           }
@@ -254,6 +255,29 @@ public class VariableConflictTracker extends ListenerAdapter {
     }
   }
 
+  private String getName(ThreadInfo ti, Instruction inst, byte type) {
+    String name;
+    int index;
+    boolean store;
+
+    if ((inst instanceof JVMLocalVariableInstruction) ||
+            (inst instanceof JVMFieldInstruction)) {
+      name = ((LocalVariableInstruction) inst).getVariableId();
+      name = name.substring(name.lastIndexOf('.') + 1);
+
+      return(name);
+    }
+
+    if (inst instanceof JVMArrayElementInstruction) {
+      store  = inst instanceof StoreInstruction;
+      name   = getArrayName(ti, type, store);
+      index  = getArrayIndex(ti, type, store);
+      return(name + '[' + index + ']');
+    }
+
+    return(null);
+  }
+
   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
     StackFrame frame;
     int lo, hi;
@@ -272,9 +296,54 @@ public class VariableConflictTracker extends ListenerAdapter {
        return(decodeValue(type, lo, hi));
     }
 
+    if (inst instanceof JVMArrayElementInstruction)
+      return(getArrayValue(ti, type));
+
     return(null);
   }
 
+  private String getArrayName(ThreadInfo ti, byte type, boolean store) {
+    String attr;
+    int offset;
+
+    offset = calcOffset(type, store) + 1;
+    // <2do> String is really not a good attribute type to retrieve!
+    StackFrame frame = ti.getTopFrame();
+    attr   = frame.getOperandAttr( offset, String.class);
+
+    if (attr != null) {
+      return(attr);
+    }
+
+    return("?");
+  }
+
+  private int getArrayIndex(ThreadInfo ti, byte type, boolean store) {
+    int offset;
+
+    offset = calcOffset(type, store);
+
+    return(ti.getTopFrame().peek(offset));
+  }
+
+  private final static int calcOffset(byte type, boolean store) {
+    if (!store)
+      return(0);
+
+    return(Types.getTypeSize(type));
+  }
+
+  private String getArrayValue(ThreadInfo ti, byte type) {
+    StackFrame frame;
+    int lo, hi;
+
+    frame = ti.getTopFrame();
+    lo    = frame.peek();
+    hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
+
+    return(decodeValue(type, lo, hi));
+  }
+
   private final static String decodeValue(byte type, int lo, int hi) {
     switch (type) {
       case Types.T_ARRAY:   return(null);
-- 
2.34.1