Commit 422412e8 authored by Joachim Müssig's avatar Joachim Müssig
Browse files

Mark disproven Summary Edges instead of removing them

parent 59d06b75
......@@ -9,8 +9,10 @@ import java.io.IOException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import org.fxmisc.richtext.CodeArea;
import org.jgrapht.ext.JGraphModelAdapter.CellFactory;
......@@ -93,6 +95,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private Map<Integer, SDGEdge> itemIndexToSummaryEdge = new HashMap<>();
private HashMap<Integer, SDGNodeTuple> currentIndexToNodeTuple = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> summaryEdgesAndCorresJavaMethods;
private Map<SDGEdge, ViolationChop> disprovenSUEdgesAndCorresViolation = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> allSummaryEdgesAndCorresJavaMethodsCopy = new HashMap<>();
private Map<SDGEdge, Boolean> suEdgeClosedMap = new HashMap<>();
private ViolationChop currentSelectedViolation;
private SDGEdge currentSelectedEdge;
......@@ -196,7 +201,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
});
setChopViewListFactory();
setSUViewListFactory();
}
public void setAllButtonsDisable(boolean disable) {
......@@ -385,6 +390,13 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
} catch (Exception e) {
}
}
private void disableDisproveButtons(boolean b) {
this.buttonOpenSelected.setDisable(b);
this.buttonRunAuto.setDisable(b);
this.buttonMarkAsDisproved.setDisable(b);
this.buttonTryDisprove.setDisable(b);
}
//#######################################################################
//this gets run whenever the selected SUMMARY EDGE changes-------------->
......@@ -395,15 +407,19 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
currentActionLogger.showMessage("");
currentSelectedEdge = itemIndexToSummaryEdge.get(newValue);
// System.out.println("currently selected Edge : " + this.currentSelectedEdge);
// System.out.println("corresponding Method : " + allSummaryEdgesAndCorresJavaMethodsCopy.get(currentSelectedEdge));
currentSelectedMethod = summaryEdgesAndCorresJavaMethods != null ?
summaryEdgesAndCorresJavaMethods.get(currentSelectedEdge) : null;
allSummaryEdgesAndCorresJavaMethodsCopy.get(currentSelectedEdge) : null;
// summaryEdgesAndCorresJavaMethods.get(currentSelectedEdge) : null;
if (currentSelectedMethod == null && 0 < summaryEdgesAndCorresJavaMethods.size()) {
currentSelectedEdge =
currentSelectedEdge == null ?
summaryEdgesAndCorresJavaMethods.keySet().iterator().next()
: currentSelectedEdge;
currentSelectedMethod = summaryEdgesAndCorresJavaMethods.get(currentSelectedEdge);
currentSelectedMethod = allSummaryEdgesAndCorresJavaMethodsCopy.get(currentSelectedEdge);
// currentSelectedMethod = summaryEdgesAndCorresJavaMethods.get(currentSelectedEdge);
}
if (currentSelectedMethod == null) {
System.err.println("No method available, but proof not finished.");
......@@ -442,6 +458,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
listViewFormalInoutPairs.getItems().add(str);
currentIndexToNodeTuple.put(index++, t);
}
if (this.suEdgeClosedMap.get(currentSelectedEdge)) {
disableDisproveButtons(true);
} else {
disableDisproveButtons(false);
}
listViewFormalInoutPairs.getSelectionModel().select(0);
}
......@@ -470,8 +491,19 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
String summaryEdge = summaryEdgesAndCorresJavaMethods.get(e).toString();
listViewSummaryEdges.getItems()
.add(edge + " : " + summaryEdge);
}
for (SDGEdge disprovenEdge : violationsWrapper.getChopAndCorrespondingDisprovenSummaryEdges()
.keySet()) {
if (violationsWrapper.getChopAndCorrespondingDisprovenSummaryEdges().get(disprovenEdge)
.equals(this.currentSelectedViolation)) {
// TODO: use data structure to save which su already disproven !
String summaryEdge = allSummaryEdgesAndCorresJavaMethodsCopy.get(e).toString();
listViewSummaryEdges.getItems().add("CLOSED " + edge + " : " + summaryEdge);
}
}
}
if (firstSU != null) {
int newIndex = getSUIndex(firstSU);
if(newIndex == -1) {
......@@ -545,6 +577,8 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
*/
private void handleNewDisproSet() throws IOException {
violationsWrapper = disprovingProject.getViolationsWrapper();
this.allSummaryEdgesAndCorresJavaMethodsCopy.putAll(violationsWrapper.getSummaryEdgesAndCorresJavaMethods());
violationsWrapper.addListener(this);
//Initialize the index data structure for all violations
......@@ -565,6 +599,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
// useMethodInlining();
// useLoopUnwinding();
// useSlicedFiles();
for (SDGEdge su : allSummaryEdgesAndCorresJavaMethodsCopy.keySet()) {
this.suEdgeClosedMap.put(su, false);
}
resetViews();
//
//setup disproving buttons
......@@ -681,15 +718,15 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
int selectedIndex = listViewSummaryEdges.getSelectionModel().getSelectedIndex();
currentIndexToNodeTuple.remove(selectedIndex);
itemIndexToSummaryEdge.remove(selectedIndex);
for (int i = selectedIndex + 1; i < listViewSummaryEdges.getItems().size(); ++i) {
SDGEdge currentEdge = itemIndexToSummaryEdge.remove(i);
itemIndexToSummaryEdge.put(i - 1, currentEdge);
SDGNodeTuple currentRemovedNodeTuple = currentIndexToNodeTuple.remove(i);
currentIndexToNodeTuple.put(i - 1, currentRemovedNodeTuple);
}
// currentIndexToNodeTuple.remove(selectedIndex);
// itemIndexToSummaryEdge.remove(selectedIndex);
//
// for (int i = selectedIndex + 1; i < listViewSummaryEdges.getItems().size(); ++i) {
// SDGEdge currentEdge = itemIndexToSummaryEdge.remove(i);
// itemIndexToSummaryEdge.put(i - 1, currentEdge);
// SDGNodeTuple currentRemovedNodeTuple = currentIndexToNodeTuple.remove(i);
// currentIndexToNodeTuple.put(i - 1, currentRemovedNodeTuple);
// }
clearCodeAreaForNewCode(methodCodeArea, "");
clearCodeAreaForNewCode(loopInvariantCodeArea, "");
......@@ -699,9 +736,16 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
resetListView(listViewFormalInoutPairs);
resetListView(listViewCalledMethodsInSE);
listViewSummaryEdges.getItems().removeIf((s) -> {
return s.startsWith(e.toString());
});
// listViewSummaryEdges.getItems().add("CLOSED " + listViewSummaryEdges.getItems().get(selectedIndex));
listViewSummaryEdges.getItems().set(selectedIndex,
"CLOSED " + listViewSummaryEdges.getItems().get(selectedIndex));
// listViewSummaryEdges.getItems().removeIf((s) -> {
// return s.startsWith(e.toString());
// });
this.disprovenSUEdgesAndCorresViolation.put(e ,currentSelectedViolation);
suEdgeClosedMap.put(e, true);
//
listViewSummaryEdges.getSelectionModel().clearSelection();
listViewSummaryEdges.getSelectionModel().select(0);
});
......@@ -762,6 +806,19 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
);
itemIndexToSummaryEdge.put(i++, e);
}
Set<SDGEdge> collectedEdges = new HashSet<SDGEdge>();
for (SDGEdge e : violationsWrapper.getChopAndCorrespondingDisprovenSummaryEdges().keySet()) {
collectedEdges.add(e);
}
for (SDGEdge e : collectedEdges) {
listViewSummaryEdges.getItems().add(
"CLOSED " +
e.toString() +
" : " +
allSummaryEdgesAndCorresJavaMethodsCopy.get(e).toString()
);
itemIndexToSummaryEdge.put(i++, e);
}
}
......@@ -823,7 +880,10 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
//TODO: maybe use a datastructure to remember which item is closed instead of checking the String
if (item.startsWith("CLOSED")) {
setStyle("-fx-control-inner-background: " + HIGHLIGHTED_CONTROL_INNER_BACKGROUND + ";");
setDisable(true);
//TODO: dont disable, so you can still see the disproven edges. But disable the buttons for closed summary edges !
// setDisable(true);
if(!violationsWrapper.allCheckedOrDisproved()) {
listViewUncheckedChops.getSelectionModel().select(0);
// onViolationSelectionChange(0);
......@@ -839,6 +899,40 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
});
}
/**
* this method set the cell factory of the violation listView.
* Change the cells if the violation is closed/checked
*/
private void setSUViewListFactory() {
listViewSummaryEdges.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")) {
setStyle("-fx-control-inner-background: " + HIGHLIGHTED_CONTROL_INNER_BACKGROUND + ";");
// setDisable(true);
} else {
setDisable(false);
setStyle("-fx-control-inner-background: " + DEFAULT_CONTROL_INNER_BACKGROUND + ";");
}
}
}
};
}
});
}
public void setSomeOtherMessageAndColor(String message, javafx.scene.paint.Color color) {
this.labelSomeOtherData.setText(message);
this.labelSomeOtherData.setTextFill(color);
......
......@@ -73,6 +73,7 @@ public class ViolationsWrapper {
private HashSet<SDGEdge> edgesToCheck = new HashSet<>();
private Map<SDGEdge, ArrayList<ViolationChop>> summaryEdgesAndContainingChops = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> summaryEdgesAndCorresJavaMethods = new HashMap<>();
private Map<SDGEdge, ViolationChop> disprovenSummaryEdgesAndCorresChop = new HashMap<>();
private Map<ViolationChop, IViolation<SecurityNode>> chopToViolationMap = new HashMap<>();
private List<SDGEdge> sortedEdgesToCheck = new ArrayList<>();
private JCallGraph callGraph = new JCallGraph();
......@@ -396,14 +397,9 @@ public class ViolationsWrapper {
}
created.add(v);
++i;
}
//bad smell. Method name. put this into a new method (removeFromUncheckedViolation)
// for (IViolation<SecurityNode> v : created) {
// uncheckedViolations.remove(v);
// }
return created;
}
}
return created;
}
private void removeFromUncheckViolations(Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle) {
for (IViolation<SecurityNode> v : nextViolationsToHandle) {
......@@ -478,7 +474,6 @@ public class ViolationsWrapper {
ViolationChop c = new ViolationChop(violationSource, violationSink, sdg);
chopToViolationMap.put(c, violationNode);
return c;
}
private ViolationPath getViolationPath(IViolation<SecurityNode> v) {
......@@ -508,6 +503,8 @@ public class ViolationsWrapper {
return true;
}
/**
*
* @param e
......@@ -522,6 +519,7 @@ public class ViolationsWrapper {
summaryEdgesAndContainingChops.get(e).forEach((vc) -> {
disprovenSummaryEdgesAndCorresChop.put(e, vc);
vc.findSummaryEdges(sdg);
//vc is empty if no path exists between source and sink -> remove violation
if (vc.isEmpty()) {
......@@ -688,4 +686,9 @@ public class ViolationsWrapper {
public void resetCheckedEdges() {
checkedEdges.clear();
}
public Map<SDGEdge, ViolationChop> getChopAndCorrespondingDisprovenSummaryEdges() {
return disprovenSummaryEdgesAndCorresChop;
}
}
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