Optimizing Set Abstract Domains – Arlen Cox (IDA/CCS)
Optimizing Set Abstract Domains
Arlen Cox (IDA/CCS)
TL;DR
I made a library.
It's fast.
It's well documented.
It's easy to use.
It uses abstract interpretation to efficiently infer inductive invariants like this:
\( S = R \uplus \{x\} \uplus T \quad \wedge \quad Q = P \setminus T \)JavaScript objects are open
var point = { x: 1, y: 2 };
point.x; // read x field
point.y; // read y field
point.z = 3; // add z field
point[“w”] = 4; // add w field
“z” in point; // ask if z exists
for(i in point) {} // iterate over fields
// i = [“w”, “y”, “x”, “z”]
Objects overwrite other objects
Hello
Hello
Hello
for(x in src) {
dst[x] = src[x];
}
Without knowing what src and dst are, what does this code do?
Infer loop invariants
src dst $x \mapsto 1$ $x \mapsto 6$ $y \mapsto 2$ $p \mapsto 7$ $z \mapsto 3$ src dst $x \mapsto 1$ $x \mapsto 1$ $y \mapsto 2$ $p \mapsto 7$ $z \mapsto 3$ $y \mapsto 2$ $z \mapsto 3$
Optimizing Set Abstract Domains
Arlen Cox (IDA/CCS)