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

feat: reject multiple setup paths #351

Merged
merged 5 commits into from
Aug 24, 2024
Merged

feat: reject multiple setup paths #351

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9f3e119
deprecated --bytecode
daejunpark Aug 23, 2024
a52ed73
deprecated --reset-bytecode
daejunpark Aug 23, 2024
a7a2aac
feat: do not allow multiple setup paths
daejunpark Aug 23, 2024
b9df6fe
test: fix flakiness of context tests for ci
daejunpark Aug 23, 2024
125f22a
Merge branch 'main' into feat/fail-multiple-setups
daejunpark Aug 24, 2024
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
7 changes: 2 additions & 5 deletions src/halmos/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -506,14 +506,11 @@ def setup(
raise HalmosException(f"No successful path found in {setup_sig}")

if len(setup_exs) > 1:
info(
f"Warning: multiple paths were found in {setup_sig}; "
"an arbitrary path has been selected for the following tests."
)

if args.debug:
print("\n".join(map(str, setup_exs)))

raise HalmosException(f"Multiple paths were found in {setup_sig}")

setup_ex = setup_exs[0]

if args.print_setup_states:
Expand Down
23 changes: 21 additions & 2 deletions tests/regression/test/Context.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,10 @@ contract ContextTest is Test {
}

function check_call0_normal(uint mode0) public payable {
require(mode0 < 9);
// vm.assume(mode0 < 9);
// NOTE: explicitly branch over mode0, as an infeasible path with mode0 >= 9 may not be eliminated due to an extremely inefficient solver environment (e.g, github workflow)
mode0 = split_mode_up_to_9(mode0);

_check_call0(mode0);
Comment on lines +194 to 198
Copy link
Collaborator

Choose a reason for hiding this comment

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

wait what? I don't understand what's going on here

Copy link
Collaborator Author

@daejunpark daejunpark Aug 24, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

this is not related to this pr. it's a temporary fix to a flaky test that i found.

details of the flaky test: when mode0 == 9, _check_call0() fails due to HalmosException (which is intentional). however, the goal of this test is to consider only success paths, so the assumption mode0 < 9 is provided at the beginning. however, the HalmosException path may still appear after path exploration, if the branching solver couldn't solve its infeasible path condition. this won't happen under normal circumstances, as the path condition mode0 < 9 && mode0 == 9 is obviously unsat. but in the github runner, the solver may timeout, leading to a test failure, due to the HalmosException path, even if it is infeasible. a proper fix is more involved, and will be implemented later.

Copy link
Collaborator

Choose a reason for hiding this comment

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

got it, thank you

}

Expand Down Expand Up @@ -221,7 +224,10 @@ contract ContextTest is Test {
}

function check_call1_normal(uint mode1, uint mode0) public payable {
require(mode0 < 9);
// vm.assume(mode0 < 9);
// NOTE: explicitly branch over mode0, as an infeasible path with mode0 >= 9 may not be eliminated due to an extremely inefficient solver environment (e.g, github workflow)
mode0 = split_mode_up_to_9(mode0);

_check_call1(mode1, mode0);
}

Expand Down Expand Up @@ -273,6 +279,19 @@ contract ContextTest is Test {
else if (mode == 10) assert(!success && retdata.length == 0);
}

function split_mode_up_to_9(uint mode) internal returns (uint) {
if (mode == 0) return 0;
else if (mode == 1) return 1;
else if (mode == 2) return 2;
else if (mode == 3) return 3;
else if (mode == 4) return 4;
else if (mode == 5) return 5;
else if (mode == 6) return 6;
else if (mode == 7) return 7;
else if (mode == 8) return 8;
else return 0;
}

function returndatasize() internal pure returns (uint size) {
assembly {
size := returndatasize()
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/test/SetupSymbolic.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ pragma solidity >=0.8.0 <0.9.0;

contract SetupSymbolicTest {
function setUpSymbolic(uint x) public pure {
if (x > 0) return; // generate multiple setup output states
if (x > 0) revert(); // generate multiple setup output states, but only a single success output state
}

function check_True() public pure {
Expand Down