Commit 32f3082d authored by Joachim Müssig's avatar Joachim Müssig

merge with herdaDev

parents b7331c3c 4553cad4
......@@ -72,6 +72,7 @@ Respective authors are listed in the following section.
This software was mainly designed and implemented by the following students:
* Joachim Müssig
* Holger Klein
* Marko Kleine Büning
* [Simon Bischof](https://pp.ipd.kit.edu/person.php?id=148)
......
......@@ -7,6 +7,7 @@ package gui;
import javafx.scene.control.Label;
import javafx.scene.control.ProgressIndicator;
import javafx.scene.paint.Color;
/**
*
......@@ -23,14 +24,75 @@ public class CurrentActionLogger {
endProgress();
}
/**
* start progress indicator and show the given string as current action on the GUI
* @param msg the message you want to show on the GUI as current action
*/
public void startProgress(String msg) {
progressIndicator.setVisible(true);
labelCurrentAction.setText(msg);
labelCurrentAction.setTextFill(Color.BLACK);
}
/**
* start progress indicator and show the given string as current action on the GUI in a specific color
* @param msg the message you want to show on the GUI as current action
* @param c the color for the message
*/
public void startProgress(String msg, Color c) {
progressIndicator.setVisible(true);
labelCurrentAction.setTextFill(c);
labelCurrentAction.setText(msg);
}
/**
* stop progress indicator and clear the current action text on the gui.
*/
public void endProgress() {
labelCurrentAction.setText("");
progressIndicator.setVisible(false);
labelCurrentAction.setTextFill(Color.BLACK);
}
/**
* stop progress indicator and show the given string as current action on the GUI
* @param msg the message you want to show on the GUI as current action
*/
public void endProgressWithMessage(String msg) {
labelCurrentAction.setText(msg);
progressIndicator.setVisible(false);
labelCurrentAction.setTextFill(Color.BLACK);
}
/**
* stop progress indicator and show the given string as current action on the GUI
* @param msg the message you want to show on the GUI as current action
* @param c the color for the message
*/
public void endProgressWithMessage(String msg, Color c) {
labelCurrentAction.setText(msg);
labelCurrentAction.setTextFill(c);
progressIndicator.setVisible(false);
}
/**
* show the given string as current action on the GUI
* @param msg the message you want to show on the GUI as current action
*/
public void showMessage(String msg) {
labelCurrentAction.setText(msg);
labelCurrentAction.setTextFill(Color.BLACK);
}
/**
* show the given string as current action on the GUI
* @param msg the message you want to show on the GUI as current action
* @param c the color for the message
*/
public void showMessage(String msg, Color c) {
labelCurrentAction.setText(msg);
labelCurrentAction.setTextFill(c);
}
}
This diff is collapsed.
......@@ -29,6 +29,7 @@ public class DisproveViaKeYAndJoanaGUI extends Application {
controller.setMainStage(stage);
Scene scene = new Scene(root);
stage.setTitle("Combined Approach KeYJoana");
stage.setScene(scene);
stage.show();
......
......@@ -5,6 +5,10 @@
*/
package gui;
import java.io.IOException;
import java.util.ArrayList;
import edu.kit.joana.ifc.sdg.graph.SDG;
import edu.kit.joana.ifc.sdg.graph.SDGEdge;
import edu.kit.joana.ifc.sdg.graph.SDGNodeTuple;
import joanakey.AutomationHelper;
......@@ -12,28 +16,30 @@ import joanakey.customlistener.SummaryEdgeAndMethodToCorresData;
import joanakey.javaforkeycreator.JavaForKeYCreator;
import joanakey.persistence.DisprovingProject;
import joanakey.staticCG.javamodel.StaticCGJavaMethod;
import joanakey.violations.ViolationChop;
import joanakey.violations.ViolationsDisproverSemantic;
import joanakey.violations.ViolationsWrapper;
import joanakey.violations.ViolationsDisproverSemantic.PO_TYPE;
import java.io.IOException;
import joanakey.violations.ViolationsWrapper;
/**
*
* @author holger
* this class can be used to start the disproving process with KeY (also with command line mode)
* @author holger, joachim
*/
public class JoanaKeYInterfacer {
private ViolationsWrapper violationsWrapper;
private JavaForKeYCreator javaForKeyCreator;
private SummaryEdgeAndMethodToCorresData summaryEdgeToCorresData;
private boolean useSlicedFiles = true;
private boolean useMethodInlining = false;
private boolean useLoopUnwinding = false;
public JoanaKeYInterfacer(
DisprovingProject disprovingProject) throws IOException {
this.violationsWrapper = disprovingProject.getViolationsWrapper();
this.javaForKeyCreator
= new JavaForKeYCreator(
disprovingProject.getPathToJava(),
disprovingProject.getPathToJava(),
disprovingProject.getCallGraph(),
disprovingProject.getSdg(),
disprovingProject.getStateSaver());
......@@ -62,34 +68,47 @@ public class JoanaKeYInterfacer {
public void openInKeY(SDGEdge e,
SDGNodeTuple tuple,
StaticCGJavaMethod corresMethod) throws IOException {
//String pathToTestJava =
javaForKeyCreator.generateJavaForFormalTupleCalledFromGui(
summaryEdgeToCorresData.getContractFor(tuple),
corresMethod,
summaryEdgeToCorresData.getEdgeToLoopInvariantTemplate().get(e),
summaryEdgeToCorresData.getEdgeToLoopInvariant().get(e),
summaryEdgeToCorresData.getMethodToMostGeneralContract()
);
AutomationHelper.openKeY(ViolationsDisproverSemantic.PO_PATH);
if(corresMethod == null) {
throw new IllegalArgumentException("No method selected");
}
ArrayList<ViolationChop> chops = violationsWrapper.getSummaryEdgesAndContainingChops().get(e);
if (chops != null && !chops.isEmpty()) {
javaForKeyCreator.setMethodInlining(this.useMethodInlining);
javaForKeyCreator.setUseLoopUnwinding(this.useLoopUnwinding);
javaForKeyCreator.generateJavaForFormalTupleCalledFromGui(summaryEdgeToCorresData.getContractFor(tuple),
corresMethod, summaryEdgeToCorresData.getEdgeToLoopInvariantTemplate().get(e),
summaryEdgeToCorresData.getEdgeToLoopInvariant().get(e),
summaryEdgeToCorresData.getMethodToMostGeneralContract(), chops.get(0), useSlicedFiles); //all chops same slice ?
AutomationHelper.openKeY(ViolationsDisproverSemantic.PO_PATH);
}
}
/**
* try to disprove the given summary Edge with KeY in command line mode.
* @param e {@link SDGEdge} you want to disprove
* @param tuple
* @param corresMethod
* @return true if successfully disproven. Otherwise return False.
* @throws IOException
*/
public boolean tryDisproveEdge(
SDGEdge e,
SDGNodeTuple tuple,
StaticCGJavaMethod corresMethod) throws IOException {
StaticCGJavaMethod corresMethod) throws IOException{
if (corresMethod == null) {
throw new IOException("No method selected!");
throw new IllegalArgumentException("No method selected!");
}
//String pathToTestJava =
javaForKeyCreator.generateJavaForFormalTupleCalledFromGui(
summaryEdgeToCorresData.getContractFor(tuple),
corresMethod,
summaryEdgeToCorresData.getEdgeToLoopInvariantTemplate().get(e),
summaryEdgeToCorresData.getEdgeToLoopInvariant().get(e),
summaryEdgeToCorresData.getMethodToMostGeneralContract()
);
boolean worked = AutomationHelper.runKeY(ViolationsDisproverSemantic.PO_PATH,
PO_TYPE.INFORMATION_FLOW);
boolean worked = false;
ArrayList<ViolationChop> chops = violationsWrapper.getSummaryEdgesAndContainingChops().get(e);
if (chops != null && !chops.isEmpty()) {
ViolationChop chop = chops.get(0); //all chop same slice ?
// String pathToTestJava =
javaForKeyCreator.generateJavaForFormalTupleCalledFromGui(summaryEdgeToCorresData.getContractFor(tuple),
corresMethod, summaryEdgeToCorresData.getEdgeToLoopInvariantTemplate().get(e),
summaryEdgeToCorresData.getEdgeToLoopInvariant().get(e),
summaryEdgeToCorresData.getMethodToMostGeneralContract(), chop, useSlicedFiles);
worked = AutomationHelper.runKeY(ViolationsDisproverSemantic.PO_PATH, PO_TYPE.INFORMATION_FLOW);
}
if (worked) {
worked = AutomationHelper.runKeY(ViolationsDisproverSemantic.PO_PATH,
PO_TYPE.FUNCTIONAL);
......@@ -100,9 +119,19 @@ public class JoanaKeYInterfacer {
return worked;
}
public void markAsDisproved(SDGEdge currentSelectedEdge) {
/**
* mark the given {@link SDGEdge} as disproven and remove it from the {@link SDG} in {@link ViolationsWrapper}.
* @param currentSelectedEdge the {@link SDGEdge} you want to mark as disproven.
* @throws IllegalArgumentException
*/
public void markAsDisproved(SDGEdge currentSelectedEdge) throws IllegalArgumentException{
if(currentSelectedEdge == null) {
throw new IllegalArgumentException("No method selected!");
}
violationsWrapper.removeEdge(currentSelectedEdge);
}
public JavaForKeYCreator getJavaForKeyCreator() {
return javaForKeyCreator;
......@@ -111,8 +140,28 @@ public class JoanaKeYInterfacer {
public SummaryEdgeAndMethodToCorresData getSummaryEdgeToCorresData() {
return summaryEdgeToCorresData;
}
public void setUseSclicedFiles(boolean selected) {
this.useSlicedFiles = selected;
}
/**
* set method inlining option for the disproving process
* @param selected true, if you want to use method inlining
*/
public void setUseMethodInlining(boolean selected) {
this.useMethodInlining = selected;
javaForKeyCreator.setMethodInlining(selected);
}
/**
* set loop unwinding option for the disproving process
* @param selected true, if you want to use loop unwinding
*/
public void setUseLoopUnwinding(boolean selected) {
this.useLoopUnwinding = selected;
javaForKeyCreator.setUseLoopUnwinding(selected);
}
}
This diff is collapsed.
This diff is collapsed.
package gui;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
/**
* this class manages the recently loaded files
* @author joachim
*
*/
public class RecentlyUsedFilesManager {
private String recentlyUsedFilesPath;
private String mostRecentlyUsedFile;
private ArrayList<String> recentlyUsedFiles;
private int maxNumberOfSavedRecentlyLoadedFiles;
public RecentlyUsedFilesManager(String path) {
// recentlyUsedFilesPath = SettingsPaths.getRecentLoadedFilesPath();
recentlyUsedFilesPath = path;
this.maxNumberOfSavedRecentlyLoadedFiles = 5;
File f = new File(recentlyUsedFilesPath);
if (!f.exists()) {
try {
f.createNewFile();
} catch (IOException e) {
System.out.println(e.getMessage());
e.printStackTrace();
}
}
loadRecentlyUsedFilesPaths(recentlyUsedFilesPath);
}
/**
* get the most recently loaded file
* @return the most recently loaded file otherwise null
*/
public File getMostRecentlyUsedFile() {
if (mostRecentlyUsedFile != null) {
return new File(mostRecentlyUsedFile);
} else {
loadRecentlyUsedFilesPaths(recentlyUsedFilesPath);
boolean updated = updateMostRecentlyLoadedFilePath();
if (!updated) {
return null;
}
if (mostRecentlyUsedFile != null) {
File f = new File(mostRecentlyUsedFile);
if (f.exists()) {
return f;
}
}
return null;
}
}
public String[] getAllRecentlyUsedFilePaths() {
String[] names = new String[this.recentlyUsedFiles.size()];
for (int i = 0; i < names.length; i++) {
names[i] = recentlyUsedFiles.get(i);
}
return names;
}
/**
* Get the path of the most recently loaded file
* @return path of the most recently loaded file as path String
*/
public String getMostRecentlyUsedFilePath() {
if (mostRecentlyUsedFile == null) {
loadRecentlyUsedFilesPaths(recentlyUsedFilesPath);
return mostRecentlyUsedFile;
}
return mostRecentlyUsedFile;
}
/**
* stores the given file to the recently loaded files and update the most recently loaded file to it
* @param file you want to store and update to the most recently loaded file
*/
public void storeFileToRecentlyUsedFiles(File file) {
if(recentlyUsedFiles.contains(file.getAbsolutePath())) {
int index = recentlyUsedFiles.indexOf(file.getAbsolutePath());
recentlyUsedFiles.remove(index);
}
recentlyUsedFiles.add(0, file.getAbsolutePath());
updateMostRecentlyLoadedFilePath();
if (recentlyUsedFiles.size() > maxNumberOfSavedRecentlyLoadedFiles) {
recentlyUsedFiles.remove(recentlyUsedFiles.size()-1);
}
//Update mostRecentlyUsedFile
//store new content in the File for recently loaded files
try {
StringBuilder created = new StringBuilder();
FileWriter writer = new FileWriter(recentlyUsedFilesPath);
// PrintWriter out = new PrintWriter(writer);
for (int i = 0; i < recentlyUsedFiles.size(); i++) {
created.append(recentlyUsedFiles.get(i));
if (i != recentlyUsedFiles.size()-1) {
created.append("\n");
}
}
writer.write("");
// File recentlyUsedFiles = new File(recentlyUsedFilesPath);
// recentlyUsedFiles.delete();
// recentlyUsedFiles.createNewFile();
writer.write(created.toString());
writer.close();
// out.close();
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
/**
* set the maximum number of recently loaded files saved
* @param maxNumber
*/
public void setMaxNumberOfSavedFiles(int maxNumber) {
this.maxNumberOfSavedRecentlyLoadedFiles = maxNumber;
}
private void loadRecentlyUsedFilesPaths(String path) {
if (new File(path).exists()) {
BufferedReader reader;
recentlyUsedFiles = new ArrayList<String>(maxNumberOfSavedRecentlyLoadedFiles);
try {
reader = new BufferedReader(new FileReader(recentlyUsedFilesPath));
String line = reader.readLine();
while (line != null) {
recentlyUsedFiles.add(line);
line = reader.readLine();
}
} catch (IOException e) {
e.printStackTrace();
}
}
}
/**
* updates the most recently loaded file
* @return true if updated and false if there are no recently loaded files yet
*/
private boolean updateMostRecentlyLoadedFilePath() {
if (recentlyUsedFiles.isEmpty()) {
return false;
}
mostRecentlyUsedFile = recentlyUsedFiles.get(0);
return true;
}
}
......@@ -8,16 +8,16 @@ package gui.asynctaskhandler;
import java.io.File;
import java.nio.charset.Charset;
import java.util.function.BiConsumer;
import org.apache.commons.io.FileUtils;
import gui.CurrentActionLogger;
import javafx.application.Platform;
import joanakey.CombinedApproach;
import joanakey.JoanaAndKeYCheckData;
import joanakey.errorhandling.ErrorLogger;
import joanakey.persistence.DisprovingProject;
import org.apache.commons.io.FileUtils;
import gui.CurrentActionLogger;
/**
*
* @author holger
......@@ -63,17 +63,21 @@ public class AsyncBackgroundLoader implements Runnable {
if (loadOption == LoadOptions.JOAK) {
try {
currentCheckData = CombinedApproach.parseInputFile(fileToLoad);
success = true;
success = true;
Platform.runLater(() -> {
actionLogger.endProgress();
uiThreadJoakCallback.accept(currentCheckData, success);
});
} catch (Exception ex) {
success = false;
ErrorLogger.logError("CombinedApproach threw " + ex.getClass().getSimpleName() +
" while trying to pass the JOAK file " + fileToLoad.getName() + ".",
ErrorLogger.ErrorTypes.ERROR_PARSING_JOAK);
}
Platform.runLater(() -> {
actionLogger.endProgress();
uiThreadJoakCallback.accept(currentCheckData, success);
});
Platform.runLater(() -> {
actionLogger.endProgressWithMessage(ex.getClass().getSimpleName() + " while parsing .joak file. Check if the .joak file is correct.");
uiThreadJoakCallback.accept(currentCheckData, success);
});
}
} else {
try {
String fileContents = FileUtils.readFileToString(fileToLoad, Charset.defaultCharset());
......@@ -81,6 +85,7 @@ public class AsyncBackgroundLoader implements Runnable {
success = true;
} c