Skip to content

GitLab

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

Fix bugs for violation selection and violation prompt

parent cd73b2a9
Hide whitespace changes
Inline Side-by-side
Showing with 168 additions and 25 deletions
src/gui/DisproHandler.java
View file @ 439f6b8f
......@@ -32,6 +32,7 @@ import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.MenuBar;
import javafx.scene.layout.AnchorPane;
import javafx.scene.paint.Color;
import javafx.util.Callback;
import joanakey.JoanaAndKeYCheckData;
import joanakey.customlistener.ViolationsWrapperListener;
......@@ -87,6 +88,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private AnchorPane anchorPaneKeyContract;
private Map<Integer, ViolationChop> itemIndexToViolation = new HashMap<>();
private Map<ViolationChop, Boolean> violationChecked = new HashMap<>();
private Map<Integer, SDGEdge> itemIndexToSummaryEdge = new HashMap<>();
private HashMap<Integer, SDGNodeTuple> currentIndexToNodeTuple = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> summaryEdgesAndCorresJavaMethods;
......@@ -301,10 +303,12 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
summaryEdgesAndCorresJavaMethods.get(currentSelectedEdge));
labelSummaryEdge.setText(currentSelectedEdge.toString());
if (worked) {
labelSomeOtherData.setText("Disproving worked.");
// labelSomeOtherData.setText("Disproving worked.");
setSomeOtherMessageAndColor("Disproving worked.", Color.GREEN);
violationsWrapper.removeEdge(currentSelectedEdge);
} else {
labelSomeOtherData.setText("Could not disprove edge.");
setSomeOtherMessageAndColor("Could not disprove edge.", Color.RED);
// labelSomeOtherData.setText("Could not disprove edge.");
}
......@@ -602,9 +606,15 @@ 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) {
//TODO dont use uncheckedViolations ! use chops ?
// Collection<? extends IViolation<SecurityNode>> uncheckedViolations =
// violationsWrapper.getUncheckedViolations();
Collection<? extends IViolation<SecurityNode>> uncheckedViolations =
violationsWrapper.getAllViolationsToCheck();
for (IViolation<SecurityNode> v : uncheckedViolations) {
assert v instanceof ClassifiedViolation;
final ClassifiedViolation c = (ClassifiedViolation)v;
final String src =
......@@ -621,6 +631,26 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
"Illegal flow from " + src + " to " + snk
+ ", visible for " + c.getAttackerLevel();
listViewUncheckedChops.getItems().add(add);
// for (ViolationChop c : chops) {
//// assert v instanceof ClassifiedViolation;
//// final ClassifiedViolation c = (ClassifiedViolation)v;
// final String src =
// (c.getViolationSource().getBytecodeName().startsWith("<") ?
// c.getViolationSource().getSr() + ":" + c.getViolationSource().getBytecodeName()
// : c.getViolationSource().getLabel())
// + " (" + c.getViolationSource() + ")";
// final String snk =
// (c.getViolationSink().getBytecodeName().startsWith("<") ?
// c.getViolationSink().getSr() + ":" + c.getViolationSink().getBytecodeName()
// : c.getViolationSink().getLabel())
// + " (" + c.getViolationSink() + ")";
// final String add =
// "Illegal flow from " + src + " to " + snk;
// + ", visible for " + c.getAttackerLevel();
// listViewUncheckedChops.getItems().add(add);
}
summaryEdgesAndCorresJavaMethods = violationsWrapper.getSummaryEdgesAndCorresJavaMethods();
......@@ -676,17 +706,23 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
@Override
public void disprovedChop(ViolationChop chop) {
Platform.runLater(() -> {
labelSomeOtherData.setText("The chop " + chop.toString() + " was fully disproved.");
checkCloseViolation(chop);
});
Platform.runLater(() -> {
checkCloseViolation(chop);
// labelSomeOtherData.setText("The chop from " + chop.getViolationSource().toString() + " to "
// + chop.getViolationSink().toString() + " was fully disproved.");
setSomeOtherMessageAndColor("The chop from " + chop.getViolationSource().toString() + " to "
+ chop.getViolationSink().toString() + " was fully disproved.", Color.GREEN);
});
}
@Override
public void disprovedAll() {
Platform.runLater(() -> {
labelSomeOtherData.setText("All security violations have been disproved with KeY!");
// labelSomeOtherData.setText("All security violations have been disproved with KeY!");
this.setSomeOtherMessageAndColor("All security violations have been disproved with KeY!", Color.GREEN);
buttonRunAuto.setDisable(true);
//TODO: check this method !
displayAllViolationChecked();
// AutomationHelper.playSound(SOUND);
});
......@@ -727,9 +763,14 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
//TODO: loaded file completely checked ?
//TODO: just append CLOSED, if not done already
//TODO: "CLOSED" check with datastructure
private void displayAllViolationChecked() {
for (int i : itemIndexToViolation.keySet()) {
listViewUncheckedChops.getItems().set(i, "CLOSED: " + listViewUncheckedChops.getItems().get(i));
String itemText = listViewUncheckedChops.getItems().get(i);
if (!itemText.startsWith("CLOSED: ")) {
listViewUncheckedChops.getItems().set(i, "CLOSED: " + listViewUncheckedChops.getItems().get(i));
}
}
}
......@@ -740,7 +781,10 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
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));
String itemText = listViewUncheckedChops.getItems().get(i);
if (!itemText.startsWith("CLOSED: ")) {
listViewUncheckedChops.getItems().set(i, "CLOSED: " + listViewUncheckedChops.getItems().get(i));
}
}
}
}
......@@ -832,7 +876,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
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()) {
......@@ -840,6 +883,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
// onViolationSelectionChange(0);
}
} else {
setDisable(false);
setStyle("-fx-control-inner-background: " + DEFAULT_CONTROL_INNER_BACKGROUND + ";");
}
}
......@@ -848,4 +892,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
});
}
public void setSomeOtherMessageAndColor(String message, javafx.scene.paint.Color color) {
this.labelSomeOtherData.setText(message);
this.labelSomeOtherData.setTextFill(color);
}
}
src/joanakey/violations/ViolationChop.java
View file @ 439f6b8f
......@@ -40,8 +40,6 @@ public class ViolationChop {
public ViolationChop(SDGNode violationSource, SDGNode violationSink, SDG sdg) {
this.violationSource = violationSource;
this.violationSink = violationSink;
System.out.println("ViolationSource: " + violationSource.getId());//TODO Debugging. Remove!
System.out.println("ViolationSink: " + violationSink.getId());//TODO Debugging. Remove!
findSummaryEdges(sdg);
}
......@@ -115,10 +113,6 @@ public class ViolationChop {
// final boolean onlyStatic = true; XXX Currently commented out, since not quite there yet
// nodesInChop = Utils.addChopForFields(nodesInChop, sdg, onlyStatic);
inducedSubgraph = sdg.subgraph(nodesInChop);
// getCallNodes(); //TODO muessig remove!
inducedSubgraph.edgeSet().forEach((e) -> {
if (isSummaryEdge(e)) {
......
src/joanakey/violations/ViolationsWrapper.java
View file @ 439f6b8f
......@@ -25,8 +25,10 @@ import org.json.JSONObject;
import edu.kit.joana.api.IFCAnalysis;
import edu.kit.joana.api.sdg.SDGMethod;
import edu.kit.joana.ifc.sdg.core.SecurityNode;
import edu.kit.joana.ifc.sdg.core.libraries.IFC;
import edu.kit.joana.ifc.sdg.core.violations.ClassifiedViolation;
import edu.kit.joana.ifc.sdg.core.violations.IViolation;
import edu.kit.joana.ifc.sdg.core.violations.IViolationVisitor;
import edu.kit.joana.ifc.sdg.core.violations.paths.ViolationPath;
import edu.kit.joana.ifc.sdg.graph.SDG;
import edu.kit.joana.ifc.sdg.graph.SDGEdge;
......@@ -66,15 +68,18 @@ public class ViolationsWrapper {
private Collection<? extends IViolation<SecurityNode>> uncheckedViolations;
private SDG sdg;
private Collection<ViolationChop> violationChops = new ArrayList<>();
private Collection<ViolationChop> allChops = new ArrayList<>();
private HashSet<SDGEdge> checkedEdges = new HashSet<>();
private HashSet<SDGEdge> edgesToCheck = new HashSet<>();
private Map<SDGEdge, ArrayList<ViolationChop>> summaryEdgesAndContainingChops = new HashMap<>();
private Map<SDGEdge, StaticCGJavaMethod> summaryEdgesAndCorresJavaMethods = new HashMap<>();
private Map<ViolationChop, IViolation<SecurityNode>> chopToViolationMap = new HashMap<>();
private List<SDGEdge> sortedEdgesToCheck = new ArrayList<>();
private JCallGraph callGraph = new JCallGraph();
private IFCAnalysis ana;
private List<String> keyCompatibleJavaFeatures = new ArrayList<>();
private List<ViolationsWrapperListener> listener = new ArrayList<>();
private Collection<? extends IViolation<SecurityNode>> allViolationsToCheck;
public ViolationsWrapper(
......@@ -93,6 +98,9 @@ public class ViolationsWrapper {
line = buf.readLine();
}
buf.close();
Collection<? extends IViolation<SecurityNode>> allViolationsToHandle = getAllViolationsToHandle();
allViolationsToCheck = allViolationsToHandle;
prepareNextSummaryEdges();
}
......@@ -283,9 +291,51 @@ public class ViolationsWrapper {
return violationChops.iterator().next();
}
private void prepareNextSummaryEdgesOld() {
Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle =
getNextViolationsToHandle(1);
removeFromUncheckViolations(nextViolationsToHandle);
// Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle =
// getNextViolationsToHandle();
nextViolationsToHandle.forEach((v) -> {
ViolationChop chop = createViolationChop(v, sdg);
violationChops.add(chop);
});
putEdgesInSet();
findCGMethodsForSummaryEdgesIfKeYCompatible();
putEdgesAndChopsInMap();
sortedEdgesToCheck = new ArrayList<>();
for (SDGEdge e : summaryEdgesAndCorresJavaMethods.keySet()) {
sortedEdgesToCheck.add(e);
}
for (int i = 0; i < 10; ++i) {
try {
sortedEdgesToCheck.sort(new SummaryEdgeComparator(this));
break;
} catch (Exception e) {
}
}
violationChops.forEach((vc) -> {
listener.forEach((l) -> {
l.parsedChop(vc);
});
});
listener.forEach((l) -> {
l.addedNewEdges(summaryEdgesAndCorresJavaMethods, sortedEdgesToCheck, sdg);
});
}
private void prepareNextSummaryEdges() {
// Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle =
// getNextViolationsToHandle(1);
// removeFromUncheckViolations(nextViolationsToHandle);
Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle =
getNextViolationsToHandle();
getAllViolationsToHandle();
// removeFromUncheckViolations(nextViolationsToHandle);
nextViolationsToHandle.forEach((v) -> {
ViolationChop chop = createViolationChop(v, sdg);
......@@ -325,9 +375,19 @@ public class ViolationsWrapper {
}
}
}
private Collection<IViolation<SecurityNode>> getAllViolationsToHandle() {
List<IViolation<SecurityNode>> created = new ArrayList<>();
for (IViolation<SecurityNode> v : uncheckedViolations) {
created.add(v);
}
return created;
}
private Collection<IViolation<SecurityNode>> getNextViolationsToHandle() {
int amt_viols = 1;
private Collection<IViolation<SecurityNode>> getNextViolationsToHandle(int amtViols) {
// int amt_viols = 1;
int amt_viols = amtViols;
List<IViolation<SecurityNode>> created = new ArrayList<>();
int i = 0;
for (IViolation<SecurityNode> v : uncheckedViolations) {
......@@ -337,10 +397,19 @@ public class ViolationsWrapper {
created.add(v);
++i;
}
for (IViolation<SecurityNode> v : created) {
//bad smell. Method name. put this into a new method (removeFromUncheckedViolation)
// for (IViolation<SecurityNode> v : created) {
// uncheckedViolations.remove(v);
// }
return created;
}
private void removeFromUncheckViolations(Collection<? extends IViolation<SecurityNode>> nextViolationsToHandle) {
for (IViolation<SecurityNode> v : nextViolationsToHandle) {
uncheckedViolations.remove(v);
}
return created;
return;
}
private void findCGMethodsForSummaryEdgesIfKeYCompatible() {
......@@ -406,7 +475,10 @@ public class ViolationsWrapper {
LinkedList<SecurityNode> violationPathList = violationPath.getPathList();
SDGNode violationSource = violationPathList.get(0);
SDGNode violationSink = violationPathList.get(1);
return new ViolationChop(violationSource, violationSink, sdg);
ViolationChop c = new ViolationChop(violationSource, violationSink, sdg);
chopToViolationMap.put(c, violationNode);
return c;
}
private ViolationPath getViolationPath(IViolation<SecurityNode> v) {
......@@ -436,6 +508,10 @@ public class ViolationsWrapper {
return true;
}
/**
*
* @param e
*/
public void removeEdge(SDGEdge e) {
sdg.removeEdge(e);
sortedEdgesToCheck.remove(e);
......@@ -443,13 +519,20 @@ public class ViolationsWrapper {
l.disprovedEdge(e);
});
if (summaryEdgesAndContainingChops.get(e) != null) {
summaryEdgesAndContainingChops.get(e).forEach((vc) -> {
vc.findSummaryEdges(sdg);
//vc is empty if no path exists between source and sink -> remove violation
if (vc.isEmpty()) {
violationChops.remove(vc);
listener.forEach((l) -> {
l.disprovedChop(vc);
});
//violation checked -> remove from unchecked
IViolation<SecurityNode> violation = chopToViolationMap.get(vc);
uncheckedViolations.remove(violation);
}
});
}
......@@ -458,6 +541,8 @@ public class ViolationsWrapper {
if (sortedEdgesToCheck.isEmpty()) {
prepareNextSummaryEdges();
}
//TODO: correct ? finished if all violations are closed !
if (sortedEdgesToCheck.isEmpty()
|| (violationChops.isEmpty()
&& uncheckedViolations.isEmpty())) { //if no more violations to check than we are finished.
......@@ -573,6 +658,13 @@ public class ViolationsWrapper {
return uncheckedViolations;
}
public Collection<? extends IViolation<SecurityNode>> getAllViolationsToCheck() {
allViolationsToCheck.forEach((v)-> {
System.out.println(v);
});
return allViolationsToCheck;
}
public Map<SDGEdge, ArrayList<ViolationChop>> getSummaryEdgesAndContainingChops() {
return summaryEdgesAndContainingChops;
}
......@@ -581,10 +673,18 @@ public class ViolationsWrapper {
return summaryEdgesAndCorresJavaMethods;
}
public Collection<ViolationChop> getAllViolationChops() {
return violationChops;
}
public SDG getSdg() {
return sdg;
}
public boolean isCheckedEdge(SDGEdge e) {
return checkedEdges.contains(e);
}
public void resetCheckedEdges() {
checkedEdges.clear();
}
......
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