Add libvsync tests (#618)

* Add libvsync tests

Signed-off-by: Hernan Ponce de Leon <[email protected]>

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

@@ -0,0 +1,86 @@
+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;
+import com.dat3m.dartagnan.utils.rules.Provider;
+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 java.io.File;
+import java.io.IOException;
+import java.util.Arrays;
+import java.util.EnumSet;
+
+import static com.dat3m.dartagnan.configuration.Arch.IMM;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
+import static com.dat3m.dartagnan.utils.Result.UNKNOWN;
+import static com.dat3m.dartagnan.utils.Result.PASS;
+import static org.junit.Assert.assertEquals;
+
+@RunWith(Parameterized.class)
+public class LibvsyncTest extends AbstractCTest {
+
+    public LibvsyncTest(String name, Arch target, Result expected) {
+        super(name, target, expected);
+    }
+
+    @Override
+    protected Provider<String> getProgramPathProvider() {
+        return Provider.fromSupplier(() -> getTestResourcePath("libvsync/" + name + "-opt.ll"));
+    }
+
+    @Override
+    protected long getTimeout() {
+        return 300000;
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.PROGRAM_SPEC, Property.LIVENESS));
+    }
+
+    @Override
+    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[][]{
+                {"caslock", IMM, UNKNOWN},
+                {"mcslock", IMM, UNKNOWN},
+                {"rec_mcslock", IMM, UNKNOWN},
+                {"rec_spinlock", IMM, UNKNOWN},
+                {"rec_ticketlock", IMM, UNKNOWN},
+                {"rwlock", IMM, UNKNOWN},
+                {"semaphore", IMM, UNKNOWN},
+                {"seqcount", IMM, PASS},
+                {"seqlock", IMM, UNKNOWN},
+                {"ticketlock", IMM, UNKNOWN},
+                {"ttaslock", IMM, UNKNOWN},
+                {"bounded_mpmc_check_empty", IMM, UNKNOWN},
+                {"bounded_mpmc_check_full", IMM, UNKNOWN},
+                {"bounded_spsc", IMM, UNKNOWN},
+        });
+    }
+
+    @Test
+    public void testRefinement() throws Exception {
+        RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+}

dartagnan/src/test/resources/libvsync/README.md

@@ -0,0 +1,62 @@
+These benchmarks where generated from [libvsync](https://github.com/open-s4c/libvsync) with commit id [4f990c4a1f22905405cbf8310eb450b9df86c5dd](https://github.com/open-s4c/libvsync/commit/4f990c4a1f22905405cbf8310eb450b9df86c5dd).
+
+- caslock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/caslock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/caslock.h)
+
+- msclock
+    - [clien-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/mcslock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/mcslock.h)
+
+- rec_mcslock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/rec_mcslock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/rec_mcslock.h)
+
+- rec_spinlock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/rec_spinlock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/rec_spinlock.h)
+
+- rec_ticketlock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/rec_ticketlock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/rec_ticketlock.h)
+
+- rwlock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/rwlock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/rwlock.h)
+
+- semaphore
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/semaphore.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/semaphore.h)
+
+- seqcount
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/seqcount.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/seqcount.h)
+
+- caslock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/seqlock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/seqlock.h)
+
+- ticketlock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/ticketlock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/ticketlock.h)
+
+- ttaslock
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/spinlock/ttaslock.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/spinlock/ttaslock.h)
+
+- bounded_spsc
+    - [client-code](https://github.com/open-s4c/libvsync/blob/main/test/queue/bounded_spsc.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/queue/bounded_spsc.h)
+
+- bounded_mpmc
+    - [client-code (empty)](https://github.com/open-s4c/libvsync/blob/main/test/queue/bounded_mpmc_check_empty.c)
+    - [client-code (full)](https://github.com/open-s4c/libvsync/blob/main/test/queue/bounded_mpmc_check_full.c)
+    - [API](https://github.com/open-s4c/libvsync/blob/main/include/vsync/queue/bounded_mpmc.h)
+
+
+
+
+
+
+
+