SV-COMP "Memory Safety" benchmark additions

[mrstanb]

This PR:

• Builds upon changes from the https://github.com/goblint/analyzer/tree/staging_memsafety branch that was used for the first benchmark runs of Goblint against the SV-COMP "Memory Safety" benchmarks
• Adds (first and hacky) support for recognizing all three memory safety properties of SV-COMP (i.e., valid-free, valid-deref, valid-memtrack)
• Adds support for the valid-memcleanup property of SV-COMP

TODO:

• Try out the changes from Add attribute goblint_cil_nested to local varinfos that are not declared at top scope cil#155 for a further benchmark run as well

[sim642]

Why does this need to be an option at all? There's no harm in having the attribute.

[michael-schwarz]

There is when you do justcil, as it will cause many compiler warnings and pollute files. If we want to keep using Goblint to create merged files, we should keep this option imo.

[sim642]

Seems to me that it'd be better to make CIL's printer not just print these special attributes like it already does with some others.
That would avoid this annotation from ever making it to the output, even when you want to both enable it (for memory analyses) and also print the merged file. Currently those annotations would be in the merged file explicitly, so reanalyzing the merged file would incorrectly have some of these attributes on variables which are all pulled up to the function level. If the attribute wasn't printed, there wouldn't be a spurious attribute which would be incorrectly placed onto pulled-up variables.

[michael-schwarz]

I thought about it, but decided against it in the end: the reasoning was that I want some way to inspect where these attributes were put.

[michael-schwarz]

Maybe always adding them and then adding an option to CIL (and here) to disable or enable printing them would be a way to achieve everything @sim642?
If yes, I can do this in a follow-up PR.

[sim642]

Maybe, but I don't consider this to be a blocking thing. I just hoped we could get away without introducing new options that allow Goblint to be used in some unintended ways. E.g. enable memory analyses but disable this option (even by default).

Right now the automation is only in the autotuner that isn't enabled by default. So maybe our check_arguments should have a case for it to prevent this.

[michael-schwarz]

I added a corresponding case to check_arguments now.

[sim642]

Due to the module moves in #1206 GitHub shows conflicts that are "too complex" to solve in the web editor. Actually you can locally just merge master into this branch and there shouldn't be any conflicts. GitHub's merge thing seems to have some move detection disabled that git should do by default.

[sim642]

I thought this was supposed to be sound, but apparently it's not. For example

./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/valid-memsafety.prp ../sv-benchmarks/c/loops/invert_string-2.c

prints SV-COMP result: true but the expected verdict if false(valid-deref).

[michael-schwarz]

It was sound when I last checked it, is this task new?

[sim642]

No, it's a random one I just picked to check. It was present in some BenchExec table that was attached here before and there it correctly returned unknown.

[michael-schwarz]

Maybe the autotuner is just not active in the setting you have given where svcomp.enabled is not set? I think it's something along these lines, we didn't do any fundamental changes since the last run.

[sim642]

conf/svcomp.json enables all of that though.

[michael-schwarz]

svcomp23-with-mem-safety.json

That was the config we used.

[michael-schwarz]

Maybe it's arrayoob that isn't set there?

[sim642]

Maybe it's arrayoob that isn't set there?

That seems to be it. I made the autotuner enable it automatically like it activates the analyses.

Although I'm surprised that the memOutOfBounds analysis doesn't check these bounds.