Numerical Abstract Domains
- Interval domain (upper lower bounds)
- Pentagon domain
- Zones
More expressive domains:
- Octagon
- TVPI
- Polyhedra
Domain transformers:
- E.g. Octagon
- Just add that constraint to the input element
- Can't be captured by the Octagon domain
Notes:
- Best approximation is exponential
- Standard approximation is quadratic
- Trivial, constant
No one way to implement domain transformers
- There's always a choice (to make them faster?)
Numerical domain analysis can be made faster through online decompositon.
- Into disjoin subsets, which we call blocks
- Then even smaller pieces, called vectors
- No constraint b/n x1, x3, x4
For example:
- We apply the standard transformer
- Only need to work on part of it, the second vector in this case (which is short for the example)
Previous work:
- Decomposing standard Octagon analysis (PLDI 15..
- Decomposing standard Polyhedra analysis (SAS 03, POPL 17)
Can't use old solutions for new domains, if I heard correctly.
It will not add any constraints, so it does not work on the first vector.
- If we make a less constrained example, this will no longer work
- Ad-hoc design
- Tailored to specific use cases
We want a universal construction
Black-box construction, assuming the original analysis is sound.
Does not require any access to how the transformer is implemented.
Our decomposed analysis:
- Fast
- Sound
- Monotonic and precise under practical conditions
Complete end-to-end implementation:
- Polyhedra
- Octagon
- Zones
At least 2x speedup, on decomposed version, much faster than original
An abstract element in domain D is conjunction of finite number of representable constraints
- the concretization function should preserve meets (not joins?)
- Compute finest unique partition, but usually very expensive
- Just maintain permissible parititions, for speed
- No constraints between the partitions
- Example of an invalid partition
With respect to an input i, if its output does not have a trivial partition..
It's possible to have two sound transformers:
- Non-decomposable
- Decomposable
One way to obtain is to design from scratch
- We construct them from non-decomposed transfomers
- 30-40 transformers
- Conditional, Assignment, Meet, Join, Widening
- (Ahh, there's join)
(Polyhedra)
-
B*_condwill merge all of the blocks in the precondition -
Our decomposed conditional transformer applies the original to
B*_cond -
Applied on small element to make it agnostic, and then the output partition contains
B*_condas a block, which can then be used. -
When we don't get any new constraints, output the result
-
We decompose, and then apply in a way that is equivalent to the "concrete"
When you apply it on the full element, it adds (<= 0) and closes it.
However, one of the added constraints is redudant, so even if you remove .. it still results in the something with the same concretization.
- After computing the output partition, we refine using:
- non-invertible assignment and join
- Converted to LLVM-IR
- Crab-llvm analyzer
- Non-decomposed transformers from PPL and decomposed from last year
In terms of results:
- 12 GB, up to 4 hours
- When PPL runs out of memory, we consider the time to be infinite
- With our refinement, we get a considerable speedup over our previous years
For Octagon:
- Largest 40x, smallest is 2x
For Zones:
- Max is 6x
- Introduced a black box consturction
- Same precision in practice
- Complete end-to-end implementation
- Significant speedup over previous results
We have more opimizations, not in the paper, that would make it even faster.
Do you consider the reduction with non-linear domains?
- We started with it, we could look into it, but not on topic
.. ?
- Real analysis can be done, but would not fit into this paper
Website: http://elina.ethz.ch