Skip to content

Commit

Permalink
Added support for include statements in cat
Browse files Browse the repository at this point in the history
  • Loading branch information
ThomasHaas committed Sep 12, 2024
1 parent ee0ebed commit ef8a507
Show file tree
Hide file tree
Showing 7 changed files with 92 additions and 20 deletions.
14 changes: 8 additions & 6 deletions dartagnan/src/main/antlr4/Cat.g4
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ mcm
;

definition
: axiomDefinition
: include
| axiomDefinition
| letDefinition
| letRecDefinition
;
Expand Down Expand Up @@ -52,6 +53,10 @@ expression
| call = NEW LPAR RPAR # exprNew
;

include
: 'include' path = QUOTED_STRING
;

LET : 'let';
REC : 'rec';
AND : 'and';
Expand Down Expand Up @@ -88,6 +93,8 @@ FLAG : 'flag';

NAME : [A-Za-z0-9\-_.]+;

QUOTED_STRING : '"' .*? '"';

LINE_COMMENT
: '//' ~[\n]*
-> skip
Expand All @@ -103,11 +110,6 @@ WS
-> skip
;

INCLUDE
: 'include "' .*? '"'
-> skip
;

MODELNAME
: '"' .*? '"'
-> skip
Expand Down
13 changes: 7 additions & 6 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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()));
}

Expand Down Expand Up @@ -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)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down
Original file line number Diff line number Diff line change
@@ -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));
Expand All @@ -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));
}
}
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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;
Expand All @@ -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<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
Expand All @@ -34,16 +51,42 @@ class VisitorBase extends CatBaseVisitor<Object> {
// 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 {
Expand Down
Original file line number Diff line number Diff line change
@@ -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 {

Expand Down Expand Up @@ -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; }
}

0 comments on commit ef8a507

Please sign in to comment.