Simplify multiple-of-element size access to arrays

[tautschnig]

Array operations may fall back to byte_extract or byte_update expressions in parts of the code base. Simplify this to index or WITH expressions, respectively, when the offset is known to be a multiple of the array-element size.

• 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

Attention: Patch coverage is 92.76316% with 11 lines in your changes missing coverage. Please review.

Project coverage is 80.38%. Comparing base (3c915eb) to head (ba35ebf).
Report is 4 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/util/simplify_expr.cpp	93.93%	6 Missing ⚠️
src/util/pointer_offset_size.cpp	90.56%	5 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff            @@
##           develop    #8627    +/-   ##
=========================================
  Coverage    80.37%   80.38%            
=========================================
  Files         1686     1686            
  Lines       206885   207022   +137     
  Branches        73       73            
=========================================
+ Hits        166276   166405   +129     
- Misses       40609    40617     +8     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[remi-delmas-3000]

Is there a way to share some of the pattern matching conditions between the array-read and array-write cases ?

[remi-delmas-3000]

Seems like we should also be able to pattern match an access to a member of a struct in an array of structs like a[i].m, the offset would be of the form i*sizeof(T) + offset(T,m) and turn that into a functional update as well ?

[tautschnig]

Seems like we should also be able to pattern match an access to a member of a struct in an array of structs like a[i].m, the offset would be of the form i*sizeof(T) + offset(T,m) and turn that into a functional update as well ?

Done.

[remi-delmas-3000]

From my understanding of the code the cases where we have a symbolic offset value with some shape that does not properly align with the underlying type of the accessed object seem to be handled, but could we add some negative tests for that ?

i.e. tests that check that the array access or array update still reduce to byte-level operations when they are supposed to ?

Also I just thought of the case you mentioned is frequent in the linux kernel, where people access struct fields using a base_pointer + offsetof(T, field), or accessing some array from its end pointer with a negative offset, which I don't think are handled.