Value sets must not be field sensitive for unions

[tautschnig]

Distinct fields in a union need not refer to distinct memory locations.
Thus treat all fields of a union the same, with pointers assigned to any
field being dereferenceable via another field.

Fixes: #5263

• 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.
• n/a 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).
• n/a 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

Merging #5713 (1b73ae5) into develop (932599e) will decrease coverage by 0.01%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5713      +/-   ##
===========================================
- Coverage    69.51%   69.49%   -0.02%     
===========================================
  Files         1243     1243              
  Lines       100695   100695              
===========================================
- Hits         69994    69979      -15     
- Misses       30701    30716      +15     

Flag	Coverage Δ
cproversmt2	43.26% <100.00%> (-0.02%)	⬇️
regression	66.38% <100.00%> (-0.02%)	⬇️
unit	32.25% <100.00%> (ø)

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

Impacted Files	Coverage Δ
src/pointer-analysis/value_set.cpp	78.39% <100.00%> (ø)
src/util/simplify_expr_struct.cpp	69.23% <0.00%> (-16.49%)	⬇️

---

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 932599e...1b73ae5. Read the comment docs.

[kroening]

It might be worth adding a comment in line 1286 to say that this case also covers unions.

[thomasspriggs]

Looks good to me. It makes sense to prioritise soundness over speed. Do you know how much of a performance difference this change makes? Do you have any ideas for doing field sensitivity for unions in a sound fashion?

[tautschnig]

Looks good to me. It makes sense to prioritise soundness over speed. Do you know how much of a performance difference this change makes? Do you have any ideas for doing field sensitivity for unions in a sound fashion?

I haven't seen a performance penalty so far, and have more far-reaching union-related changes in the queue that do improve performance for me. I believe that, at present, a fair comparison is not possible, because we're simply missing the right entries from the value set and thus performance is, well, rather arbitrary. Performance might even be improved by this patch, because pointers can now be dereferenced and symex can work with actual objects when previously we'd try to work with __CPROVER_memory.