Spir-V parser

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusAArch64 visitor = new VisitorLitmusAArch64();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -21,9 +21,8 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusC visitor = new VisitorLitmusC();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
         // C programs can be compiled to different targets,
         // thus we don't set the architectures.
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusLISA visitor = new VisitorLitmusLISA();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusPPC visitor = new VisitorLitmusPPC();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusPTX visitor = new VisitorLitmusPTX();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusRISCV visitor = new VisitorLitmusRISCV();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusVulkan visitor = new VisitorLitmusVulkan();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -23,7 +23,6 @@ public Program parse(CharStream charStream) {
         ParserRuleContext parserEntryPoint = parser.main();
         VisitorLitmusX86 visitor = new VisitorLitmusX86();
 
-        Program program = (Program) parserEntryPoint.accept(visitor);
-        return program;
+        return (Program) parserEntryPoint.accept(visitor);
     }
 }

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

@@ -0,0 +1,28 @@
+package com.dat3m.dartagnan.parsers.program;
+
+import com.dat3m.dartagnan.exception.ParserErrorListener;
+import com.dat3m.dartagnan.parsers.*;
+import com.dat3m.dartagnan.parsers.program.visitors.VisitorSpirv;
+import com.dat3m.dartagnan.program.Program;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.DiagnosticErrorListener;
+import org.antlr.v4.runtime.ParserRuleContext;
+
+public class ParserSpirv implements ParserInterface {
+
+    @Override
+    public Program parse(CharStream charStream) {
+        SpirvLexer lexer = new SpirvLexer(charStream);
+        CommonTokenStream tokenStream = new CommonTokenStream(lexer);
+
+        SpirvParser parser = new SpirvParser(tokenStream);
+        parser.addErrorListener(new DiagnosticErrorListener(true));
+        parser.addErrorListener(new ParserErrorListener());
+        ParserRuleContext parserEntryPoint = parser.spv();
+        VisitorSpirv visitor = new VisitorSpirv();
+
+        parserEntryPoint.accept(visitor);
+        return visitor.buildProgram();
+    }
+}

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

@@ -17,7 +17,7 @@ public class ProgramParser {
     private static final String TYPE_LITMUS_RISCV = "RISCV";
     private static final String TYPE_LITMUS_X86 = "X86";
     private static final String TYPE_LITMUS_PTX = "PTX";
-    private static final String TYPE_LITMUS_VULKAN      = "VULKAN";
+    private static final String TYPE_LITMUS_VULKAN = "VULKAN";
     private static final String TYPE_LITMUS_LISA = "LISA";
     private static final String TYPE_LITMUS_C = "C";
 
@@ -71,12 +71,14 @@ public Program parse(String raw, String path, String format, String cflags) thro
 
     private ParserInterface getConcreteParser(File file) throws IOException {
         String name = file.getName();
-        String format = name.substring(name.lastIndexOf(".") + 1);
-        switch (format) {
-            case "ll":
-                return new ParserLlvm();
-            case "litmus":
-                return getConcreteLitmusParser(readFirstLine(file).toUpperCase());
+        if (name.endsWith(".ll")) {
+            return new ParserLlvm();
+        }
+        if (name.endsWith(".spv.dis")) {
+            return new ParserSpirv();
+        }
+        if (name.endsWith(".litmus")) {
+            return getConcreteLitmusParser(readFirstLine(file).toUpperCase());
         }
         throw new ParsingException("Unknown input file type");
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorSpirv.java

@@ -0,0 +1,14 @@
+package com.dat3m.dartagnan.parsers.program.visitors;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.parsers.SpirvBaseVisitor;
+import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder;
+import com.dat3m.dartagnan.program.Program;
+
+public class VisitorSpirv extends SpirvBaseVisitor<Expression> {
+
+    private final ProgramBuilder programBuilder = ProgramBuilder.forLanguage(Program.SourceLanguage.SPV);
+    public Program buildProgram() {
+        return programBuilder.build();
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java

@@ -12,7 +12,7 @@
 
 public class Program {
 
-    public enum SourceLanguage { LITMUS, LLVM }
+    public enum SourceLanguage { LITMUS, LLVM, SPV }
 
     private String name;
     private AbstractAssert spec;

dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/ParserSpirvTest.java

@@ -0,0 +1,54 @@
+package com.dat3m.dartagnan.parsers.program;
+
+import com.dat3m.dartagnan.program.Program;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CharStreams;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.stream.Stream;
+
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
+import static org.junit.Assert.assertNotNull;
+
+@RunWith(Parameterized.class)
+public class ParserSpirvTest {
+
+    private static final String PATH = "parsers/program/spirv/";
+
+    private final String filename;
+
+    public ParserSpirvTest(String filename) {
+        this.filename = filename;
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}")
+    public static Iterable<Object[]> data() throws IOException {
+        String path = Paths.get(getTestResourcePath(PATH)).toString();
+        File dir = new File(path);
+        File[] files = dir.listFiles();
+        assertNotNull(files);
+        return Stream.of(files)
+                .filter(file -> !file.isDirectory())
+                .map(f -> new Object[]{f.getName()})
+                .toList();
+    }
+
+    @Test
+    public void testParsingFile() throws IOException {
+        Program program;
+        Path path = Paths.get(getTestResourcePath(PATH + filename));
+        try (FileInputStream stream = new FileInputStream(path.toString())) {
+            CharStream charStream = CharStreams.fromStream(stream);
+            ParserSpirv parser = new ParserSpirv();
+            program = parser.parse(charStream);
+        }
+        assertNotNull(program);
+    }
+}