MRA Region Injection Bugs

[l-kent]

MRAMemoryRegionSystemTestsGTIRB still fails for the test correct/initialisation/gcc:GTIRB and MRAMemoryRegionSystemTestsBAP still fails for the tests correct/initialisation/gcc:BAP and correct/initialisation/clang_O2:BAP.

These tests fail because of issues with reconciling the size of an array a in the symbol table with the smaller array accesses that actually occur in the program. The array a is an array of two 32-bit/4-byte values. The symbol table lists it as 64-bit, but each access to a[0] or a[1] in the program is a 32-bit access to either the address of a or a + 4 and this is not handled properly, as the smaller accesses are overridden by the larger size in the symbol table. This causes inconsistencies between the GRA results and the DataRegions in the MMM, leading to incorrect regions created in the Boogie output. This is quite difficult to untangle at the moment.

There are further difficulties as the GRA and MRA use 1 byte as the default size of a DataRegion, including as a placeholder that is later overridden, but this is also a valid access size for 1 byte accesses.

[l-kent]

There is additionally some sort of non-determinism issue with these tests.

When running testOnly MRAMemoryRegionSystemTestsBAP -- -z correct/initialisationMRAMemoryRegionSystemTestsBAP and testOnly MRAMemoryRegionSystemTestsBAP -- -z correct/initialisationMRAMemoryRegionSystemTestsGTIRB, the number of tests that succeed is random.