Scripted parallel property checking using CBMC

[tautschnig]

Adds a (Python) script to check all properties contained in a given GOTO
binary individually, but in parallel. This can yield a somewhat
different user experience in that some of the results become available
early on while other properties are still being checked for, as opposed
to the all-or-nothing experience when doing all properties at once.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6895 (c45eead) into develop (577b0ec) will increase coverage by 0.01%.
The diff coverage is 90.19%.

@@             Coverage Diff             @@
##           develop    #6895      +/-   ##
===========================================
+ Coverage    77.81%   77.82%   +0.01%     
===========================================
  Files         1568     1568              
  Lines       179975   180004      +29     
===========================================
+ Hits        140044   140092      +48     
+ Misses       39931    39912      -19     

Impacted Files	Coverage Δ
.../goto-instrument/goto_instrument_parse_options.cpp	70.90% <73.33%> (-0.23%)	⬇️
src/ansi-c/c_typecheck_base.cpp	81.15% <95.23%> (+2.27%)	⬆️
src/ansi-c/goto_check_c.cpp	91.55% <100.00%> (+0.07%)	⬆️
src/goto-symex/symex_target_equation.cpp	95.35% <100.00%> (+0.02%)	⬆️
src/ansi-c/expr2c.cpp	67.53% <0.00%> (-0.10%)	⬇️
src/solvers/smt2/smt2_conv.cpp	67.61% <0.00%> (+0.35%)	⬆️
...olvers/flattening/c_bit_field_replacement_type.cpp	100.00% <0.00%> (+46.66%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 15d60af...c45eead. Read the comment docs.

[NlightNFotis]

Can we get a bit of documentation on this? Like, what is it and how do I use it?

I'm asking because the scripts/ folder has ended up with a great number of things that are only useful to their authors, so maybe it's a good idea to start requiring docs so that they become more widely useful.

[jimgrundy]

Agree with fotis. At the very least can we get a descriptive header comment in the file explaining what it is an how to use it.

[tautschnig]

@NlightNFotis @jimgrundy I have now added documentation at the top of the file, and am also including this in the --help output. All feedback on how to improve this documentation would be appreciated!

[NlightNFotis]

Thank you. That already looks great!

On a separate note, the functionality this implements looks like a great fit for internal functionality. Is this a stand-in for that, or do we plan to rely on this script to provide this functionality?

[tautschnig]

On a separate note, the functionality this implements looks like a great fit for internal functionality. Is this a stand-in for that, or do we plan to rely on this script to provide this functionality?

Building that into the tool (and thereby reducing the overhead) is on the agenda :-)