Commit 09d26df9 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'master' into weigl/kp2

* master:
  fixing settings dialog glitches
  RunAllProofs in UI
  Refactoring of the testgen UI into separate module to reduce the compile dependency.
  add textareas to the settings dialog
  Fixing some smaller GUI glitches in settings dialog
  fixing smaller issues with the settings GUI

# Conflicts:
#	key/settings.gradle
parents b6b30869 09f80284
......@@ -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) {