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

Uniswap modifications to enable summarization #28

Merged
merged 9 commits into from
Sep 11, 2024
Merged

Conversation

mariaKt
Copy link
Contributor

@mariaKt mariaKt commented Sep 9, 2024

This PR creates a copy of the UniswapV2Swap test, and makes the following changes, mostly related to names:

  • replace all names starting with a capital letter. We replace the capital letter with the lowercase letter, or append a descriptive prefix. This is done to avoid having these names treated as Variables from the K parser when parsing a configuration.
  • replace names that include underscores. We convert the names to camel case. If the names start with underscore, we also append a prefix (vid for variables, fid for functions).
  • we add names to key and value types of mappings. This is done because accessors automatically generated by the semantics are prefixed with $, and the parser attempts to treat them as symbolic variables.

The test has been locally tested to rewrite to .K for the provided input.

@mariaKt mariaKt marked this pull request as ready for review September 9, 2024 22:49
Copy link
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

Seems fine but I'd like us to get regression testing working. So please either set up a test harness for the test/examples directory (preferred), or just put this in test/regression.

@mariaKt
Copy link
Contributor Author

mariaKt commented Sep 11, 2024

I set up the infrastructure for testing in the examples directory.
The idea is that we may want to execute a contract with multiple .tnx files , or none. So, I chose the convention that the transactions will have the same directory structure as the examples directory, but for each C.sol file there will be a matching directory, named C. C will contain all transaction files .tnx we want to execute C.sol with. For each T.tnx, C will also contain the corresponding reference output T.ref.

@mariaKt mariaKt merged commit 53aacb1 into main Sep 11, 2024
1 check passed
@mariaKt mariaKt deleted the uniswap-renames branch September 11, 2024 15:21
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.

2 participants