Allow to switch solver in unit tests and add EBR test

dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java

@@ -15,6 +15,7 @@
 import org.junit.rules.Timeout;
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext;
 
@@ -46,6 +47,10 @@ protected Provider<Integer> getBoundProvider() {
         return Provider.fromSupplier(() -> 1);
     }
 
+    protected Provider<Solvers> getSolverProvider() {
+        return Provider.fromSupplier(() -> Solvers.Z3);
+    }
+
     protected Provider<Wmm> getWmmProvider() {
         return Providers.createWmmFromArch(targetProvider);
     }
@@ -69,10 +74,11 @@ protected Provider<Configuration> getConfigurationProvider() {
     protected final Provider<Integer> boundProvider = getBoundProvider();
     protected final Provider<Program> programProvider = Providers.createProgramFromPath(filePathProvider);
     protected final Provider<Wmm> wmmProvider = getWmmProvider();
+    protected final Provider<Solvers> solverProvider = getSolverProvider();
     protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
     protected final Provider<Configuration> configurationProvider = getConfigurationProvider();
     protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider);
-    protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider);
+    protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider);
     protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);
 
     // Special rules
@@ -88,6 +94,7 @@ protected Provider<Configuration> getConfigurationProvider() {
             .around(boundProvider)
             .around(programProvider)
             .around(wmmProvider)
+            .around(solverProvider)
             .around(propertyProvider)
             .around(taskProvider)
             .around(timeout)

dartagnan/src/test/java/com/dat3m/dartagnan/c/EBRTest.java

@@ -0,0 +1,62 @@
+package com.dat3m.dartagnan.c;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
+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.java_smt.SolverContextFactory.Solvers;
+
+import java.io.IOException;
+import java.util.Arrays;
+import static com.dat3m.dartagnan.configuration.Arch.*;
+import static com.dat3m.dartagnan.utils.ResourceHelper.*;
+import static com.dat3m.dartagnan.utils.Result.*;
+import static org.junit.Assert.assertEquals;
+
+@RunWith(Parameterized.class)
+public class EBRTest extends AbstractCTest {
+
+    public EBRTest(String name, Arch target, Result expected) {
+        super(name, target, expected);
+    }
+
+    @Override
+    protected Provider<String> getProgramPathProvider() {
+        return Provider.fromSupplier(() -> getTestResourcePath("smr/" + name + ".ll"));
+    }
+
+    @Override
+    protected long getTimeout() {
+        return 180000;
+    }
+
+    @Override
+    protected Provider<Solvers> getSolverProvider() {
+        return Provider.fromSupplier(() -> Solvers.YICES2);
+    }
+
+    @Override
+    protected Provider<Configuration> getConfigurationProvider() {
+        return Provider.fromSupplier(() -> Configuration.defaultConfiguration());
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, target={1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return Arrays.asList(new Object[][]{
+            {"ck_ebr", IMM, FAIL},
+            {"ck_ebr", ARM8, PASS},
+            {"ck_ebr", POWER, PASS},
+            {"ck_ebr", RISCV, PASS},
+        });
+    }
+
+    @Test
+    public void testRefinement() throws Exception {
+        RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+}

dartagnan/src/test/java/com/dat3m/dartagnan/c/LibvsyncTest.java

@@ -1,7 +1,6 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.configuration.Property;
 import com.dat3m.dartagnan.parsers.cat.ParserCat;
 import com.dat3m.dartagnan.utils.Result;
@@ -42,6 +41,11 @@ protected long getTimeout() {
         return 300000;
     }
 
+    @Override
+    protected Provider<Configuration> getConfigurationProvider() {
+        return Provider.fromSupplier(() -> Configuration.defaultConfiguration());
+    }
+
     @Override
     protected Provider<EnumSet<Property>> getPropertyProvider() {
         return Provider.fromSupplier(() -> EnumSet.of(Property.PROGRAM_SPEC, Property.LIVENESS));
@@ -52,12 +56,6 @@ protected Provider<Wmm> getWmmProvider() {
         return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat"))));
     }
 
-    protected Provider<Configuration> getConfigurationProvider() {
-        return Provider.fromSupplier(() -> Configuration.builder()
-                .setOption(OptionNames.SOLVER, "yices2")
-                .build());
-    }
-
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{

dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java

@@ -18,6 +18,7 @@
 import org.junit.rules.Timeout;
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -93,8 +94,8 @@ protected Provider<Configuration> getConfigurationProvider() {
     protected final Provider<Configuration> configProvider = getConfigurationProvider();
     protected final Provider<VerificationTask> task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider);
     protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider,  () -> 1, configProvider);
-    protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider);
-    protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider);
+    protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
+    protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
     protected final Provider<ProverEnvironment> prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS);
     protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS);
 

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java

