2005-03-03 12:36:01 +00:00
|
|
|
#!/usr/bin/python
|
2005-03-02 14:28:41 +00:00
|
|
|
#
|
2005-03-04 15:34:41 +00:00
|
|
|
# Scyther wrapper
|
2005-03-02 14:28:41 +00:00
|
|
|
#
|
2005-03-04 15:34:41 +00:00
|
|
|
# Standard tests
|
2005-03-02 14:28:41 +00:00
|
|
|
#
|
2005-03-02 15:02:34 +00:00
|
|
|
import sys
|
2005-03-03 15:25:59 +00:00
|
|
|
from optparse import OptionParser
|
2005-03-04 15:34:41 +00:00
|
|
|
from scythercache import evaluate
|
2005-03-02 14:28:41 +00:00
|
|
|
|
2005-03-03 12:36:01 +00:00
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
# Parsing Output
|
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
|
2005-03-04 14:21:49 +00:00
|
|
|
# status
|
|
|
|
def error_status(status):
|
|
|
|
if status == 1 or status < 0:
|
|
|
|
return True
|
|
|
|
else:
|
|
|
|
return False
|
|
|
|
|
2005-03-03 12:36:01 +00:00
|
|
|
# Parse output
|
|
|
|
def parse(scout):
|
|
|
|
results = {}
|
|
|
|
lines = scout.splitlines()
|
|
|
|
for line in lines:
|
|
|
|
data = line.split()
|
|
|
|
if len(data) > 6 and data[0] == 'claim':
|
|
|
|
claim = " ".join(data[1:4])
|
|
|
|
tag = data[6]
|
|
|
|
value = -1
|
|
|
|
if tag == 'failed:':
|
|
|
|
value = 0
|
|
|
|
if tag == 'correct:':
|
|
|
|
value = 1
|
|
|
|
if value == -1:
|
|
|
|
raise IOError, 'Scyther output for ' + commandline + ', line ' + line + ' cannot be parsed.'
|
|
|
|
results[claim] = value
|
|
|
|
return results
|
|
|
|
|
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
# Default tests
|
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
|
|
|
|
# Yield default protocol list (from any other one)
|
|
|
|
def default_protocols(plist):
|
2005-03-03 13:09:21 +00:00
|
|
|
plist.sort()
|
2005-03-03 12:36:01 +00:00
|
|
|
return ['../spdl/spdl-defaults.inc'] + plist
|
|
|
|
|
2005-03-03 13:09:21 +00:00
|
|
|
|
2005-03-03 12:36:01 +00:00
|
|
|
# Yield arguments, given a bound type:
|
|
|
|
# 0: fast
|
|
|
|
# 1: thorough
|
|
|
|
#
|
|
|
|
def default_arguments(plist,match,bounds):
|
|
|
|
n = len(plist)
|
|
|
|
# These bounds assume at least two protocols, otherwise
|
|
|
|
# stuff breaks.
|
|
|
|
if n < 2:
|
|
|
|
nmin = 2
|
|
|
|
else:
|
|
|
|
nmin = n
|
|
|
|
timer = 1
|
|
|
|
maxruns = 2
|
|
|
|
maxlength = 10
|
|
|
|
if bounds == 0:
|
|
|
|
timer = nmin**2
|
|
|
|
maxruns = 2*nmin
|
2005-03-04 13:40:23 +00:00
|
|
|
maxlength = 2 + maxruns * 4
|
2005-03-03 12:36:01 +00:00
|
|
|
elif bounds == 1:
|
|
|
|
timer = nmin**3
|
|
|
|
maxruns = 3*nmin
|
2005-03-04 13:40:23 +00:00
|
|
|
maxlength = 2 + maxruns * 6
|
2005-03-03 12:36:01 +00:00
|
|
|
else:
|
|
|
|
print "Don't know bounds method", bounds
|
|
|
|
sys.exit()
|
|
|
|
|
|
|
|
args = "--arachne --timer=%i --max-runs=%i --max-length=%i" % (timer, maxruns, maxlength)
|
|
|
|
matching = "--match=" + str(match)
|
|
|
|
allargs = "--summary " + matching + " " + args
|
|
|
|
return allargs
|
|
|
|
|
|
|
|
# Yield test results
|
|
|
|
def default_test(plist, match, bounds):
|
|
|
|
pl = default_protocols(plist)
|
|
|
|
args = default_arguments(plist,match,bounds)
|
|
|
|
|
|
|
|
input = ""
|
|
|
|
for fn in pl:
|
|
|
|
if len(fn) > 0:
|
|
|
|
f = open(fn, "r")
|
|
|
|
input = input + f.read()
|
|
|
|
f.close()
|
|
|
|
|
|
|
|
# Use Scyther
|
|
|
|
(status,scout) = evaluate(args,input)
|
|
|
|
return (status,scout)
|
|
|
|
|
|
|
|
# Test, check for status, yield parsed results
|
|
|
|
def default_parsed(plist, match, bounds):
|
|
|
|
(status,scout) = default_test(plist, match, bounds)
|
2005-03-04 14:21:49 +00:00
|
|
|
if error_status(status):
|
2005-03-03 12:36:01 +00:00
|
|
|
# Something went wrong
|
|
|
|
print "*** Error when checking [", plist, match, bounds, "]"
|
|
|
|
print
|
|
|
|
sys.exit()
|
|
|
|
return parse(scout)
|
|
|
|
|
2005-03-04 14:21:49 +00:00
|
|
|
# Some default options for the scyther wrapper
|
2005-03-03 15:25:59 +00:00
|
|
|
def default_options(parser):
|
|
|
|
parser.add_option("-m","--match", dest="match",
|
|
|
|
default = 0,
|
|
|
|
help = "select matching method (0: no type flaws, 2: \
|
|
|
|
full type flaws")
|
|
|
|
parser.add_option("-b","--bounds", dest="bounds",
|
|
|
|
default = 0,
|
|
|
|
help = "bound type selection (0: quickscan, 1:thorough)")
|
2005-03-03 12:36:01 +00:00
|
|
|
|
2005-03-04 14:21:49 +00:00
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
# Some default testing stuff
|
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
|
|
|
|
def all_unless_given(plist):
|
|
|
|
if plist == []:
|
|
|
|
# Get the list
|
|
|
|
import protocollist
|
|
|
|
return protocollist.from_all()
|
|
|
|
else:
|
|
|
|
return plist
|
|
|
|
|
|
|
|
# Scan for compilation errors or stuff like that
|
|
|
|
|
|
|
|
def scan_for_errors(options,args):
|
|
|
|
# Select specific list
|
|
|
|
plist = all_unless_given(args)
|
|
|
|
# Now check all things in the list
|
|
|
|
errorcount = 0
|
|
|
|
for p in plist:
|
|
|
|
# Test and gather output
|
|
|
|
(status,scout) = default_test([p], 0, 0)
|
|
|
|
error = False
|
|
|
|
if error_status(status):
|
|
|
|
error = True
|
|
|
|
else:
|
|
|
|
if scout.rfind("ERROR") != -1:
|
|
|
|
error = True
|
|
|
|
if scout.rfind("error") != -1:
|
|
|
|
error = True
|
|
|
|
if error:
|
|
|
|
print "There is an error in the output for", p
|
|
|
|
errorcount = errorcount + 1
|
|
|
|
|
|
|
|
if errorcount > 0:
|
|
|
|
print
|
|
|
|
print "Scan complete. Found", errorcount, "error(s) in", len(plist), "files."
|
|
|
|
|
|
|
|
# Scan for timeout protocols
|
|
|
|
#
|
|
|
|
# The idea is that some things will generate a timeout, and we would like
|
|
|
|
# to know which ones. However, this can just be a problem of the time
|
|
|
|
# limit, and might not be caused by a loop at all. Therefore, some
|
|
|
|
# scanning is needed.
|
|
|
|
|
|
|
|
def scan_for_timeouts(options,args):
|
|
|
|
|
|
|
|
def parse_timeout(status,scout):
|
|
|
|
if not error_status(status):
|
|
|
|
if scout.rfind("time=") != -1:
|
|
|
|
return True
|
|
|
|
return False
|
|
|
|
|
|
|
|
def check_for_timeout(p):
|
|
|
|
# First a simple test
|
|
|
|
(status,scout) = default_test([p], 0, 1)
|
|
|
|
if not parse_timeout(status,scout):
|
|
|
|
# Well if there is no timeout here...
|
|
|
|
return False
|
|
|
|
|
|
|
|
# More testing...
|
|
|
|
|
|
|
|
return True
|
|
|
|
|
|
|
|
# Select specific list
|
|
|
|
plist = all_unless_given(args)
|
|
|
|
# Now check all things in the list
|
|
|
|
errorcount = 0
|
|
|
|
for p in plist:
|
|
|
|
# Test and gather output
|
|
|
|
if check_for_timeout(p):
|
|
|
|
print "There is a timeout for", p
|
|
|
|
errorcount = errorcount + 1
|
|
|
|
|
|
|
|
if errorcount > 0:
|
|
|
|
print
|
|
|
|
print "Scan complete. Found", errorcount, "timeout(s) in", len(plist), "files."
|
2005-03-02 14:28:41 +00:00
|
|
|
|
2005-03-03 15:25:59 +00:00
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
# Standalone usage
|
|
|
|
#----------------------------------------------------------------------------
|
|
|
|
|
|
|
|
def main():
|
|
|
|
parser = OptionParser()
|
|
|
|
default_options(parser)
|
|
|
|
parser.add_option("-e","--errors", dest="errors",
|
|
|
|
default = "False",
|
|
|
|
action = "store_true",
|
|
|
|
help = "detect compilation errors for all protocols [in list_all]")
|
2005-03-04 14:21:49 +00:00
|
|
|
parser.add_option("-t","--timeouts", dest="timeouts",
|
|
|
|
default = "False",
|
|
|
|
action = "store_true",
|
|
|
|
help = "scan for timeout errors for all protocols [in list_all]")
|
2005-03-03 15:25:59 +00:00
|
|
|
(options, args) = parser.parse_args()
|
|
|
|
|
|
|
|
# Subcases
|
|
|
|
if options.errors != "False":
|
2005-03-04 14:21:49 +00:00
|
|
|
scan_for_errors(options,args)
|
|
|
|
elif options.timeouts != "False":
|
|
|
|
scan_for_timeouts(options,args)
|
2005-03-03 15:25:59 +00:00
|
|
|
else:
|
|
|
|
# Not any other switch: just test the list then
|
|
|
|
if args == []:
|
|
|
|
print "Scyther default test needs at least one input file."
|
|
|
|
sys.exit()
|
|
|
|
(status,scout) = default_test(args, options.match, options.bounds)
|
|
|
|
print "Status:", status
|
|
|
|
print scout
|
|
|
|
|
|
|
|
# Only if main stuff
|
|
|
|
if __name__ == '__main__':
|
|
|
|
main()
|