Merge pull request #18 from hernanponcedeleon/2.0.3

2.0.3

.gitignore

@@ -34,3 +34,4 @@ Thumbs.db
 ##########
 dartagnan/target/
 porthos/target/
+ui/target/

Makefile

@@ -0,0 +1,20 @@
+JARPATH=$(PWD)/ui/target/ui-2.0.3-jar-with-dependencies.jar
+ICONPATH=$(PWD)/ui/src/main/resources/dat3m.png
+
+.PHONY: all install linux
+
+all: install linux
+
+install:
+	mvn install:install-file -Dfile=lib/z3-4.3.2.jar -DgroupId=com.microsoft -DartifactId="z3" -Dversion=4.3.2 -Dpackaging=jar
+	mvn clean install -DskipTests
+
+linux:
+	echo '[Desktop Entry]' > ./dat3m.desktop
+	echo 'Type=Application' >> ./dat3m.desktop
+	echo 'Name=Dat3M' >> ./dat3m.desktop
+	echo 'Comment=Dat3M' >> ./dat3m.desktop
+	echo 'Terminal=false' >> ./dat3m.desktop
+	echo 'Exec=java -jar -Djava.library.path='$(PWD)'/lib '$(JARPATH) >> ./dat3m.desktop
+	echo 'Icon='$(ICONPATH) >> ./dat3m.desktop
+	chmod +x "./dat3m.desktop" 

README.md

@@ -1,18 +1,13 @@
 # Dat3M: Memory Model Aware Verification
 
-This tool suite is currently composed of two tools.
-
-* **DARTAGNAN:** a tool to check state reachability under weak memory models.
-
 <p align="center"> 
-<img src="extras/dartagnan_small.jpg">
+<img src="ui/src/main/resources/dat3m.png">
 </p>
 
-* **PORTHOS:** a tool to check state inclusion under weak memory models.
+This tool suite is currently composed of two tools.
 
-<p align="center"> 
-<img src="extras/porthos_small.jpg">
-</p>
+* **DARTAGNAN:** a tool to check state reachability under weak memory models.
+* **PORTHOS:** a tool to check state inclusion under weak memory models.
 
 Requeriments
 ======
@@ -26,12 +21,16 @@ apt-get install maven
 Installation
 ======
 To build the tools, from the Dat3M/ directory run
+* **Linux:**
+```
+make
+```
+* **MacOS:**
 ```
 mvn install:install-file -Dfile=lib/z3-4.3.2.jar -DgroupId=com.microsoft -DartifactId="z3" -Dversion=4.3.2 -Dpackaging=jar
 mvn clean install -DskipTests
-export LD_LIBRARY_PATH=./lib/
+export DYLD_LIBRARY_PATH=./lib/
 ```
-(use DYLD_LIBRARY_PATH in MacOS)
 
 Unit Tests
 ======
@@ -42,15 +41,22 @@ mvn test
 
 Usage
 ======
+* **Linux:** You can start the tool by double-clicking the <img src="ui/src/main/resources/dat3m.png" width="30" height="30"> launcher
+* **MacOS:** To run the tool, from the Dat3M/ directory run
+```
+java -jar ui/target/ui-2.0.3-jar-with-dependencies.jar
+```
+Additionally, you can run DARTAGNAN and PORTHOS from the console.
+
 For checking reachability:
 ```
-java -jar dartagnan/target/dartagnan-2.0.2-jar-with-dependencies.jar -cat <CAT file> -i <program file> [-t <target>] [options]
+java -jar dartagnan/target/dartagnan-2.0.3-jar-with-dependencies.jar -cat <CAT file> -i <program file> [-t <target>] [options]
 ```
 For checking state inclusion:
 ```
-java -jar porthos/target/porthos-2.0.2-jar-with-dependencies.jar -s <source> -scat <CAT file> -t <target> -tcat <CAT file> -i <program file> [options]
+java -jar porthos/target/porthos-2.0.3-jar-with-dependencies.jar -s <source> -scat <CAT file> -t <target> -tcat <CAT file> -i <program file> [options]
 ```
