New option --mmio-regions to specify memory regions

[tautschnig]

This new option will enable us to eventually drop support for
__CPROVER_allocated_memory, which

1. requires awkward scanning of goto functions in goto_check_c,
2. wrongly suggests these declarations are limited to some scope, and
3. yields a spurious undefined-function warning in symex.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• 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.

[kroening]

Is that a 'check' or an 'instrumentation'?

[codecov]

Codecov Report

Merging #6747 (fafe18a) into develop (09e1041) will increase coverage by 0.00%.
The diff coverage is 83.33%.

@@            Coverage Diff            @@
##           develop    #6747    +/-   ##
=========================================
  Coverage    77.81%   77.82%            
=========================================
  Files         1570     1569     -1     
  Lines       180682   180565   -117     
=========================================
- Hits        140601   140522    -79     
+ Misses       40081    40043    -38     

Impacted Files	Coverage Δ
src/linking/linking.cpp	59.36% <68.96%> (+0.65%)	⬆️
src/ansi-c/goto_check_c.cpp	91.54% <90.90%> (-0.01%)	⬇️
src/analyses/does_remove_const.cpp	100.00% <100.00%> (ø)
src/crangler/mini_c_parser.cpp	72.58% <100.00%> (+1.55%)	⬆️
src/goto-instrument/replace_calls.cpp	89.70% <100.00%> (-0.15%)	⬇️
src/goto-programs/goto_program.cpp	81.80% <100.00%> (ø)
src/goto-programs/remove_function_pointers.cpp	92.79% <100.00%> (ø)
...nalyses/does_remove_const/does_expr_lose_const.cpp	100.00% <100.00%> (ø)
...ove_const/does_type_preserve_const_correctness.cpp	100.00% <100.00%> (ø)
...does_remove_const/is_type_at_least_as_const_as.cpp	100.00% <100.00%> (ø)
... and 3 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 365871d...fafe18a. Read the comment docs.

[tautschnig]

Is that a 'check' or an 'instrumentation'?

It affects what checks are generated (instrumented?).

[kroening]

It affects what checks are generated (instrumented?).

The test goes as follows: how would the flow with goto-cc look like?

[tautschnig]

It affects what checks are generated (instrumented?).

The test goes as follows: how would the flow with goto-cc look like?

I see two possible approaches we could take, with the current PR implementing the first variant, but we could also go for option 2 (or any other approach that I might not be aware of at this time):

1. goto-cc does not have awareness of MMIO regions. Checks added by goto_check_c are updated based on the information provided by --mmio-regions. Two invocations of CBMC on the same GOTO binary may use different MMIO regions and thereby may yield different verification outcomes.
2. goto-cc gets the --mmio-regions flag and adds such information to the architecture configuration, storing it in the GOTO binary as we already do for other architecture/platform aspects. Requires updating the GOTO binary version and users might have to change their compilation workflow. The advantage, however, is that the implementation is simpler in that we wouldn't have to update properties after the fact.

[jimgrundy]

I see two possible approaches we could take, with the current PR implementing the first variant, but we could also go for option 2 (or any other approach that I might not be aware of at this time):

1. goto-cc does not have awareness of MMIO regions. Checks added by goto_check_c are updated based on the information provided by --mmio-regions. Two invocations of CBMC on the same GOTO binary may use different MMIO regions and thereby may yield different verification outcomes.
2. goto-cc gets the --mmio-regions flag and adds such information to the architecture configuration, storing it in the GOTO binary as we already do for other architecture/platform aspects. ...

If "2" seems more like the the right thing to do, then let's do the right thing rather than the easy thing.

[danielsn]

Can we make sure this PR also adds documentation to the user manual about the behaviour of MMIO?

[TGWDB]

Documentation here: #7157

[jimgrundy]

@kroening - now that we have the requested documentation can we have approval for this PR?

[kroening]

CBMC should not get new options that change the model. Modeling should be done in goto-instrument, but not in CBMC. We should gradually remove model creation from CBMC.

[esteffin]

@tautschnig As a PR (#6748) depending on this is marked version 6, should this also be considered part of version 6?