Fix PreciseRaceDetector false alarms (#344), a backport of PR #345 (#347

)

* Change the misused API which causes PreciseRaceDetector to raise false alarms

* Add four unit tests (two for true positive and two for true negative)

src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java

@@ -88,7 +88,7 @@ public Object getIndexOperandAttr (ThreadInfo ti){
 
   @Override
   public ElementInfo peekArrayElementInfo (ThreadInfo ti){
-    int aref = getArrayRef(ti);
+    int aref = peekArrayRef(ti);
     return ti.getElementInfo(aref);
   }
 

src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java

@@ -30,6 +30,8 @@
 class SharedObject {
   int instanceField;
   int whatEver;
+  int[] instanceArrayField1 = new int[2];
+  int[] instanceArrayField2 = new int[2];
 }
 
 
@@ -262,6 +264,97 @@ public void run() {
     }
   }
 
+  public static void writeFirstElem(int[] arr) {
+    arr[0] = 0;
+  }
+
+  @Test
+  public void testInstanceArrayFieldRace() {
+    if (verifyPropertyViolation(PROPERTY, LISTENER)) {
+      SharedObject o = new SharedObject();
+      Thread t1 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(o.instanceArrayField1);
+        }
+      };
+      Thread t2 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(o.instanceArrayField1);
+        }
+      };
+      t1.start();
+      t2.start();
+    }
+  }
+
+  @Test
+  public void testInstanceArrayFieldNoRace() {
+    if (verifyNoPropertyViolation(LISTENER)) {
+      SharedObject o = new SharedObject();
+      Thread t1 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(o.instanceArrayField1);
+        }
+      };
+      Thread t2 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(o.instanceArrayField2);
+        }
+      };
+      t1.start();
+      t2.start();
+    }
+  }
+
+  public static int[] staticArrayField1 = new int[2];
+  public static int[] staticArrayField2 = new int[2];
+
+  @Test
+  public void testStaticArrayFieldRace() {
+    if (verifyPropertyViolation(PROPERTY, LISTENER)) {
+      Thread t1 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(staticArrayField1);
+        }
+      };
+      Thread t2 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(staticArrayField1);
+        }
+      };
+      t1.start();
+      t2.start();
+    }
+  }
+
+  @Test
+  public void testStaticArrayFieldNoRace() {
+    if (verifyNoPropertyViolation(LISTENER)) {
+      Thread t1 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(staticArrayField1);
+        }
+      };
+      Thread t2 = new Thread() {
+        @Override
+        public void run() {
+          writeFirstElem(staticArrayField2);
+        }
+      };
+      t1.start();
+      t2.start();
+    }
+  }
+
+
+
   /*
    * mostly the same as above except of that the race candidates are the same insn instance, i.e. use the same
    * cached insn fields values