Repository navigation
Fix warnings on non-exhaustive matches for rules #2248
Description
These warnings are emitted during the kompilation process.
[Warning] Compiler: Non exhaustive match detected:
`#lenOfHead(_)_EVM-ABI_Int_TypedArg`(`abi_type_tuple`(_))
Source(/nix/store/0ldpwmslqv838p5gcw0cadyxnd96nbdm-python3.10-kevm-pyk-1.0.406/lib/python3.10/site-packages/kevm_pyk/kproj/evm-semantics/abi.md)
Location(291,20,291,61)
291 | syntax Int ::= #lenOfHead ( TypedArg ) [function, total]
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Non exhaustive match detected:
`#isStaticType(_)_EVM-ABI_Bool_TypedArg`(`abi_type_tuple`(_))
Source(/nix/store/0ldpwmslqv838p5gcw0cadyxnd96nbdm-python3.10-kevm-pyk-1.0.406/lib/python3.10/site-packages/kevm_pyk/kproj/evm-semantics/abi.md)
Location(402,21,402,65)
402 | syntax Bool ::= #isStaticType ( TypedArg ) [function, total]
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Non exhaustive match detected:
`_<Gas__GAS-SYNTAX_Bool_Gas_Gas`(infGas(_),_)
Source(/nix/store/0ldpwmslqv838p5gcw0cadyxnd96nbdm-python3.10-kevm-pyk-1.0.406/lib/python3.10/site-packages/kevm_pyk/kproj/evm-semantics/gas.md)
Location(23,21,23,54)
23 | syntax Bool ::= Gas "<Gas" Gas [function, total]
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Non exhaustive match detected:
`_<=Gas__GAS-SYNTAX_Bool_Gas_Gas`(infGas(_),infGas(_))
Source(/nix/store/0ldpwmslqv838p5gcw0cadyxnd96nbdm-python3.10-kevm-pyk-1.0.406/lib/python3.10/site-packages/kevm_pyk/kproj/evm-semantics/gas.md)
Location(24,21,24,54)
24 | | Gas "<=Gas" Gas [function, total]
```
Activity
anvacaru commentedon Jan 10, 2024
The rule for
#lenOfHead( #tuple(_) )is missing. Maybe refactor all#lenOfHeadrules into a single rule like:The rule for
#isStaticType (#tuple ( TUPLE_ARGS ))is missing. We should add some logic here that does anORonisStaticType()for each argument inTUPLE_ARGS.simplification, so the llvm-backend issuesNon-Exhaustive matchon the operators<Gas,<=Gasfor these cases (source here).Why do they have to be marked as
simplification? Should the entireINFINITE-GASmodule be marked assymbolic?cc @ehildenb @dkcumming
dkcumming commentedon Jan 10, 2024
@anvacaru I believe the original rules that this module was replacing marked the rules as
[simplification], and that I was getting slower results for performance if[simplification]was not added for this module. I concluded that it must be doing short circuit evaluation and avoiding evaluation LHS and RHS of the comparison if the attribute was added, but I don't have much confidence in that now. It is entirely possible that they ought not be marked[simplification].I am not sure if the whole module should be marked as
symbolicsorry, perhaps @ehildenb can offer more insight.[-]Address warnings on non-exhaustive matches for rules[/-][+]Fix warnings on non-exhaustive matches for rules[/+]