From 5665054ebebff35b43fe8987e1597f3729e4de84 Mon Sep 17 00:00:00 2001
From: Daohan Qu <quadhier@163.com>
Date: Mon, 27 Mar 2023 22:56:05 +0800
Subject: [PATCH] Fix PreciseRaceDetector false alarms (#344)

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

* Add four unit tests (two for true positive and two for true negative)
---
 .../bytecode/JVMArrayElementInstruction.java  |  2 +-
 .../nasa/jpf/test/mc/threads/RaceTest.java    | 93 +++++++++++++++++++
 2 files changed, 94 insertions(+), 1 deletion(-)

diff --git a/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java b/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java
index 0dee5921..1aabaf73 100644
--- a/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java
+++ b/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);
   }
   
diff --git a/src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java b/src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java
index 91186b95..ee16c9f6 100644
--- a/src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java
+++ b/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