Lab 4: Lattice

Overview

In this lab, you will design several lattices and implement two program analysis algorithms based on lattice theory.

This lab consists of three parts: First, in part A, you will implement three classical lattices (diamond lattice, flat lattice, and powerset lattice). Second, in part B, you will implement a zero-value analysis algorithm based on the diamond lattice. Finally, in part C, you will restructure the liveness analysis algorithm based on the powerset lattice and implement a monotonic framework (if you are interested in it).

Getting Started

First check out the source we offered you for lab 4:

    $ git commit -am 'my solution to lab3'
    $ git fetch
    $ git checkout -b lab4 origin/lab4

these commands will first commit your changes to the lab3 branch of your local Git repository, and then create a local lab4 branch and check out the remote lab4 branch into the new local lab4 branch.

Again, you will need to merge your code from lab3 into the new lab4 branch:

    $ git merge lab3

Do not forget to resolve any conflicts before commiting to the local lab4 branch:

    $ git commit -am 'lab4 init'

You should first import the new lab4 code into your favorite IDE. There are a bunch of new files that you should browse through:

    cfg/lab4/LivenessLattice.java  liveness analysis framework
    cfg/lab4/ZeroAnalysis.java     zero analysis framework
    util/lattice/*                 lattice class definitions

Hand-in Procedure

When you finished this lab, zip you code and submit to the online teaching system.

Part A: Lattice

In compiler, lattice theory provides the mathematical foundation for data flow analysis. In this part, you'll learn and implement three types of lattices, and implement the operations to compute their least upper bounds.

Diamond Lattice

         ⊤
       /    \
      M0     M1
       \    /
         ⊥
    

Flat Lattice

          ⊤
     /  /    \   \
    a1 a2   ...  an
     \  \    /   /
          ⊥
    

Powerset Lattice

        {a,b,c}
       /    |   \
     /      |     \
    {a,b} {a,c} {b,c}
    | \   /   \   / |
    |  \ /     \ /  |
    |  / \     / \  |
    {a}    {b}    {c}
      \     |     /
        \   |   /
            ∅
    

Part B: Zero Analysis

In this part of the lab, you will implement a zero analysis algorithm to determine whether variables (and expressions) in a program can evaluate to zero. This analysis uses a diamond lattice to represent the possible states of a variable’s value:

         ⊤
       /    \
      0     Z-0
       \    /
         ⊥
    

Part C: Liveness Lattice

In this part of the lab, You will use the powerset lattice introduced in Exercise 3 to restructure the liveness analysis from Lab 2.

The monotonic framework is an abstract program analysis framework based on lattice theory. It ensures the termination and correctness of the analysis process by defining monotonic operations over partially ordered sets to represent program semantics. A monotonic framework generally consists of three components: a lattice, transfer functions, and a fixed-point iteration algorithm.

The Rustc compiler incorporates an exquisitely designed monotonic framework called Analysis trait. This framework primarily includes:

• Domain: Records data flow states at given program locations while requiring satisfaction of a partial ordering relation.
• Direction: Specifies the analysis orientation (Forward or Backward).
• Transfer functions: Evaluates the impact of a given statement (statement or transfer) on the current data flow state.
• Fixed-point algorithm: iteratively computes the solution to data flow problems.

By defining the analysis domain, direction, and transfer function for the analysis process (the fixed-point algorithm is officially provided, requiring no user implementation), various program analysis algorithms can be implemented efficiently.

Hand-in

This completes the lab. Remember to hand in your solution to the online teaching system.