summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/runTests.bat2
-rw-r--r--Test/runTests.py123
2 files changed, 68 insertions, 57 deletions
diff --git a/Test/runTests.bat b/Test/runTests.bat
index 4eeed06b..ced3bd27 100644
--- a/Test/runTests.bat
+++ b/Test/runTests.bat
@@ -1,2 +1,2 @@
@REM runTests.bat -f "/dprelude PRELUDE_FILE" -r REPORT_NAME INPUT_FILES
-C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 %*
+C:/Python34/python.exe runTests.py --flags "/useBaseNameForFileName /compile:1 /nologo" --difftool "C:/Program Files (x86)/Meld/Meld.exe" %*
diff --git a/Test/runTests.py b/Test/runTests.py
index bf4b0d9d..df233a94 100644
--- a/Test/runTests.py
+++ b/Test/runTests.py
@@ -80,7 +80,7 @@ class TestStatus(Enum):
class Test:
COLUMNS = ["name", "status", "start", "end", "duration", "returncodes", "suite_time", "njobs", "proc_info", "source_path", "temp_directory", "cmds", "expected", "output"]
- def __init__(self, name, source_path, cmds, timeout):
+ def __init__(self, name, source_path, cmds, timeout, compiler_id = 0):
self.name = name
self.source_path = source_path
self.expect_path = Test.source_to_expect_path(self.source_path)
@@ -93,6 +93,7 @@ class Test:
self.cmds = cmds
self.timeout = timeout
+ self.compiler_id = compiler_id
self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds]
self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds]
@@ -137,18 +138,17 @@ class Test:
@staticmethod
def summarize(results):
debug(None, "")
- debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results)))
+ debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results)))
if results:
- debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs))
-
grouped = defaultdict(list)
for t in results:
grouped[t.status].append(t)
for status, ts in sorted(grouped.items(), key=lambda x: x[0].index):
if ts:
- debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), ", ".join(t.name for t in ts)), headers=status)
+ debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), " ".join(t.name for t in ts)), headers=status)
+ debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs))
def run(self):
debug(Debug.DEBUG, "Starting {}".format(self.name))
@@ -198,8 +198,8 @@ class Test:
self.output = Test.read_normalize(self.temp_output_path)
self.status = TestStatus.PASSED if self.expected == self.output else TestStatus.FAILED
- def report(self, tid):
- debug(Debug.INFO, "{} ({})".format(self.name, tid), headers=self.status)
+ def report(self, tid, total):
+ debug(Debug.INFO, "[{}] [{:.2f}s] {} ({} of {})".format(self.compiler_id, self.duration, self.name, tid, total), headers=self.status)
@staticmethod
def write_bytes(base_directory, relative_path, extension, contents):
@@ -224,11 +224,11 @@ def setup_parser():
parser.add_argument('paths', type=str, action='store', nargs='+',
help='Input files or folders. Folders are searched for .dfy files.')
- parser.add_argument('--compiler', type=str, action='store', default='Dafny.exe',
- help='Command to use for %dafny.')
+ parser.add_argument('--compiler', type=str, action='append', default=[],
+ help='Dafny executable.')
- parser.add_argument('--more-flags', '-f', type=str, action='store', default='',
- help='Command used to run the tests.')
+ parser.add_argument('--flags', '-f', type=str, action='append', default=[],
+ help='Arguments to pass to dafny. Multiple --flags are concatenated.')
parser.add_argument('--njobs', '-j', action='store', type=int, default=None,
help='Number of test workers.')
@@ -248,6 +248,9 @@ def setup_parser():
parser.add_argument('--compare', action='store_true',
help="Compare two previously generated reports.")
+ parser.add_argument('--time-all', action='store_true',
+ help="When comparing, include all timings.")
+
parser.add_argument('--diff', '-d', action='store_const', const=True, default=False,
help="Don't run tests; show differences for one file.")
@@ -282,73 +285,76 @@ def run_one(test_args):
test.status = TestStatus.UNKNOWN
return test
-def read_one_test(name, fname, compiler_cmd, timeout):
- 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)
- if match:
- cmds.append(match.groups()[0].replace("%dafny", compiler_cmd))
+def read_one_test(name, 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)
+ if match:
+ cmds.append(match.groups()[0].replace("%dafny", compiler_cmd))
+ else:
+ break
+ if cmds:
+ if os.path.exists(Test.source_to_expect_path(source_path)):
+ yield Test(name, source_path, cmds, timeout, cid)
else:
- break
- if cmds:
- if os.path.exists(Test.source_to_expect_path(source_path)):
- return [Test(name, source_path, cmds, timeout)]
+ debug(Debug.DEBUG, "Test file {} has no .expect".format(fname))
else:
- debug(Debug.DEBUG, "Test file {} has no .expect".format(fname))
- else:
- debug(Debug.INFO, "Test file {} has no RUN specification".format(fname))
-
- return []
+ debug(Debug.INFO, "Test file {} has no RUN specification".format(fname))
-def find_one(name, fname, compiler_cmd, timeout):
+def find_one(name, fname, compiler_cmds, timeout):
name, ext = os.path.splitext(fname)
if ext == ".dfy":
if os.path.exists(fname):
debug(Debug.TRACE, "Found test file: {}".format(fname))
- yield from read_one_test(name, fname, compiler_cmd, timeout)
+ yield from read_one_test(name, fname, compiler_cmds, timeout)
else:
debug(Debug.ERROR, "Test file {} not found".format(fname))
else:
debug(Debug.TRACE, "Ignoring {}".format(fname))
-def find_tests(paths, compiler_cmd, excluded, timeout):
+def find_tests(paths, compiler_cmds, excluded, timeout):
for path in 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_cmd, timeout)
+ yield from find_one(fname, os.path.join(base, fname), compiler_cmds, timeout)
else:
- yield from find_one(path, path, compiler_cmd, timeout)
+ yield from find_one(path, path, compiler_cmds, timeout)
def run_tests(args):
- compiler_cmd = shlex.split(args.compiler)
- compiler_bin = compiler_cmd[0]
+ if args.compiler is []:
+ base_directory = os.path.dirname(os.path.realpath(__file__))
+ args.compiler = [os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe"))]
- if not os.path.exists(compiler_cmd[0]):
- debug(Debug.ERROR, "Compiler not found: {}".format(compiler_bin))
- return
+ for compiler in args.compiler:
+ if not os.path.exists(compiler):
+ debug(Debug.ERROR, "Compiler not found: {}".format(compiler))
+ return
- tests = list(find_tests(args.paths, args.compiler + ' ' + args.more_flags,
+ tests = list(find_tests(args.paths, [compiler + ' ' + " ".join(args.flags)
+ for compiler in args.compiler],
args.exclude + ALWAYS_EXCLUDED, args.timeout))
tests.sort(key=operator.attrgetter("name"))
args.njobs = args.njobs or os.cpu_count() or 1
- debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f} **".format(len(tests), args.njobs, args.timeout))
+ debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f}, started at {}**".format(len(tests), args.njobs, args.timeout, strftime("%H:%M:%S")))
+
try:
- pool = Pool(args.njobs) #, init_tester)
+ pool = Pool(args.njobs)
start = time()
results = []
for tid, test in enumerate(pool.imap_unordered(run_one, [(t, args) for t in tests], 1)):
- test.report(tid + 1)
+ test.report(tid + 1, len(tests))
results.append(test)
pool.close()
pool.join()
@@ -367,18 +373,22 @@ def run_tests(args):
def diff(paths, accept, difftool):
- if len(paths) > 1:
- debug(Debug.ERROR, "Please specify a single path")
- elif not os.path.exists(paths[0]):
- debug(Debug.ERROR, "Not found: {}".format(paths[0]))
- else:
- test = Test(None, paths[0], [], None)
- if accept:
- shutil.copy(test.temp_output_path, test.expect_path)
+ for path in paths:
+ if not path.endswith(".dfy"):
+ path += ".dfy"
+
+ if not os.path.exists(path):
+ debug(Debug.ERROR, "Not found: {}".format(path))
else:
- call([difftool, test.expect_path, test.temp_output_path])
+ test = Test(None, path, [], None)
+ if not accept:
+ call([difftool, test.expect_path, test.temp_output_path])
+
+ if accept or input("Accept this change? (y/N)") == "y":
+ debug(Debug.INFO, path, "Accepted")
+ shutil.copy(test.temp_output_path, test.expect_path)
-def compare_results(globs):
+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}
@@ -403,8 +413,9 @@ def compare_results(globs):
row.append(name)
row.append(ref_duration)
for path in paths[1:]:
- test_status, test_duration = resultsets[path][name]
- if test_status == ref_status:
+ res = resultsets[path].get(name)
+ test_status, test_duration = res if res else (TestStatus.UNKNOWN, None)
+ if res is not None and (test_status == ref_status or time_all):
result = "{:.2%}".format((test_duration - ref_duration) / ref_duration)
else:
result = test_status.name + "?!"
@@ -449,7 +460,7 @@ def main():
elif args.open:
os.startfile(args.paths[0])
elif args.compare:
- compare_results(args.paths)
+ compare_results(args.paths, args.time_all)
else:
run_tests(args)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 00:14:48 +0000