Harness Output in Individual Files

[Alexander-Aghili]

Requested feature: Harness Output in Individual Files
Use case: Easily parse output by having each harness output be an a unique file.
Printing is done to the std output but having each harness output be in a file helps with parsing. Possibly files named based on harness name.
This is currently done in each harness here in kani-driver line 124:

if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
    println!(
        "{}",
        result.render(
            &self.args.output_format,
            harness.attributes.should_panic,
            self.args.coverage
        )
    );
}

[jaisnan]

Thank you for the feature request! This is a great idea for an improvement. Can you describe a little bit more about how this would be useful for a user in a project, if possible?

[Alexander-Aghili]

Hi @jaisnan, for a project our team is working on we wanted the capability to use Kani in a CD/CI capacity, and provide information about the run in a quick easy interface. Having to manually parse the single large output file seems more difficult than having the option of having individual harnesses output into files which can then be managed.

[Alexander-Aghili]

I have a test version of what it could look like but I'm not sure if this is how you guys would want to do it:

           if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
                let file_name = String::from("./kani-harness-result/".to_owned() + &harness.pretty_name.clone()); 
                let path = Path::new(&file_name);
                let prefix = path.parent().unwrap();
                std::fs::create_dir_all(prefix).unwrap();

                let file = File::create(file_name.clone());

                let output = result.render(
                    &self.args.output_format,
                    harness.attributes.should_panic,
                    self.args.coverage,
                );

                if let Err(e) = writeln!(file.unwrap(), "{}", output) {
                    eprintln!("Failed to write to file {}: {}", file_name, e);
                }
                println!("{}", output);

            }

Basically it makes a directory structure based on the harness names and then puts the output of a harness into a single file based on its name.
I can make a pull request if you think that's appropriate. It doesn't have a flag to enable it but I assume adding that would be relatively simple.

[jaisnan]

Of course! We encourage and welcome external pull requests! Please feel free to add your changes as a PR.

[celinval]

I really like this idea. In fact, I would suggest that this should be done whenever the terse output is selected (which I think should be the default one). In this case, Kani could print the verification summary and save detailed result in a file, like you mentioned.

One feedback for your potential patch is to use the target directory as the base directory of your new result directory.