Added support for includes and functions in cat

cat/aarch64.cat

@@ -49,7 +49,7 @@ include "cos.cat"
 (*
  * Include aarch64fences.cat so that barriers show up in generated diagrams.
  *)
-include "aarch64fences.cat"
+//include "aarch64fences.cat"
 
 (*
  * As a restriction of the model, all observers are limited to the same

cat/linux-kernel.cat

@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*

cat/lkmm/lkmm-v00.cat

@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

cat/lkmm/lkmm-v01.cat

@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

cat/lkmm/lkmm-v02.cat

@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |

dartagnan/src/main/antlr4/Cat.g4

@@ -5,11 +5,12 @@ import com.dat3m.dartagnan.wmm.axiom.*;
 }
 
 mcm
-    :   (NAME)? definition+ EOF
+    :   (NAME)? (QUOTED_STRING)? (definition | include)+ EOF
     ;
 
 definition
     :   axiomDefinition
+    |   letFuncDefinition
     |   letDefinition
     |   letRecDefinition
     ;
@@ -20,6 +21,10 @@ axiomDefinition locals [Class<?> cls]
     |   (flag = FLAG)? (negate = NOT)? EMPTY { $cls = Emptiness.class; } e = expression (AS NAME)?
     ;
 
+letFuncDefinition
+    :   LET (fname = NAME) LPAR params = parameterList RPAR EQ e = expression
+    ;
+
 letDefinition
     :   LET n = NAME EQ e = expression
     ;
@@ -50,6 +55,19 @@ expression
     |   LPAR e = expression RPAR                                        # expr
     |   n = NAME                                                        # exprBasic
     |   call = NEW LPAR RPAR                                            # exprNew
+    |   call = NAME LPAR args = argumentList RPAR                       # exprCall
+    ;
+
+include
+    :   'include' path = QUOTED_STRING
+    ;
+
+parameterList
+    : (NAME (COMMA NAME)*)
+    ;
+
+argumentList
+    : expression (COMMA expression)*
     ;
 
 LET     :   'let';
@@ -78,6 +96,7 @@ LPAR    :   '(';
 RPAR    :   ')';
 LBRAC   :   '[';
 RBRAC   :   ']';
+COMMA   :   ',';
 
 FENCEREL    :   'fencerel';
 DOMAIN      :   'domain';
@@ -86,6 +105,8 @@ NEW         :   'new';
 
 FLAG       :   'flag';
 
+QUOTED_STRING : '"' .*? '"';
+
 NAME    : [A-Za-z0-9\-_.]+;
 
 LINE_COMMENT
@@ -102,13 +123,3 @@ WS
     :   [ \t\r\n]+
         -> skip
     ;
-
-INCLUDE
-    :   'include "' .*? '"'
-        -> skip
-    ;
-
-MODELNAME
-    :   '"' .*? '"'
-        -> skip
-    ;

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -52,6 +52,7 @@
 import java.io.FileReader;
 import java.io.IOException;
 import java.math.BigInteger;
+import java.nio.file.Path;
 import java.util.*;
 
 import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory;
@@ -112,19 +113,20 @@ public static void main(String[] args) throws Exception {
         File fileProgram = new File(Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith))
                 .findFirst()
                 .orElseThrow(() -> new IllegalArgumentException("Input program not given or format not recognized")));
-        logger.info("Program path: " + fileProgram);
+        logger.info("Program path: {}", fileProgram);
 
         File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst()
                 .orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized")));
-        logger.info("CAT file path: " + fileModel);
+        logger.info("CAT file path: {}", fileModel);
 
-        Wmm mcm = new ParserCat().parse(fileModel);
+
+        Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(fileModel);
         Program p = new ProgramParser().parse(fileProgram);
         EnumSet<Property> properties = o.getProperty();
 
         WitnessGraph witness = new WitnessGraph();
         if (o.runValidator()) {
-            logger.info("Witness path: " + o.getWitnessPath());
+            logger.info("Witness path: {}", o.getWitnessPath());
             witness = new ParserWitness().parse(new File(o.getWitnessPath()));
         }
 
