General system for outputting custom metrics for BenchExec, etc

[sim642]

BenchExec allows tools to output special values that can easily be shown as additional columns in the tables:

Overwriting the function get_value_from_output will allow you to add <column> tags with custom values to your table-definition files, and table-generator will extract the respective values from the output of your tool using this function.

More information at https://github.com/sosy-lab/benchexec/blob/0e0f79cf8d7cc52bf7e7c9a4c622f8d070c855d7/doc/table-generator.md#column-features and https://github.com/sosy-lab/benchexec/blob/0e0f79cf8d7cc52bf7e7c9a4c622f8d070c855d7/doc/tool-integration.md#writing-a-tool-info-module.

Instead of hardcoding a multitude of special-purpose regexes into the tool-info module, which would have to be submitted each time we want to add more, it would be better to have special output syntax in Goblint (and a module for abstracting it) to print these such that the tool-info module can pick them up unchanged. This should be separate from the user-readable output (such that one can be changed without affecting the other) and probably optional.

A consistent output format for such statistics, etc wouldn't be useful for just BenchExec, but also our own benchmarking scripts that currently grep out a variety of specific outputs, which is error-prone when the user-readable output is changed.
And in BenchExec instead of just displaying them in columns, it would also be easy to then make comparative plots against any metric, not just CPU time.

Metrics

• Solver vars and evals
• Solver aborts (TD3: optimize destabilization by aborting transfer function when unchanged #364)
• Race counts (total, safe, vulnerable?, unsafe)
• Uncalled functions count
• Missing function definitions count
• Line counts (total logical, dead, live)
• Message counts by severity (or even category/tag?)

Feel free to suggest any others.

[vogler]

For save_run there are some json files and a solver_stats.csv (new row each dbg.solver-stats-interval) written.

analyzer/src/framework/control.ml

Lines 457 to 464 in 4d7c06f

	if save_run <> "" then (
	let analyses = Filename.concat save_run "analyses.marshalled" in
	let config = Filename.concat save_run "config.json" in
	let meta = Filename.concat save_run "meta.json" in
	let solver_stats = Filename.concat save_run "solver_stats.csv" in (* see Generic.SolverStats... *)
	let cil = Filename.concat save_run "cil.marshalled" in
	let warnings = Filename.concat save_run "warnings.marshalled" in
	let stats = Filename.concat save_run "stats.marshalled" in

[sim642]

Interesting, I wasn't aware of that output, although it's somewhat different, because there the idea is to regularly print the same statistics. For benchmarking results overview and comparison it's just some final overall metrics that would be interesting in the tables.

[vogler]

Should check printstats, all the open_out and get_out and replace with something similar to this Meta.json.
I would print those metrics as json to stdout since it's easy enough to read, and some special file(s).