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)
javapathfinder · Mar 27, 2023 · 5665054 · 5665054
1 parent a816054
commit 5665054
Show file tree

Hide file tree

Showing 2 changed files with 94 additions and 1 deletion.
diff --git 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
@@ -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