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

feat: support natspec annotations #133

Merged
merged 11 commits into from
Jul 21, 2023
Merged

feat: support natspec annotations #133

merged 11 commits into from
Jul 21, 2023

Conversation

daejunpark
Copy link
Collaborator

@daejunpark daejunpark commented Jul 20, 2023

fix #131

Support @custom:halmos natspec annotation to specify additional commandline options.

The natspec for a contract is inherited by every function in the contract. The natspec for a function can overwrite the inherited natspec.

For example, given:

/// @custom:halmos --opt1 --loop 1
contract C {

    /// @custom:halmos --opt2 --loop 2
    function checkA() { ... }
}

The options for the checkA() function are: --opt1 --opt2 --loop 2

Note that it inherits --opt1 but overwrites --loop 1.

--

The halmos natspec can be provided in multiline:

/// @custom:halmos --x
///                --y

or, using multiple tags:

/// @custom:halmos --x
/// @custom:halmos --y

@@ -887,9 +700,18 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]:
return test_results


def extend_args(args: Namespace, more_opts: str) -> Namespace:
if more_opts:
new_args = deepcopy(args)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I was looking for something to avoid the need for a deepcopy here, I ended up with this:

import argparse
import collections

parser = argparse.ArgumentParser()
parser.add_argument('--foo')
parser.add_argument('--bar')
parser.add_argument('--loop')

def dictify(args):
    return {k: v for k, v in vars(args).items() if v is not None}

defaults = parser.parse_args(['--foo', 'beep', '--bar', 'boop'])
overrides = parser.parse_args(['--foo', 'ding', '--loop', '42'])
combined = collections.ChainMap(dictify(overrides), dictify(defaults))

print(combined['foo']) # 'ding' comes from overrides, takes precedence over defaults
print(combined['bar']) # 'boop' comes from defaults
print(combined['loop']) # '42' comes from overrides, not specified in defaults

ChainMap is cool but in the end it's not necessarily better because there is still some copying involved because of a poor interaction with Namespace. Might make sense to write our own NamespaceChain-like wrapper that avoids any copying at all at a later point

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

do you suggest using chainmap now, or doing something better later?

i wasn't super happy with using deepcopy here, but thought that the namespace object should be small enough and deepcopy wouldn't affect performance much. are there any other issues that i missed?

Copy link
Collaborator

Choose a reason for hiding this comment

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

no it's just a general dislike of deepcopy creep. Disregard for now

karmacoma-eth
karmacoma-eth previously approved these changes Jul 20, 2023
Copy link
Collaborator

@karmacoma-eth karmacoma-eth left a comment

Choose a reason for hiding this comment

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

this is great, can't wait to start using it

@daejunpark
Copy link
Collaborator Author

the external test failures are independent from this pr. it will be fixed by #134. will merge this pr after merging that.

@daejunpark daejunpark merged commit 0b92223 into main Jul 21, 2023
@daejunpark daejunpark deleted the feat/halmos-annotation branch July 21, 2023 00:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support for custom NatSpec annotations
2 participants