model-checking
Harness output individual files
Resolves #3356
- Changes allow for directory with individual output of files named by the full harness name. --output-into-files command line argument will allow for placing all output of individual harnesses into files named by the full harness pretty_name. The output directory is either --target-dir or a hard coded default: "kani_output" directory. (These can be changed if there is a better interface). Still prints output to std::out exactly as previous.
- Previously, all output was placed into std::out. This will allow for some control over output. It will also enable easier parsing of harness output.
- Only solved #3356 but could be expanded to include more features.
- Ran manually to check the flags and output behaved as expected. Indeed: --output-into-files enabled will place output into individual files, disabled will not --output-terse will create terse output to command line, regular output to individual files if --output-into-files is enabled. --target-dir will place output into target-dir directory when --output-into-files is enabled, and will not place file output when disabled.
Let me know if you need specific explanations of code segments, a clean list of all the testing configurations, or any feature enhancement for greater configuration options.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This output format is untested as of this PR. I'd like to see one regression test added at least. This isn't a blocking request, but likely something we want to add immediately, maybe in a follow up PR.
This output format is untested as of this PR. I'd like to see one regression test added at least. This isn't a blocking request, but likely something we want to add immediately, maybe in a follow up PR.
I agree that tests should be added. I'd be fine adding it as a component of this PR or as a separate one, whichever is easier for you guys.
Hey guys, sorry I haven't gotten to this in a minute. I was testing this on a server used by my research group, but my laptop's SSD failed with my ssh key so I can't really access the server at the moment. Should be fixed in a couple days. Thanks for the patience.
Okay I tested it and added the -Z --unstable-options instead of --enable-unstable. Do we still want to add tests as a part of this PR?
Okay I tested it and added the -Z --unstable-options instead of --enable-unstable. Do we still want to add tests as a part of this PR?
I'm okay without a regression for this specific output format since its a really special case and testing will involve some work. I can take that up in a follow up PR. You might want to do the following though (in order of priorities),
Required :-
- Fix existing regression tests that are failing
- Add comments on the functions related to processing the output.
- Format the code with
cargo fmtand runcargo clippyon it once.
Optionally
- Create an issue to test the new output format.
Hey there, I've done most of it but I ran into this issue when running regression tests: ERROR: CBMC version is 5.89.0, expected at least 5.95.0 How can I upgrade the CBMC version?
Hey there, I've done most of it but I ran into this issue when running regression tests: ERROR: CBMC version is 5.89.0, expected at least 5.95.0 How can I upgrade the CBMC version?
You can re-run the script responsible for installing the dependencies to install the appropriate CBMC version. Here is a link to the wiki page that explains what exactly to run: https://model-checking.github.io/kani/build-from-source.html#dependencies.
If you're using a Mac, run:
./scripts/setup/macos/install_cbmc.sh
If you're using Ubuntu, run:
./scripts/setup/ubuntu/install_cbmc.sh
I don't want to be the bottleneck on this but in short, I am having a difficult time upgrading because of permissions issues on my remote server, and thus, if others want to try and fix the regression tests, then that is fine as well. Otherwise I am going to have to spend some time fixing the issue on the server I do my development work on and I'm out of town at the moment.
I don't want to be the bottleneck on this but in short, I am having a difficult time upgrading because of permissions issues on my remote server, and thus, if others want to try and fix the regression tests, then that is fine as well. Otherwise I am going to have to spend some time fixing the issue on the server I do my development work on and I'm out of town at the moment.
Hi @Alexander-Aghili, the regression tests should pass now after the fix from @celinval. You should be able to resume development if you have the time to add tests. If not, please let us know and we can take on the task of adding a test on this PR 😄
Hi guys, Sorry for taking so long, I've been out on holiday. I made an issue for adding regression tests. Do we want to complete that in this PR? If not, what needs to be done with this PR to merge it? If we do, how should the regression test be done?
Hi guys, Sorry for taking so long, I've been out on holiday. I made an issue for adding regression tests. Do we want to complete that in this PR? If not, what needs to be done with this PR to merge it? If we do, how should the regression test be done?
For this pr to be merged, we are looking for at least something that uses the new flag and ensure Kani still succeeds. It doesn't need to check that the files exist, just needs to test that Kani doesn't break. If you can add that, I am OK with merging the PR. Lmk if thats putting too much on your plate, and I can take over this PR and add those changes myself as well. In any case, thank you very much for the changes :D.
I swear I'm not as flaky as I seem but my computer's screen just broke and I'm going to have to get it replaced which might take some time. If you want to take it over and finish the PR feel free to do so otherwise I'll get on it immediately when I can.
I swear I'm not as flaky as I seem but my computer's screen just broke and I'm going to have to get it replaced which might take some time. If you want to take it over and finish the PR feel free to do so otherwise I'll get on it immediately when I can.
No worries :D
Finally getting back around to this. I will be creating that test and merging in the new base, then asking for a review to be merged.
Finally getting back around to this. I will be creating that test and merging in the new base, then asking for a review to be merged.
Awesome, thank you!
Hey, I was checking the other UI tests and they verify the validity of the response by running a proof in a main.rs file and checking it with an expected output which is a single txt. With the proper output being a directory, how should I handle that? Also, do you use git merge or git rebase when updating the git structure?
Hey, I was checking the other UI tests and they verify the validity of the response by running a proof in a main.rs file and checking it with an expected output which is a single txt. With the proper output being a directory, how should I handle that? Also, do you use git merge or git rebase when updating the git structure?
Great question. Most of our tests check Kani's console output. For cases like this PR, we have a script based regression that we store in tests/script-based-pre. You can find more details here: https://model-checking.github.io/kani/regression-testing.html#script-based-tests
About git. I personally prefer rebasing as I'm developing a feature, but once I publish a PR, I switch to merge since the GitHub UI seems to handle it better. Our PR merge strategy uses squash, so each PR eventually becomes a single commit. I hope that answers your questions.
Thanks again for your collaboration! I can't wait for this PR to be merged. 😃
So I think when I merged, it included all of the commits in the commit history here. Is there a way to prevent that in the future? Also, I looked at the script-based-pre testing and it seemed like the .expected file checks the output of the command to stdout but I wasn't sure how to verify the generation of the output to directories. I decided that I would do it through a script which is almost done. Would it be better to do it another way or do you need to see the code first to decide?
So I think when I merged, it included all of the commits in the commit history here. Is there a way to prevent that in the future? Also, I looked at the script-based-pre testing and it seemed like the .expected file checks the output of the command to stdout but I wasn't sure how to verify the generation of the output to directories. I decided that I would do it through a script which is almost done. Would it be better to do it another way or do you need to see the code first to decide?
Hi @Alexander-Aghili, the only problem I see is that you seem to have accidentally a target/tools folder. If you remove this, it should be good to go.
@celinval I updated with a test to ensure the feature operates and behaves as expected... how could I remove the target/tools file from the commit if that matters because git rm --cached is not working.
Just remove the folder with regular rm and create a new commit. It's fine.
Hey everyone, any update here?
Almost there, can you resolve the merge conflicts and push again?
Okay I updated it. However, it seems like sometimes the tests fail only on the CI?
Before we merge, can you resolve the merge conflicts locally? It'll allow us to see CI as well