Don't use the broken overflow builtins for pointers

[danielsn]

Description of changes:

Currently, we emit __builtin_overflow_p operations for pointer arithmetic. This is basically broken, since CBMC converts to integers and does integer arithmetic under the hood, which is not what we want.

Resolved issues:

Initial step towards addressing #786

Call-outs:

1. This relies on --pointer-overflow-check being used on CBMC for soundness. We currently do so, but it would be better to have a __pointer_overflow builtin we could use when we need this behaviour. The overflow intrinsics have surprising behaviour on pointer arithmatic diffblue/cbmc#6627

2. Also fixed some confusing missing brackets in the typechecking code for binops.

Testing:

• How is this change tested? Existing regression 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.

[adpaco-aws]

Good to restrict this case to integers because I do not think we were handling floating point numbers anyway.

[celinval]

I don't have a lot of context here, but I thought that was the goal of these checks. They were complementary to CBMC pointer checks. These were just making sure the arithmetic operations would not overflow.

One could argue that they are redundant but I don't know if broken is how I would describe them.

[celinval]

Can you please add a test that would trigger the overflow to ensure the verification will still fail due to other checks?

[danielsn]

Can you please add a test that would trigger the overflow to ensure the verification will still fail due to other checks?

Done

[danielsn]

I don't have a lot of context here, but I thought that was the goal of these checks. They were complementary to CBMC pointer checks. These were just making sure the arithmetic operations would not overflow.

One could argue that they are redundant but I don't know if broken is how I would describe them.

The issue is that the semantics of the arithmetic operation being done, and the semantics of the check, don't line up. The arithmetic operation is doing pointer arithmetic, while the overflow check is doing integer arithmetic. So its possible for the actual addition to overflow, but the overflow check to report no overflow.

[celinval]

I don't have a lot of context here, but I thought that was the goal of these checks. They were complementary to CBMC pointer checks. These were just making sure the arithmetic operations would not overflow.
One could argue that they are redundant but I don't know if broken is how I would describe them.

The issue is that the semantics of the arithmetic operation being done, and the semantics of the check, don't line up. The arithmetic operation is doing pointer arithmetic, while the overflow check is doing integer arithmetic. So its possible for the actual addition to overflow, but the overflow check to report no overflow.

Can we account for the type size?

[celinval]

I believe this change is currently blocked waiting for a CBMC fix to be released. @danielsn Please let us know once this is ready for review again. Cheers!