Programming language analysis

Instructor: Matt Might.

TA: .

Office hours: Any time my door is open, or set up a meeting by email.

Time: Tuesdays and Thursdays from 10:45am to 12:05pm.

Links: [google group] [rss]

Disclaimer: This syllabus is tentative and subject to change.

Course summary and objective

Static analysis is the field of study concerned with algorithms that extract information about the run-time behavior of a program from the source code (or machine code) of that program. Static analysis has been a vibrant field of research since the dawn of computing, and today, static analysis is the driving force behind compiler-based program optimization, tool-based software engineering, bottom-up information security, formal program verification and automatic program parallelization.

For example, in the following Java code:

  for (int i = 0; i < a.length; ++i) {
   a[i] = read() ;
  }

Turing's halting problem prevents any given static analyzer from recovering perfect information for all programs. Consequently, techniques in static analysis rely on models that approximate program behavior in a computable fashion. The primary objective in the design of a static analysis is to model the desired run-time behavior as accurately as necessary, but to keep the analysis efficiently computable for the average case.

Upon completing this course, students should be comfortable reading a recently published research paper in the field of static analysis, and students will be familiar with the standard techniques for static analysis of both functional and imperative programs.

Prerequisites

Topics

• Formal semantics.
• Small-step semantics.
• Big-step semantics.
• Basic order theory up to lattices.
• Basic fixed-point theory.
• Static-single-assignment form (SSA).
• Lambda calculus.
• Administrative normal form lambda calculus (ANF).
• Continuation-passing-style lambda calculus (CPS).
• Intraprocedural data-flow analyses.
• Constraint-based analyses.
• Unification-based analyses.
• Abstract interpretation.
• Type-based analyses.
• Higher-order control-flow analysis (k-CFA).
• Alias and pointer analysis (Steensgard, Andersen).
• Dependence analysis.
• Escape analysis.
• Array-bounds analysis.
• Analysis-driven program transformations.
• Proof techniques for demonstrating soundness.
• Analysis of parallel programs.

Required textbook

The latest version of the class notes are available here. Updated weekly.

Any papers assigned for reading will be provided as pdfs.

Supplementary textbooks

The following textbooks are not required, but they are a useful secondary point of reference for the course material. Students considering doing research in static analysis or related areas will almost certainly want to grab a copy.

The Nielsons' book Semantics with Applications is one of the best introductions to formal semantics out there, and the application featured in the book is static analysis:

The same authors (plus Hankin) have also written a book on static analysis, Principles of Program Analysis:

I also maintain a list of useful books, papers and materials for graduate students.

Grading

Your final grade is the better of:

• your grade on the comprehensive final exam; or
• your average grade for the projects.

In other words, if you get an A on the final, then you get an A in the class, no matter how badly you did on the projects. Or, if you get a B average on the projects, but an F on the final, then you still get a B for the class.

Projects

There will be roughly four or five miniprojects throughout the semester. Each miniproject will involve implementing a known static analysis for a toy language. The syntax of each toy language will always be S-Expression-based, so motivated students may complete the assigment in the programming language of their choosing by writing their own parser. However, a parser for the toy language will always be provided that works with both the Java and Scala programming languages. If you decide to use a language other than Java or Scala, contact me in advance to make sure I can run it on Mac OS X.

Jon Rafkind has kindly supplied an example that illustrates how to get ant and scala to cooperate.

Collaboration policy

For projects, share anything but code.

Bonus

There are bonus opportunities to add percentage points to your final grade:

