- Started to work on a caching mechanism.

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"
+ScytherMethods	= "--match=1 --arachne"
-ScytherBounds	= "--timer=10 --max-runs=5 --max-length=20"
+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
+	outs = "***\t" + str(newattacks)
-	print "New attack [[", newattacks, "]] at", processed, "/", TupleCount, ":", claim, " using",CommandLine( protocols)
+	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
 

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)
+
+