- Improved refactoring, layout.
This commit is contained in:
parent
6069b36cd5
commit
4b98120da9
@ -5,17 +5,13 @@
|
|||||||
""" Import externals """
|
""" Import externals """
|
||||||
import wx
|
import wx
|
||||||
import os.path
|
import os.path
|
||||||
import sys
|
|
||||||
import wx.lib.mixins.listctrl as listmix
|
|
||||||
|
|
||||||
#---------------------------------------------------------------------------
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
""" Import scyther-gui components """
|
""" Import scyther-gui components """
|
||||||
import Preference
|
import Settingswindow
|
||||||
import Attackwindow
|
|
||||||
import Scytherthread
|
import Scytherthread
|
||||||
import Icon
|
import Icon
|
||||||
import Scyther.Claim as Claim
|
|
||||||
|
|
||||||
#---------------------------------------------------------------------------
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
@ -102,7 +98,7 @@ class MainWindow(wx.Frame):
|
|||||||
os.chdir(self.dirname)
|
os.chdir(self.dirname)
|
||||||
textfile.close()
|
textfile.close()
|
||||||
self.top.AddPage(self.control,"Protocol description")
|
self.top.AddPage(self.control,"Protocol description")
|
||||||
self.settings = SettingsWindow(self.top,self)
|
self.settings = Settingswindow.SettingsWindow(self.top,self)
|
||||||
self.top.AddPage(self.settings,"Verification parameters")
|
self.top.AddPage(self.settings,"Verification parameters")
|
||||||
|
|
||||||
#sizer.Add(self.top,1,wx.EXPAND,1)
|
#sizer.Add(self.top,1,wx.EXPAND,1)
|
||||||
@ -232,101 +228,3 @@ class MainWindow(wx.Frame):
|
|||||||
|
|
||||||
#---------------------------------------------------------------------------
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
class SettingsWindow(wx.Panel):
|
|
||||||
|
|
||||||
def __init__(self,parent,daddy):
|
|
||||||
wx.Panel.__init__(self,parent,-1)
|
|
||||||
|
|
||||||
self.win = daddy
|
|
||||||
|
|
||||||
# Bound on the number of runs
|
|
||||||
self.maxruns = int(Preference.get('maxruns','5'))
|
|
||||||
r1 = wx.StaticText(self,-1,"Maximum number of runs (0 disables bound)")
|
|
||||||
l1 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT)
|
|
||||||
l1.SetRange(0,100)
|
|
||||||
l1.SetValue(self.maxruns)
|
|
||||||
self.Bind(wx.EVT_SPINCTRL,self.EvtRuns,l1)
|
|
||||||
|
|
||||||
# Matchin options
|
|
||||||
self.match = int(Preference.get('match','0'))
|
|
||||||
claimoptions = ['typed matching','find basic type flaws','find all type flaws']
|
|
||||||
r2 = wx.StaticText(self,-1,"Matching type")
|
|
||||||
l2 = self.ch = wx.Choice(self,-1,choices=claimoptions)
|
|
||||||
l2.SetSelection(self.match)
|
|
||||||
self.Bind(wx.EVT_CHOICE,self.EvtMatch,l2)
|
|
||||||
|
|
||||||
### MISC expert stuff
|
|
||||||
|
|
||||||
# Bound on the number of classes/attacks
|
|
||||||
self.maxattacks = int(Preference.get('maxattacks','100'))
|
|
||||||
stname = Claim.stateDescription(True,2,False)
|
|
||||||
atname = Claim.stateDescription(False,2,False)
|
|
||||||
txt = "%s/%s" % (stname,atname)
|
|
||||||
r9 = wx.StaticText(self,-1,"Maximum number of %s for all claims combined (0 disables maximum)" % txt)
|
|
||||||
l9 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT)
|
|
||||||
l9.SetRange(0,100)
|
|
||||||
l9.SetValue(self.maxattacks)
|
|
||||||
self.Bind(wx.EVT_SPINCTRL,self.EvtMaxAttacks,l9)
|
|
||||||
|
|
||||||
self.misc = Preference.get('scytheroptions','')
|
|
||||||
r10 = wx.StaticText(self,-1,"Additional parameters for the Scyther tool")
|
|
||||||
l10 = wx.TextCtrl(self,-1,self.misc,size=(150,-1))
|
|
||||||
self.Bind(wx.EVT_TEXT,self.EvtMisc,l10)
|
|
||||||
|
|
||||||
# Combine
|
|
||||||
space = 10
|
|
||||||
sizer = wx.FlexGridSizer(cols=3, hgap=space,vgap=space)
|
|
||||||
sizer.AddMany([ l1,r1, (0,0),
|
|
||||||
l2,r2, (0,0),
|
|
||||||
l9,r9, (0,0),
|
|
||||||
l10,r10, (0,0),
|
|
||||||
])
|
|
||||||
self.SetSizer(sizer)
|
|
||||||
self.SetAutoLayout(True)
|
|
||||||
|
|
||||||
def EvtMatch(self,evt):
|
|
||||||
self.match = evt.GetInt()
|
|
||||||
|
|
||||||
def EvtRuns(self,evt):
|
|
||||||
self.maxruns = evt.GetInt()
|
|
||||||
|
|
||||||
def EvtMaxAttacks(self,evt):
|
|
||||||
self.maxattacks = evt.GetInt()
|
|
||||||
|
|
||||||
def EvtMisc(self,evt):
|
|
||||||
self.misc = evt.GetString()
|
|
||||||
|
|
||||||
def ScytherArguments(self,mode):
|
|
||||||
""" Note: constructed strings should have a space at the end to
|
|
||||||
correctly separate the options.
|
|
||||||
"""
|
|
||||||
|
|
||||||
tstr = ""
|
|
||||||
|
|
||||||
# Number of runs
|
|
||||||
tstr += "--max-runs=%s " % (str(self.maxruns))
|
|
||||||
# Matching type
|
|
||||||
tstr += "--match=%s " % (str(self.match))
|
|
||||||
# Max attacks/classes
|
|
||||||
if self.maxattacks != 0:
|
|
||||||
tstr += "--max-attacks=%s " % (str(self.maxattacks))
|
|
||||||
|
|
||||||
# Verification type
|
|
||||||
if mode == "check":
|
|
||||||
tstr += "--check "
|
|
||||||
elif mode == "autoverify":
|
|
||||||
tstr += "--auto-claims "
|
|
||||||
elif mode == "statespace":
|
|
||||||
tstr += "--state-space "
|
|
||||||
|
|
||||||
# Anything else?
|
|
||||||
if self.misc != "":
|
|
||||||
tstr += " " + self.misc + " "
|
|
||||||
|
|
||||||
return tstr
|
|
||||||
|
|
||||||
#---------------------------------------------------------------------------
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -111,63 +111,47 @@ class AttackThread(threading.Thread):
|
|||||||
|
|
||||||
def writeGraph(self,txt,fp):
|
def writeGraph(self,txt,fp):
|
||||||
|
|
||||||
|
EDGE = 0
|
||||||
|
NODE = 1
|
||||||
|
DEFAULT = 2
|
||||||
|
ALL = 3
|
||||||
|
|
||||||
def graphLine(txt):
|
def graphLine(txt):
|
||||||
fp.write("\t%s;\n" % (txt))
|
fp.write("\t%s;\n" % (txt))
|
||||||
|
|
||||||
def setAttr(EdgeNodeDefAll,atxt):
|
def setAttr(atxt,EdgeNodeDefAll=ALL):
|
||||||
if EdgeNodeDefAll == 3:
|
if EdgeNodeDefAll == ALL:
|
||||||
setAttr(0,atxt)
|
setAttr(atxt,EDGE)
|
||||||
setAttr(1,atxt)
|
setAttr(atxt,NODE)
|
||||||
setAttr(2,atxt)
|
setAttr(atxt,DEFAULT)
|
||||||
else:
|
else:
|
||||||
if EdgeNodeDefAll == 0:
|
if EdgeNodeDefAll == EDGE:
|
||||||
edge = "edge"
|
edge = "edge"
|
||||||
elif EdgeNodeDefAll == 1:
|
elif EdgeNodeDefAll == NODE:
|
||||||
edge = "node"
|
edge = "node"
|
||||||
else:
|
else:
|
||||||
graphLine("%s" % atxt)
|
graphLine("%s" % atxt)
|
||||||
return
|
return
|
||||||
graphLine("%s [%s]" % (edge,atxt))
|
graphLine("%s [%s]" % (edge,atxt))
|
||||||
|
|
||||||
def oldFontDefs(txt):
|
# write all graph lines but add layout modifiers
|
||||||
"""
|
|
||||||
Old hack. Remove after windows recompile TODO
|
|
||||||
"""
|
|
||||||
if txt.startswith("\tfontname"):
|
|
||||||
return True
|
|
||||||
if txt.startswith("\tfontsize"):
|
|
||||||
return True
|
|
||||||
if txt.startswith("\tnode [fontname"):
|
|
||||||
return True
|
|
||||||
if txt.startswith("\tnode [fontsize"):
|
|
||||||
return True
|
|
||||||
if txt.startswith("\tedge [fontname"):
|
|
||||||
return True
|
|
||||||
if txt.startswith("\tedge [fontsize"):
|
|
||||||
return True
|
|
||||||
return False
|
|
||||||
|
|
||||||
for l in txt.splitlines():
|
for l in txt.splitlines():
|
||||||
# hack to get rid of font defs
|
fp.write(l)
|
||||||
# TODO remove this once new windows version is compiled
|
if l.startswith("digraph"):
|
||||||
if not oldFontDefs(l):
|
# Write additional stuff for this graph
|
||||||
fp.write(l)
|
graphLine("dpi=96")
|
||||||
if l.startswith("digraph"):
|
graphLine("rankdir=TB")
|
||||||
# Write additional stuff for this graph
|
graphLine("nodesep=0.1")
|
||||||
graphLine("dpi=96")
|
graphLine("ranksep=0.001")
|
||||||
graphLine("rankdir=TB")
|
graphLine("mindist=0.1")
|
||||||
graphLine("nodesep=0.1")
|
if sys.platform.startswith("lin"):
|
||||||
graphLine("ranksep=0.001")
|
setAttr("fontname=\"Helvetica\"")
|
||||||
graphLine("mindist=0.1")
|
else:
|
||||||
if sys.platform.startswith("lin"):
|
setAttr("fontname=\"Arial\"")
|
||||||
setAttr(3,"fontname=\"Sans\"")
|
setAttr("fontsize=12")
|
||||||
else:
|
setAttr("height=\"0.01\"",NODE)
|
||||||
setAttr(3,"fontname=\"Arial\"")
|
setAttr("width=\"0.01\"",NODE)
|
||||||
setAttr(3,"fontsize=10")
|
setAttr("margin=\"0.08,0.03\"",NODE)
|
||||||
setAttr(1,"height=\"0.01\"")
|
|
||||||
setAttr(1,"width=\"0.01\"")
|
|
||||||
setAttr(1,"margin=\"0.08,0.03\"")
|
|
||||||
#setAttr(0,"decorate=true")
|
|
||||||
|
|
||||||
def makeImage(self,attack):
|
def makeImage(self,attack):
|
||||||
""" create image for this particular attack """
|
""" create image for this particular attack """
|
||||||
|
117
gui/Gui/Settingswindow.py
Normal file
117
gui/Gui/Settingswindow.py
Normal file
@ -0,0 +1,117 @@
|
|||||||
|
#!/usr/bin/python
|
||||||
|
|
||||||
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
""" Import externals """
|
||||||
|
import wx
|
||||||
|
|
||||||
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
""" Import scyther-gui components """
|
||||||
|
import Preference
|
||||||
|
import Scyther.Claim as Claim
|
||||||
|
|
||||||
|
#---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
class SettingsWindow(wx.Panel):
|
||||||
|
|
||||||
|
def __init__(self,parent,daddy):
|
||||||
|
wx.Panel.__init__(self,parent,-1)
|
||||||
|
|
||||||
|
self.win = daddy
|
||||||
|
space = 10
|
||||||
|
grid = wx.GridBagSizer(hgap=space,vgap=space)
|
||||||
|
ypos = 0
|
||||||
|
|
||||||
|
# Bound on the number of runs
|
||||||
|
self.maxruns = int(Preference.get('maxruns','5'))
|
||||||
|
txt = wx.StaticText(self,-1,"Maximum number of runs (0 disables bound)")
|
||||||
|
ctrl = wx.SpinCtrl(self, -1, "",style=wx.RIGHT)
|
||||||
|
ctrl.SetRange(0,100)
|
||||||
|
ctrl.SetValue(self.maxruns)
|
||||||
|
self.Bind(wx.EVT_SPINCTRL,self.EvtRuns,ctrl)
|
||||||
|
grid.Add(ctrl,(ypos,0))
|
||||||
|
grid.Add(txt,(ypos,1))
|
||||||
|
ypos += 1
|
||||||
|
|
||||||
|
# Matchin options
|
||||||
|
self.match = int(Preference.get('match','0'))
|
||||||
|
claimoptions = ['typed matching','find basic type flaws','find all type flaws']
|
||||||
|
r2 = wx.StaticText(self,-1,"Matching type")
|
||||||
|
l2 = self.ch = wx.Choice(self,-1,choices=claimoptions)
|
||||||
|
l2.SetSelection(self.match)
|
||||||
|
self.Bind(wx.EVT_CHOICE,self.EvtMatch,l2)
|
||||||
|
grid.Add(l2,(ypos,0))
|
||||||
|
grid.Add(r2,(ypos,1))
|
||||||
|
ypos += 1
|
||||||
|
|
||||||
|
### MISC expert stuff
|
||||||
|
|
||||||
|
# Bound on the number of classes/attacks
|
||||||
|
self.maxattacks = int(Preference.get('maxattacks','100'))
|
||||||
|
stname = Claim.stateDescription(True,2,False)
|
||||||
|
atname = Claim.stateDescription(False,2,False)
|
||||||
|
txt = "%s/%s" % (stname,atname)
|
||||||
|
r9 = wx.StaticText(self,-1,"Maximum number of %s for all claims combined (0 disables maximum)" % txt)
|
||||||
|
l9 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT)
|
||||||
|
l9.SetRange(0,100)
|
||||||
|
l9.SetValue(self.maxattacks)
|
||||||
|
self.Bind(wx.EVT_SPINCTRL,self.EvtMaxAttacks,l9)
|
||||||
|
grid.Add(l9,(ypos,0))
|
||||||
|
grid.Add(r9,(ypos,1))
|
||||||
|
ypos += 1
|
||||||
|
|
||||||
|
self.misc = Preference.get('scytheroptions','')
|
||||||
|
r10 = wx.StaticText(self,-1,"Additional parameters for the Scyther tool")
|
||||||
|
l10 = wx.TextCtrl(self,-1,self.misc,size=(150,-1))
|
||||||
|
self.Bind(wx.EVT_TEXT,self.EvtMisc,l10)
|
||||||
|
grid.Add(l10,(ypos,0))
|
||||||
|
grid.Add(r10,(ypos,1))
|
||||||
|
ypos += 1
|
||||||
|
|
||||||
|
# Combine
|
||||||
|
self.SetSizer(grid)
|
||||||
|
self.SetAutoLayout(True)
|
||||||
|
|
||||||
|
def EvtMatch(self,evt):
|
||||||
|
self.match = evt.GetInt()
|
||||||
|
|
||||||
|
def EvtRuns(self,evt):
|
||||||
|
self.maxruns = evt.GetInt()
|
||||||
|
|
||||||
|
def EvtMaxAttacks(self,evt):
|
||||||
|
self.maxattacks = evt.GetInt()
|
||||||
|
|
||||||
|
def EvtMisc(self,evt):
|
||||||
|
self.misc = evt.GetString()
|
||||||
|
|
||||||
|
def ScytherArguments(self,mode):
|
||||||
|
""" Note: constructed strings should have a space at the end to
|
||||||
|
correctly separate the options.
|
||||||
|
"""
|
||||||
|
|
||||||
|
tstr = ""
|
||||||
|
|
||||||
|
# Number of runs
|
||||||
|
tstr += "--max-runs=%s " % (str(self.maxruns))
|
||||||
|
# Matching type
|
||||||
|
tstr += "--match=%s " % (str(self.match))
|
||||||
|
# Max attacks/classes
|
||||||
|
if self.maxattacks != 0:
|
||||||
|
tstr += "--max-attacks=%s " % (str(self.maxattacks))
|
||||||
|
|
||||||
|
# Verification type
|
||||||
|
if mode == "check":
|
||||||
|
tstr += "--check "
|
||||||
|
elif mode == "autoverify":
|
||||||
|
tstr += "--auto-claims "
|
||||||
|
elif mode == "statespace":
|
||||||
|
tstr += "--state-space "
|
||||||
|
|
||||||
|
# Anything else?
|
||||||
|
if self.misc != "":
|
||||||
|
tstr += " " + self.misc + " "
|
||||||
|
|
||||||
|
return tstr
|
||||||
|
|
||||||
|
#---------------------------------------------------------------------------
|
Loading…
Reference in New Issue
Block a user