Reads without init events

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.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext;
@@ -37,12 +38,18 @@ public AbstractCTest(String name, Arch target, Result expected) {
 
     // =================== Modifiable behavior ====================
 
+    protected abstract long getTimeout();
+
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.builder()
+                .setOption(OptionNames.USE_INTEGERS, "true")
+                .build();
+    }
+
     protected Provider<String> getProgramPathProvider() {
         return Provider.fromSupplier(() -> getTestResourcePath(name + ".ll"));
     }
 
-    protected abstract long getTimeout();
-
     protected Provider<Integer> getBoundProvider() {
         return Provider.fromSupplier(() -> 1);
     }
@@ -60,9 +67,7 @@ protected Provider<EnumSet<Property>> getPropertyProvider() {
     }
 
     protected Provider<Configuration> getConfigurationProvider() {
-        return Provider.fromSupplier(() -> Configuration.builder()
-                .setOption(OptionNames.USE_INTEGERS, "true")
-                .build());
+        return Provider.fromSupplier(this::getConfiguration);
     }
 
     // =============================================================
@@ -76,7 +81,7 @@ protected Provider<Configuration> getConfigurationProvider() {
     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<Configuration> configurationProvider = Provider.fromSupplier(this::getConfiguration);
     protected final Provider<VerificationTask> taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider);
     protected final Provider<SolverContext> contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider);
     protected final Provider<ProverEnvironment> proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS);

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

@@ -1,22 +1,20 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.parsers.cat.ParserCat;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
 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;
 import org.junit.runners.Parameterized;
 
-import java.io.File;
 import java.io.IOException;
 import java.util.Arrays;
 
 import static com.dat3m.dartagnan.configuration.Arch.C11;
