Function contracts: check target validity, simplify snapshot instrumentation

[remi-delmas-3000]

In assigns clause checking, for better usability and performance with conditional targets:

• Check that user-specified targets point to non-invalid locations when their condition holds
• Replace the all_dereferences_valid with a simpler not_null check in the validity condition, remove conditional jumps
• Rewrite inclusion checks to tolerate NULL targets only when necessary (calls to 'free')

Benefits:

• Detect and report errors user-specified target conditions
• Up to x1.5-x2 faster runs on large benchmarks (from ~1800s to ~900s on large s2n-tls benchmarks)

Details

Problem

We now support conditional assigns targets of the form condition: target.

The condition lets the user specify when the target expression is assignable by the function.

We also need to make sure the target expression denotes a valid memory location when the condition holds.

Today this is achieved using this instrumentation code:

bool __car_valid := condition & all_dereferences_valid(target) & w_ok(target_start_address, target_size);
char *__car_lb := NULL;
char *__car_ub := NULL;
if(__car_valid)
{
  __car_lb := start_address_of(target);
  __car_ub := __car_lb + target_size(target); // this instruction is instrumented with pointer overflow checks
}

Inclusion checks are performed using:

ASSERT __car_valid ==> is_included(car, set-of-legit-locations)

With this encoding, if the target expression happens to be invalid when the user-provided condition is true, we silently compute an empty conditional address range and we will reject assignments to this invalid target location (as expected),

The results can however be hard to interpret from the user's perspective since he does not know that the target is invalid when he specified it should be assignable. It is most likely the sign of an involuntary error in the target condition

Moreover, the use of all_dereferences_valid and w_ok predicates creates large formulas and causes long runtimes.

Proposed Fix

We distinguish the following uses for an address range snaphsot (__car_valid, __car_lb, __car_ub):

1. Snapshotting a user-specified conditional target found in an assigns clause. In that case:
   a. when the condition holds, the target_start_address pointer shall be either NULL or writable with the expected size. We allow NULL because it can be passed as a valid argument to functions such as free(), and the user code might attempt to do this.
   b. we forbid invalid target_start_address pointers because they are not accepted in any meaningful operation.
2. Snapshotting the address range of a pointer passed to free(). The pointer must either be a NULL pointer or a pointer to the start address of a valid object (with offset 0, but we will not check that since free checks it itself).
3. Snapshotting the LHS of an assignment or an argument to a havoc function, in order to perform an inclusion check against a set of allowed target locations (themselves derived from cases 1 and 4). In that case:
   a. we want to check that the target_start_address is neither NULL nor INVALID when its condition holds.
4. Snapshotting a DECL or a pointer returned by malloc. Conditions 1.a. and 1.b. would apply here, but they are always satisfied by construction (a stack allocated var is always backed by an object of the right size for its type, and CBMC's malloc either returns a NULL pointer or a pointer backed by an object of the right size).

So, in order to check for target validity in cases 1. and 2. (user specified targets and parameters to free), we use:

ASSERT condition ==> (target_start_address == NULL || w_ok(target_start_address, target_size)) ;

To check for target validity in case 3. (assignment LHS), we use:

ASSERT condition ==> w_ok(target_start_address, target_size);

These assertions will be falsified if target_start_address is an invalid pointer.

As explained above, in case 4 the target is valid by construction, so we do not generate an assertion.

In cases 1, 2, 3 and 4 the snapshot is rid of conditional jumps and becomes:

bool __car_valid := condition & not_null(target_start_address);
__car_lb := target_start_address;
__car_ub := __car_lb + target_size(target);

Assuming the "target validity" assertion was proved, if condition & not_null(target_start_address) holds then w_ok(target_start_address, target_size) holds and the computed __car_lb and __car_ub are meaningful.

If the target happens to be NULL, __car_valid will be false and __car_lb and __car_ub will contain garbage values but will never be used in inclusion checks, which are guarded by __car_valid.

If the target happens to be invalid, then all snapshot variables can take arbitrary and incoherent values which may or may not fail the inclusion checks. In all cases, since the target validity assertions will surely fail, the assigns clause checking analysis as a whole will not succeed.

Inclusion checks

The inclusion check for assignments and havoc parameters is written as:

ASSERT __car_valid & is_included(car, set-of-legit-locations);

An for parameters to free we allow NULL as a special case:

ASSERT target_start_address!=NULL ==> __car_valid & is_included(car, set-of-legit-locations);

Summary

With this new encoding,

• we can detect bad conditions which allow invalid targets in assigns clause specifications,
• we remove conditional jumps and extra pointer assertions

For a full assigns clause check to be considered successful:

• the user specified targets must all pass the target validity checks
• all assignments and arguments to havoc or free must pass the inclusion check

---

• 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 #6564 (ec3902c) into develop (9ba013d) will decrease coverage by 0.00%.
The diff coverage is 98.24%.

@@             Coverage Diff             @@
##           develop    #6564      +/-   ##
===========================================
- Coverage    76.01%   76.01%   -0.01%     
===========================================
  Files         1579     1579              
  Lines       181304   181303       -1     
===========================================
- Hits        137819   137817       -2     
- Misses       43485    43486       +1     

Impacted Files	Coverage Δ
src/goto-instrument/contracts/assigns.h	100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
...trument/contracts/havoc_assigns_clause_targets.cpp	97.72% <ø> (-0.72%)	⬇️
src/goto-instrument/contracts/assigns.cpp	95.86% <97.50%> (-0.49%)	⬇️
src/goto-instrument/contracts/contracts.cpp	91.37% <100.00%> (+0.09%)	⬆️
src/goto-instrument/contracts/utils.cpp	89.69% <100.00%> (+0.32%)	⬆️

---

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 29584b3...ec3902c. Read the comment docs.