Introduce stdlib.cat

Signed-off-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Oct 10, 2024 · a4d1226 · a4d1226
1 parent 7ffb695
commit a4d1226
Show file tree

Hide file tree

Showing 9 changed files with 8 additions and 15 deletions.
diff --git a/cat/c11-orig.cat b/cat/c11-orig.cat
@@ -9,7 +9,6 @@ Rewritten by Luc Maranget for herd7
 
 *)
 
-include "basic.cat"
 include "c11_cos.cat"
 include "c11_los.cat"
 

diff --git a/cat/c11.cat b/cat/c11.cat
@@ -14,7 +14,6 @@ Rewritten by Luc Maranget for herd7
    may be missing. As a consequence, reads may have no rf-edge if they read from initial memory.
 *)
 
-include "basic.cat"
 include "c11_cos.cat"
 include "c11_los.cat"
 

diff --git a/cat/cos.cat b/cat/cos.cat
diff --git a/cat/imm.cat b/cat/imm.cat
@@ -8,8 +8,6 @@
  * following GenMC's implementation
  *)
 
-include "basic.cat"
-
 (* coherence *)
 let rs = [W];po-loc;[W] | [W];(po-loc?;rf;rmw)*                                                                                     (* release sequence *)
 (* GenMC uses the same sw definition as RC11 *)

diff --git a/cat/ptx-v6.0.cat b/cat/ptx-v6.0.cat
@@ -12,8 +12,6 @@ PTX
 // GPU: Graphics processing unit. The GPU scope is the set of all threads executing in the same cluster as the current thread.
 // SYS: System. The SYS scope is the set of all threads in the current program.
 
-include "basic.cat"
-
 (*******************)
 (*   Auxiliaries   *)
 (*******************)

diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat
@@ -26,8 +26,6 @@ PTX
 // The ASPLOS'19 paper and the documentation refer to "rf | fr" (non-optional). 
 // We follow the later.
 
-include "basic.cat"
-
 (*******************)
 (*   Auxiliaries   *)
 (*******************)

diff --git a/cat/basic.cat → cat/stdlib.cat b/cat/basic.cat → cat/stdlib.cat
diff --git a/cat/vmm.cat b/cat/vmm.cat
@@ -56,8 +56,6 @@
 let ext = ext & ((~IW) * M)
 let int = int | (IW * M)
 
-include "basic.cat"
-
 (** Atomicity **)
 empty rmw & (fre;coe)
 

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
@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.parsers.cat;
 
+import com.dat3m.dartagnan.GlobalSettings;
 import com.dat3m.dartagnan.exception.AbortErrorListener;
 import com.dat3m.dartagnan.exception.MalformedMemoryModelException;
 import com.dat3m.dartagnan.exception.ParsingException;
@@ -62,6 +63,13 @@ public String toString() {
     VisitorCat(Path includePath) {
         this.includePath = includePath;
         this.wmm = new Wmm();
+        try {
+            // The standard library is a cat file stdlib.cat which all models include by default
+            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);
+        }
     }
 
     @Override
-Original file line number
+Diff line change
@@ Expand Up / @@ -9,7 +9,6 @@ Rewritten by Luc Maranget for herd7 @@
     *)
-    include "basic.cat"
     include "c11_cos.cat"
     include "c11_los.cat"
@@ Expand Down @@