Commit 36de1efb authored by Florian Lugou's avatar Florian Lugou

changed ProVerif output analysis to print results in real time

parent 43e3e594
......@@ -51,7 +51,7 @@ import ui.avatarbd.AvatarBDPragma;
import java.util.*;
public abstract class AvatarPragma extends AvatarElement {
public abstract class AvatarPragma extends AvatarElement implements Comparable<AvatarPragma> {
public static final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"};
public static final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"};
......@@ -423,4 +423,10 @@ public abstract class AvatarPragma extends AvatarElement {
* @return A full clone of the pragma.
*/
public abstract AvatarPragma advancedClone(AvatarSpecification avspec);
@Override
public int compareTo(AvatarPragma b)
{
return this.toString().compareTo(b.toString());
}
}
......@@ -311,13 +311,13 @@ class ExecutionThread extends Thread {
return;
}
TraceManager.addDev("Going to start command " + cmd + "..." );
// TraceManager.addDev("Going to start command " + cmd + "..." );
final PrintStream out = new PrintStream( s.getOutputStream(), true );
proc = Runtime.getRuntime().exec(cmd);
if ( parentExecThread != null ) {
TraceManager.addDev( "Giving my pipe to the other..." );
// TraceManager.addDev( "Giving my pipe to the other..." );
parentExecThread.setMyPipe( proc.getOutputStream() );
}
......@@ -326,7 +326,7 @@ class ExecutionThread extends Thread {
//TraceManager.addDev("Reading the output stream of the process " + cmd);
while ( go && ( str = proc_in.readLine() ) != null ) {
TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
// TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
respond( out, ResponseCode.PROCESS_OUTPUT, str );
}
......
......@@ -318,6 +318,15 @@ public class RshClient {
}
}
public RshClientReader getDataReaderFromProcess() throws LauncherException {
Socket socket = connect(portString);
try {
return new RshClientReader(socket);
} catch(IOException e) {
throw new LauncherException(IO_ERROR, e);
}
}
public void writeCommandMessages( final Writer output )
throws LauncherException {
......
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT enst.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
package launcher;
import java.io.Reader;
import java.io.PipedInputStream;
import java.io.PipedOutputStream;
import java.io.InputStreamReader;
import java.io.IOException;
import java.net.Socket;
import java.net.SocketTimeoutException;
/**
* Class RshClientReader
* Creation: 03/06/2017
* @version 1 03/06/2017
* @author Florian LUGOU
*/
public class RshClientReader extends Reader implements Runnable {
private PipedOutputStream pos;
private InputStreamReader pis;
private Socket clientSocket;
private Thread forwardingThread;
private boolean go = true;
private StringBuilder builder;
private boolean isNewLine = true;
public RshClientReader(Socket clientSocket) throws IOException {
this.clientSocket = clientSocket;
this.pos = new PipedOutputStream();
this.pis = new InputStreamReader(new PipedInputStream(pos));
this.forwardingThread = new Thread(this);
try {
this.forwardingThread.start();
} catch (IllegalThreadStateException e) {}
}
private void consumeOldLine(String s) throws IOException
{
int n = s.indexOf('\n');
if (n >= 0) {
this.pos.write(s.substring(0, n+1).getBytes());
this.pos.flush();
isNewLine = true;
this.consumeNewLine(s.substring(n+1));
} else {
this.pos.write(s.getBytes());
this.pos.flush();
}
}
private void consumeNewLine(String s) throws IOException
{
ResponseCode code = SocketComHelper.responseCode(s);
if (code == ResponseCode.PROCESS_END) {
this.go = false;
}
else if (code == null) {
this.builder.append(s);
}
else {
s = SocketComHelper.message(code, s);
this.isNewLine = false;
this.consumeOldLine(s);
}
}
@Override
public void run()
{
this.builder = new StringBuilder();
try {
this.clientSocket.setSoTimeout(100);
InputStreamReader socketReader = new InputStreamReader(this.clientSocket.getInputStream());
try {
while(this.go)
{
char[] cbuf = new char[50];
int n = 0;
try {
n = socketReader.read(cbuf);
if (n < 0)
break;
} catch(SocketTimeoutException e) {
if (n > 0)
this.builder.append(cbuf, 0, n);
continue;
}
this.builder.append(cbuf, 0, n);
String s = this.builder.toString();
this.builder = new StringBuilder();
if (isNewLine)
{
this.consumeNewLine(s);
}
else
{
this.consumeOldLine(s);
}
}
} catch(IOException e) {
} finally {
try {
socketReader.close();
} catch(IOException e) {}
try {
this.pos.close();
} catch(IOException e) {}
}
} catch(IOException e) {
} finally {
try {
this.clientSocket.close();
} catch(IOException e) {}
}
}
@Override
public int read(char[] cbuf, int off, int len) throws IOException
{
int n = this.pis.read(cbuf, off, len);
return n;
}
@Override
public void close() throws IOException
{
this.go = false;
try {
this.pis.close();
} catch(IOException e) {}
}
}
......@@ -48,10 +48,12 @@ package proverifspec;
import avatartranslator.*;
import avatartranslator.toproverif.AVATAR2ProVerif;
import java.io.Reader;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.StringReader;
import java.util.HashMap;
import java.util.Map;
import java.util.concurrent.ConcurrentHashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.regex.Matcher;
......@@ -80,19 +82,38 @@ public class ProVerifOutputAnalyzer {
private final static String untypedAuthSplit = "==> evinj:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private final static String untypedWeakAuthSplit = "==> ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private HashMap<AvatarPragma, ProVerifQueryResult> results;
private ConcurrentHashMap<AvatarPragma, ProVerifQueryResult> results;
private LinkedList<String> errors;
private LinkedList<ProVerifOutputListener> listeners;
private AVATAR2ProVerif avatar2proverif;
public ProVerifOutputAnalyzer(AVATAR2ProVerif avatar2proverif) {
this.avatar2proverif = avatar2proverif;
this.errors = null;
this.results = null;
this.listeners = new LinkedList<>();
}
public void addListener(ProVerifOutputListener listener)
{
this.listeners.add(listener);
}
public void removeListener(ProVerifOutputListener listener)
{
this.listeners.remove(listener);
}
private void notifyListeners()
{
for (ProVerifOutputListener listener: this.listeners)
listener.proVerifOutputChanged();
}
public void analyzeOutput(String _s, boolean isTyped) {
BufferedReader reader = new BufferedReader(new StringReader(_s));
public void analyzeOutput(Reader reader, boolean isTyped) {
BufferedReader bReader = new BufferedReader(reader);
List<AvatarPragma> pragmas = this.avatar2proverif.getAvatarSpecification().getPragmas();
String previous = null;
String str;
......@@ -101,7 +122,7 @@ public class ProVerifOutputAnalyzer {
ProVerifResultTrace resultTrace = new ProVerifResultTrace(proverifProcess);
boolean isInTrace = false;
this.results = new HashMap<AvatarPragma, ProVerifQueryResult> ();
this.results = new ConcurrentHashMap<AvatarPragma, ProVerifQueryResult> ();
this.errors = new LinkedList<String>();
Pattern procPattern = Pattern.compile(" *\\{\\d+\\}(.*)");
......@@ -109,7 +130,7 @@ public class ProVerifOutputAnalyzer {
try {
// Loop through every line in the output
while ((str = reader.readLine()) != null)
while ((str = bReader.readLine()) != null)
{
if (str.isEmpty())
continue;
......@@ -194,6 +215,7 @@ public class ProVerifOutputAnalyzer {
if (reachabilityPragma != null)
{
this.results.put(reachabilityPragma, result);
this.notifyListeners();
}
}
......@@ -226,6 +248,7 @@ public class ProVerifOutputAnalyzer {
if (trueName != null && trueName.equals(attributeName))
{
this.results.put(pragma, result);
this.notifyListeners();
}
}
}
......@@ -306,6 +329,7 @@ public class ProVerifOutputAnalyzer {
&& pragmaAuth.getAttrB().getAttribute() == attribute1)
{
this.results.put(pragma, result);
this.notifyListeners();
break;
}
}
......@@ -320,6 +344,7 @@ public class ProVerifOutputAnalyzer {
if (previousAuthPragma != null)
{
previousAuthPragma.setWeakSatisfied(true);
this.notifyListeners();
}
previousAuthPragma = null;
}
......@@ -331,6 +356,7 @@ public class ProVerifOutputAnalyzer {
if (previousAuthPragma != null)
{
previousAuthPragma.setWeakSatisfied(false);
this.notifyListeners();
}
previousAuthPragma = null;
}
......@@ -341,7 +367,9 @@ public class ProVerifOutputAnalyzer {
// Found an error
else if (str.contains("Error:"))
{
this.errors.add(str + ": " + previous);
synchronized(errors) {
this.errors.add(str + ": " + previous);
}
}
previous = str;
......@@ -398,7 +426,7 @@ public class ProVerifOutputAnalyzer {
return state;
}
public HashMap<AvatarPragma, ProVerifQueryResult> getResults()
public Map<AvatarPragma, ProVerifQueryResult> getResults()
{
return this.results;
}
......@@ -458,6 +486,8 @@ public class ProVerifOutputAnalyzer {
}
public LinkedList<String> getErrors() {
return errors;
synchronized(errors) {
return errors;
}
}
}
/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT enst.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*
* /**
* Class ProVerifOutputListener
* Creation: 02/06/2017
* @version 1.0 02/06/2017
* @author Florian LUGOU
* @see
*/
package proverifspec;
public interface ProVerifOutputListener {
public void proVerifOutputChanged();
}
......@@ -1990,7 +1990,7 @@ public class GTURTLEModeling {
rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
rshc.sendExecuteCommandRequest();
String data = rshc.getDataFromProcess();
Reader data = rshc.getDataReaderFromProcess();
ProVerifOutputAnalyzer pvoa = getProVerifOutputAnalyzer ();
pvoa.analyzeOutput(data, true);
......
......@@ -55,6 +55,8 @@ import javax.swing.*;
import java.awt.*;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.io.BufferedReader;
//import javax.swing.event.*;
......@@ -105,6 +107,14 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
initActions();
makeComponents();
//setComponents();
this.addComponentListener(new ComponentAdapter() {
@Override
public void componentResized(ComponentEvent e)
{
if (JFrameSimulationSDPanel.this.sdpanel != null)
JFrameSimulationSDPanel.this.sdpanel.resized();
}
});
}
private JLabel createStatusBar() {
......
......@@ -176,6 +176,11 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
public void setMyScrollPanel(JScrollPane _jsp) {
jsp = _jsp;
}
public void resized() {
this.spaceBetweenLifeLinesComputed = false;
this.repaint();
}
protected void paintComponent(Graphics g) {
super.paintComponent(g);
......
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