• Write or significantly clean and expand a wikipedia article on a topic related to the class. (+2%)
• Write a detailed critique (what's good, what's bad, what's missing) of a chapter of the textbook. (+2%)
• Write a peer-review-quality report of a research paper. (+5%)
• Implement and empirically test an analysis from an unpublished research paper. Contact me to gain access to an archive of eligible unpublished papers. [Warning: This will require mastery of virtually all course material.] (+100%)
• Propose your own project. (+x%)
• Any other bonus projects announced in class.

There are also bonus opportunities for each project:

• Implement the fastest correct analysis. (+5%)
• Parallelize the code for a project. (Multiply the grade for that project by s/p, where s is the time taken by the fastest project running on a single core, and p is the time taken on two cores for a benchmark suite of my choosing.)
• Write a benchmark that causes another student's analysis to fail. (+0.2% for each failure; maximum of +10% for all benchmarks.)

Late policy

Late assignments will have min(2^d - 1, 100) percentage points subtracted from the final grade of the assignment, where d is the number of days late.

Tentative schedule

This schedule is subject to change. Once a pace for the course is established, the rest of the schedule will be fleshed out.

Assignments

Project 3: Classic data-flow analysis

Due: Sunday, April 11th 2009, 23:59:59 MT

Goals

• Construct a constant-propagation analysis for a flat imperative language.

Description

Constant propagation is one of the most important static analyses from a software engineering perspective. In constant propagation, expressions which have a constant value during execution are converted into constants. Psychologically, this frees a programmer to structure code more naturally. For example, with constant propagation, a programmer could have a global variable, isDebugMode indicating whether or not the program is in debugging mode. Debugging-mode only tests can be wrapped in if (isDebugMode) { ... }. Programmers would probably shy away from such practices if they didn't trust the compiler to inline the value of isDebugMode and eliminate the test.

In this project, you will construct a constant-propagation analysis for a simple, flat abstract machine-code language: Macho. The S-Expression grammar for Macho is:

   prog in Prog ::=  (program stmt*)

   stmt in Stmt ::=  (:= lhs rhs)
                 |   (println rhs)
                 |   (if cond goto lab)
                 |   (label lab)
                 |   (skip)
                 |   (goto lab)
                 |   (return rv)

   lab  in Lab   =   an infinite set of labels

   lhs  in LHS  ::=  v

   rhs  in RHS  ::=  v                  [variable reference]
                 |   z                  [integer constant]
                 |   (op rhs1 ... rhsN) [primitive expression]

   rv   in Ret   =  RHS
   cond in Cond  =  RHS

   op   in Op    = {==,<=,+,*,-,/}
  

For example, the following program computes the factorial of 6:

 
 (program         (:= x 6)
                  (:= a 1)
  (label fact)    (if (<= x 0) goto end)
                  (skip)
                  (:= a (* x a))
                  (:= x (- x 1))
                  (goto fact)
  (label end)     (println a)
                  (return a))

Note that in Macho, labels are actually statements. In fact, they behave like skip instructions, except that they can be the target of a conditional branch or a goto.

In Macho, zero is false and non-zero is true with respect to branching conditionals. Conditional operations, like <= and == return either 0 or 1.

Useful(?) files

The files are provided without any warranty as to correctness. Your professor coded them with haste, tested them three times and assumed correctness. If you find what you believe to be bugs, please let me know!

1. Macho.scala: A Macho interpreter.
2. macho.zip: A reference implementation of the constant propagation analysis; to run:

    scala -cp . languages.macho.MachoCPA < machofile
   

Requirements

1. Tarball and name the turnin file/directory like in project 1. If you want to use zip instead of tar+gzip, go ahead.
2. In the README file, briefly note what's working, what's broken and which bonus features are implemented. Feel free to include anything else you think might interest the grader.
3. Include a Makefile with your turnin even if you use ant.
4. make all should compile everything.
5. make run should execute your analysis on stdin and print the result on stdout.
6. The output should generate an in/out entry for each statement of the program that looks like the following:

       ((in   map)
        (stmt stmt)
        (out  map))
      

   Each map is an associative list which maps variables into the constant-propagation lattice: {bot,...,-1,0,1,...,top}.

Examples

1. Input:

   (program         (:= x 6)
                    (:= a 1)
    (label fact)    (if (<= x 0) goto end)
                    (skip)
                    (:= a (* x a))
                    (:= x (- x 1))
                    (goto fact)
    (label end)     (println a)
                    (return a))
     

   Output:

   ((in   ())
    (stmt (:= x 6))
    (out  ((x 6))))
   
   ((in   ((x 6)))
    (stmt (:= a 1))
    (out  ((a 1) (x 6))))
   
   ((in   ((a top) (x top)))
    (stmt (label fact))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (if (<= x 0) goto end))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (skip))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (:= a (* x a)))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (:= x (- x 1)))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (goto fact))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (label end))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (println a))
    (out  ((a top) (x top))))
   
   ((in   ((a top) (x top)))
    (stmt (return a))
    (out  ((a top) (x top))))
     

