Skip to content

GitLab

Commit cd73b2a9 authored by Joachim Müssig's avatar Joachim Müssig
Browse files
Options

Fix bug for multiple violations and add a violation selection

parent ba49f09a
Hide whitespace changes
Inline Side-by-side
Showing with 268 additions and 39 deletions
src/gui/DisproHandler.java
View file @ cd73b2a9
......@@ -6,12 +6,14 @@
package gui;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.fxmisc.richtext.CodeArea;
import org.jgrapht.ext.JGraphModelAdapter.CellFactory;
import edu.kit.joana.ifc.sdg.core.SecurityNode;
import edu.kit.joana.ifc.sdg.core.violations.ClassifiedViolation;
......@@ -26,9 +28,11 @@ import javafx.event.ActionEvent;
import javafx.scene.control.Button;
import javafx.scene.control.CheckMenuItem;
import javafx.scene.control.Label;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.MenuBar;
import javafx.scene.layout.AnchorPane;
import javafx.util.Callback;
import joanakey.JoanaAndKeYCheckData;
import joanakey.customlistener.ViolationsWrapperListener;
import joanakey.errorhandling.ErrorLogger;
......@@ -82,10 +86,12 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private AnchorPane anchorPaneLoopInvariant;
private AnchorPane anchorPaneKeyContract;
private Map<Integer, ViolationChop> itemIndexToViolation = new HashMap<>();
private Map<Integer, SDGEdge> itemIndexToSummaryEdge = new HashMap<>();
private HashMap<Integer, SDGNodeTuple> currentIndexToNodeTuple = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> summaryEdgesAndCorresJavaMethods;
private ViolationChop currentSelectedViolation;
private SDGEdge currentSelectedEdge;
private StaticCGJavaMethod currentSelectedMethod;
private CurrentActionLogger currentActionLogger;
......@@ -93,7 +99,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private boolean useSlicing = false;
private boolean useLoopUnwinding = false;
private boolean useMethodInlining = false;
private static final String DEFAULT_CONTROL_INNER_BACKGROUND = "derive(-fx-base,80%)";
private static final String HIGHLIGHTED_CONTROL_INNER_BACKGROUND = "derive(palegreen, 50%)";
public DisproHandler(
CurrentActionLogger currentActionLogger,
......@@ -164,6 +172,12 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
labelProjName.setText("");
labelSummaryEdge.setText("");
labelSomeOtherData.setText("");
listViewUncheckedChops.getSelectionModel().selectedIndexProperty()
.addListener((observable, oldValue, newValue) -> {
clearView();
onViolationSelectionChange((int) newValue);
});
listViewSummaryEdges.getSelectionModel().selectedIndexProperty()
.addListener((observable, oldValue, newValue) -> {
......@@ -178,6 +192,8 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
onLoopInvSelectionChanged((int) newValue);
});
setChopViewListFactory();
}
public void setAllButtonsDisable(boolean disable) {
......@@ -368,6 +384,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
//#######################################################################
//this gets run whenever the selected SUMMARY EDGE changes-------------->
//#######################################################################
//TODO: check if the right value is selected after selecting a su with a violation
private void onSummaryEdgeSelectionChange(int newValue) {
if (newValue < 0) {
return;
......@@ -424,6 +441,58 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
listViewFormalInoutPairs.getSelectionModel().select(0);
}
//this gets run whenever the selected violation changes
private void onViolationSelectionChange(int newValue) {
if (newValue < 0) {
return;
}
resetListView(listViewSummaryEdges);
//index 0 "All" entry -> show all SU
if (newValue == 0) {
showAllSU();
} else {
SDGEdge firstSU = null;
//TODO:This field is null after selecting another violation -> exception
this.currentSelectedViolation = this.itemIndexToViolation.get(newValue);
for (SDGEdge e : currentSelectedViolation.getSummaryEdges()) {
if (e == null) break;
if (firstSU == null) {
firstSU = e;
}
if (!violationsWrapper.isCheckedEdge(e)) {
listViewSummaryEdges.getItems()
.add(e.toString() + " : " + summaryEdgesAndCorresJavaMethods.get(e).toString());
//TODO: NUllpointerException ?! after all disproven ? Debug !
}
}
if (firstSU != null) {
int newIndex = getSUIndex(firstSU);
if(newIndex == -1) {
//TODO: can this occure ?
}
this.listViewSummaryEdges.getSelectionModel().select(0);
this.onSummaryEdgeSelectionChange(newIndex);
System.out.println(currentSelectedEdge.toString());
}
}
}
private int getSUIndex(SDGEdge su) {
for(int i = 0; i<itemIndexToSummaryEdge.size(); i++) {
if (itemIndexToSummaryEdge.get(i) != null) {
if (itemIndexToSummaryEdge.get(i).equals(su)) {
return i;
}
}
}
return -1;
}
//#######################################################################
//this gets run whenever the selected FORMAL NODE TUPLE changes-------------->
//#######################################################################
......@@ -468,6 +537,17 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private void handleNewDisproSet() throws IOException {
violationsWrapper = disprovingProject.getViolationsWrapper();
violationsWrapper.addListener(this);
//Initialize the index data structure for all violations
int violationIndex = 1;
//index 0 for "all" entry
this.itemIndexToViolation.put(0, null);
// violationsWrapper.getAllViolationChops()
for (ViolationChop chop : violationsWrapper.getAllViolationChops()) {
this.itemIndexToViolation.put(violationIndex, chop);
violationIndex++;
}
joanaKeyInterfacer = new JoanaKeYInterfacer(disprovingProject);
useMethodInlining(keyJoanaSettings.getMethodExpandSetting());
......@@ -501,7 +581,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
// checkMenuItemUseMethodInlining.setOnAction((event) -> {
// useMethodInlining();
// });
//Initially selected violation is "All"
onViolationSelectionChange(0);
}
private void resetViews() {
//
......@@ -517,6 +601,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
itemIndexToSummaryEdge = new HashMap<>();
listViewUncheckedChops.getItems().add("All");
Collection<? extends IViolation<SecurityNode>> uncheckedViolations =
violationsWrapper.getUncheckedViolations();
for (IViolation<SecurityNode> v : uncheckedViolations) {
......@@ -539,16 +624,16 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
summaryEdgesAndCorresJavaMethods = violationsWrapper.getSummaryEdgesAndCorresJavaMethods();
int i = 0;
for (SDGEdge e : summaryEdgesAndCorresJavaMethods.keySet()) {
listViewSummaryEdges.getItems().add(
e.toString() +
" : " +
summaryEdgesAndCorresJavaMethods.get(e).toString()
);
itemIndexToSummaryEdge.put(i++, e);
}
this.showAllSU();
// int i = 0;
// for (SDGEdge e : summaryEdgesAndCorresJavaMethods.keySet()) {
// listViewSummaryEdges.getItems().add(
// e.toString() +
// " : " +
// summaryEdgesAndCorresJavaMethods.get(e).toString()
// );
// itemIndexToSummaryEdge.put(i++, e);
// }
}
@Override
......@@ -586,12 +671,14 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
listViewSummaryEdges.getSelectionModel().clearSelection();
listViewSummaryEdges.getSelectionModel().select(0);
});
}
@Override
public void disprovedChop(ViolationChop chop) {
Platform.runLater(() -> {
labelSomeOtherData.setText("The chop " + chop.toString() + " was fully disproved.");
checkCloseViolation(chop);
});
}
......@@ -600,6 +687,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
Platform.runLater(() -> {
labelSomeOtherData.setText("All security violations have been disproved with KeY!");
buttonRunAuto.setDisable(true);
displayAllViolationChecked();
// AutomationHelper.playSound(SOUND);
});
}
......@@ -624,4 +712,140 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
useLoopUnwinding(keyJoanaSettings.getLoopUnwindSetting());
useSlicedFiles(keyJoanaSettings.getSlicingSetting());
}
private void showAllSU() {
int i = 0;
for (SDGEdge e : summaryEdgesAndCorresJavaMethods.keySet()) {
listViewSummaryEdges.getItems().add(
e.toString() +
" : " +
summaryEdgesAndCorresJavaMethods.get(e).toString()
);
itemIndexToSummaryEdge.put(i++, e);
}
}
//TODO: loaded file completely checked ?
private void displayAllViolationChecked() {
for (int i : itemIndexToViolation.keySet()) {
listViewUncheckedChops.getItems().set(i, "CLOSED: " + listViewUncheckedChops.getItems().get(i));
}
}
//TODO: correct this and use this method to close violations if possible after disproving a SU
private void checkCloseViolation(ViolationChop v) {
for(int i : itemIndexToViolation.keySet()) {
if (i != 0) {
if (itemIndexToViolation.get(i).equals(v)) {
//FIXME: index out of bound exception if all disproven !
if (!violationsWrapper.getAllViolationChops().contains(v)) {
listViewUncheckedChops.getItems().set(i, "CLOSED: " + listViewUncheckedChops.getItems().get(i));
}
}
}
}
// if (false) {
// itemIndexToViolation.forEach((index, itemViolation) -> {
// if (index != 0) {
// int i = index;
// String item = listViewUncheckedChops.getItems().get(index);
// Collection<ViolationChop> s = violationsWrapper.getAllViolationChops();
// System.out.println(s);
// if (!violationsWrapper.getAllViolationChops().contains(itemViolation)) {
// System.out.println("close: " +i);
// if (!item.startsWith("CLOSED")) {
// listViewUncheckedChops.getItems().set(index, "CLOSED: " + item);
// }
// if (violationsWrapper.allCheckedOrDisproved()) {
// // All closed
// item = listViewUncheckedChops.getItems().get(0);
// listViewUncheckedChops.getItems().set(0, "CLOSED: " + item);
// }
// }
//
// }
//
// });
// }
// boolean closeViolation = true;
// Collection<SDGEdge> suEdges = itemViolation.getSummaryEdges();
// for (SDGEdge edge : suEdges) {
// if (!violationsWrapper.isCheckedEdge(edge)) {
// closeViolation = false;
// }
// }
// if (closeViolation) {
// listViewUncheckedChops.getItems().set(index, listViewUncheckedChops.getItems().get(index) + " CLOSED");
//
// //TODO: dont remove it -> disable list element and mark it as closed.
// listViewUncheckedChops.getItems().remove(index);
// listViewUncheckedChops.setCellFactory(new Callback<ListView<String>, ListCell<String>>() {
// @Override
// public ListCell<String> call(ListView<String> param) {
// return new ListCell<String>() {
// @Override
// protected void updateItem(String item, boolean empty) {
// super.updateItem(item, empty);
// if(item.contains(" CLOSED")) {
// setDisable(true);
// }
// setText(item);
// }
//
// };
// }
// });
// }
}
private void clearView() {
resetListView(listViewSummaryEdges);
resetListView(listViewCalledMethodsInSE);
resetListView(listViewLoopsInSE);
resetListView(listViewFormalInoutPairs);
clearCodeAreaForNewCode(methodCodeArea, "");
clearCodeAreaForNewCode(loopInvariantCodeArea, "");
clearCodeAreaForNewCode(keyContractCodeArea, "");
}
/**
* this method set the cell factory of the violation listView.
* Change the cells if the violation is closed/checked
*/
private void setChopViewListFactory() {
listViewUncheckedChops.setCellFactory(new Callback<ListView<String>, ListCell<String>>() {
@Override
public ListCell<String> call(ListView<String> param) {
return new ListCell<String>() {
@Override
protected void updateItem(String item, boolean empty) {
super.updateItem(item, empty);
if (item == null || empty) {
setText(null);
setStyle("-fx-control-inner-background: " + DEFAULT_CONTROL_INNER_BACKGROUND + ";");
} else {
setText(item);
//TODO: maybe use a datastructure to remember which item is closed instead of checking the String
if (item.startsWith("CLOSED")) {
System.out.println("closed and disable : " + item);
setStyle("-fx-control-inner-background: " + HIGHLIGHTED_CONTROL_INNER_BACKGROUND + ";");
setDisable(true);
if(!violationsWrapper.allCheckedOrDisproved()) {
listViewUncheckedChops.getSelectionModel().select(0);
// onViolationSelectionChange(0);
}
} else {
setStyle("-fx-control-inner-background: " + DEFAULT_CONTROL_INNER_BACKGROUND + ";");
}
}
}
};
}
});
}
}
src/gui/MainWindowFXMLDoc.fxml
View file @ cd73b2a9
......@@ -91,32 +91,46 @@
<children>
<TabPane accessibleRole="COMBO_BOX" prefHeight="205.0" prefWidth="772.0" tabClosingPolicy="UNAVAILABLE" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
<tabs>
<Tab text="Currently Not Disproven Summary Edges">
<Tab text="Unchecked Violations Chops">
<content>
<AnchorPane minHeight="0.0" minWidth="0.0">
<children>
<SplitPane dividerPositions="0.546875" AnchorPane.bottomAnchor="-6.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
<SplitPane dividerPositions="0.5952080706179067" prefHeight="160.0" prefWidth="200.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
<items>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="160.0" prefWidth="100.0">
<AnchorPane prefHeight="170.0" prefWidth="250.0">
<children>
<SplitPane dividerPositions="0.5945945945945946" prefHeight="160.0" prefWidth="200.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
<items>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="160.0" prefWidth="100.0">
<children>
<ListView fx:id="listViewUncheckedEdges" prefHeight="200.0" prefWidth="200.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="30.0" />
<Label text="Summary Edges" AnchorPane.leftAnchor="0.0" AnchorPane.topAnchor="0.0" />
</children>
</AnchorPane>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="169.0" prefWidth="132.0">
<children>
<Label text="Formal In/Out Pairs" AnchorPane.leftAnchor="0.0" AnchorPane.topAnchor="0.0" />
<ListView fx:id="listViewFormalInoutPairs" layoutX="-28.0" layoutY="-24.0" prefHeight="200.0" prefWidth="200.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="30.0" />
</children>
</AnchorPane>
</items>
</SplitPane>
<ListView fx:id="listViewUncheckedChops" layoutY="32.0" prefHeight="140.0" prefWidth="250.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="-3.0" AnchorPane.topAnchor="30.0" />
<Label text="Violation to check" />
</children>
</AnchorPane>
<SplitPane dividerPositions="0.5" prefHeight="200.0" prefWidth="200.0">
<items>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="170.0" prefWidth="0.0">
<children>
<ListView fx:id="listViewUncheckedEdges" prefHeight="200.0" prefWidth="73.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="30.0" />
<Label text="Summary Edges" AnchorPane.leftAnchor="0.0" AnchorPane.topAnchor="0.0" />
</children>
</AnchorPane>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="169.0" prefWidth="132.0">
<children>
<Label text="Formal In/Out Pairs" AnchorPane.leftAnchor="0.0" AnchorPane.topAnchor="0.0" />
<ListView fx:id="listViewFormalInoutPairs" layoutX="-13.0" layoutY="-24.0" prefHeight="140.0" prefWidth="323.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="-13.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="30.0" />
</children>
</AnchorPane>
</items>
</SplitPane>
</items>
</SplitPane>
</children>
</AnchorPane>
</content>
</Tab>
<Tab text="Currently Not Disproven Summary Edges">
<content>
<AnchorPane minHeight="0.0" minWidth="0.0">
<children>
<SplitPane AnchorPane.bottomAnchor="-6.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
<items>
<AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="137.0" prefWidth="462.0">
<children>
<SplitPane dividerPositions="0.5" layoutX="54.0" prefHeight="160.0" prefWidth="200.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
......@@ -143,15 +157,6 @@
</AnchorPane>
</content>
</Tab>
<Tab text="Unchecked Violations Chops">
<content>
<AnchorPane minHeight="0.0" minWidth="0.0">
<children>
<ListView fx:id="listViewUncheckedChops" layoutY="-4.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="-4.0" />
</children>
</AnchorPane>
</content>
</Tab>
</tabs>
</TabPane>
</children>
......
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