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

Competed paths number becomes frozen #444

Open
igorganich opened this issue Jan 17, 2025 · 1 comment
Open

Competed paths number becomes frozen #444

igorganich opened this issue Jan 17, 2025 · 1 comment
Labels
bug Something isn't working

Comments

@igorganich
Copy link

Describe the bug
The number of completed paths stops changing at some point.
Due to this, traces with the -vvvvv option are not even displayed.
At the same time, the analysis continues, as the number of outstanding paths constantly increases and decreases

To Reproduce

  1. checkout on
    igorganich/damn-vulnerable-defi-halmos@e4f554f
  2. run halmos --solver-timeout-assertion 0 --function check_backdoor --loop 100
  3. See frozen number of completed paths. It is 294 paths on my machine.

Environment:

  • OS: ubuntu wsl
  • Python version: Python 3.12.3
  • Halmos and other dependency versions: halmos 0.2.4.dev6+g606ac51
@igorganich igorganich added the bug Something isn't working label Jan 17, 2025
@igorganich igorganich changed the title Broken paths generation Competed paths number becomes frozen Jan 17, 2025
@igorganich
Copy link
Author

I suspect the problem is using vm.snapshotState() function and assuming that the state was changed after some symbolic call.
And if not - the path will not count as "completed". Since it can't find any completed path it looks like this number is frozen.

But It is hard to debug such paths. Maybe halmos should print even such non-reverted but stopped by "assume" paths?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant