Limit address sets to include at most one string pointer

[jerhard]

This PR changes the abstraction of a string pointer from StrPtr of string to StrPtr of string option. Now, a StrPtr None abstracts any possible string pointer.

As there is the possibility that there may the same string in the binary multiple times, the function is_definite was changed so that is_definite (StrPtr _) now returns false.

Closes #807

[michael-schwarz]

I think this behavior should be configurable via some option. Apart from that, it looks good!

[jerhard]

I think this behavior should be configurable via some option. Apart from that, it looks good!

Should this option be active by default or not? Probably makes sense to enable it for the defaults configurations for large and mid-sized programs.

[sim642]

I think this behavior should be configurable via some option.

Having an option is good indeed since we still have some use cases for distinguishing string pointers. Given the choice now, it looks to me like a choice between unit domain and flat domain (of strings) for StrPtr. Maybe it could even be implemented as such with an option like ana.base.strings.domain?

[jerhard]

Given the choice now, it looks to me like a choice between unit domain and flat domain (of strings) for StrPtr.

The flat domain of strings would, as-is, result in the behavior that limits address sets to contain at most one string pointer: The join of two different non-bottom elements yields Top in the flat lattice. The unit lattice would not be able to track any string pointer.

In case we want to implement the tracking of string pointers via other domains, one would require a flat-domain that raises a Lattice.Uncomparable when joining different non-bottom elements, if we want to keep the current behavior as an option.

[sim642]

The flat domain of strings would, as-is, result in the behavior that limits address sets to contain at most one string pointer: The join of two different non-bottom elements yields Top in the flat lattice. The unit lattice would not be able to track any string pointer.

In case we want to implement the tracking of string pointers via other domains, one would require a flat-domain that raises a Lattice.Uncomparable when joining different non-bottom elements, if we want to keep the current behavior as an option.

True, it'd be a flat lattice without lifted bottom and top. Lattice.Fake would be like that.

[michael-schwarz]

I think as it currently is is a good state. Replacing the string components with a further lattice only makes the code harder to read IMO.

[jerhard]

This assert currently succeeds, but in the concrete there's nothing saying the compiler must use the same constant.

In this PR, this asserts is unknown, as it should be, as I changed the is_definite (StrPtr _) to return false; as I mentioned above.

[michael-schwarz]

Yes, sorry, I did not read your comment above closely enough!

[jerhard]

With this option activated (by default), and the following command line, goblint terminates in 11:45h:

/goblint ../../benchmarks/sqlite-amalgamation-3370200/sqlite3.c ../../benchmarks/sqlite-amalgamation-3370200/sqlite3.h ../../benchmarks/sqlite-amalgamation-3370200/sqlite3ext.h ../../benchmarks/sqlite-amalgamation-3370200/shell.c -v --set pre.cppflags[+] -DSQLITE_DEBUG --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper

With the option deactivated, Goblint still has not terminated after running 17:51h.