-Dartagnan supports programs written in the .litmus or .pts formats (see below). For Porthos, programs shall be written in the .pts format since they need to be compiled to two different architectures.
+DARTAGNAN supports programs written in the .litmus or .pts formats (see below). For PORTHOS, programs shall be written in the .pts format since they need to be compiled to two different architectures.
 
 The -cat,-scat,-tcat options specify the paths to the CAT files.
 
@@ -62,10 +68,10 @@ They must be one of the following:
 - arm
 - arm8
 
-**Note:** Option target is mandatory in dartagnan when using the.pts format.
+**Note:** Option target is mandatory in DARTAGNAN when using the.pts format.
 
 Other optional arguments include:
-- -m, --mode {knastertarski, idl, kleene}: specifies the encoding for fixed points. Knaster-tarski (default mode) uses the encoding introduced in [1]. Mode idl uses the Integer Difference Logic iteration encoding introduced in [2]. Kleene mode uses the Kleene iteration encoding using one Boolean variable for each iteration step.
+- -m, --mode {knastertarski, idl, kleene}: specifies the encoding for fixed points. Knaster-tarski (default mode) uses the encoding introduced in [2]. Mode idl uses the Integer Difference Logic iteration encoding introduced in [3]. Kleene mode uses the Kleene iteration encoding using one Boolean variable for each iteration step.
 - -a, --alias {none, andersen, cfs}: specifies the alias-analysis used. Option andersen (the default one) uses a control-flow-insensitive method. Option cfs uses a control-flow-sensitive method. Option none performs no alias analysis.
 - -unroll: unrolling bound for the BMC.
 
