Symex max depth default max

[TGWDB]

This PR implements the recommended fix in #2295.

• Each commit message has a non-empty body, explaining why the change was made.
• 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.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6222 (57afd55) into develop (141f3ce) will decrease coverage by 0.17%.
The diff coverage is 100.00%.

❗ Current head 57afd55 differs from pull request most recent head c344048. Consider uploading reports for the commit c344048 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6222      +/-   ##
===========================================
- Coverage    75.30%   75.13%   -0.18%     
===========================================
  Files         1458     1459       +1     
  Lines       161436   161449      +13     
===========================================
- Hits        121575   121305     -270     
- Misses       39861    40144     +283     

Impacted Files	Coverage Δ
jbmc/src/jbmc/jbmc_parse_options.cpp	72.32% <100.00%> (+0.05%)	⬆️
src/cbmc/cbmc_parse_options.cpp	77.41% <100.00%> (+0.04%)	⬆️
src/goto-symex/symex_main.cpp	85.96% <100.00%> (ø)
src/util/find_symbols.h	0.00% <0.00%> (-100.00%)	⬇️
src/goto-instrument/accelerate/path.h	0.00% <0.00%> (-100.00%)	⬇️
src/goto-instrument/accelerate/polynomial.h	0.00% <0.00%> (-100.00%)	⬇️
...o-instrument/accelerate/polynomial_accelerator.cpp	0.00% <0.00%> (-78.13%)	⬇️
src/goto-instrument/accelerate/accelerator.h	7.69% <0.00%> (-46.16%)	⬇️
...ument/accelerate/enumerating_loop_acceleration.cpp	62.50% <0.00%> (-37.50%)	⬇️
...goto-instrument/accelerate/sat_path_enumerator.cpp	58.13% <0.00%> (-37.21%)	⬇️
... and 17 more

---

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 665abf7...c344048. Read the comment docs.

[kroening]

The default should be dealt with earlier, meaning when setting up optionst.

[martin-cs]

Daniel is correct; I should not have approved this. The correct fix is an else here:

cbmc/src/cbmc/cbmc_parse_options.cpp

Line 261 in 06c563a

which sets the correct value. It might be worth seeing if unwind has similar behaviour.

[TGWDB]

I tried changing the creation of the optiont and this now breaks unit tests (these can be fixed). I'm unclear why the "depth" option is a special case that should be handled outside, when other options passed in to the symex_config that are missing are handled in the constructor. (The main difference appears to be that "depth" has a different default value, but this is also handled in the constructor for the "max_field_sensitivity_array_size" option.)

[martin-cs]

@TGWDB It is a fair question. In an ideal world the *_parse_options.cpp file should read the cmdlinet and use it to populate an optionst along with default values if they are not 0 (or whatever optionst returns for the "asking for an option that hasn't been set" case). Unit tests can then simply create an appropriate optionst. However it is made, it is the optionst which gets passed to the actual code and used to configure things. Ideally this will be in a constructor, RAII-style. There is a little bit of a grey area about whether and how the constructors should handle cases when the configuration is complex and has multiple, non-orthogonal options.

Historically, this bit of design intent has not been as widely followed as maybe it should have been, so in the older parts of the code you do find configuration parameters lurking much deeper. These should be treated as a legacy issue and ideally modernised and moved into the "parse_options.cpp builds an optionst and that is it for configuration" world.

HTH

[TGWDB]

Rather than an explicit else case I set the default value for the option in the creation of optionst. This seems like the cleanest solution.

[martin-cs]

Seems a reasonable solution.

[TGWDB]

@kroening Any chance of a codeowner review now?

[tautschnig]

@TGWDB Please cleanup the commit history on this one.

[TGWDB]

@TGWDB Please cleanup the commit history on this one.

Commit messages tidied up. This should just be waiting on codeowner review now.

[martin-cs]

Paging @peterschrammel