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

Merge branch 'weigl/testgen' into 'master'

Testgen UI via UI extension

The module `key.core.testgen` is currently not maintained. This MR lowers the dependencies of `key.ui` to this module, allowing an easy removal of `key.core.testgen` in the future.

This MR refactors out the classes depending on `key.core.testgen` in `key.ui` into a separate module `keyext.ui.testgen`. I also fixed the errors and smells identified by SonarQube.

**All features of testgen are still available in KeY ui.**

## Changes

* New gradle module `keyext.ui.testgen`
  * containing the old classes for actions, settings panel etc. from `key.ui`
  * `KeyGuiExtension` implementation to provide main-menu entries and toolbar.
* Change the dependency from `compile 'key.core.testgen` to `runtimeOnly 'keyext.ui.testgen`.

See merge request key/key!324
parents 030a6c71 66838c2d
......@@ -56,6 +56,14 @@ sonarqube {
}
}
sonarqube {
properties {
property "sonar.projectKey", "key-main"
property "sonar.organization", "keyproject"
property "sonar.host.url", "https://sonarcloud.io"
}
}
subprojects {
apply plugin: "java"
apply plugin: "java-library"
......
......@@ -14,149 +14,144 @@ import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.RuleApp;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
import de.uka.ilkd.key.settings.TestGenerationSettings;
import de.uka.ilkd.key.strategy.NumberRuleAppCost;
import de.uka.ilkd.key.strategy.RuleAppCost;
import de.uka.ilkd.key.strategy.Strategy;
public class TestGenMacro extends StrategyProofMacro {
/**
* The Class FilterAppManager is a special strategy assigning to any rule
* infinite costs if the goal has no modality
*/
private static class TestGenStrategy extends FilterStrategy {
private static final Name NAME = new Name(
TestGenStrategy.class.getSimpleName());
private static final Set<String> unwindRules;
private static final int UNWIND_COST = 1000;
private final int limit;
static {
unwindRules = new HashSet<String>();
TestGenStrategy.unwindRules.add("loopUnwind");
TestGenStrategy.unwindRules.add("doWhileUnwind");
TestGenStrategy.unwindRules.add("methodCall");
TestGenStrategy.unwindRules.add("methodCallWithAssignment");
TestGenStrategy.unwindRules.add("staticMethodCall");
TestGenStrategy.unwindRules.add("staticMethodCallWithAssignment");
}
private static boolean isUnwindRule(Rule rule) {
if (rule == null) {
return false;
}
final String name = rule.name().toString();
return TestGenStrategy.unwindRules.contains(name);
}
@Override
protected Strategy createStrategy(Proof proof,
PosInOccurrence posInOcc) {
return new TestGenStrategy(proof
.getActiveStrategy());
}
public TestGenStrategy(Strategy delegate) {
super(delegate);
limit = ProofIndependentSettings.DEFAULT_INSTANCE
.getTestGenerationSettings().getMaximalUnwinds();
}
@Override
public String getDescription() {
return "Finish symbolic execution but restrict loop unwinding.";
}
@Override
public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
Goal goal) {
if (TestGenStrategy.isUnwindRule(app.rule())) {
return NumberRuleAppCost.create(TestGenStrategy.UNWIND_COST);
}
return super.computeCost(app, pio, goal);
}
@Override
public String getName() {
return "TestGen (finite loop unwinding)";
}
private int computeUnwindRules(Goal goal) {
int totalUnwinds = 0;
Node node = goal.node();
while (!node.root()) {
final RuleApp app = node.getAppliedRuleApp();
if (app != null) {
final Rule rule = app.rule();
if (TestGenStrategy.isUnwindRule(rule)) {
++totalUnwinds;
}
}
node = node.parent();
}
return totalUnwinds;
}
@Override
public String getCategory() {
return null;
}
@Override
public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) {
if (!TestGenMacro.hasModality(goal.node())) {
return false;
}
if (TestGenStrategy.isUnwindRule(app.rule())) {
// System.out.println("Found unwind rule!!");
final int unwindRules = computeUnwindRules(goal);
// System.out.println(unwindRules);
if (unwindRules >= limit) {
return false;
} else {
return true;
}
}
return super.isApprovedApp(app, pio, goal);
}
@Override
public Name name() {
return TestGenStrategy.NAME;
}
}
@Override
public boolean isStopAtFirstNonCloseableGoal() {
return false;
}
/**
* The Class FilterAppManager is a special strategy assigning to any rule
* infinite costs if the goal has no modality
*/
class TestGenStrategy extends FilterStrategy {
private static final Name NAME = new Name(
TestGenStrategy.class.getSimpleName());
private static final Set<String> unwindRules;
private static final int UNWIND_COST = 1000;
private final int limit;
static {
unwindRules = new HashSet<>();
TestGenStrategy.unwindRules.add("loopUnwind");
TestGenStrategy.unwindRules.add("doWhileUnwind");
TestGenStrategy.unwindRules.add("methodCall");
TestGenStrategy.unwindRules.add("methodCallWithAssignment");
TestGenStrategy.unwindRules.add("staticMethodCall");
TestGenStrategy.unwindRules.add("staticMethodCallWithAssignment");
}
/*
* find a modality term in a node
* recursively descent into the term to detect a modality.
*/
private static boolean hasModality(Node node) {
final Sequent sequent = node.sequent();
for (final SequentFormula sequentFormula : sequent) {
if (TestGenMacro.hasModality(sequentFormula.formula())) {
private static boolean hasModality(Term term) {
if (term.op() instanceof Modality) {
return true;
}
for (final Term sub : term.subs()) {
if (hasModality(sub)) {
return true;
}
}
return false;
}
/*
* recursively descent into the term to detect a modality.
* find a modality term in a node
*/
private static boolean hasModality(Term term) {
if (term.op() instanceof Modality) {
return true;
}
for (final Term sub : term.subs()) {
if (TestGenMacro.hasModality(sub)) {
private static boolean hasModality(Node node) {
final Sequent sequent = node.sequent();
for (final SequentFormula sequentFormula : sequent) {
if (hasModality(sequentFormula.formula())) {
return true;
}
}
return false;
}
@Override
protected Strategy createStrategy(Proof proof,
PosInOccurrence posInOcc) {
return new TestGenStrategy(proof
.getActiveStrategy());
private static boolean isUnwindRule(Rule rule) {
if (rule == null) {
return false;
}
final String name = rule.name().toString();
return TestGenStrategy.unwindRules.contains(name);
}
@Override
public String getDescription() {
return "Finish symbolic execution but restrict loop unwinding.";
public TestGenStrategy(Strategy delegate) {
super(delegate);
limit = TestGenerationSettings.getInstance().getMaximalUnwinds();
}
@Override
public String getName() {
return "TestGen (finite loop unwinding)";
public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
Goal goal) {
if (TestGenStrategy.isUnwindRule(app.rule())) {
return NumberRuleAppCost.create(TestGenStrategy.UNWIND_COST);
}
return super.computeCost(app, pio, goal);
}
private int computeUnwindRules(Goal goal) {
int totalUnwinds = 0;
Node node = goal.node();
while (!node.root()) {
final RuleApp app = node.getAppliedRuleApp();
if (app != null) {
final Rule rule = app.rule();
if (TestGenStrategy.isUnwindRule(rule)) {
++totalUnwinds;
}
}
node = node.parent();
}
return totalUnwinds;
}
@Override
public String getCategory() {
return null;
public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) {
if (!hasModality(goal.node())) {
return false;
}
if (TestGenStrategy.isUnwindRule(app.rule())) {
final int noUnwindRules = computeUnwindRules(goal);
return noUnwindRules < limit;
}
return super.isApprovedApp(app, pio, goal);
}
@Override
public Name name() {
return TestGenStrategy.NAME;
}
@Override
public boolean isStopAtFirstNonCloseableGoal() {
return false;
}
}
package de.uka.ilkd.key.settings;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import java.io.File;
import java.util.Collection;
import java.util.EventObject;
import java.util.LinkedHashSet;
import java.util.Properties;
public class TestGenerationSettings implements Settings, Cloneable {
//region Default Values for option fields
private static final boolean DEFAULT_APPLYSYMBOLICEX = false;
private static final int DEFAULT_MAXUNWINDS = 3;
private static final int DEFAULT_CONCURRENTPROCESSES = 1;
private static final String DEFAULT_OUTPUTPATH = System.getProperty("user.home") + File.separator + "testFiles";
private static final boolean DEFAULT_REMOVEDUPLICATES = true;
private static final boolean DEFAULT_USERFL = false;
private static final boolean DEFAULT_USEJUNIT = false;
private static final boolean DEFAULT_INVARIANTFORALL = true;
private static final String DEFAULT_OPENJMLPATH = ".";
private static final String DEFAULT_OBJENESISPATH = ".";
private static final boolean DEFAULT_INCLUDEPOSTCONDITION = false;
//endregion
// region property names
private static final String PROP_APPLY_SYMBOLIC_EXECUTION = "[TestGenSettings]applySymbolicExecution";
private static final String PROP_MAX_UWINDS = "[TestGenSettings]maxUnwinds";
private static final String PROP_OUTPUT_PATH = "[TestGenSettings]OutputPath";
private static final String PROP_REMOVE_DUPLICATES = "[TestGenSettings]RemoveDuplicates";
private static final String PROP_USE_RFL = "[TestGenSettings]UseRFL";
private static final String PROP_USE_JUNIT = "[TestGenSettings]UseJUnit";
private static final String PROP_CONCURRENT_PROCESSES = "[TestGenSettings]ConcurrentProcesses";
private static final String PROP_INVARIANT_FOR_ALL = "[TestGenSettings]InvariantForAll";
private static final String PROP_OPENJML_PATH = "[TestGenSettings]OpenJMLPath";
private static final String PROP_OBJENESIS_PATH = "[TestGenSettings]ObjenesisPath";
private static final String PROP_INCLUDE_POST_CONDITION = "[TestGenSettings]IncludePostCondition";
//endregion
private final Collection<SettingsListener> listeners;
// Option fields
private boolean applySymbolicExecution;
private int maxUnwinds;
private String outputPath;
private String openjmlPath;
private String objenesisPath;
private boolean removeDuplicates;
private boolean useRFL;
private boolean useJunit;
private int concurrentProcesses;
private boolean invariantForAll;
private boolean includePostCondition;
public TestGenerationSettings() {
listeners = new LinkedHashSet<>();
applySymbolicExecution = TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX;
maxUnwinds = TestGenerationSettings.DEFAULT_MAXUNWINDS;
outputPath = TestGenerationSettings.DEFAULT_OUTPUTPATH;
removeDuplicates = TestGenerationSettings.DEFAULT_REMOVEDUPLICATES;
useRFL = TestGenerationSettings.DEFAULT_USERFL;
useJunit = TestGenerationSettings.DEFAULT_USEJUNIT;
concurrentProcesses = TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES;
invariantForAll = TestGenerationSettings.DEFAULT_INVARIANTFORALL;
openjmlPath = DEFAULT_OPENJMLPATH;
objenesisPath = DEFAULT_OBJENESISPATH;
includePostCondition = DEFAULT_INCLUDEPOSTCONDITION;
}
public TestGenerationSettings(TestGenerationSettings data) {
listeners = new LinkedHashSet<>();
listeners.addAll(data.listeners);
applySymbolicExecution = data.applySymbolicExecution;
maxUnwinds = data.maxUnwinds;
outputPath = data.outputPath;
removeDuplicates = data.removeDuplicates;
useJunit = data.useJunit;
useRFL = data.useRFL;
concurrentProcesses = data.concurrentProcesses;
invariantForAll = data.invariantForAll;
openjmlPath = data.openjmlPath;
objenesisPath = data.objenesisPath;
includePostCondition = data.includePostCondition;
}
@Override
public void addSettingsListener(SettingsListener l) {
listeners.add(l);
}
//FIXME weigl: This method seems broken. I would expect: clone() = new TGS(this)
public TestGenerationSettings clone(TestGenerationSettings data) {
return new TestGenerationSettings(data);
}
public void fireSettingsChanged() {
for (final SettingsListener aListenerList : listeners) {
aListenerList.settingsChanged(new EventObject(this));
}
}
public boolean getApplySymbolicExecution() {
return applySymbolicExecution;
}
public void setApplySymbolicExecution(boolean applySymbolicExecution) {
this.applySymbolicExecution = applySymbolicExecution;
}
public int getMaximalUnwinds() {
return maxUnwinds;
}
public int getNumberOfProcesses() {
return concurrentProcesses;
}
public String getOutputFolderPath() {
return outputPath;
}
public boolean invariantForAll() {
return invariantForAll;
}
public boolean includePostCondition() {
return includePostCondition;
}
@Override
public void readSettings(Properties props) {
applySymbolicExecution = SettingsConverter.read(props,
TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX);
maxUnwinds = SettingsConverter.read(props,
TestGenerationSettings.PROP_MAX_UWINDS,
TestGenerationSettings.DEFAULT_MAXUNWINDS);
outputPath = SettingsConverter.read(props,
TestGenerationSettings.PROP_OUTPUT_PATH,
TestGenerationSettings.DEFAULT_OUTPUTPATH);
removeDuplicates = SettingsConverter.read(props,
TestGenerationSettings.PROP_REMOVE_DUPLICATES,
TestGenerationSettings.DEFAULT_REMOVEDUPLICATES);
useRFL = SettingsConverter.read(props,
TestGenerationSettings.PROP_USE_RFL,
TestGenerationSettings.DEFAULT_USERFL);
useJunit = SettingsConverter.read(props,
TestGenerationSettings.PROP_USE_JUNIT,
TestGenerationSettings.DEFAULT_USEJUNIT);
concurrentProcesses = SettingsConverter.read(props,
TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES);
invariantForAll = SettingsConverter.read(props,
TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
TestGenerationSettings.DEFAULT_INVARIANTFORALL);
openjmlPath = SettingsConverter.read(props,
TestGenerationSettings.PROP_OPENJML_PATH,
TestGenerationSettings.DEFAULT_OPENJMLPATH);
objenesisPath = SettingsConverter.read(props,
TestGenerationSettings.PROP_OBJENESIS_PATH,
TestGenerationSettings.DEFAULT_OBJENESISPATH);
includePostCondition = SettingsConverter.read(props,
TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
TestGenerationSettings.DEFAULT_INCLUDEPOSTCONDITION);
}
public boolean removeDuplicates() {
return removeDuplicates;
}
public void setConcurrentProcesses(int concurrentProcesses) {
this.concurrentProcesses = concurrentProcesses;
}
public void setInvariantForAll(boolean invariantForAll) {
this.invariantForAll = invariantForAll;
}
public void setMaxUnwinds(int maxUnwinds) {
this.maxUnwinds = maxUnwinds;
}
public void setOutputPath(String outputPath) {
this.outputPath = outputPath;
}
public void setRemoveDuplicates(boolean removeDuplicates) {
this.removeDuplicates = removeDuplicates;
}
public void setIncludePostCondition(boolean includePostCondition) {
this.includePostCondition = includePostCondition;
}
public void setRFL(boolean useRFL) {
this.useRFL = useRFL;
}
public void setUseJunit(boolean useJunit) {
this.useJunit = useJunit;
}
public String getObjenesisPath() {
return objenesisPath;
}
public void setObjenesisPath(String objenesisPath) {
this.objenesisPath = objenesisPath;
}
public String getOpenjmlPath() {
return openjmlPath;
}
public void setOpenjmlPath(String openjmlPath) {
this.openjmlPath = openjmlPath;
}
public boolean useRFL() {
return useRFL;
}
public boolean useJunit() {
return useJunit;
}
@Override
public void writeSettings(Properties props) {
SettingsConverter.store(props,
TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
applySymbolicExecution);
SettingsConverter.store(props,
TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
concurrentProcesses);
SettingsConverter.store(props,
TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
invariantForAll);
SettingsConverter.store(props, TestGenerationSettings.PROP_MAX_UWINDS,
maxUnwinds);
SettingsConverter.store(props, TestGenerationSettings.PROP_OUTPUT_PATH,
outputPath);
SettingsConverter.store(props,
TestGenerationSettings.PROP_REMOVE_DUPLICATES,
removeDuplicates);
SettingsConverter.store(props,
TestGenerationSettings.PROP_USE_RFL,
useRFL);
SettingsConverter.store(props, TestGenerationSettings.PROP_USE_JUNIT,
useJunit);
SettingsConverter.store(props, TestGenerationSettings.PROP_OPENJML_PATH,
openjmlPath);
SettingsConverter.store(props, TestGenerationSettings.PROP_OBJENESIS_PATH,
objenesisPath);
SettingsConverter.store(props, TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
includePostCondition);
}
public void set(TestGenerationSettings settings) {
Properties p = new Properties();
settings.writeSettings(p);
readSettings(p);
}
private static @Nullable TestGenerationSettings instance;
public static @NotNull TestGenerationSettings getInstance() {
if (instance == null) {
instance = new TestGenerationSettings();
ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(instance);
}
return instance;
}
}
package de.uka.ilkd.key.smt.testgen;
import java.util.Arrays;
import java.util.Collection;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Vector;
import java.io.IOException;
import java.util.*;
import org.key_project.util.collection.ImmutableList;
......@@ -59,23 +55,22 @@ public abstract class AbstractTestGenerator {
private final Proof originalProof;
private SolverLauncher launcher;
private List<Proof> proofs;
/**
* Constructor.
* @param ui The {@link UserInterfaceControl} to use.
* @param originalProof The {@link Proof} to generate test cases for.
*/
public AbstractTestGenerator(UserInterfaceControl ui, Proof originalProof) {
protected AbstractTestGenerator(UserInterfaceControl ui, Proof originalProof) {