Harness output individual files

[Alexander-Aghili]

Resolves #3356

1. 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.
2. 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.
3. Only solved Harness Output in Individual Files #3356 but could be expanded to include more features.
4. 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.

[jaisnan]

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.

[Alexander-Aghili]

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.

[Alexander-Aghili]

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.

[Alexander-Aghili]

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?

[jaisnan]

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 :-

1. Fix existing regression tests that are failing
2. Add comments on the functions related to processing the output.
3. Format the code with cargo fmt and run cargo clippy on it once.

Optionally

1. Create an issue to test the new output format.

[Alexander-Aghili]

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?

[artemagvanian]

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.

[zhassan-aws]

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

[Alexander-Aghili]

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.

[Alexander-Aghili]

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?

[celinval]

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. 😃

[Alexander-Aghili]

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?

[celinval]

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.

[Alexander-Aghili]

@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.

[celinval]

Just remove the folder with regular rm and create a new commit. It's fine.

[Alexander-Aghili]

Given it passes the regression tests, it should be good to go.

[Alexander-Aghili]

Hey everyone, any update here?

[jaisnan]

Hey everyone, any update here?

Almost there, can you resolve the merge conflicts and push again?

[Alexander-Aghili]

@jaisnan Fixed

[Alexander-Aghili]

Okay I updated it. However, it seems like sometimes the tests fail only on the CI?

[celinval]

What is the error?

[celinval]

Awesome!! Thanks

[jaisnan]

Before we merge, can you resolve the merge conflicts locally? It'll allow us to see CI as well