Skip to content

Commit

Permalink
Merge branch 'development' into backwards-reaching-definitions
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren authored Sep 5, 2024
2 parents 494ebb7 + 1bd4bd0 commit ecd5d7e
Show file tree
Hide file tree
Showing 8 changed files with 36 additions and 33 deletions.
6 changes: 4 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@

import static com.dat3m.dartagnan.configuration.Property.*;
import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM;
import static com.dat3m.dartagnan.program.Program.SpecificationType.ASSERT;
import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO;

public class PropertyEncoder implements Encoder {
Expand Down Expand Up @@ -275,17 +276,18 @@ private TrackableFormula encodeProgramSpecification() {
case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context));
case EXISTS -> PROGRAM_SPEC.getSMTVariable(context);
};
if (!program.getFormat().equals(LLVM)) {
if (!ASSERT.equals(program.getSpecificationType())) {
encoding = bmgr.and(encoding, encodeProgramTermination());
}
return new TrackableFormula(trackingLiteral, encoding);
}

private BooleanFormula encodeProgramTermination() {
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
return bmgr.and(program.getThreads().stream()
BooleanFormula exitReached = bmgr.and(program.getThreads().stream()
.map(t -> bmgr.equivalence(context.execution(t.getEntry()), context.execution(t.getExit())))
.toList());
return bmgr.and(exitReached, bmgr.not(encodeBoundEventExec()));
}

// ======================================================================
Expand Down
15 changes: 12 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -469,6 +469,13 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS
// ================================================================================================================
// Special memory model processing

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 || def instanceof SameVirtualLocation; // GPUs
}

private static RefinementModel generateRefinementModel(Wmm original) {
// We cut (i) negated axioms, (ii) negated relations (if derived),
// and (iii) some special relations because they are derived from internal relations (like data/addr/ctrl)
Expand All @@ -492,7 +499,7 @@ private static RefinementModel generateRefinementModel(Wmm original) {
} else if (c instanceof Definition def && def.getDefinedRelation().hasName()) {
// (iii) Special relations
final String name = def.getDefinedRelation().getName().get();
if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || name.equals(CRIT)) {
if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) {
constraintsToCut.add(c);
}
} else if (c instanceof Definition def && def instanceof Fences) {
Expand All @@ -516,15 +523,17 @@ private static void addBiases(Wmm memoryModel, EnumSet<Baseline> biases) {
memoryModel.getOrCreatePredefinedRelation(POLOC),
rf,
memoryModel.getOrCreatePredefinedRelation(CO),
memoryModel.getOrCreatePredefinedRelation(FR)))));
memoryModel.getOrCreatePredefinedRelation(FR)
))));
}
if (biases.contains(Baseline.NO_OOTA)) {
// ---- acyclic (dep | rf) ----
memoryModel.addConstraint(new Acyclicity(memoryModel.addDefinition(new Union(memoryModel.newRelation(),
memoryModel.getOrCreatePredefinedRelation(CTRL),
memoryModel.getOrCreatePredefinedRelation(DATA),
memoryModel.getOrCreatePredefinedRelation(ADDR),
rf))));
rf)
)));
}
if (biases.contains(Baseline.ATOMIC_RMW)) {
// ---- empty (rmw & fre;coe) ----
Expand Down
28 changes: 10 additions & 18 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -27,8 +28,7 @@
import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC;
import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath;
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)
Expand Down Expand Up @@ -78,30 +78,23 @@ public static Iterable<Object[]> data() throws IOException {
{"builtin-all-321.spv.dis", 1, PASS},
{"branch-cond-ff.spv.dis", 1, PASS},
{"branch-cond-ff-inverted.spv.dis", 1, PASS},
{"branch-cond-bf.spv.dis", 1, FAIL},
{"branch-cond-bf.spv.dis", 1, UNKNOWN},
{"branch-cond-bf.spv.dis", 2, PASS},
{"branch-cond-bf.spv.dis", 3, PASS},
{"branch-cond-fb.spv.dis", 1, FAIL},
{"branch-cond-fb.spv.dis", 1, UNKNOWN},
{"branch-cond-fb.spv.dis", 2, PASS},
{"branch-cond-fb.spv.dis", 3, PASS},
{"branch-cond-struct.spv.dis", 1, PASS},
{"branch-cond-struct-read-write.spv.dis", 1, PASS},
{"branch-race.spv.dis", 1, PASS},
{"branch-loop.spv.dis", 2, FAIL},
{"branch-loop.spv.dis", 2, UNKNOWN},
{"branch-loop.spv.dis", 3, PASS},
{"branch-loop.spv.dis", 4, PASS},
{"loop-struct-cond.spv.dis", 1, FAIL},
{"loop-struct-cond.spv.dis", 1, UNKNOWN},
{"loop-struct-cond.spv.dis", 2, PASS},
{"loop-struct-cond.spv.dis", 3, PASS},
{"loop-struct-cond-suffix.spv.dis", 1, FAIL},
{"loop-struct-cond-suffix.spv.dis", 1, UNKNOWN},
{"loop-struct-cond-suffix.spv.dis", 2, PASS},
{"loop-struct-cond-suffix.spv.dis", 3, PASS},
{"loop-struct-cond-sequence.spv.dis", 2, FAIL},
{"loop-struct-cond-sequence.spv.dis", 2, UNKNOWN},
{"loop-struct-cond-sequence.spv.dis", 3, PASS},
{"loop-struct-cond-sequence.spv.dis", 4, PASS},
{"loop-struct-cond-nested.spv.dis", 2, FAIL},
{"loop-struct-cond-nested.spv.dis", 2, UNKNOWN},
{"loop-struct-cond-nested.spv.dis", 3, PASS},
{"loop-struct-cond-nested.spv.dis", 4, PASS},
{"phi.spv.dis", 1, PASS},
{"phi-unstruct-true.spv.dis", 1, PASS},
{"phi-unstruct-false.spv.dis", 1, PASS},
Expand All @@ -120,10 +113,9 @@ public static Iterable<Object[]> 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());
}
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -113,10 +114,9 @@ public static Iterable<Object[]> 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());
}
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -117,10 +118,9 @@ public static Iterable<Object[]> 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());
}
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -118,10 +119,9 @@ public static Iterable<Object[]> 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());
}
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -345,10 +346,9 @@ public static Iterable<Object[]> 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());
}
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -345,10 +346,9 @@ public static Iterable<Object[]> 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());
}
Expand Down

0 comments on commit ecd5d7e

Please sign in to comment.