scyther/gui/Scytherthread.py

328 lines
9.4 KiB
Python
Raw Normal View History

2006-08-02 13:59:57 +01:00
#!/usr/bin/python
#---------------------------------------------------------------------------
""" Import externals """
import wx
import wx.lib.newevent
import os
import sys
import re
import threading
import StringIO
#---------------------------------------------------------------------------
""" Import scyther components """
import XMLReader
""" Import scyther-gui components """
import Tempfile
import Claim
import Preference
import Scyther
2006-08-03 14:40:39 +01:00
import Attackwindow
2006-08-02 13:59:57 +01:00
#---------------------------------------------------------------------------
#---------------------------------------------------------------------------
class ScytherThread(threading.Thread):
2006-08-04 23:00:22 +01:00
""" The reason this is a thread is because we might to decide to
abort it. However, apparently Python has no good support for killing
threads yet :( """
# Override Thread's __init__ method to accept the parameters needed:
def __init__ ( self, parent ):
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
self.parent = parent
parent.verified = False
parent.claims = []
2006-08-02 13:59:57 +01:00
threading.Thread.__init__ ( self )
def run(self):
self.claimResults()
# Results are done (claimstatus can be reported)
2006-08-03 13:06:43 +01:00
# Shoot down the verification window and let the RunScyther function handle the rest
2006-08-04 23:00:22 +01:00
self.parent.verified = True
self.parent.verifywin.Close()
2006-08-02 13:59:57 +01:00
def claimResults(self):
""" Convert spdl to result (using Scyther)
"""
2006-08-02 13:59:57 +01:00
scyther = Scyther.Scyther()
2006-08-02 23:07:29 +01:00
2006-08-04 23:00:22 +01:00
scyther.options = self.parent.options
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
scyther.setInput(self.parent.spdl)
self.parent.claims = scyther.verify()
self.parent.summary = str(scyther)
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
#---------------------------------------------------------------------------
2006-08-03 13:06:43 +01:00
class AttackThread(threading.Thread):
2006-08-04 23:00:22 +01:00
""" This is a thread because it computes images from stuff in the
background """
2006-08-03 13:06:43 +01:00
# Override Thread's __init__ method to accept the parameters needed:
2006-08-04 23:00:22 +01:00
def __init__ ( self, parent, resultwin ):
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
self.parent = parent
2006-08-03 13:06:43 +01:00
self.resultwin = resultwin
threading.Thread.__init__ ( self )
def run(self):
# create the images in the background
self.makeImages()
2006-08-02 13:59:57 +01:00
def makeImages(self):
""" create images """
2006-08-04 23:00:22 +01:00
for cl in self.parent.claims:
for attack in cl.attacks:
self.makeImage(attack)
2006-08-03 15:14:38 +01:00
if cl.button and len(cl.attacks) > 0:
2006-08-03 14:40:39 +01:00
cl.button.Enable()
def makeImage(self,attack):
""" create image for this particular attack """
(fd2,fpname2) = Tempfile.tempcleaned(".png")
pw,pr = os.popen2("dot -Tpng -o%s" % (fpname2))
pw.write(attack.scytherDot)
pw.close()
2006-08-03 14:40:39 +01:00
pr.close()
attack.pngfile = fpname2 # this is where the file name is stored
#---------------------------------------------------------------------------
2006-08-03 13:06:43 +01:00
class VerificationWindow(wx.Dialog):
def __init__(
self, parent, ID, title, pos=wx.DefaultPosition, size=wx.DefaultSize,
2006-08-03 13:06:43 +01:00
style=wx.DEFAULT_DIALOG_STYLE
):
wx.Dialog.__init__(self,parent,ID,title,pos,size,style)
2006-08-03 13:06:43 +01:00
sizer = wx.BoxSizer(wx.VERTICAL)
label = wx.StaticText(self, -1, "Verifying protocol description")
2006-08-03 13:06:43 +01:00
sizer.Add(label, 0, wx.ALIGN_CENTRE|wx.ALL, 5)
line = wx.StaticLine(self, -1, size=(20,-1), style=wx.LI_HORIZONTAL)
sizer.Add(line, 0, wx.GROW|wx.ALIGN_CENTER_VERTICAL|wx.RIGHT|wx.TOP, 5)
btnsizer = wx.StdDialogButtonSizer()
btn = wx.Button(self, wx.ID_CANCEL)
btnsizer.AddButton(btn)
btnsizer.Realize()
sizer.Add(btnsizer, 0, wx.ALIGN_CENTER_VERTICAL|wx.ALL, 5)
self.SetSizer(sizer)
sizer.Fit(self)
#---------------------------------------------------------------------------
2006-08-03 14:40:39 +01:00
class ResultWindow(wx.Frame):
2006-08-03 13:06:43 +01:00
def __init__(
2006-08-04 23:00:22 +01:00
self, parent, parentwindow, title, pos=wx.DefaultPosition, size=wx.DefaultSize,
2006-08-04 22:19:38 +01:00
style=wx.DEFAULT_DIALOG_STYLE
2006-08-03 13:06:43 +01:00
):
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
self.parent = parent
2006-08-04 23:00:22 +01:00
wx.Frame.__init__(self,parentwindow,-1,title,pos,size,style)
2006-08-03 14:40:39 +01:00
self.thread = None
self.Bind(wx.EVT_CLOSE, self.onCloseWindow)
2006-08-03 13:06:43 +01:00
2006-08-04 22:28:58 +01:00
self.BuildTable()
def onViewButton(self,evt):
btn = evt.GetEventObject()
2006-08-04 23:08:00 +01:00
w = Attackwindow.AttackWindow(btn.claim)
w.Show(True)
2006-08-04 22:28:58 +01:00
def onCloseWindow(self,evt):
# TODO we should kill self.thread
2006-08-04 23:00:22 +01:00
# Clean up
for cl in self.parent.claims:
2006-08-04 23:08:00 +01:00
for attack in cl.attacks:
if attack.pngfile:
os.unlink(attack.pngfile)
attack.pngfile = None
2006-08-04 23:00:22 +01:00
self.parent.claims = None
2006-08-04 22:28:58 +01:00
self.Destroy()
def BuildTable(self):
2006-08-03 13:06:43 +01:00
# Now continue with the normal construction of the dialog
# contents
sizer = wx.BoxSizer(wx.VERTICAL)
2006-08-04 22:28:58 +01:00
# For these claims...
2006-08-04 23:00:22 +01:00
claims = self.parent.claims
2006-08-04 22:28:58 +01:00
2006-08-03 14:40:39 +01:00
# set up grid
2006-08-03 15:45:47 +01:00
self.grid = grid = wx.GridBagSizer(7,1+len(claims))
2006-08-03 14:40:39 +01:00
def titlebar(x,title,width=1):
txt = wx.StaticText(self,-1,title)
2006-08-03 15:14:38 +01:00
font = wx.Font(14,wx.NORMAL,wx.NORMAL,wx.NORMAL)
txt.SetFont(font)
grid.Add(txt,(0,x),(1,width))
2006-08-03 15:14:38 +01:00
titlebar(0,"Claim",5)
if len(claims) > 0:
sn = claims[0].stateName(2)
resulttxt = sn[0].upper() + sn[1:]
else:
resultxt = "Results"
titlebar(5,resulttxt,2)
2006-08-03 14:40:39 +01:00
2006-08-04 22:28:58 +01:00
self.lastprot = None
self.lastrole = None
for index in range(0,len(claims)):
# we reverse the display order of the claims!
2006-08-04 22:28:58 +01:00
cl = claims[len(claims)-index-1]
self.BuildClaim(grid,cl,index+1)
2006-08-03 14:40:39 +01:00
sizer.Add(grid, 0,wx.ALIGN_CENTRE|wx.ALL,5)
2006-08-03 13:06:43 +01:00
self.SetSizer(sizer)
sizer.Fit(self)
2006-08-04 22:28:58 +01:00
def BuildClaim(self,grid,cl,ypos):
# a support function
def addtxt(txt,column):
grid.Add(wx.StaticText(self,-1,txt),(ypos,column),(1,1),wx.ALIGN_CENTER_VERTICAL)
2006-08-04 22:28:58 +01:00
# button for ok/fail
tsize = (16,16)
if cl.okay:
bmp = wx.ArtProvider_GetBitmap(wx.ART_TICK_MARK,wx.ART_CMN_DIALOG,tsize)
else:
bmp = wx.ArtProvider_GetBitmap(wx.ART_CROSS_MARK,wx.ART_CMN_DIALOG,tsize)
if not bmp.Ok():
bmp = wx.EmptyBitmap(tsize)
bmpfield = wx.StaticBitmap(self,-1,bmp)
grid.Add(bmpfield,(ypos,0),(1,1),wx.ALIGN_CENTER_VERTICAL)
# protocol, role, label
prot = str(cl.protocol)
showPR = False
if prot != self.lastprot:
self.lastprot = prot
showPR = True
role = str(cl.role)
if role != self.lastrole:
self.lastrole = role
showPR = True
if showPR:
addtxt(prot,1)
addtxt(role,2)
addtxt(str(cl.shortlabel),3)
claimdetails = str(cl.claimtype)
if cl.parameter:
claimdetails += " %s " % (cl.parameter)
addtxt(claimdetails,4)
# add view button (if needed)
n = len(cl.attacks)
cl.button = wx.Button(self,-1,"%i %s" % (n,cl.stateName(n)))
2006-08-04 23:08:00 +01:00
cl.button.claim = cl
2006-08-04 22:28:58 +01:00
grid.Add(cl.button,(ypos,5),(1,1),wx.ALIGN_CENTER_VERTICAL)
cl.button.Disable()
if n > 0:
# Aha, something to show
self.Bind(wx.EVT_BUTTON, self.onViewButton,cl.button)
# remark something about completeness
remark = ""
if not cl.complete:
if n == 0:
# no attacks, no states within bounds
remark = "within bounds"
else:
# some attacks/states within bounds
remark = "at least, maybe more"
else:
if n == 0:
# no attacks, no states
remark = "none"
else:
# there exist n states/attacks (within any number of runs)
remark = "exactly"
addtxt(" (%s)" % remark,6)
2006-08-03 14:40:39 +01:00
2006-08-03 13:06:43 +01:00
#---------------------------------------------------------------------------
2006-08-04 23:00:22 +01:00
class ScytherRun(object):
def __init__(self,mainwin,mode):
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
self.mainwin = mainwin
self.mode = mode
self.spdl = mainwin.control.GetValue()
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
# Verification window
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
self.verifywin = verifywin = VerificationWindow(mainwin,-1,mode)
verifywin.CenterOnScreen()
verifywin.Show(True)
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
# start the thread
self.options = mainwin.settings.ScytherArguments(mode)
self.verified = False
verifywin.SetCursor(wx.StockCursor(wx.CURSOR_WAIT))
2006-08-02 13:59:57 +01:00
2006-08-04 23:00:22 +01:00
t = ScytherThread(self)
t.start()
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
# start the window and show until something happens
# if it terminates, this is a cancel, and should also kill the thread. (what happens to a spawned Scyther in that case?)
# if the thread terminames, it should close the window normally, and we end up here as well.
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
val = verifywin.ShowModal()
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
# Cursor back to normal
verifywin.SetCursor(wx.StockCursor(wx.CURSOR_ARROW))
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
if self.verified:
# Great, we verified stuff, progress to the claim report
title = "Scyther results : %s" % mode
self.resultwin = resultwin = ResultWindow(self,mainwin,title)
resultwin.Show(1)
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
t = AttackThread(self,resultwin)
t.start()
2006-08-03 13:06:43 +01:00
2006-08-04 23:00:22 +01:00
resultwin.thread = t
resultwin.CenterOnScreen()
resultwin.Show(True)
#---------------------------------------------------------------------------
2006-08-03 13:06:43 +01:00
2006-08-02 13:59:57 +01:00