Variables of type KList break krun

[radumereuta]

I've been working on trying to disambiguate C, and I need a few tools for that. One of them is a visitor that can traverse the entire AST resulted after parsing.

I've been trying to revive the visitors built by @traiansf in K3.6, but K4 has a bad 'habit' of crashing with java.lang.ClassCastException.

Here is a small example:

module TEST
  configuration <k> isValid($PGM:Int) </k>
  syntax KBott ::= isValid(K)
                 | validKL(KList)
    rule isValid(KL:KLabel(KLs:KList)) => KL(isValidKL(KLs))
endmodule

Usage: kompile test.k | krun a.test a.test contains: 1 Error:

java.lang.ClassCastException: org.kframework.backend.java.kil.Variable cannot be cast to org.kframework.backend.java.kil.KList
        at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:87)
        at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117)
        at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291)
        at java.util.stream.ReferencePipeline$3$1.accept(Unknown Source)
        at java.util.Iterator.forEachRemaining(Unknown Source)
...

kompile --version
K framework version 4.0.1-SNAPSHOT
Git revision: 7f2704e
Git branch: master
Build date: Mon Mar 27 14:38:05 EEST 2017

My question is: why am I getting this error here? Can we do something to improve error messages? In this case, I had to run the example in IntelliJ debug mode and stop exactly at the exception to get at least a location information (it crashes around variables of type KList).

@dlucanu have I left something out from this example?

[lucaspena]

Hi Radu,

You are receiving this error because you're trying to match on a KLabel, which unfortunately is not supported in the current version of K, as we do not support meta-level reasoning within K.

The error message is unintuitive because we are not expecting users to attempt such meta-level reasoning. We will work on providing better error messages in the future.

On Wed, Mar 29, 2017 at 6:19 AM, Radu Mereuta [email protected] wrote:

I've been working on trying to disambiguate C, and I need a few tools for that. One of them is a visitor that can traverse the entire AST resulted after parsing.

I've been trying to revive the visitors built by @traiansf https://github.com/traiansf in K3.6, but K4 has a bad 'habit' of crashing with java.lang.ClassCastException.

Here is a small example:

module TEST configuration isValid($PGM:Int) syntax KBott ::= isValid(K) | validKL(KList) rule isValid(KL:KLabel(KLs:KList)) => KL(isValidKL(KLs)) endmodule

Usage: kompile test.k | krun a.test a.test contains: 1 Error:

java.lang.ClassCastException: org.kframework.backend.java.kil.Variable cannot be cast to org.kframework.backend.java.kil.KList at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:87) at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117) at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291) at java.util.stream.ReferencePipeline$3$1.accept(Unknown Source) at java.util.Iterator.forEachRemaining(Unknown Source) ...

kompile --version K framework version 4.0.1-SNAPSHOT Git revision: 7f2704e Git branch: master Build date: Mon Mar 27 14:38:05 EEST 2017

My question is: why am I getting this error here? Can we do something to improve error messages? In this case, I had to run the example in IntelliJ debug mode and stop exactly at the exception to get at least a location information (it crashes around variables of type KList).

@dlucanu https://github.com/dlucanu have I left something out from this example?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/kframework/k/issues/2293, or mute the thread https://github.com/notifications/unsubscribe-auth/AD1ZLkLFl96bvY0rxHx1WIbtZUuleinMks5rqj5egaJpZM4Ms12s .

-- Lucas Peña University of Illinois at Urbana-Champaign [email protected] (954) 882-7070

[dlucanu]

This is a bit unexpected for me. I know that KLabel is replaced with Symbol (or something like that) in the new ML approach, but I expect the user to have access to the AST representation. It should be a way to write generic rules on ASTs, otherwise a rule like rule isValid(KL:KLabel(KLs:KList)) => KL(isValidKL(KLs)) has to be implemented/replaced with several thousands of rules for a language definition like C or Java. What solution do you recommend for such situations?

[lucaspena]

Unfortunately, there is no good solution for this right now. As you mentioned, K is going through some structural changes right now, and there is a lot that still needs to be done. Having such meta-level reasoning will be very useful, and it is something we are working towards adding in the future (hopefully sooner rather than later).

Specifically, here's one idea for an implementation of meta-level for your original example:

module TEST configuration isValid($PGM:Int) syntax MetaTerm ::= isValid(K) | isvalidKL(KList) rule isValid( [[ KL:KLabel(KLs:KList) ]] ) => [[ KL(isValidKL(KLs)) ]] endmodule

The double bracket would just be syntactic sugar for the construct downTerm which we will make available at the K-level. What this means is that if you have isValid(foo) in a particular program, foo will first be "upped" in order to match the rule, then the result will be "downed" on the right-hand side of the rule.

This is just one idea for a cleaner meta-level implementation we are working towards, which would nicely separate meta-level vs object level in K. Let us know if you have any ideas or suggestions for this. Also, let us know if this is a feature you need implemented immediately.

Hope this cleared things up.

On Thu, Mar 30, 2017 at 12:19 AM, Dorel Lucanu [email protected] wrote:

This is a bit unexpected for me. I know that KLabel is replaced with Symbol (or something like that) in the new ML approach, but I expect the user to have access to the AST representation. It should be a way to write generic rules on ASTs, otherwise a rule like rule isValid(KL:KLabel(KLs:KList)) => KL(isValidKL(KLs)) has to be implemented/replaced with several thousands of rules for a language definition like C or Java. What solution do you recommend for such situations?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/kframework/k/issues/2293#issuecomment-290305163, or mute the thread https://github.com/notifications/unsubscribe-auth/AD1ZLsT7g5jkciblYjc1KkOMVoqt1UZFks5rqztlgaJpZM4Ms12s .

-- Lucas Peña University of Illinois at Urbana-Champaign [email protected] (954) 882-7070

[radumereuta]

Actually, having access to the meta level would work even better. I'm not sure what is the status of that. Do you have some documentation and examples?

[dlucanu]

Thank you very much for the detailed explanations. In the new ML-based approach does it make sense to clearly separate object level and metalevel. The only thing not clear for me is whether do you intend to use the double bracket syntax or explicit functions #downTerm() and #upTerm() (as in Maude). Now the use of double brackets is confusing since its meaning in the lhs of the rule is different from that in the rhs.

YES, it is critical and urgent for us to have this feature. For the beginning a implementation that works on examples like above is fine for us. Thank you very much.