Question about usage of `[locations]` and `#location`

[ppooii12009]

Hello, I am trying to use the [location] attribute for inserting some proper information while handling errors. I followed the documentation in here . And my code is :

module LANGUAGE-SYNTAX
    imports DOMAINS-SYNTAX
    imports K-LOCATIONS
    imports KAST

    syntax Exp [locations]
    syntax Exp ::= Exp "/" Exp [seqstrict]
        | Int
    syntax KResult ::= Int
    syntax Exp ::= String
endmodule

module LANGUAGE
    imports LANGUAGE-SYNTAX
    imports DOMAINS

    configuration <k> $PGM:Exp </k>

rule A:Int / B:Int => A /Int B
    requires B =/=K 0

rule #location(_ / 0, File, StartLine, _StartColumn, _EndLine, _EndColumn) =>
  "Error: Division by zero at " +String File +String ":" +String Int2String(StartLine)

endmodule

It passed the kompile command, but the #location rule seemed not work. I ran a program with only 6 / 0 in it, then the output was directly <k> 6 / 0 ~.> .K </k>. Is there something wrong with my usage, or some bugs with #location?

[Baltoli]

This does look like a pretty straightforward error in our documentation, really sorry about that @ppooii12009!

The reason that your code doesn't work as you expect is that the term 6 / 0 will be parsed as something like:

#location(_/_(#location(6, ...), #location(0, ...), ...)

which doesn't match a RHS of the form:

#location(_/_(_, 0), ...)

This isn't visible to you because we don't print the #location nodes in pretty-printed output, but if you were to use krun --depth 0 --output kore you would see the actual KORE IR to which the first rewriting step will apply (including #location nodes).

The way that we typically use locations in K is something like the following:

module LANGUAGE-SYNTAX
    imports DOMAINS-SYNTAX
    imports K-LOCATIONS

    syntax Exp [locations]
    syntax Exp ::= Exp "/" Exp [seqstrict]
        | Int
    syntax KResult ::= Int
    syntax Exp ::= String
endmodule

module LANGUAGE
    imports LANGUAGE-SYNTAX
    imports DOMAINS

    syntax Location ::= Loc(file: String, startLine: Int, startColumn: Int, endLine: Int, endColumn: Int)

    configuration
      <k> $PGM </k>
      <loc> Loc("<unknown>", 0, 0, 0, 0) </loc>

    rule A:Int / B:Int => A /Int B
        requires B =/=K 0

    syntax String ::= divZeroError(Location) [function]
    rule divZeroError(L) =>
      "Error: Division by zero at "
        +String file(L)
        +String ":"
        +String Int2String(startLine(L))

    rule
      <k> _ / 0 => divZeroError(L) ...</k>
      <loc> L </loc>

    rule
      <k> #location(E:Exp, File, StartLine, StartColumn, EndLine, EndColumn) => E ...</k>
      <loc> _ => Loc(File, StartLine, StartColumn, EndLine, EndColumn) </loc>
endmodule

Every time you see a node with a location, rewrite to its underlying term and store the location in the configuration. You can then extend this with language-specific location tracking (for example, if your language has procedure call and return semantics, you'd want to store the location in a stack frame entry).

We don't automate this because languages will want to handle their location-tracking differently.

Hope this helps, and I'll make sure to get the documentation updated!

[ppooii12009]

It really helps. Thank you very much!