CONTRACTS: force success for necessary pointer predicates

[remi-delmas-3000]

Force success for pointer predicates that must necessarily hold if they ever get invoked in an assumption context. This ensures that the value sets of pointers as as small as possible after assuming a requires or an ensures clause and solves a performance issue with z3. All predicates in the cprover_contracts.c library now have an extra input may_fail controlling the failure behaviour, DFCC instrumentation sets the may_fail parameter to true or false using a recursive downwards propagation algorithm that takes into account the shortcutting behaviour of ==>, && and ||. This applies to all predicates (pointer_equals, is_fresh, pointer_in_range and obeys_contract for function pointers).

The test that regressed due to #8562 now passes again.

Example

void foo(int len_a, int* a, int len_b, int *b)
__CPROVER_requires(len_a > 0 ==> is_fresh(a, len_a) && len_b > 0 ==> is_fresh(b, len_b));

Is tagged as follows :

                         AND[F]
                ___________|_____________
               /                         \
              /                           \
         IMPLIES[F]                    IMPLIES[F]
          /      \                     /         \
        /         \                   /           \
 len_a>0[T]   is_fresh(a,len)[F]  len_b>0[T] is_fresh(b,len_b)[F]

In order for the the requires clause to hold when assumed, the is_fresh predicates in the RHS of implications
must not fail if they ever get invoked, those left of disjunctions may fail

Example

void foo(int len, int* a, int *b, int *c, int *d)
__CPROVER_ensures(
   is_fresh(a, len) && 
   is_fresh(b, len)  && 
   is_fresh(c, len) && 
   (pointer_equals(d, a) || pointer_equals(d, b) || pointer_equals(d, c))
)

Will be tagged

                                     AND[F]
                 ____________________|___________________________
                /                /                   |           \
               /                /                    |            \
              /                /                     |             \
    is_fresh(a,len)[F]  is_fresh(b,len)[F]  is_fresh(c,len)[F]    OR [F]
                                                                ______|_________
                                                               /      |         \
                                                              /       |          \
                                                             /        |           \
                                                 ptr_eq(d,a)[T]  ptr_eq(d,b)[T]  ptr_eq(d,c)[F]

The top conjuncts may not fail for the whole expression to hold, and the last element of the disjunction may not fail if it ever gets invoked after all other leftmost disjuncts may have failed.

• 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

Attention: Patch coverage is 46.46465% with 53 lines in your changes missing coverage. Please review.

Project coverage is 78.87%. Comparing base (d4757e2) to head (3ddd4b6).
Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
.../contracts/dynamic-frames/dfcc_wrapper_program.cpp	38.57%	43 Missing ⚠️
...t/contracts/dynamic-frames/dfcc_pointer_equals.cpp	50.00%	4 Missing ⚠️
...t/contracts/dynamic-frames/dfcc_obeys_contract.cpp	40.00%	3 Missing ⚠️
...contracts/dynamic-frames/dfcc_pointer_in_range.cpp	66.66%	2 Missing ⚠️
...trument/contracts/dynamic-frames/dfcc_is_fresh.cpp	80.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8574      +/-   ##
===========================================
- Coverage    78.94%   78.87%   -0.07%     
===========================================
  Files         1732     1732              
  Lines       198845   199066     +221     
  Branches     18351    18560     +209     
===========================================
+ Hits        156974   157021      +47     
- Misses       41871    42045     +174     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[hanno-becker]

mlkem-native CI running for this PR here: pq-code-package/mlkem-native#688

[hanno-becker]

This is looking good @remi-delmas-3000; mlkem-native CI passing on pq-code-package/mlkem-native#688 without noticable performance regresisons. Thanks a lot 🎉!