Replace `new-smt-backend` tag with inverted `no-new-smt` tag #8002

thomasspriggs · 2023-11-07T20:14:32Z

This makes it somewhat more straight forward to find tests where the new smt backend is not currently run. It also helps with testing with the new smt support on new tests by default.

The tags in the .desc files are flipped using a one-off python script. I am including it here below rather than in a separate commit as it is intended for a singular usage and it may be more straight forward to review the script than the .desc file updates.

import os
import sys
from pathlib import Path

def usage():
    print("Usage " + sys.argv[0] + " [directory]")
    print("Processes all test tags within a [directory].")

def update_file(file_path) -> bool:
    with file_path.open("rt") as file:
        lines = file.readlines()
    if len(lines) == 0:
        print("File " + file_path + " is empty")
        return False
    if "CORE" not in lines[0]:
        return False
    if " new-smt-backend" not in lines[0] and " no-new-smt" not in lines[0]:
        lines[0] = lines[0].replace("\n", " no-new-smt\n")
    else:
        lines[0] = lines[0].replace(" new-smt-backend", "")
    with file_path.open("wt") as file:
        file.writelines(lines)
    return True

def main() -> int:
    if len(sys.argv) != 2:
        usage()
        return os.EX_USAGE
    directory = Path(sys.argv[1])
    if not directory.is_absolute():
        directory = Path(os.getcwd()) / directory
    print("Running against directory " + os.fspath(directory))
    if not directory.is_dir():
        print("Error - This is not a directory.")
        return os.EX_IOERR
    files = directory.glob("*/*.desc")
    tests_updated = 0
    for file_path in files:
        if not file_path.is_file():
            print(os.fspath(file_path) + " was expected to be a file but is "
                                         "not a file")
            continue
        if update_file(file_path):
            tests_updated += 1
    if tests_updated == 0:
        print("Error - No tests updated")
        return os.EX_NOTFOUND
    print(str(tests_updated) + " tests updated.")
    return os.EX_OK

if __name__ == '__main__':
    sys.exit(main())

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2023-11-07T20:44:07Z

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (cb62568) 78.80% compared to head (4590da1) 79.09%.
Report is 20 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8002      +/-   ##
===========================================
+ Coverage    78.80%   79.09%   +0.29%     
===========================================
  Files         1701     1699       -2     
  Lines       196462   196508      +46     
===========================================
+ Hits        154819   155433     +614     
+ Misses       41643    41075     -568

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

TGWDB

This causes my browser to grind to a sluggish crawl so I only checked the first 35% or so. I think the make and cmake files need to be checked and corrected in a few places (at least regarding comments).

TGWDB · 2023-11-07T23:19:05Z

regression/book-examples/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
    "CORE"
 )

-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-I` (include flag) is passed, test.pl will exclude the tests matching the label following it.


Comment is now wrong.

Fixed. The explanation in the comment is now updated in all 3 places.

TGWDB · 2023-11-07T23:19:38Z

regression/cbmc-primitives/CMakeLists.txt

@@ -5,11 +5,11 @@ if(Z3_EXISTS)
        "$<TARGET_FILE:cbmc>"
    )

-    # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+    # If `-X` (include flag) is passed, test.pl will exclude the tests matching the label following it.


Comment is wrong

I have fixed the text in the brackets.

TGWDB · 2023-11-07T23:21:17Z

regression/cbmc-primitives/CMakeLists.txt

    add_test_pl_profile(
            "cbmc-primitives-new-smt-backend"
            "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-            "-I;new-smt-backend;-s;new-smt-backend"
+            "-X;no-new-smt;-s;new-smt-backend"


This looks off, but I don't recall the exact syntax here.

I'm not convinced there is anything wrong here? We want to flip to selectively excluding rather than selectively including tests.

I clearly was not really clear. The change from -I to -X is correct, but there remains the -s;new-smt-backend which looks off to me. That said, I don't recall the syntax (and should check).

I guess that's ok for it's an arbitrary string to disambiguate log files:

$ regression/test.pl --help [...] -s <suffix> append <suffix> to all output and log files. Enables concurrent testing of the same desc file with different commands or options, as runs with different suffixes will operate independently and keep independent logs. [...]

As per the previous comment the -s disambiguates log files. So updating it to contain "no" for example would seem incorrect/misleading. It would match the tag but appear in the file name of output files where the "no" tag is not present. @TGWDB Ok if I consider this comment to be resolved?

TGWDB · 2023-11-07T23:22:47Z

regression/cbmc/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
    "CORE"
 )

-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-X` (include flag) is passed, test.pl will exclude the tests matching the label following it.


Comment is wrong

I have fixed the text in the brackets.

TGWDB · 2023-11-07T23:23:32Z

