Crash on `checkSubstitutionCoverage`

kheradmand commented 3 years ago

Version

RV-K version 1.0-SNAPSHOT
Git revision: 
Git branch: UNKNOWN_BRANCH
Build date: Thu Mar 25 04:00:09 IRDT 2021

Module

module TEST-SYNTAX
imports ID
        syntax ControlFunctionDeclaration ::= "control" Id ControlBlock
        syntax ControlBlock ::= "{" ControlStatements "}"
        syntax ControlStatements ::= List{ControlStatement,""} [klabel(controlStatements)]
        syntax ControlStatement ::=
                      ApplyTableCall
                    | IfElseStatement

        syntax ApplyTableCall ::= "apply" "(" TableName ")" ";"

        syntax IfElseStatement ::=
              "if" "(" BoolExpr ")" ControlBlock
            | "if" "(" BoolExpr ")" ControlBlock ElseBlock

        syntax ElseBlock ::= "else" ControlBlock | "else" IfElseStatement

        syntax BoolExpr ::= Bool

        syntax TableName ::= Id
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX
       configuration
           <k> @evalStatements($PGM:ControlStatements) </k>
           <ts> .List </ts>

       syntax KItem ::= "@evalStatements" "(" ControlStatements ")" | "@evalStatement" "(" ControlStatement ")"

       rule @evalStatements(S:ControlStatement Rest:ControlStatements) => @evalStatement(S) ~> @evalStatements(Rest)
       rule @evalStatements(.ControlStatements) => .K
       rule @evalStatement(S) => S

       rule if ( B:BoolExpr ) C:ControlBlock Rest:ControlStatements => if ( B ) C else { .ControlStatements } Rest  [macro]
       rule if (true) {C1} else {_} => @evalStatements(C1)

       syntax KResult ::= Bool

endmodule

intput.test

if (true){
    apply (t);
}

Steps:

