- First integration steps, untested.
This commit is contained in:
parent
9533f6f548
commit
6e77e7cf93
@ -24,6 +24,8 @@
|
|||||||
|
|
||||||
import tuplesdo
|
import tuplesdo
|
||||||
import copy
|
import copy
|
||||||
|
import scythercache
|
||||||
|
from tempfile import NamedTemporaryFile
|
||||||
|
|
||||||
# ***********************
|
# ***********************
|
||||||
# PARAMETERS
|
# PARAMETERS
|
||||||
@ -38,7 +40,6 @@ TempFileTuples = "scyther-blip.tmp"
|
|||||||
|
|
||||||
# External programs
|
# External programs
|
||||||
TupleProgram = "./tuples.py"
|
TupleProgram = "./tuples.py"
|
||||||
ScytherProgram = "../src/scyther"
|
|
||||||
|
|
||||||
# Scyther parameters
|
# Scyther parameters
|
||||||
ScytherDefaults = "--summary"
|
ScytherDefaults = "--summary"
|
||||||
@ -47,7 +48,7 @@ ScytherBounds = "--timer=5 --max-runs=5 --max-length=20"
|
|||||||
|
|
||||||
# Build a large part of the command line (for Scyther) already
|
# Build a large part of the command line (for Scyther) already
|
||||||
ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds
|
ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds
|
||||||
CommandPrefix = ScytherProgram + " " + ScytherArgs
|
CommandPrefix = "scyther "
|
||||||
|
|
||||||
# Some default settings for Agents, untrusted e with sk(e) and k(a,e) etc.
|
# Some default settings for Agents, untrusted e with sk(e) and k(a,e) etc.
|
||||||
IncludeProtocols = '../spdl/spdl-defaults.inc'
|
IncludeProtocols = '../spdl/spdl-defaults.inc'
|
||||||
@ -132,8 +133,15 @@ def ScytherEval (plist):
|
|||||||
sys.stdout.flush()
|
sys.stdout.flush()
|
||||||
sys.stderr.flush()
|
sys.stderr.flush()
|
||||||
|
|
||||||
|
# Combine protocol list to an input
|
||||||
|
input = ""
|
||||||
|
for fn in plist:
|
||||||
|
f = open(fn, "r")
|
||||||
|
input = input + f.read()
|
||||||
|
f.close()
|
||||||
|
|
||||||
# Use Scyther
|
# Use Scyther
|
||||||
(status,scout) = commands.getstatusoutput(CommandLine (plist))
|
(status,scout) = scythercache.eval(ScytherArgs,input)
|
||||||
|
|
||||||
if status == 1 or status < 0:
|
if status == 1 or status < 0:
|
||||||
# Something went wrong
|
# Something went wrong
|
||||||
|
@ -9,6 +9,8 @@
|
|||||||
import md5
|
import md5
|
||||||
import commands
|
import commands
|
||||||
import os
|
import os
|
||||||
|
import sys
|
||||||
|
from tempfile import NamedTemporaryFile, gettempdir
|
||||||
|
|
||||||
# scyther should reside in $PATH
|
# scyther should reside in $PATH
|
||||||
def scythercall (argumentstring, inputfile):
|
def scythercall (argumentstring, inputfile):
|
||||||
@ -19,7 +21,7 @@ def scythercall (argumentstring, inputfile):
|
|||||||
# cached results
|
# cached results
|
||||||
# input: a large string (consisting of read input files)
|
# input: a large string (consisting of read input files)
|
||||||
# argstring: a smaller string
|
# argstring: a smaller string
|
||||||
def scythercache (argumentstring, inputstring):
|
def eval (argumentstring, inputstring):
|
||||||
|
|
||||||
def cacheid():
|
def cacheid():
|
||||||
m = md5.new()
|
m = md5.new()
|
||||||
@ -42,29 +44,28 @@ def scythercache (argumentstring, inputstring):
|
|||||||
# Return a readable ID (good for a filename)
|
# Return a readable ID (good for a filename)
|
||||||
return m.hexdigest()
|
return m.hexdigest()
|
||||||
|
|
||||||
|
# Ensure directory
|
||||||
|
def ensureDirectory (path):
|
||||||
|
if not os.path.exists(path):
|
||||||
|
os.mkdir(path)
|
||||||
|
|
||||||
# Ensure directories for a file
|
# Ensure directories for a file
|
||||||
def ensureDirectories (filename):
|
def ensureDirectories (filename):
|
||||||
|
for i in range(1,len(filename)):
|
||||||
def ensureDir (plist):
|
if filename[i] == '/':
|
||||||
if len(plist) > 1:
|
np = i+1
|
||||||
ensureDir (plist[:-1])
|
ensureDirectory(filename[:np])
|
||||||
path = plist.join("/")
|
|
||||||
if not os.path.exists(path):
|
|
||||||
os.mkdir(path)
|
|
||||||
|
|
||||||
dir = os.path.dirname(filename)
|
|
||||||
ensuredir (dir.split("/"))
|
|
||||||
|
|
||||||
# Determine the unique filename for this test
|
# Determine the unique filename for this test
|
||||||
id = cacheid()
|
id = cacheid()
|
||||||
filename = "scythercache/" + id[:2] + "/res-" + id[2:] + ".txt"
|
filename = "scyther/cache-" + id[:3] + "/res-" + id[3:] + ".txt"
|
||||||
cachefile = gettempdir() + "/" + filename
|
cachefile = gettempdir() + "/" + filename
|
||||||
ensureDirectories(cachefile)
|
ensureDirectories(cachefile)
|
||||||
|
|
||||||
# Does it already exist?
|
# Does it already exist?
|
||||||
if os.path.exists(cachefile):
|
if os.path.exists(cachefile):
|
||||||
# Great: return the cached results
|
# Great: return the cached results
|
||||||
f = open(cachefile,"r")
|
f = open(cachefile,'r')
|
||||||
res = f.read()
|
res = f.read()
|
||||||
f.close()
|
f.close()
|
||||||
return (0,res)
|
return (0,res)
|
||||||
@ -72,11 +73,20 @@ def scythercache (argumentstring, inputstring):
|
|||||||
# Hmm, we need to compute this result
|
# Hmm, we need to compute this result
|
||||||
h = NamedTemporaryFile()
|
h = NamedTemporaryFile()
|
||||||
h.write(inputstring)
|
h.write(inputstring)
|
||||||
|
h.flush()
|
||||||
(status, scout) = scythercall (argumentstring, h.name)
|
(status, scout) = scythercall (argumentstring, h.name)
|
||||||
h.close()
|
h.close()
|
||||||
f = open(cachefile,"w")
|
if not(status <= 0 or status == 1):
|
||||||
f.write(scout)
|
# All is well
|
||||||
f.close()
|
f = open(cachefile,'w')
|
||||||
|
f.write(scout)
|
||||||
|
f.close()
|
||||||
|
else:
|
||||||
|
print status
|
||||||
|
print scout
|
||||||
|
print h.name
|
||||||
|
|
||||||
|
sys.exit()
|
||||||
return (status,scout)
|
return (status,scout)
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user