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)
  • [x] 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.
  • [x] 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)
  • [x] 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 https://github.com/goblint/analyzer/pull/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)
  • [x] look into the write accesses in print_context_append in print.c (4): same thread-local problem as in ignore.c
• options.h (8)
  • [x] 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
  • [x] opts.stream_line_num write only and comment "This should totally not be in here" options.h (1)
  • [x] 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.
  • [x] 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!
  • [x] 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 https://github.com/goblint/analyzer/pull/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
  • [x] 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?