From c7c77bf58f81cec46a41eeb2cbde7451cd7949fd Mon Sep 17 00:00:00 2001
From: dblouin <dominique.blouin@telecom-paristech.fr>
Date: Fri, 25 May 2018 17:10:26 +0200
Subject: [PATCH] Issue #131 + code cleanup
---
.../proverifspec/ProVerifOutputAnalyzer.java | 16 +--
src/main/java/tmltranslator/TMLModeling.java | 10 +-
.../tmltranslator/toavatar/TML2Avatar.java | 2 +-
src/main/java/ui/AvatarDesignPanel.java | 11 +-
src/main/java/ui/GTURTLEModeling.java | 14 ++-
.../window/JDialogProverifVerification.java | 110 +++++++++++++-----
6 files changed, 110 insertions(+), 53 deletions(-)
diff --git a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
index 006baf48f3..f1233297aa 100644
--- a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
@@ -80,9 +80,9 @@ public class ProVerifOutputAnalyzer {
private final static String typedWeakNonAuth = "(even event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private final static String untypedWeakNonAuth = "(even ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private final static String typedAuthSplit = "==> inj-event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
- private final static String typedWeakAuthSplit = "==> event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ //private final static String typedWeakAuthSplit = "==> event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private final static String untypedAuthSplit = "==> evinj:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
- private final static String untypedWeakAuthSplit = "==> ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ //private final static String untypedWeakAuthSplit = "==> ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private ConcurrentHashMap<AvatarPragma, ProVerifQueryResult> results;
private LinkedList<String> errors;
@@ -433,7 +433,7 @@ public class ProVerifOutputAnalyzer {
return this.results;
}
- public HashMap<AvatarPragmaSecret, ProVerifQueryResult> getConfidentialityResults()
+ public Map<AvatarPragmaSecret, ProVerifQueryResult> getConfidentialityResults()
{
if (this.results == null)
return null;
@@ -451,12 +451,12 @@ public class ProVerifOutputAnalyzer {
return resultMap;
}
- public HashMap<AvatarPragmaReachability, ProVerifQueryResult> getReachabilityResults()
+ public Map<AvatarPragmaReachability, ProVerifQueryResult> getReachabilityResults()
{
if (this.results == null)
return null;
- HashMap<AvatarPragmaReachability, ProVerifQueryResult> resultMap = new HashMap<AvatarPragmaReachability, ProVerifQueryResult> ();
+ Map<AvatarPragmaReachability, ProVerifQueryResult> resultMap = new HashMap<AvatarPragmaReachability, ProVerifQueryResult> ();
for (AvatarPragma pragma: this.results.keySet())
{
@@ -469,12 +469,12 @@ public class ProVerifOutputAnalyzer {
return resultMap;
}
- public HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> getAuthenticityResults()
+ public Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> getAuthenticityResults()
{
if (this.results == null)
return null;
- HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> resultMap = new HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> ();
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> resultMap = new HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> ();
for (AvatarPragma pragma: this.results.keySet())
{
@@ -487,7 +487,7 @@ public class ProVerifOutputAnalyzer {
return resultMap;
}
- public LinkedList<String> getErrors() {
+ public List<String> getErrors() {
synchronized(errors) {
return errors;
}
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index bc1191c1cb..2255bf09de 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -757,7 +757,7 @@ public class TMLModeling<E> {
public void backtrace(ProVerifOutputAnalyzer pvoa, String mappingName){
//System.out.println("Backtracing Confidentiality");
- HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (AvatarPragmaSecret pragma: confResults.keySet()) {
ProVerifQueryResult result = confResults.get(pragma);
@@ -829,7 +829,7 @@ public class TMLModeling<E> {
}
- public void backtraceAuthenticity(HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults, String mappingName) {
+ public void backtraceAuthenticity(Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults, String mappingName) {
// System.out.println("Backtracing Authenticity");
for (AvatarPragmaAuthenticity pragma: authenticityResults.keySet()) {
ProVerifQueryAuthResult result = authenticityResults.get(pragma);
@@ -912,7 +912,7 @@ public class TMLModeling<E> {
for (String channelName: channels){
if (channelName.contains("retData_") || channelName.contains("data_")){
channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- String header= channelName.split("__retData_")[0];
+ //String header= channelName.split("__retData_")[0];
for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
channelName = channelName.replace("_"+t.getName().split("__")[1],"");
@@ -1008,7 +1008,7 @@ public class TMLModeling<E> {
for (String channelName: channels){
if (channelName.contains("retData_") || channelName.contains("data_")){
channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- String header= channelName.split("__retData_")[0];
+ //String header= channelName.split("__retData_")[0];
for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
channelName = channelName.replace("_"+t.getName().split("__")[1],"");
@@ -1112,7 +1112,7 @@ public class TMLModeling<E> {
for (String channelName: channels){
if (channelName.contains("retData_") || channelName.contains("data_")){
channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- String header= channelName.split("__retData_")[0];
+ //String header= channelName.split("__retData_")[0];
for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
channelName = channelName.replace("_"+t.getName().split("__")[1],"");
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index 43f4430b0c..30980565bc 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -2115,7 +2115,7 @@ outerloop:
return avspec;
}
- public void backtraceReachability(HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
+ public void backtraceReachability( Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
{
ProVerifQueryResult result = reachabilityResults.get(pragma);
diff --git a/src/main/java/ui/AvatarDesignPanel.java b/src/main/java/ui/AvatarDesignPanel.java
index 88e8454867..5e590ebbe4 100644
--- a/src/main/java/ui/AvatarDesignPanel.java
+++ b/src/main/java/ui/AvatarDesignPanel.java
@@ -63,6 +63,7 @@ import javax.swing.event.ChangeEvent;
import javax.swing.event.ChangeListener;
import java.awt.*;
import java.util.*;
+import java.util.List;
/**
* Class AvatarDesignPanel
@@ -451,9 +452,9 @@ public class AvatarDesignPanel extends TURTLEPanel {
resetModelBacktracingProVerif();
// Confidential attributes
- HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
- LinkedList<AvatarAttribute> secretAttributes = new LinkedList<AvatarAttribute> ();
- LinkedList<AvatarAttribute> nonSecretAttributes = new LinkedList<AvatarAttribute> ();
+ Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ List<AvatarAttribute> secretAttributes = new LinkedList<AvatarAttribute> ();
+ List<AvatarAttribute> nonSecretAttributes = new LinkedList<AvatarAttribute> ();
for (AvatarPragmaSecret pragma: confResults.keySet())
{
ProVerifQueryResult result = confResults.get(pragma);
@@ -505,7 +506,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
// Reachable states
- HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachResults = pvoa.getReachabilityResults();
+ Map<AvatarPragmaReachability, ProVerifQueryResult> reachResults = pvoa.getReachabilityResults();
for (AvatarPragmaReachability pragma: reachResults.keySet())
{
ProVerifQueryResult result = reachResults.get(pragma);
@@ -530,7 +531,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
}
- HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
for (Object ob: abdp.getComponentList())
if (ob instanceof AvatarBDPragma) {
AvatarBDPragma pragma = (AvatarBDPragma) ob;
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 0f8e24046f..d126806844 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -2031,20 +2031,26 @@ public class GTURTLEModeling {
try {
proverif = avatar2proverif.generateProVerif(true, true, 1, true, false);
warnings = avatar2proverif.getWarnings();
+
+ // Issue #131
+ final String proverifSpecFile = SpecConfigTTool.ProVerifCodeDirectory + "pvspec";
- if (!avatar2proverif.saveInFile("pvspec")) {
+ if (!avatar2proverif.saveInFile( proverifSpecFile )) {
+// if (!avatar2proverif.saveInFile("pvspec")) {
return;
}
RshClient rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
- rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
+ // Issue #131
+ rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + proverifSpecFile );
+// rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
rshc.sendExecuteCommandRequest();
Reader data = rshc.getDataReaderFromProcess();
ProVerifOutputAnalyzer pvoa = getProVerifOutputAnalyzer();
pvoa.analyzeOutput(data, true);
- HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (AvatarPragmaSecret pragma : confResults.keySet()) {
if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
@@ -2055,7 +2061,7 @@ public class GTURTLEModeling {
}
}
}
- HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getAttribute().getName().replaceAll("_chData", ""));
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 836f53590f..1c1615bb1d 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -39,6 +39,56 @@
package ui.window;
+import java.awt.BorderLayout;
+import java.awt.Component;
+import java.awt.Container;
+import java.awt.Dialog;
+import java.awt.Dimension;
+import java.awt.Font;
+import java.awt.Frame;
+import java.awt.GridBagConstraints;
+import java.awt.GridBagLayout;
+import java.awt.Insets;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.awt.event.MouseEvent;
+import java.awt.event.MouseListener;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Map;
+import java.util.Vector;
+
+import javax.swing.Box;
+import javax.swing.ButtonGroup;
+import javax.swing.JButton;
+import javax.swing.JCheckBox;
+import javax.swing.JComboBox;
+import javax.swing.JDialog;
+import javax.swing.JLabel;
+import javax.swing.JList;
+import javax.swing.JMenuItem;
+import javax.swing.JPanel;
+import javax.swing.JPopupMenu;
+import javax.swing.JRadioButton;
+import javax.swing.JScrollPane;
+import javax.swing.JTabbedPane;
+import javax.swing.JTextField;
+import javax.swing.ListSelectionModel;
+import javax.swing.event.ListSelectionEvent;
+import javax.swing.event.ListSelectionListener;
+
import avatartranslator.AvatarPragma;
import avatartranslator.AvatarPragmaAuthenticity;
import avatartranslator.AvatarPragmaReachability;
@@ -48,34 +98,21 @@ import launcher.LauncherException;
import launcher.RshClient;
import launcher.RshClientReader;
import myutil.FileException;
-import myutil.FileUtils;
import myutil.GraphicLib;
import myutil.MasterProcessInterface;
import myutil.TraceManager;
import proverifspec.ProVerifOutputAnalyzer;
+import proverifspec.ProVerifOutputListener;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
import proverifspec.ProVerifResultTraceStep;
-import proverifspec.ProVerifOutputListener;
+import tmltranslator.TMLMapping;
import ui.AvatarDesignPanel;
-import ui.util.IconManager;
import ui.MainGUI;
-import ui.TURTLEPanel;
import ui.TMLArchiPanel;
-
+import ui.TURTLEPanel;
import ui.interactivesimulation.JFrameSimulationSDPanel;
-import tmltranslator.*;
-
-import javax.swing.*;
-import javax.swing.event.ListSelectionEvent;
-import javax.swing.event.ListSelectionListener;
-import java.awt.*;
-import java.awt.event.ActionEvent;
-import java.awt.event.ActionListener;
-import java.awt.event.MouseEvent;
-import java.awt.event.MouseListener;
-import java.io.*;
-import java.util.*;
+import ui.util.IconManager;
/**
@@ -152,7 +189,12 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
Map<JCheckBox, ArrayList<JCheckBox>> cpuTaskObjs = new HashMap<JCheckBox, ArrayList<JCheckBox>>();
private class MyMenuItem extends JMenuItem {
- AvatarPragma pragma;
+ /**
+ *
+ */
+ private static final long serialVersionUID = -344414299222823444L;
+
+ AvatarPragma pragma;
ProVerifQueryResult result;
MyMenuItem(String text) {
@@ -183,15 +225,21 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private class ProVerifVerificationException extends Exception {
- private String message;
-
- ProVerifVerificationException(String message) {
- this.message = message;
- }
+ /**
+ *
+ */
+ private static final long serialVersionUID = -2359743729229833671L;
+
+ // Issue #131 Already defined in super class
+ //private String message;
- public String getMessage() {
- return this.message;
+ public ProVerifVerificationException(String message) {
+ super( message );
}
+//
+// public String getMessage() {
+// return this.message;
+// }
}
/**
@@ -787,13 +835,15 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
mgui.gtm.autoMapKeys();
}
mode = NOT_STARTED;
- } else {
+ }
+ else {
testGo();
pathCode = code1.getText().trim();
- if (pathCode.isEmpty()) {
- pathCode += "pvspec";
- }
+ // Issue #131: Not needed. Would duplicate file name
+// if (pathCode.isEmpty()) {
+// pathCode += "pvspec";
+// }
SpecConfigTTool.checkAndCreateProverifDir(pathCode);
@@ -933,7 +983,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private void maybeShowPopup(MouseEvent e) {
if (e.isPopupTrigger() && e.getComponent() instanceof JList) {
- JList curList = (JList) e.getComponent();
+ JList<?> curList = (JList<?>) e.getComponent();
int row = curList.locationToIndex(e.getPoint());
curList.clearSelection();
curList.setSelectedIndex(row);
--
GitLab