From a4d1226e04be2cb357788a2ee9a2bab59c2b0eba Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Thu, 10 Oct 2024 11:53:08 +0200
Subject: [PATCH] Introduce stdlib.cat

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 cat/c11-orig.cat                                          | 1 -
 cat/c11.cat                                               | 1 -
 cat/cos.cat                                               | 5 -----
 cat/imm.cat                                               | 2 --
 cat/ptx-v6.0.cat                                          | 2 --
 cat/ptx-v7.5.cat                                          | 2 --
 cat/{basic.cat => stdlib.cat}                             | 0
 cat/vmm.cat                                               | 2 --
 .../java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java  | 8 ++++++++
 9 files changed, 8 insertions(+), 15 deletions(-)
 delete mode 100644 cat/cos.cat
 rename cat/{basic.cat => stdlib.cat} (100%)

diff --git a/cat/c11-orig.cat b/cat/c11-orig.cat
index 0c99bce685..e216b2a4f0 100644
--- 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
index 31c032c097..ddd736defd 100644
--- 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
deleted file mode 100644
index d73247c001..0000000000
--- a/cat/cos.cat
+++ /dev/null
@@ -1,5 +0,0 @@
-// Herd7 uses cos.cat for generating coherence.
-// It usually also defines some derived relations used in many memory models.
-// Dartagnan does not need the former; the later is handled by basic.cat below.
-
-include "basic.cat"
\ No newline at end of file
diff --git a/cat/imm.cat b/cat/imm.cat
index ac3120310c..76a1a7d478 100644
--- 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
index 8a1b3352cb..6689a0f8e4 100644
--- 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
index de3f88f869..600f1972b6 100644
--- 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 b/cat/stdlib.cat
similarity index 100%
rename from cat/basic.cat
rename to cat/stdlib.cat
diff --git a/cat/vmm.cat b/cat/vmm.cat
index f6dd21e5ea..9170347f15 100644
--- 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
index be11ef0c07..86f6d2f1e0 100644
--- 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