java backend function not terminate when compile

[liyili2]

I find this set of rules:

     syntax ValueProp ::= Int  
                        | #ptr(SymLoc, Type)
                        | #struct(List, FieldInfo)
                        | #union(List, FieldInfo)

     syntax CProp ::= ValueProp | CId 
                    | "-" CProp
                    | "+" CProp
                    | "*" CProp
                    > CProp "[" CProp "]"
                    | CProp "." CId
                    | CProp "->" CId
                    > CProp "*" CProp [left]
                    | CProp "/" CProp [left]
                    > CProp "+" CProp [left]
                    | CProp "-" CProp [left]
                    > CProp "<" CProp [left]
                    | CProp "<=" CProp [left]
                    | CProp ">" CProp [left]
                    | CProp ">=" CProp [left]
                    > CProp "==" CProp [left]
                    | CProp "!=" CProp [left]

     syntax Prop ::= CProp | Bool | "__running" | "__error"

     syntax ValueProp ::= ltlRVal(Bag, Prop) [function]

     rule ltlRVal(B:Bag, - P:CProp) 
          => ltlRVal(B, 0 - ltlRVal(B, P))
     rule ltlRVal(B:Bag, L:CProp[R:CProp])
          => ltlRVal(B, * (L + R))
     rule ltlRVal(B:Bag, L:KLabel(P:CProp))
        => ltlRVal(B, L(ltlRVal(B, P)))
          when notBool (isValueProp(P:CProp) ==K true)
     rule ltlRVal(B:Bag, M:KLabel(L:CProp,, KL:KList))
        => ltlRVal(B, M(ltlRVal(B, L),, KL))
          when notBool (isValueProp(L:CProp) ==K true)
     rule ltlRVal(B:Bag, Lbl:KLabel(KL:KList,, R:CProp))
        => ltlRVal(B, Lbl(KL,, ltlRVal(B, R)))
          when notBool (isValueProp(R:CProp) ==K true)
               // Don't try resolving the field specifier.
               andBool (Lbl =/=KLabel '_._)
               andBool (Lbl =/=KLabel '_->_)

     rule ltlRVal(B:Bag, P:CProp -> X:CId)
          => ltlRVal(B, (* P) . X)
     rule ltlRVal(B:Bag, X:CId) => ltlRVal(B, * ltlLVal(B, X))

Any one of these rules will cause the compiling files not to terminate.

When we carefully look at this rules, we can found that there are two features of these rules:

1, ltlRVal function rewrite to some larger term as: "ltlRVal(B,T(R)) => ltlRVal(B,T(ltlRVal(B,R))"

2, the function rewrites some terms to some other terms with prefix operators which have similar infix operators associative with them, such as: "rule ltlRVal(B:Bag, - P:CProp) => ltlRVal(B, 0 - ltlRVal(B, P))"

[yilongli]

If you can create a small example and put it in a complete module, I can try to figure out what's wrong.

[liyili2]

Yes. I have already come up with a smallest set of definitions which will cause the non-termination:

module C-LTLMC
     syntax CId ::= Identifier(String) [klabel('Identifier)] // new

     syntax Expression ::= "*" K
     syntax Expression ::= CId
     syntax C ::= Attribute(String, K) [klabel('Attribute)]

     syntax FieldInfo ::= fieldInfo(List, Map, Map)

     // Ltl atomic propositions.
     syntax ValueProp ::= Int  

     syntax CProp ::= ValueProp | CId 
                    | "*" CProp

     syntax Prop ::= CProp 

     syntax ValueProp ::= ltlRVal(Bag, Prop) [function]

     rule ltlRVal(B:Bag, X:CId) => ltlRVal(B, * ltlLVal(B, X))
     // Not so interested in l-values.
     syntax ValueProp ::= ltlLVal(Bag, CId) [function]

endmodule

This is actually one of the smallest set. I think for the other rules of ltlRVal I mentioned above, there are other smallest sets of rules which will cause the same non-termination.

[liyili2]

A funny thing is that if I remove the code: syntax C ::= Attribute(String, K) [klabel('Attribute)], it will compile successfully.

[radumereuta]

From the "did you know category": C ::= Attribute(String, K) automatically ads the klabel attribute with the value 'Attribute (the name of the function. But if you write it like: C ::= "Attribute" "(" String "," K ")" Then the klabel would contain the parenthesis too: 'Attribute(`,) So in your definition, the klabel attribute is redundant.

[grosu]

Liyi, can you please check whether this is explained in the manual-to-be, and if not, add it there? This is something that definitely needs to be discussed there.

[liyili2]

I search both c-semantics and k-unified-builtins. There is file whose name is manual-to-be. I think you mean the readme file in c semantics. I think there is something for saying "cat" format, but there is no something for describing this problem.

I can add it.

[grosu]

Daejun, can you please let Liyi know where it is? Is it still under k/documentation, or it is now a wiki? It should be in only one place and I am afraid it may be in two different places right now, which is bad. This file will eventually become the K manual.

[liyili2]

Now, I do more tests and found that these two sets of rules will not terminated also:

module C-LTLMC
     //imports C-SYNTAX

     syntax C ::= TypeSpecifier

     syntax TypeSpecifier ::= TAtomic(K, K)
          [klabel('TAtomic)]
     syntax Expression ::= "-" K [prec(22)]
                         | "+" K [prec(22)]
                         | "!" K [prec(22)]
                         | "~" K [prec(22)]
                         | "*" K [prec(22)]
                         | "&" K [strict, prec(22)]

     syntax CId ::= "#NoName" // new
     syntax C ::= CId
     syntax Expression ::= CId
     syntax Bits ::= Int
     syntax SymLoc ::= "NullPointer"
     syntax SymBase ::= string(String)
     syntax CSize ::= Int
     syntax CValue ::= CSize
     syntax Statement ::= "loopMarked"
     syntax Type ::= type(K) [function]
     syntax FieldInfo ::= fieldInfo(List, Map, Map)
     // Ltl atomic propositions.
     syntax ValueProp ::= Int  
                        | #ptr(SymLoc, Type)
                        | #struct(List, FieldInfo)
                        | #union(List, FieldInfo)

     syntax CProp ::= ValueProp | CId 
                    | "-" CProp
                    | "+" CProp
                    | "*" CProp
                    > CProp "[" CProp "]"
                    > CProp "+" CProp [left]
                    | CProp "-" CProp [left]

     syntax Prop ::= CProp

     syntax ValueProp ::= ltlRVal(Bag, Prop) [function]

     rule ltlRVal(_, V:ValueProp) => V

     rule ltlRVal(B:Bag, - P:CProp) 
          => ltlRVal(B, 0 - ltlRVal(B, P))

     rule ltlRVal(B:Bag, + P:CProp) 
          => ltlRVal(B, P)

     rule ltlRVal(B:Bag, L:CProp[R:CProp])
          => ltlRVal(B, * (L + R))

     rule ltlRVal(B:Bag, X:CId) => ltlRVal(B, * ltlLVal(B, X))

     // Not so interested in l-values.
     syntax ValueProp ::= ltlLVal(Bag, CId) [function]
     syntax ValueProp ::= "ltlLVal'" "(" Bag "," String ")" [function]

endmodule

module C-LTLMC

     syntax C ::= AttributeWrapper(K, K) [klabel('AttributeWrapper)]

     syntax Expression ::= "-" K [prec(22)]
                         | "+" K [prec(22)]
                         | "!" K [prec(22)]
                         | "~" K [prec(22)]
                         | "*" K [prec(22)]
                         | "&" K [strict, prec(22)]

     syntax CId ::= "#NoName" // new
     syntax C ::= CId
     syntax Expression ::= CId
     syntax Bits ::= Int
     syntax SymLoc ::= "NullPointer"
     syntax SymBase ::= string(String)
     syntax CSize ::= Int
     syntax CValue ::= CSize
     syntax Statement ::= "loopMarked"
     syntax Type ::= type(K) [function]
     syntax FieldInfo ::= fieldInfo(List, Map, Map)
     // Ltl atomic propositions.
     syntax ValueProp ::= Int  
                        | #ptr(SymLoc, Type)
                        | #struct(List, FieldInfo)
                        | #union(List, FieldInfo)

     syntax CProp ::= ValueProp | CId 
                    | "-" CProp
                    | "+" CProp
                    | "*" CProp
                    > CProp "[" CProp "]"
                    > CProp "+" CProp [left]
                    | CProp "-" CProp [left]

     syntax Prop ::= CProp

     syntax ValueProp ::= ltlRVal(Bag, Prop) [function]

     rule ltlRVal(_, V:ValueProp) => V

     rule ltlRVal(B:Bag, - P:CProp) 
          => ltlRVal(B, 0 - ltlRVal(B, P))

     rule ltlRVal(B:Bag, + P:CProp) 
          => ltlRVal(B, P)

     rule ltlRVal(B:Bag, L:CProp[R:CProp])
          => ltlRVal(B, * (L + R))

     rule ltlRVal(B:Bag, X:CId) => ltlRVal(B, * ltlLVal(B, X))

     // Not so interested in l-values.
     syntax ValueProp ::= ltlLVal(Bag, CId) [function]
     syntax ValueProp ::= "ltlLVal'" "(" Bag "," String ")" [function]

endmodule

[liyili2]

The similarity between these two sets of rules is that if I remove the syntax C ::= SomeName(K,K), the sets of rules can be compiled. However, if I need anything like the sytanx declaration above, the kompile in java backend will result in non-termination.

[yilongli]

The problem is that the following function rule will be expanded infinitely in the partial evaluation phase during kompilation: rule ltlRVal(B:Bag, X:CId) => ltlRVal(B, * ltlLVal(B, X))

To be more specific, KItem * ltlLVal(B, X) is incorrectly(?) sorted as CId instead of CProp. The sort of * ltlLVal(B, X) is computed as follows in the Java backend:

1. find productions that match this KItem, that is, syntax Expression ::= "*" K and syntax CProp ::= "*" Prop;
2. then take the GLB of sorts of these productions, so getGLB(Expression, CProp) becomes CId.

If you write such subsort relation in Maude, you will fail the preregularity check. I am not sure how to detect this problem properly in the Java backend.

For now, a quick fix would be to subsort CProp to Expression.

[liyili2]

Not that easy. This is just one of the candidate of causing problems. Now, I am trying to come up with another set of rules which will delete the ltlLVal function completely and it still does not terminate.

[yilongli]

What do you mean by saying that it is just one of the problems? What are the other problems?

[liyili2]

I mean if I delete "ltlLVal" in c semantics, it will still be non-terminated because of some other rules in ltlmc.

[liyili2]

I mean this problem happens in ltlmc file only which is the ltl model checker of the c semantics, and it does not relate to any semantics issue of c. It means that we can run c program without it. So I am trying to identify all problems here in order for you to fully understand and fix the problem properly.

[liyili2]

This is another set of rules which will cause non-termination by using java backend, which is without "ltlLVal" function. This set even does not have "Attribute" operators declared as sort "C".

The maude backend can successfully compile this file. It is very hard to fine in c semantics. A set of expression operators is declared in one file, and the two marcos that are related to this set of operators, and then a set of similar operators is defined in LTLMC module. Usually, without running the whole c semantics, we cannot observe this non-termination.

module C-SYNTAX

     syntax C ::= CId
     syntax CId ::= "#NoName" // new
     syntax Expression ::= "*" K [prec(22)]
                         > K "+" K [prec(33), left]
     syntax Expression ::= CId

     syntax Expression ::= K "[" K "]"
     syntax Expression ::= K "." CId
     syntax Expression ::= K "->" CId

     rule K:K -> F:CId => (* K) . F [macro, structural]
     rule E1:K[E2:K] => *(E1 + E2) 
          [macro, structural]
endmodule

module C-LTLMC
     imports C-SYNTAX
     syntax ValueProp ::= Int  

     syntax CProp ::= ValueProp | CId 
                    | "*" CProp
                    > CProp "[" CProp "]"
                    | CProp "." CId
                    | CProp "->" CId
                    > CProp "+" CProp [left]

     syntax Prop ::= CProp 

     syntax ValueProp ::= ltlRVal(Bag, Prop) [function]

     rule ltlRVal(_, V:ValueProp) => V

     rule ltlRVal(B:Bag, L:CProp[R:CProp])
          => ltlRVal(B, * (L + R))
endmodule

[liyili2]

I think the set of rules I mentioned above is essentially different from the other sets of rules. I think we should refer to this set as non-termination due to macros, and the other sets are non-termination due to sorts.

[yilongli]

For this example, the following two rules together result in infinite unrolling of the RHS of the first rule during partial evaluation: rule ltlRVal(B:Bag, L:CProp[R:CProp]) => ltlRVal(B, * (L + R)) rule E1:K[E2:K] => *(E1 + E2) [macro, structural]

@dwightguth we should probably implement some check in the macro expansion phase and partial evaluation phase in KILtoBackendKILTransformer to throw an error if a rule is unrolled too many times. I don't have any specific idea on how to do this right now. Anyway, I am handing this over to you. Thanks a lot.

[liyili2]

Why it will cause infinite unrolling? i do not understand.

From rewriting logic, if you have a function f, and f(a) => f(b), while a => b, either. Why there is an infinite rewriting here? These two rules are even confluent. You can say it is redundunt, but I cannot see why it is non-terminating here.

I think that is why maude backend can allow this file to be compiled.

[yilongli]

As I said ealier, it is because the Java backend attempts to perform partial evaluation on the RHS of a function rule as much as possible.

[liyili2]

Oh, ok. Can you tell me what is the partial evaluation output for these two rules here.

[liyili2]

Would you mind to give me one or two steps rewriting here.

I mean I am very surprised that your partial evaluation cannot deal with this problem while Maude can deal with it. Then, I guess once we merge AC matching in K, the partial evaluation algorithm will need to be rewritten completely in this case.

For equation rewriting, why not just borrow ideas from Maude, since equation rewriting is very fast in Maude (Maude backend is slow because it uses a lot of rule rewriting, and rule rewriting is very slow). If we want to forget about AC matching now; why not borrow ideas from ML language such as Ocaml, since rewriting logic without AC matching is just functional programming and ML language is basically the fastest programming language in general.

[dwightguth]

Liyi: the problem here is that macros in maude simply do not do what we want. We would like in the long run to say that a macro rule means that the left and right hand terms should be treated as equivalent. So when you say: rule E1:K[E2:K] => *(E1 + E2) [macro, structural]

It means that the rule rule ltlRVal(B:Bag, L:CProp[R:CProp]) => ltlRVal(B, * (L + R))

should be treated identically to the rule rule ltlRVal(B:Bag, * (L:CProp + R:CProp)) => ltlRVal(B, * (L + R)) because that is the macro-expanded version of the rule.

Note that this rule is rewriting a term to itself. That is why kompile does not terminate. The correct solution is to delete the rule rule ltlRVal(B:Bag, L:CProp[R:CProp]) => ltlRVal(B, * (L + R)) from your semantics.

I am assigning this task back to Yilong because it is not blocking you, and he can get to it when he has some time after the deliverable.

[liyili2]

Yes, I cannot see what is the differences between Maude and K in this concept. First, I think the equivalent rules of the macros in K are equations. Second, they treat equations as building equivalent equations between LHS and RHS, and they actually prove that by any rewriting orders of equations, the result should be eventually the same.

What I mean is that if macros are introducing equivalent relations among terms, since they are equivalent, why not just pick one. If any order of rewriting is acceptable, why not just pick one path. I think it is enough, since when users write macros, they assume that LHS and RHS are equivalent, and we only need to care about one of them.

[liyili2]

What I propose is that we can learn the equation rewriting in Maude, and assume that the users always write confluent and terminating macros and functions, and use only one path of evaluation orders to do the rewriting and we do not need to care about all rewriting orders for macros and functions, since users cannot actually see the evaluations of macros and functions.

[dwightguth]

I am closing this. The intuition of macros is that they are macros, i.e. statically applied before rewriting. The rule is therefore not a "order of rewriting" but a term rewriting to itself. I don't know how to be any clearer.

[liyili2]

@dwightguth, why do you want to close this. We have not yet solved the problem. There are two troubles here to cause the non-termination.

[dwightguth]

I will hold this open while we discuss this issue. Please find me tomorrow so I can explain what you need to do.

[dwightguth]

You should now get a good error message showing the trace of function calls that terminate. Please give this a try to resolve the nontermination bugs that you see. I am closing this, but feel free to come find me if you need help figuring out how to fix the underlying issues.

Fixed #641

[liyili2]

Good.