$ kompile --backend haskell test.k --syntax-module TEST-SYNTAX --main-module TEST
$ krun input.test
kore-exec: [475835] Error (ErrorRewritesInstantiation):
    While rewriting the configuration:
        \and{SortGeneratedTopCell{}}(
            /* term: */
            /* Fl Fn D Sfa Cl */
            Lbl'-LT-'generatedTop'-GT-'{}(
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'k'-GT-'{}(
                    /* Fl Fn D Sfa Cl */
                    kseq{}(
                        /* Fl Fn D Sfa Cl */
                        Lbl'-AT-'evalStatements'LParUndsRParUnds'TEST'Unds'KItem'Unds'ControlStatements{}(
                            /* Fl Fn D Sfa Cl */
                            Lbl'Stop'List'LBraQuotUndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements'QuotRBraUnds'ControlStatements{}()
                        ),
                        /* Fl Fn D Sfa Cl */ dotk{}()
                    )
                ),
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'generatedCounter'-GT-'{}(
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                ),
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'ts'-GT-'{}(
                    /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
                )
            ),
        \and{SortGeneratedTopCell{}}(
            /* predicate: */
            /* Sfa */
            \equals{SortControlStatements{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa Cl */
                Lbl'Stop'List'LBraQuotUndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements'QuotRBraUnds'ControlStatements{}(),
                /* Fl Fn D Sfa */
                Lbl'UndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements{}(
                    /* Fl Fn D Sfa Cli */
                    /* Inj: */ inj{SortApplyTableCall{}, SortControlStatement{}}(
                        /* Fl Fn D Sfa Cl */
                        Lblapply'LParUndsRParSClnUnds'TEST-SYNTAX'Unds'ApplyTableCall'Unds'TableName{}(
                            /* Fl Fn D Sfa Cli */
                            /* Inj: */ inj{SortId{}, SortTableName{}}(
                                /* Fl Fn D Sfa Cl */
                                \dv{SortId{}}(/* Fl Fn D Sfa Cl */ "t")
                            )
                        )
                    ),
                    /* Fl Fn D Sfa Cl */
                    Lbl'Stop'List'LBraQuotUndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements'QuotRBraUnds'ControlStatements{}()
                )
            ),
            /* substitution: */
            \top{SortGeneratedTopCell{}}()
        ))
    Unable to instantiate semantic rule at /Users/ali/FSL/p4-semantics/debug/./test16.k:36:13-36:117
    Unification did not find a solution for the variables:
        RuleVarRest RuleVarS
    The unification solution was:
    \and{SortGeneratedTopCell{}}(
        /* term: */
        /* Spa */
        \rewrites{SortGeneratedTopCell{}}(
            /* Spa */
            \and{SortGeneratedTopCell{}}(
                /* D Sfa */ \top{SortGeneratedTopCell{}}(),
                /* Fl Fn D Sfa */
                Lbl'-LT-'generatedTop'-GT-'{}(
                    /* Fl Fn D Sfa */
                    Lbl'-LT-'k'-GT-'{}(
                        /* Fl Fn D Sfa */
                        kseq{}(
                            /* Fl Fn D Sfa */
                            Lbl'-AT-'evalStatements'LParUndsRParUnds'TEST'Unds'KItem'Unds'ControlStatements{}(
                                /* Fl Fn D Sfa */
                                Lbl'UndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements{}(
                                    /* Fl Fn D Sfa */
                                    RuleVarS:SortControlStatement{},
                                    /* Fl Fn D Sfa */
                                    RuleVarRest:SortControlStatements{}
                                )
                            ),
                            /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
                        )
                    ),
                    /* Fl Fn D Sfa */ RuleVar'Unds'0:SortGeneratedCounterCell{},
                    /* Fl Fn D Sfa */ RuleVar'Unds'1:SortTsCell{}
                )
            ),
            /* Fl Fn D Spa */
            Lbl'-LT-'generatedTop'-GT-'{}(
                /* Fl Fn D Spa */
                Lbl'-LT-'k'-GT-'{}(
                    /* Fl Fn D Spa */
                    kseq{}(
                        /* Fl Fn D Spa */
                        Lbl'-AT-'evalStatement'LParUndsRParUnds'TEST'Unds'KItem'Unds'ControlStatement{}(
                            /* Fl Fn D Sfa */ RuleVarS:SortControlStatement{}
                        ),
                        /* Fl Fn D Spa */
                        kseq{}(
                            /* Fl Fn D Spa */
                            Lbl'-AT-'evalStatements'LParUndsRParUnds'TEST'Unds'KItem'Unds'ControlStatements{}(
                                /* Fl Fn D Sfa */
                                RuleVarRest:SortControlStatements{}
                            ),
                            /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
                        )
                    )
                ),
                /* Fl Fn D Sfa */ RuleVar'Unds'0:SortGeneratedCounterCell{},
                /* Fl Fn D Sfa */ RuleVar'Unds'1:SortTsCell{}
            )
        ),
    \and{SortGeneratedTopCell{}}(
        /* predicate: */
        /* Sfa */
        \equals{SortControlStatements{}, SortGeneratedTopCell{}}(
            /* Fl Fn D Sfa Cl */
            Lbl'Stop'List'LBraQuotUndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements'QuotRBraUnds'ControlStatements{}(),
            /* Fl Fn D Sfa */
            Lbl'UndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements{}(
                /* Fl Fn D Sfa */ RuleVarS:SortControlStatement{},
                /* Fl Fn D Sfa */ RuleVarRest:SortControlStatements{}
            )
        ),
        /* substitution: */
        \and{SortGeneratedTopCell{}}(
            /* Spa */
            \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa */ RuleVar'Unds'0:SortGeneratedCounterCell{},
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'generatedCounter'-GT-'{}(
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                )
            ),
        \and{SortGeneratedTopCell{}}(
            /* Spa */
            \equals{SortTsCell{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa */ RuleVar'Unds'1:SortTsCell{},
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'ts'-GT-'{}(
                    /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
                )
            ),
            /* Spa */
            \equals{SortK{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{},
                /* Fl Fn D Sfa Cl */ dotk{}()
            )
        ))
    ))
    Error! Please report this.
    CallStack (from HasCallStack):
      checkSubstitutionCoverage, called at src/Kore/Step/RewriteStep.hs:201:9 in kore-0.42.0.0-4oagSTEx51qJzsWiO2fwIO:Kore.Step.RewriteStep
Created bug report: kore-exec.tar.gz
[Error] Critical: Backend crashed during rewriting with exit code 1

kore-exec.tar.gz

kheradmand commented 3 years ago

