From a4af45a6689be85ec7f764fda2ad903b59950c73 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng <107266531+CapZTr@users.noreply.github.com> Date: Thu, 21 Nov 2024 19:48:10 +0100 Subject: [PATCH] Fix some unit tests (#784) * Use C11 as a target for vmm code * Set option INIT_DYNAMIC_ALLOCATIONS for C11LFDSTest and C11LocksTest --------- Signed-off-by: Tianrui Zheng Co-authored-by: Tianrui Zheng --- .../com/dat3m/dartagnan/c/C11LFDSTest.java | 26 ++++++++++---- .../com/dat3m/dartagnan/c/C11LocksTest.java | 10 ++++++ .../dat3m/dartagnan/c/C11OrigLFDSTest.java | 11 ------ .../dat3m/dartagnan/c/C11OrigLocksTest.java | 11 ------ .../com/dat3m/dartagnan/c/VMMLFDSTest.java | 35 +++++++++++++------ 5 files changed, 54 insertions(+), 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 index 906f18f90d..4f7bd8c601 100644 --- 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 getProgramPathProvider() { return () -> getTestResourcePath("lfds/" + name + ".ll"); @@ -46,15 +56,19 @@ protected Provider getWmmProvider() { return Providers.createWmmFromName(() -> "c11"); } + @Override + protected Provider getSolverProvider() { + return () -> Solvers.YICES2; + } + @Parameterized.Parameters(name = "{index}: {0}, target={1}") public static Iterable 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 index b9d50c1e27..32006ed96e 100644 --- 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 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 index 66a2c7a387..513da1402b 100644 --- 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 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 index 304e49b730..da84efd8e7 100644 --- 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 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 index 7db0a3bf28..9566fa7bde 100644 --- 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 getProgramPathProvider() { return () -> getTestResourcePath("lfds/" + name + ".ll"); @@ -53,20 +61,25 @@ protected Provider getWmmProvider() { return Providers.createWmmFromName(() -> "vmm"); } + @Override + protected Provider getSolverProvider() { + return () -> Solvers.YICES2; + } + @Parameterized.Parameters(name = "{index}: {0}, target={1}") public static Iterable 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}, }); }