Tracking Benchmark Changes for Thesis

[michael-schwarz]

The branch I used to benchmark for my thesis diverges at d8be117080e1f6d0bdc9e8331e888f2d3ac2cf7c.

This draft MR is not intended to be merged but should allow me to keep an overview of the changes and see what should be maybe back-ported.

Back-ported:

• Typos (c28ca496b78dcab8e1d7191b16b0398896022ea8, e192c8e8d0489535fe5bfa91c7e28da5fc4ab12a, 5073759d37e158441e78dc48abcd80f48933632f, c5d2b3619b6a8b127273ec8418340ab2d9cfd861)
• Traces: Enable def_exc_widen_by_join for reproducability for SAS '21 results 3e13e04c021923485553471cb12437aa8f20d7b7

To consider:

• Way to supply suffix to name of privPrecCompare output
• Quick fix for #1421
• Do not colorize privPrecCompare output to stderr (in case it is saved to somewhere)
• exp.priv-prec-dump-proj option to project precision of dumps to enums, intervals, and def_exc for comparison between different activated domains
• Warn instead of crash if an argument to a string function does not evaluate to an address.

• 1431

• 22fdef68328223ec98454fd9ffed518cc6d68582 (adapt traces and traces-rel configurations to be more similar)
• 1b180d46133db724a3d34228c4f1200134944915 (Add bot_in_blob_leq_bot so bot and Blob(bot) compare equal in privPrecCompare)
• Cherry-picked #1435
• Fix to force refinement to only happen when dumping precision comparisons (to avoid #1005)
• Cherry-picked #1458
• Cherry-picked #1468
• Manually included #1471 1471
• Cherry-picked #1481
• Cherry-picked #1444
• Cherry-picked #1492
• Cherry-picked #1430
• Cherry-picked #1500
• Cherry-picked #1475
• (Partly) Cherry-picked #1508

Hotfixes:

• Hotfix for https://github.com/goblint/analyzer/issues/1513 (should be solved by addressing https://github.com/goblint/cil/issues/169 instead)

[michael-schwarz]

[Debug] cava.c:1507:9-1507:27 (alloc@sid:459@tid:[main]): write less precise than mine-W-interval
  write: (value:⊤, size:1024, no zeroinit:true)
  less precise than
  mine-W-interval: (value:⊤, size:1024, no zeroinit:true)
  diff: 1024 instead of 1024

 [Debug] cava.c:3552:5-3553:47 (alloc@sid:2113@tid:[main, input_fifo@cava.c:1931:5-1932:83]): protection more precise than write
  protection: Uninitialized
  more precise than
  write: (trivial arrays:Array: (value:Uninitialized, size:4096, no zeroinit:false), IntDomLifter(intdomtuple):1)
  reverse diff: compound: (trivial arrays:Array: (value:Uninitialized, size:4096, no zeroinit:false), IntDomLifter(intdomtuple):1) not same type as Uninitialized

both seem fishy.

[sim642]

cava has a lot of missing library functions though, so how exactly are you intending to analyze it without losing all precision from invalidations? I'm not sure how correctly those invalidations work with the more involved privatizations.

[michael-schwarz]

I now added the same handling we have for the non-relational privatizations upon threadenter with unknown function also to the relational privatization.

While that may be of questionable nature, handling this differently in different privatizations is even more so.