[DRAFT] Support MMIO regions

[danielsn]

Description of changes:

Adds support for MMIO regions to kani proof harnesses.

Resolved issues:

Resolves #1304

Call-outs:

• [ ] This is dependent on https://github.com/diffblue/cbmc/pull/6747. It will not work until that is released. I tested against a locally built copy.
• [ ] We need documentation for this feature
• [x] Should probably add some negative tests too
• [ ] Should test that it behaves like MMIO: writes don't need to be the same as is read back, two reads can get different values

Testing:

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

[kroening]

Why not simply have --mmio_region enabled by default?

[kroening]

Why not simply have --mmio_region enabled by default?

(Ignore, it is already)

[celinval]

@danielsn any news here?