-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;
@@ -45,7 +43,7 @@ protected Provider<Integer> getBoundProvider() {
 
     @Override
     protected Provider<Wmm> getWmmProvider() {
-        return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/c11.cat"))));
+        return Providers.createWmmFromName(() -> "c11");
     }
 
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")

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

@@ -1,22 +1,21 @@
 package com.dat3m.dartagnan.c;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.parsers.cat.ParserCat;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
 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;
 import org.junit.runners.Parameterized;
 
-import java.io.File;
 import java.io.IOException;
 import java.util.Arrays;
 
 import static com.dat3m.dartagnan.configuration.Arch.C11;
-import static com.dat3m.dartagnan.utils.ResourceHelper.*;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
 import static com.dat3m.dartagnan.utils.Result.*;
 import static org.junit.Assert.assertEquals;
 
@@ -39,7 +38,7 @@ protected long getTimeout() {
 
     @Override
     protected Provider<Wmm> getWmmProvider() {
-        return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/c11.cat"))));
+        return Providers.createWmmFromName(() -> "c11");
     }
 
     @Parameterized.Parameters(name = "{index}: {0}, target={1}")

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

@@ -0,0 +1,90 @@
+package com.dat3m.dartagnan.c;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.OptionNames;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
+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;
+import org.junit.runners.Parameterized;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+
+import java.io.IOException;
+import java.util.Arrays;
+
+import static com.dat3m.dartagnan.configuration.Arch.C11;
+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 org.junit.Assert.assertEquals;
+
+@RunWith(Parameterized.class)
+public class C11OrigLFDSTest extends AbstractCTest {
+
+    public C11OrigLFDSTest(String name, Arch target, Result expected) {
+        super(name, target, expected);
+    }
+
+    @Override
+    protected Provider<String> getProgramPathProvider() {
+        return Provider.fromSupplier(() -> getTestResourcePath("lfds/" + name + ".ll"));
+    }
+
+    @Override
+    protected long getTimeout() {
+        return 600000;
+    }
+
+    protected Provider<Integer> getBoundProvider() {
+        return Provider.fromSupplier(() -> 2);
+    }
+
+    @Override
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.builder()
+                .copyFrom(super.getConfiguration())
+                .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
+                .build();
+    }
+
+    @Override
+    protected Provider<Wmm> getWmmProvider() {
+        return Providers.createWmmFromName(() -> "c11-orig");
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, target={1}")
+    public static Iterable<Object[]> data() throws IOException {
+        // Commented ones take too long ATM
+        return Arrays.asList(new Object[][]{
+                // {"dglm", C11, UNKNOWN},
+                {"dglm-CAS-relaxed", C11, FAIL},
+                // {"ms", C11, UNKNOWN},
+                {"ms-CAS-relaxed", C11, FAIL},
+                // {"treiber", C11, UNKNOWN},
+                {"treiber-CAS-relaxed", C11, FAIL},
+                {"chase-lev", C11, PASS},
+                // These ones have an extra thief that violate the assertion
+                {"chase-lev-fail", C11, FAIL},
+                {"hash_table", C11, PASS},
+                {"hash_table-fail", C11, FAIL},
+        });
+    }
+
+    @Test
+    public void testAssume() throws Exception {
+        AssumeSolver s = AssumeSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+
+    // CAAT might not yet work for C11 
+    // @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/C11OrigLocksTest.java

@@ -0,0 +1,101 @@
+package com.dat3m.dartagnan.c;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.OptionNames;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
+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;
+import org.junit.runners.Parameterized;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+
+import java.io.IOException;
+import java.util.Arrays;
+
+import static com.dat3m.dartagnan.configuration.Arch.C11;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
+import static com.dat3m.dartagnan.utils.Result.*;
+import static org.junit.Assert.assertEquals;
+
+@RunWith(Parameterized.class)
+public class C11OrigLocksTest extends AbstractCTest {
+
+    public C11OrigLocksTest(String name, Arch target, Result expected) {
+        super(name, target, expected);
+    }
+
+    @Override
+    protected Provider<String> getProgramPathProvider() {
+        return Provider.fromSupplier(() -> getTestResourcePath("locks/" + name + ".ll"));
+    }
+
+    @Override
+    protected long getTimeout() {
+        return 180000;
+    }
+
+    @Override
+    protected Configuration getConfiguration() throws InvalidConfigurationException {
+        return Configuration.builder()
+                .copyFrom(super.getConfiguration())
+                .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true")
+                .build();
+    }
+
+    @Override
+    protected Provider<Wmm> getWmmProvider() {
+        return Providers.createWmmFromName(() -> "c11-orig");
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, target={1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return Arrays.asList(new Object[][]{
+                {"ttas", C11, UNKNOWN},
+                {"ttas-acq2rx", C11, FAIL},
+                {"ttas-rel2rx", C11, FAIL},
+                {"ticketlock", C11, PASS},
+                {"ticketlock-acq2rx", C11, FAIL},
+                {"ticketlock-rel2rx", C11, FAIL},
+                {"mutex", C11, UNKNOWN},
+                {"mutex-acq2rx_futex", C11, UNKNOWN},
+                {"mutex-acq2rx_lock", C11, FAIL},
+                {"mutex-rel2rx_futex", C11, UNKNOWN},
+                {"mutex-rel2rx_unlock", C11, FAIL},
+                {"spinlock", C11, PASS},
+                {"spinlock-acq2rx", C11, FAIL},
+                {"spinlock-rel2rx", C11, FAIL},
+                // For most models the one below is safe (UNKNOWN)
+                // It could be the case for C11 is unsafe (because it is weaker)
+                // but we are not 100% sure about this
+                {"linuxrwlock", C11, FAIL},
+                {"mutex_musl", C11, UNKNOWN},
+                {"mutex_musl-acq2rx_futex", C11, UNKNOWN},
+                {"mutex_musl-acq2rx_lock", C11, FAIL},
+                {"mutex_musl-rel2rx_futex", C11, UNKNOWN},
+                {"mutex_musl-rel2rx_unlock", C11, FAIL},
+                {"seqlock", C11, PASS},
+                {"clh_mutex", C11, UNKNOWN},
+                {"clh_mutex-acq2rx", C11, FAIL},
+                {"ticket_awnsb_mutex", C11, PASS},
+                {"ticket_awnsb_mutex-acq2rx", C11, FAIL},
+        });
+    }
+
+    @Test
+    public void testAssume() throws Exception {
+        AssumeSolver s = AssumeSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+
+    // CAAT might not yet work for C11 
+    // @Test
+    public void testRefinement() throws Exception {
+        RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+}