From 6deac6d853eb87a493b1c3b9646d52f85d6034ae Mon Sep 17 00:00:00 2001
From: Letitia Li <letitia.li@telecom-paristech.fr>
Date: Thu, 19 Jan 2017 16:31:08 +0100
Subject: [PATCH] Autocomplete for security pragmas
---
src/ui/avatarbd/AvatarBDPanel.java | 22 ++-
src/ui/avatarbd/AvatarBDPragma.java | 216 +++++++++++-----------
src/ui/avatarbd/AvatarBDSafetyPragma.java | 2 +-
src/ui/window/JDialogPragma.java | 104 +++++++++--
4 files changed, 208 insertions(+), 136 deletions(-)
diff --git a/src/ui/avatarbd/AvatarBDPanel.java b/src/ui/avatarbd/AvatarBDPanel.java
index ae1e590a8e..5d703efcee 100644
--- a/src/ui/avatarbd/AvatarBDPanel.java
+++ b/src/ui/avatarbd/AvatarBDPanel.java
@@ -420,18 +420,22 @@ public class AvatarBDPanel extends TDiagramPanel {
}
}
- public HashMap<String, List<String>> getBlockStrings(){
- HashMap<String,List<String>> blockAttributeMap = new HashMap<String, List<String>>();
+ public HashMap<String, List<String>> getBlockStrings(boolean addAttributes, boolean addStates){
+ HashMap<String,List<String>> blockStringMap = new HashMap<String, List<String>>();
for (AvatarBDBlock block: getFullBlockList()){
- List<String> attrs = new ArrayList<String>();
- for (TAttribute attr: getAllAttributesOfBlock(block.getBlockName())){
- attrs.add(attr.getId());
+ List<String> strs = new ArrayList<String>();
+ if (addAttributes){
+ for (TAttribute attr: getAllAttributesOfBlock(block.getBlockName())){
+ strs.add(attr.getId());
+ }
}
- AvatarSMDPanel smd = block.getAvatarSMDPanel();
- attrs.addAll(smd.getAllStates());
- blockAttributeMap.put(block.getBlockName(), attrs);
+ if (addStates){
+ AvatarSMDPanel smd = block.getAvatarSMDPanel();
+ strs.addAll(smd.getAllStates());
+ }
+ blockStringMap.put(block.getBlockName(), strs);
}
- return blockAttributeMap;
+ return blockStringMap;
}
public LinkedList<AvatarBDStateMachineOwner> getFullStateMachineOwnerList() {
diff --git a/src/ui/avatarbd/AvatarBDPragma.java b/src/ui/avatarbd/AvatarBDPragma.java
index 6ec8090bc1..f1602a4e9d 100755
--- a/src/ui/avatarbd/AvatarBDPragma.java
+++ b/src/ui/avatarbd/AvatarBDPragma.java
@@ -94,28 +94,28 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
height = 30;
minWidth = 80;
minHeight = 10;
- models = new LinkedList<String>();
- properties = new LinkedList<String>();
- authStrongMap = new HashMap<String, Integer>();
- authWeakMap = new HashMap<String, Integer>();
+ models = new LinkedList<String>();
+ properties = new LinkedList<String>();
+ authStrongMap = new HashMap<String, Integer>();
+ authWeakMap = new HashMap<String, Integer>();
oldScaleFactor = tdp.getZoom();
nbConnectingPoint = 0;
//addTGConnectingPointsComment();
- int len = makeTGConnectingPointsComment(16);
- int decw = 0;
- int dech = 0;
- for(int i=0; i<2; i++) {
- connectingPoint[len] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 0.0 + dech);
- connectingPoint[len + 1 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.5 + decw, 0.0 + dech);
- connectingPoint[len + 2 ] = new TGConnectingPointComment(this, 0, 0, true, true, 1.0 + decw, 0.0 + dech);
- connectingPoint[len + 3 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 0.5 + dech);
- connectingPoint[len + 4 ] = new TGConnectingPointComment(this, 0, 0, true, true, 1.0 + decw, 0.5 + dech);
- connectingPoint[len + 5 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 1.0 + dech);
- connectingPoint[len + 6 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.5 + decw, 1.0 + dech);
- connectingPoint[len + 7 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.9 + decw, 1.0 + dech);
- len += 8;
- }
+ int len = makeTGConnectingPointsComment(16);
+ int decw = 0;
+ int dech = 0;
+ for(int i=0; i<2; i++) {
+ connectingPoint[len] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 0.0 + dech);
+ connectingPoint[len + 1 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.5 + decw, 0.0 + dech);
+ connectingPoint[len + 2 ] = new TGConnectingPointComment(this, 0, 0, true, true, 1.0 + decw, 0.0 + dech);
+ connectingPoint[len + 3 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 0.5 + dech);
+ connectingPoint[len + 4 ] = new TGConnectingPointComment(this, 0, 0, true, true, 1.0 + decw, 0.5 + dech);
+ connectingPoint[len + 5 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.0 + decw, 1.0 + dech);
+ connectingPoint[len + 6 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.5 + decw, 1.0 + dech);
+ connectingPoint[len + 7 ] = new TGConnectingPointComment(this, 0, 0, true, true, 0.9 + decw, 1.0 + dech);
+ len += 8;
+ }
moveable = true;
editable = true;
@@ -131,11 +131,11 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
return values;
}
public void setValues(String[] v){
- values=v;
- makeValue();
+ values=v;
+ makeValue();
}
public LinkedList<String> getProperties() {
- return properties;
+ return properties;
}
public void internalDrawing(Graphics g) {
@@ -177,11 +177,11 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
* from the Graphics object.
* Thus we use a saved FontMetrics object in TDiagramPanel that only changes when zoom changes.
*/
- int desiredWidth = Math.max(this.minWidth, 2*this.tdp.stringWidth(g, "Property Pragma") + marginX+ textX);
+ int desiredWidth = Math.max(this.minWidth, 2*this.tdp.stringWidth(g, "Property Pragma") + marginX+ textX);
for(int i=0; i< values.length; i++)
desiredWidth = Math.max(desiredWidth, this.tdp.stringWidth(g, values[i]) + marginX+textX);
-// currentFontSize= 5;
+ // currentFontSize= 5;
int desiredHeight = ((models.size() + properties.size()+4)*currentFontSize) + textY + 1;
//TraceManager.addDev("resize: " + desiredWidth + "," + desiredHeight);
@@ -212,32 +212,32 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
g.setColor(c);
- int i = 1;
- Font heading = new Font("heading", Font.BOLD, this.tdp.getFontSize ()*7/6);
- g.setFont(heading);
- g.drawString("Model Pragma", x+textX, y+textY + currentFontSize);
- g.setFont(fold);
- for (String s: models){
- g.drawString(s, x + textX, y + textY + (i+1)* currentFontSize);
- i++;
- }
+ int i = 1;
+ Font heading = new Font("heading", Font.BOLD, this.tdp.getFontSize ()*7/6);
+ g.setFont(heading);
+ g.drawString("Model Pragma", x+textX, y+textY + currentFontSize);
+ g.setFont(fold);
+ for (String s: models){
+ g.drawString(s, x + textX, y + textY + (i+1)* currentFontSize);
+ i++;
+ }
// FIXME: why the empty string ?
- g.drawString(" ", x+ textX, y+ textY+(i+1)*currentFontSize);
- i++;
- g.drawLine(x, y+textY/2+i*currentFontSize, x+width, y+textY/2+i*currentFontSize);
- g.setFont(heading);
- g.drawString("Property Pragma", x+textX, y+textY+(i+1)* currentFontSize);
- g.setFont(fold);
- i++;
- for (String s: properties){
- if (authStrongMap.containsKey(s) || authWeakMap.containsKey(s)){
- g.setFont(new Font("tmp", Font.PLAIN, 7));
- drawConfidentialityVerification(s, g, x+ lockX, y + lockY + (i+1)*currentFontSize);
+ g.drawString(" ", x+ textX, y+ textY+(i+1)*currentFontSize);
+ i++;
+ g.drawLine(x, y+textY/2+i*currentFontSize, x+width, y+textY/2+i*currentFontSize);
+ g.setFont(heading);
+ g.drawString("Property Pragma", x+textX, y+textY+(i+1)* currentFontSize);
g.setFont(fold);
- }
- g.drawString(s, x + textX, y + textY + (i+1)* currentFontSize);
- i++;
- }
+ i++;
+ for (String s: properties){
+ if (authStrongMap.containsKey(s) || authWeakMap.containsKey(s)){
+ g.setFont(new Font("tmp", Font.PLAIN, 7));
+ drawConfidentialityVerification(s, g, x+ lockX, y + lockY + (i+1)*currentFontSize);
+ g.setFont(fold);
+ }
+ g.drawString(s, x + textX, y + textY + (i+1)* currentFontSize);
+ i++;
+ }
/* for (int i = 0; i<values.length; i++) {
//TraceManager.addDev("x+texX=" + (x + textX) + " y+textY=" + y + textY + i* h + ": " + values[i]);
@@ -250,24 +250,24 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
public void makeValue() {
values = Conversion.wrapText(value);
- models.clear();
- properties.clear();
- for (String s: values){
- if (s.isEmpty() || s.split(" ").length < 1){
- //Ignore
- }
- else if (Arrays.asList(mPragma).contains(s.split(" ")[0])){
- models.add(s);
- }
- else if (Arrays.asList(pPragma).contains(s.split(" ")[0])){
- properties.add(s);
- }
- else {
- //Warning Message
- JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
+ models.clear();
+ properties.clear();
+ for (String s: values){
+ if (s.isEmpty() || s.split(" ").length < 1){
+ //Ignore
+ }
+ else if (Arrays.asList(mPragma).contains(s.split(" ")[0])){
+ models.add(s);
+ }
+ else if (Arrays.asList(pPragma).contains(s.split(" ")[0])){
+ properties.add(s);
+ }
+ else {
+ //Warning Message
+ JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
JOptionPane.INFORMATION_MESSAGE);
- }
- }
+ }
+ }
//checkMySize();
}
@@ -289,64 +289,63 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
private void drawConfidentialityVerification(String s, Graphics g, int _x, int _y) {
Color c = g.getColor();
Color c1;
- Color c2;
- int confStatus;
- if (authStrongMap.containsKey(s)){
- confStatus = authStrongMap.get(s);
- switch(confStatus) {
- case PROVED_TRUE:
+ Color c2;
+ int confStatus;
+ if (authStrongMap.containsKey(s)){
+ confStatus = authStrongMap.get(s);
+ switch(confStatus) {
+ case PROVED_TRUE:
c1 = Color.green;
- break;
- case PROVED_FALSE:
+ break;
+ case PROVED_FALSE:
c1 = Color.red;
break;
- case NOT_PROVED:
- c1 = Color.gray;
- break;
- default:
+ case NOT_PROVED:
+ c1 = Color.gray;
+ break;
+ default:
return;
}
- } else {
- c1 = Color.gray;
- }
-
- if (authWeakMap.containsKey(s)){
- confStatus = authWeakMap.get(s);
- switch(confStatus) {
- case PROVED_TRUE:
+ } else {
+ c1 = Color.gray;
+ }
+ if (authWeakMap.containsKey(s)){
+ confStatus = authWeakMap.get(s);
+ switch(confStatus) {
+ case PROVED_TRUE:
c2 = Color.green;
- break;
- case PROVED_FALSE:
+ break;
+ case PROVED_FALSE:
c2 = Color.red;
break;
- case NOT_PROVED:
- c2 = Color.gray;
- break;
- default:
+ case NOT_PROVED:
+ c2 = Color.gray;
+ break;
+ default:
return;
}
- } else {
- c2 = c1;
- }
+ } else {
+ c2 = c1;
+ }
- g.drawOval(_x+6, _y-16, 10, 15);
- g.setColor(c1);
- int[] xps = new int[]{_x+4, _x+4, _x+20};
- int[] yps = new int[]{_y-10, _y+4, _y+4};
- int[] xpw = new int[]{_x+20, _x+20, _x+4};
- int[] ypw = new int[]{_y+4, _y-10, _y-10};
- g.fillPolygon(xps, yps,3);
+ g.drawOval(_x+6, _y-16, 10, 15);
+ g.setColor(c1);
+ int[] xps = new int[]{_x+4, _x+4, _x+20};
+ int[] yps = new int[]{_y-10, _y+4, _y+4};
+ int[] xpw = new int[]{_x+20, _x+20, _x+4};
+ int[] ypw = new int[]{_y+4, _y-10, _y-10};
+ g.fillPolygon(xps, yps,3);
- g.setColor(c2);
- g.fillPolygon(xpw, ypw, 3);
+ g.setColor(c2);
+ g.fillPolygon(xpw, ypw, 3);
// g.fillRect(_x+4, _y-7, 18, 14);
- g.setColor(c);
+ g.setColor(c);
// g.drawRect(_x+4, _y-7, 18, 14);
- g.drawPolygon(xps, yps,3);
- g.drawPolygon(xpw, ypw, 3);
- g.drawString("S", _x+6, _y+2);
- g.drawString("W", _x+13, _y-2);
+ g.drawPolygon(xps, yps,3);
+ g.drawPolygon(xpw, ypw, 3);
+ g.drawString("S", _x+6, _y+2);
+ g.drawString("W", _x+13, _y-2);
// if (c1==Color.gray){
// g.drawString("?", _x+4, _y+2);
// }
@@ -357,6 +356,9 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
JDialogPragma jdn = new JDialogPragma(frame, "Setting the pragma", value);
//jdn.setLocation(200, 150);
+ AvatarBDPanel abdp = (AvatarBDPanel) tdp;
+ jdn.blockAttributeMap = abdp.getBlockStrings(true,false);
+ jdn.blockStateMap = abdp.getBlockStrings(false,true);
GraphicLib.centerOnParent(jdn);
jdn.show(); // blocked until dialog has been closed
diff --git a/src/ui/avatarbd/AvatarBDSafetyPragma.java b/src/ui/avatarbd/AvatarBDSafetyPragma.java
index a0aaf29a04..ec38f3077b 100644
--- a/src/ui/avatarbd/AvatarBDSafetyPragma.java
+++ b/src/ui/avatarbd/AvatarBDSafetyPragma.java
@@ -256,7 +256,7 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent {
//jdn.setLocation(200, 150);
GraphicLib.centerOnParent(jdn);
AvatarBDPanel abdp = (AvatarBDPanel) tdp;
- jdn.blockAttributeMap = abdp.getBlockStrings();
+ jdn.blockAttributeMap = abdp.getBlockStrings(true,true);
jdn.show(); // blocked until dialog has been closed
String s = jdn.getText();
diff --git a/src/ui/window/JDialogPragma.java b/src/ui/window/JDialogPragma.java
index 0995477281..acc9bfe2b0 100755
--- a/src/ui/window/JDialogPragma.java
+++ b/src/ui/window/JDialogPragma.java
@@ -52,6 +52,7 @@ import javax.swing.*;
import javax.swing.text.*;
import ui.*;
import java.util.*;
+import java.util.regex.*;
public class JDialogPragma extends javax.swing.JDialog implements ActionListener {
@@ -64,7 +65,8 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
protected JMenuBar menuBar;
protected JMenu help;
protected JPopupMenu helpPopup;
-
+ public HashMap<String, java.util.List<String>> blockAttributeMap = new HashMap<String, java.util.List<String>>();
+ public HashMap<String, java.util.List<String>> blockStateMap = new HashMap<String, java.util.List<String>>();
/** Creates new form */
public JDialogPragma(Frame f, String title, String _text) {
super(f, title, true);
@@ -76,24 +78,24 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
//Suggestion Panel code from: http://stackoverflow.com/questions/10873748/how-to-show-autocomplete-as-i-type-in-jtextarea
public class SuggestionPanel {
- private final String[] pragma = {"#Authenticity", "#Confidentiality", "#PublicConstant", "#PrivateConstant", "#InitialSessionKnowledge", "#InitialSystemKnowledge", "#PrivatePublicKeys", "#Public", "#SecrecyAssumption", "#Secret"};
- private JList list;
+ private final String[] pragma = {"#Authenticity", "#Confidentiality", "#PublicConstant", "#PrivateConstant", "#InitialSessionKnowledge", "#InitialSystemKnowledge", "#PrivatePublicKeys", "#Public", "#SecrecyAssumption", "#Secret"};
+ private JList list;
private JPopupMenu popupMenu;
private String subWord;
private final int insertionPosition;
- public SuggestionPanel(JTextArea textarea, int position, String subWord, Point location) {
+ public SuggestionPanel(JTextArea textarea, int position, String subWord, Point location, String header) {
this.insertionPosition = position;
this.subWord = subWord;
popupMenu = new JPopupMenu();
popupMenu.removeAll();
popupMenu.setOpaque(false);
popupMenu.setBorder(null);
- popupMenu.add(list = createSuggestionList(position, subWord), BorderLayout.CENTER);
- //Show popupMenu only if there are matching suggestions
- if (list.getModel().getSize() >0){
+ popupMenu.add(list = createSuggestionList(position, subWord, header), BorderLayout.CENTER);
+ //Show popupMenu only if there are matching suggestions
+ if (list.getModel().getSize() >0){
popupMenu.show(textarea, location.x, textarea.getBaseline(0, 0) + location.y);
- }
+ }
}
public void hide() {
@@ -103,16 +105,62 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
}
}
- private JList createSuggestionList(final int position, final String subWord) {
- ArrayList<String> matches = new ArrayList<String>();
- if (subWord.startsWith("#")){
- for (String p: pragma) {
- if (p.startsWith(subWord)){
- matches.add(p);
- }
- }
- }
- Object[] data = new Object[matches.size()];
+ private JList createSuggestionList(final int position, final String subWord, String header) {
+ ArrayList<String> matches = new ArrayList<String>();
+ if (subWord.startsWith("#")){
+ for (String p: pragma) {
+ if (p.startsWith(subWord)){
+ matches.add(p);
+ }
+ }
+ }
+ else if (header.contains("#")){
+ //Find instances of '.'
+ Pattern p = Pattern.compile("\\.");
+ Matcher m = p.matcher(subWord);
+ int count = 0;
+ while (m.find()){
+ count +=1;
+ }
+ if (count==0){
+ //Suggest block names
+ for (String block: blockAttributeMap.keySet()){
+ if (block.startsWith(subWord)){
+ matches.add(block);
+ }
+ }
+ }
+ else if (count==1){
+ if (header.contains("Authenticity")){
+ //Suggest state names
+ String block = subWord.split("\\.")[0];
+ for (String st: blockStateMap.get(block)){
+ if (st.startsWith(subWord.split("\\.")[1])){
+ matches.add(block+"."+st);
+ }
+ }
+ }
+ else {
+ String block = subWord.split("\\.")[0];
+ for (String attr: blockAttributeMap.get(block)){
+ if (attr.startsWith(subWord.split("\\.")[1])){
+ matches.add(block+"."+attr);
+ }
+ }
+ }
+ }
+ else {
+ String block = subWord.split("\\.")[0];
+ String state = subWord.split("\\.")[1];
+ for (String attr: blockAttributeMap.get(block)){
+ if (attr.startsWith(subWord.split("\\.")[2])){
+ matches.add(block+"."+state+"."+attr);
+ }
+ }
+
+ }
+ }
+ Object[] data = new Object[matches.size()];
data = matches.toArray(data);
JList list = new JList(data);
list.setBorder(BorderFactory.createLineBorder(Color.DARK_GRAY, 1));
@@ -207,7 +255,25 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
if (subWord.length() < 1) {
return;
}
- suggestion = new SuggestionPanel(textarea, position, subWord, location);
+ String header="";
+ //Find the most recent pragma name
+ start=Math.max(0,position-1);
+ while (start>0){
+ //Find previous new line position
+ if (!String.valueOf(text.charAt(start)).matches(".")){
+ break;
+ }
+ else {
+ start--;
+ }
+ }
+ if (start==0){
+ header = text.substring(start, position).split(" ")[0];
+ }
+ else {
+ header = text.substring(start+1,position).split(" ")[0];
+ }
+ suggestion = new SuggestionPanel(textarea, position, subWord, location, header);
SwingUtilities.invokeLater(new Runnable() {
@Override
public void run() {
--
GitLab