From 65334f8f33c92a1e37376d6484d60ee45b55ca1d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 15:11:03 -0700 Subject: Add tests for the server --- Test/runTests.py | 89 ++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 55 insertions(+), 34 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index fc9c20e7..ebdb0655 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -38,6 +38,7 @@ class Defaults: DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:300"] + EXTENSIONS = [".dfy", ".transcript"] class Colors: RED = '\033[91m' @@ -103,7 +104,6 @@ class Test: def __init__(self, name, source_path, cmds, timeout, compiler_id = 0): self.name = name - self.dfy = None if self.name is None else (self.name + ".dfy") self.source_path = Test.uncygdrive(source_path) self.expect_path = Test.source_to_expect_path(self.source_path) self.source_directory, self.fname = os.path.split(self.source_path) @@ -182,7 +182,7 @@ class Test: debug(Debug.REPORT, "{} of {}".format(len(tests), len(results)), headers=status) if status != TestStatus.PASSED: for test in tests: - debug(Debug.REPORT, "* " + test.dfy, headers=status, silentheaders=True) + debug(Debug.REPORT, "* " + test.name, headers=status, silentheaders=True) debug(Debug.REPORT) @@ -190,14 +190,14 @@ class Test: if failing: with open("failing.lst", mode='w') as writer: for t in failing: - writer.write("{}\t{}\n".format(t.name, t.source_path)) + writer.write("{}\n".format(t.name)) debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests") debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) def run(self): - debug(Debug.DEBUG, "Starting {}".format(self.dfy)) + debug(Debug.DEBUG, "Starting {}".format(self.name)) os.makedirs(self.temp_directory, exist_ok=True) # os.chdir(self.source_directory) @@ -227,7 +227,7 @@ class Test: stdout, stderr = stdout.strip(), stderr.strip() if stdout != b"" or stderr != b"": - debug(Debug.TRACE, "Writing the output of {} to {}".format(self.dfy, self.temp_output_path)) + debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) with open(self.temp_output_path, mode='ab') as writer: writer.write(stdout + stderr) if stderr != b"": @@ -249,7 +249,7 @@ class Test: fstring = "[{:5.2f}s] {} ({}{})" progress = "{}/{}".format(tid, len(alltests)) - message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), + message = fstring.format(self.duration, wrap_color(self.name, Colors.BRIGHT), wrap_color(progress, Colors.BRIGHT), running) debug(Debug.INFO, message, headers=self.status) @@ -275,7 +275,7 @@ def setup_parser(): parser = argparse.ArgumentParser(description='Run the Dafny test suite.') parser.add_argument('path', type=str, action='store', nargs='+', - help='Input files or folders. Folders are searched for .dfy files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') + help='Input files or folders. Folders are searched for test files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') parser.add_argument('--compiler', type=str, action='append', default=None, help='Dafny executable. Default: {}'.format(Defaults.DAFNY_BIN)) @@ -293,11 +293,14 @@ def setup_parser(): help='Excluded directories. {} are automatically added.'.format(Defaults.ALWAYS_EXCLUDED)) parser.add_argument('--verbosity', action='store', type=int, default=1, - help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') + help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info; 3: Trace.') parser.add_argument('-v', action='store_const', default=1, dest="verbosity", const=2, help='Short for --verbosity 2.') + parser.add_argument('-vv', action='store_const', default=1, dest="verbosity", const=3, + help='Short for --verbosity 3.') + parser.add_argument('--report', '-r', action='store', type=str, default=None, help='Give an explicit name to the report file. Defaults to the current date and time.') @@ -339,7 +342,7 @@ def run_one_internal(test, test_id, args, running): # ignore further work once you receive a kill signal KILLED = True except Exception as e: - debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) + debug(Debug.ERROR, "[{}] {}".format(test.name, e)) test.status = TestStatus.UNKNOWN finally: running.remove(test_id) @@ -349,53 +352,71 @@ def run_one_internal(test, test_id, args, running): def run_one(args): return run_one_internal(*args) -def read_one_test(name, fname, compiler_cmds, timeout): +def get_server_path(compiler): + REGEXP = r"\bDafny.exe\b.*" + if re.search(REGEXP, compiler): + return re.sub(REGEXP, "DafnyServer.exe", compiler) + else: + return None + +def substitute_binaries(cmd, compiler): + cmd = cmd.replace("%dafny", compiler) + cmd = cmd.replace("%server", get_server_path(compiler)) + return cmd + +def read_one_test(fname, compiler_cmds, timeout): for cid, compiler_cmd in enumerate(compiler_cmds): source_path = os.path.realpath(fname) with open(source_path, mode='r') as reader: cmds = [] for line in reader: line = line.strip() - match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) + match = re.match("^[/# ]*RUN: *(?!%diff)([^ ].*)$", line) if match: - cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) + debug(Debug.TRACE, "Found RUN spec: {}".format(line)) + cmds.append(substitute_binaries(match.groups()[0], compiler_cmd)) else: break if cmds: - yield Test(name, source_path, cmds, timeout, cid) + yield Test(fname, source_path, cmds, timeout, cid) else: - debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) + debug(Debug.WARNING, "Test file {} has no RUN specification".format(fname)) -def find_one(name, fname, compiler_cmds, timeout, allow_lst=False): - name, ext = os.path.splitext(fname) - if ext == ".dfy": +def find_one(fname, compiler_cmds, timeout): + _, ext = os.path.splitext(fname) + if ext in Defaults.EXTENSIONS: if os.path.exists(fname): debug(Debug.TRACE, "Found test file: {}".format(fname)) - yield from read_one_test(name, fname, compiler_cmds, timeout) + yield from read_one_test(fname, compiler_cmds, timeout) else: debug(Debug.ERROR, "Test file {} not found".format(fname)) - elif ext == ".lst" and allow_lst: #lst files are only read if explicitly listed on the CLI - debug(Debug.INFO, "Loading tests from {}".format(fname)) - with open(fname) as reader: - for line in reader: - _name, _path = line.strip().split() - yield from find_one(_name, _path, compiler_cmds, timeout) else: debug(Debug.TRACE, "Ignoring {}".format(fname)) -def find_tests(paths, compiler_cmds, excluded, timeout): +def expand_lsts(paths): for path in paths: + _, ext = os.path.splitext(path) + if ext == ".lst": #lst files are only read if explicitly listed on the CLI + debug(Debug.INFO, "Loading tests from {}".format(path)) + with open(path) as reader: + for line in reader: + _path = line.strip() + yield _path + else: + yield path + +def find_tests(paths, compiler_cmds, excluded, timeout): + for path in expand_lsts(paths): if os.path.isdir(path): debug(Debug.TRACE, "Searching for tests in {}".format(path)) for base, dirnames, fnames in os.walk(path): dirnames[:] = [d for d in dirnames if d not in excluded] for fname in fnames: - yield from find_one(fname, os.path.join(base, fname), compiler_cmds, timeout) + yield from find_one(os.path.join(base, fname), compiler_cmds, timeout) else: - yield from find_one(path, path, compiler_cmds, timeout, True) - + yield from find_one(path, compiler_cmds, timeout) def run_tests(args): if args.compiler is None: @@ -404,12 +425,15 @@ def run_tests(args): args.base_flags = Defaults.FLAGS for compiler in args.compiler: + server = get_server_path(compiler) if not os.path.exists(compiler): debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) return + if not os.path.exists(server): + debug(Debug.WARNING, "Server not found") tests = list(find_tests(args.path, [compiler + ' ' + " ".join(args.base_flags + args.flags) - for compiler in args.compiler], + for compiler in args.compiler], args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) @@ -447,10 +471,7 @@ def run_tests(args): def diff(paths, accept, difftool): - for path in paths: - if not path.endswith(".dfy"): - path += ".dfy" - + for path in expand_lsts(paths): if not os.path.exists(path): debug(Debug.ERROR, "Not found: {}".format(path)) else: @@ -470,7 +491,7 @@ def compare_results(globs, time_all): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} - resultsets = {path: {test.dfy: (test.status, test.duration) for test in report} + resultsets = {path: {test.name: (test.status, test.duration) for test in report} for path, report in reports.items()} all_tests = set(name for resultset in resultsets.values() for name in resultset.keys()) -- cgit v1.2.3