The problem may be related to kframework/k#1950 because there is a similar unexpected non-determinism a few steps before the crash. In addition, when I remove rule if ( B:BoolExpr ) C:ControlBlock Rest:ControlStatements => if ( B ) C else { .ControlStatements } Rest [macro], there is no crash.

ttuegel commented 3 years ago

It is very suspicious that the symbol Lbl'UndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements{} is not a constructor.

ttuegel commented 3 years ago

I confirmed my suspicion: Lbl'UndsUndsUnds'TEST-SYNTAX'Unds'ControlStatements'Unds'ControlStatement'Unds'ControlStatements is given the macro attribute and so not given the constructor attribute. I'm sending this back to the frontend.

ehildenb commented 3 years ago

@kheradmand actually, I think you may be able to fix this pretty simply by just changing the macro rule to not use the list-concat symbol as well.

       rule if ( B:BoolExpr ) C:ControlBlock => if ( B ) C else { .ControlStatements }  [macro]

Notice how Rest is removed.

kheradmand commented 3 years ago

@ehildenb Thanks! Using your suggestion does prevent the crash (I also prevented it by removing the macro). However I opened this issue due to the crash itself (per the crash message).

I'm not sure if the crash is due to an internal problem or a user error. In any case, a more informative warning or error message would be nice as there was no easy way (that I know) to find out that the crash was due to using this macro (took about two full weeks of trial and error in a moderately sized definition to pinpoint it). Once it was pinpointed, the "fix" was easy.

ttuegel commented 3 years ago

I'm not sure if the crash is due to an internal problem or a user error.

It is due to user error. The root cause is that requiring the macro attribute on the rule allows for this kind of "action at a distance". The frontend should make it hard to do this by accident, by requiring the macro attribute on the syntax.

ehildenb commented 1 year ago

The frontend now correctly outputs a warning:

% kompile --backend haskell test.k
[Warning] Compiler: The attribute [macro] has been deprecated on rules. Use
this label on syntax declarations instead.
        Source(/home/dev/src/k/test.k)
        Location(37,13,37,115)
        37 |           rule if ( B:BoolExpr ) C:ControlBlock Rest:ControlStatements => if
( B ) C else { .ControlStatements } Rest  [macro]
           .               
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

And krun still crashes as expected. The following definition works:

module TEST-SYNTAX
imports ID
imports BOOL
        syntax ControlFunctionDeclaration ::= "control" Id ControlBlock
        syntax ControlBlock ::= "{" ControlStatements "}"
        syntax ControlStatements ::= List{ControlStatement,""} [klabel(controlStatements)]
        syntax ControlStatement ::=
                      ApplyTableCall
                    | IfElseStatement

        syntax ApplyTableCall ::= "apply" "(" TableName ")" ";"

        syntax IfElseStatement ::=
              "if" "(" BoolExpr ")" ControlBlock [macro] 
            | "if" "(" BoolExpr ")" ControlBlock ElseBlock

        syntax ElseBlock ::= "else" ControlBlock | "else" IfElseStatement

        syntax BoolExpr ::= Bool

        syntax TableName ::= Id
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX
       configuration
           <k> @evalStatements($PGM:ControlStatements) </k>
           <ts> .List </ts>

       syntax KItem ::= "@evalStatements" "(" ControlStatements ")" | "@evalStatement" "(" ControlStatement ")"

       rule @evalStatements(S:ControlStatement Rest:ControlStatements) => @evalStatement(S) ~> @evalStatements(Rest)
       rule @evalStatements(.ControlStatements) => .K
       rule @evalStatement(S) => S

       rule if ( B:BoolExpr ) C:ControlBlock => if ( B ) C else { .ControlStatements }
       rule if (true) {C1} else {_} => @evalStatements(C1)

       syntax KResult ::= Bool

endmodule

You get:

% kompile --backend haskell test.k

% krun input.test                 
<generatedTop>
  <k>
    apply ( t ) ; ~> @evalStatements ( .ControlStatements ) ~> @evalStatements ( .ControlStatements ) ~> .
  </k>
  <ts>
    .List
  </ts>
</generatedTop>

Note the changes I had to make to the definition:

Add imports BOOL to TEST-SYNTAX.
Move the macro symbol to the if(_){_} production.
Modify the macro rule to not have the variable REST, which is not under the macro production.

Closing this as resolved, as the frontend is correctly reporting the problem to the user now.

runtimeverification / k

Crash on `checkSubstitutionCoverage` #1956