Merge branch 'development' into caat_domainIdentity

hernanponcedeleon · Nov 21, 2024 · 35742da · 35742da
2 parents 336e853 + a4af45a
commit 35742da
Show file tree

Hide file tree

Showing 5 changed files with 54 additions and 39 deletions.
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java
@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
 import com.dat3m.dartagnan.utils.rules.Providers;
@@ -10,14 +11,16 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 
 import java.io.IOException;
 import java.util.Arrays;
 
 import static com.dat3m.dartagnan.configuration.Arch.C11;
 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)
@@ -27,6 +30,13 @@ public C11LFDSTest(String name, Arch target, Result expected) {
         super(name, target, expected);
     }
 
+    @Override
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.builder()
+                            .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
+                            .build();
+    }
+
     @Override
     protected Provider<String> getProgramPathProvider() {
         return () -> getTestResourcePath("lfds/" + name + ".ll");
@@ -46,15 +56,19 @@ protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "c11");
     }
 
+    @Override
+    protected Provider<Solvers> getSolverProvider() {
+        return () -> Solvers.YICES2;
+    }
+
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")
     public static Iterable<Object[]> data() throws IOException {
-        // Commented ones take too long ATM
         return Arrays.asList(new Object[][]{
-                // {"dglm", C11, UNKNOWN},
+                {"dglm", C11, UNKNOWN},
                 {"dglm-CAS-relaxed", C11, FAIL},
-                // {"ms", C11, UNKNOWN},
+                {"ms", C11, UNKNOWN},
                 {"ms-CAS-relaxed", C11, FAIL},
-                // {"treiber", C11, UNKNOWN},
+                {"treiber", C11, UNKNOWN},
                 {"treiber-CAS-relaxed", C11, FAIL},
                 {"chase-lev", C11, PASS},
                 // These have an extra thief that violate the assertion

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java
@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
 import com.dat3m.dartagnan.utils.rules.Providers;
@@ -10,6 +11,8 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
 
 import java.io.IOException;
 import java.util.Arrays;
@@ -26,6 +29,13 @@ public C11LocksTest(String name, Arch target, Result expected) {
         super(name, target, expected);
     }
 
+    @Override
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.builder()
+                            .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
+                            .build();
+    }
+
     @Override
     protected Provider<String> getProgramPathProvider() {
         return () -> getTestResourcePath("locks/" + name + ".ll");

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLFDSTest.java
@@ -1,15 +1,12 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
 import com.dat3m.dartagnan.utils.rules.Providers;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
-import org.sosy_lab.common.configuration.Configuration;
-import org.sosy_lab.common.configuration.InvalidConfigurationException;
 
 @RunWith(Parameterized.class)
 public class C11OrigLFDSTest extends C11LFDSTest {
@@ -18,14 +15,6 @@ public C11OrigLFDSTest(String name, Arch target, Result expected) {
         super(name, target, expected);
     }
 
-    @Override
-    protected Configuration getConfiguration() throws InvalidConfigurationException {
-        return Configuration.builder()
-                .copyFrom(super.getConfiguration())
-                .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
-                .build();
-    }
-
     @Override
     protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "c11-orig");

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLocksTest.java
@@ -1,15 +1,12 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
 import com.dat3m.dartagnan.utils.rules.Providers;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
-import org.sosy_lab.common.configuration.Configuration;
-import org.sosy_lab.common.configuration.InvalidConfigurationException;
 
 @RunWith(Parameterized.class)
 public class C11OrigLocksTest extends C11LocksTest {
@@ -18,14 +15,6 @@ public C11OrigLocksTest(String name, Arch target, Result expected) {
         super(name, target, expected);
     }
 
-    @Override
-    protected Configuration getConfiguration() throws InvalidConfigurationException {
-        return Configuration.builder()
-                .copyFrom(super.getConfiguration())
-                .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
-                .build();
-    }
-
     @Override
     protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "c11-orig");

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java
@@ -10,12 +10,15 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 
 import java.io.IOException;
 import java.util.Arrays;
 import java.util.EnumSet;
 
-import static com.dat3m.dartagnan.configuration.Arch.IMM;
+import static com.dat3m.dartagnan.configuration.Arch.C11;
 import static com.dat3m.dartagnan.configuration.Property.*;
 import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
 import static com.dat3m.dartagnan.utils.Result.*;
@@ -28,6 +31,11 @@ public VMMLFDSTest(String name, Arch target, Result expected) {
         super(name, target, expected);
     }
 
+    @Override
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.defaultConfiguration();
+    }
+
     @Override
     protected Provider<String> getProgramPathProvider() {
         return () -> getTestResourcePath("lfds/" + name + ".ll");
@@ -53,20 +61,25 @@ protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromName(() -> "vmm");
     }
 
+    @Override
+    protected Provider<Solvers> getSolverProvider() {
+        return () -> Solvers.YICES2;
+    }
+
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{
-                {"dglm", IMM, UNKNOWN},
-                {"dglm-CAS-relaxed", IMM, FAIL},
-                {"ms", IMM, UNKNOWN},
-                {"ms-CAS-relaxed", IMM, FAIL},
-                {"treiber", IMM, UNKNOWN},
-                {"treiber-CAS-relaxed", IMM, FAIL},
-                {"chase-lev", IMM, PASS},
+                {"dglm", C11, UNKNOWN},
+                {"dglm-CAS-relaxed", C11, FAIL},
+                {"ms", C11, UNKNOWN},
+                {"ms-CAS-relaxed", C11, FAIL},
+                {"treiber", C11, UNKNOWN},
+                {"treiber-CAS-relaxed", C11, FAIL},
+                {"chase-lev", C11, PASS},
                 // These have an extra thief that violate the assertion
-                {"chase-lev-fail", IMM, FAIL},
-                {"hash_table", IMM, PASS},
-                {"hash_table-fail", IMM, FAIL},
+                {"chase-lev-fail", C11, FAIL},
+                {"hash_table", C11, PASS},
+                {"hash_table-fail", C11, FAIL},
         });
     }