Instead of running a three-line program for every possible input, this example
tracks only the sign of each variable: negative, zero, or positive. A handful
of rules propagate signs through both branches of an if, merge them, and
raise a warning because one path can reach the division with y equal to zero.
Run it in the playground ยท Source
The program under analysis is:
x := input();
if x < 0 then y := -x else y := x;
z := 10 / y;
Is 10 / y safe for every input? Testing integers one by one never finishes.
Abstract interpretation replaces each value by a coarse description, here
its sign, so that a finite computation covers every concrete run.
input_sign(neg).
input_sign(zero).
input_sign(pos).
abs_state(input, x, Sign) :- input_sign(Sign).
abs_state(Point, Var, Sign) says that at program point Point, variable
Var may have sign Sign. The input statement allows all three signs.
abs_state(negative_branch, x, neg) :- abs_state(input, x, neg).
abs_state(nonnegative_branch, x, zero) :- abs_state(input, x, zero).
abs_state(nonnegative_branch, x, pos) :- abs_state(input, x, pos).
abs_state(negative_branch, y, pos) :- abs_state(negative_branch, x, neg).
abs_state(nonnegative_branch, y, Sign) :- abs_state(nonnegative_branch, x, Sign).
abs_state(join, Var, Sign) :- abs_state(negative_branch, Var, Sign).
abs_state(join, Var, Sign) :- abs_state(nonnegative_branch, Var, Sign).
possible_division_by_zero(join) :- abs_state(join, y, zero).
The branch test refines x. Each assignment maps signs to signs: y := -x
turns a negative x into a positive y. At the join point the analysis keeps
everything either branch allows, which makes it conservative: it may warn
about a run that cannot happen, but never misses one that can.
eyeprolog examples/abstract-interpretation.pl
absState(join, x, sign(neg)).
absState(join, y, sign(pos)).
absState(join, x, sign(zero)).
absState(join, x, sign(pos)).
absState(join, y, sign(zero)).
absWarning(division_by_zero, join).
absConclusion(case, "abstract interpretation keeps all feasible signs and warns because y may be zero").
These are the last 7 of 16 answers; the first 9 list the signs at the input
and in each branch. At the join, y may be positive or zero, so the division is
flagged. The warning is real: input 0 takes the non-negative branch and sets
y := 0.
eyeprolog --proof examples/abstract-interpretation.pl
step(abs_state(input, x, zero), rule(4), ['Sign' = zero], [input_sign(zero)]).
step(abs_state(nonnegative_branch, x, zero), rule(6), [], [abs_state(input, x, zero)]).
The proof of the warning walks the zero path: the input may be zero (rule 4,
from the fact input_sign(zero)), that zero enters the non-negative branch
(rule 6), is copied into y, and reaches the join. The proof is a witness path
through the program.
condition('C1', resolution, ok, 34).
condition('C4', coverage, ok, 47).
condition('C7', relevance, ok, 50).
trusted(0).
claims(16).
verdict(checked).
All 34 steps resolve against the clauses they cite, all 16 claims are covered, and nothing is trusted. The analysis is pure Horn clauses, so the checker can verify it completely.
y := x + 1: replace the zero/pos rule for y in
nonnegative_branch with rules that map zero to pos. Does the warning
disappear?nonneg, and explain where precision is lost at
the join.5 cover, and which would it
miss?Learn more in The Art of EyeProlog, Chapter 43, Laboratory 8 (a static analyzer).