Verified Commit afd55c73 authored by Amin Bandali's avatar Amin Bandali
Browse files

Break MainCLI down into SSR and Mut subcommands

parent c176b3f1
......@@ -53,7 +53,7 @@
<dependency>
<groupId>info.picocli</groupId>
<artifactId>picocli</artifactId>
<version>3.9.1</version>
<version>4.0.0-alpha-3</version>
</dependency>
<dependency>
<groupId>com.google.code.gson</groupId>
......
package org.aminb.alloy.catalyst;
import picocli.CommandLine.Command;
import java.nio.file.Path;
import java.util.ArrayList;
import java.util.concurrent.atomic.AtomicInteger;
import com.google.gson.Gson;
import picocli.CommandLine.Option;
@Command(
name = "catalyst",
version = { "catalyst 0.1",
"Copyright (C) 2018-2019 Amin Bandali",
"License: Expat (MIT) <https://gnu.org/licenses/license-list.html#Expat>.",
"This is free software: you are free to change and redistribute it.",
"There is NO WARRANTY, to the extent permitted by law.",
"",
"Written by Amin Bandali."
},
description = "A framework for analyzing performance of Alloy models.",
mixinStandardHelpOptions = true,
showDefaultValues = true)
public class Options implements Runnable {
private transient MainCLI app;
public abstract class CatalystCommand {
protected transient Result r;
protected transient Gson gson;
protected transient AtomicInteger errorCount;
protected transient Printer pr;
@Option(names = "--models-dir",
required = true,
......@@ -43,10 +38,6 @@ public class Options implements Runnable {
description = "Output directory for analysis debugging information")
protected String debugDir;
@Option(names = "--mutation-count",
description = "Number of mutations to generate per Alloy file")
protected int mutationCount = 3;
@Option(names = "--separator",
description = "Separator used instead of forward slash in output file" +
" names; e.g. with \"$_\", /a/b/c becomes $_a$_b$_c")
......@@ -66,18 +57,18 @@ public class Options implements Runnable {
description = "Comma-separated list of file names to be skipped")
protected String[] ignoredFiles = { "nasa_fgs_mode_logic.als" }; // takes way too long
@Option(names = "--ssr", description = "Structure Signature Removal (SSR) mode")
protected boolean ssr;
@Option(names = "--parallel", description = "Parallel mode (use parallel streams)")
protected boolean parallel;
public Options(MainCLI cli) {
app = cli;
}
public void run() {
app.run(this);
protected void initialize() {
r = new Result();
r.options = this;
r.results = new ArrayList<CorpusResult>();
gson = new Gson();
errorCount = new AtomicInteger();
}
abstract protected CorpusResult analyzeCorpus(Printer mainPr, String corpus);
abstract protected FileResult analyzeFile(Printer mainPr, String corpus, Path p,
int index, int total);
}
package org.aminb.alloy.catalyst;
import java.io.FileNotFoundException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.time.Duration;
import java.time.Instant;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.Map.Entry;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.MailBug;
import edu.mit.csail.sdg.ast.Sig;
import edu.mit.csail.sdg.parser.CompModule;
import edu.mit.csail.sdg.parser.CompUtil;
import edu.mit.csail.sdg.translator.A4Options;
import edu.mit.csail.sdg.translator.A4Options.SatSolver;
import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
import com.google.gson.Gson;
import com.google.gson.GsonBuilder;
enum Solver {
minisat(SatSolver.MiniSatJNI),
minisatprover(SatSolver.MiniSatProverJNI),
glucose(SatSolver.GlucoseJNI),
sat4j(SatSolver.SAT4J);
public final SatSolver solver;
private Solver(SatSolver solver) {
this.solver = solver;
}
}
enum MutationKind {
ORIGINAL,
MUT_RANDOM
}
enum SolverResult {
SAT, UNSAT
}
public final class MainCLI {
private Options o;
private Result r;
private Gson gson;
private static AtomicInteger errorCount;
import picocli.CommandLine;
import picocli.CommandLine.Command;
@Command(
name = "catalyst",
version = {
"catalyst 0.1",
"Copyright (C) 2018-2019 Amin Bandali",
"License: Expat (MIT) <https://gnu.org/licenses/license-list.html#Expat>.",
"Catalyst is free software: you are free to change and redistribute it.",
"There is NO WARRANTY, to the extent permitted by law.",
"",
"Written by Amin Bandali."
},
description = "A framework for analysis/optimization of performance of Alloy models.",
customSynopsis = "@|bold catalyst|@ [OPTION] COMMAND",
mixinStandardHelpOptions = true,
showDefaultValues = true,
subcommands = { SSR.class, Mut.class })
public final class MainCLI implements Runnable {
public static void main(String[] args) {
picocli.CommandLine.run(new Options(new MainCLI()), args);
}
public void run(Options options) {
o = options;
r = new Result();
r.options = o;
r.results = new ArrayList<CorpusResult>();
gson = new GsonBuilder().setPrettyPrinting().create();
errorCount = new AtomicInteger();
// ugly workaround to load the solvers' native libraries
// right off the bat and get it over with, to avoid polluting
// stdout for the first file's first execution
new kodkod.engine.satlab.InitSolvers(Arrays.stream(o.solvers)
.map(s -> s.solver)
.toArray(SatSolver[]::new));
Printer pr;
try {
pr = new Printer(Paths.get(o.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 : o.corpora)
r.results.add(analyzeCorpus(pr, 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));
pr.ln(gson.toJson(r));
pr.close();
}
private CorpusResult analyzeCorpus(Printer mainPr, String corpus) {
CorpusResult cr = new CorpusResult();
cr.corpus_name = corpus;
cr.file_results = Collections.synchronizedList(new ArrayList<FileResult>());
mainPr.ln();
Instant start = Instant.now();
try {
List<Path> files = Files.walk(Paths.get(o.modelsDir, corpus))
.filter(Files::isRegularFile)
.collect(Collectors.toList());
cr.file_count = files.size();
mainPr.ln("number of " + corpus + " models: " + cr.file_count);
r.total_file_count += cr.file_count;
AtomicInteger i = new AtomicInteger(1);
Stream<Path> fs = o.parallel ? files.parallelStream() : files.stream();
fs.filter(p -> p.getFileName().toString().endsWith(".als"))
.filter(p -> !Arrays.asList(o.ignoredFiles).contains(p.getFileName().toString()))
.forEach(p -> cr.file_results.add(analyzeFile(mainPr, p, corpus, 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));
System.out.print(cr.error);
throw Utils.systemExit(1);
}
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));
if (o.ssr) {
long ssrs = 0, ssrc = 0;
for (FileResult fr : cr.file_results) {
ssrs += fr.ssr_result.sig_count;
ssrc += fr.ssr_result.ssr_candidate_count;
}
mainPr.ln(String.format("SSR candidates: %d/%d (%.2f%%)",
ssrc, ssrs, 100. * ssrc / ssrs));
cr.ssr_result = new SSRResult();
cr.ssr_result.sig_count = ssrs;
cr.ssr_result.ssr_candidate_count = ssrc;
}
mainPr.ln();
return cr;
}
private FileResult analyzeFile(Printer mainPr, Path p, String corpus, int index, int total) {
FileResult fr = new FileResult();
fr.file_name = p.toString();
fr.mutation_results = new ArrayList<MutationResult>();
fr.error = new ArrayList<ParseOrTypeError>();
String progress = String.format("[%d/%d]: ", index, total);
Path outputFile = Paths.get(o.resultsDir, corpus, fr.file_name.replace("/", o.outSep));
Path outputFileDebug = Paths.get(o.debugDir, corpus, fr.file_name.replace("/", o.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.error.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...");
CompModule world;
try {
world = CompUtil.parseEverything_fromFile(rep, null, fr.file_name);
} 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.error.add(new ParseOrTypeError(r.error, true));
errorCount.getAndIncrement();
return fr;
}
if (o.ssr) { // if we're in SSR mode
fr.ssr_result = detectRemovableSigs(world);
mainPr.ln(progress + "done: " + fr.file_name);
pr.close();
return fr;
}
if (moduleHasCommands(world)) {
pr.ln(o.mutationCount + 1);
pr.lnd(" number of executions: " + (o.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));
} 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.error.add(new ParseOrTypeError(r.error, true));
errorCount.getAndIncrement();
return fr;
}
pr.lnd(" done...");
for (int i = 1; i <= o.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));
} 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.error.add(new ParseOrTypeError(r.error, 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();
return fr;
}
private SSRResult detectRemovableSigs(CompModule world) {
SSRVisitor v = new SSRVisitor();
world.visitExpressions(v);
SSRResult r = new SSRResult();
r.sig_count = v.candidates.size();
r.ssr_candidate_count = Collections.frequency(v.candidates.values(), true);
// System.out.println("SSR candidates: " + v.candidates);
// System.out.println();
return r;
}
private static boolean moduleHasCommands(CompModule module) {
return module.getAllCommands().size() > 0;
System.exit(new CommandLine(new MainCLI()).execute(args));
}
private class RunReporter extends A4Reporter {
public Run run = new Run();
@Override
public void resultSAT(Object command, long solvingTime, Object solution) {
RunResult res = new RunResult();
res.result = SolverResult.SAT;
res.solving_time = solvingTime;
run.takes.add(res);
}
@Override
public void resultUNSAT(Object command, long solvingTime, Object solution) {
RunResult res = new RunResult();
res.result = SolverResult.UNSAT;
res.solving_time = solvingTime;
run.takes.add(res);
}
public void run () {
new CommandLine(new MainCLI()).usage(System.out);
}
private MutationResult mutateModule(Printer pr, 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
for (Solver solver : o.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;
Stream<edu.mit.csail.sdg.ast.Command> cs = o.parallel ?
module.getAllCommands().parallelStream() : module.getAllCommands().stream();
cs.forEach(c -> {
RunReporter rep = new RunReporter();
Run run = new Run();
run.solver_id = solver.solver.id();
run.solver_name = solver.solver.toString();
run.command = c.toString();
run.takes = Collections.synchronizedList(new ArrayList<RunResult>());
rep.run = run;
IntStream is = o.parallel ?
IntStream.range(0, 3).parallel() : IntStream.range(0, 3);
is.forEach(i -> {
TranslateAlloyToKodkod.execute_command(rep, allReachableSigs, c, options);
});
mr.runs.add(run);
});
Instant stop = Instant.now();
long elapsed = Duration.between(start, stop).toMillis();
pr.noln(elapsed);
if(++s_i == o.solvers.length) // if this is the last solver
pr.ln();
else
pr.noln(",");
pr.lnd(" all commands: " + elapsed + "ms");
}
return mr;
}
private static void shuffleSigs(CompModule module) {
List<Entry<String,Sig>> sigs = new ArrayList<>();
for (Entry<String,Sig> e : module.getAllSigsMap().entrySet()) {
sigs.add(e);
}
module.getAllSigsMap().clear();
Collections.shuffle(sigs);
for (Entry<String,Sig> e : sigs) {
module.getAllSigsMap().put(e.getKey(), e.getValue());
}
}
}
package org.aminb.alloy.catalyst;
import java.io.FileNotFoundException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.time.Duration;
import java.time.Instant;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.Map.Entry;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.MailBug;
import edu.mit.csail.sdg.ast.Sig;
import edu.mit.csail.sdg.parser.CompModule;
import edu.mit.csail.sdg.parser.CompUtil;
import edu.mit.csail.sdg.translator.A4Options;
import edu.mit.csail.sdg.translator.A4Options.SatSolver;
import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
import com.google.gson.GsonBuilder;
import picocli.CommandLine.Command;
import picocli.CommandLine.Option;
enum Solver {
minisat(SatSolver.MiniSatJNI),
minisatprover(SatSolver.MiniSatProverJNI),
glucose(SatSolver.GlucoseJNI),
sat4j(SatSolver.SAT4J);
public final SatSolver solver;
private Solver(SatSolver solver) {
this.solver = solver;
}
}
enum MutationKind {
ORIGINAL,
MUT_RANDOM
}
enum SolverResult {
SAT, UNSAT
}
@Command(name = "mut", description = "Mutation analysis mode")
public final class Mut extends CatalystCommand implements Runnable {
@Option(names = "--mutation-count",
description = "Number of mutations to generate per Alloy file")
protected int mutationCount = 3;
public Mut() {}
public void run() {
initialize();
gson = new GsonBuilder().setPrettyPrinting().create();
// ugly workaround to load the solvers' native libraries
// right off the bat and get it over with, to avoid polluting
// stdout for the fir