From 2ed1bd4184de4a79e81234a2ba146fd5db4cbdaa Mon Sep 17 00:00:00 2001
From: Letitia Li <letitia.li@telecom-paristech.fr>
Date: Thu, 12 Jul 2018 16:29:59 +0200
Subject: [PATCH] Show proverif result trace in primitive ports and latency
panel scrollbars added
---
src/main/java/tmltranslator/TMLModeling.java | 62 +++++++++++++++++-
.../tmltranslator/toavatar/TML2Avatar.java | 2 +-
src/main/java/ui/GTURTLEModeling.java | 2 +-
src/main/java/ui/MainGUI.java | 4 +-
src/main/java/ui/TDiagramPanel.java | 21 +++++-
.../JFrameAvatarInteractiveSimulation.java | 6 +-
.../JFrameInteractiveSimulation.java | 5 +-
.../java/ui/tmlcompd/TMLCPrimitivePort.java | 65 +++++++++++++++++++
8 files changed, 154 insertions(+), 13 deletions(-)
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 31b7ead148..408f74b0e1 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -50,6 +50,7 @@ import myutil.TraceManager;
import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
+import proverifspec.ProVerifResultTrace;
import ui.TAttribute;
import ui.tmlcompd.TMLCPrimitiveComponent;
import ui.tmlcompd.TMLCPrimitivePort;
@@ -806,6 +807,12 @@ public class TMLModeling<E> {
if (port.checkConf && !invalidate){
port.checkConfStatus = r;
port.mappingName= mappingName;
+ //Add Result Trace also
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -857,14 +864,16 @@ public class TMLModeling<E> {
}
}*/
}
+ //
}
public TGComponent getTGComponent(){
return (TGComponent) getTasks().get(0).getReferenceObject();
}
- public void backtraceAuthenticity(Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults, String mappingName) {
+ public void backtraceAuthenticity(ProVerifOutputAnalyzer pvoa, String mappingName) {
// TraceManager.addDev("Backtracing Authenticity");
+ Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults();
for (AvatarPragmaAuthenticity pragma: authenticityResults.keySet()) {
ProVerifQueryAuthResult result = authenticityResults.get(pragma);
// TODO: deal directly with pragma instead of s
@@ -885,6 +894,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkStrongAuthStatus = 3;
port.mappingName= mappingName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -932,6 +946,11 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 3;
TraceManager.addDev("not verified " + signalName);
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -958,6 +977,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkWeakAuthStatus = 3;
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -976,7 +1000,12 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkWeakAuthStatus = 2;
port.mappingName= mappingName;
- }
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
+ }
}
}
signalName = s.split("_reqData")[0];
@@ -1028,6 +1057,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkWeakAuthStatus = 2;
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -1054,6 +1088,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkWeakAuthStatus = 2;
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -1076,6 +1115,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkStrongAuthStatus = 2;
port.mappingName= mappingName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -1128,9 +1172,14 @@ public class TMLModeling<E> {
if (channel!=null){
for (TMLCPrimitivePort port:channel.ports){
// TraceManager.addDev("adding to port " + channelName);
- if (port.checkAuth){
+ if (port.checkAuth){
port.checkStrongAuthStatus = 2;
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -1158,6 +1207,11 @@ public class TMLModeling<E> {
if (port.checkAuth){
port.checkStrongAuthStatus = 2;
port.secName= signalName;
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace !=null){
+ port.setResultTrace(trace);
+ port.setPragmaString(pragma.toString());
+ }
}
}
}
@@ -1181,6 +1235,8 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 1;
port.checkWeakAuthStatus=1;
}
+ port.setResultTrace(null);
+ port.setPragmaString("");
}
}
for (TMLRequest req: getRequests()){
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index f82f2a6bde..945c824752 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -1481,7 +1481,7 @@ public class TML2Avatar {
this.avspec = new AvatarSpecification("spec", null);
}
attrsToCheck.clear();
- //tmlmodel.removeForksAndJoins();
+ tmlmodel.removeForksAndJoins();
//Only set the loop limit if it's a number
String pattern = "^[0-9]{1,2}$";
Pattern r = Pattern.compile(pattern);
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index ec035b63bf..af83b0ad73 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1712,7 +1712,7 @@ memloop:
} else if (tmap != null) {
t2a = new TML2Avatar(tmap, false, true);
avatarspec = t2a.generateAvatarSpec(loopLimit);
- // drawPanel(avatarspec, mgui.getFirstAvatarDesignPanelFound());
+ // drawPanel(avatarspec, mgui.getFirstAvatarDesignPanelFound());
} else if (tmlm != null) {
//Generate default mapping
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index bf3fd49ab2..8d624c4a52 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4469,12 +4469,12 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getAuthenticityResults(), getTabName(tp));
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
} else if (tp instanceof TMLComponentDesignPanel) {
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getAuthenticityResults(), "Default Mapping");
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, "Default Mapping");
}
return;
}
diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java
index 249f3f5e6e..832e888d50 100755
--- a/src/main/java/ui/TDiagramPanel.java
+++ b/src/main/java/ui/TDiagramPanel.java
@@ -65,6 +65,7 @@ import ui.syscams.SysCAMSRecordComponent;
import ui.tmlcd.TMLTaskOperator;
import ui.tmlcompd.TMLCCompositeComponent;
import ui.tmlcompd.TMLCPrimitiveComponent;
+import ui.tmlcompd.TMLCPrimitivePort;
import ui.tmlcompd.TMLCRecordComponent;
import ui.window.JDialogCode;
import ui.window.JDialogNote;
@@ -131,6 +132,7 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
protected JMenuItem remove, edit, clone, bringFront, bringBack, makeSquare, setJavaCode, removeJavaCode, setInternalComment, removeInternalComment, attach, detach, hide, unhide, search, enableDisable, setAsCryptoBlock, setAsRegularBlock;
protected JMenuItem checkAccessibility, checkInvariant, checkMasterMutex, checkLatency;
protected JMenuItem gotoReference;
+ protected JMenuItem showProVerifTrace;
protected JMenuItem breakpoint;
protected JMenuItem paste, insertLibrary, upX, upY, downX, downY, fitToContent, backToMainDiagram;
protected JMenuItem cut, copy, saveAsLibrary, captureSelected;
@@ -1454,6 +1456,7 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
componentMenu.add(checkInvariant);
componentMenu.add(checkLatency);
componentMenu.add(gotoReference);
+ componentMenu.add(showProVerifTrace);
componentMenu.add(checkMasterMutex);
componentMenu.add(breakpoint);
@@ -1569,6 +1572,9 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
gotoReference = new JMenuItem("Go to reference");
gotoReference.addActionListener(menuAL);
+
+ showProVerifTrace= new JMenuItem("Show ProVerif Trace");
+ showProVerifTrace.addActionListener(menuAL);
search = new JMenuItem("External Search");
search.addActionListener(menuAL);
@@ -1848,7 +1854,13 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
}
}
-
+
+ if (e.getSource() == showProVerifTrace) {
+ if (componentPopup instanceof TMLCPrimitivePort){
+ ((TMLCPrimitivePort) componentPopup).showTrace();
+ }
+ }
+
if (e.getSource() == checkMasterMutex) {
if (componentPopup instanceof CheckableInvariant) {
@@ -2101,6 +2113,13 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
gotoReference.setEnabled(false);
}
+
+ if (componentPointed instanceof TMLCPrimitivePort){
+ showProVerifTrace.setEnabled(true);
+ } else {
+ showProVerifTrace.setEnabled(false);
+ }
+
if (componentPointed instanceof CheckableInvariant) {
checkInvariant.setEnabled(true);
diff --git a/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java b/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
index 9cca0d125a..88098c5904 100755
--- a/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
+++ b/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
@@ -905,7 +905,7 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS
// Latencies
latencyPanel = new JPanel();
- infoTab.addTab("Latencies", IconManager.imgic1202, latencyPanel, "Latencies");
+ infoTab.addTab("Latencies", IconManager.imgic1202, new JScrollPane(latencyPanel), "Latencies");
GridBagLayout gridbag0 = new GridBagLayout();
GridBagConstraints c0 = new GridBagConstraints();
latencyPanel.setLayout(gridbag0);
@@ -955,8 +955,8 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS
((latTable.getColumnModel()).getColumn(3)).setPreferredWidth(100);
((latTable.getColumnModel()).getColumn(4)).setPreferredWidth(100);
((latTable.getColumnModel()).getColumn(5)).setPreferredWidth(100);
- latTable.setAutoResizeMode(JTable.AUTO_RESIZE_ALL_COLUMNS);
- jspLatency = new JScrollPane(latTable);
+ // latTable.setAutoResizeMode(JTable.AUTO_RESIZE_OFF);
+ jspLatency = new JScrollPane(latTable, JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED, JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
jspLatency.setWheelScrollingEnabled(true);
jspLatency.getVerticalScrollBar().setUnitIncrement(10);
jspLatency.setMinimumSize(new Dimension(1200, 100));
diff --git a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
index 6137d19b9e..0280a3ee7f 100755
--- a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
+++ b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
@@ -932,7 +932,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
GridBagLayout gridbag0 = new GridBagLayout();
GridBagConstraints c0 = new GridBagConstraints();
latencyPanel.setLayout(gridbag0);
- infoTab.addTab("Latency", null, latencyPanel, "Latency Measurements");
+ infoTab.addTab("Latency", null, new JScrollPane(latencyPanel), "Latency Measurements");
c0.gridwidth = GridBagConstraints.REMAINDER;
latencyPanel.add(new JLabel("Latencies shown in number of cycles relative to the main clock"), c0);
@@ -1875,6 +1875,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
// for (int i=0; i<elt.getAttributes().getLength(); i++){
//
// }
+ // System.out.println("element " + elt);
id = null;
name = null;
command = null;
@@ -1994,7 +1995,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
}
if (elt.getTagName().compareTo(SIMULATION_TRANS) == 0) {
-
+ //System.out.println("EL " + elt.getAttribute("messageid"));
SimulationTransaction st = new SimulationTransaction();
st.nodeType = elt.getAttribute("deviceid");
diff --git a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
index 7bff1cfa02..087baf4e4f 100755
--- a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
@@ -59,6 +59,18 @@ import ui.tmlad.TMLADNotifiedEvent;
import ui.tmldd.TMLArchiCPNode;
import ui.tmldd.TMLArchiPortArtifact;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
+
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
+
import javax.swing.*;
import java.awt.*;
import java.util.Vector;
@@ -108,14 +120,22 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
public static int TOCHECK = 1;
public static int CHECKED_CONF = 2;
public static int CHECKED_UNCONF = 3;
+
+ //ProVerifTrace
+ String pragma;
+ ProVerifResultTrace resTrace;
+
public String mappingName="???";
protected int decPoint = 3;
+
protected boolean conflict = false;
protected String conflictMessage;
protected String dataFlowType = "VOID";
protected String associatedEvent = "VOID";
+
+
public int verification;
@@ -454,6 +474,8 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
g.drawRect(x-lockwidth*3/2, y+lockheight/2+yoffset, lockwidth, lockheight);
}
}
+
+
public void manageMove() {
//
@@ -624,8 +646,43 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
((TMLComponentTaskDiagramPanel)tdp).updatePorts();
+
return true;
}
+
+ public void showTrace(){
+ //Show Result trace
+ PipedOutputStream pos = new PipedOutputStream();
+ try {
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), pragma);
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
+ jfssdp.setVisible(true);
+ //jfssdp.setModalExclusionType(ModalExclusionType
+ // .APPLICATION_EXCLUDE);
+ jfssdp.toFront();
+
+ // TraceManager.addDev("\n--- Trace ---");
+ int i = 0;
+ for (ProVerifResultTraceStep step : resTrace.getTrace()) {
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ } finally {
+ try {
+ pos.close();
+ } catch (IOException ignored) {
+ }
+ }
+
+ }
protected String translateExtraParam() {
TType a;
@@ -966,6 +1023,14 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
}
return true;
}
+
+ public void setResultTrace(ProVerifResultTrace trace){
+ resTrace = trace;
+ }
+
+ public void setPragmaString(String str){
+ pragma=str;
+ }
public void setPortName(String s) {
for (TURTLEPanel tp : tdp.getMainGUI().tabs) {
--
GitLab