7
edits
Changes
m
no edit summary
* A '''program point''' is the (notional) point just before or after each instruction. The function has a well-defined state at program points, so our analysis facts will always refer to program points. E.g., at the program point just before 't1 := k + m', k is constant with value 2.
==Concrete Interpretation==
To explain abstract interpretation, we'll start with concrete interpretation, which is just the normal kind you are already familiar with. We'll use it to build up to abstract interpretation.
We could imagine trying to guess which variables are constant just by calling the function with different inputs, and finding which variables are constant over all those runs. Let's start by running with "a = 0, b = 7" and trace the run:
(instruction) (interpreter state after instruction)
ENTRY a = 0, b = 7
k := 1 a = 0, b = 7, k = 1
COND a == 0 (TRUE)
k := k + 1 a = 0, b = 7, k = 2 m := a a = 0, b = 7, k = 2, m = 0 n := b a = 0, b = 7, k = 2, m = 0, n = 7 t1 := k + m a = 0, b = 7, k = 2, m = 0, n = 7, t1 = 2 ret := t1 + n a = 0, b = 7, k = 2, m = 0, n = 7, t1 = 2, ret = 9
RETURN ret
EXIT
So k = 2 just before its use in 't1 := k + m'. We can run with many other inputs and get the same result. But testing can never tell us that k = 2 for all inputs. (Well, actually it can, but only if you can run 2<mathsup>2^64</mathsup> test cases.)
==Approaching Abstract Interpretation==
