New command kore-load for computing needed issues with definitions

[ehildenb]

Currently, at load time, the booster is checking whether rules preserve definedness and then marking them as such. We can make users able to optimize their own definitions with new Ceil rules by showing them where the definition does not preserve definedness. This can be done either:

• At load time of the rpc server, or
• As a separate command.

Basically, as a first cut, it should:

• Do the preserve definedness check for both rewrites and equations.
• Print out "remainder" ceil conditions for any rules (rewrites or equations) it cannot determine that it preserves definedness.

Then workflow would then be:

• User writes a definition.
• User calls kore-load definition.kore (or some other name).
• Tool prints out:

Rule SOME_RULE_ID at location: SOME_LOCATION_ID does not preserve definedness.

    rule f(X) => 1000 / X

Remainder definedness condition is:

    #Ceil(1000 / X)

Then the user could write a rule that says:

rule #Ceil(1000 / X) => #Top

And re-run the tool, and not get the same warning anymore.

This example is obviously unsound, but it demonstrates the point of enabling the user to make progress on definedness without bothering the backend team, and also collecting a very direct and specific set of #Ceil rules that the backend team can go back and analyze themselves later (without having to respond directly to a users issue, so less rushed).