krun should distinguish \bottom from stuck states

[ttuegel]

kore-exec (as krun) does not report \bottom results, but instead reports their parents as stuck states.

Reported by: @nishantjr

Example

test.k:

module TEST
    imports INT
    syntax FOO ::= "foo"
    configuration <k> foo ~> $PGM:Int </k>
    rule <k> foo => #Bottom ... </k>
endmodule

input:

1

Both of the following examples should report #Bottom:

$ krun input 
<k>
  foo ~> 1 ~> .
</k>

$ krun --search-final input 
{
  Result:GeneratedTopCell
#Equals
  <k>
    foo ~> 1 ~> .
  </k>
}

Solution

We can add a Bottom constructor to ProgramState. For comparison, see the Proven constructor to ClaimState, which serves a similar function. The transitionRule must return Bottom when any Simplify or Rewrite step yields no children. Then, execution terminates for transitionRuleWorker _ Begin Bottom.