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

Jump to bottom

Fix non-exhaustive warnings on gas related rules #2332

Closed
wants to merge 6 commits into from
Closed

Fix non-exhaustive warnings on gas related rules #2332

wants to merge 6 commits into from

Conversation

anvacaru
Copy link
Contributor

@anvacaru anvacaru commented Mar 6, 2024

closes: #2248

@anvacaru
Copy link
Contributor Author

anvacaru commented Mar 7, 2024

It looks like there is a slowdown

 Test                                                                | kevm-master-626fda1919 time                               | kevm-gas_warnings-28da00950c time                               | (kevm-master-626fda1919/kevm-gas_warnings-28da00950c) time 
---------------------------------------------------------------------+-----------------------------------------------------------+-----------------------------------------------------------------+------------------------------------------------------------
 erc20/ds/balanceOf-spec.k                                           | 61.17                                                     | 81.5                                                            | 0.7505521472392638                                         
 bihu/forwardToHotWallet-success-1-spec.k                            | 107.57                                                    | 141.22                                                          | 0.761719303214842                                          
 erc20/ds/transfer-failure-2-a-spec.k                                | 87.45                                                     | 104.84                                                          | 0.834128195345288                                          
 erc20/ds/transferFrom-failure-1-d-spec.k                            | 70.79                                                     | 82.28                                                           | 0.8603548857559553                                         
 bihu/forwardToHotWallet-failure-3-spec.k                            | 93.97                                                     | 107.94                                                          | 0.8705762460626274                                         
 mcd/vat-addui-pass-spec.k                                           | 151.92                                                    | 171.61                                                          | 0.8852630965561447                                         
 bihu/forwardToHotWallet-failure-4-spec.k                            | 171.32                                                    | 184.09                                                          | 0.9306317562062034                                         
 kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k     | 111.84                                                    | 119.29                                                          | 0.9375471539944672                                         
 mcd/end-subuu-pass-spec.k                                           | 78.32                                                     | 82.85                                                           | 0.9453228726614363                                         
 mcd/dsvalue-read-pass-summarize-spec.k                              | 69.34                                                     | 72.04                                                           | 0.9625208217656857                                         
 mcd/cat-file-addr-pass-rough-spec.k                                 | 136.62                                                    | 141.8                                                           | 0.9634696755994357                                         
 erc20/ds/transferFrom-success-1-spec.k                              | 106.35                                                    | 100.29                                                          | 1.0604247681723002                                         
 mcd/flipper-tau-pass-spec.k                                         | 74.92                                                     | 70.54                                                           | 1.0620924298270484                                         
 kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k | 94.19                                                     | 87.58                                                           | 1.0754738524777347                                         
 TOTAL                                                               | 1415.7700000000002                                        | 1547.8699999999997                                              | 0.9146569156324501

@PetarMax
Copy link
Contributor

PetarMax commented Mar 7, 2024

I believe that the slowdown is coming from the fact that the backend would be able to apply two rewrite rules instead of one if the [simplification] is removed. I had a similar discussion about andBool with the backend team, I will check what the solution was. Perhaps we could put all of the rules as [simplification]s (and add no-evaluators to the function if there are further complaints from the compiler).

@anvacaru
Copy link
Contributor Author

Marking all the 4 rules as simplification and adding [no-evaluators] is still raising the warnings:

[Warning] Compiler: Non exhaustive match detected:                                                                                          
`_<Gas__GAS-SYNTAX_Bool_Gas_Gas`(infGas(_),_)                                                                                               
        Source(/home/anvacaru/rv/evm-semantics/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md)                                     
        Location(23,21,23,69)                                                                                                               
        23 |        syntax Bool ::= Gas  "<Gas" Gas [function, total, no-evaluators]                                                        
           .                        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~                                                        
[Warning] Compiler: Non exhaustive match detected:                                                                                          
`_<=Gas__GAS-SYNTAX_Bool_Gas_Gas`(infGas(_),_)                                                                                              
        Source(/home/anvacaru/rv/evm-semantics/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md)                                     
        Location(24,21,24,69)                                                                                                               
        24 |                      | Gas "<=Gas" Gas [function, total, no-evaluators]

@ehildenb
Copy link
Member

Closing for now as a won't fix. We can re-open if it bumps in priority again.

@ehildenb ehildenb closed this Mar 12, 2024
@ehildenb ehildenb deleted the gas_warnings branch March 12, 2024 15:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ehildenb ehildenb ehildenb left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Fix warnings on non-exhaustive matches for rules
3 participants
@anvacaru @PetarMax @ehildenb