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.

[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

[Alexander-Aghili]

Anything more needed here?

[zhassan-aws]

We should be good to go after resolving the conflicts.

[celinval]

I solved the conflict. So if the CI passes, this should merge. Thanks again for the contribution @Alexander-Aghili!

[Alexander-Aghili]

Hooray! Thanks for all the help and guidance everyone.