Skip to content

Make unique states checking for regular symbolic tests #559

@igorganich

Description

@igorganich

Is your feature request related to a problem? Please describe.
In invariant testing, halmos has an optimization that allows us to process only unique paths after a symbolic call to the next function. But this can be improved if we can specify "checkpoints" directly in the solidity code, at the location of which we want to see only unique states.

Describe the solution you'd like
Add new cheatcode assumeUniqueState(uint256 checkpoint_id)

Reference is from here

fallback() external payable {
  ...
  executeSymbolicallyAllTargets("fallback_target");
  ...
}

In callback processing I would also like to have a way to filter out known duplicate paths:

fallback() external payable {
  ...
  executeSymbolicallyAllTargets("fallback_target");
  svm.assumeUniqueState(0x0);
  ...
}

The parameter is the checkpoint id. We need it because we can set many such checkpoints in different places.
A clear and concise description of what you want to happen.

Describe alternatives you've considered
Add the --only_unique_calls parameter to halmos itself, which would automatically process all external calls and check the uniqueness of the state before/after each external call of each contract (taking into account the location itself, as the checkpoint ID). That is, make states filtering more universal, not only for invariant testing

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions