Skip to content

Commit d54fd82

Browse files
ThomasHaasThomasHaas
committed
Cleanup Dartagnan.java
1 parent 57769a7 commit d54fd82

4 files changed

Lines changed: 110 additions & 97 deletions

File tree

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

Lines changed: 102 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package com.dat3m.dartagnan;
22

3+
import com.dat3m.dartagnan.configuration.OptionInfo;
34
import com.dat3m.dartagnan.configuration.ProgressModel;
45
import com.dat3m.dartagnan.exception.MalformedProgramException;
56
import com.dat3m.dartagnan.parsers.cat.ParserCat;
@@ -16,7 +17,6 @@
1617
import com.dat3m.dartagnan.verification.VerificationTask.VerificationTaskBuilder;
1718
import com.dat3m.dartagnan.witness.graphml.WitnessGraph;
1819
import com.dat3m.dartagnan.wmm.Wmm;
19-
import com.google.common.collect.ImmutableSet;
2020
import com.google.common.io.CharSource;
2121
import org.apache.maven.model.io.xpp3.MavenXpp3Reader;
2222
import org.slf4j.Logger;
@@ -31,93 +31,60 @@
3131
import java.nio.file.Files;
3232
import java.nio.file.Path;
3333
import java.nio.file.Paths;
34-
import java.util.*;
34+
import java.util.ArrayList;
35+
import java.util.Arrays;
36+
import java.util.Comparator;
37+
import java.util.List;
3538
import java.util.stream.Stream;
3639

37-
import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions;
38-
import static com.dat3m.dartagnan.configuration.OptionNames.*;
39-
import static com.dat3m.dartagnan.utils.ExitCode.*;
40+
import static com.dat3m.dartagnan.configuration.OptionNames.TARGET;
41+
import static com.dat3m.dartagnan.utils.ExitCode.NORMAL_TERMINATION;
4042
import static com.dat3m.dartagnan.utils.GitInfo.*;
41-
import static com.dat3m.dartagnan.witness.graphviz.ExecutionGraphVisualizer.generateGraphvizFile;
4243

