Lin2var relations fine-tuning - switching from array to map by DrMichaelPetter · Pull Request #1412 · goblint/analyzer

DrMichaelPetter · 2024-04-12T14:34:37Z

This swaps out the basic datastructure in lin2var analysis from an array to a hashtable. Since we expect very sparse information kept in the relational part anyway, we expect a sizeable amount of runtime improvements vs. the conventional array implementation.

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

michael-schwarz · 2024-04-17T09:08:06Z

Already very curious how the performance is gonna be!

sim642 · 2024-04-17T09:21:44Z

Depends on the benchmark results, but I'm wondering if maybe immutable Maps would be the better choice even. You get the same sparsity benefit, but Maps also can share unmodified subtrees while Hashtbls cannot (due to the mutability).
Moreover, copy (which we do a lot) for a Map would essentially be identity as opposed to copying of Hashtbls. The only complication is that we sometimes want to exploit mutable _with operations on relational domains, which wouldn't be possible with Map. A generic lifting via ref (to a Map) like I already have in #1339 easily provides the necessary conversion.

DrMichaelPetter · 2024-04-17T11:07:55Z

Depends on the benchmark results, but I'm wondering if maybe immutable Maps would be the better choice even. You get the same sparsity benefit, but Maps also can share unmodified subtrees while Hashtbls cannot (due to the mutability). Moreover, copy (which we do a lot) for a Map would essentially be identity as opposed to copying of Hashtbls. The only complication is that we sometimes want to exploit mutable _with operations on relational domains, which wouldn't be possible with Map. A generic lifting via ref (to a Map) like I already have in #1339 easily provides the necessary conversion.

This sounds reasonable. Thank you for this in-depth insight into Ocaml data-structures. This is where my lack of experience in Ocaml shines through 😞

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

src/cdomains/apron/sharedFunctions.apron.ml

tests/regression/77-lin2vareq/33-dimarray.c

src/cdomains/apron/sharedFunctions.apron.ml

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

transitioning to hashtables; part 1: make types consistent again

f66ac96

DrMichaelPetter self-assigned this Apr 12, 2024

DrMichaelPetter added in progress performance Analysis time, memory usage labels Apr 12, 2024

DrMichaelPetter added 5 commits April 15, 2024 15:04

with equal and compare now

999299f

iterating over sparse entries needs some precaution

c195216

forgot the extra check

ac7ca72

fixed shifting of keys on remove_variables_from_domain

911c00f

offset bug fixed

aa1f1bf

github-advanced-security bot found potential problems Apr 16, 2024

View reviewed changes

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml Fixed Show fixed Hide fixed

DrMichaelPetter and others added 4 commits April 16, 2024 14:36

stupid old debug output removed

fbd7762

small beautifcations

4a2d888

added conf for benchmarking purposes

7cdf585

Merge branch 'master' into lin2var-hashtables

af9db43