2. Input:

   (program          (:= x 1)
                     (:= a 5)
                     (if x goto alt)
                     (:= a (- 0 a))
                     (:= y (* a a))
                     (goto end)
       (label alt)   (:= y (* a a))
                     (goto end)
       (label end)   (return y))
   

   Output:

   ((in   ())
    (stmt (:= x 1))
    (out  ((x 1))))
   
   ((in   ((x 1)))
    (stmt (:= a 5))
    (out  ((a 5) (x 1))))
   
   ((in   ((a 5) (x 1)))
    (stmt (if x goto alt))
    (out  ((a 5) (x 1))))
   
   ((in   ((a 5) (x 1)))
    (stmt (:= a (- 0 a)))
    (out  ((a -5) (x 1))))
   
   ((in   ((a -5) (x 1)))
    (stmt (:= y (* a a)))
    (out  ((a -5) (x 1) (y 25))))
   
   ((in   ((a -5) (x 1) (y 25)))
    (stmt (goto end))
    (out  ((a -5) (x 1) (y 25))))
   
   ((in   ((a 5) (x 1)))
    (stmt (label alt))
    (out  ((a 5) (x 1))))
   
   ((in   ((a 5) (x 1)))
    (stmt (:= y (* a a)))
    (out  ((a 5) (x 1) (y 25))))
   
   ((in   ((a 5) (x 1) (y 25)))
    (stmt (goto end))
    (out  ((a 5) (x 1) (y 25))))
   
   ((in   ((a top) (x 1) (y 25)))
    (stmt (label end))
    (out  ((a top) (x 1) (y 25))))
   
   ((in   ((a top) (x 1) (y 25)))
    (stmt (return y))
    (out  ((a top) (x 1) (y 25))))
   

3. Input:

   (program         (:= debug 1)
                    (:= x 1)
                    (:= a 1)
   
    (label loop)    (if (<= x 1) goto end)
                    (if (== debug 0) goto skip1)
                     (println x)
    (label skip1)   (skip)
                    (:= x (+ x 1))
                    (goto loop)
   
    (label end)     (println x)
                    (return x))
   

   Output:

   ((in   ())
    (stmt (:= debug 1))
    (out  ((debug 1))))
   
   ((in   ((debug 1)))
    (stmt (:= x 1))
    (out  ((debug 1) (x 1))))
   
   ((in   ((debug 1) (x 1)))
    (stmt (:= a 1))
    (out  ((a 1) (debug 1) (x 1))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (label loop))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (if (<= x 1) goto end))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (if (== debug 0) goto skip1))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (println x))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (label skip1))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (skip))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (:= x (+ x 1)))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (goto loop))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (label end))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (println x))
    (out  ((a 1) (debug 1) (x top))))
   
   ((in   ((a 1) (debug 1) (x top)))
    (stmt (return x))
    (out  ((a 1) (debug 1) (x top))))
   

Project 2: CPS-conversion and 0CFA

 f,e in Exp = v                         [Variable]
            | (lambda (v1 ... vn) e)    [Lambda term]
            | (let* ((v e) ...) e)      [Sequential let]
            | (f e1 ... en)             [Application]
            | (if-zero e1 e2 e3)        [Conditional]
            | z                         [Integer]
            | succ                      [Successor]
            | pred                      [Predecessor]

(let* ((Y (lambda (X)
            ((lambda (procedure)
               (X (lambda (arg) ((procedure procedure) arg))))
             (lambda (procedure)
               (X (lambda (arg) ((procedure procedure) arg)))))))
       
       (countdown (Y (lambda (countdown) (lambda (n)
                                   (if-zero n
                                            0
                                            (countdown (-1 n))))))))
  (countdown 10))

 f,e  in Exp   =   Lam + Var + Int + Prim
 p    in Prim ::=  (cps succ)  |  (cps pred)  |  halt
 lam  in Lam  ::=  (lambda (v1 ... vn) call)
 call in Call ::=  (f e1 ... en)
               |   (if-zero e1 e2 e3)

Project 1: A λ-calculus interpreter and programming with Church encodings

 <exp> ::= <app> | <var> | <lam> | <let*>
 <app> ::= '(' <exp> <exp> * ')'
 <let*> ::= '(' 'let*' '(' ( '(' <var> <exp> ')' ) * ')' <exp> ')'
 <lam> ::= '(' 'lambda' '(' <var> * ')' <exp> ')'
 <var> ::= [^)( \n\t\r]+ 

 <exp> ::= <app> | <var> | <lam> 
 <app> ::= '(' <exp> <exp> * ')'
 <lam> ::= '(' 'lambda' '(' <var> * ')' <exp> ')'
 <var> ::= [^)( \n\t\r]+