313
edits
Changes
no edit summary
Notice that this time, we didn't have to divide up states at the start, we just started with no knowledge, which is perfectly general. Also, because we rejoin execution streams, in a loop-free method, we only have to interpret each instruction once, so we have completely solved the path explosion problem. (We haven't tried loops yet, and they are a bit harder--they require us to analyze statements more than once, but only finitely many times.)
=Algorithms=
Above, we showed how to do abstract interpretation informally, by hand. In order to code this up, we need a more technical description.
==Specifying an Abstract Interpretation==
In order to create an abstract interpretation, we have to specify three things: the abstract values, the flow function, and the initial state. We can perform an unlimited number of different analyses using the exact same framework just by varying those things.
In the following, I'm going to simplify things so I don't have to explain everything at once. So if you're an expert, you'll notice that I lie a bit in places, but I'm only ignoring certain design options that aren't important yet.
===Abstract Values and Lattices===
Every abstract interpretation requires a defined collection of abstract values. An abstract value is just a set of concrete values. In the standard integer constant propagation analysis, the abstract values are:
* ⊤, called "top" (remember the T for top), the set of all integer values
* 1, 2, ..., the singleton sets of integer values
* ⊥, called "bottom", the empty set
For our Mozilla analyses, we use these abstract values, and we add a "nonzero" value '''NZ''', which is useful for analyzing tests for zero that appear in if statements. Notice that NZ contains abstract values like 1 and 2. We can depict the set containment relationship graphically.
[[Image:treehydra-lattice.png|right]]
The mathematical structure corresponding to the picture is called a lattice.
Notice how the lattice controls the level of approximation of the abstract interpretation. For example, if a value can be 1 or -1, the closest covering approximation in our lattice is NZ. A different lattice could provide an abstract value that represents this set more precisely.
'''Merging.''' The lattice is key: among other things, it tells us how to merge two abstract values. To merge two abstract values v1 and v2, find the lowest value in the lattice that covers both v1 and v2. The technical term is '''least upper bound''' or '''lub'''. The funny symbol way to write "the lub of v1 and v2" is "v1 ⊔ v2".
The funny symbol is like a square set union symbol, and in fact, the lub operation can be described as "the approximate set union". Consider merging states where "x = 1" and "x = 2". Looking at the lattice, we see that 1 ⊔ 2 = NZ. But abstract values are just sets of values, so merging them should be like taking a union. In fact, {1} union {2} = {1,2}, but we can't represent {1,2} exactly in our lattice. The closest cover is NZ, which is 1 ⊔ 2.
===Flow Functions===
Abstract interpretation requires us to maintain an abstract interpreter state and then interpret each instruction in the current state (technically, the state at the program point before the instruction).
The flow function is what does that interpretation. The input is an abstract state and an instruction. The output is the abstract state after executing the instruction. Thus, the flow function describes the ''abstract semantics'' of every instruction type.
An implementation of a flow function looks much like an interpreter's main switch statement, just operating on abstract values.
'''Deriving flow functions.''' Usually you can figure out what the flow function should do just by thinking about it. For example, for a statement "x := K" where K is any integer literal, it's pretty obvious that the result is that x gets abstract value K.
There is also a mechanical procedure for deriving the flow function for a statement "x = a op b" for any binary operator. (This also applies to unary and nullary operators, making the needed changes.) For each pair of possible input abstract values va and vb:
* Evaluate "ca op cb" for every concrete value ca covered by va and every concrete value cb covered by vb. (Formally: let C = { ca op cb | ca in va, cb in vb }.)
* Collect the set of results and translate to an abstract value vr. (Find the lowest node in the lattice that covers C.)
* Then, the flow function should have "va op vb -> vr".
For example, consider our lattice with NZ and the operation "x = a + 1". For "a = NZ", we evaluate "ca + 1" for ca in "everything but 0". The result is "everything but 1". The lowest covering abstract value is "top".
=== Initial State ===
Finally, we need to specify the initial abstract state, the one that holds when the function is entered. For constant propagation, we used the state of no information, namely, everything set to "top" (any value). This is often a good choice, but some analyses need other choices. For example, the outparams analysis is all about whether an outparam has been written to inside the function, so the initial state of the outparams is NOT_WRITTEN.
=== Example ===
Let's use this framework to define another abstract interpretation. This time, we'll try a bug checker: we'll assume there is an API with lock() and unlock() functions, and check that every unlock() is preceded by a lock().
In a practical problem, the first step of all is to figure out the core analysis that needs to be defined, separately from the checkers, code transformers, and other tools. In this case, the property we need abstract interpretation to discover is, at every program point whether lock() was the last locking API call. Given that information, we can finish the checker by looking at the program point before each call to unlock() and verifying that lock() was called. Now we just need to define the abstract interpretation to gather that information.
'''Lattice.''' Usually, the hard part is designing the lattice. In this kind of problem, it is standard to model the lock (or other object whose protocol is being checked) as a state machine. We'll say that locks can be in either the state L (locked) or U (unlocked). We'll have top and bottom as always, finishing our lattice.
'''Flow function.''' With the lattice in place, the flow function is easy. We can write down a chart:
(statement) (result)
x.lock() x = L
x.unlock() x = U
anything else no effect
'''Initial state.''' Our spec said that lock() had to be called before unlock(). This suggests that on entry, locks are not locked, so we'll use a starting state of U for all locks.
==Solving==
