Commit 40b9de37 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Merge remote-tracking branch 'origin/grebing_luong_workbranch' into grebing_luong_workbranch

parents 27c503a0 90a2cd22
# This is the Gradle build system for JVM applications
# https://gradle.org/
# https://github.com/gradle/gradle
image: key-dev-jdk10
image: key-dev-jdk8
cache:
paths:
......@@ -13,9 +13,7 @@ cache:
# runtime for each build is more reliable since the runtime is completely
# isolated from any previous builds.
variables:
GRADLE_OPTS: "-Dorg.gradle.daemon=false \
--add-modules java.xml.bind \
'-Dorg.gradle.jvmargs=--add-modules java.xml.bind'"
GRADLE_OPTS: "-Dorg.gradle.daemon=false"
GIT_SSL_NO_VERIFY: "true"
before_script:
......@@ -28,32 +26,6 @@ stages:
- test
- deploy
build:jdk9:
stage: build
image: key-dev-jdk9
script: gradle --build-cache assemble
allow_failure: true
cache:
key: "$CI_COMMIT_REF_NAME"
policy: push
paths:
- build
- .gradle
build:jdk10:
stage: build
image: key-dev-jdk10
script: gradle --build-cache assemble
allow_failure: true
cache:
key: "$CI_COMMIT_REF_NAME"
policy: push
paths:
- build
- .gradle
build:jdk8:
stage: build
variables:
......
......@@ -177,7 +177,7 @@ public class KeYProofFacade {
* Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
*/
public InterpreterBuilder buildInterpreter() {
assert readyToExecute.getValue();
//weigl: duplicate with next line: assert readyToExecute.getValue();
assert getEnvironment() != null && getProof() != null : "No proof loaded";
InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
interpreterBuilder
......
......@@ -4,6 +4,8 @@ import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import lombok.Getter;
import lombok.Setter;
import org.apache.commons.io.IOUtils;
import java.io.*;
......@@ -11,26 +13,18 @@ import java.net.URL;
import java.nio.charset.Charset;
/**
* Under construction!!!!!!
* @author Alexander Weigl
*/
public class JavaExample extends Example {
private URL projectFile;
public void setJavaFile(URL javaFile) {
this.javaFile = javaFile;
}
//public void setProjectFile(URL projectFile){this.projectFile = projectFile;}
@Getter
@Setter
protected URL javaFile;
@Getter
@Setter
protected URL settingsFile;
public void setSettingsFile(URL settingsFile) {
this.settingsFile = settingsFile;
}
@Getter
@Setter
private URL projectFile;
@Override
public void open(DebuggerMain debuggerMain) {
......
package edu.kit.iti.formal.psdbg.examples.java.sumPositive;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class SumPositiveExample extends JavaExample {
public SumPositiveExample () {
setName("SumPositive example");
setJavaFile(getClass().
getResource("SumPositive.java"));
setScriptFile(getClass().
getResource("script.kps"));
}
}
......@@ -310,9 +310,9 @@ public class ScriptTreeGraph {
if(branchlabel.size() != 0) {
//TODO: remove
System.out.println("_______Branchlabels");
Lists.reverse(branchlabel).forEach(k -> System.out.println(k.getNode().serialNr() + " " + k.getLabelName()));
Lists.reverse(branchlabel).forEach(k ->
System.out.println(k.getNode().serialNr() + " " + k.getLabelName()));
insertBranchLabels(callnode, branchlabel);
addPlaceholder(branchlabel.get(0), gn.getData().getNode());
......@@ -500,7 +500,6 @@ public class ScriptTreeGraph {
ptn,
ptn.getStatement().getStartPosition().getLineNumber(),
false);
//TODO: replacePlaceholder(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), ftn);
replacePlaceholder(n, ftn);
addPlaceholder(ftn, n);
......@@ -509,6 +508,12 @@ public class ScriptTreeGraph {
}
}
/**
* Get all Branchlabels from child to parent GoalNode
* @param parent
* @param child
* @return
*/
private List<BranchLabelNode> getBranchLabels(GoalNode<KeyData> parent, GoalNode<KeyData> child) {
List<BranchLabelNode> branchlabels = new ArrayList<>();
Node parentnode = parent.getData().getNode();
......@@ -517,7 +522,7 @@ public class ScriptTreeGraph {
try {
while (childnode.parent() != parentnode) {
if (childnode.getNodeInfo().getBranchLabel() != null
&& isBranchLabel(childnode.getNodeInfo().getBranchLabel())&& !sameBranchlabelBefore(branchlabels, childnode))
&& isBranchLabel(childnode.getNodeInfo().getBranchLabel()) && !sameBranchlabelBefore(branchlabels, childnode))
branchlabels.add(new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
childnode = childnode.parent();
}
......@@ -527,18 +532,22 @@ public class ScriptTreeGraph {
return branchlabels;
}
private boolean sameBranchlabelBefore(List<BranchLabelNode> branchlabels, Node node) {
if(branchlabels.size() == 0) return false;
return branchlabels.get(branchlabels.size()-1).getLabelName().equals(node.getNodeInfo().getBranchLabel());
return branchlabels.get(branchlabels.size()-1).getNode().serialNr() == node.serialNr();
}
private boolean isBranchLabel(String label) {
if (label.contains("rule") || label.contains("rules")) return false;
if (label.contains("rule") || label.contains("rules") || label.equals("Normal Execution")) return false;
return true;
}
/**
* Inserts given node after Branchlabelnodes
* @param node
* @param branchlabels
*/
private void insertBranchLabels(Node node, List<BranchLabelNode> branchlabels) {
if(branchlabels == null) return;
Node topBranchNode = branchlabels.get(branchlabels.size()-1).getNode(); //start from last to first
......@@ -548,10 +557,12 @@ public class ScriptTreeGraph {
//check which Branchlabels are already in mapping -> afterwards forall x of [0,i]; branchlabels[x] not in mapping yet
if(mapping.containsKey(topBranchNode) && ((BranchLabelNode)mapping.get(topBranchNode)).getLabelName() == branchlabels.get(i).getLabelName()) {
currentChildren = mapping.get(topBranchNode).getChildren();
i--;
while (0 <= i && currentChildren != null && currentChildren.contains(branchlabels.get(i))) {
currentChildren = currentChildren.get(currentChildren.indexOf(branchlabels.get(i))).getChildren();
//check
while (0 <= i && currentChildren != null && 0 <= getIndexOfAbsNode(currentChildren, branchlabels.get(i))) {
currentChildren = currentChildren.get(getIndexOfAbsNode(currentChildren, branchlabels.get(i))).getChildren();
i--;
}
}
......@@ -571,48 +582,33 @@ public class ScriptTreeGraph {
putIntoMapping(branchlabels.get(i).getNode(), branchlabels.get(i));
}
// add parent and child relation
if (0 <= i - 1) {
BranchLabelNode child = branchlabels.get(i - 1);
BranchLabelNode parent = branchlabels.get(i);
child.setParent(parent);
addToChildren(parent.getNode(), child);
/*
if (i == branchlabels.size() - 2) {
addToChildren(node, child);
} else {
addToChildren(parent.getNode(), child);
}
*/
}
/* old implementation
mapping.put(node, branchlabels.get(branchlabels.size()-1));
for (int i = branchlabels.size() -2; 0 <= i; i--) {
//to check if Branchlabel already exists
Node n = branchlabels.get(i).getNode();
if(!mapping.containsKey(n) || mapping.get(n) != branchlabels.get(i)) {
putIntoMapping(branchlabels.get(i).getNode(), branchlabels.get(i));
if(0 <= i-1) {
BranchLabelNode child = branchlabels.get(i-1);
BranchLabelNode parent = branchlabels.get(i);
child.setParent(parent);
}
if(i == branchlabels.size() -2) {
addToChildren(node, child);
} else {
addToChildren(parent.getNode(), child);
}
}
}
/**
* Returns index of AbstractTreeNode in given list if it exists, else -1
* @param nodeList
* @param node
* @return
*/
private int getIndexOfAbsNode(List<AbstractTreeNode> nodeList, AbstractTreeNode node) {
for(int i = 0; i < nodeList.size(); i++) {
if(nodeList.get(i).getNode().serialNr() == node.getNode().serialNr()) {
return i;
}
}
*/
}
return -1;
}
private void addGoals() {
......
......@@ -5,6 +5,7 @@ edu.kit.iti.formal.psdbg.examples.java.maxtriplet.MaxTripletExample
#edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
#edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
edu.kit.iti.formal.psdbg.examples.java.sumPositive.SumPositiveExample
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
#edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
#edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
......
package edu.kit.iti.formal.psdbg.examples.java.sumPositive;
public class SumPositive{
/*@ public normal_behaviour
@ requires a != null;
@ ensures \result >= 0;
@*/
public int sumPositiveArray(int[] a) {
int sum = 0;
/*@
@ loop_invariant 0 <= i && i <= a.length;
@ loop_invariant \old(sum) <= sum;
@ decreases a.length - i;
@ assignable sum;
@*/
for (int i = 0; i < a.length; i++) {
if(a[i] >= 0) {
sum += a[i];
}
}
return sum;
}
}
\ No newline at end of file
package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.base.Strings;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.scene.control.TreeItem;
......@@ -21,13 +24,11 @@ import java.util.List;
public class ProofTreeTest {
private KeYProofFacade facade;
private List<ProofScript> scripts;
private Interpreter<KeyData> interpreter;
private static void printTree(TreeItem<TreeNode> rootItem, int level) {
System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label);
rootItem.getChildren().forEach(item -> {
printTree(item, level+1);
printTree(item, level + 1);
});
}
......@@ -37,7 +38,9 @@ public class ProofTreeTest {
}
@Test
public void testScriptTree() throws IOException, ProblemLoaderException {
public void testScriptTreeContraPosition() throws IOException, ProblemLoaderException {
List<ProofScript> scripts;
Interpreter<KeyData> interpreter;
File keyProblem = new File(getClass().getResource("contraposition.key").getFile());
facade.loadKeyFileSync(keyProblem);
scripts = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("proofTreeScript.kps")));
......@@ -65,5 +68,31 @@ public class ProofTreeTest {
}
@Test
public void testScriptTreeQuicksort() throws IOException, ProblemLoaderException, ProofInputException {
QuickSort qs = new QuickSort();
File javaFile = new File(qs.getJavaFile().getFile());
List<Contract> contracts = facade.getContractsForJavaFile(javaFile);
Contract c = contracts.get(0);
facade.activateContract(c);
System.out.println("Contract: '" + c.getName() + "' activated!");
List<ProofScript> scripts = Facade.getAST(
CharStreams.fromStream(qs.getScriptFile().openStream()));
System.out.println("Script loaded.");
InterpreterBuilder ib = facade.buildInterpreter();
KeyInterpreter interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0));
System.out.println("Interpreter ready! Start proofing...");
interpreter.interpret(scripts.get(0));
System.out.println("Script successfully finished!");
System.out.println("Begin construction of the tree...");
ScriptTreeGraph stg = new ScriptTreeGraph();
stg.createGraph(df.getPtreeManager().getStartNode(), facade.getProof().root());
System.out.println("stg = " + stg);
}
}
\ No newline at end of file
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