From 0e6845fb9f3eeb63767a083168c43c73bcf05044 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 2 Sep 2024 17:27:27 +0200 Subject: [PATCH] - Added cutting of vloc relation (Refinement still fails to understand virtual memory properly) - Enabled Spirv tests --- .../dartagnan/verification/solving/RefinementSolver.java | 2 +- .../com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java | 4 ++-- .../dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java | 4 ++-- 7 files changed, 13 insertions(+), 13 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 24cebd241a..f432c68d0f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -473,7 +473,7 @@ private static boolean isUnknownDefinitionForCAAT(Definition def) { // TODO: We should probably automatically cut all "unknown relation", // i.e., use a white-list of known relations instead of a blacklist of unknown one's. return def instanceof LinuxCriticalSections // LKMM - || def instanceof SyncFence || def instanceof SyncBar; // GPUs + || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs } private static RefinementModel generateRefinementModel(Wmm original) { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 18878d7f92..9c2f3fa06c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -120,10 +121,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 96acad8bbc..9006c1b99f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -113,10 +114,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index 6043e53303..c217abd6f7 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -117,10 +118,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index 5f4ac94440..a5c88e5f77 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -118,10 +119,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index 6124efb5b0..b682b3505e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index 29b7ad7990..da21d9fb30 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); }