Skip to content

Commit c6cc3be

Browse files
hernanponcedeleonhernanponcedeleon
authored
Allow to switch solver in unit tests and add EBR test (#621)
* Allow to switch solver in unit tests * Add EBR test --------- Signed-off-by: Hernan Ponce de Leon <[email protected]>
1 parent f2d9588 commit c6cc3be

File tree

8 files changed

+1864
-20
lines changed

8 files changed

+1864
-20
lines changed

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import org.junit.rules.Timeout;
1616
import org.sosy_lab.common.ShutdownManager;
1717
import org.sosy_lab.common.configuration.Configuration;
18+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
1819
import org.sosy_lab.java_smt.api.ProverEnvironment;
1920
import org.sosy_lab.java_smt.api.SolverContext;
2021

@@ -46,6 +47,10 @@ protected Provider<Integer> getBoundProvider() {
4647
return Provider.fromSupplier(() -> 1);
4748
}
4849

50+
protected Provider<Solvers> getSolverProvider() {
51+
return Provider.fromSupplier(() -> Solvers.Z3);
52+
}
53+
4954
protected Provider<Wmm> getWmmProvider() {
5055
return Providers.createWmmFromArch(targetProvider);
5156
}
@@ -69,10 +74,11 @@ protected Provider<Configuration> getConfigurationProvider() {
6974
protected final Provider<Integer> boundProvider = getBoundProvider();
7075
protected final Provider<Program> programProvider = Providers.createProgramFromPath(filePathProvider);
7176
protected final Provider<Wmm> wmmProvider = getWmmProvider();
77+
protected final Provider<Solvers> solverProvider = getSolverProvider();
7278
protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
7379
protected final Provider<Configuration> configurationProvider = getConfigurationProvider();
7480
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider);
75-
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider);
81+
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider);
7682
protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);
7783

7884
// Special rules
@@ -88,6 +94,7 @@ protected Provider<Configuration> getConfigurationProvider() {
8894
.around(boundProvider)
8995
.around(programProvider)
9096
.around(wmmProvider)
97+
.around(solverProvider)
9198
.around(propertyProvider)
9299
.around(taskProvider)
93100
.around(timeout)

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
package com.dat3m.dartagnan.c;
2+
3+
import com.dat3m.dartagnan.configuration.Arch;
4+
import com.dat3m.dartagnan.utils.Result;
5+
import com.dat3m.dartagnan.utils.rules.Provider;
6+
import com.dat3m.dartagnan.verification.solving.RefinementSolver;
7+
import org.junit.Test;
8+
import org.junit.runner.RunWith;
9+
import org.junit.runners.Parameterized;
10+
import org.sosy_lab.common.configuration.Configuration;
11+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
12+
13+
import java.io.IOException;
14+
import java.util.Arrays;
15+
import static com.dat3m.dartagnan.configuration.Arch.*;
16+
import static com.dat3m.dartagnan.utils.ResourceHelper.*;
17+
import static com.dat3m.dartagnan.utils.Result.*;
18+
import static org.junit.Assert.assertEquals;
19+
20+
@RunWith(Parameterized.class)
21+
public class EBRTest extends AbstractCTest {
22+
23+
public EBRTest(String name, Arch target, Result expected) {
24+
super(name, target, expected);
25+
}
26+
27+
@Override
28+
protected Provider<String> getProgramPathProvider() {
29+
return Provider.fromSupplier(() -> getTestResourcePath("smr/" + name + ".ll"));
30+
}
31+
32+
@Override
33+
protected long getTimeout() {
34+
return 180000;
35+
}
36+
37+
@Override
38+
protected Provider<Solvers> getSolverProvider() {
39+
return Provider.fromSupplier(() -> Solvers.YICES2);
40+
}
41+
42+
@Override
43+
protected Provider<Configuration> getConfigurationProvider() {
44+
return Provider.fromSupplier(() -> Configuration.defaultConfiguration());
45+
}
46+
47+
@Parameterized.Parameters(name = "{index}: {0}, target={1}")
48+
public static Iterable<Object[]> data() throws IOException {
49+
return Arrays.asList(new Object[][]{
50+
{"ck_ebr", IMM, FAIL},
51+
{"ck_ebr", ARM8, PASS},
52+
{"ck_ebr", POWER, PASS},
53+
{"ck_ebr", RISCV, PASS},
54+
});
55+
}
56+
57+
@Test
58+
public void testRefinement() throws Exception {
59+
RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
60+
assertEquals(expected, s.getResult());
61+
}
62+
}

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

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package com.dat3m.dartagnan.c;
22

33
import com.dat3m.dartagnan.configuration.Arch;
4-
import com.dat3m.dartagnan.configuration.OptionNames;
54
import com.dat3m.dartagnan.configuration.Property;
65
import com.dat3m.dartagnan.parsers.cat.ParserCat;
76
import com.dat3m.dartagnan.utils.Result;
@@ -42,6 +41,11 @@ protected long getTimeout() {
4241
return 300000;
4342
}
4443

44+
@Override
45+
protected Provider<Configuration> getConfigurationProvider() {
46+
return Provider.fromSupplier(() -> Configuration.defaultConfiguration());
47+
}
48+
4549
@Override
4650
protected Provider<EnumSet<Property>> getPropertyProvider() {
4751
return Provider.fromSupplier(() -> EnumSet.of(Property.PROGRAM_SPEC, Property.LIVENESS));
@@ -52,12 +56,6 @@ protected Provider<Wmm> getWmmProvider() {
5256
return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat"))));
5357
}
5458

55-
protected Provider<Configuration> getConfigurationProvider() {
56-
return Provider.fromSupplier(() -> Configuration.builder()
57-
.setOption(OptionNames.SOLVER, "yices2")
58-
.build());
59-
}
60-
6159
@Parameterized.Parameters(name = "{index}: {0}, target={1}")
6260
public static Iterable<Object[]> data() throws IOException {
6361
return Arrays.asList(new Object[][]{

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import org.junit.rules.Timeout;
1919
import org.sosy_lab.common.ShutdownManager;
2020
import org.sosy_lab.common.configuration.Configuration;
21+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
2122
import org.sosy_lab.java_smt.api.ProverEnvironment;
2223
import org.sosy_lab.java_smt.api.SolverContext;
2324
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -93,8 +94,8 @@ protected Provider<Configuration> getConfigurationProvider() {
9394
protected final Provider<Configuration> configProvider = getConfigurationProvider();
9495
protected final Provider<VerificationTask> task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider);
9596
protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider);
96-
protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider);
97-
protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider);
97+
protected final Provider<SolverContext> context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
98+
protected final Provider<SolverContext> context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
9899
protected final Provider<ProverEnvironment> prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS);
99100
protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS);
100101

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import org.junit.rules.Timeout;
1919
import org.sosy_lab.common.ShutdownManager;
2020
import org.sosy_lab.common.configuration.Configuration;
21+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
2122
import org.sosy_lab.java_smt.api.ProverEnvironment;
2223
import org.sosy_lab.java_smt.api.SolverContext;
2324
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -108,7 +109,7 @@ protected long getTimeout() {
108109
protected final Provider<Result> expectedResultProvider = Provider.fromSupplier(() -> expectedResults.get(filePathProvider.get().substring(filePathProvider.get().indexOf("/") + 1)));
109110
protected final Provider<Configuration> configProvider = getConfigurationProvider();
110111
protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider);
111-
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider);
112+
protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3);
112113
protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
113114
protected final Provider<ProverEnvironment> prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS);
114115

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

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import org.sosy_lab.common.configuration.InvalidConfigurationException;
88
import org.sosy_lab.common.log.BasicLogManager;
99
import org.sosy_lab.java_smt.SolverContextFactory;
10+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
1011
import org.sosy_lab.java_smt.api.SolverContext;
1112

