update expectationss

hernanponcedeleon · Feb 13, 2025 · 62f28c5 · 62f28c5
1 parent 6b10bf4
commit 62f28c5
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 16 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java
@@ -395,7 +395,7 @@ public static List<String> getScopeTags() {
         }
 
         public static List<String> getSpaceTags() {
-            return List.of(GLOBAL_SPACE, LOCAL_SPACE);
+            return List.of(GLOBAL_SPACE, LOCAL_SPACE, GENERIC_SPACE);
         }
 
         public static List<String> getSpaceTags(Event e) {

diff --git a/.../src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java b/.../src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java
@@ -106,6 +106,7 @@ public List<Event> visitSpirvCmpXchg(SpirvCmpXchg e) {
         }
         String scope = toOpenCLTag(Tag.Spirv.getScopeTag(e.getTags()));
         String storageClass = toOpenCLTag(Tag.Spirv.getStorageClassTag(e.getTags()));
+        e.addTags(scope, storageClass);
         String mo = toOpenCLTag(spvMoEq);
         if (mo == null) {
             mo = Tag.C11.MO_RELAXED;
@@ -120,8 +121,6 @@ public List<Event> visitSpirvCmpXchg(SpirvCmpXchg e) {
         RMWStore store = newRMWStoreWithMo(load, address, value, Tag.C11.storeMO(mo));
         Local local = newLocal(cmpResultRegister, expressions.makeEQ(resultRegister, expected));
         CondJump condJump = newJumpUnless(cmpResultRegister, casEnd);
-        load.addTags(scope, storageClass);
-        store.addTags(scope, storageClass);
         return tagList(e, eventSequence(
                 load,
                 local,

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvAssertionsTest.java
@@ -28,8 +28,7 @@
 import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
-import static com.dat3m.dartagnan.utils.Result.FAIL;
-import static com.dat3m.dartagnan.utils.Result.PASS;
+import static com.dat3m.dartagnan.utils.Result.*;
 import static org.junit.Assert.assertEquals;
 
 @RunWith(Parameterized.class)
@@ -49,11 +48,11 @@ public ClangSpirvAssertionsTest(String file, int bound, Result expected) {
     @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{
-                {"caslock-1.1.2.spv.dis", 2, PASS},
-                {"caslock-2.1.1.spv.dis", 2, PASS},
+                {"caslock-1.1.2.spv.dis", 2, UNKNOWN},
+                {"caslock-2.1.1.spv.dis", 2, UNKNOWN},
                 {"caslock-acq2rx.spv.dis", 2, FAIL},
                 {"caslock-rel2rx.spv.dis", 2, FAIL},
-                {"caslock-dv2wg-2.1.1.spv.dis", 2, PASS},
+                {"caslock-dv2wg-2.1.1.spv.dis", 2, UNKNOWN},
                 {"caslock-dv2wg-1.1.2.spv.dis", 2, FAIL},
                 {"CORR.spv.dis", 1, PASS},
                 {"IRIW.spv.dis", 1, PASS},
@@ -75,8 +74,8 @@ public static Iterable<Object[]> data() throws IOException {
                 {"ttaslock-dv2wg-1.1.2.spv.dis", 1, FAIL},
 
                 {"xf-barrier-2.1.2.spv.dis", 9, PASS},
-                {"xf-barrier-3.1.3.spv.dis", 9, PASS},
-                {"xf-barrier-1.1.2.spv.dis", 2, PASS},
+                // {"xf-barrier-3.1.3.spv.dis", 9, PASS},
+                // {"xf-barrier-1.1.2.spv.dis", 2, PASS},
                 {"xf-barrier-2.1.1.spv.dis", 9, PASS},
                 {"xf-barrier-fail1.spv.dis", 9, FAIL},
                 {"xf-barrier-fail2.spv.dis", 9, FAIL},

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvRacesTest.java
@@ -27,8 +27,7 @@
 import static com.dat3m.dartagnan.configuration.Property.CAT_SPEC;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
-import static com.dat3m.dartagnan.utils.Result.FAIL;
-import static com.dat3m.dartagnan.utils.Result.PASS;
+import static com.dat3m.dartagnan.utils.Result.*;
 import static org.junit.Assert.assertEquals;
 
 @RunWith(Parameterized.class)
@@ -48,13 +47,13 @@ public ClangSpirvRacesTest(String file, int bound, Result expected) {
     @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{
-                {"caslock-1.1.2.spv.dis", 2, PASS},
-                {"caslock-2.1.1.spv.dis", 2, PASS},
+                {"caslock-1.1.2.spv.dis", 2, UNKNOWN},
+                {"caslock-2.1.1.spv.dis", 2, UNKNOWN},
                 {"caslock-acq2rx.spv.dis", 2, FAIL},
                 {"caslock-rel2rx.spv.dis", 2, FAIL},
-                {"caslock-dv2wg-2.1.1.spv.dis", 2, PASS},
+                {"caslock-dv2wg-2.1.1.spv.dis", 2, UNKNOWN},
                 {"caslock-dv2wg-1.1.2.spv.dis", 1, FAIL},
-                {"caslock-dv2wg-2.2.1.spv.dis", 2, PASS},
+                {"caslock-dv2wg-2.2.1.spv.dis", 2, UNKNOWN},
                 {"caslock-dv2wg-2.2.2.spv.dis", 1, FAIL},
                 {"CORR.spv.dis", 1, PASS},
                 {"IRIW.spv.dis", 1, PASS},