@@ -101,12 +107,15 @@ Examples are provided in the **benchmarks/** folder.
           | ⟨expr⟩ % ⟨expr⟩ 
   ```
 
-Author and Contact
+Authors and Contact
 ======
 Dat3M is developed and maintained by [Hernán Ponce de León](mailto:ponce@fortiss.org), [Florian Furbach](mailto:f.furbach@tu-braunschweig.de) and [Natalia Gavrilenko](mailto:natalia.gavrilenko@aalto.fi). Please feel free to contact us in case of questions or to send feedback.
 
 References
 ======
-[1] Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: **BMC with Memory Models as Modules**. FMCAD 2018.
+[1] Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: **BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings**. CAV 2019.
+
+[2] Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: **BMC with Memory Models as Modules**. FMCAD 2018.
+
+[3] Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: **Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models**. SAS 2017.
 
-[2] Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: **Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models**. SAS 2017.

cat/arm.cat

@@ -32,15 +32,15 @@ let ppo = (R*W & ic) | (R*R & ii)
 (* fences *)
 (**********)
 
-let fence = isb
+let fence = ish
 
 (* happens before *)
 let hb = ppo | fence | rfe
 acyclic hb
 
 (* prop *)
 let propbase = (fence | (rfe;fence));hb*
-let prop = (W*W & propbase)| (com*;propbase*;isb;hb*)
+let prop = (W*W & propbase)| (com*;propbase*;ish;hb*)
 
 acyclic co | prop
 irreflexive fre;prop;hb*

dartagnan/pom.xml

@@ -6,7 +6,7 @@
   <parent>
     <groupId>com.dat3m</groupId>
     <artifactId>dat3m</artifactId>
-    <version>2.0.2</version>
+    <version>2.0.3</version>
   </parent>
 
   <groupId>com.dat3m.dartagnan</groupId>

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

@@ -15,6 +15,8 @@
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.apache.commons.cli.*;
 
+import java.io.File;
+import java.io.FileWriter;
 import java.io.IOException;
 import java.util.Arrays;
 
@@ -67,7 +69,7 @@ public static void main(String[] args) throws IOException {
         Mode mode = Mode.get(cmd.getOptionValue("mode"));
         Alias alias = Alias.get(cmd.getOptionValue("alias"));
 
-        Program p = new ProgramParser().parse(inputFilePath);
+        Program p = new ProgramParser().parse(new File(inputFilePath));
 
         Arch target = p.getArch();
 
@@ -85,7 +87,7 @@ public static void main(String[] args) throws IOException {
             throw new RuntimeException("Assert is required for Dartagnan tests");
         }
 
-        Wmm mcm = new ParserCat().parse(cmd.getOptionValue("cat"));
+        Wmm mcm = new ParserCat().parse(new File(cmd.getOptionValue("cat")));
 
         if(cmd.hasOption("draw")) {
             mcm.setDrawExecutionGraph();
@@ -112,13 +114,10 @@ public static void main(String[] args) throws IOException {
         System.out.println(result ? "Ok" : "No");
 
         if(cmd.hasOption("draw") && canDrawGraph(p.getAss(), result)) {
-            Graph graph = new Graph(s.getModel(), ctx);
             String outputPath = cmd.getOptionValue("draw");
+            String[] relations = cmd.hasOption("rels") ? cmd.getOptionValue("rels").split(",") : new String[0];
             ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
-            if(cmd.hasOption("rels")) {
-                graph.addRelations(Arrays.asList(cmd.getOptionValue("rels").split(",")));
-            }
-            graph.build(p).draw(outputPath);
+            drawGraph(new Graph(s.getModel(), ctx, p, relations), outputPath);
             System.out.println("Execution graph is written to " + outputPath);
         }
 
@@ -147,7 +146,7 @@ public static boolean testProgram(Solver solver, Context ctx, Program program, W
         return result;
     }
 
-    private static boolean canDrawGraph(AbstractAssert ass, boolean result){
+    public static boolean canDrawGraph(AbstractAssert ass, boolean result){
         String type = ass.getType();
         if(type == null){
             return result;
@@ -158,4 +157,11 @@ private static boolean canDrawGraph(AbstractAssert ass, boolean result){
         }
         return type.equals(AbstractAssert.ASSERT_TYPE_NOT_EXISTS) || type.equals(AbstractAssert.ASSERT_TYPE_FORALL);
     }
+
+    public static void drawGraph(Graph graph, String path) throws IOException {
+        File newTextFile = new File(path);
+        FileWriter fw = new FileWriter(newTextFile);
+        fw.write(graph.toString());
+        fw.close();
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java

@@ -3,6 +3,7 @@
 import com.dat3m.dartagnan.parsers.CatParser;
 import com.dat3m.dartagnan.parsers.CatLexer;
 import com.dat3m.dartagnan.parsers.cat.visitors.VisitorBase;
+import com.dat3m.dartagnan.parsers.program.utils.ParserErrorListener;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.antlr.v4.runtime.*;
 
@@ -12,16 +13,23 @@
 
 public class ParserCat {
 
-    public Wmm parse(String inputFilePath) throws IOException {
-        File file = new File(inputFilePath);
+    public Wmm parse(File file) throws IOException {
         FileInputStream stream = new FileInputStream(file);
-        CharStream charStream = CharStreams.fromStream(stream);
+        Wmm wmm = parse(CharStreams.fromStream(stream));
+        stream.close();
+        return wmm;
+    }
+
+    public Wmm parse(String raw) {
+        return parse(CharStreams.fromString(raw));
+    }
+
+    private Wmm parse(CharStream charStream){
         CatLexer lexer = new CatLexer(charStream);
         CommonTokenStream tokenStream = new CommonTokenStream(lexer);
-        stream.close();
 
         CatParser parser = new CatParser(tokenStream);
-        parser.setErrorHandler(new BailErrorStrategy());
+        parser.addErrorListener(new ParserErrorListener());
         ParserRuleContext parserEntryPoint = parser.mcm();
         return (Wmm) parserEntryPoint.accept(new VisitorBase());
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserInterface.java

@@ -1,10 +1,9 @@
 package com.dat3m.dartagnan.parsers.program;
 
 import com.dat3m.dartagnan.program.Program;
+import org.antlr.v4.runtime.CharStream;
 
-import java.io.IOException;
+interface ParserInterface {
 
-public interface ParserInterface {
-
-    Program parse(String inputFilePath) throws IOException;
+    Program parse(CharStream charStream);
 }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLitmusAArch64.java

@@ -10,20 +10,12 @@
 
 import org.antlr.v4.runtime.*;
 
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.IOException;
-
-public class ParserLitmusAArch64 implements ParserInterface {
+class ParserLitmusAArch64 implements ParserInterface {
 
     @Override
-    public Program parse(String inputFilePath) throws IOException {
-        File file = new File(inputFilePath);
-        FileInputStream stream = new FileInputStream(file);
-        CharStream charStream = CharStreams.fromStream(stream);
+    public Program parse(CharStream charStream) {
         LitmusAArch64Lexer lexer = new LitmusAArch64Lexer(charStream);
         CommonTokenStream tokenStream = new CommonTokenStream(lexer);
-        stream.close();
 
         LitmusAArch64Parser parser = new LitmusAArch64Parser(tokenStream);
         parser.addErrorListener(new DiagnosticErrorListener(true));
@@ -33,7 +25,6 @@ public Program parse(String inputFilePath) throws IOException {
         VisitorLitmusAArch64 visitor = new VisitorLitmusAArch64(pb);
 
         Program program = (Program) parserEntryPoint.accept(visitor);
-        program.setName(inputFilePath);
         program.setArch(Arch.ARM8);
         return program;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLitmusC.java

@@ -9,20 +9,12 @@
 
 import org.antlr.v4.runtime.*;
 
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.IOException;
-
-public class ParserLitmusC implements ParserInterface {
+class ParserLitmusC implements ParserInterface {
 
     @Override
-    public Program parse(String inputFilePath) throws IOException {
-        File file = new File(inputFilePath);
-        FileInputStream stream = new FileInputStream(file);
-        CharStream charStream = CharStreams.fromStream(stream);
+    public Program parse(CharStream charStream) {
         LitmusCLexer lexer = new LitmusCLexer(charStream);
         CommonTokenStream tokenStream = new CommonTokenStream(lexer);
-        stream.close();
 
         LitmusCParser parser = new LitmusCParser(tokenStream);
         parser.setErrorHandler(new BailErrorStrategy());
@@ -31,7 +23,6 @@ public Program parse(String inputFilePath) throws IOException {
         VisitorLitmusC visitor = new VisitorLitmusC(pb);
 
         Program program = (Program) parserEntryPoint.accept(visitor);
-        program.setName(inputFilePath);
         program.setArch(Arch.NONE);
         return program;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLitmusPPC.java

@@ -10,20 +10,12 @@
 
 import org.antlr.v4.runtime.*;
 
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.IOException;
-
-public class ParserLitmusPPC implements ParserInterface {
+class ParserLitmusPPC implements ParserInterface {
 
     @Override
-    public Program parse(String inputFilePath) throws IOException {
-        File file = new File(inputFilePath);
-        FileInputStream stream = new FileInputStream(file);
-        CharStream charStream = CharStreams.fromStream(stream);
+    public Program parse(CharStream charStream) {
         LitmusPPCLexer lexer = new LitmusPPCLexer(charStream);
         CommonTokenStream tokenStream = new CommonTokenStream(lexer);
-        stream.close();
 
         LitmusPPCParser parser = new LitmusPPCParser(tokenStream);
         parser.addErrorListener(new DiagnosticErrorListener(true));
@@ -33,7 +25,6 @@ public Program parse(String inputFilePath) throws IOException {
         VisitorLitmusPPC visitor = new VisitorLitmusPPC(pb);
 
         Program program = (Program) parserEntryPoint.accept(visitor);
-        program.setName(inputFilePath);
         program.setArch(Arch.POWER);
         return program;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLitmusX86.java

@@ -10,20 +10,12 @@
 
 import org.antlr.v4.runtime.*;
 
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.IOException;
-
-public class ParserLitmusX86 implements ParserInterface {
+class ParserLitmusX86 implements ParserInterface {
 
     @Override
-    public Program parse(String inputFilePath) throws IOException {
-        File file = new File(inputFilePath);
-        FileInputStream stream = new FileInputStream(file);
-        CharStream charStream = CharStreams.fromStream(stream);
+    public Program parse(CharStream charStream) {
         LitmusX86Lexer lexer = new LitmusX86Lexer(charStream);
         CommonTokenStream tokenStream = new CommonTokenStream(lexer);
-        stream.close();
 
         LitmusX86Parser parser = new LitmusX86Parser(tokenStream);
         parser.addErrorListener(new DiagnosticErrorListener(true));
@@ -33,7 +25,6 @@ public Program parse(String inputFilePath) throws IOException {
         VisitorLitmusX86 visitor = new VisitorLitmusX86(pb);
 
         Program program = (Program) parserEntryPoint.accept(visitor);
-        program.setName(inputFilePath);
         program.setArch(Arch.TSO);
         return program;
     }