Audit copy_nonoverlapping intrinsic

[adpaco-aws]

Description of changes:

Completes the audit for the copy_nonoverlapping intrinsic by reusing the work done on the copy intrinsic (see #1199):

• Adds alignment checks for both src and dst.
• Adds overflow check for the count in bytes (this is not mentioned in the documentation).
• Adds tests for all possible cases.

Resolved issues:

Resolves #1198
Part of #1163

Testing:

• How is this change tested? Existing regression and new tests

• Is this a refactor change? No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thanks for reducing the duplicated code. I just have a few comments besides my previous comment that I published too soon. ☺️

[celinval]

Is this a CBMC message? I was wondering if we change it to say copy_nonoverlap here. Do we use memcpy anywhere else?

[adpaco-aws]

Yes, this is a CBMC message so there's not much we can do. We use memcpy in our __rust_realloc C implementation but we don't generate calls to memcpy anywhere else.

[celinval]

Looks good! Thanks