@@ -165,8 +167,7 @@ public static void main(String[] args) throws Exception {
                     sdm.getNotifier(),
                     o.getSolver());
                     ProverWithTracker prover = new ProverWithTracker(ctx,
-                        o.getDumpSmtLib() ?
-                            System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "",
+                        o.getDumpSmtLib() ? GlobalSettings.getOutputDirectory() + String.format("/%s.smt2", p.getName()) : "",
                         ProverOptions.GENERATE_MODELS)) {
                 ModelChecker modelChecker;
                 if (properties.contains(DATARACEFREEDOM)) {

dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java

@@ -59,6 +59,12 @@ public static String getHomeDirectory() {
         return env;
     }
 
+    public static String getCatDirectory() {
+        String env = System.getenv("DAT3M_HOME");
+        env = env == null ? "" : env;
+        return env + "/cat";
+    }
+
     public static String getOrCreateOutputDirectory() throws IOException {
         String path = getOutputDirectory();
         Files.createDirectories(Paths.get(path));

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java

@@ -13,6 +13,7 @@ public class OptionNames {
     public static final String COVERAGE = "coverage";
     public static final String WITNESS = "witness";
     public static final String SMTLIB2 = "smtlib2";
+    public static final String CAT_INCLUDE = "cat.include";
 
     // Modeling Options
     public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";

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

@@ -1,17 +1,29 @@
 package com.dat3m.dartagnan.parsers.cat;
 
+import com.dat3m.dartagnan.GlobalSettings;
+import com.dat3m.dartagnan.exception.AbortErrorListener;
 import com.dat3m.dartagnan.parsers.CatLexer;
 import com.dat3m.dartagnan.parsers.CatParser;
-import com.dat3m.dartagnan.exception.AbortErrorListener;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.antlr.v4.runtime.*;
 
 import java.io.File;
 import java.io.FileInputStream;
 import java.io.IOException;
+import java.nio.file.Path;
 
 public class ParserCat {
 
+    private final Path includePath;
+
+    public ParserCat() {
+        includePath = Path.of(GlobalSettings.getCatDirectory());
+    }
+
+    public ParserCat(Path includePath) {
+        this.includePath = includePath;
+    }
+
     public Wmm parse(File file) throws IOException {
         try (FileInputStream stream = new FileInputStream(file)) {
             return parse(CharStreams.fromStream(stream));
@@ -32,6 +44,6 @@ private Wmm parse(CharStream charStream){
         parser.addErrorListener(new AbortErrorListener());
         parser.addErrorListener(new DiagnosticErrorListener(true));
         ParserRuleContext parserEntryPoint = parser.mcm();
-        return (Wmm) parserEntryPoint.accept(new VisitorBase());
+        return (Wmm) parserEntryPoint.accept(new VisitorCat(includePath));
     }
 }

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

@@ -1,8 +1,11 @@
 package com.dat3m.dartagnan.parsers.cat;
 
+import com.dat3m.dartagnan.exception.AbortErrorListener;
 import com.dat3m.dartagnan.exception.MalformedMemoryModelException;
 import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.parsers.CatBaseVisitor;
+import com.dat3m.dartagnan.parsers.CatLexer;
+import com.dat3m.dartagnan.parsers.CatParser;
 import com.dat3m.dartagnan.parsers.CatParser.*;
 import com.dat3m.dartagnan.program.filter.Filter;
 import com.dat3m.dartagnan.wmm.Definition;
@@ -11,39 +14,92 @@
 import com.dat3m.dartagnan.wmm.Wmm;
 import com.dat3m.dartagnan.wmm.axiom.Axiom;
 import com.dat3m.dartagnan.wmm.definition.*;
+import com.google.common.collect.ImmutableMap;
+import org.antlr.v4.runtime.*;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 
+import java.io.IOException;
 import java.lang.reflect.Constructor;
 import java.lang.reflect.InvocationTargetException;
-import java.util.Arrays;
-import java.util.HashMap;
-import java.util.Map;
-import java.util.Optional;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.*;
+import java.util.stream.Collectors;
 
 import static com.dat3m.dartagnan.program.event.Tag.VISIBLE;
 import static com.dat3m.dartagnan.wmm.RelationNameRepository.ID;
 
-class VisitorBase extends CatBaseVisitor<Object> {
+class VisitorCat extends CatBaseVisitor<Object> {
+
+    private static final Logger logger = LogManager.getLogger(VisitorCat.class);
+
+    // The directory path used to resolve include statements.
+    private final Path includePath;
 
     private final Wmm wmm;
-    // Maps names used on the lhs of definitions ("let name = relexpr") to the
-    // predicate they identify (either a Relation or a Filter).
-    private final Map<String, Object> namespace = new HashMap<>();
+    // Maps names used on the lhs of definitions ("let name = relexpr" or "let name(params) = relexpr") to the
+    // predicate (either a Relation or a Filter) or the function (FuncDefinition) they identify
+    private Map<String, Object> namespace = new HashMap<>();
     // Counts the number of occurrences of a name on the lhs of a definition
     // This is used to give proper names to re-definitions
     private final Map<String, Integer> nameOccurrenceCounter = new HashMap<>();
     // Used to handle recursive definitions properly
     private Relation relationToBeDefined;
 
-    VisitorBase() {
+    private record FuncDefinition(String name, List<String> params, String expression,
+                                  Map<String, Object> capturedNamespace) {
+        @Override
+        public String toString() {
+            return String.format("%s%s := %s",
+                    name,
+                    params.stream().collect(Collectors.joining(", ", "(", ")")),
+                    expression
+            );
+        }
+    }
+
+    VisitorCat(Path includePath) {
+        this.includePath = includePath;
         this.wmm = new Wmm();
     }
 
+
     @Override
     public Object visitMcm(McmContext ctx) {
         super.visitMcm(ctx);
         return wmm;
     }
 
+    @Override
+    public Object visitLetFuncDefinition(LetFuncDefinitionContext ctx) {
+        final String fname = ctx.fname.getText();
+        final List<String> params = ctx.params.NAME().stream().map(Object::toString).toList();
+        final String expression = ctx.expression().getText();
+        final Map<String, Object> capturedNamespace = ImmutableMap.copyOf(namespace);
+
+        final FuncDefinition definition = new FuncDefinition(fname, params, expression, capturedNamespace);
+        namespace.put(fname, definition);
+        return null;
+    }
+
+    @Override
+    public Object visitInclude(IncludeContext ctx) {
+        final String fileName = ctx.path.getText().substring(1, ctx.path.getText().length() - 1);
+        final Path filePath = includePath.resolve(Path.of(fileName));
+        if (!Files.exists(filePath)) {
+            logger.warn("Included file '{}' not found. Skipped inclusion.", filePath);
+            return null;
+        }
+
+        try {
+            final CatParser parser = getParser(CharStreams.fromPath(filePath));
+            return parser.mcm().accept(this);
+        } catch (IOException e) {
+            throw new ParsingException(String.format("Error parsing file '%s'", filePath), e);
+        }
+    }
+
     @Override
     public Void visitAxiomDefinition(AxiomDefinitionContext ctx) {
         try {
@@ -154,6 +210,34 @@ public Object visitExprBasic(ExprBasicContext ctx) {
         return predicate;
     }
 
+    @Override
+    public Object visitExprCall(ExprCallContext ctx) {
+        final String calledFunc = ctx.call.getText();
+        if (!(namespace.get(calledFunc) instanceof FuncDefinition funcDef)) {
+            final String error = String.format("Invalid call %s: %s is undefined or no function.", ctx.getText(), calledFunc);
+            throw new ParsingException(error);
+        }
+
+        final List<CatParser.ExpressionContext> args = ctx.args.expression();
+        if (args.size() != funcDef.params().size()) {
+            final String error = String.format("Invalid call %s to function %s: wrong number of arguments.",
+                    ctx.getText(), funcDef);
+            throw new ParsingException(error);
+        }
+        final List<Object> arguments = ctx.args.expression().stream().map(e -> e.accept(this)).toList();
+        final Map<String, Object> functionNamespace = new HashMap<>(funcDef.capturedNamespace());
+        for (int i = 0; i < arguments.size(); i++) {
+            functionNamespace.put(funcDef.params.get(i), arguments.get(i));
+        }
+
+        final Map<String, Object> curNamespace = namespace;
+        namespace = functionNamespace;
+        final CatParser parser = getParser(CharStreams.fromString(funcDef.expression));
+        Object result =  parser.expression().accept(this);
+        namespace = curNamespace;
+        return result;
+    }
+
     @Override
     public Object visitExprIntersection(ExprIntersectionContext c) {
         Optional<Relation> defRel = getAndResetRelationToBeDefined();
@@ -322,5 +406,17 @@ private static Filter parseAsFilter(Object o, ExpressionContext t) {
         }
         throw new ParsingException("Expected set, got " + o.getClass().getSimpleName() + " " + o + " from expression " + t.getText());
     }
+
+    private static CatParser getParser(CharStream input) {
+        final Lexer lexer = new CatLexer(input);
+        lexer.addErrorListener(new AbortErrorListener());
+        lexer.addErrorListener(new DiagnosticErrorListener(true));
+        final CommonTokenStream tokenStream = new CommonTokenStream(lexer);
+
+        final CatParser parser = new CatParser(tokenStream);
+        parser.addErrorListener(new AbortErrorListener());
+        parser.addErrorListener(new DiagnosticErrorListener(true));
+        return parser;
+    }
 }