Simmo Saan
Simmo Saan
Just to document this here: yesterday we discovered region analysis unsoundness in `ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--iowarrior.ko.cil.i` as well, where we miss a race on the `opened` field of `iowarrior` struct, because it appears...
## SQLite Analyzing https://www.sqlite.org/2022/sqlite-amalgamation-3370200.zip for ~1 minute with ```console goblint sqlite3.c sqlite3.h sqlite3ext.h shell.c -v --set pre.cppflags[+] -DSQLITE_DEBUG --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none...
> Impressive! Could you check if a short-circuiting `equal` still leads to further improvements here? If yes, one probably wants both. Prepending `x == y || ` to `equal` of...
> It might be interesting to leave it running for a while longer, one would expect the shortcut to start paying off as soon as address sets become large. It...
## sv-benchmarks ### Before vs after with `SetDomain.Joined` for `AddressDomain` buckets  ([Full results](https://goblint.cs.ut.ee/results/75-all-fast-hoaredomain-after-joined-fix/results/results.2022-08-03_07-04-59.table.html#/scatter?filter=0(0*status*(status(in(unknown,true)))),1(0*status*(status(in(unknown,true))))&toolY=1&columnY=1&scaling=Linear&results=All&line=1.2®ression=Linear)) Overall it's a 6% speedup. Most of the noisy blobs that show some slowdown are ReachSafety-ECA...
> The runtime with with the short-circuit evaluation was 42955.290s, and 43475.717s without it. That makes a difference of 520seconds = 8min40s. The version without short-circuit evaluation was 1.2% slower...
Also adapting `WitnessConstraints.PathSensitive3` to a similar construction from 8d6b8cff1 to cde436f39 gives a huge speedup in some cases (mostly those ECA tasks):  [Full results](https://goblint.cs.ut.ee/results/81-all-fast-hoaredomain-after-map-fp/results/results.2022-08-09_07-42-18.table.html#/scatter?filter=0(0*status*(status(in(true,unknown)))),1(0*status*(status(in(true,unknown))))&toolY=1&columnY=1®ression=Linear&scaling=Linear&results=All) Somehow it also makes us...
To avoid hard problems related to #816, it's possible to just use a partitioning which keeps `a`, `a[0]` and `a.fst` strictly separate. This implies a constant number of additional elements...
I hunted down the reason for these new unsoundnesses in our own race_reach benchmarks. It was a very subtle misplacement of `try`. The latest run on sv-benchmarks fixes those three,...
> Does this PR also attempt to fix tests 02/{91, 92, 92} that are also closely related to the address domain? Not at all. On the contrary, it makes the...