From ef8a50771c02386bfc5dc1a799abcce68a094d95 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 12 Sep 2024 12:49:09 +0200 Subject: [PATCH] Added support for include statements in cat --- dartagnan/src/main/antlr4/Cat.g4 | 14 +++--- .../java/com/dat3m/dartagnan/Dartagnan.java | 13 ++--- .../com/dat3m/dartagnan/GlobalSettings.java | 6 +++ .../dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/parsers/cat/ParserCat.java | 16 +++++- .../cat/{VisitorBase.java => VisitorCat.java} | 49 +++++++++++++++++-- .../dartagnan/utils/options/BaseOptions.java | 13 +++-- 7 files changed, 92 insertions(+), 20 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/{VisitorBase.java => VisitorCat.java} (87%) diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4 index c3e268437c..95949fe3f2 100755 --- a/dartagnan/src/main/antlr4/Cat.g4 +++ b/dartagnan/src/main/antlr4/Cat.g4 @@ -9,7 +9,8 @@ mcm ; definition - : axiomDefinition + : include + | axiomDefinition | letDefinition | letRecDefinition ; @@ -52,6 +53,10 @@ expression | call = NEW LPAR RPAR # exprNew ; +include + : 'include' path = QUOTED_STRING + ; + LET : 'let'; REC : 'rec'; AND : 'and'; @@ -88,6 +93,8 @@ FLAG : 'flag'; NAME : [A-Za-z0-9\-_.]+; +QUOTED_STRING : '"' .*? '"'; + LINE_COMMENT : '//' ~[\n]* -> skip @@ -103,11 +110,6 @@ WS -> skip ; -INCLUDE - : 'include "' .*? '"' - -> skip - ; - MODELNAME : '"' .*? '"' -> skip diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 161486f7cd..d50601af43 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/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 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)) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index 8d7d52b1fb..6e36bebf24 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/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)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 18a0ca89fc..56b931b8d1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/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"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java index 753625ce88..33f7315286 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java +++ b/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)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java similarity index 87% rename from dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 400c120d7a..d85f3cebc6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java +++ b/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,9 +14,18 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.dat3m.dartagnan.wmm.definition.*; - +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; +import org.antlr.v4.runtime.DiagnosticErrorListener; +import org.antlr.v4.runtime.Lexer; +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.nio.file.Files; +import java.nio.file.Path; import java.util.Arrays; import java.util.HashMap; import java.util.Map; @@ -22,7 +34,12 @@ import static com.dat3m.dartagnan.program.event.Tag.VISIBLE; import static com.dat3m.dartagnan.wmm.RelationNameRepository.ID; -class VisitorBase extends CatBaseVisitor { +class VisitorCat extends CatBaseVisitor { + + 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 @@ -34,16 +51,42 @@ class VisitorBase extends CatBaseVisitor { // Used to handle recursive definitions properly private Relation relationToBeDefined; - VisitorBase() { + VisitorCat(Path includePath) { + this.includePath = includePath; this.wmm = new Wmm(); } + @Override public Object visitMcm(McmContext ctx) { super.visitMcm(ctx); return wmm; } + @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 Lexer lexer = new CatLexer(CharStreams.fromPath(filePath)); + 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.mcm().accept(this); + } catch (IOException e) { + throw new ParsingException(String.format("Error parsing file '%s'", filePath), e); + } + } + @Override public Void visitAxiomDefinition(AxiomDefinitionContext ctx) { try { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index fd166a38e0..273e4cfeaa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -1,17 +1,17 @@ package com.dat3m.dartagnan.utils.options; +import com.dat3m.dartagnan.GlobalSettings; import com.dat3m.dartagnan.configuration.Method; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.witness.WitnessType; - import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import static com.dat3m.dartagnan.configuration.OptionNames.*; - import java.util.EnumSet; +import static com.dat3m.dartagnan.configuration.OptionNames.*; + @Options public abstract class BaseOptions { @@ -75,4 +75,11 @@ public abstract class BaseOptions { private boolean smtlib=false; public boolean getDumpSmtLib() { return smtlib; } + + @Option( + name=CAT_INCLUDE, + description = "The directory used to resolve cat include statements. Defaults to Dartagnan's cat directory." + ) + private String catIncludePath = GlobalSettings.getCatDirectory(); + public String getCatIncludePath() { return catIncludePath; } } \ No newline at end of file