Added support for loop_entry history variable.

[aalok-thakkar]

In this commit we introduce a new expression, __CPROVER_loop_entry, which can be used within loop invariants to track history of variables.
__CPROVER_loop_entry(x) returns the initial value of a variable just before the very first iteration of a loop.

• 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[feliperodri]

We need regression tests.

[codecov]

Codecov Report

Merging #6278 (f8cca6c) into develop (448421b) will decrease coverage by 0.00%.
The diff coverage is 88.57%.

@@             Coverage Diff             @@
##           develop    #6278      +/-   ##
===========================================
- Coverage    75.91%   75.91%   -0.01%     
===========================================
  Files         1514     1514              
  Lines       163972   163984      +12     
===========================================
+ Hits        124476   124485       +9     
- Misses       39496    39499       +3     

Impacted Files	Coverage Δ
...mc/src/java_bytecode/java_local_variable_table.cpp	95.22% <ø> (ø)
...nit/java-testing-utils/require_goto_statements.cpp	82.82% <ø> (ø)
...de/java_trace_validation/java_trace_validation.cpp	100.00% <ø> (ø)
src/analyses/local_bitvector_analysis.cpp	74.85% <ø> (ø)
src/analyses/local_cfg.h	75.00% <ø> (ø)
src/analyses/local_safe_pointers.cpp	81.55% <ø> (ø)
src/analyses/local_safe_pointers.h	100.00% <ø> (ø)
src/analyses/uncaught_exceptions_analysis.cpp	92.77% <ø> (ø)
...yses/variable-sensitivity/abstract_environment.cpp	95.02% <ø> (ø)
...riable-sensitivity/variable_sensitivity_domain.cpp	89.38% <ø> (ø)
... and 83 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 a023d0f...f8cca6c. Read the comment docs.

[feliperodri]

LGTM modulo Saswat's comments.

[feliperodri]

Almost there 😊

[SaswatPadhi]

There is a bit of code duplication between disallow_loop_history_variables and disallow_history_variables.

Can we remove disallow_loop_history_variables, add an additional argument to disallow_history_variables which would be the id of the history variable expressions we want to disallow, and just reuse the code in both contexts?

[SaswatPadhi]

Thanks; LGTM modulo the build issues with CI.

[feliperodri]

@aalok-thakkar CI failures are due to regex on test descriptions (not compatible with Windows). You also need to run clang-format.

[feliperodri]

LGTM modulo CI failures.

[chrisr-diffblue]

Code looks great, but I wonder if I might ask for a couple of extras:

1. Some more negative tests - at the moment the regression tests you've added all lead either to VERIFICATION SUCCESSFUL, or CONVERSION ERROR... Could we perhaps have some tests that also lead to verification failure? This might also help with my next point :-)
2. This is more optional... but it would be super nice if we could also have a small bit of user documentation for this new predicate... indicating its purpose, how it should be used, etc.

I won't block the review just for missing user documentation, but I think we could do with the extra "negative test" before we merge.

[SaswatPadhi]

Thanks @chrisr-diffblue!

@aalok-thakkar I don't understand the new test. I think by negative tests Chris was suggesting that we include a test where it would be violated, and we check that CBMC correctly catches it. An example would be:

while(y > 0)
    __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
    {
      --y;
      x += 1;
      x -= 2;
    }
}

[SaswatPadhi]

LGTM. Thanks for all the fixes, @aalok-thakkar :)

[feliperodri]

@chrisr-diffblue could you take another look?

[SaswatPadhi]

Some issues with pointers.

(They were not caught because the tests are not run with --pointer-check)

[SaswatPadhi]

The CI failures are due to .desc files being out of sync. You should also update *x -> x in those files.

Minor comment on the commit description: please change a new predicate __CPROVER_loop_entry -> a new unary expression __CPROVER_loop_entry. __CPROVER_loop_entry is not a predicate (a bool-returning function).

[chrisr-diffblue]

Approved, pending fixing the issue @SaswatPadhi has mentioned with --pointer-check