- More refactoring.

This commit is contained in:
ccremers 2006-08-04 22:00:22 +00:00
parent 83e1d9375d
commit 4034e3a42e
3 changed files with 93 additions and 70 deletions

View File

@ -221,7 +221,7 @@ class MainWindow(wx.Frame):
os.chdir(self.dirname) os.chdir(self.dirname)
def RunScyther(self, mode): def RunScyther(self, mode):
Scytherthread.RunScyther(self,mode) s = Scytherthread.ScytherRun(self,mode)
def OnVerify(self, event): def OnVerify(self, event):
self.RunScyther("verify") self.RunScyther("verify")
@ -288,7 +288,7 @@ class SettingsWindow(wx.Panel):
def EvtMisc(self,evt): def EvtMisc(self,evt):
self.misc = evt.GetString() self.misc = evt.GetString()
def ScytherArguments(self): def ScytherArguments(self,mode):
""" Note: constructed strings should have a space at the end to """ Note: constructed strings should have a space at the end to
correctly separate the options. correctly separate the options.
""" """
@ -301,11 +301,11 @@ class SettingsWindow(wx.Panel):
tstr += "--match=%s " % (str(self.match)) tstr += "--match=%s " % (str(self.match))
# Verification type # Verification type
if self.mode == "check": if mode == "check":
tstr += "--check " tstr += "--check "
if self.mode == "autoverify": elif mode == "autoverify":
tstr += "--auto-claims " tstr += "--auto-claims "
elif self.mode == "statespace": elif mode == "statespace":
tstr += "--state-space " tstr += "--state-space "
# Anything else? # Anything else?

View File

@ -21,7 +21,18 @@ from Misc import *
class Scyther(object): class Scyther(object):
def __init__ ( self): def __init__ ( self):
# Where is my executable?
if sys.platform.startswith('win'):
""" Windows """
# TODO hardcoded for now, bad
scyther.program = "c:\\Scyther.exe"
if not os.path.isfile(scyther.program):
print "I can't find the Scyther executable %s" % (scyther.program)
else:
""" Non-windows """
self.program = "scyther" self.program = "scyther"
self.options = "" self.options = ""
self.spdl = None self.spdl = None
self.inputfile = None self.inputfile = None

View File

