Add cut-point rules for specific functions / intrinsics#931
Add cut-point rules for specific functions / intrinsics#931
Conversation
The `breakOnFunctions` cell will contain identifiers of functions that should be broken on by the `termCallFunctionFilter` rule. Which is identical to `termCallFunction` except it checks if the id is in the `breakOnFunctions` cell and has a different identifier for the cut point rules.
Fully qualified paths may have commas. Instead of using a separator use multiple occurances of the flag
dkcumming
requested review from
jberthold,
mariaKt,
palinatolmach and
tothtamas28
|
As discussed today in a meeting: This seems like a very useful feature for debugging proofs and semantic corner cases. Maybe there is an easy way to modify the pending nodes in a proof (updating this config cell)? |
jberthold
left a comment
jberthold
left a comment
There was a problem hiding this comment.
Approving, we can merge this for now (will be easy to back out later).
In the long run we might want to use some K IO for this (\CC @ehildenb ) something like reading an environment variable with https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#shell-access
|
An alternative approach that @dkcumming and I have considered was instrumenting the program definition as follows:
With this approach, there’s no need to extend the configuration. The open question is what the |
…on)) (#960) This PR builds upon #931 modifying the approach in response to the comments on that PR. For full context read #931 _first_. The `kmir prove-rs` flag `--break-on-function` is implemented in this PR as a compiled definition with hooked function to retrieve the function names to match on. This is similar to the already existing pattern that compiles the static data of a KMIR configuration into the definition. This allows for functions to be provided both when creating the initial proof, and when reading from disc (triggers a recompile of llvm if different flags are provided). I added a test to demonstrate this working on functions and intrinsics, only matching those provided. I do not have a test from reading a partial proof and adding different function names - I did test it but it seemed a bit overboard for a test just now. I did try the method with [K shell access impure function](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#shell-access), however this created branching for every function call since the result was stored in a symbolic value. I couldn't figure out how to get that working concretely (I don't think it is possible but might be wrong).
|
#960 supersedes |
3 participants
This PR enables the ability to provide strings to
kmir prove-rscommand via flag--break-on-function <STR>that can will then be broken on as a cut point rule if the a function call matches the string. In particular, the are added to a set in the K configuration and each function / intrinsic call is modified to follow this logic:breakOnFunctionscell is a substring of the the function / instrinsic call, then break on call (processing the terminator in the same way);Multiple strings can be added to the set but each needs to be provided with a new
--break-on-functionflag since I couldn' think of a separator that was common and would not appear in the the fully qualified path of a function (if we want to provide the fully qualified path).I tested this on the local mir-semantics tests and on SPL token and both worked as expected.