Skip to content

Commit 62cab51

Browse files
ThomasHaasThomasHaas
authored
Merge branch 'development' into tbaa
2 parents bf5db18 + c6cc3be commit 62cab51

File tree

11 files changed

+1877
-31
lines changed

11 files changed

+1877
-31
lines changed

‎dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntLiteral.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,10 @@ public int getValueAsInt() {
3131
return value.intValueExact();
3232
}
3333

34+
public long getValueAsLong() {
35+
return value.longValueExact();
36+
}
37+
3438
public boolean isOne() { return value.equals(BigInteger.ONE); }
3539
public boolean isZero() { return value.equals(BigInteger.ZERO); }
3640

‎dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -97,11 +97,11 @@ private void promoteAll(Function function, Matcher matcher) {
9797
if (event instanceof Load load) {
9898
final Register reg = load.getResultRegister();
9999
assert load.getUsers().isEmpty();
100-
load.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(registers.get(access.offset), reg.getType())));
100+
load.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(registers.get((int)access.offset), reg.getType())));
101101
loadCount++;
102102
}
103103
if (event instanceof Store store) {
104-
final Register reg = registers.get(access.offset);
104+
final Register reg = registers.get((int)access.offset);
105105
assert store.getUsers().isEmpty();
106106
store.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(store.getMemValue(), reg.getType())));
107107
storeCount++;
@@ -142,14 +142,14 @@ private List<Type> getPrimitiveReplacementTypes(Alloc allocation) {
142142
}
143143

144144
// Invariant: base != null
145-
private record AddressOffset(RegWriter base, int offset) {
146-
private AddressOffset increase(int o) {
145+
private record AddressOffset(RegWriter base, long offset) {
146+
private AddressOffset increase(long o) {
147147
return o == 0 ? this : new AddressOffset(base, offset + o);
148148
}
149149
}
150150

151151
// Invariant: register != null
152-
private record RegisterOffset(Register register, int offset) {}
152+
private record RegisterOffset(Register register, long offset) {}
153153

154154
// Processes events in program order.
155155
// Returns a label, if it is program-ordered before the current event and its symbolic state was updated.
@@ -327,14 +327,14 @@ private void publishRegisters(Set<Register> registers) {
327327
}
328328

329329
private RegisterOffset matchGEP(Expression expression) {
330-
int sum = 0;
330+
long sum = 0;
331331
while (!(expression instanceof Register register)) {
332332
if (!(expression instanceof IntBinaryExpr bin) ||
333333
bin.getKind() != IntBinaryOp.ADD ||
334334
!(bin.getRight() instanceof IntLiteral offset)) {
335335
return null;
336336
}
337-
sum += offset.getValueAsInt();
337+
sum += offset.getValueAsLong();
338338
expression = bin.getLeft();
339339
}
340340
return new RegisterOffset(register, sum);

‎dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -25,10 +25,8 @@ public void run(Program program) {
2525
program.getThreadEvents(RegReader.class).forEach(r -> r.transformExpressions(collector));
2626
// Also add MemoryObjects referenced by initial values (this does happen in Litmus code)
2727
for (MemoryObject obj : memory.getObjects()) {
28-
for (int field : obj.getStaticallyInitializedFields()) {
29-
if (obj.getInitialValue(field) instanceof MemoryObject memObj) {
30-
collector.memoryObjects.add(memObj);
31-
}
28+
for (Integer field : obj.getStaticallyInitializedFields()) {
29+
obj.getInitialValue(field).accept(collector);
3230
}
3331
}
3432
// FIXME: We should also traverse the program spec for references to memory objects

‎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)