Concurrency: treat updates to an unknown field as atomic

[tautschnig]

Writing to an object that is composed of multiple fields is generally
treated in a field-sensitive (and thus: single-field) manner, which had
fixed several issues in handling shared arrays or structs. When the
specific field being updated cannot be determined during symbolic
execution (as is the case with non-const indices into arrays), we update
all fields that make up the full object. Such a full-object update must
then be treated as an atomic operation to avoid losing intermittent
writes performed by other threads.

Fixes: #123

• 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

Patch coverage: 100.00% and project coverage change: +0.09 🎉

Comparison is base (535e6b2) 78.38% compared to head (f5b35b4) 78.48%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #6123      +/-   ##
===========================================
+ Coverage    78.38%   78.48%   +0.09%     
===========================================
  Files         1686     1686              
  Lines       192915   192926      +11     
===========================================
+ Hits        151215   151412     +197     
+ Misses       41700    41514     -186     

Impacted Files	Coverage Δ
src/goto-symex/goto_symex.cpp	98.67% <100.00%> (+0.02%)	⬆️

... and 20 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[martin-cs]

Thanks for the comment that makes this clear but ... I am a little concerned about this because now
struct s = t; and

struct s;
s.x = t.x;
s.y = t.y;

can have different behaviour. I guess there is a very valid question about what the atomic actions in the CPROVER concurrency model are.

[tautschnig]

Although this case shouldn't arise for structs and mainly affects arrays: you are absolutely right that this is questionable either way. Without this patch, we'll have spurious results (as documented in the regression test). With this patch, we may miss some behaviour, depending on what exactly we otherwise consider to be atomic.