Commit b200f82a authored by Alexander Weigl's avatar Alexander Weigl
Browse files

replace GenRAP

Extension for generating run all proves unit tests.
Helps to (re-)run a specific proof.
parent 257466ee
......@@ -109,6 +109,16 @@ task testRunAllProofs(type: Test) {
}
}
task generateRunAllProofs(type: JavaExec) {
//Test runtime
classpath = sourceSets.test.runtimeClasspath
main = "de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests"
args "$buildDir/generated-src/rap-unittests/test"
}
sourceSets.test.java.srcDir "$buildDir/generated-src/rap-unittests/test"
//Generation of the three version files within the resources by executing `git'.
task generateVersionFiles() {
def outputFolder = file("build/resources/main/de/uka/ilkd/key/util")
......
package de.uka.ilkd.key.proof.runallproofs;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile;
import java.io.File;
import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Generation of test cases (JUnit) for given proof collection files.
* <p>
* This class is intended to be called from gradle. See the gradle task
* {@code generateRunAllProofs}.
* <p>
* The considered proof collections files are configured
* statically in {@link #collections}.
*
* @author Alexander Weigl
* @version 1 (6/14/20)
*/
public class GenerateUnitTests {
/**
* Output folder. Set on command line.
*/
private static String outputFolder;
/**
* List of considered proofs collections.
*/
private final static String[] collections = new String[]{
RunAllProofsFunctional.INDEX_FILE,
RunAllProofsInfFlow.INDEX_FILE
};
public static void main(String[] args) throws IOException {
if (args.length != 1) {
System.err.println("Usage: <main> <ouput-folder>");
System.exit(1);
}
outputFolder = args[0];
log("Output folder %s%n", outputFolder);
File out = new File(outputFolder);
out.mkdirs();
for (String index : collections) {
log("Index file: %s", index);
ProofCollection col = RunAllProofsTest.parseIndexFile(index);
for (RunAllProofsTestUnit unit : col.createRunAllProofsTestUnits()) {
createUnitClass(col, unit);
}
}
}
private static final String TEMPLATE_CONTENT = "package $packageName;\n" +
"\n" +
"import org.junit.*;\n" +
//"import de.uka.ilkd.key.util.NamedRunner;\n" +
//"import de.uka.ilkd.key.util.TestName;\n" +
"import org.junit.rules.Timeout;\n" +
"import org.junit.runner.RunWith;\n" +
"\n" +
//"@org.junit.experimental.categories.Category(org.key_project.util.testcategories.ProofTestCategory.class)\n" +
//"@RunWith(NamedRunner.class)\n" +
"public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest {\n" +
"\n" +
" @Before public void setUp() {\n" +
" this.baseDirectory = \"$baseDirectory\";\n" +
" this.statisticsFile = \"$statisticsFile\";\n" +
" this.name = \"$name\";\n" +
" this.reloadEnabled = $reloadEnabled;\n" +
" this.tempDir = \"$tempDir\";\n" +
"\n" +
" this.globalSettings = \"$keySettings\";\n" +
" this.localSettings = \"$localSettings\";\n" +
" }\n" +
"\n" +
" $timeout\n" +
"\n" +
" $methods\n" +
"\n" +
"}\n";
/**
* Generates the test classes for the given proof collection,
* and writes the java files.
*
* @param col
* @param unit
* @throws IOException if the file is not writable
*/
private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit unit) throws IOException {
String packageName = "de.uka.ilkd.key.proof.runallproofs";
String name = unit.getTestName();
String className = name
.replaceAll("\\.java", "")
.replaceAll("\\.key", "")
.replaceAll("[^a-zA-Z0-9]+", "_");
ProofCollectionSettings settings = unit.getSettings();
Map<String, String> vars = new TreeMap<>();
vars.put("className", className);
vars.put("packageName", packageName);
vars.put("baseDirectory", settings.getBaseDirectory().getAbsolutePath());
vars.put("statisticsFile", settings.getStatisticsFile().getStatisticsFile().getAbsolutePath());
vars.put("name", name);
vars.put("reloadEnabled", String.valueOf(settings.reloadEnabled()));
vars.put("tempDir", settings.getTempDir().getAbsolutePath());
vars.put("globalSettings", settings.getGlobalKeYSettings()
.replace("\n", "\\n"));
vars.put("localSettings", (
settings.getLocalKeYSettings() == null ? "" : settings.getLocalKeYSettings())
.replace("\n", "\\n"));
vars.put("timeout", "");
if (false) {// disabled
int globalTimeout = 0;
if (globalTimeout > 0)
vars.put("timeout", "@Rule public Timeout globalTimeout = Timeout.seconds(" + globalTimeout + ");");
}
StringBuilder methods = new StringBuilder();
Set<String> usedMethodNames = new TreeSet<>();
int clashCounter = 0;
for (TestFile<?> file : unit.getTestFiles()) {
File keyFile = file.getKeYFile();
String testName = keyFile.getName()
.replaceAll("\\.java", "")
.replaceAll("\\.key", "")
.replaceAll("[^a-zA-Z0-9]+", "_");
if (usedMethodNames.contains(testName)) {
testName += "_" + (++clashCounter);
}
usedMethodNames.add(testName);
//int timeout = 0; (timeout <= 0 ? parent.timeout : 0)
String to = ""; //timeout > 0 ? "timeout=${1000 * timeout}" : "";
methods.append("\n");
methods.append("@Test(").append(to).append(")")
//.append("@TestName(\"").append(keyFile.getName()).append("\")")
.append("public void test").append(testName).append("() throws Exception {\n");
// "// This tests is based on").append(keyFile.getAbsolutePath()).append("\n");
switch (file.getTestProperty()) {
case PROVABLE:
methods.append("assertProvability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
case NOTPROVABLE:
methods.append("assertUnProvability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
case LOADABLE:
methods.append("assertLoadability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
}
methods.append("}");
}
vars.put("methods", methods.toString());
Pattern regex = Pattern.compile("[$](\\w+)");
Matcher m = regex.matcher(TEMPLATE_CONTENT);
StringBuffer sb = new StringBuffer();
while (m.find()) {
String key = m.group(1);
m.appendReplacement(sb, vars.getOrDefault(key, "/*not-found*/"));
}
m.appendTail(sb);
File folder = new File(outputFolder, packageName.replace('.', '/'));
folder.mkdirs();
Files.write(Paths.get(folder.getAbsolutePath(), className + ".java"), sb.toString().getBytes());
}
private static void log(String fmt, Object... args) {
System.out.printf(">>> " + fmt + "\n", args);
}
}
package de.uka.ilkd.key.proof.runallproofs;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.macros.scripts.ProofScriptEngine;
import de.uka.ilkd.key.parser.Location;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.AbstractProblemLoader;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.StatisticsFile;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.TestProperty;
import de.uka.ilkd.key.settings.ProofSettings;
import de.uka.ilkd.key.util.Pair;
import java.io.File;
import java.io.IOException;
import java.util.List;
import static org.junit.Assert.*;
/**
* This class provides an API for running proves in JUnit test cases.
* <p>
* It is not intended to use this class outside of JUnit tests.
* The API mimics the same behavior as run-all-proves.
* So {@link #assertLoadability(String)}, {@link #assertLoadability(String)},
* and {@link #assertUnProvability(String)}
* correspond to the commands in the proof collection file.
* <p>
* Use the the member variables to configure the execution. Their meaning is identical to the variable in
* {@link de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection}.
* <p>
* This class is used by generated unit tests from the proof collections.
*
* @author Alexander Weigl
* @version 1 (12.07.19)
* @see GenerateUnitTests
*/
public class ProveTest {
protected boolean verbose = Boolean.getBoolean("prooftests.verbose");
protected String baseDirectory = "";
protected String statisticsFile = "tmp.csv";
protected String name = "unnamed_tests";
protected boolean reloadEnabled = false;
protected String tempDir = "/tmp";
protected String globalSettings = "";
protected String localSettings = "";
private StatisticsFile statistics;
protected void assertProvability(String file) throws Exception {
runKey(file, TestProperty.PROVABLE);
}
protected void assertUnProvability(String file) throws Exception {
runKey(file, TestProperty.NOTPROVABLE);
}
protected void assertLoadability(String file) throws Exception {
runKey(file, TestProperty.LOADABLE);
}
private void runKey(String file, TestProperty testProperty) throws Exception {
// Initialize KeY settings.
ProofSettings.DEFAULT_SETTINGS.loadSettingsFromString(globalSettings);
if (localSettings != null && !"".equals(localSettings)) {
// local settings must be complete to have desired effect
ProofSettings.DEFAULT_SETTINGS.loadSettingsFromString(localSettings);
}
File keyFile = new File(file);
assertTrue("File " + keyFile + " does not exists", keyFile.exists());
// Name resolution for the available KeY file.
debugOut("Now processing file %s", keyFile);
// File that the created proof will be saved to.
File proofFile = new File(keyFile.getAbsolutePath() + ".proof");
KeYEnvironment<DefaultUserInterfaceControl> env = null;
Proof loadedProof = null;
boolean success = false;
try {
// Initialize KeY environment and load proof.
Pair<KeYEnvironment<DefaultUserInterfaceControl>, Pair<String, Location>> pair = load(keyFile);
env = pair.first;
Pair<String, Location> script = pair.second;
loadedProof = env.getLoadedProof();
AbstractProblemLoader.ReplayResult replayResult = env.getReplayResult();
if (replayResult.hasErrors() && verbose) {
System.err.println("... error(s) while loading");
for (Throwable error : replayResult.getErrorList()) {
error.printStackTrace();
}
}
assertFalse("Loading problem file failed", replayResult.hasErrors());
// For a reload test we are done at this point. Loading was successful.
if (testProperty == TestProperty.LOADABLE) {
success = true;
debugOut("... success: loaded");
} else {
autoMode(env, loadedProof, script);
success = (testProperty == TestProperty.PROVABLE) == loadedProof.closed();
debugOut("... finished proof: " + (success ? "closed." : "open goal(s)"));
appendStatistics(loadedProof, keyFile);
if (success) reload(proofFile, loadedProof);
}
} finally {
if (loadedProof != null) {
loadedProof.dispose();
}
if (env != null) {
env.dispose();
}
}
String message = String.format("%sVerifying property \"%s\"%sfor file: %s",
success ? "pass: " : "FAIL: ",
testProperty.toString().toLowerCase(),
success ? " was successful " : " failed ",
keyFile.toString());
if (!success) {
fail(message);
}
}
/**
* Override this method in order to change reload behaviour.
*/
private void reload(File proofFile, Proof loadedProof) throws Exception {
if (reloadEnabled) {
System.err.println("Test reloadability.");
// Save the available proof to a temporary file.
loadedProof.saveToFile(proofFile);
boolean reloadedClosed = reloadProof(proofFile);
assertEquals("Reloaded proof did not close: " + proofFile,
loadedProof.closed(), reloadedClosed);
debugOut("... success: reloaded.");
}
}
/**
* By overriding this method we can change the way how we invoke automode,
* for instance if we want to use a different strategy.
*/
private void autoMode(KeYEnvironment<DefaultUserInterfaceControl> env, Proof loadedProof,
Pair<String, Location> script) throws Exception {
// Run KeY prover.
if (script == null) {
// auto mode
env.getProofControl().startAndWaitForAutoMode(loadedProof);
} else {
// ... script
ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second);
pse.execute(env.getUi(), env.getLoadedProof());
}
}
/*
* has resemblances with KeYEnvironment.load ...
*/
private Pair<KeYEnvironment<DefaultUserInterfaceControl>, Pair<String, Location>> load(File keyFile) throws ProblemLoaderException, ProofInputException {
KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(keyFile);
return new Pair<>(env, env.getProofScript());
}
/**
* Reload proof that was previously saved at the location corresponding to
* the given {@link File} object.
*
* @param proofFile File that contains the proof that will be (re-)loaded.
*/
private boolean reloadProof(File proofFile) throws Exception {
/*
* Reload proof and dispose corresponding KeY environment immediately
* afterwards. If no exception is thrown it is assumed that loading works
* properly.
*/
KeYEnvironment<DefaultUserInterfaceControl> proofLoadEnvironment = null;
Proof reloadedProof = null;
try {
proofLoadEnvironment = KeYEnvironment.load(proofFile);
AbstractProblemLoader.ReplayResult result = proofLoadEnvironment.getReplayResult();
if (result.hasErrors()) {
List<Throwable> errorList = result.getErrorList();
for (Throwable ex : errorList) {
ex.printStackTrace();
}
throw errorList.get(0);
}
reloadedProof = proofLoadEnvironment.getLoadedProof();
return reloadedProof.closed();
} catch (Throwable t) {
throw new Exception(
"Exception while loading proof (see cause for details): "
+ proofFile, t);
} finally {
if (reloadedProof != null) {
reloadedProof.dispose();
}
if (proofLoadEnvironment != null) {
proofLoadEnvironment.dispose();
}
}
}
private StatisticsFile getStatisticsFile() {
if (!statisticsFile.isEmpty()) {
if (statistics == null) statistics = new StatisticsFile(new File(statisticsFile));
return statistics;
}
return null;
}
private void appendStatistics(Proof loadedProof, File keyFile) {
// Write statistics.
StatisticsFile statisticsFile = getStatisticsFile();
if (statisticsFile != null) {
try {
statisticsFile.appendStatistics(loadedProof, keyFile);
} catch (IOException e) {
e.printStackTrace();
}
}
}
private void debugOut(String format, Object... args) {
if (verbose) {
System.err.format(format, args);
}
}
}
\ No newline at end of file
......@@ -151,4 +151,12 @@ public final class RunAllProofsTestUnit implements Serializable {
}
return tempDir;
}
public List<TestFile> getTestFiles() {
return testFiles;
}
public ProofCollectionSettings getSettings() {
return settings;
}
}
......@@ -349,4 +349,7 @@ public class StatisticsFile implements Serializable {
boolean proofClosed);
}
public File getStatisticsFile() {
return statisticsFile;
}
}
......@@ -325,4 +325,7 @@ public class TestFile<Directories extends RunAllProofsDirectories> implements Se
return settings;
}
public TestProperty getTestProperty() {
return testProperty;
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment