String Literals Domain

[nathanschmidt]

This PR extends the base analysis with cases for strcpy (adapted), strncpy, strcat, strncat, strlen, strstr, strcmp and strncmp. The following scenarios can now be analyzed:

• If the parameter dest of strcpy, strncpy, strcat or strncat potentially is a string literal, Goblint will now warn about a possible undefined behavior. For this purpose, the previous implementation of strcpy had to be adapted.
• If all the potential values of the parameters of the functions strlen, strstr, strcmp and strncmp are string literals, Goblint can now compute the exact return value of these functions.

I also added two regression tests, both with assertions that can now be tracked and assertions for which the String Literals Domain can still not make any assertion.
Note: The regression tests fail on MacOS while they succeed on Linux. I couldn't yet figure out why that is the case.

[sim642]

@sim642 You had some way to debug OS X things iirc? Do you mind sharing how that worked again?

The CI summary page has a suite_result artifact at the bottom, which contains all the logs from the failed OSX job.

[sim642]

I suspect this might not be so easy because C strings and OCaml strings are different. In particular a string literal "hello\0world" would have strlen 5, but the OCaml string has length 11.
The same probably applies to other length-related functionality as well.

Maybe CIL has some helper functions for manipulating strings with C semantics?

[nathanschmidt]

That's absolutely right, again thank you for thinking about this case! I couldn't find a CIL function that would help me in this case in a quick search, but I'll have another look. Otherwise, String.split_on_char '\x00' x and taking the first element of the resulting list would do the trick.

[sim642]

It is now fixed for strlen, but I think it still needs to be fixed for some of the other functions. I think it matters for strstr and strcmp as well. Right now they're just performing the operations on OCaml strings, but all of those operations need to be performed with C semantics, so only up to the NUL byte considered when checking for inclusion etc.

I'm wondering if a better solution is to maybe just do the stripping initially, so it doesn't have to be done for every operation individually. Or maybe CIL is already doing that as well?
I haven't checked, but it would be good to have tests for these things. If sv-benchmarks doesn't contain such cases, it would be nice to also contribute those because this detail is easy to get wrong and become unsound.

[nathanschmidt]

My first assumption was that CIL would cut the string at the first NULL byte, that's why I didn't do the stripping. After your comment, I tested this and found out that's not the case.

As you're right that this also concerns strstr and str(n)cmp, I introduced a new function to_c_string performing the stripping which I now use accross all my other functions. I didn't change to_string as some parts of the base analysis not related to my PR rely on it.

I added a new 02-string_literals_with_null.c test to verify this edge case is now correctly covered.

[michael-schwarz]

@sim642 do you want to do a final pass or are you good with merging?