[CONTRACTS] Check side effect of loop contracts during instrumentation

[qinheping]

Now, CBMC check side effect of loop contracts in goto_convertt by rejecting all side_effect_exprt. However, we might want to accept side-effect loop contracts and remove the side effect during instrumentation, or accept side_effect_exprt which is actually side-effect free (see the added regression test of this PR as an example).

This PR postpone the check of side effect of loop contracts from code converting to the actual instrumentation time. It also provide a new options to disable the side-effect check.

This PR include the commit from #8359. The regression test added in this PR also test #8359 (introducing new symbols) and #8282 (containing a GOTO jump in the loop invariant).

• 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.

[remi-delmas-3000]

Allowing arbitrary side_effect_exprt allows things like __CPROVER_is_fresh and __CPROVER_r_ok to be used in the loop invariant. Since __CPROVER_r_ok might not work as expected in assumption contexts, and since the semantics if __CPROVER_is_fresh is only well defined in the context of requires and ensures clauses relative to some call site, we still may want to ban them for now.

Also if when using DFCC, all functions of the model are extended with a write set parameter, and any function called in the loop invariant must be passed either a write set pointer, either NULL (in which case no checks will be done) or a valid pointer to some write set (and checks will be performed).

But we should try to actually check for side effects semantically using DFCC and an empty write set.

We already do it for preconditions and postconditions in function contracts
see here

You can declare and build the write set in PREFIX program

// PREFIX
DECL ws : write_set_t ;
DECL ws_ptr : write_set_t* ;
ASSIGN ws_ptr = &ws;
CALL write_set_create(
ws_ptr,
assigns_size = 0,
frees_size = 0,
replacement_mode = false, ... );

Then you goto-convert the invariant clause and instrument the resulting program snippet against the empty write set:

 // will contain the invariant evaluation
goto_programt loop_inv_prog;
converter.goto_convert(loop_inv, loop_inv_prog, language_mode);
// fix calls to memory predicates like `__CPROVER_is_fresh`
memory_predicates.fix_calls(loop_inv_prog);
loop_inv_prog.add(goto_programt::make_end_function());
instrument.instrument_goto_program(
    prog_id,
    loop_inv_prog,
    ws_ptr, // symbol that represents the empty loop invariant write set
    function_pointer_contracts);
// turn it back into a sequence of statements
requires_program.instructions.back().turn_into_skip();

Then generate a SUFFIX program that checks that evaluating the invariant did not allocate of free any memory, release the write set :

// SUFFIX
DECL __check_no_alloc: bool;
// checks that evaluating the invariant did not use malloc or free
CALL __check_no_alloc = check_empty_alloc_dealloc(requilres_write_set);
ASSERT __check_no_alloc;
DEAD __check_no_alloc: bool;
CALL write_set_release(ws_ptr); // releases resources used by the write set.
DEAD ws_ptr;
DEAD ws;

Finally concatenate the PREFIX, invariant evaluation program and SUFFIX, and insert the into the program at the base case and step case locations.

This will ensure that the invariant expression has no side effects, and since it uses the global DFCC instrumentation system, it will also work if the side_effect_exprt of the invariant is a call to a function that also calls other functions, etc.

[qinheping]

Thank you @remi-delmas-3000 ! Yes, I think it is really good idea to apply the dfcc side-effect checks here.
However, it should be implemented in a following PR. This PR only moves the current checks from typechecking time to instrumentation time, and add a flag to disable side-effect check to allow us experiment kani loop contracts while we develop the new side-effect checks.

[codecov]

Codecov Report

Attention: Patch coverage is 82.75862% with 10 lines in your changes missing coverage. Please review.

Project coverage is 78.25%. Comparing base (66ae03f) to head (2d416e1).
Report is 30 commits behind head on develop.

Files	Patch %	Lines
...trument/contracts/dynamic-frames/dfcc_cfg_info.cpp	72.72%	6 Missing ⚠️
src/cprover/instrument_given_invariants.cpp	50.00%	2 Missing ⚠️
src/goto-instrument/contracts/utils.cpp	92.00%	2 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8360      +/-   ##
===========================================
- Coverage    78.34%   78.25%   -0.10%     
===========================================
  Files         1726     1726              
  Lines       188437   188696     +259     
  Branches     18244    18252       +8     
===========================================
+ Hits        147638   147663      +25     
- Misses       40799    41033     +234     

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

[remi-delmas-3000]

One minor optional comment about option naming.

[tautschnig]

I'm ok with this other than as indicated in the comment below, provided that there will be follow-up work that will make this option completely unnecessary and we instead check for which side effects we genuinely cannot tolerate.