@@ -18,6 +18,7 @@
 import org.junit.rules.Timeout;
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -108,7 +109,7 @@ protected long getTimeout() {
     protected final Provider<Result> expectedResultProvider = Provider.fromSupplier(() -> expectedResults.get(filePathProvider.get().substring(filePathProvider.get().indexOf("/") + 1)));
     protected final Provider<Configuration> configProvider = getConfigurationProvider();
     protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider);
-    protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider);
+    protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
     protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
     protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
 

dartagnan/src/test/java/com/dat3m/dartagnan/utils/TestHelper.java

@@ -7,6 +7,7 @@
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.common.log.BasicLogManager;
 import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.SolverContext;
 
 public class TestHelper {
@@ -15,17 +16,19 @@ private TestHelper() {
     }
 
     public static SolverContext createContext() throws InvalidConfigurationException {
-        return createContextWithShutdownNotifier(ShutdownNotifier.createDummy());
+        return createContextWithShutdownNotifier(ShutdownNotifier.createDummy(), Solvers.Z3);
     }
 
-    public static SolverContext createContextWithShutdownNotifier(ShutdownNotifier notifier) throws InvalidConfigurationException {
-        Configuration config = Configuration.builder()
+    public static SolverContext createContextWithShutdownNotifier(ShutdownNotifier notifier, Solvers solver) throws InvalidConfigurationException {
+        Configuration config = solver.equals(Solvers.Z3) ?
+            Configuration.builder()
                 .setOption(PHANTOM_REFERENCES, "true")
-                .build();
+                .build() :
+            Configuration.defaultConfiguration();
         return SolverContextFactory.createSolverContext(
                 config,
                 BasicLogManager.create(config),
                 notifier,
-                SolverContextFactory.Solvers.Z3);
+                solver);
     }
 }

dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java

@@ -12,6 +12,7 @@
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext;
 
@@ -72,12 +73,12 @@ public static Provider<VerificationTask> createTask(Supplier<Program> programSup
 
     // =========================== Solving related providers ==============================
 
-    public static Provider<SolverContext> createSolverContext(Supplier<ShutdownNotifier> shutdownNotifierSupplier) {
-        return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownNotifierSupplier.get()));
+    public static Provider<SolverContext> createSolverContext(Supplier<ShutdownNotifier> shutdownNotifierSupplier, Supplier<Solvers> solverSupplier) {
+        return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownNotifierSupplier.get(), solverSupplier.get()));
     }
 
-    public static Provider<SolverContext> createSolverContextFromManager(Supplier<ShutdownManager> shutdownManagerSupplier) {
-        return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier()));
+    public static Provider<SolverContext> createSolverContextFromManager(Supplier<ShutdownManager> shutdownManagerSupplier, Supplier<Solvers> solverSupplier) {
+        return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get()));
     }
 
     public static Provider<ProverEnvironment> createProver(Supplier<SolverContext> contextSupplier, Supplier<SolverContext.ProverOptions[]> optionsSupplier) {