CONTRACTS: loop assigns clause inference function

[remi-delmas-3000]

The first commit is from #7636, do not review.

Co-authored with @qinheping

Loop assigns clause inference function. Uses loop_utils.h to get a set of lvalue expressions modulo aliasing that may be assigned by the loop.
The lvalue expressions are then post processed.

• If an inferred target depends on a loop-local variable (i.e. a variable that does not exist outside of the loop body) it is widened to its base object. If the base object still depends on a loop local, the target is discarded, otherwise __CPROVER_object_whole(&root_object) is kept as inferred target.
• If the address of an inferred target is non-constant, then __CPROVER_object_whole(&target) is used as widened target.

Extracted from #7541, can only be tested once all features are in place.

• 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

Patch and project coverage have no change.

Comparison is base (53b50bc) 78.51% compared to head (1b899b1) 78.51%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7629   +/-   ##
========================================
  Coverage    78.51%   78.51%           
========================================
  Files         1674     1674           
  Lines       191935   191935           
========================================
  Hits        150704   150704           
  Misses       41231    41231           

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 in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[remi-delmas-3000]

@tautschnig @qinheping I just pushed a revised version that uses root objects to widen targets, should be stable now

[qinheping]

LGTM

[feliperodri]

@tautschnig if you have the time, could you do another round of review on this PR?

[tautschnig]

Just minor cleanup, will be good to go once the depended-on PR is merged.

[tautschnig]

What happens behind the scenes with a pointer passed to object-whole? Would it be the same as the root_object case above?

[remi-delmas-3000]

The meaning of object_whole(&expr) or object_whole(&root_object(expr)) is the same so we don't bother computing the root object. In the first case we compute the root_object to try and get rid of a dependency on loop locals or drop the target if the root object is still local to the loop. In the second case we have a non-constant expression that does not depend on loop locals, and we just widen it directly.

[remi-delmas-3000]

we have to use object_whole because this is the predicate that DFCC understands to specify byte ranges.

[remi-delmas-3000]

@tautschnig all suggestions implemented, could you please take a last look ?