Cleanup vulkan parser (#787)

hernanponcedeleon · Nov 25, 2024 · 39dd3a1 · 39dd3a1
1 parent 21f6e90
commit 39dd3a1
Show file tree

Hide file tree

Showing 65 changed files with 740 additions and 2,599 deletions.
diff --git a/dartagnan/src/main/antlr4/LitmusVulkan.g4 b/dartagnan/src/main/antlr4/LitmusVulkan.g4
@@ -83,8 +83,12 @@ queuefamilyScope
     :   Queuefamily scopeID
     ;
 
+scopeID returns [int id]
+    :   t = DigitSequence {$id = Integer.parseInt($t.text);}
+    ;
+
 instructionList
-    :   (instructionRow) +
+    :   instructionRow+
     ;
 
 instructionRow
@@ -95,94 +99,67 @@ instruction
     :
     |   storeInstruction
     |   loadInstruction
-    |   rmwInstruction
-    |   fenceInstruction
+    |   atomicStoreInstruction
+    |   atomicLoadInstruction
+    |   atomicRmwInstruction
+    |   memoryBarrierInstruction
+    |   controlBarrierInstruction
+    |   localInstruction
+    |   labelInstruction
+    |   jumpInstruction
+    |   condJumpInstruction
     |   deviceOperation
-    |   label
-    |   branchCond
-    |   jump
     ;
 
 storeInstruction
-    :   Store atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList location Comma value
+    :   Store (nonpriv | (av scope))? sc location Comma value
     ;
 
 loadInstruction
-    :   localValue
-    |   localAdd
-    |   localSub
-    |   localMul
-    |   localDiv
-    |   loadLocation
-    ;
-
-localValue
-    :   Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma value
+    :   Load (nonpriv | (vis scope))? sc register Comma location
     ;
 
-localAdd
-    :   Add register Comma value Comma value
+atomicStoreInstruction
+    :   Store Period Atom (scope sc | moRel scope sc semSc+ semAv?) location Comma value
     ;
 
-localSub
-    :   Sub register Comma value Comma value
+atomicLoadInstruction
+    :   Load Period Atom (scope sc | moAcq scope sc semSc+ semVis?) register Comma location
     ;
 
-localMul
-    :   Mul register Comma value Comma value
+atomicRmwInstruction
+    :   RMW Period Atom (scope sc | moAcq scope sc semSc+ semVis? | moRel scope sc semSc+ semAv? | moAcqRel scope sc semSc+ semAv? semVis?) (Period operation)? register Comma location Comma value
     ;
 
-localDiv
-    :   Div register Comma value Comma value
+memoryBarrierInstruction
+    :   MemoryBarrier (moAcq scope semSc+ semVis? | moRel scope semSc+ semAv? | moAcqRel scope semSc+ semAv? semVis?)
     ;
 
-loadLocation
-    :   Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location
+controlBarrierInstruction
+    :   ControlBarrier (scope | moAcq scope semSc+ semVis? | moRel scope semSc+ semAv? | moAcqRel scope semSc+ semAv? semVis?) value
     ;
 
-rmwInstruction
-    :   rmwValue
-    |   rmwOp
+localInstruction
+    :   operation register Comma value Comma value
     ;
 
-rmwValue
-    :   RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location Comma value
-    ;
-
-rmwOp
-    :   RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList operation register Comma location Comma value
-    ;
-
-fenceInstruction
-    :   memoryBarrier
-    |   controlBarrier
+labelInstruction
+    :   Label Colon
     ;
 
-memoryBarrier
-    :   MemoryBarrier mo? avvis? scope? storageClassSemanticList avvisSemanticList
+jumpInstruction
+    :   Goto Label
     ;
 
-controlBarrier
-    :   ControlBarrier mo? avvis? scope? storageClassSemanticList avvisSemanticList value
+condJumpInstruction
+    :   cond value Comma value Comma Label
     ;
 
 deviceOperation
     :   AVDEVICE
     |   VISDEVICE
     ;
 
-label
-    :   Label Colon
-    ;
-
-branchCond
-    :   cond value Comma value Comma Label
-    ;
-
-jump
-    :   Goto Label
-    ;
-
 value
     :   constant
     |   register
@@ -202,65 +179,63 @@ assertionValue
     |   constant
     ;
 
-atomic returns [Boolean isAtomic]
-    :   Period Atom {$isAtomic = true;}
-    |   {$isAtomic = false;}
+moAcq
+    :   Period Acquire
     ;
 
-scope returns [String content]
-    :   Period Subgroup {$content = "SG";}
-    |   Period Workgroup {$content = "WG";}
-    |   Period Queuefamily {$content = "QF";}
-    |   Period Device {$content = "DV";}
-    |   Period Nonprivate {$content = "NONPRIV";}
+moRel
+    :   Period Release
     ;
 
-scopeID returns [int id]
-    :   t = DigitSequence {$id = Integer.parseInt($t.text);}
+moAcqRel
+    :   Period Acq_rel
     ;
 
-mo returns [String content]
-    :   Period Acquire {$content = "ACQ";}
-    |   Period Release {$content = "REL";}
-    |   Period Acq_rel {$content = "ACQ_REL";}
+nonpriv
+    :   Period Nonprivate
     ;
 
-avvis returns [String content]
-    :   Period Visible {$content = "VIS";}
-    |   Period Available {$content = "AV";}
+av
+    :   Period Available
     ;
 
-storageClass returns [String content]
-    :   Period Sc0 {$content = "SC0";}
-    |   Period Sc1 {$content = "SC1";}
+vis
+    :   Period Visible
     ;
 
-storageClassSemantic returns [String content]
-    :   Period Semsc0 {$content = "SEMSC0";}
-    |   Period Semsc1 {$content = "SEMSC1";}
+semAv
+    :   Period SemAv
     ;
 
-storageClassSemanticList
-    :   (storageClassSemantic)*
+semVis
+    :   Period SemVis
     ;
 
-avvisSemantic returns [String content]
-    :   Period SemVis {$content = "SEMVIS";}
-    |   Period SemAv {$content = "SEMAV";}
+scope returns [String content]
+    :   Period Subgroup {$content = "SG";}
+    |   Period Workgroup {$content = "WG";}
+    |   Period Queuefamily {$content = "QF";}
+    |   Period Device {$content = "DV";}
     ;
 
-avvisSemanticList
-    :   (avvisSemantic)*
+sc returns [String content]
+    :   Period Sc0 {$content = "SC0";}
+    |   Period Sc1 {$content = "SC1";}
+    ;
+
+semSc returns [String content]
+    :   Period Semsc0 {$content = "SEMSC0";}
+    |   Period Semsc1 {$content = "SEMSC1";}
     ;
 
 operation locals [IntBinaryOp op]
-    :   Period Add {$op = IntBinaryOp.ADD;}
-    |   Period Sub {$op = IntBinaryOp.SUB;}
-    |   Period Mul {$op = IntBinaryOp.MUL;}
-    |   Period Div {$op = IntBinaryOp.DIV;}
-    |   Period And {$op = IntBinaryOp.AND;}
-    |   Period Or {$op = IntBinaryOp.OR;}
-    |   Period Xor {$op = IntBinaryOp.XOR;}
+    :   Add {$op = IntBinaryOp.ADD;}
+    |   Sub {$op = IntBinaryOp.SUB;}
+    |   Mul {$op = IntBinaryOp.MUL;}
+    |   Div {$op = IntBinaryOp.DIV;}
+    |   And {$op = IntBinaryOp.AND;}
+    |   Or {$op = IntBinaryOp.OR;}
+    |   Xor {$op = IntBinaryOp.XOR;}
     ;
 
 cond returns [IntCmpOp op]

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/exception/AbortErrorListener.java b/dartagnan/src/main/java/com/dat3m/dartagnan/exception/AbortErrorListener.java
@@ -15,6 +15,6 @@ public void syntaxError(
             String msg,
             RecognitionException e
     ) throws ParsingException {
-        throw new ParsingException("Line " + line + ":" + charPositionInLine + " " + msg);
+        throw new ParsingException(e, "Line " + line + ":" + charPositionInLine + " " + msg);
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/exception/ParsingException.java b/dartagnan/src/main/java/com/dat3m/dartagnan/exception/ParsingException.java
@@ -7,6 +7,10 @@ public ParsingException(String msg){
     }
 
     public ParsingException(String format, Object... args){
-        this(String.format(format, args));
+        super(String.format(format, args));
+    }
+
+    public ParsingException(Throwable cause, String format, Object... args){
+        super(String.format(format, args), cause);
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java
@@ -72,7 +72,7 @@ private void includeStdlib() {
             final CatParser parser = getParser(CharStreams.fromPath(Path.of(GlobalSettings.getCatDirectory() + "/stdlib.cat")));
             parser.mcm().accept(this);
         } catch (IOException e) {
-            throw new ParsingException("Error parsing stdlib.cat file", e);
+            throw new ParsingException(e, "Error parsing stdlib.cat file");
         }
     }
 
@@ -107,7 +107,7 @@ public Object visitInclude(IncludeContext ctx) {
             final CatParser parser = getParser(CharStreams.fromPath(filePath));
             return parser.mcm().accept(this);
         } catch (IOException e) {
-            throw new ParsingException(String.format("Error parsing file '%s'", filePath), e);
+            throw new ParsingException(e, String.format("Error parsing file '%s'", filePath));
         }
     }