Lab for Automated Reasoning and Analysis LARA

Lecture 15: Introduction to Program Analysis

Control-Flow Graphs

Key Background

Control-Flow Graph Definition

Why control-flow graphs instead of syntax trees

  • they can represent arbitrary jumps
  • they are simple: conditions and loops represented uniformly
  • used in most compilers (including LLVM and GCC)

Translation of syntax trees to control-flow graphs is (at a high-level) similar to translation from regular expressions to finite-state machines (see closure properties of finite state machines).

Decomposing Complex Expressions

If Statements to CFG

While Statements to CFG

Source and Target CFG Vertices

In Scala:

Data-Flow Analysis

Initializatoin

Live Variable Analysis

References

 
cc11/lecture_15.txt · Last modified: 2012/12/02 17:43 by vkuncak