diff --git a/test/multiprotocoltest.py b/test/multiprotocoltest.py index 442705a..f8145c9 100755 --- a/test/multiprotocoltest.py +++ b/test/multiprotocoltest.py @@ -30,7 +30,7 @@ import copy # *********************** # Tuple width (number of concurrent protocols) -TupleWidth = "3" +TupleWidth = "2" # Temporary files TempFileList = "scyther-blap.tmp" @@ -42,8 +42,8 @@ ScytherProgram = "../src/scyther" # Scyther parameters ScytherDefaults = "--summary" -ScytherMethods = "--match=0 --arachne" -ScytherBounds = "--timer=10 --max-runs=5 --max-length=20" +ScytherMethods = "--match=1 --arachne" +ScytherBounds = "--timer=5 --max-runs=5 --max-length=20" # Build a large part of the command line (for Scyther) already ScytherArgs = ScytherDefaults + " " + ScytherMethods + " " + ScytherBounds @@ -227,6 +227,30 @@ def ClearProgress (n,txt): sys.stderr.flush() +def DescribeContextBrief (filep, protocols, claim, prefix): + + filep.write (prefix) + + prlist = [] + for prfile in protocols: + prnames = GetKeys (ProtocolToFileMap, prfile) + prlist = prlist + prnames + newprname = claim.split()[0] + filep.write ("\t" + newprname) + + filep.write ("\t" + claim) + + prlistclean = [] + prliststr = "" + for pn in prlist: + if pn not in prlistclean: + if pn != newprname: + prlistclean.append(pn) + prliststr = prliststr + "\t" + pn + filep.write (prliststr) + + filep.write ("\n") + def DescribeContext (filep, protocols, claim): def DC_Claim(cl,v): if v == 0: @@ -345,15 +369,14 @@ def SignalAttack (protocols, claim): return 0 ClearProgress (TupleCount, safetxt) - print "-" * 40 - print "New attack [[", newattacks, "]] at", processed, "/", TupleCount, ":", claim, " using",CommandLine( protocols) + outs = "***\t" + str(newattacks) + outs = outs + "\t" + str(processed) + "/" + str(TupleCount) for helper in GetListKeys (ProtocolToFileMap, protocols): clprname = claim.split()[0] if helper <> clprname: if helper not in ProtocolToEffectsMap.keys(): # new ProtocolToEffectsMap[helper] = [clprname] - print "% Detected a new flaw helper:", helper else: # already noted as helper, add destruction now if clprname not in ProtocolToEffectsMap[helper]: @@ -366,7 +389,7 @@ def SignalAttack (protocols, claim): # error log thingy. Furthermore, # explicitly recreate the commandline # and the claim that is newly violated - DescribeContext (sys.stdout, protocols, claim) + DescribeContextBrief (sys.stdout, protocols, claim, outs) return 1 diff --git a/test/scythercache.py b/test/scythercache.py new file mode 100644 index 0000000..85812e0 --- /dev/null +++ b/test/scythercache.py @@ -0,0 +1,82 @@ +# +# Scyther caching mechanism +# +# Uses md5 hashes to store previously calculated results. +# +# (c)2005 Cas Cremers +# +# +import md5 +import commands +import os + +# scyther should reside in $PATH +def scythercall (argumentstring, inputfile): + clstring = "scyther " + argumentstring + " " + inputfile + (status,scout) = commands.getstatusoutput(clstring) + return (status,scout) + +# cached results +# input: a large string (consisting of read input files) +# argstring: a smaller string +def scythercache (argumentstring, inputstring): + + def cacheid(): + m = md5.new() + + # # Determine scyther version + # (status, scout) = scythercall ("--version", "") + # if status == 1 or status < 0: + # # some problem + # print "Problem with determining scyther version!" + # os.exit() + # # Add version to hash + # m.update (scout) + + # Add inputfile to hash + m.update (inputstring) + + # Add arguments to hash + m.update (argumentstring) + + # Return a readable ID (good for a filename) + return m.hexdigest() + + # Ensure directories for a file + def ensureDirectories (filename): + + def ensureDir (plist): + if len(plist) > 1: + ensureDir (plist[:-1]) + 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 + id = cacheid() + filename = "scythercache/" + id[:2] + "/res-" + id[2:] + ".txt" + cachefile = gettempdir() + "/" + filename + ensureDirectories(cachefile) + + # Does it already exist? + if os.path.exists(cachefile): + # Great: return the cached results + f = open(cachefile,"r") + res = f.read() + f.close() + return (0,res) + else: + # Hmm, we need to compute this result + h = NamedTemporaryFile() + h.write(inputstring) + (status, scout) = scythercall (argumentstring, h.name) + h.close() + f = open(cachefile,"w") + f.write(scout) + f.close() + return (status,scout) + +