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.

Sign up for GitHub

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

fix: check infeasible errors #445

Merged
merged 3 commits into from
Jan 22, 2025
Merged

fix: check infeasible errors #445

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
edeb7c6
ci: snekmate venom
daejunpark Jan 21, 2025
11e84e4
fix: check infeasible errors
daejunpark Jan 21, 2025
12ec493
debug message for checking error conditions
daejunpark Jan 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions .github/workflows/test-external.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,22 +54,22 @@ jobs:
dir: "snekmate"
cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
branch: ""
profile: "halmos"
profile: "halmos-venom"
- repo: "pcaversaccio/snekmate"
dir: "snekmate"
cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
branch: ""
profile: "halmos"
profile: "halmos-venom"
- repo: "pcaversaccio/snekmate"
dir: "snekmate"
cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
branch: ""
profile: "halmos"
profile: "halmos-venom"
- repo: "pcaversaccio/snekmate"
dir: "snekmate"
cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
branch: ""
profile: "halmos"
profile: "halmos-venom"

steps:
- name: Checkout halmos
Expand Down
9 changes: 6 additions & 3 deletions src/halmos/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -724,9 +724,12 @@ def future_callback(future_model):
future_models.append(future_model)

elif ex.context.is_stuck():
stuck.append((idx, ex, ex.context.get_stuck_reason()))
if args.print_blocked_states:
traces[idx] = f"{hexify(ex.path)}\n{rendered_trace(ex.context)}"
debug(f"Potential error path (id: {idx+1})")
res, _, _ = solve(ex.path.to_smt2(args), args)
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

performance concern: this may block the path exploration thread.

an alternative approach is to add this into the assertion-solving thread pool, but it requires further code refactoring. not sure it's worth it at this point.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yeah that would be a big change, and would break some assumptions in the assertion-solving thread pool (sincewe collect/triage/print counterexamples). If necessary we could add a separation branch-solving thread pool, but I don't think it would interact well with the z3 context push/pop mechanism (can't really keep exploring another branch until this one is done)

if res != unsat:
stuck.append((idx, ex, ex.context.get_stuck_reason()))
if args.print_blocked_states:
traces[idx] = f"{hexify(ex.path)}\n{rendered_trace(ex.context)}"

elif not error_output:
if args.print_success_states:
Expand Down
Loading