Add a warning on non-test analysis w/o foundry_success checking

[lisandrasilva]

If the test doesn't start with test, check, or prove, it is being symbolically explored but is not reported as failing even if the test reverts. This might confuse the user, so we emit a warning informing the user that the test is not being checked for failures.

Closes #386.

[palinatolmach]

@lisandrasilva @ehildenb I just ran it locally with --verbose, and the info message gets buried in other execution logs, so I'm worried that our external users won't see it:

INFO 2024-03-13 15:40:52,493 pyk.kore.rpc - Starting KoreServer: kore-rpc-booster ../timeout-test/out/kompiled/definition.kore --module FOUNDRY-MAIN --server-port 0 --smt-timeout 300 --smt-retry-limit 10 --llvm-backend-library ../timeout-test/out/kompiled/llvm-library/interpreter.dylib
[Info#proxy] Loading definition from ../timeout-test/out/kompiled/definition.kore, main module "FOUNDRY-MAIN"
[Info#kore] : Info (LogMessage):
    Reading the input file TimeSpec {sec = 0, nsec = 74923000} []
[Info#kore] : Info (LogMessage):
    Parsing the file TimeSpec {sec = 0, nsec = 0} []
[Info#kore] : Info (LogMessage):
    Verifying the definition TimeSpec {sec = 0, nsec = 0} []
[Info#kore] : Info (LogMessage):
    Executing TimeSpec {sec = 1, nsec = 88710000} []
[Info#kore] : Info (LogMessage):
    Reading the input file TimeSpec {sec = 0, nsec = 77683000} []
[Info#kore] : Info (LogMessage):
    Parsing the file TimeSpec {sec = 0, nsec = 0} []
[Info#kore] : Info (LogMessage):
    Verifying the definition TimeSpec {sec = 0, nsec = 1000} []
[Info#proxy] Starting RPC server
INFO 2024-03-13 15:41:02,840 pyk.kore.rpc - KoreServer started: :::57343, pid=11646
INFO 2024-03-13 15:41:02,840 pyk.kore.rpc - Connecting to host: localhost:57343
INFO 2024-03-13 15:41:02,842 pyk.kore.rpc - Connected to host: localhost:57343
INFO 2024-03-13 15:41:02,842 pyk.kast.outer - Loading JSON definition: ../timeout-test/out/kompiled/compiled.json
INFO 2024-03-13 15:41:03,159 pyk.kast.outer - Converting JSON definition to Kast: ../timeout-test/out/kompiled/compiled.json
INFO 2024-03-13 15:41:03,730 pyk.kore.kompiled - Reading JSON definition: ../timeout-test/out/kompiled/pyk-definition.kore.json
INFO 2024-03-13 15:41:03,983 kontrol.prove - Initializing KCFG for test: test%ConstructorTest.run_constructor():0
INFO 2024-03-13 15:41:04,054 kontrol.prove - test%ConstructorTest.run_constructor() is not prefixed with test or testFail, therefore it is not reported as failing in the presence of reverts or assertion violations.
INFO 2024-03-13 15:41:04,056 kontrol.prove - Expanding macros in node 1 for test: test%ConstructorTest.run_constructor()
INFO 2024-03-13 15:41:04,149 kontrol.prove - Computing definedness constraint for node 1 for test: test%ConstructorTest.run_constructor()
INFO 2024-03-13 15:41:04,158 pyk.kore.rpc - Sending request to localhost:57343: 1 - simplify
[Info] Process request 1 simplify
[Info#booster] Simplifying predicates

Can we maybe bring it closer to the start of the execution or, instead, print it next to the proof execution result (PROOF PASSED ...)?

[lisandrasilva]

Can we maybe bring it closer to the start of the execution or, instead, print it next to the proof execution result (PROOF PASSED ...)?
@palinatolmach Yes, I can take care of that. Which option do you prefer? At the beginning of execution or next to the execution result?

[palinatolmach]

@palinatolmach Yes, I can take care of that. Which option do you prefer? At the beginning of execution or next to the execution result?

Thanks @lisandrasilva! I think I'd prefer it next to the result to make sure people interpret PASSING correctly, but it's better to check with @ehildenb too.

[lisandrasilva]

Right now, the warning is as follows:

...
[Info] Process request 15 implies
[Info#proxy] ImpliesM (using kore)
[Info] Process request 16 implies
[Info#proxy] ImpliesM (using kore)
WARNING 2024-03-13 16:26:37,760 kontrol.prove - assertEq_true(uint256) is not prefixed with test or testFail, therefore it is not reported as failing in the presence of reverts or assertion violations.
[Info#proxy] Server shutting down
PROOF PASSED: test%HevmTests.assertEq_true(uint256):0
time: 55s

It's still not ideal since if there is more than one proof running it gets again buried in the execution log. I'll print it together with the proof status so it's more visible to the user.

[lisandrasilva]

Right now, it is printed as follows:

...
[Info] Process request 15 implies
[Info#proxy] ImpliesM (using kore)
[Info] Process request 16 implies
[Info#proxy] ImpliesM (using kore)
[Info#proxy] Server shutting down
PROOF PASSED: test%HevmTests.assertEq_true(uint256):0
time: 55s
Info: test%HevmTests.assertEq_true(uint256):0 is not prefixed with test or testFail, therefore it is not reported as failing in the presence of reverts or assertion violations.

Please let me know what you think.

[palinatolmach]

Thank you @lisandrasilva! It looks great. A few minor nits from my side:

• If Everett's ok with it, maybe we can leave it a warning, as you did originally, I think this format reads more naturally:

WARNING 2024-03-13 16:26:37,760 kontrol.prove - assertEq_true(uint256) is not prefixed with test or testFail, therefore it is not reported as failing in the presence of reverts or assertion violations.

Or maybe we can just make INFO all uppercase? If nor, I think it'd also be fine if we just unify time and Info to both start with a capital (or a small) letter.

• Another stylistic comment: I feel like it'd be more natural if we print this warning either before PROOF PASSED or between PROOF PASSED and time: .... Maybe we can print it only for passing proofs?
• I'd change is not prefixed with test or testFail to if not prefixed with 'test', 'prove', or 'check' to make sure we don't confuse users about what is considered a "test"

I don't have a strong opinion about any of these, please let me know what you'd prefer!

[palinatolmach]

Approved with some stylistic comments (please see #432 (comment)). It also requires updating expected output to include the new info message for failing tests.

[lisandrasilva]

If Everett's ok with it, maybe we can leave it a warning, as you did originally, I think this format reads more naturally

I agree!

• Another stylistic comment: I feel like it'd be more natural if we print this warning either before PROOF PASSED or between PROOF PASSED and time: .... Maybe we can print it only for passing proofs?

I would prefer before PROOF PASSED.

[lisandrasilva]

At the moment, the output is as follows:

...
[Info#proxy] Server shutting down
WARNING 2024-03-14 09:48:29,943 kontrol.__main__ - assertEq_true(uint256) is not prefixed with 'test', 'prove', or 'check', therefore, it is not reported as failing in the presence of reverts or assertion violations.
PROOF PASSED: test%HevmTests.assertEq_true(uint256):0
time: 54s

[palinatolmach]

Temporarily removed automerge to let #355 go through first.