CONTRACTS: Add an option to not unwind transformed loops after applying loop contracts

[qinheping]

• 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).
• n/a 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.

Background

With the loop contracts simplification, applying loop contracts will result in transformed loops which will be executed exactly twice. It requires that the unwinding numbers of transformed loops have to be at least two to pass unwinding assertions. In #7318, we chose to unwind transformed loops for users to avoid them provide unwinding numbers less than two unaware.

Issue

Although unwinding transformed loops for users reduce the risk of unwinding-assertion failures, it introduces some new confusion. Besides making the GOTO program more complicated and less readable, it also duplicate all assertions twice, including the assertions that check whether the loop invariants hold before entry of the loop. Such duplicated properties are reported in the result if we run CBMC on the instrumented GOTO program, which may make users harder to locate the failure.

More importantly, when an assertion is designed to be unique with a unique ID, for example, Kani assign every reachability check a unique ID, duplicate such assertion will result that two assertions have the same ID and fail Kani' CBMC-result rendering.

Solution

In this PR, we add an option, in both goto-instrument and goto-synthesizer, so that users can choose to not unwind the transformed loops to avoid duplicate properties.

[codecov]

Codecov Report

Base: 78.50% // Head: 78.28% // Decreases project coverage by -0.22% ⚠️

Coverage data is based on head (e6e8137) compared to base (3f578e1).
Patch coverage: 100.00% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7524      +/-   ##
===========================================
- Coverage    78.50%   78.28%   -0.22%     
===========================================
  Files         1663     1663              
  Lines       191297   191339      +42     
===========================================
- Hits        150174   149787     -387     
- Misses       41123    41552     +429     

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
...rc/goto-instrument/goto_instrument_parse_options.h	100.00% <ø> (ø)
.../goto-synthesizer/goto_synthesizer_parse_options.h	100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.cpp	95.54% <100.00%> (+<0.01%)	⬆️
.../goto-instrument/goto_instrument_parse_options.cpp	71.47% <100.00%> (+0.16%)	⬆️
src/goto-synthesizer/cegis_verifier.cpp	88.74% <100.00%> (+0.03%)	⬆️
...oto-synthesizer/goto_synthesizer_parse_options.cpp	67.64% <100.00%> (+0.98%)	⬆️
src/util/type.cpp	27.27% <0.00%> (-45.46%)	⬇️
src/util/timestamper.h	33.33% <0.00%> (-33.34%)	⬇️
src/big-int/bigint.cc	56.01% <0.00%> (-32.99%)	⬇️
... and 27 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.