Merge remote-tracking branch 'refs/remotes/origin/development' into a…

…lias.rebase

Dartagnan-SVCOMP.sh

@@ -1,14 +1,12 @@
 #!/bin/bash
 
-version=4.0.0
-
 if [ $# -eq 0 ]; then
     echo "No input file supplied"
     exit 0
 fi
 
 if [ $1 == "-v" ] || [ $1 == "--version" ]; then
-    echo $version
+    cmd="java -jar dartagnan/target/dartagnan.jar --version"
 else
     if [ $1 == "-witness" ]; then
         witness="--validate="$2
@@ -35,6 +33,6 @@ else
         skip_assertions_of_type=""
     fi
 
-    cmd="java -jar svcomp/target/svcomp.jar --method=assume --encoding.integers=true $skip_assertions_of_type --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness
-    $cmd
-fi
+    cmd="java -jar svcomp/target/svcomp.jar --method=eager --encoding.integers=true $skip_assertions_of_type --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness
+fi
+$cmd

dartagnan/pom.xml

@@ -5,7 +5,7 @@
     <parent>
         <groupId>com.dat3m</groupId>
         <artifactId>dat3m</artifactId>
-        <version>4.0.0</version>
+        <version>4.0.1</version>
     </parent>
     <artifactId>dartagnan</artifactId>
     <packaging>jar</packaging>
@@ -42,6 +42,11 @@
             <artifactId>log4j-core</artifactId>
             <version>${log4j.version}</version>
         </dependency>
+        <dependency>
+            <groupId>org.apache.maven</groupId>
+            <artifactId>maven-model</artifactId>
+            <version>3.3.9</version>
+        </dependency>
 
         <!-- Z3 dependency (OS independent) -->
         <dependency>

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -28,6 +28,7 @@
 import com.google.common.collect.ImmutableSet;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.apache.maven.model.io.xpp3.MavenXpp3Reader;
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -41,6 +42,7 @@
 import org.sosy_lab.java_smt.api.SolverException;
 
 import java.io.File;
+import java.io.FileReader;
 import java.math.BigInteger;
 import java.util.*;
 
@@ -51,7 +53,7 @@
 import static com.dat3m.dartagnan.configuration.OptionNames.TARGET;
 import static com.dat3m.dartagnan.configuration.Property.*;
 import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*;
-import static com.dat3m.dartagnan.utils.GitInfo.CreateGitInfo;
+import static com.dat3m.dartagnan.utils.GitInfo.*;
 import static com.dat3m.dartagnan.utils.Result.*;
 import static com.dat3m.dartagnan.utils.visualization.ExecutionGraphVisualizer.generateGraphvizFile;
 import static java.lang.Boolean.FALSE;
@@ -72,12 +74,22 @@ private Dartagnan(Configuration config) throws InvalidConfigurationException {
 
     public static void main(String[] args) throws Exception {
 
+        initGitInfo();
+
         if (Arrays.asList(args).contains("--help")) {
             collectOptions();
             return;
         }
 
-        CreateGitInfo();
+        if (Arrays.asList(args).contains("--version")) {
+            final MavenXpp3Reader mvnReader = new MavenXpp3Reader();
+            final FileReader fileReader = new FileReader(System.getenv("DAT3M_HOME") + "/pom.xml");
+            final String version = String.format("%s (commit %s)", mvnReader.read(fileReader).getVersion(), getGitId());
+            System.out.println(version);
+            return;
+        }
+
+        logGitInfo();
 
         String[] argKeyword = Arrays.stream(args)
                 .filter(s -> s.startsWith("-"))

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java

@@ -25,9 +25,11 @@
 import static com.dat3m.dartagnan.GlobalSettings.REFINEMENT_SYMMETRIC_LEARNING;
 import static com.dat3m.dartagnan.wmm.RelationNameRepository.*;
 
-// The CoreReasoner transforms base reasons of the CAATSolver to core reason of the WMMSolver.
+// The CoreReasoner transforms base reasons of the CAATSolver to core reasons of the WMMSolver.
 public class CoreReasoner {
 
+    // An upper bound on the number of reasons computed per iteration,
+    // This is mostly used to limit "reason explosion" for highly symmetric benchmarks.
     private final static int MAX_NUM_COMPUTED_REASONS = 1000;
 
     public enum SymmetricLearning { NONE, FULL }
@@ -61,7 +63,8 @@ public Set<Conjunction<CoreLiteral>> toCoreReasons(DNF<CAATLiteral> baseReasons)
                 HashBiMap.create(baseReasons.getNumberOfCubes());
         for (Conjunction<CAATLiteral> baseReason : baseReasons.getCubes()) {
             final Conjunction<CoreLiteral> coreReason = toCoreReasonNoSymmetry(baseReason);
-            if (!base2core.containsValue(coreReason)) {
+            if (!coreReason.isFalse() && !base2core.containsValue(coreReason)) {
+                // NOTE: We only add productive base reasons whose core reasons are not FALSE.
                 base2core.put(baseReason, coreReason);
             }
         }
@@ -108,11 +111,12 @@ public Set<Conjunction<CoreLiteral>> toCoreReasons(Conjunction<CAATLiteral> base
         }
 
         // Now we can reduce all computed (symmetric) reasons.
-        return orbit.stream().map(this::reduce).map(Conjunction::new).collect(Collectors.toSet());
+        return orbit.stream().map(this::reduce).filter(Objects::nonNull).map(Conjunction::new).collect(Collectors.toSet());
     }
 
     private Conjunction<CoreLiteral> toCoreReasonNoSymmetry(Conjunction<CAATLiteral> baseReason) {
-        return new Conjunction<>(reduce(toUnreducedCoreReason(baseReason, executionGraph.getDomain())));
+        List<CoreLiteral> reduced = reduce(toUnreducedCoreReason(baseReason, executionGraph.getDomain()));
+        return reduced == null ? Conjunction.FALSE() : new Conjunction<>(reduced);
     }
 
     private List<CoreLiteral> getPermuted(List<CoreLiteral> reason, Function<Event, Event> perm) {
@@ -156,6 +160,7 @@ private List<CoreLiteral> toUnreducedCoreReason(Conjunction<CAATLiteral> baseRea
 
     // Reduce a core reason by applying knowledge about the semantics of its literals
     // (relation analysis / base semantics / control-flow information etc.)
+    // This may return NULL, if our knowledge tells us that this is impossible to happen.
     private List<CoreLiteral> reduce(List<CoreLiteral> reason) {
         final List<CoreLiteral> simplified = new ArrayList<>();
         for (CoreLiteral lit : reason) {
@@ -165,18 +170,27 @@ private List<CoreLiteral> reduce(List<CoreLiteral> reason) {
                 final Event e1 = relLiteral.getSource();
                 final Event e2 = relLiteral.getTarget();
                 final Relation rel = relLiteral.getRelation();
-                if (relLiteral.isPositive() && ra.getKnowledge(rel).getMustSet().contains(e1, e2)) {
+                final RelationAnalysis.Knowledge k = ra.getKnowledge(rel);
+
+                if (relLiteral.isPositive() && k.getMustSet().contains(e1, e2)) {
                     addExecReason(e1, e2, simplified);
-                } else if (relLiteral.isNegative() && !ra.getKnowledge(rel).getMaySet().contains(e1, e2)) {
-                    // Negated literal is always true, no need to remember it.
+                } else if (!k.getMaySet().contains(e1, e2)) {
+                    if (lit.isPositive()) {
+                        // Positive literal is never true, so the whole reason is impossible.
+                        // We return NULL to indicate this.
+                        return null;
+                    } else {
+                        // Negated literal is always true, no need to remember it / do anything.
+                    }
                 } else {
-                    String name = rel.getName().orElse(null);
+                    final String name = rel.getName().orElse(null);
                     if (RF.equals(name) || CO.equals(name) || executionGraph.getCutRelations().contains(rel)) {
                         simplified.add(lit);
                     } else if (LOC.equals(name)) {
                         simplified.add(new AddressLiteral(e1, e2, lit.isPositive()));
                     } else {
-                        throw new UnsupportedOperationException(String.format("Literals of type %s are not supported.", rel));
+                        final String errorMsg = String.format("Literals of type %s are not supported.", rel);
+                        throw new UnsupportedOperationException(errorMsg);
                     }
                 }
             }
@@ -221,6 +235,7 @@ private void addExecReason(Event e1, Event e2, List<CoreLiteral> coreReasons) {
     // =============================================================================================
 
     // Computes a list of generators for the symmetry group of threads.
+    // NOTE We always add the identity as generator, although it is unnecessary.
     private List<Function<Event, Event>> computeSymmetryGenerators(
             ThreadSymmetry symm, SymmetricLearning learningOption) {
         final Set<? extends EquivalenceClass<Thread>> symmClasses = symm.getNonTrivialClasses();

dartagnan/src/main/java/com/dat3m/dartagnan/utils/GitInfo.java

@@ -11,19 +11,28 @@
 
 public class GitInfo {
 
-	private static final Logger logger = LogManager.getLogger(Dartagnan.class);  
+    private static final Logger logger = LogManager.getLogger(GitInfo.class);
 
-	static Properties properties = new Properties();
-	
-	public static void CreateGitInfo() throws IOException {
-       try (InputStream is = Dartagnan.class.getClassLoader()
+    static Properties properties = new Properties();
+
+    public static void initGitInfo() throws IOException {
+        try (InputStream is = Dartagnan.class.getClassLoader()
                 .getResourceAsStream("git.properties")) {
-		   if (is == null) {
-			   return;
-		   }
-		   properties.load(is);
-		   logger.info("Git branch: " + properties.getProperty("git.branch"));
-		   logger.info("Git commit ID: " + properties.getProperty("git.commit.id"));
+            if (is == null) {
+                logger.warn("Failed to load git.properties");
+                return;
+            }
+            properties.load(is);
         }
-	}	
+    }
+
+    public static void logGitInfo() {
+        logger.info("Git branch: " + properties.getProperty("git.branch", "unknown"));
+        logger.info("Git commit ID: " + properties.getProperty("git.commit.id", "unknown"));
+    }
+
+    public static String getGitId() {
+        return properties.getProperty("git.commit.id", "unknown");
+    }
+
 }