regression/cbmc/CMakeLists.txt

 add_test_pl_profile(
  "cbmc-new-smt-backend"
  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
+  "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"


Check this?

Same here: I think this is ok?!

See previous comments on the -s flag.

tautschnig

Thank you for implementing this change! I have reviewed the changes locally to circumvent the problems that @TGWDB mentioned. Happy with the changes other than what @TGWDB mentioned.

tautschnig · 2023-11-08T12:33:15Z

regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

@@ -1,4 +1,4 @@
-CORE  new-smt-backend


Nit pick (here and elsewhere): for some reason there are two spaces here, and the (automated) changes leave one of them behind, meaning there is a space at the end of the line.

esteffin

LGTM, when the requested changes are merged

This makes it somewhat more straight forward to find tests where the new smt backend is not currently run. It also helps with testing with the new smt support on new tests by default. The tags in the `.desc` files are flipped using a one-off python script. I am including it here below in the commit message body rather than in a separate commit as it is intended for a singular usage and it may be more straight forward to review the script than the `.desc` file updates. ``` import os import sys from pathlib import Path def usage(): print("Usage " + sys.argv[0] + " [directory]") print("Processes all test tags within a [directory].") def update_file(file_path) -> bool: with file_path.open("rt") as file: lines = file.readlines() if len(lines) == 0: print("File " + file_path + " is empty") return False if "CORE" not in lines[0]: return False if " new-smt-backend" not in lines[0] and " no-new-smt" not in lines[0]: lines[0] = lines[0].replace("\n", " no-new-smt\n") else: lines[0] = lines[0].replace(" new-smt-backend", "") with file_path.open("wt") as file: file.writelines(lines) return True def main() -> int: if len(sys.argv) != 2: usage() return os.EX_USAGE directory = Path(sys.argv[1]) if not directory.is_absolute(): directory = Path(os.getcwd()) / directory print("Running against directory " + os.fspath(directory)) if not directory.is_dir(): print("Error - This is not a directory.") return os.EX_IOERR files = directory.glob("*/*.desc") tests_updated = 0 for file_path in files: if not file_path.is_file(): print(os.fspath(file_path) + " was expected to be a file but is " "not a file") continue if update_file(file_path): tests_updated += 1 if tests_updated == 0: print("Error - No tests updated") return os.EX_NOTFOUND print(str(tests_updated) + " tests updated.") return os.EX_OK if __name__ == '__main__': sys.exit(main()) ```

In order to make the tags in the previous commit work as expected.

thomasspriggs · 2023-11-14T11:19:47Z

@TGWDB I have addressed your comments and separated the PR into 2 commits for ease of review. All commits will still have all tests pass. The first commit will cause the smt tests not to run and the second will re-instate them.

I think these were introduced in the preceding commit due to trailing spaces on end of lines before this PR. Python script for the update - ``` import os import sys from pathlib import Path def usage(): print("Usage " + sys.argv[0] + " [directory]") print("Processes all test tags within a [directory].") def update_file(file_path) -> bool: with file_path.open("rt") as file: lines = file.readlines() if len(lines) == 0: print("File " + file_path + " is empty") return False if " " not in lines[0]: return False lines[0] = lines[0].replace(" ", " ") with file_path.open("wt") as file: file.writelines(lines) return True def main() -> int: if len(sys.argv) != 2: usage() return os.EX_USAGE directory = Path(sys.argv[1]) if not directory.is_absolute(): directory = Path(os.getcwd()) / directory print("Running against directory " + os.fspath(directory)) if not directory.is_dir(): print("Error - This is not a directory.") return os.EX_IOERR files = directory.glob("*/*.desc") tests_updated = 0 for file_path in files: if not file_path.is_file(): print(os.fspath(file_path) + " was expected to be a file " "but is not a file") continue if update_file(file_path): tests_updated += 1 if tests_updated == 0: print("Error - No tests updated") return os.EX_NOTFOUND print(str(tests_updated) + " tests updated.") return os.EX_OK if __name__ == '__main__': sys.exit(main()) ```

TGWDB reviewed Nov 7, 2023

View reviewed changes

tautschnig approved these changes Nov 8, 2023

View reviewed changes

esteffin approved these changes Nov 9, 2023

View reviewed changes

thomasspriggs added 2 commits November 14, 2023 11:07

Update test runner replace new-smt-backend with no-new-smt

4452558

In order to make the tags in the previous commit work as expected.

thomasspriggs force-pushed the tas/smt-test-flip branch from 22102cc to 4452558 Compare November 14, 2023 11:12

TGWDB approved these changes Nov 14, 2023

View reviewed changes

thomasspriggs merged commit 03f93ef into diffblue:develop Nov 14, 2023

thomasspriggs deleted the tas/smt-test-flip branch November 14, 2023 13:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replace `new-smt-backend` tag with inverted `no-new-smt` tag #8002

Replace `new-smt-backend` tag with inverted `no-new-smt` tag #8002

thomasspriggs commented Nov 7, 2023 •

edited

Loading

codecov bot commented Nov 7, 2023 •

edited

Loading

TGWDB left a comment

TGWDB Nov 7, 2023

thomasspriggs Nov 14, 2023

TGWDB Nov 7, 2023

thomasspriggs Nov 14, 2023

TGWDB Nov 7, 2023

tautschnig Nov 8, 2023

TGWDB Nov 8, 2023

tautschnig Nov 8, 2023

thomasspriggs Nov 14, 2023

TGWDB Nov 7, 2023

thomasspriggs Nov 14, 2023

TGWDB Nov 7, 2023

tautschnig Nov 8, 2023

thomasspriggs Nov 14, 2023

tautschnig left a comment

tautschnig Nov 8, 2023

esteffin left a comment

thomasspriggs commented Nov 14, 2023

Replace new-smt-backend tag with inverted no-new-smt tag #8002

Replace new-smt-backend tag with inverted no-new-smt tag #8002

Conversation

thomasspriggs commented Nov 7, 2023 • edited Loading

codecov bot commented Nov 7, 2023 • edited Loading

Codecov Report

TGWDB left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

esteffin left a comment

Choose a reason for hiding this comment

thomasspriggs commented Nov 14, 2023

Replace `new-smt-backend` tag with inverted `no-new-smt` tag #8002

Replace `new-smt-backend` tag with inverted `no-new-smt` tag #8002

thomasspriggs commented Nov 7, 2023 •

edited

Loading

codecov bot commented Nov 7, 2023 •

edited

Loading