Verified Commit 24d8b6f3 authored by Amin Bandali's avatar Amin Bandali
Browse files

Simplify printing logic and remove the Printer class

parent afd55c73
package org.aminb.alloy.catalyst;
import java.io.BufferedOutputStream;
import java.io.BufferedWriter;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.io.Writer;
import java.nio.file.Path;
import java.util.ArrayList;
import java.util.concurrent.atomic.AtomicInteger;
......@@ -13,7 +20,8 @@ public abstract class CatalystCommand {
protected transient Result r;
protected transient Gson gson;
protected transient AtomicInteger errorCount;
protected transient Printer pr;
protected transient Writer wtxt, wjson;
protected transient PrintWriter ptxt;
@Option(names = "--models-dir",
required = true,
......@@ -60,15 +68,52 @@ public abstract class CatalystCommand {
@Option(names = "--parallel", description = "Parallel mode (use parallel streams)")
protected boolean parallel;
protected void initialize() {
protected void initialize(Path outputTxtFile, Path outputJsonFile) {
r = new Result();
r.options = this;
r.results = new ArrayList<CorpusResult>();
gson = new Gson();
errorCount = new AtomicInteger();
wtxt = setupWriter(outputTxtFile, true);
wjson = setupWriter(outputJsonFile, true);
ptxt = new PrintWriter(wtxt);
}
abstract protected CorpusResult analyzeCorpus(Printer mainPr, String corpus);
abstract protected FileResult analyzeFile(Printer mainPr, String corpus, Path p,
int index, int total);
abstract protected CorpusResult analyzeCorpus(String corpus);
abstract protected FileResult analyzeFile(String corpus, Path p, int index, int total);
private BufferedWriter setupWriter(Path p, boolean createParents) {
if (createParents)
p.getParent().toFile().mkdirs();
BufferedWriter w;
try {
w = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(p.toString())));
}
catch (FileNotFoundException e) {
String msg = "Failed to set up file output stream for " +
p.toString();
r.error = String.format("%s%n%s", msg, Utils.toString(e));
System.out.print(r.error);
throw Utils.systemExit(1);
}
return w;
}
protected void p(String s) {
System.out.println(s);
ptxt.print(s);
}
protected void pln(String s) {
p(s + System.lineSeparator());
}
protected void pln() {
pln("");
}
protected void pf(String format, Object... args) {
p(String.format(format, args));
}
}
......@@ -63,10 +63,13 @@ public final class Mut extends CatalystCommand implements Runnable {
description = "Number of mutations to generate per Alloy file")
protected int mutationCount = 3;
final private Path OUT_TEXT = Paths.get(resultsDir, "catalyst_mut.txt");
final private Path OUT_JSON = Paths.get(resultsDir, "catalyst_mut.json");
public Mut() {}
public void run() {
initialize();
initialize(OUT_TEXT, OUT_JSON);
gson = new GsonBuilder().setPrettyPrinting().create();
// ugly workaround to load the solvers' native libraries
......@@ -76,44 +79,31 @@ public final class Mut extends CatalystCommand implements Runnable {
.map(s -> s.solver)
.toArray(SatSolver[]::new));
try {
pr = new Printer(Paths.get(resultsDir, "catalyst_out.txt"), null,
Printer.StdoutMode.NORMAL_ONLY,
Printer.FileOutMode.NORMAL_ONLY,
true);
} catch (FileNotFoundException e) {
String msg = "Failed to set up file output stream " +
"for general Catalyst output.";
r.error = String.format("%s%n%s", msg, MailBug.dump(e));
System.out.print(r.error);
throw Utils.systemExit(1);
}
Instant start = Instant.now();
for (String corpus : corpora)
r.results.add(analyzeCorpus(pr, corpus));
r.results.add(analyzeCorpus(corpus));
Instant end = Instant.now();
r.total_error_count = errorCount.get();
r.total_elapsed_time = Duration.between(start, end).toMillis();
pr.ln(String.format("total number of analyzed files: %d", r.total_file_count));
pr.ln(String.format("total error count: %d", r.total_error_count));
pr.ln(String.format("total elapsed time: %dms", r.total_elapsed_time));
pln(String.format("total number of analyzed files: %d", r.total_file_count));
pln(String.format("total error count: %d", r.total_error_count));
pln(String.format("total elapsed time: %dms", r.total_elapsed_time));
pr.ln(gson.toJson(r));
pr.close();
pln(gson.toJson(r));
ptxt.close();
}
@Override
protected final CorpusResult analyzeCorpus(Printer mainPr, String corpus) {
protected final CorpusResult analyzeCorpus(String corpus) {
CorpusResult cr = new CorpusResult();
cr.corpus_name = corpus;
cr.file_results = parallel ?
Collections.synchronizedList(new ArrayList<FileResult>()) :
new ArrayList<FileResult>();
mainPr.ln();
pln();
Instant start = Instant.now();
try {
......@@ -121,13 +111,13 @@ public final class Mut extends CatalystCommand implements Runnable {
.filter(Files::isRegularFile)
.collect(Collectors.toList());
cr.file_count = files.size();
mainPr.ln("number of " + corpus + " models: " + cr.file_count);
pln("number of " + corpus + " models: " + cr.file_count);
r.total_file_count += cr.file_count;
AtomicInteger i = new AtomicInteger(1);
Stream<Path> fs = parallel ? files.parallelStream() : files.stream();
fs.filter(p -> p.getFileName().toString().endsWith(".als"))
.filter(p -> !Arrays.asList(ignoredFiles).contains(p.getFileName().toString()))
.forEach(p -> cr.file_results.add(analyzeFile(mainPr, corpus, p, i.getAndIncrement(), cr.file_count)));
.forEach(p -> cr.file_results.add(analyzeFile(corpus, p, i.getAndIncrement(), cr.file_count)));
} catch (Exception e) {
String msg = "Failed while trying to iterate through and analyze " + corpus + " models.";
cr.error = String.format("%s%n%s", msg, MailBug.dump(e));
......@@ -137,16 +127,16 @@ public final class Mut extends CatalystCommand implements Runnable {
Instant end = Instant.now();
cr.elapsed_time = Duration.between(start, end).toMillis();
mainPr.ln(String.format("time taken to analyze %s models: %dms",
corpus, cr.elapsed_time));
pln(String.format("time taken to analyze %s models: %dms",
corpus, cr.elapsed_time));
mainPr.ln();
pln();
return cr;
}
@Override
protected final FileResult analyzeFile(Printer mainPr, String corpus, Path p, int index, int total) {
protected final FileResult analyzeFile(String corpus, Path p, int index, int total) {
FileResult fr = new FileResult();
fr.file_name = p.toString();
fr.mutation_results = new ArrayList<MutationResult>();
......@@ -154,36 +144,14 @@ public final class Mut extends CatalystCommand implements Runnable {
String progress = String.format("[%d/%d]: ", index, total);
Path outputFile = Paths.get(resultsDir, corpus, fr.file_name.replace("/", outSep));
Path outputFileDebug = Paths.get(debugDir, corpus, fr.file_name.replace("/", outSep));
Printer pr;
try {
pr = new Printer(outputFile, outputFileDebug,
Printer.StdoutMode.NONE,
Printer.FileOutMode.BOTH,
true);
} catch (FileNotFoundException e) {
System.out.println("Failed to set up file output streams for " +
"the normal result and/or debug file(s).");
e.printStackTrace();
throw Utils.systemExit(1);
}
A4Reporter rep = new A4Reporter() {
@Override
public void warning(ErrorWarning msg) {
fr.errors.add(new ParseOrTypeError(msg.toString().trim(), false));
pr.lnd("WARNING: " + (msg.toString().trim()) + "\n");
System.out.flush();
}
};
pr.ln(fr.file_name);
pr.lnd("- file:" + fr.file_name);
mainPr.ln(progress + "start: " + fr.file_name);
pr.lnd(" parsing and typechecking...");
pln(progress + "start: " + fr.file_name);
CompModule world;
try {
......@@ -191,78 +159,40 @@ public final class Mut extends CatalystCommand implements Runnable {
} catch (Err e) {
String msg = "Error in parsing or type checking. Stack trace from the exception:",
err = e.dump();
mainPr.ln(progress + "error: " + fr.file_name);
pr.lnd(msg);
pr.lnd(err);
pr.ln("parse-or-type error");
r.error = String.format("%s%n%s", msg, e.dump());
fr.errors.add(new ParseOrTypeError(r.error, true));
pln(progress + "error: " + fr.file_name);
fr.errors.add(new ParseOrTypeError(String.format("%s%n%s", msg, e.dump()), true));
errorCount.getAndIncrement();
return fr;
}
if (moduleHasCommands(world)) {
pr.ln(mutationCount + 1);
pr.lnd(" number of executions: " + (mutationCount + 1));
pr.lnd(" + mutation 0 (original)");
pr.lnd(world.getAllSigsMap().toString());
pr.lnd(" running...");
try {
fr.mutation_results.add(mutateModule(pr, world, MutationKind.ORIGINAL));
fr.mutation_results.add(mutateModule(world, MutationKind.ORIGINAL));
} catch (Err e) {
String msg = "Error while analyzing original module. Stack trace from the exception:",
err = e.dump();
mainPr.ln(progress + "error: " + fr.file_name);
pr.lnd(msg);
pr.lnd(err);
pr.ln("execute error");
r.error = String.format("%s%n%s", msg, e.dump());
fr.errors.add(new ParseOrTypeError(r.error, true));
pln(progress + "error: " + fr.file_name);
fr.errors.add(new ParseOrTypeError(String.format("%s%n%s", msg, e.dump()), true));
errorCount.getAndIncrement();
return fr;
}
pr.lnd(" done...");
for (int i = 1; i <= mutationCount; i++) {
pr.lnd(" + mutation " + i);
shuffleSigs(world);
pr.lnd(world.getAllSigsMap().toString());
pr.lnd(" running...");
try {
fr.mutation_results.add(mutateModule(pr, world, MutationKind.MUT_RANDOM));
fr.mutation_results.add(mutateModule(world, MutationKind.MUT_RANDOM));
} catch (Err e) {
String msg = "Error while analyzing mutation. Stack trace from the exception:",
err = e.dump();
mainPr.ln(progress + "error: " + fr.file_name);
pr.lnd(msg);
pr.lnd(err);
pr.ln("execute error");
r.error = String.format("%s%n%s", msg, e.dump());
fr.errors.add(new ParseOrTypeError(r.error, true));
pln(progress + "error: " + fr.file_name);
fr.errors.add(new ParseOrTypeError(String.format("%s%n%s", msg, e.dump()), true));
errorCount.getAndIncrement();
return fr;
}
pr.lnd(" done...");
}
} else {
pr.ln(0);
pr.lnd(" module has no commands");
}
mainPr.ln(progress + "done: " + fr.file_name);
pr.close();
pln(progress + "done: " + fr.file_name);
return fr;
}
......@@ -290,19 +220,15 @@ public final class Mut extends CatalystCommand implements Runnable {
}
}
private MutationResult mutateModule(Printer pr, CompModule module, MutationKind kind) throws Err {
private MutationResult mutateModule(CompModule module, MutationKind kind) throws Err {
MutationResult mr = new MutationResult();
mr.kind = kind;
mr.runs = Collections.synchronizedList(new ArrayList<Run>());
int s_i = 0; // keep track of the current solver's position
mr.sigs = module.getAllSigsMap().toString();
mr.runs = parallel ?
Collections.synchronizedList(new ArrayList<Run>()) :
new ArrayList<>();
for (Solver solver : solvers) {
pr.noln(solver.solver.id() + ":");
pr.lnd(" solver: " + solver.solver);
Instant start = Instant.now();
ConstList<Sig> allReachableSigs = module.getAllReachableSigs();
A4Options options = new A4Options();
options.solver = solver.solver;
......@@ -323,16 +249,6 @@ public final class Mut extends CatalystCommand implements Runnable {
});
mr.runs.add(run);
});
Instant stop = Instant.now();
long elapsed = Duration.between(start, stop).toMillis();
pr.noln(elapsed);
if(++s_i == solvers.length) // if this is the last solver
pr.ln();
else
pr.noln(",");
pr.lnd(" all commands: " + elapsed + "ms");
}
return mr;
......
package org.aminb.alloy.catalyst;
import java.io.BufferedOutputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintStream;
import java.nio.file.Path;
public class Printer {
// helper for printing out to stdout and a pair files (normal and debug)
public enum StdoutMode {
NORMAL_ONLY,
DEBUG_ONLY,
NONE
}
public enum FileOutMode {
NORMAL_ONLY,
DEBUG_ONLY,
BOTH,
NONE
}
private Path normalFileName, debugFileName;
private PrintStream normal, debug;
private StdoutMode stdoutMode;
private FileOutMode fileOutMode;
private boolean createParents;
private void initializeNormal() throws FileNotFoundException {
if (createParents)
normalFileName.getParent().toFile().mkdirs();
normal = new PrintStream(new BufferedOutputStream(new FileOutputStream(normalFileName.toString())), true);
}
private void initializeDebug() throws FileNotFoundException {
if (createParents)
debugFileName.getParent().toFile().mkdirs();
debug = new PrintStream(new BufferedOutputStream(new FileOutputStream(debugFileName.toString())), true);
}
Printer(Path outFile, Path outFileDebug,
StdoutMode stdoutMode, FileOutMode fileOutMode,
boolean createParents) throws FileNotFoundException {
this.normal = this.debug = null;
this.normalFileName = outFile;
this.debugFileName = outFileDebug;
this.stdoutMode = stdoutMode;
this.fileOutMode = fileOutMode;
this.createParents = createParents;
switch (fileOutMode) {
case NORMAL_ONLY:
initializeNormal();
break;
case DEBUG_ONLY:
initializeDebug();
break;
case BOTH:
initializeNormal();
initializeDebug();
break;
default:
break;
}
}
public void setStdoutMode(StdoutMode mode) {
stdoutMode = mode;
}
public void setFileOutMode(FileOutMode mode) throws FileNotFoundException {
if (normal == null)
if (mode == FileOutMode.NORMAL_ONLY || mode == FileOutMode.BOTH)
initializeNormal();
if (debug == null)
if (mode == FileOutMode.DEBUG_ONLY || mode == FileOutMode.BOTH)
initializeDebug();
fileOutMode = mode;
}
public void close() {
if (normal != null)
normal.close();
if (debug != null)
debug.close();
}
public void noln(String s) {
synchronized (this) {
switch (stdoutMode) {
case NORMAL_ONLY:
System.out.print(s);
break;
default:
break;
}
switch (fileOutMode) {
case NORMAL_ONLY:
case BOTH:
normal.print(s);
break;
default:
break;
}
}
}
public void noln(int i) {
noln(Integer.toString(i));
}
public void noln(long i) {
noln(Long.toString(i));
}
public void ln(String s) {
noln(s);
noln(System.lineSeparator());
}
public void ln(int i) {
ln(Integer.toString(i));
}
public void ln(long i) {
ln(Long.toString(i));
}
public void ln() {
ln("");
}
public void lnd(String s) {
synchronized (this) {
switch (stdoutMode) {
case DEBUG_ONLY:
System.out.println(s);
break;
default:
break;
}
switch (fileOutMode) {
case DEBUG_ONLY:
case BOTH:
debug.println(s);
break;
default:
break;
}
}
}
public void lnd() {
lnd("");
}
public void lnd(int i) {
lnd(Integer.toString(i));
}
}
......@@ -45,15 +45,16 @@ class SSRResult {
}
class MutationResult {
MutationKind kind;
List<Run> runs;
public MutationKind kind;
public String sigs;
public List<Run> runs;
}
class Run {
public String solver_id;
public String solver_name;
public String command;
List<RunResult> takes;
public List<RunResult> takes;
}
class RunResult {
......
......@@ -29,47 +29,38 @@ import picocli.CommandLine.Command;
public final class SSR extends CatalystCommand implements Runnable {
public SSR() {}
final private Path OUT_TEXT = Paths.get(resultsDir, "catalyst_ssr.txt");
final private Path OUT_JSON = Paths.get(resultsDir, "catalyst_ssr.json");
public void run() {
initialize();
initialize(OUT_TEXT, OUT_JSON);
gson = new GsonBuilder().setPrettyPrinting().create();
try {
pr = new Printer(Paths.get(resultsDir, "catalyst_ssr_out.txt"), null,
Printer.StdoutMode.NORMAL_ONLY,
Printer.FileOutMode.NORMAL_ONLY,
true);
} catch (FileNotFoundException e) {
String msg = "Failed to set up file output stream " +
"for general Catalyst output.";
r.error = String.format("%s%n%s", msg, MailBug.dump(e));
System.out.print(r.error);
throw Utils.systemExit(1);
}
Instant start = Instant.now();
for (String corpus : corpora)
r.results.add(analyzeCorpus(pr, corpus));
r.results.add(analyzeCorpus(corpus));
Instant end = Instant.now();
r.total_error_count = errorCount.get();
r.total_elapsed_time = Duration.between(start, end).toMillis();
pr.ln(String.format("total number of analyzed files: %d", r.total_file_count));
pr.ln(String.format("total error count: %d", r.total_error_count));
pr.ln(String.format("total elapsed time: %dms", r.total_elapsed_time));