Vsd - widening during abstract object merge

[jezhiggins]

Implements widening during abstract object merges.

Widening during a merge is determined by the trace_ptrt locations passed into variable_sensitivity_domaint::merge. When widening should occur hasn't been changed, what this PR does is actually try and widen when requested.

If a merge result is unmodified, no widening will take place.

Constants don't need to be widened - rather, they already do because they go TOP.

For intervals, we consider which bound is being extended by the merge then extend that further out by the width of the interval. Eg.

• normal merge of [1, 3] with 4 results in [1, 4]
• widening merge of [1,3] with 4 results in [1, 8].
  • The merge result [1, 4] has been extended on the upper bound (4 > 3).
  • The interval width is also 4, so the new upper bound is 4 + 4, hence [1, 8]
• widening merge of [4, 5] with -1 results in [-4, 5]
  • The merge result [1, 5] has been extended on the lower bound (1 < 4).
  • The interval width is 5, so the new lower bound is 1 - 5, hence [-4, 5].
    If the merge extends both upper and lower bounds, we extend at both ends.

For value-sets, a similar mechanism is applied. If the upper or lower value in the set has changed in the merge, we extend that further, either by replacing a constant value with an interval or by extending the interval. Eg.

• merging { 1, 3 } with 4 gives { 1, 3, 4 }
• widening merge of { 1, 3 } with 4 results in { 1, 3, [4, 8] }

This PR also includes value-set compacting. When a value-set becomes large, that is has more than value_set_abstract_objectt::max_value_set_size elements, it is compacted. This has two stages

• non-destructive compacting - if the set contains any intervals, combine overlapping intervals together and then discard any values contained in those intervals
  • compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [5, 12] } would give { 1, 2, 3, 4, [5, 12] }
  • compacting { 1, 2, 3, 4, 5, 7, 8, [5, 10], [8, 12] } would give { 1, 2, 3, 4, [5, 12] }
  • compacting { [1, 4], 1, 2, 4, 5, 6, 7, [8, 10], [6, 12] } would give { [1, 4], 5, [6, 12] }
    If the value-set is still too large, we move to the second stage
• destructive compacting - creating new intervals in value-set, then reapplying the non-destructive compact.
  • the intervals span the lower and upper third of the set's range
  • so { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 } would become { [1, 4], 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, [9, 12] }, which would compact to { [1, 4], 5, 6, 7, 8, [9, 12] }.
  • if value set is still too large (because of outlier values), split the value-set into two intervals spanning the lower and upper half of the range.

[codecov]

Codecov Report

Merging #6046 (48146e0) into develop (0002950) will increase coverage by 7.94%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6046      +/-   ##
===========================================
+ Coverage    67.40%   75.35%   +7.94%     
===========================================
  Files         1157     1454     +297     
  Lines        95236   160914   +65678     
===========================================
+ Hits         64197   121253   +57056     
- Misses       31039    39661    +8622     

Flag	Coverage Δ
cproversmt2	?
regression	?
unit	?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	52.94% <0.00%> (-47.06%)	⬇️
src/solvers/prop/prop.cpp	42.85% <0.00%> (-41.76%)	⬇️
src/solvers/flattening/boolbv_member.cpp	53.65% <0.00%> (-38.65%)	⬇️
src/cpp/cpp_storage_spec.cpp	65.00% <0.00%> (-35.00%)	⬇️
src/util/cmdline.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/array_pool.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/string_refinement.h	66.66% <0.00%> (-33.34%)	⬇️
...rs/strings/string_concatenation_builtin_function.h	0.00% <0.00%> (-33.34%)	⬇️
src/cbmc/c_test_input_generator.cpp	60.00% <0.00%> (-30.33%)	⬇️
src/ansi-c/c_typecheck_base.cpp	55.76% <0.00%> (-25.13%)	⬇️
... and 1433 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 f847fcd...48146e0. Read the comment docs.

[martin-cs]

Although the PR is large, it seems the changes are mostly pretty straight-forward and a lot of it is tracing the extra parameter to merge through the various interfaces.