The source code is available here.
| ListUtil | Theorems about lists, including decision procedures for some standard predicates on lists |
| Maps | Functors for building finite map and set implementations |
| Tactics | Generally-useful tactics |
This is the example from the first day of class. It's a certified must-not-alias procedure based on Andersen's Analysis. The basic structure of the development goes like:
| Machine |
Define both concrete and flow-insensitive reachability for generic machines. Prove that flow-insensitive execution conservatively approximates flow-sensitive execution. Define and prove correct and terminating a generic procedure for calculating flow-insensitive dataflow fixed points. |
| Pointer |
Define the toy language to analyze, including its instructions, machine states, and small-step semantics. Define what a must-not-alias procedure is. The rest of the development works towards constructing a value of this type. |
| AndersenModel |
Define an abstracted version of the concrete language and semantics, where each allocation instruction has an associated symbolic allocation site that we pretend is always the result of an allocation there. Gives the abstract instructions, machine states, and small-step collecting semantics. Define a compilation from real programs into abstract programs. |
| AndersenSound |
Formalize the abstract machine as an abstract interpretation of the concrete machine by defining an abstraction relation whose central idea is "Concrete state c and abstract state a are related if any two paths through memory in c starting from variables that lead to the same destination have corresponding abstract paths in a that lead to the same destination." Prove that the abstraction relation is preserved by one execution step, and so the abstract model conservatively approximates the concrete model. As a result, two variables never alias if the sets of their possible abstract values never intersect in any reachable abstract state. |
| AndersenIter |
Define a lattice structure on abstract states using only the variables and allocation sites of a fixed program, where state s1 approximates state s2 if every variable and allocation site is mapped by s1 to a (not necessarily strict) superset of the allocation sites that s2 maps it to. Prove that the abstract machine semantics never decreases a state and is monotonic with respect to the approximation relation. Define for the lattice a relation capturing the notion of when one state conveys strictly more information than another and prove that this relation is well-founded, making it a good basis for a dataflow algorithm termination argument. Put these pieces together to define a fixed-point calculation algorithm for the abstract machine, using the generic procedure from Machine. |
| Andersen | The suspense is over as we define a must-not-alias procedure based on these previous results. |