merge

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)