Track deallocated/dead in an array

[tautschnig]

This enables tracking of all deallocations and all dead objects, and
thereby use of deallocated/dead_object predicates within assumptions.

This requires performance evaluation.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Base: 77.92% // Head: 77.96% // Increases project coverage by +0.03% 🎉

Coverage data is based on head (5be34fb) compared to base (50c43e2).
Patch coverage: 74.74% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #6506      +/-   ##
===========================================
+ Coverage    77.92%   77.96%   +0.03%     
===========================================
  Files         1616     1616              
  Lines       186814   186798      -16     
===========================================
+ Hits        145580   145628      +48     
+ Misses       41234    41170      -64     

Impacted Files	Coverage Δ
src/analyses/interval_analysis.cpp	0.00% <0.00%> (ø)
src/ansi-c/ansi_c_internal_additions.cpp	90.12% <ø> (ø)
src/goto-instrument/race_check.cpp	0.00% <0.00%> (ø)
.../goto-instrument/synthesizer/synthesizer_utils.cpp	92.85% <ø> (-0.17%)	⬇️
src/goto-instrument/thread_instrumentation.cpp	0.00% <0.00%> (ø)
src/goto-instrument/undefined_functions.cpp	0.00% <0.00%> (ø)
src/goto-programs/string_instrumentation.cpp	25.11% <0.00%> (ø)
src/linking/linking_class.h	100.00% <ø> (ø)
src/util/c_types.cpp	91.16% <ø> (+1.97%)	⬆️
src/util/c_types.h	100.00% <ø> (ø)
... and 44 more

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

[tautschnig]

The above scatter plot shows current develop (y axis) vs this proposed change (x axis) on SV-COMP's MemSafety-Heap category. This one is the benchmark set with the strongest negative signal I have found so far (several others show no significant difference, some even an improvement): on this benchmark set, CBMC is now only able to solve 140 instead of 145 tasks within the resource limits. Three of those that can no longer be solved now run out of memory, two trigger a bug (fixed in #6772). This is perhaps to be expected for we end up making use of the array theory, which may generate a lot of extra constraints.

Despite this data, I'd like to see this change being considered for inclusion as it would alleviate subtle usage limitations of __CPROVER_r_ok (it would now be safe to be used in assumptions), and might even make it possible to get rid of --pointer-primitive-check at some point, which is an option that is hard to explain to users.

[peterschrammel]

What are the special characteristics of the benchmark that is such an outlier?

[tautschnig]

What are the special characteristics of the benchmark that is such an outlier?

I'd say: a lot of objects to track where constant propagation might be unable to pick out one specific object each time there's a read to the array newly introduced in this PR. Two trouble makers are https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-ext-properties/test-0217_1.c and https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/memsafety/test-0235-3.c.

There are also two tests that appear to cause an invariant failure that may point to a bug elsewhere.

[tautschnig]

There are also two tests that appear to cause an invariant failure that may point to a bug elsewhere.

This bug is now addressed by #6772. The more frequent use of this code via this PR just made it visible.