Change default value of property and force thread creation options (h…

…ernanponcedeleon#675)

* Check all three properties by default

* Force thread creation to succeed by default

* Improve error msg for mixed type properties

---------

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>

README.md

@@ -102,6 +102,7 @@ The target architecture is supposed to match (this is responsibility of the user
 
 Further options can be specified using `--<option>=<value>`. Common options include:
 - `bound`: unrolling bound for the BMC (default is 1).
+- `property`: the properties to be checked. Possible values are `program_spec` (e.g, safety properties as program assertions), `liveness` (i.e., all spinloops terminate), `cat_spec` (e.g., [data races as specified in the cat file](https://github.com/hernanponcedeleon/Dat3M/blob/master/cat/rc11.cat#L34-L39)). Default is `program_spec,cat_spec,liveness`.
 - `solver`: specifies which SMT solver to use as a backend. Since we use [JavaSMT](https://github.com/sosy-lab/java-smt), several SMT solvers are supported depending on the OS and the used SMT logic (default is Z3).
 - `method`: specifies which solving method to use. Option `lazy` (the default one) uses a customized solver for memory consistency. Option `eager` solves a monolithic formula using SMT solving. 
 

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java

@@ -67,7 +67,7 @@ public BooleanFormula getSMTVariable(Axiom ax, EncodingContext ctx) {
     // ------------------------- Static -------------------------
 
     public static EnumSet<Property> getDefault() {
-        return EnumSet.of(PROGRAM_SPEC);
+        return EnumSet.of(PROGRAM_SPEC, LIVENESS, CAT_SPEC);
     }
 
     // Used to decide the order shown by the selector in the UI

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java

@@ -104,7 +104,8 @@ public BooleanFormula encodeProperties(EnumSet<Property> properties) {
         if (specType == Property.Type.MIXED) {
             final String error = String.format(
                     "The set of properties %s are of mixed type (safety and reachability properties). " +
-                            "Cannot encode mixed properties into a single SMT-query.", properties);
+                            "Cannot encode mixed properties into a single SMT-query. Please select a different set of properties.",
+                    properties);
             throw new IllegalArgumentException(error);
         }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java

@@ -62,7 +62,7 @@ public class ThreadCreation implements ProgramProcessor {
             description = "Calling pthread_create is guaranteed to succeed.",
             secure = true,
             toUppercase = true)
-    private boolean forceStart = false;
+    private boolean forceStart = true;
 
     private final Compilation compiler;
 

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

@@ -63,7 +63,7 @@ protected Provider<Wmm> getWmmProvider() {
     }
 
     protected Provider<EnumSet<Property>> getPropertyProvider() {
-        return Provider.fromSupplier(Property::getDefault);
+        return Provider.fromSupplier(() -> EnumSet.of(Property.PROGRAM_SPEC));
     }
 
     protected Provider<Configuration> getConfigurationProvider() {

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

@@ -71,6 +71,9 @@ protected Provider<Wmm> getSourceWmmProvider() {
     protected Provider<Wmm> getTargetWmmProvider() {
         return Providers.createWmmFromArch(getTargetProvider());
     }
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.PROGRAM_SPEC));
+    }
     protected long getTimeout() { return 10000; }
     // List of tests that are known to show bugs in the compilation scheme and thus the expected result should be FAIL instead of PASS
     protected List<String> getCompilationBreakers() { return emptyList(); }
@@ -90,7 +93,7 @@ protected Provider<Configuration> getConfigurationProvider() {
     protected final Provider<Program> program2Provider = Providers.createProgramFromPath(filePathProvider);
     protected final Provider<Wmm> wmm1Provider = getSourceWmmProvider();
     protected final Provider<Wmm> wmm2Provider = getTargetWmmProvider();
-    protected final Provider<EnumSet<Property>> propertyProvider = Provider.fromSupplier(Property::getDefault);
+    protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
     protected final Provider<Configuration> configProvider = getConfigurationProvider();
     protected final Provider<VerificationTask> task1Provider = Providers.createTask(program1Provider, wmm1Provider, propertyProvider, sourceProvider, () -> 1, configProvider);
     protected final Provider<VerificationTask> task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider,  () -> 1, configProvider);

dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java

@@ -25,6 +25,7 @@
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.nio.file.Paths;
+import java.util.EnumSet;
 import java.util.List;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
@@ -99,7 +100,7 @@ public void test() {
             VerificationTask task = VerificationTask.builder()
                     .withSolverTimeout(60)
                     .withTarget(Arch.LKMM)
-                    .build(program, wmm, Property.getDefault());
+                    .build(program, wmm, EnumSet.of(Property.PROGRAM_SPEC));
             AssumeSolver s = AssumeSolver.run(ctx, prover, task);
             assertEquals(expected, s.getResult());
         } catch (Exception e) {