Share stats printing, improve Soteria.Terminal
#209
Conversation
N1ark
added
soteria-core
|
Am I correct to understand that the last bullet point is now gone in favour of some dune magic? |
yes correct :) changed that the other day because it was hacky and i realised i could just set env vars in the cram config which i wasnt aware of |
|
Yeah looking at the commit, it's much prettier and very clever, hadn't thought of it either :) |
| let functions_to_analyse = as_nonempty_list functions_to_analyse in | ||
| let@ () = initialise ~log_config ~term_config ~solver_config config in | ||
| let@ () = | ||
| initialise ~log_config ~term_config ~solver_config ~stats_config config |
There was a problem hiding this comment.
We're starting to need a single ~soteria-config term
| (* | "requires" { REQUIRES } *) | ||
| (* | "ensures" { ENSURES } *) | ||
| (* | "RW" { RW } *) | ||
| (* | "Freed" { FREED } *) |
There was a problem hiding this comment.
I'm cleaning up some of linear in the logic PR so I'm a bit worried about this creating conflicts, but at the same time I think it's minor enough that it doesn't have to move.
soteria/lib/terminal/printers.ml
Outdated
| (** Pretty-prints a time quantity in seconds, displaying it in either seconds or | ||
| milli-seconds for smaller values (< 0.05s). Wrapped in [pp_unstable]. *) |
There was a problem hiding this comment.
Don't spend time doing this but fyi you can reference {!pp_unstable} to have a link in the doc
| @@ -1,9 +1,9 @@ | |||
| (executables | |||
| (names run_twice deep_give_up if_sure) | |||
| (names run_twice deep_give_up if_sure print_stats) | |||
There was a problem hiding this comment.
Urgh my other PR removes cram tests for symex, it's going to be a mess :(
There was a problem hiding this comment.
your price to pay for taking 3 weeks to review 👿
|
Clarification: most comments are things I thought about in the moment, the only thing I'd like changed before merging if you can is the parameter to pp_unstable, otherwise feel free to merge |
Fixes #154
A lot more changes than what the issue required but I want the user-facing part of Soteria (i.e.
Terminal) to be really nice and clean and shareable so the user experience is nice and homogeneous! So I added a bunch of utility that could be shared so we have only one way of output things across the tool.Removed
--dump-statsfrom Soteria-C and--statsfrom Soteria-Rust; instead added aConfigmodule to stats to configure stats outputting, with a flag--output-stats(alias--dump-stats,--stats) to either dump the stats to the given file if specified, or to the terminal if the specified string isstdout.Added
Terminal.Printerswith some utility printers:pp_time,pp_plural,pp_percent, andpp_unstable.pp_unstablewraps a printer for "unstable" values, i.e. values that change frequently. If the flag--hide-unstable(alias--diffable) is passed,pp_unstableprints a placeholder value instead (e.g.<time>).For instance,
pp_timeis wrapped inpp_unstable, and in Soteria-Rust I also wrapped code ranges in it, to avoid test diffs when I upgrade Rust versions and the call-traces move around.AddedSoteria.Terminal.Config.in_test_environment : unit -> bool, that returns whether we are currently in a test environment (dune test). This is used to automatically enable some flags (--hide-unstableand--cleanin Soteria-Rust), avoiding the need to have them everywhere in the test files.