kframework / k-legacy

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

the rule parser and the program parser have different behavior on the same code #217

Open dlucanu opened 10 years ago

dlucanu commented 10 years ago

Let us consider the following definition:

module SYMVAR
  syntax Variable ::= Token{[A-Z][a-zA-Z0-9]*[\:][a-zA-Z]+} [variable, onlyLabel]
  syntax Int ::= Variable

  syntax Exp ::= Int | Id | Exp "=" Exp

  configuration
    <k> $PGM:K </k>
    <in> $IN:List </in>
    <out> .List </out>

  rule <k> X:Id = (_ => I) </k>
       <in> ListItem(I:Int) => . </in>

  rule <k> X:Id = I:Int => . </k>
       <out> _ => ListItem(I) </out>

endmodule

Assume that the file "ex.symvar" includes the expression "x = N:Int". If we we execute the usual command for krun then the output is the expected one:

 $ krun ex.symvar -cIN=".List"
<k>
    .K
</k>
<in>
    .List
</in>
<out>
    ListItem(N:Int)
</out>

If instead we give the same expression as argument for -CPGM in the command line, the rule writing in the out cell is not fired anymore:

$ krun -cPGM="x=N:Int" -cIN=".List"
<k>
    x = N
</k>
<in>
    .List
</in>
<out>
    .List
</out>

We get a similar behaviour if we give N:Int as a input argument:

$ krun -cPGM="x=y" -cIN="ListItem(N:Int)"
<k>
    x = y
</k>
<in>
    ListItem(N)
</in>
<out>
    .List
</out>

But it works fine with "#symInt(N)":

$ krun -cPGM="x=y" -cIN="ListItem(#symInt(N))"
<k>
    .K
</k>
<in>
    .List
</in>
<out>
    ListItem(#symInt(N))
</out>

The reason for different behaviour is given by the fact that krun uses different parsers: if the program is read from the file then the program parser is used, and it know how to parse "N:Int", and if the program is given as value for the option -cPGM then the rule parser is used and it does not know how to parse "N:Int". We should have the same behaviour (the expected one!) in all cases.

This block us to unify the krun arguments for the two backends; maude and java.

andreiarusoaie commented 10 years ago

This happens because the krun command line arguments are parsed with the ground parser and the programs are parsed with the program parser. For some reason, all the experiments above work properly (from the point of view of parsing) on Windows but they don't work on any Linux or Mac (at least on my machines).

I've done some debugging in KTool and it seems that N is always parsed as an Identifier on Linux while on Windows it parses as a Variable (which the correct behavior in this case). From my point of view this is either an SDF problem or a subtle parser bug that I couldn't find.