Change Machdep based on SV-COMP architecture

[sim642]

Closes #54, at least for SV-COMP usage.

TODO

• Merge Generate 32bit and 64bit Machdep if possible cil#173.
• Why doesn't fix Unsoundness on SV-COMP for No-Overflow & Memory Properties #1385/SV-Comp incorrect result in no-overflow tasks #1501? It has overflow in cast.
• Add tests.
• Run on sv-benchmarks.
• Fix MacOS CI.

[sim642]

The sv-benchmarks results (with 60s timeout) indicate some changes to verdicts:

• 32 tasks go from unknown to true thanks to the more precise bounds we use for ILP32.
• 56 tasks go from true to unknown which are all cases of previous unsoundness: we assumed larger type bounds for some no-overflow tasks than they actually have and were simply lucky to still have sound verdicts.
• 55 tasks go from true to EXCEPTION (IntDomain.IncompatibleIKinds) which for some reason all are valid-memsafety tasks.

[michael-schwarz]

I think we should investigate the 55 new EXCEPTION (IntDomain.IncompatibleIKinds exceptions before merging, while we still have an idea of what could be the case.

Also, when this is addressed, I think it makes sense to do a full ressource run the state before this and after it on server01 here before merging. I can start it if you ping me.

[sim642]

I just made a fix ea2f616 which fixes one of those. I'm doing another quick run to see if that covers all of them.
EDIT: It fixes all those cases, so you can try a full resources run @michael-schwarz.

[michael-schwarz]

The runs for the context gas values are now finished, I just started the comparison run on the current master (approx 24h), and will then start the run with this after.

[michael-schwarz]

In the meantime, there seems to be some problems with OS X left here.

[michael-schwarz]

The comparison run I started yesterday has finished this morning, I Just started https://github.com/goblint/analyzer/tree/staging_machdep-arch now.

[michael-schwarz]

Good to go from my view as soon as the OS X issue is fixed.

[sim642]

For now I disabled the test on MacOS. But I also added error messages about the missing machine definition. At least it's still possible to do SV-COMP runs on MacOS for ILP32 tasks but there will be a clear message about the possible unsoundness. The alternative would be to just crash when the machdep is missing, but that might be too harsh and inconvenient (because -m64 probably also doesn't work).

In the future we might want to provide pre-generated machdeps in CIL (at least for type sizes if not all machdep components). That should be enough for SV-COMP where preprocessing isn't needed.