1213
public class TestHelper {
@@ -15,17 +16,19 @@ private TestHelper() {
1516
}
1617

1718
public static SolverContext createContext() throws InvalidConfigurationException {
18-
return createContextWithShutdownNotifier(ShutdownNotifier.createDummy());
19+
return createContextWithShutdownNotifier(ShutdownNotifier.createDummy(), Solvers.Z3);
1920
}
2021

21-
public static SolverContext createContextWithShutdownNotifier(ShutdownNotifier notifier) throws InvalidConfigurationException {
22-
Configuration config = Configuration.builder()
22+
public static SolverContext createContextWithShutdownNotifier(ShutdownNotifier notifier, Solvers solver) throws InvalidConfigurationException {
23+
Configuration config = solver.equals(Solvers.Z3) ?
24+
Configuration.builder()
2325
.setOption(PHANTOM_REFERENCES, "true")
24-
.build();
26+
.build() :
27+
Configuration.defaultConfiguration();
2528
return SolverContextFactory.createSolverContext(
2629
config,
2730
BasicLogManager.create(config),
2831
notifier,
29-
SolverContextFactory.Solvers.Z3);
32+
solver);
3033
}
3134
}

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import org.sosy_lab.common.ShutdownManager;
1313
import org.sosy_lab.common.ShutdownNotifier;
1414
import org.sosy_lab.common.configuration.Configuration;
15+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
1516
import org.sosy_lab.java_smt.api.ProverEnvironment;
1617
import org.sosy_lab.java_smt.api.SolverContext;
1718

@@ -72,12 +73,12 @@ public static Provider<VerificationTask> createTask(Supplier<Program> programSup
7273

7374
// =========================== Solving related providers ==============================
7475

75-
public static Provider<SolverContext> createSolverContext(Supplier<ShutdownNotifier> shutdownNotifierSupplier) {
76-
return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownNotifierSupplier.get()));
76+
public static Provider<SolverContext> createSolverContext(Supplier<ShutdownNotifier> shutdownNotifierSupplier, Supplier<Solvers> solverSupplier) {
77+
return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownNotifierSupplier.get(), solverSupplier.get()));
7778
}
7879

79-
public static Provider<SolverContext> createSolverContextFromManager(Supplier<ShutdownManager> shutdownManagerSupplier) {
80-
return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier()));
80+
public static Provider<SolverContext> createSolverContextFromManager(Supplier<ShutdownManager> shutdownManagerSupplier, Supplier<Solvers> solverSupplier) {
81+
return Provider.fromSupplier(() -> TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get()));
8182
}
8283

8384
public static Provider<ProverEnvironment> createProver(Supplier<SolverContext> contextSupplier, Supplier<SolverContext.ProverOptions[]> optionsSupplier) {

0 commit comments

Comments
 (0)