diff --git a/test/compareheuristics.py b/test/compareheuristics.py new file mode 100755 index 0000000..c332149 --- /dev/null +++ b/test/compareheuristics.py @@ -0,0 +1,72 @@ +#!/usr/bin/python +# +# Compare heuristics +# +import sys +from optparse import OptionParser + +import scythertest + +# Parse +def parse(scout): + ra = 0 + rb = 0 + rp = 0 + nc = 0 + for l in scout.splitlines(): + data = l.split() + if len(data) > 6 and data[0] == 'claim': + nc = nc + 1 + tag = data[6] + if tag == 'failed:': + ra = ra + 1 + if tag == 'correct:': + if l.rfind("complete_proof") != -1: + rp = rp + 1 + else: + rb = rb + 1 + return (ra,rb,rp,nc) + + +# Test with a goal selector +def test_goal_selector(goalselector): + import protocollist + + scythertest.set_extra_parameters("--goal-select=" + str(goalselector)) + result = str(goalselector) + plist = protocollist.from_literature() + np = len(plist) + + attacks = 0 + bounds = 0 + proofs = 0 + claims = 0 + for p in plist: + (status,scout) = scythertest.default_test([p],0,0) + (ra,rb,rp,nc) = parse(scout) + attacks = attacks + ra + bounds = bounds + rb + proofs = proofs + rp + claims = claims + nc + + return (attacks,bounds,proofs,claims,np) + + +# Main code +def main(): + parser = OptionParser() + scythertest.default_options(parser) + (options, args) = parser.parse_args() + scythertest.process_default_options(options) + + print "G-sel\tAttack\tBound\tProof" + print + for g in range(1,31): + (ra,rb,rp,nc,np) = test_goal_selector(g) + print str(g) + "\t" + str(ra) + "\t" + str(rb) + "\t" + str(rp) + "\t" + str(nc) + print + print "Goal selector scan completed." + +# Only if main stuff +if __name__ == '__main__': + main() diff --git a/test/multiprotocoltest.py b/test/multiprotocoltest.py index 6f1abef..dff528c 100755 --- a/test/multiprotocoltest.py +++ b/test/multiprotocoltest.py @@ -537,6 +537,7 @@ def main(): help = "suppress a progress bar") (options, args) = parser.parse_args() + scythertest.process_default_options(options) the_great_houdini(args, int(options.tuplewidth), int(options.match)) diff --git a/test/scythercache.py b/test/scythercache.py index 0abd713..571a85e 100755 --- a/test/scythercache.py +++ b/test/scythercache.py @@ -21,6 +21,19 @@ from tempfile import NamedTemporaryFile, gettempdir # Minimum duration for a test to get into the cache (in seconds) CacheTimer = 0.1 +ScytherProgram = "scyther" + +#---------------------------------------------------------------------------- +# How to override Scyther program setting +#---------------------------------------------------------------------------- + +def scytheroverride (newprg): + global ScytherProgram + + ScytherProgram = newprg + if not os.path.exists(ScytherProgram): + print "Cannot find any file at", ScytherProgram, " and it cannot be used as a Scyther executable." + sys.exit() #---------------------------------------------------------------------------- # How to call Scyther @@ -28,7 +41,9 @@ CacheTimer = 0.1 # scyther should reside in $PATH def scythercall (argumentstring, inputfile): - clstring = "scyther " + argumentstring + " " + inputfile + global ScytherProgram + + clstring = ScytherProgram + " " + argumentstring + " " + inputfile (status,scout) = commands.getstatusoutput(clstring) return (status,scout) diff --git a/test/scythertest.py b/test/scythertest.py index 1c37eb6..58c950a 100755 --- a/test/scythertest.py +++ b/test/scythertest.py @@ -6,7 +6,13 @@ # import sys from optparse import OptionParser -from scythercache import evaluate +from scythercache import evaluate, scytheroverride + + +#---------------------------------------------------------------------------- +# Globals +#---------------------------------------------------------------------------- +g_extra = "" #---------------------------------------------------------------------------- # Parsing Output @@ -47,6 +53,26 @@ def default_protocols(plist): plist.sort() return ['../spdl/spdl-defaults.inc'] + plist +# Get the extra parameters +def get_extra_parameters(): + global g_extra + + return g_extra + +# Set the extra parameters +def set_extra_parameters(args): + global g_extra + + g_extra = args + +# Add the extra parameters +def add_extra_parameters(args): + global g_extra + + if args != "": + if g_extra != "": + g_extra = g_extra + " " + g_extra = g_extra + args # Yield arguments, given a bound type: # 0: fast @@ -78,6 +104,10 @@ def default_arguments(plist,match,bounds): args = "--arachne --timer=%i --max-runs=%i --max-length=%i" % (timer, maxruns, maxlength) matching = "--match=" + str(match) allargs = "--summary " + matching + " " + args + + extra = get_extra_parameters() + if extra != "": + allargs = extra + " " + allargs return allargs # Yield test results @@ -115,6 +145,23 @@ def default_options(parser): parser.add_option("-b","--bounds", dest="bounds", default = 0, help = "bound type selection (0: quickscan, 1:thorough)") + parser.add_option("-x","--extra", dest="extra", + default = "", + help = "add arguments to pass to Scyther") + parser.add_option("-P","--program", dest="program", + default = "", + help = "define alternative scyther executable") + +# Process the default options +def process_default_options(options): + if options.program != "": + scytheroverride(options.program) + print "Using", options.program, "as Scyther executable." + if options.extra != "": + add_extra_parameters(options.extra) + print "Added extra options, now:", get_extra_parameters(options.extra) + + #---------------------------------------------------------------------------- # Some default testing stuff @@ -130,6 +177,18 @@ def all_unless_given(plist): # Scan for compilation errors or stuff like that +def scan_for_results(options,args): + # Select specific list + plist = all_unless_given(args) + # Now check all things in the list + for p in plist: + # Test and gather output + (status,scout) = default_test([p], 0, 0) + print scout + + print + print "Scan complete." + def scan_for_errors(options,args): # Select specific list plist = all_unless_given(args) @@ -205,15 +264,24 @@ def main(): default = "False", action = "store_true", help = "detect compilation errors for all protocols [in list_all]") + parser.add_option("-r","--results", dest="results", + default = "False", + action = "store_true", + help = "scan for results for all protocols [in list_all]") parser.add_option("-t","--timeouts", dest="timeouts", default = "False", action = "store_true", help = "scan for timeout errors for all protocols [in list_all]") (options, args) = parser.parse_args() + # Globals + process_default_options(options) + # Subcases if options.errors != "False": scan_for_errors(options,args) + elif options.results != "False": + scan_for_results(options,args) elif options.timeouts != "False": scan_for_timeouts(options,args) else: