analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard
verified publisher icon goblint

Tracking Benchmark Changes for Thesis

Open michael-schwarz opened this issue 2 years ago • 3 comments

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, 3ad6b396681e0cb936eba09c4d7b6ebed882a0a2)
  • Traces: Enable def_exc_widen_by_join for reproducibility 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
  • Merged #1545
  • Fixed #1551
  • Merged #1559

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 avatar Apr 17 '24 11:04 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, [email protected]: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.

michael-schwarz avatar May 08 '24 15:05 michael-schwarz

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.

sim642 avatar May 09 '24 06:05 sim642

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.

michael-schwarz avatar Jun 25 '24 17:06 michael-schwarz

Everything that should be extracted now lives on its own PR. We can thus close this one.

michael-schwarz avatar Dec 17 '24 15:12 michael-schwarz