Updated CAT grammar to correctly parse LKMM.

Commented out includes in LKMM because the included file contains unsupported features.
hernanponcedeleon · Sep 12, 2024 · dec62f9 · dec62f9
1 parent ef8a507
commit dec62f9
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 14 deletions.
diff --git a/cat/linux-kernel.cat b/cat/linux-kernel.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*

diff --git a/cat/lkmm/lkmm-v00.cat b/cat/lkmm/lkmm-v00.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

diff --git a/cat/lkmm/lkmm-v01.cat b/cat/lkmm/lkmm-v01.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

diff --git a/cat/lkmm/lkmm-v02.cat b/cat/lkmm/lkmm-v02.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4
@@ -5,12 +5,11 @@ import com.dat3m.dartagnan.wmm.axiom.*;
 }
 
 mcm
-    :   (NAME)? definition+ EOF
+    :   (NAME| QUOTED_STRING)? (definition | include)+ EOF
     ;
 
 definition
-    :   include
-    |   axiomDefinition
+    :   axiomDefinition
     |   letDefinition
     |   letRecDefinition
     ;
@@ -91,10 +90,10 @@ NEW         :   'new';
 
 FLAG       :   'flag';
 
-NAME    : [A-Za-z0-9\-_.]+;
-
 QUOTED_STRING : '"' .*? '"';
 
+NAME    : [A-Za-z0-9\-_.]+;
+
 LINE_COMMENT
     :   '//' ~[\n]*
         -> skip
@@ -109,8 +108,3 @@ WS
     :   [ \t\r\n]+
         -> skip
     ;
-
-MODELNAME
-    :   '"' .*? '"'
-        -> skip
-    ;