runtimeverification/evm-semantics

Fix warnings on non-exhaustive matches for rules

Opened this issue · 2 comments

anvacaru commented

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]
        ```
anvacaru commented 
`#lenOfHead(_)_EVM-ABI_Int_TypedArg`(`abi_type_tuple`(_))

The rule for #lenOfHead( #tuple(_) ) is missing. Maybe refactor all #lenOfHead rules into a single rule like:

rule #lenOfHead ( _ ) => 32

`#isStaticType(_)_EVM-ABI_Bool_TypedArg`(`abi_type_tuple`(_))

The rule for #isStaticType (#tuple ( TUPLE_ARGS )) is missing. We should add some logic here that does an OR on isStaticType() for each argument in TUPLE_ARGS.

  1. and 4. Both rules below are marked as simplification, so the llvm-backend issues Non-Exhaustive match on the operators <Gas, <=Gas for these cases (source here).
    rule #gas(_)  <Gas _       => false [simplification]
    rule _       <=Gas #gas(_) => true  [simplification]

Why do they have to be marked as simplification? Should the entire INFINITE-GAS module be marked as symbolic?
cc @ehildenb @dkcumming

dkcumming commented

@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 symbolic sorry, perhaps @ehildenb can offer more insight.

  • 👍1