search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

A bug in java backend to recognize the sort of variables #549

Closed liyili2 closed 9 years ago

liyili2 commented 10 years ago

I find that if we put different shapes of variables, the java backend will give you different results for the same things. For example

module TEST

  syntax K ::= aset(Set)
  rule aset(A (.Set => SetItem(0)))
endmodule

The java backend will say: [Error] Critical: Could not infer a unique sort for variable 'A'. Possible sorts: KLabel, Set File: /home/qangel/project/k-unified/bin/test.k Location: (4,3,4,35)

For this file:

module TEST

  syntax K ::= aset(Set)
  rule aset(_:Set (.Set => SetItem(0)))
endmodule

Java backend will kompile it finely.

For the file:

module TEST

  syntax K ::= aset(Set)
  rule aset(_ (.Set => Set))
endmodule

Java backend will put out this error: Exception in thread "main" java.lang.AssertionError: unexpected kind KItem for frame variable GeneratedFreshVar358; expected kind KList at org.kframework.backend.java.kil.Collection.(Collection.java:38) at org.kframework.backend.java.kil.KCollection.(KCollection.java:63) at org.kframework.backend.java.kil.KList.(KList.java:49) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:164) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.KApp.accept(KApp.java:175) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:256) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.KList.accept(KList.java:52) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:161) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.KApp.accept(KApp.java:175) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:171) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.KItemProjection.accept(KItemProjection.java:70) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:236) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.KSequence.accept(KSequence.java:46) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:275) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.Cell.accept(Cell.java:287) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:321) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.Bag.accept(Bag.java:69) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:265) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.Cell.accept(Cell.java:287) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:567) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.Rule.accept(Rule.java:72) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:690) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:76) at org.kframework.kil.Definition.accept(Definition.java:185) at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92) at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.transformDefinition(KILtoBackendJavaKILTransformer.java:103) at org.kframework.backend.java.symbolic.JavaSymbolicBackend.lastStep(JavaSymbolicBackend.java:65) at org.kframework.main.LastStep.compile(LastStep.java:22) at org.kframework.main.LastStep.compile(LastStep.java:11) at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:44) at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:192) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:161) at org.kframework.kompile.KompileFrontEnd.main(KompileFrontEnd.java:72) at org.kframework.main.Main.main(Main.java:49)

bmmoore commented 10 years ago

I also see an exception like Exception in thread "main" java.lang.AssertionError: unexpected kind KItem for frame variable when compiling for the java backend on the untyped-builtins2 branch

It's from the "isVaList(P)" term in this rule in my partially updated CIL semantics (which compiles fine with the Maude backend on the untyped-builtins2 branch).

rule *tv(T:Type, P:Ptr) => lv(downPtr(T), P) when isVaList(P) =/=K true

isVaList is the automatically generated sort predicate for this sort:

syntax VaList ::= "va_list" "(" TypedValues ")"

catching it in the debugger, "isVaList(P)" is a KApp of the KLabelConstant isVarList directly to a Variable P:Ptr, while the KILtoBackendJava visitor tries to do this on the child of any KApp:

    if (kList instanceof Variable) {
        kList = new KList((Variable) kList);
    }
bmmoore commented 10 years ago

It looks like this affects functions called with single non-KList variables.

bmmoore commented 10 years ago

Should the code be more like this? I don't know what invariants you try to keep in the KIL classes, but my file finishes compiling if I change the if to this:

    if (kList instanceof Variable) {
        if (kList.sort() == "KList") {
            kList = new KList((Variable)kList);
        } else {
            kList = new KList(ImmutableList.of(kList));
        }
    }
yilongli commented 10 years ago

@bmmoore Your suggestion makes sense to me, but it probably requires more effort to resolve this problem completely. I will take a closer look when I get a chance.

dwightguth commented 10 years ago

We need to fix this bug in order to be able to port the CIL semantics which is needed for our deliverable. Can you please make sure that this is a priority for you, @yilongli ?

yilongli commented 10 years ago

@dwightguth OK, I will try to fix it this afternoon.

dwightguth commented 10 years ago

Actually, no, I take it back. This is actually a parsing bug.

If I write:

P:Ptr ~> Kl:KLabel(P)

The ASTNode it creates should have a KList between the KApp and the Variable. However, it only does this if I type P both places.

I am reassigning this to @radumereuta for him to fix.

yilongli commented 10 years ago

What do you mean by "it only does this if I type P both places"?

yilongli commented 10 years ago

This is an failure-inducing example I isolated from the CIL semantics:

module TEST
  syntax Ptr ::= "foo"

  rule P:Ptr => . when isKResult(P)
endmodule
dwightguth commented 10 years ago

Yilong: the issue is that at SDF time, the parser does not know whether the P inside isKResult is a KList variable or not, so it doesn't inject a KList constructor. However, it also does not add the correct injection later, causing the code to fail because the AST produced by the parser is malformed. This is a bug in the kompile frontend, which is why I assigned it to Radu. You can work with him on it if you want, but the bug is no longer assigned to you. On Jun 12, 2014 12:07 PM, "Yilong Li" notifications@github.com wrote:

This is an failure-inducing example I isolated from the CIL semantics:

module TEST syntax Ptr ::= "foo"

rule P:Ptr => . when isKResult(P) endmodule

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/549#issuecomment-45919776.