unexpected result of rule application

[kheradmand]

I have a the following (the irrelevant parts are omitted)

module P4-COMMON
    imports VALUE-SYNTAX
    imports HEADER-SYNTAX
  
    syntax P4Program ::= P4Declarations

   
    syntax P4Declarations ::= List{P4Declaration,""}  [klabel('P4Declarations)] 

    syntax P4Declaration ::=
                  HeaderTypeDeclaration

endmodule

module CONFIGURATION
imports P4-COMMON


syntax KItem ::= "@exec"
syntax Kitem ::= "@splitDeclarations" "(" P4Declarations ")" [function]

configuration
<T>
    <k>  $PGM:P4Program ~> @exec </k>

    <tables>
        <table multiplicity="*">
            .K
        </table>
    </tables>

    <headers>
        <header multiplicity="*">
            .K
        </header>
    </headers>

   
</T>


rule <k> (P:P4Declarations => @splitDeclarations(P)) ... </k> [structural]


rule <k> @splitDeclarations(((H:HeaderTypeDeclaration Rest:P4Declarations) => Rest)) ... </k>
        <headers>
            ...
            (.Bag => <header> H </header>)
            ...
        </headers>

//rule <k> (H:HeaderTypeDeclaration Rest:P4Declarations) => Rest ... </k> <headers> ... (.Bag => <header> H </header>) ... </headers>
//rule <k> (.P4Declarations => .) ... </k>

endmodule

for input

header_type ethernet_t {
    fields {
        dstAddr : 48;
    }
}

header_type y_t {
    fields {
        xx : 12;
    }
}

Using these two rules:

rule <k> (H:HeaderTypeDeclaration Rest:P4Declarations) => Rest ... </k> <headers> ... (.Bag => <header> H </header>) ... </headers>
rule <k> (.P4Declarations => .) ... </k>

I get the output that I want:

krun ../input --debug 
<T> <k> @exec </k> <tables> .TableCellBag </tables> <headers> <header> header_type y_t { fields { xx : 12 ;  .FieldDecs } } </header> <header> header_type ethernet_t { fields { dstAddr : 48 ;  .FieldDecs } } </header> </headers> <instances> . </instances> <parser> . </parser> </T>

But using the other two rules:

rule <k> (P:P4Declarations => @splitDeclarations(P)) ... </k> [structural]


rule <k> @splitDeclarations(((H:HeaderTypeDeclaration Rest:P4Declarations) => Rest)) ... </k>
        <headers>
            ...
            (.Bag => <header> H </header>)
            ...
        </headers>

I get some variables in the output (V0 and V1) which I didn't expect. Also it seems that it goes into an infinite loop (that is why I provided --depth 2)

krun ../input --debug --depth 2
<T> <k> @splitDeclarations ( V0 ) ~> @exec </k> <tables> .TableCellBag </tables> <headers> <header> V1 </header> </headers> <instances> . </instances> <parser> . </parser> </T>

What is the problem?

┆Issue is synchronized with this Asana task

[daejunpark]

@kheradmand The problem is due to the function attribute [function]. The rule for the functional term cannot mention other cells. So, a fix could be to either drop the function attribute or make the rule for @splitDeclarations not mention other cells.

That being said, kompile should have provided a warning or an error message.

[kheradmand]

@daejunpark Thanks Daejun. I just want mention that my problem was solved by dropping [function]. I don't know if you want to keep the issue open (for the kompile warning) or not.