Introduce stdlib.cat (#751)

Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>

Author: hernanponcedeleon

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"
 

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"
 

cat/cos.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 *)

cat/imm.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   *)
 (*******************)

cat/ptx-v6.0.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   *)
 (*******************)

cat/ptx-v7.5.cat

@@ -2,7 +2,7 @@
  * Copyright (C) Huawei Technologies Co., Ltd. 2024. All rights reserved.
  * SPDX-License-Identifier: MIT
  *
- * Version 0.9.1
+ * Version 0.9.3
  */
 
 (* Notation
@@ -55,8 +55,12 @@
 
 let ext = ext & ((~IW) * M)
 let int = int | (IW * M)
-
-include "basic.cat"
+let rfe = rf & ext
+let coe = co & ext
+let fre = fr & ext
+let rfi = rf & int
+let coi = co & int
+let fri = fr & int
 
 (** Atomicity **)
 empty rmw & (fre;coe)
@@ -66,8 +70,8 @@ acyclic co | rf | fr | po-loc
 
 let Marked = RLX | ACQ | REL | SC
 let Plain = ~Marked
-let Acq = ACQ | (SC & R)
-let Rel = REL | (SC & W)
+let Acq = (ACQ | SC) & (R | F)
+let Rel = (REL | SC) & (W | F)
 
 (** Ordering **)
 (* In our model, dependencies only order stores:

cat/basic.cat renamed to cat/stdlib.cat

@@ -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,17 @@ public String toString() {
     VisitorCat(Path includePath) {
         this.includePath = includePath;
         this.wmm = new Wmm();
+        includeStdlib();
+    }
+
+    private void includeStdlib() {
+        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