Skip to content

Rule merger: bug fix and better error messages #2230

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
Merged
merged 12 commits into from
Nov 6, 2020
Merged

Rule merger: bug fix and better error messages #2230

merged 12 commits into from
Nov 6, 2020

Conversation

ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Oct 28, 2020 •
edited
Loading

Fixes #2228
Fixes #2226

Reviewer checklist
  • Test coverage: stack test --coverage
  • Public API documentation: stack haddock

@ana-pantilie
Copy link
Contributor Author

ana-pantilie commented Oct 29, 2020 •
edited
Loading

Output from the test in #2226:

/*  */
\rewrites{SortGeneratedTopCell{}}(
    /*  */
    \and{SortGeneratedTopCell{}}(
        /*  */ \not{SortGeneratedTopCell{}}(/*  */ priorityLE40{}()),
        /* Spc */
        \and{SortGeneratedTopCell{}}(
            /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
            /* Sfc */
            \and{SortGeneratedTopCell{}}(
                /* Sfa */
                \equals{SortBool{}, SortGeneratedTopCell{}}(
                    /* Fl Fn D Sfa Cl */
                    /* builtin: */ \dv{SortBool{}}("false"),
                    /* Fn Sfa */
                    Lbl'Hash'stackUnderflow'LParUndsCommUndsRParUnds'EVM'Unds'Bool'Unds'WordStack'Unds'Int{}(
                        /* Fl Fn D Sfa */ VarWS:SortWordStack{},
                        /* Fn Sfa */
                        Lbl'Hash'stackNeeded'LParUndsRParUnds'EVM'Unds'Int'Unds'OpCode{}(
                            /* Fl Fn D Sfa */ VarOP0:SortOpCode{}
                        )
                    )
                ),
                /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                /* Spc */
                \and{SortGeneratedTopCell{}}(
                    /* Sfa */
                    \equals{SortBool{}, SortGeneratedTopCell{}}(
                        /* Fl Fn D Sfa Cl */
                        /* builtin: */ \dv{SortBool{}}("false"),
                        /* Fn Sfa */
                        Lbl'Unds'andBool'Unds'{}(
                            /* Fl Fn D Sfa */ VarSTATIC:SortBool{},
                            /* Fn Sfa */
                            Lbl'Hash'changesState'LParUndsCommUndsRParUnds'EVM'Unds'Bool'Unds'OpCode'Unds'WordStack{}(
                                /* Fl Fn D Sfa */ VarOP0:SortOpCode{},
                                /* Fl Fn D Sfa */ VarWS:SortWordStack{}
                            )
                        )
                    ),
                    /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                    /* Spc */
                    \and{SortGeneratedTopCell{}}(
                        /* Sfa */
                        \equals{SortBool{}, SortGeneratedTopCell{}}(
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortBool{}}("false"),
                            /* Fn Sfa */
                            Lbl'Unds-GT-'Int'Unds'{}(
                                /* Fn Sfa */
                                Lbl'UndsPlus'Int'Unds'{}(
                                    /* Fl Fn D Sfa */
                                    Lbl'Hash'sizeWordStack'LParUndsCommUndsRParUnds'EVM-TYPES'Unds'Int'Unds'WordStack'Unds'Int{}(
                                        /* Fl Fn D Sfa */ VarWS:SortWordStack{},
                                        /* Fl Fn D Sfa Cl */
                                        /* builtin: */ \dv{SortInt{}}("0")
                                    ),
                                    /* Fn Sfa */
                                    Lbl'Unds'-Int'Unds'{}(
                                        /* Fn Sfa */
                                        Lbl'Hash'stackAdded'LParUndsRParUnds'EVM'Unds'Int'Unds'OpCode{}(
                                            /* Fl Fn D Sfa */
                                            VarOP0:SortOpCode{}
                                        ),
                                        /* Fn Sfa */
                                        Lbl'Hash'stackNeeded'LParUndsRParUnds'EVM'Unds'Int'Unds'OpCode{}(
                                            /* Fl Fn D Sfa */
                                            VarOP0:SortOpCode{}
                                        )
                                    )
                                ),
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("1024")
                            )
                        ),
                        /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                        /* Spc */
                        \and{SortGeneratedTopCell{}}(
                            /* Sfc */
                            \equals{SortBool{}, SortGeneratedTopCell{}}(
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortBool{}}("false"),
                                /* Fn Sfc */
                                LblisCallOp{}(
                                    /* Fl Fn D Sfc */
                                    kseq{}(
                                        /* Fl Fn D Sfc */
                                        /* Inj: */ inj{SortOpCode{}, SortKItem{}}(
                                            /* Fl Fn D Sfa */
                                            VarOP0:SortOpCode{}
                                        ),
                                        /* Fl Fn D Sfa Cl */ dotk{}()
                                    )
                                )
                            ),
                            /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                            /* Spc */
                            \and{SortGeneratedTopCell{}}(
                                /* Sfc */
                                \equals{SortBool{}, SortGeneratedTopCell{}}(
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortBool{}}("false"),
                                    /* Fn Sfc */
                                    LblisCallSixOp{}(
                                        /* Fl Fn D Sfc */
                                        kseq{}(
                                            /* Fl Fn D Sfc */
                                            /* Inj: */ inj{SortOpCode{}, SortKItem{}}(
                                                /* Fl Fn D Sfa */
                                                VarOP0:SortOpCode{}
                                            ),
                                            /* Fl Fn D Sfa Cl */ dotk{}()
                                        )
                                    )
                                ),
                                /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                                /* Spa */
                                \and{SortGeneratedTopCell{}}(
                                    /* Sfa */
                                    \not{SortGeneratedTopCell{}}(
                                        /* Spa */
                                        \equals{SortOpCode{}, SortGeneratedTopCell{}}(
                                            /* Fl Fn D Sfa */
                                            VarOP0:SortOpCode{},
                                            /* Fl Fn D Sfa Cli */
                                            /* Inj: */ inj{SortQuadStackOp{}, SortOpCode{}}(
                                                /* Fl Fn D Sfa Cl */
                                                LblEXTCODECOPY'Unds'EVM'Unds'QuadStackOp{}()
                                            )
                                        )
                                    ),
                                    /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                                    /* Spa */
                                    \and{SortGeneratedTopCell{}}(
                                        /* Sfa */
                                        \not{SortGeneratedTopCell{}}(
                                            /* Spa */
                                            \equals{SortOpCode{}, SortGeneratedTopCell{}}(
                                                /* Fl Fn D Sfa */
                                                VarOP0:SortOpCode{},
                                                /* Fl Fn D Sfa Cli */
                                                /* Inj: */ inj{SortUnStackOp{}, SortOpCode{}}(
                                                    /* Fl Fn D Sfa Cl */
                                                    LblBALANCE'Unds'EVM'Unds'UnStackOp{}()
                                                )
                                            )
                                        ),
                                        /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                                        /* Spa */
                                        \and{SortGeneratedTopCell{}}(
                                            /* Sfa */
                                            \not{SortGeneratedTopCell{}}(
                                                /* Spa */
                                                \equals{SortOpCode{}, SortGeneratedTopCell{}}(
                                                    /* Fl Fn D Sfa */
                                                    VarOP0:SortOpCode{},
                                                    /* Fl Fn D Sfa Cli */
                                                    /* Inj: */ inj{SortUnStackOp{}, SortOpCode{}}(
                                                        /* Fl Fn D Sfa Cl */
                                                        LblEXTCODEHASH'Unds'EVM'Unds'UnStackOp{}()
                                                    )
                                                )
                                            ),
                                            /* Created: Kore.Internal.MultiAnd.makeAndPredicate */
                                            /* Spa */
                                            \and{SortGeneratedTopCell{}}(
                                                /* Sfa */
                                                \not{SortGeneratedTopCell{}}(
                                                    /* Spa */
                                                    \equals{SortOpCode{}, SortGeneratedTopCell{}}(
                                                        /* Fl Fn D Sfa */
                                                        VarOP0:SortOpCode{},
                                                        /* Fl Fn D Sfa Cli */
                                                        /* Inj: */ inj{SortUnStackOp{}, SortOpCode{}}(
                                                            /* Fl Fn D Sfa Cl */
                                                            LblEXTCODESIZE'Unds'EVM'Unds'UnStackOp{}()
                                                        )
                                                    )
                                                ),
                                                /* Sfa */
                                                \not{SortGeneratedTopCell{}}(
                                                    /* Spa */
                                                    \equals{SortOpCode{}, SortGeneratedTopCell{}}(
                                                        /* Fl Fn D Sfa */
                                                        VarOP0:SortOpCode{},
                                                        /* Fl Fn D Sfa Cli */
                                                        /* Inj: */ inj{SortUnStackOp{}, SortOpCode{}}(
                                                            /* Fl Fn D Sfa Cl */
                                                            LblSELFDESTRUCT'Unds'EVM'Unds'UnStackOp{}()
                                                        )
                                                    )
                                                )
                                            )
                                        )
                                    )
                                )
                            )
                        )
                    )
                )
            ),
            /* Fl Fn D Spa */
            Lbl'-LT-'generatedTop'-GT-'{}(
                /* Fl Fn D Spa */
                Lbl'-LT-'firefly'-GT-'{}(
                    /* Fl Fn D Sfa */ Var'Unds'63:SortKevmCoverageCell{},
                    /* Fl Fn D Sfa */ Var'Unds'64:SortWeb3DebugCell{},
                    /* Fl Fn D Spa */
                    Lbl'-LT-'kevm-client'-GT-'{}(
                        /* Fl Fn D Spa */
                        Lbl'-LT-'kevm'-GT-'{}(
                            /* Fl Fn D Spa */
                            Lbl'-LT-'k'-GT-'{}(
                                /* Fl Fn D Spa */
                                kseq{}(
                                    /* Fl Fn D Spa */
                                    /* Inj: */ inj{SortInternalOp{}, SortKItem{}}(
                                        /* Fl Fn D Spa */
                                        Lbl'Hash'next'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode{}(
                                            /* Fl Fn D Sfa */
                                            VarOP0:SortOpCode{}
                                        )
                                    ),
                                    /* Fl Fn D Sfa */ Var'Unds'DotVar4:SortK{}
                                )
                            ),
                            /* Fl Fn D Sfa */ Var'Unds'44:SortExitCodeCell{},
                            /* Fl Fn D Sfa */ Var'Unds'45:SortModeCell{},
                            /* Fl Fn D Sfa */ Var'Unds'46:SortScheduleCell{},
                            /* Fl Fn D Sfa */
                            Lbl'-LT-'ethereum'-GT-'{}(
                                /* Fl Fn D Sfa */
                                Lbl'-LT-'evm'-GT-'{}(
                                    /* Fl Fn D Sfa */
                                    Var'Unds'12:SortOutputCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'13:SortStatusCodeCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'14:SortEndPCCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'15:SortCallStackCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'16:SortInterimStatesCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'17:SortTouchedAccountsCell{},
                                    /* Fl Fn D Sfa */
                                    Lbl'-LT-'callState'-GT-'{}(
                                        /* Fl Fn D Sfa */
                                        Var'Unds'0:SortProgramCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'1:SortJumpDestsCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'2:SortIdCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'3:SortCallerCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'4:SortCallDataCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'5:SortCallValueCell{},
                                        /* Fl Fn D Sfa */
                                        Lbl'-LT-'wordStack'-GT-'{}(
                                            /* Fl Fn D Sfa */
                                            VarWS:SortWordStack{}
                                        ),
                                        /* Fl Fn D Sfa */
                                        Var'Unds'6:SortLocalMemCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'7:SortPcCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'8:SortGasCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'9:SortMemoryUsedCell{},
                                        /* Fl Fn D Sfa */
                                        Var'Unds'10:SortCallGasCell{},
                                        /* Fl Fn D Sfa */
                                        Lbl'-LT-'static'-GT-'{}(
                                            /* Fl Fn D Sfa */
                                            VarSTATIC:SortBool{}
                                        ),
                                        /* Fl Fn D Sfa */
                                        Var'Unds'11:SortCallDepthCell{}
                                    ),
                                    /* Fl Fn D Sfa */
                                    Var'Unds'18:SortSubstateCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'19:SortGasPriceCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'20:SortOriginCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'21:SortBlockhashesCell{},
                                    /* Fl Fn D Sfa */
                                    Var'Unds'22:SortBlockCell{}
                                ),
                                /* Fl Fn D Sfa */
                                Var'Unds'DotVar5:SortNetworkCell{}
                            )
                        ),
                        /* Fl Fn D Sfa */ Var'Unds'48:SortJsonRpcCell{},
                        /* Fl Fn D Sfa */ Var'Unds'49:SortBlockchainCell{},
                        /* Fl Fn D Sfa */ Var'Unds'50:SortStateTrieCell{},
                        /* Fl Fn D Sfa */ Var'Unds'51:SortDefaultGasPriceCell{},
                        /* Fl Fn D Sfa */ Var'Unds'52:SortDefaultGasLimitCell{},
                        /* Fl Fn D Sfa */ Var'Unds'53:SortTimeDiffCell{},
                        /* Fl Fn D Sfa */ Var'Unds'54:SortTimeFreezeCell{},
                        /* Fl Fn D Sfa */
                        Var'Unds'55:SortUnlimitedContractsCell{},
                        /* Fl Fn D Sfa */ Var'Unds'56:SortAccountKeysCell{},
                        /* Fl Fn D Sfa */ Var'Unds'57:SortNextFilterSlotCell{},
                        /* Fl Fn D Sfa */ Var'Unds'58:SortTxReceiptsCell{},
                        /* Fl Fn D Sfa */ Var'Unds'59:SortFiltersCell{},
                        /* Fl Fn D Sfa */ Var'Unds'60:SortSnapshotsCell{},
                        /* Fl Fn D Sfa */
                        Var'Unds'61:SortWeb3shutdownableCell{},
                        /* Fl Fn D Sfa */
                        Var'Unds'62:SortWeb3notificationsCell{}
                    ),
                    /* Fl Fn D Sfa */ Var'Unds'65:SortRandomizerCell{}
                ),
                /* Fl Fn D Sfa */ Var'Unds'DotVar6:SortGeneratedCounterCell{}
            )
        )
    ),
    /* Fl Fn D Spc */
    Lbl'-LT-'generatedTop'-GT-'{}(
        /* Fl Fn D Spc */
        Lbl'-LT-'firefly'-GT-'{}(
            /* Fl Fn D Sfa */ Var'Unds'63:SortKevmCoverageCell{},
            /* Fl Fn D Sfa */ Var'Unds'64:SortWeb3DebugCell{},
            /* Fl Fn D Spc */
            Lbl'-LT-'kevm-client'-GT-'{}(
                /* Fl Fn D Spc */
                Lbl'-LT-'kevm'-GT-'{}(
                    /* Fl Fn D Spc */
                    Lbl'-LT-'k'-GT-'{}(
                        /* Fl Fn D Sfc */
                        kseq{}(
                            /* Fl Fn D Sfc */
                            /* Inj: */ inj{SortInternalOp{}, SortKItem{}}(
                                /* Fl Fn D Sfa */
                                Lbl'Hash'exec'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode{}(
                                    /* Fl Fn D Sfa */ VarOP0:SortOpCode{}
                                )
                            ),
                            /* Fl Fn D Sfc */
                            kseq{}(
                                /* Fl Fn D Sfc */
                                /* Inj: */ inj{SortInternalOp{}, SortKItem{}}(
                                    /* Fl Fn D Sfa */
                                    Lbl'Hash'pc'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode{}(
                                        /* Fl Fn D Sfa */ VarOP0:SortOpCode{}
                                    )
                                ),
                                /* Fl Fn D Sfa */ Var'Unds'DotVar4:SortK{}
                            )
                        )
                    ),
                    /* Fl Fn D Sfa */ Var'Unds'44:SortExitCodeCell{},
                    /* Fl Fn D Sfa */ Var'Unds'45:SortModeCell{},
                    /* Fl Fn D Sfa */ Var'Unds'46:SortScheduleCell{},
                    /* Fl Fn D Sfa */
                    Lbl'-LT-'ethereum'-GT-'{}(
                        /* Fl Fn D Sfa */
                        Lbl'-LT-'evm'-GT-'{}(
                            /* Fl Fn D Sfa */ Var'Unds'12:SortOutputCell{},
                            /* Fl Fn D Sfa */ Var'Unds'13:SortStatusCodeCell{},
                            /* Fl Fn D Sfa */ Var'Unds'14:SortEndPCCell{},
                            /* Fl Fn D Sfa */ Var'Unds'15:SortCallStackCell{},
                            /* Fl Fn D Sfa */
                            Var'Unds'16:SortInterimStatesCell{},
                            /* Fl Fn D Sfa */
                            Var'Unds'17:SortTouchedAccountsCell{},
                            /* Fl Fn D Sfa */
                            Lbl'-LT-'callState'-GT-'{}(
                                /* Fl Fn D Sfa */ Var'Unds'0:SortProgramCell{},
                                /* Fl Fn D Sfa */
                                Var'Unds'1:SortJumpDestsCell{},
                                /* Fl Fn D Sfa */ Var'Unds'2:SortIdCell{},
                                /* Fl Fn D Sfa */ Var'Unds'3:SortCallerCell{},
                                /* Fl Fn D Sfa */ Var'Unds'4:SortCallDataCell{},
                                /* Fl Fn D Sfa */
                                Var'Unds'5:SortCallValueCell{},
                                /* Fl Fn D Sfa */
                                Lbl'-LT-'wordStack'-GT-'{}(
                                    /* Fl Fn D Sfa */ VarWS:SortWordStack{}
                                ),
                                /* Fl Fn D Sfa */ Var'Unds'6:SortLocalMemCell{},
                                /* Fl Fn D Sfa */ Var'Unds'7:SortPcCell{},
                                /* Fl Fn D Sfa */ Var'Unds'8:SortGasCell{},
                                /* Fl Fn D Sfa */
                                Var'Unds'9:SortMemoryUsedCell{},
                                /* Fl Fn D Sfa */ Var'Unds'10:SortCallGasCell{},
                                /* Fl Fn D Sfa */
                                Lbl'-LT-'static'-GT-'{}(
                                    /* Fl Fn D Sfa */ VarSTATIC:SortBool{}
                                ),
                                /* Fl Fn D Sfa */
                                Var'Unds'11:SortCallDepthCell{}
                            ),
                            /* Fl Fn D Sfa */ Var'Unds'18:SortSubstateCell{},
                            /* Fl Fn D Sfa */ Var'Unds'19:SortGasPriceCell{},
                            /* Fl Fn D Sfa */ Var'Unds'20:SortOriginCell{},
                            /* Fl Fn D Sfa */ Var'Unds'21:SortBlockhashesCell{},
                            /* Fl Fn D Sfa */ Var'Unds'22:SortBlockCell{}
                        ),
                        /* Fl Fn D Sfa */ Var'Unds'DotVar5:SortNetworkCell{}
                    )
                ),
                /* Fl Fn D Sfa */ Var'Unds'48:SortJsonRpcCell{},
                /* Fl Fn D Sfa */ Var'Unds'49:SortBlockchainCell{},
                /* Fl Fn D Sfa */ Var'Unds'50:SortStateTrieCell{},
                /* Fl Fn D Sfa */ Var'Unds'51:SortDefaultGasPriceCell{},
                /* Fl Fn D Sfa */ Var'Unds'52:SortDefaultGasLimitCell{},
                /* Fl Fn D Sfa */ Var'Unds'53:SortTimeDiffCell{},
                /* Fl Fn D Sfa */ Var'Unds'54:SortTimeFreezeCell{},
                /* Fl Fn D Sfa */ Var'Unds'55:SortUnlimitedContractsCell{},
                /* Fl Fn D Sfa */ Var'Unds'56:SortAccountKeysCell{},
                /* Fl Fn D Sfa */ Var'Unds'57:SortNextFilterSlotCell{},
                /* Fl Fn D Sfa */ Var'Unds'58:SortTxReceiptsCell{},
                /* Fl Fn D Sfa */ Var'Unds'59:SortFiltersCell{},
                /* Fl Fn D Sfa */ Var'Unds'60:SortSnapshotsCell{},
                /* Fl Fn D Sfa */ Var'Unds'61:SortWeb3shutdownableCell{},
                /* Fl Fn D Sfa */ Var'Unds'62:SortWeb3notificationsCell{}
            ),
            /* Fl Fn D Sfa */ Var'Unds'65:SortRandomizerCell{}
        ),
        /* Fl Fn D Sfa */ Var'Unds'DotVar6:SortGeneratedCounterCell{}
    )
kore-exec: [108400777] Warning (WarnIfLowProductivity):
    Productivity dropped to: 76%
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/kframework/kore/issues

Update: this is still the output from the test, with the current commit on this PR

@ana-pantilie ana-pantilie marked this pull request as ready for review October 31, 2020 18:05
@ana-pantilie ana-pantilie changed the title Rule merger: better error messages Rule merger: bug fix and better error messages Oct 31, 2020
@ttuegel ttuegel requested a review from andreiburdusa November 2, 2020 15:10
@ana-pantilie ana-pantilie merged commit 5892a0e into runtimeverification:master Nov 6, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreiburdusa andreiburdusa andreiburdusa approved these changes

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

Successfully merging this pull request may close these issues.

Rule merger should identify duplicate rules in error message Rule merger breaks on KEVM
2 participants
@ana-pantilie @andreiburdusa