-
Notifications
You must be signed in to change notification settings - Fork 32
CrabNumericalDomains
The following table summarizes the most commonly used numerical abstract domains in Crab. The table shows for each numerical domain its complexity and its expresiveness by showing the kind of constraints that it can represent.
| Domain | Complexity | Template |
|---|---|---|
| interval (aka box) | O(n) | lb <= x <= ub |
| dis-interval | O(n) | lb1 <= x <= ub1 \/ lb2 <= x <= ub2 \/ ... \/ lbn <= x <= ubn where ub1 < lb2 /\ ... /\ ubn-1 < lbn |
| term(interval) | O(n^2) | x = f(y1,...,yn) /\ lb <= x <= ub where f is an uninterpreted function |
| zones | O(n^3) | c1 * x - c2 * y <= k where c1,c2 \in {0,1} |
| octagons | O(n^3) | c1 * x - c2 * y <=k where c1,c2 \in {-1,0,1} |
| polyhedra | O(2^n) | c1 * x1 + c2 * x2 + ... + cn*xn <= k |
| boxes | O(2^j) (*) | \/ (lb1 <= x1 <= ub1 /\ ... /\ lbn <= xn <= ubn) |
n is the number of program variables and j is the number of join operations (typically from confluence points in the CFG).
lb, ub, lb1, ... , lbn, ub1, ..., ubn, k, c1, c2, ..., cn are numbers
x, y, x1, ... , xn are program variables
(*) The boxes domain can add mores splits (disjunctions) apart from joins. For instance, for boolean operators (or and xor), multiplication, etc.
Note from the above list, interval and dis-interval are non-relational domains. Boxes can be also considered non-relational but it can infer implications between variables of the form (k1 <= x <= k2 => k3 <= y <= k4) where => is logical implication. The rest of the domains are relational.
Most numerical domains operate on mathematical integers so they assume that arithmetic operations cannot overflow. The only exception is the wrapped interval domain.
Crab numerical domains do not support unsigned comparisons. One solution is to convert unsigned comparisons into signed comparisons during the construction of CrabIR. This is what clam does when option --crab-lower-unsigned-icmp is enabled.