@ -28,16 +28,17 @@ import Attackwindow
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
class ScytherThread(threading.Thread): class ScytherThread(threading.Thread):
""" 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: # Override Thread's __init__ method to accept the parameters needed:
def __init__ ( self, mainwin, spdl, details, verifywin ): def __init__ ( self, parent ):
self.mainwin = mainwin self.parent = parent
self.verifywin = verifywin parent.verified = False
self.spdl = spdl parent.claims = []
self.details = details
self.verified = False
self.claims = []
threading.Thread.__init__ ( self ) threading.Thread.__init__ ( self )
@ -48,35 +49,32 @@ class ScytherThread(threading.Thread):
# Results are done (claimstatus can be reported) # Results are done (claimstatus can be reported)
# Shoot down the verification window and let the RunScyther function handle the rest # Shoot down the verification window and let the RunScyther function handle the rest
self.verified = True self.parent.verified = True
self.verifywin.Close() self.parent.verifywin.Close()
def claimResults(self): def claimResults(self):
""" Convert spdl to result (using Scyther) """ Convert spdl to result (using Scyther)
The list of claim goes back to self.mainwin.claims, which is a
property of the main window
""" """
scyther = Scyther.Scyther() scyther = Scyther.Scyther()
scyther.options = self.mainwin.settings.ScytherArguments() scyther.options = self.parent.options
if sys.platform.startswith('win'):
""" Windows """
scyther.program = "c:\\Scyther.exe"
if not os.path.isfile(scyther.program):
print "I can't find the Scyther executable %s" % (scyther.program)
scyther.setInput(self.spdl) scyther.setInput(self.parent.spdl)
self.mainwin.claims = scyther.verify() self.parent.claims = scyther.verify()
self.summary = str(scyther) self.parent.summary = str(scyther)
#---------------------------------------------------------------------------
class AttackThread(threading.Thread): class AttackThread(threading.Thread):
# Override Thread's __init__ method to accept the parameters needed:
def __init__ ( self, mainwin, resultwin ):
self.mainwin = mainwin """ This is a thread because it computes images from stuff in the
background """
# Override Thread's __init__ method to accept the parameters needed:
def __init__ ( self, parent, resultwin ):
self.parent = parent
self.resultwin = resultwin self.resultwin = resultwin
threading.Thread.__init__ ( self ) threading.Thread.__init__ ( self )
@ -88,7 +86,7 @@ class AttackThread(threading.Thread):
def makeImages(self): def makeImages(self):
""" create images """ """ create images """
for cl in self.mainwin.claims: for cl in self.parent.claims:
for attack in cl.attacks: for attack in cl.attacks:
self.makeImage(attack) self.makeImage(attack)
if cl.button and len(cl.attacks) > 0: if cl.button and len(cl.attacks) > 0:
@ -138,13 +136,13 @@ class VerificationWindow(wx.Dialog):
class ResultWindow(wx.Frame): class ResultWindow(wx.Frame):
def __init__( def __init__(
self, mainwindow, ID, title, pos=wx.DefaultPosition, size=wx.DefaultSize, self, parent, parentwindow, title, pos=wx.DefaultPosition, size=wx.DefaultSize,
style=wx.DEFAULT_DIALOG_STYLE style=wx.DEFAULT_DIALOG_STYLE
): ):
self.mainwindow = mainwindow self.parent = parent
wx.Frame.__init__(self,mainwindow,ID,title,pos,size,style) wx.Frame.__init__(self,parentwindow,-1,title,pos,size,style)
self.thread = None self.thread = None
self.Bind(wx.EVT_CLOSE, self.onCloseWindow) self.Bind(wx.EVT_CLOSE, self.onCloseWindow)
@ -155,14 +153,21 @@ class ResultWindow(wx.Frame):
def onViewButton(self,evt): def onViewButton(self,evt):
btn = evt.GetEventObject() btn = evt.GetEventObject()
(y,x) = self.grid.GetItemPosition(btn) (y,x) = self.grid.GetItemPosition(btn)
n = len(self.mainwindow.claims) n = len(self.parent.claims)
cln = n-y cln = n-y
cl = self.mainwindow.claims[cln] cl = self.parent.claims[cln]
w = Attackwindow.AttackWindow(cl) w = Attackwindow.AttackWindow(cl)
def onCloseWindow(self,evt): def onCloseWindow(self,evt):
# TODO we should kill self.thread # TODO we should kill self.thread
self.mainwindow.claims = None
# Clean up
for cl in self.parent.claims:
if cl.pngfile:
os.unlink(cl.pngfile)
cl.pngfile = None
self.parent.claims = None
self.Destroy() self.Destroy()
@ -172,7 +177,7 @@ class ResultWindow(wx.Frame):
sizer = wx.BoxSizer(wx.VERTICAL) sizer = wx.BoxSizer(wx.VERTICAL)
# For these claims... # For these claims...
claims = self.mainwindow.claims claims = self.parent.claims
# set up grid # set up grid
self.grid = grid = wx.GridBagSizer(7,1+len(claims)) self.grid = grid = wx.GridBagSizer(7,1+len(claims))
@ -272,20 +277,26 @@ class ResultWindow(wx.Frame):
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
def RunScyther(mainwin,mode): class ScytherRun(object):
def __init__(self,mainwin,mode):
self.mainwin = mainwin
self.mode = mode
self.spdl = mainwin.control.GetValue()
# Verification window # Verification window
verifywin = VerificationWindow(mainwin,-1,mode) self.verifywin = verifywin = VerificationWindow(mainwin,-1,mode)
verifywin.CenterOnScreen() verifywin.CenterOnScreen()
verifywin.Show(True) verifywin.Show(True)
# start the thread # start the thread
self.options = mainwin.settings.ScytherArguments(mode)
self.verified = False
verifywin.SetCursor(wx.StockCursor(wx.CURSOR_WAIT)) verifywin.SetCursor(wx.StockCursor(wx.CURSOR_WAIT))
mainwin.settings.mode = mode t = ScytherThread(self)
t = ScytherThread(mainwin,mainwin.control.GetValue(),"",verifywin)
t.start() t.start()
# start the window and show until something happens # start the window and show until something happens
@ -297,19 +308,20 @@ def RunScyther(mainwin,mode):
# Cursor back to normal # Cursor back to normal
verifywin.SetCursor(wx.StockCursor(wx.CURSOR_ARROW)) verifywin.SetCursor(wx.StockCursor(wx.CURSOR_ARROW))
if t.verified: if self.verified:
# Great, we verified stuff, progress to the claim report # Great, we verified stuff, progress to the claim report
title = "Scyther results : %s" % mode title = "Scyther results : %s" % mode
resultwin = ResultWindow(mainwin,-1,title) self.resultwin = resultwin = ResultWindow(self,mainwin,title)
resultwin.Show(1) resultwin.Show(1)
t = AttackThread(mainwin,resultwin) t = AttackThread(self,resultwin)
t.start() t.start()
resultwin.thread = t resultwin.thread = t
resultwin.CenterOnScreen() resultwin.CenterOnScreen()
resultwin.Show(True) resultwin.Show(True)
#---------------------------------------------------------------------------