Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verify proveX and checkX functions similarly to testX #249

Merged
merged 11 commits into from
Jan 12, 2024

Conversation

palinatolmach
Copy link
Collaborator

@palinatolmach palinatolmach commented Dec 15, 2023

Closes #247.

Currently, this PR adds an error that is thrown if any of the function names provided with --match-test do not start with test or testFail, but should be refactored.

At the moment, only functions starting with test and testFail are checked for Foundry success predicate and will fail if the function reverts. There are two issues with this approach:

  • tests prefixed with test/testFail are picked up for fuzzing during a forge test run, and we don't provide a way to specify Kontrol-specific functions
  • symbolic tests written for other tools (Halmos and hevm, in particular)

The changes introduced in this PR include:

  • the ability to handle functions that start with prove and check prefixes similarly to those starting with test
  • a simple tests for this new functionality: prove_assert_true(); this test is skipped in the legacy CI in order to not increase it's runtime and since the change is relatively minor

@palinatolmach palinatolmach marked this pull request as ready for review December 15, 2023 09:13
@palinatolmach palinatolmach marked this pull request as draft December 15, 2023 09:20
@palinatolmach palinatolmach changed the title Error if test doesn't start with test/testFail Prove tests that don't start with test/testFail correctly Dec 15, 2023
src/kontrol/__main__.py Outdated Show resolved Hide resolved
src/kontrol/__main__.py Outdated Show resolved Hide resolved
@palinatolmach palinatolmach changed the title Prove tests that don't start with test/testFail correctly [do not merge] Prove tests that don't start with test/testFail correctly Dec 18, 2023
@palinatolmach
Copy link
Collaborator Author

As highlighted by @RaoulSchaffranek and @anvacaru, some of our use-cases such as the debugger and CSE require executing functions that do not start with test. In this case, we should probably make it clear that we're not checking for violations in the documentation and/or through a warning message to the user.

@palinatolmach
Copy link
Collaborator Author

palinatolmach commented Jan 11, 2024

Based on the discussion in today's standup, we decided to handle tests prefixed with prove and proveFail similarly to those starting with test. That would help us define Kontrol-specific functions that would not get executed during a forge test run and would also make Kontrol compatible with Halmos and hevm symbolic tests.

cc @JuanCoRo

@palinatolmach palinatolmach changed the title [do not merge] Prove tests that don't start with test/testFail correctly [do not merge] Verify proveX functions similarly to testX Jan 11, 2024
@palinatolmach palinatolmach reopened this Jan 11, 2024
@palinatolmach palinatolmach changed the title [do not merge] Verify proveX functions similarly to testX Verify proveX functions similarly to testX Jan 11, 2024
@palinatolmach palinatolmach changed the title Verify proveX functions similarly to testX Verify proveX and checkX functions similarly to testX Jan 11, 2024
@palinatolmach palinatolmach marked this pull request as ready for review January 11, 2024 14:18
src/kontrol/prove.py Outdated Show resolved Hide resolved
@anvacaru
Copy link
Contributor

Can you test this by renaming one of the existing tests (for which we check the output) with the new prefixes?

src/kontrol/prove.py Outdated Show resolved Hide resolved
@palinatolmach palinatolmach deleted the rescrict-test-names branch January 12, 2024 05:58
@palinatolmach palinatolmach restored the rescrict-test-names branch January 12, 2024 06:01
@palinatolmach palinatolmach reopened this Jan 12, 2024
@palinatolmach
Copy link
Collaborator Author

Can you test this by renaming one of the existing tests (for which we check the output) with the new prefixes?

@anvacaru I renamed one of the tests for which we check expected output from AssertTest.testFail_assert_false() to AssertTest.checkFail_assert_false() in 51848f4. To avoid increasing the CI load, I removed testFail_assert_false, so there's only checkFail_assert_false now. I find it sufficient, since the change is rather small and we're checking similar functionality with other testFail tests. prove prefix is also checked in AssertTest.prove_assert_true(), though without the expected output check.

Please let me know if you think we should test it more exhaustively, and thank you for all the suggestions!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Failed proof isn't reported if function doesn't start with test or testFail
5 participants