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