Skip to content

Commit a4d1226

Browse files
Introduce stdlib.cat
Signed-off-by: Hernan Ponce de Leon <[email protected]>
1 parent 7ffb695 commit a4d1226

File tree

9 files changed

+8
-15
lines changed

9 files changed

+8
-15
lines changed

cat/c11-orig.cat

-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ Rewritten by Luc Maranget for herd7
99

1010
*)
1111

12-
include "basic.cat"
1312
include "c11_cos.cat"
1413
include "c11_los.cat"
1514

cat/c11.cat

-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Rewritten by Luc Maranget for herd7
1414
may be missing. As a consequence, reads may have no rf-edge if they read from initial memory.
1515
*)
1616

17-
include "basic.cat"
1817
include "c11_cos.cat"
1918
include "c11_los.cat"
2019

cat/cos.cat

-5
This file was deleted.

cat/imm.cat

-2
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@
88
* following GenMC's implementation
99
*)
1010

11-
include "basic.cat"
12-
1311
(* coherence *)
1412
let rs = [W];po-loc;[W] | [W];(po-loc?;rf;rmw)* (* release sequence *)
1513
(* GenMC uses the same sw definition as RC11 *)

cat/ptx-v6.0.cat

-2
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@ PTX
1212
// GPU: Graphics processing unit. The GPU scope is the set of all threads executing in the same cluster as the current thread.
1313
// SYS: System. The SYS scope is the set of all threads in the current program.
1414

15-
include "basic.cat"
16-
1715
(*******************)
1816
(* Auxiliaries *)
1917
(*******************)

cat/ptx-v7.5.cat

-2
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,6 @@ PTX
2626
// The ASPLOS'19 paper and the documentation refer to "rf | fr" (non-optional).
2727
// We follow the later.
2828

29-
include "basic.cat"
30-
3129
(*******************)
3230
(* Auxiliaries *)
3331
(*******************)
File renamed without changes.

cat/vmm.cat

-2
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,6 @@
5656
let ext = ext & ((~IW) * M)
5757
let int = int | (IW * M)
5858

59-
include "basic.cat"
60-
6159
(** Atomicity **)
6260
empty rmw & (fre;coe)
6361

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java

+8
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package com.dat3m.dartagnan.parsers.cat;
22

3+
import com.dat3m.dartagnan.GlobalSettings;
34
import com.dat3m.dartagnan.exception.AbortErrorListener;
45
import com.dat3m.dartagnan.exception.MalformedMemoryModelException;
56
import com.dat3m.dartagnan.exception.ParsingException;
@@ -62,6 +63,13 @@ public String toString() {
6263
VisitorCat(Path includePath) {
6364
this.includePath = includePath;
6465
this.wmm = new Wmm();
66+
try {
67+
// The standard library is a cat file stdlib.cat which all models include by default
68+
final CatParser parser = getParser(CharStreams.fromPath(Path.of(GlobalSettings.getCatDirectory() + "/stdlib.cat")));
69+
parser.mcm().accept(this);
70+
} catch (IOException e) {
71+
throw new ParsingException("Error parsing stdlib.cat file", e);
72+
}
6573
}
6674

6775
@Override

0 commit comments

Comments
 (0)