Uncaught exception by map looku

[dlucanu]

Consider the following definition:

module TEST
  syntax Exp ::= Id | Int
  syntax Stmt ::= Exp ";" [strict]

  configuration
    <k> $PGM:Stmt </k>
    <state> $ST:Map </state> 

  rule <k> X:Id => St[X] ...</k>
       <state> St </state>
endmodule

and the file ex.test including x;. If we run the above definition with the empty map assigned to ST then we get an Uncaught exception error message:

$ krun ex.test -cST=".Map"
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please file a bug report at https://github.com/kframework/k/issues

This error is due to the lookup operation over maps. This can be easily observed if we run the example with a valid map:

$ krun ex.test -cST="x |-> 2"
<k>
    2 ~> (HOLE ;)
</k>
<state>
    x |-> 2
</state>

The same is true for the update operation over maps.

[dwightguth]

This seems to be intricately tied with the way lookups happen in KItoBackendJavaKILTransformer, which is likely to change in the new implementation. So I am going to make sure this works in the new KORE, but not fix it for the current version.

[dwightguth]

This seems to work as expected in the new pipeline. Your code gets stuck heating because the heating rule has the notBool isKResult side condition, and you didn't declare KResult. But there's no assertion error and if you add syntax KResult ::= Int then it will heat and cool correctly. I am going to close this now.

[dwightguth]

Actually never mind I just retested and we are getting a different error. Namely, it is throwing an AssertionError because the MapLookup is returning Bottom and the rewriter doesn't know how to handle this. I am going to assign this to @andreistefanescu . Andrei, obviously there should be some kind of friendly error message here.