Automate regeneration of test cases #987
Comments
Following runtimeverification/k#3989, the KORE attribute that encodes "this axiom declares an overload equality over two symbols `X` and `Y`" is being gradually renamed from `overload(_,_)` to `symbol-overload(_,_)`. This PR moves the LLVM backend over to accepting the new attribute rather than the old one; doing so is a simple renaming process on the attribute following #983. The checked-in KORE test files are updated by a simple renaming of the attribute.[^1] ~~Blocked on: #983~~ [^1]: See #987; it's a pain to regenerate all the KORE at the moment so I've edited the files manually using `sed` rather than the actual K frontend. This is fine for this case in the frontend, but in the future if we make more complex changes to the structure of compiled KORE definitions we should implement a more robust way of rebuilding the test suite to pin against a particular frontend version.
|
This would be good to bring up at the next K meeting and enforce more broadly across all of RV. That is, every checked-in KORE file should either be:
When I changed all the There'll be similar pain whenever we change anything related to the standard library (runtimeverification/k#3801, runtimeverification/k#3986) or emitted attributes (runtimeverification/k#3988, runtimeverification/k#3960). |
|
@Scott-Guest mentions that we also have the input files checked in as KORE; we should parse these and regenerate the KORE from surface syntax. |
|
The runner interface should allow for ergonomic usage (i.e. update a single file only) |
Currently, we have a directory of checked-in KORE files that encode test cases using
lit. The corresponding K source code also exists in the repo, but the process of actually generating the KORE from the K is not automatic and requires a reasonable amount of manual work.We should implement a script that can take a K source definition and automatically regenerate the corresponding KORE that the backend actually runs. This should remain a manual process run by developers when something changes in the frontend; we don't really want to introduce a dependency on K in CI.
The script will need to:
kompilea definition and copy thedefinition.koreto the test directory in an appropriate place.// RUN: ...lines from the K file and paste them at the front of the KORE file.The text was updated successfully, but these errors were encountered: