Explanations on how to make the silver searcher analysis more precise

[karoliineh]

This PR includes descriptions of configurations and annotations to make the analysis more precise on the silver searcher as well as explanations on why/how they help with reducing the number of warnings.

The goals are to:

1. Understand, why the warnings are produced and what needs to be done to reduce the number of false positives;
2. Give insight into which configurations (and how) one might want to configure for Goblint to produce fewer warnings.

Remaining races (28) (13.09.23):

• decompress.c (4)
  • look into HASH_ADD write accesses in search.c (2):
    symhash is global but only used by main thread in multi-threaded mode, value must be computed flow-sensitively.
    Two accesses have region:{symhash}, but third should have bullet, but doesn't.
  • look into lzma_end read-write-spawn accesses in decompress.c (2): mallocFresh might get rid of this (because region analysis gets rid of these with no region)
    buf_getline should return bullet from argument to another argument via pointer?
• ignore.c (3)
  • look into the write accesses in print_context_append in print.c: things with _thread keyword that are thread-local but the cases discussed in Ignore accesses to variables with __thread keyword analyzer#1071, and an unknownptr comes from the pointer in that thread-local variable being NULL due to globals init, although it is thread-local and initialized every time the new thread is created (and if not, the program crashes on its own anyways)
• main.c (1)
  • spurious race: needs symbolic thread-id
• options.c (4)
  • look into the write accesses in print_context_append in print.c (4): same thread-local problem as in ignore.c
• options.h (8)
  • look into the write accesses in print_context_append in print.c (4): regions knows that those fields (opts.color_line_number, opts.color_match, opts.color_path,opts.query) are not modified elsewhere
  • opts.stream_line_num write only and comment "This should totally not be in here" options.h (1)
  • opts.match_found does not race with read, and has a comment "This should totally not be in here" in options.h (1)
    Could be protected by print_mtx.
  • opts.print_line_numbers real race (1)
    Only written by main thread in multi-threaded mode before workers do any work (and read it) — value/cond based.
    Some workers might already start and read when search_dir is still adding to queue and writing!
  • opts.print_path real race (1)
    Writes are safe: only written by main thread in multi-threaded mode before workers do any work (and read it) or with print_mtx.
    Some reads without print_mtx, in search_stream? Looks like real race.
• util.c (2)
  • spurious races: needs mallocFresh analysis (which @karoliineh tried to fix, but the whole mallocFresh came out to be unsound and that is not resolved yet Improve mallocFresh analysis analyzer#1069): the races are on matches which is fresh (2): region analysis gets rid of these with no region
• string.h (1)
  • true race: has a comment in code: "/* XXXX: strerror is not thread-safe */"
• search.c (5)
  • same matches as in util.c, just allocated at different locations (4): region analysis gets rid of these with no region
  • look into the write accesses in print_context_append in print.c (1): same thread-local problem as in ignore.c

[michael-schwarz]

Is there still something to do here, or should we merge it?

[sim642]

I added your config (with region) and some patches.

[sim642]

Is this still true? Doesn't seem to reduce anything for me.

[sim642]

Also zlib and liblzma now.

[sim642]

This was probably useless.