4344
@Options
4445
public class Dartagnan extends BaseOptions {
4546

4647
private static final Logger logger = LoggerFactory.getLogger(Dartagnan.class);
4748

48-
private static final Set<String> supportedFormats = ImmutableSet.copyOf(ProgramParser.SUPPORTED_EXTENSIONS);
49-
5049
private Dartagnan(Configuration config) throws InvalidConfigurationException {
5150
config.recursiveInject(this);
5251
}
5352

54-
private static Configuration loadConfiguration(String[] args) throws InvalidConfigurationException, IOException {
55-
final var preamble = new StringBuilder();
56-
final var options = new StringBuilder();
57-
for (String argument : args) {
58-
if (argument.startsWith("--")) {
59-
options.append(argument.substring("--".length())).append("\n");
60-
} else if (argument.endsWith(".properties")) {
61-
preamble.append("#include ").append(argument).append("\n");
62-
}
63-
}
64-
final CharSource source = CharSource.concat(CharSource.wrap(preamble), CharSource.wrap(options));
65-
return Configuration.builder()
66-
.addConverter(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER)
67-
.loadFromSource(source, ".", ".")
68-
.build();
69-
}
70-
71-
7253
public static void main(String[] args) throws Exception {
7354

7455
initGitInfo();
7556

7657
if (Arrays.asList(args).contains("--help")) {
77-
collectOptions();
58+
printOptions();
7859
return;
79-
}
80-
81-
if (Arrays.asList(args).contains("--version")) {
82-
final MavenXpp3Reader mvnReader = new MavenXpp3Reader();
83-
final FileReader fileReader = new FileReader(System.getenv("DAT3M_HOME") + "/pom.xml");
84-
final String base = mvnReader.read(fileReader).getVersion();
85-
final String version = base.equals(getGitTags()) ? base : String.format("%s (commit %s)", base, getGitId());
86-
System.out.println(version);
60+
} else if (Arrays.asList(args).contains("--version")) {
61+
printVersion();
8762
return;
8863
}
8964

9065
logGitInfo();
9166

92-
final Configuration config = loadConfiguration(args);
67+
final Configuration config = loadConfigurationFromArgs(args);
9368
final Dartagnan o = new Dartagnan(config);
9469

95-
final File wmmFile = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst()
96-
.orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized")));
97-
logger.info("CAT file path: {}", wmmFile);
98-
final OutputLogger output = new OutputLogger(wmmFile, config);
99-
100-
final WitnessGraph witness;
101-
if (o.runValidator()) {
102-
logger.info("Witness path: {}", o.getWitnessPath());
103-
witness = new ParserWitness().parse(new File(o.getWitnessPath()));
104-
} else {
105-
witness = new WitnessGraph();
106-
}
70+
final File catFile = getCatFileFromArgs(args);
71+
final List<File> progFiles = getProgramFilesFromArgs(args);
72+
final boolean isBatchMode = progFiles.size() > 1;
10773

108-
ResultSummary summary = null;
109-
final List<File> files = getProgramFilesFromArgs(args);
74+
final WitnessGraph witness = getWitnessGraph(o, isBatchMode);
75+
76+
final OutputLogger output = new OutputLogger(catFile, config);
11077
final TaskResultAnalyzer resultAnalyzer = TaskResultAnalyzer.create();
111-
for (File f : files) {
112-
final String progFilePath = f.getPath();
78+
ResultSummary summary = null;
79+
for (File progFile : progFiles) {
11380
try {
11481
// ----------- Generate verification task -----------
115-
final Program p = new ProgramParser().parse(f);
82+
final Program p = new ProgramParser().parse(progFile);
11683
if (o.overrideEntryFunction()) {
11784
p.setEntrypoint(new Entrypoint.Simple(p.getFunctionByName(o.getEntryFunction()).orElseThrow(
11885
() -> new MalformedProgramException(String.format("Program has no function named %s. Select a different entry point.", o.getEntryFunction())))));
11986
}
120-
final Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(wmmFile);
87+
final Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(catFile);
12188
final VerificationTaskBuilder builder = VerificationTask.builder()
12289
.withConfig(config)
12390
.withProgressModel(o.getProgressModel())
@@ -135,65 +102,109 @@ public static void main(String[] args) throws Exception {
135102
taskSolver.run();
136103

137104
// ----------- Generate output-----------
138-
summary = resultAnalyzer.getSummaryFromSolver(taskSolver, f.getPath());
105+
summary = resultAnalyzer.getSummaryFromSolver(taskSolver, progFile.getPath());
139106
// We only generate witnesses if we are not validating one.
140107
if (!o.runValidator()) {
141-
final String progName = task.getProgram().getName();
142-
final int fileSuffixIndex = progName.lastIndexOf('.');
143-
final String filename = o.hasWitnessFilename() ?
144-
o.getWitnessFilename() :
145-
progName.isEmpty() ?
146-
"unnamed_program" :
147-
(fileSuffixIndex == -1) ? progName : progName.substring(0, fileSuffixIndex);
148-
108+
final String filename = getWitnessFileName(task.getProgram(), o);
149109
resultAnalyzer.generateWitnessIfAble(taskSolver, o.getWitnessType(), filename, summary.reason() + "\n" + summary.details(), o.generateWitnessForUnknown());
150110
}
151111
} catch (Exception e) {
152-
summary = resultAnalyzer.getSummaryFromException(e, progFilePath);
112+
summary = resultAnalyzer.getSummaryFromException(e, progFile.getPath());
153113
}
154114
output.addResult(summary);
155115
}
156-
output.toStdOut(files.size() > 1);
116+
output.toStdOut(isBatchMode);
157117
// Running batch mode results in normal termination independent of the individual results
158-
System.exit((files.size() > 1 ? NORMAL_TERMINATION : summary.code()).asInt());
118+
System.exit((isBatchMode ? NORMAL_TERMINATION : summary.code()).asInt());
119+
}
120+
121+
// ----------------------------------------------------------------------------------------------------
122+
123+
private static void printOptions() {
124+
OptionInfo.stream().sorted().forEach(System.out::print);
125+
}
126+
127+
private static void printVersion() throws Exception {
128+
final MavenXpp3Reader mvnReader = new MavenXpp3Reader();
129+
final FileReader fileReader = new FileReader(System.getenv("DAT3M_HOME") + "/pom.xml");
130+
final String base = mvnReader.read(fileReader).getVersion();
131+
final String version = base.equals(getGitTags()) ? base : String.format("%s (commit %s)", base, getGitId());
132+
133+
System.out.println(version);
134+
}
135+
136+
private static Configuration loadConfigurationFromArgs(String[] args) throws InvalidConfigurationException, IOException {
137+
final var preamble = new StringBuilder();
138+
final var options = new StringBuilder();
139+
for (String argument : args) {
140+
if (argument.startsWith("--")) {
141+
options.append(argument.substring("--".length())).append("\n");
142+
} else if (argument.endsWith(".properties")) {
143+
preamble.append("#include ").append(argument).append("\n");
144+
}
145+
}
146+
final CharSource source = CharSource.concat(CharSource.wrap(preamble), CharSource.wrap(options));
147+
return Configuration.builder()
148+
.addConverter(ProgressModel.Hierarchy.class, ProgressModel.HIERARCHY_CONVERTER)
149+
.loadFromSource(source, ".", ".")
150+
.build();
151+
}
152+
153+
private static File getCatFileFromArgs(String[] args) {
154+
File catFile = Arrays.stream(args)
155+
.filter(a -> a.endsWith(".cat"))
156+
.findFirst()
157+
.map(File::new)
158+
.orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized"));
159+
logger.info("CAT file path: {}", catFile);
160+
return catFile;
159161
}
160162

161163
private static List<File> getProgramFilesFromArgs(String[] args) {
162164
final List<File> files = new ArrayList<>();
163-
Stream.of(args)
164-
.map(File::new)
165-
.forEach(file -> {
166-
if (file.exists()) {
167-
final String path = file.getAbsolutePath();
168-
if (file.isDirectory()) {
169-
logger.info("Programs path: {}", path);
170-
files.addAll(getProgramFiles(path));
171-
} else if (file.isFile() && supportedFormats.stream().anyMatch(file.getName()::endsWith)) {
172-
logger.info("Program path: {}", path);
173-
files.add(file);
174-
}
175-
}
176-
});
165+
Stream.of(args).map(Paths::get).filter(Files::exists)
166+
.forEach(path -> {
167+
logger.info("Program(s) path: {}", path.normalize());
168+
files.addAll(getProgramFiles(path));
169+
});
177170
if (files.isEmpty()) {
178171
throw new IllegalArgumentException("Path to input program(s) not given or format not recognized");
179172
}
180173
return files;
181174
}
182175

183-
private static List<File> getProgramFiles(String dirPath) {
184-
List<File> files = new ArrayList<>();
185-
try (Stream<Path> stream = Files.walk(Paths.get(dirPath))) {
186-
files = stream.filter(Files::isRegularFile)
187-
.filter(p -> supportedFormats.stream().anyMatch(p.toString()::endsWith))
188-
.map(Path::toFile)
189-
.sorted(Comparator.comparing(File::toString))
190-
.toList();
176+
private static List<File> getProgramFiles(Path path) {
177+
try (Stream<Path> stream = Files.walk(path)) {
178+
return stream.filter(Files::isRegularFile)
179+
.filter(ProgramParser::isSupported)
180+
.sorted(Comparator.comparing(Path::toString))
181+
.map(Path::toFile)
182+
.toList();
191183
} catch (IOException e) {
192-
logger.error("There was an I/O error when accessing path {}", dirPath);
193-
System.exit(UNKNOWN_ERROR.asInt());
184+
logger.error("There was an I/O error when accessing path {}", path);
185+
return List.of();
194186
}
195-
return files;
196187
}
197188

189+
private static WitnessGraph getWitnessGraph(Dartagnan o, boolean isBatchMode) throws IOException {
190+
if (!o.runValidator()) {
191+
return new WitnessGraph();
192+
}
193+
194+
if (isBatchMode) {
195+
throw new IllegalArgumentException("Cannot run validator in batch mode.");
196+
}
197+
logger.info("Witness path: {}", o.getWitnessPath());
198+
return new ParserWitness().parse(new File(o.getWitnessPath()));
199+
}
198200

201+
private static String getWitnessFileName(Program program, Dartagnan o) {
202+
if (o.hasWitnessFilename()) {
203+
return o.getWitnessFilename();
204+
}
205+
206+
return program.getName().isEmpty()
207+
? "unnamed_program"
208+
: com.google.common.io.Files.getNameWithoutExtension(program.getName());
209+
}
199210
}

‎dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionInfo.java‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,10 +31,6 @@
3131

3232
public final class OptionInfo implements Comparable<OptionInfo> {
3333

34-
public static void collectOptions() {
35-
stream().sorted().forEach(System.out::print);
36-
}
37-
3834
public static Stream<OptionInfo> stream() {
3935
return classes().flatMap(OptionInfo::collectOptions);
4036
}

‎dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ProgramParser.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@
22

33
import com.dat3m.dartagnan.exception.ParsingException;
44
import com.dat3m.dartagnan.program.Program;
5+
import com.google.common.io.Files;
56
import org.antlr.v4.runtime.CharStream;
67
import org.antlr.v4.runtime.CharStreams;
78
import org.slf4j.Logger;
89
import org.slf4j.LoggerFactory;
910

1011
import java.io.*;
12+
import java.nio.file.Path;
1113
import java.util.List;
1214

1315
import static com.dat3m.dartagnan.parsers.program.utils.Compilation.compileWithClang;
@@ -34,6 +36,11 @@ public class ProgramParser {
3436
public static final List<String> SUPPORTED_EXTENSIONS = List.of(
3537
EXTENSION_C, EXTENSION_I, EXTENSION_LL, EXTENSION_LITMUS, EXTENSION_SPV_DIS, EXTENSION_SPVASM);
3638

39+
public static boolean isSupported(Path filePath) {
40+
final String extension = "." + Files.getFileExtension(filePath.getFileName().toString());
41+
return SUPPORTED_EXTENSIONS.contains(extension);
42+
}
43+
3744
public Program parse(File file) throws Exception {
3845
if (needsClang(file)) {
3946
file = compileWithClang(file, "");

‎dartagnan/src/main/java/com/dat3m/dartagnan/utils/GitInfo.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package com.dat3m.dartagnan.utils;
22

33
import com.dat3m.dartagnan.Dartagnan;
4-
54
import org.slf4j.Logger;
65
import org.slf4j.LoggerFactory;
76

@@ -13,7 +12,7 @@ public class GitInfo {
1312

1413
private static final Logger logger = LoggerFactory.getLogger(GitInfo.class);
1514

16-
static Properties properties = new Properties();
15+
private final static Properties properties = new Properties();
1716

1817
public static void initGitInfo() throws IOException {
1918
try (InputStream is = Dartagnan.class.getClassLoader()

0 commit comments

Comments
 (0)