Program Analysis
Nguyễn Thu Trang
UET-VNU
1
How do you verify the
correctness of a software
program?
2
Testing is one of the most
common methods:
• Bug detection
• Correctness verification
3
Is there any other method
for software quality
assurance without running
the program?
4
What is static (program) analysis?
5
• Static analyis is a method of (automatically)
examining the source code without having to
What is execute the program.
• Goals:
static • Detect (potential) defects
analysis? • Find sercurity vulnerabilites
• Find code quality issues
• Optimize performance
• When: early in the development process
6
Static vs. Dynamic analysis
Static analysis Dynamic analysis
• Do not require code execution • Require code execution
• Analyze all code (regardless of whether • Only analyze the executed code
it’s executed or not) • Under-approximate program behavior
• Over-approximate program behavior
• Detect runtime-specific issues
• Detect potential defects, vulnerabilites,
• Miss errors in unexecuted paths (false
code quality issues negatives)
• May have many false positives (and also
• Example: Monkey testing tool, seleminum
false negatives)
• Example: compilers, lint-like tools
7
Example
What are the
possible outputs?
8
Example
• Over-approximation:
“yes”, “no”, “maybe”
• Consider all paths (that are
feasible based on limited
knowledge)
• [Link]() actually
returns a value in [0, 1)
à Out = “maybe” is infeasible
9
Example
• Under-approximation:
“yes”
• Execute the program once
10
Example
• Sound and complete:
“yes”, “no”
• For this example: can
explore both feasible paths
11
Another
example
What are the
possible outputs?
12
Another
example
• Over-approximation:
any value
• Consider all paths (that
are feasible based on
limited knowledge about
random())
13
Another
example
• Under-approximation:
some value in [0, 2)
• Execute the program once
14
Another
example
• Sound and complete?
• Exploring all possible
outputs: practically
impossible
• This is the case for most
real-world programs
15
Under vs. Over-approximation
• Program: P
• For input 𝑖 ∈ I, we observe a behavior P(𝑖)
All possible behaviors (what we want, ideally)
P(i1) P(i3) Under-approximation (e.g., testing, dynamic
analysis)
Over-approximation (most static analysis)
P(i2)
False negatives
False positives
16
Source code representation
• Raw source code
• Token stream
• Abstract syntax tree (AST)
• Control flow graph
• Program dependence graph
• Binary code/machine code
17
Types of program analysis
• Lexical analysis: analyze the basic tokens of the source code
• Syntactic analysis: ensure the source code follows correct syntax
• Data flow analysis: analyze how data defined and used through the source
code
• Control flow analysis: analyze the flow of the program
• Type checking: ensure the correct and consistent useage of the types
18
Data flow analysis
One popular way of formulating a static analysis
19
• Propagate analysis information along the
edges of a control flow graph
Data flow • Goal: Compute analysis state at each
program point
analysis • For each satement, define how it affects the
analysis state
• For loops: Iterate until fix-point reached
20
Available expression analysis
Very busy expression
Data flow
analysis Reaching definitions analysis
Live variables analysis
21
• Goal: for each program point,
compute which expressions must
Available have already been computed, and not
later modified.
expression • Useful, e.g., to avoid re-computing
analysis an expression
• Used as part of compiler
optimizations
22
Example
Available every time
execution reaches this point
23
• Transfer function of a statement:
How the statement affects the analysis state
• Here: analysis state = available
Transfer expressions
• Two functions:
functions • gen: Available expressions generated by
a statement
• kill: Available expressions killed by a
statement
24
Funtion 𝑔𝑒𝑛: 𝑆𝑡𝑚𝑡 → 𝑃(𝐸𝑥𝑝𝑟)
• A statement generates an available expression
e if:
gen function
• It evaluates e and
• It does not later write any variable used in e
• Otherwise, function returns empty set
Example:
var x = a + b; generates a + b
25
Function 𝑘𝑖𝑙𝑙: 𝑆𝑡𝑚𝑡 → 𝑃(𝐸𝑥𝑝𝑟)
• A statement kills an available expression e
if:
kill function • It modifies any of the variables used in e
• Otherwise, function returns empty set
Example:
a = 23; kills a * b
26
Example
Draw the control flow
graph of this code snippet
27
entry
Example x=a+b
y=a*b
y>a+b
T
F a=a+1
x=a+b
exit
28
entry
Example (1)x = a + b
(2)y = a * b
Non-trivial expressions: (3)y > a + b
a+b
T
a*b (4)a = a + 1
F
a+1
(5)x = a + b
exit
29
entry
Example (1)x = a + b
(2)y = a * b
Non-trivial expressions: a + b, a*b, a + 1 (3)y > a + b
T
Statement s 𝑔𝑒𝑛(𝑠) 𝑘𝑖𝑙𝑙(𝑠) (4)a = a + 1
F
1 {a + b} ∅
2 {a*b} ∅ (5)x = a + b
3 {a + b} ∅
4 ∅ {a + b, a* b, a + 1}
exit
5 {a + b} ∅
30
• Initially, no available expressions
• Forward analysis: Propagate available
expressions in the direction of control flow
Propagating • For each statement 𝑠, outgoing available
available epressions are: incomming available
expressions minus 𝑘𝑖𝑙𝑙𝑠(𝑠) plus 𝑔𝑒𝑛(𝑠)
expressions • When control flow splits, propagate available
expressions both ways
• When control flow merge, intersect the
incoming available expressions
31
Data flow equations entry
(1)x = a + b
• 𝐴𝐸!"#$% (𝑠) : available expression at the entry of s
• 𝐴𝐸!&'# (𝑠) : available expression at the exit of s
(2)y = a * b
• 𝐴𝐸!"#$% 1 = ∅
• 𝐴𝐸!"#$% 2 = 𝐴𝐸!&'# (1) (3)y > a + b
• 𝐴𝐸!"#$% 3 = 𝐴𝐸!&'# 2 ∩ 𝐴𝐸!&'# (5)
T
• 𝐴𝐸!"#$% 4 = 𝐴𝐸!&'# (3) (4)a = a + 1
F
• 𝐴𝐸!"#$% 5 = 𝐴𝐸!&'# (4)
• 𝐴𝐸!&'# 1 = 𝐴𝐸!"#$% 1 ∪ 𝑎 + 𝑏 (5)x = a + b
• 𝐴𝐸!&'# 2 = 𝐴𝐸!"#$% 2 ∪ 𝑎 ∗ 𝑏
exit
• 𝐴𝐸!&'# 3 = 𝐴𝐸!"#$% 3 ∪ 𝑎 + 𝑏
• 𝐴𝐸!&'# 4 = 𝐴𝐸!"#$% 4 \ 𝑎 + 𝑏, 𝑎 ∗ 𝑏, 𝑎 + 1
• 𝐴𝐸!&'# 5 = 𝐴𝐸!"#$% 5 ∪ 𝑎 + 𝑏 32
Solving algorithm
33
• Transfer functions yield data flow
equations for each statement
• At entry, e.g., AE_entry(2) =
Data flow • At exit, e..g., AE_exit(3) =
equations • May depend on each other
• How to solve these equations?
• Goal: Fix point, i.e., nothong changes
any more
34
• For each statement s: Initalize entry and exit sets
• Initialize W with initial/final node (for
forward/backward analysis)
Work list • While W not empty:
• Remove a statement s from W
algorithm • Update entry set of s by applying meet operator
to exit sets of incoming statements
• Compute exit set of s based on its entry set
• If exit set has changed (or statement visted for
the first time): Add successors of s to W
35
Solution of the equation
• 𝐴𝐸!"#$% 1 = ∅
• 𝐴𝐸!"#$% 2 = 𝐴𝐸!&'# (1)
• 𝐴𝐸!"#$% 3 = 𝐴𝐸!&'# 2 ∩ 𝐴𝐸!&'# (5) S 𝐴𝐸!"#$% 𝑆 𝐴𝐸!&'# (𝑆)
1 ∅ 𝑎+𝑏
• 𝐴𝐸!"#$% 4 = 𝐴𝐸!&'# (3)
2 𝑎+𝑏 𝑎 + 𝑏, 𝑎 ∗ 𝑏
• 𝐴𝐸!"#$% 5 = 𝐴𝐸!&'# (4) 3 𝑎+𝑏 𝑎+𝑏
• 𝐴𝐸!&'# 1 = 𝐴𝐸!"#$% 1 ∪ 𝑎 + 𝑏 4 𝑎+𝑏 ∅
• 𝐴𝐸!&'# 2 = 𝐴𝐸!"#$% 2 ∪ 𝑎 ∗ 𝑏 5 ∅ 𝑎+𝑏
• 𝐴𝐸!&'# 3 = 𝐴𝐸!"#$% 3 ∪ 𝑎 + 𝑏
• 𝐴𝐸!&'# 4 = 𝐴𝐸!"#$% 4 \ 𝑎 + 𝑏, 𝑎 ∗ 𝑏, 𝑎 + 1
• 𝐴𝐸!&'# 5 = 𝐴𝐸!"#$% 5 ∪ 𝑎 + 𝑏
36
Solution of the equation
S 𝐴𝐸!"#$% 𝑆 𝐴𝐸!&'# (𝑆)
1 ∅ 𝑎+𝑏
2 𝑎+𝑏 𝑎 + 𝑏, 𝑎 ∗ 𝑏
3 𝑎+𝑏 𝑎+𝑏
4 𝑎+𝑏 ∅
5 ∅ 𝑎+𝑏
At the entry of statement 3, expression 𝑎 + 𝑏 has already been computed
37
Quiz
is x – y an available
expression when
entering the statement
7?
38
Any data flow analysis is defined by six properties:
Defining a • Domain
• Direction
data flow • Transfer function
• Meet operator
analysis • Boundary condition
• Initial values
39
• Analysis associates some information with
every program point
• “Information” means elements of a set
Domain • Domain of the analysis: All possible
elements the set may have
• E.g., for available expressions analysis:
Domain is set of non-trivial expressions
40
• Analysis propagates information along the
control flow graph:
• Forward analysis: normal flow of control
Direction • Backward anlysis: invert all edges
• Reasons about exections in reverse
• E.g., available expression analysis: Forward
41
• Defines how a statement affects the
Transfer propagated information
• 𝐷𝐹3456 (𝑠) = some function of 𝐷𝐹37689 (𝑠)
function • E.g., for available expression analysis:
𝐴𝐸3456 𝑠 = 𝐴𝐸37689 𝑠 ∖ kill 𝑠 ∪ 𝑔𝑒𝑛(𝑠)
42
• What if two statements s:, s; flow to a
statement s?
• Forward analysis: Execution branches merge
Meet
• Backward analysis: branching point
• Meet operator defines how to combine the
operator incoming information
• Union:
DF()*+, s = DF(-.* s/ ∪ DF(-.* (s0 )
• Intersection:
DF()*+, s = DF(-.* s/ ∩ DF(-.* (s0 )
43
• What information to start with at the first CFG
node?
Boundary • Forward analysis: first node is entry node
• Backward analysis: first node is exit node
condition • Common choices:
• Empty set
• Entire domain
44
• What is the information to start with at
Initial intermediate nodes?
• Common choices:
values • Empty set
• Entire domain
45
Any data flow analysis is defined by six properties:
Defining a • Domain
• Direction
data flow • Transfer function
• Meet operator
analysis • Boundary condition
• Initial values
46
Defining a data flow analysis
Any data flow analysis is defined by six Available expression is defined as:
properties:
• Domain • Non-trivial expression
• Direction • Forward
• Transfer function
• 𝐴𝐸!&'# 𝑠 = 𝐴𝐸!"#$% 𝑠 ∖ kill 𝑠 ∪
• Meet operator
𝑔𝑒𝑛(𝑠)
• Boundary condition
• Intersection (∩)
• Initial values
• 𝐴𝐸!"#$% 𝑒𝑛𝑡𝑟𝑦𝑁𝑜𝑑𝑒 = ∅
• ∅
47
Reaching • Goal: for each program point, compute
which assignments may have been made
definitions and may not have been overwritten
• Useful in various program analyses
analysis • E.g. to compute a data flow graph
48
Example
Definition (x)
reaches the
entry of this
statement
49
Example
All
definitions
reaches the
entry of this
statement
50
• Domain: Definitions (assigments) in the code
• Set of pairs (𝑣, 𝑠) of variables and stmts
Defining the • (𝑣, 𝑠) means a definition of 𝑣 at 𝑠
• Direction: forward
Analysis • Meet operator: Union
• Because we care about definitions that may
reach a program point
51
• Transfer function:
𝑅D<456 𝑠 = (𝑅𝐷37689 𝑠 ∖ 𝑘𝑖𝑙𝑙 𝑠 ) ∪ 𝑔𝑒𝑛(𝑠)
• Function 𝑔𝑒𝑛(𝑠)
Defining the • If 𝑠 is assignment to 𝑣: (𝑣, 𝑠)
• Otherwise: empty set
Analysis (2) • Function 𝑘𝑖𝑙𝑙(𝑠)
• If 𝑠 is assignment to 𝑣: (𝑣, 𝑠’) for all 𝑠’ that
define 𝑣
• Otherwise: empty set
52
• Boundary condition: Entry node starts will all
variables undefined
Defining the • Special “statement” for undefined
variables: ?
Analysis (3) • 𝑅𝐷37689 𝑒𝑛𝑡𝑟𝑦𝑁𝑜𝑑𝑒 = 𝑣, ? 𝑣 ∈ 𝑉𝑎𝑟𝑠}
• Initially, all nodes have no reaching
definitions
53
Example
Draw CFG for this code
snippet
54
entry
(1)x = 5
Example
(2)y = 1
(3)x > 1
T
(4)y = x * y
F
(5)x = x - 1
exit
55
entry
(1)x = 5
Example
(2)y = 1
Domain: (x, ?), (x, 1), (x, 5)
(y, ?), (y, 2), (y, 4) (3)x > 1
T
s 𝑔𝑒𝑛(𝑠) 𝑘𝑖𝑙𝑙(𝑠) (4)y = x * y
F
1 {(x, 1)} {(x, 5), (x, ?)}
2 {(y, 2)} {(y, 4), (y, ?)} (5)x = x - 1
3 ∅ ∅
4 {(y, 4)} {(y, 2), (y, ?)}
exit
5 {(x, 5)} {(x, 1), (x, ?)}
56
Data flow equations
entry
(1)x = 5
• 𝑅𝐷!"#$% 1 = 𝑥, ? , 𝑦, ?
• 𝑅𝐷!"#$% 2 = 𝑅𝐷!&'# 1 (2)y = 1
• 𝑅𝐷!"#$% 3 = 𝑅𝐷!&'# 2 ∪ 𝑅𝐷!&'# 5
• 𝑅𝐷!"#$% 4 = 𝑅𝐷!&'# 3 (3)x > 1
• 𝑅𝐷!"#$% 5 = 𝑅𝐷!&'# 4 T
• 𝑅𝐷!&'# 1 = (𝑅𝐷!"#$% 1 ∖ 𝑥, 5 , 𝑥, ? ) ∪ {𝑥, 1} (4)y = x * y
• 𝑅𝐷!&'# 2 = (𝑅𝐷!"#$% 2 ∖ 𝑦, 4 , 𝑦, ? ) ∪ {𝑦, 2} F
• 𝑅𝐷!&'# 3 = 𝑅𝐷!"#$% 3
(5)x = x - 1
• 𝑅𝐷!&'# 4 = (𝑅𝐷!"#$% 4 ∖ 𝑦, 2 , 𝑦, ? ) ∪ {𝑦, 4}
• 𝑅𝐷!&'# 5 = (𝑅𝐷!"#$% 5 ∖ 𝑥, 1 , 𝑥, ? ) ∪ {𝑥, 5}
exit
57
Solution of the equation
• 𝑅𝐷!"#$% 1 = 𝑥, ? , 𝑦, ? S 𝑅𝐷!"#$% 𝑆 𝑹𝑫!&'# (𝑆)
• 𝑅𝐷!"#$% 2 = 𝑅𝐷!&'# 1 1 𝑥, ? , 𝑦, ? 𝑥, 1 , 𝑦, ?
• 𝑅𝐷!"#$% 3 = 𝑅𝐷!&'# 2 ∪ 𝑅𝐷!&'# 5 2 𝑥, 1 , 𝑦, ? 𝑥, 1 , 𝑦, 2
3 𝑥, 1 , 𝑦, 2 , 𝑥, 1 , 𝑦, 2 ,
• 𝑅𝐷!"#$% 4 = 𝑅𝐷!&'# 3 (𝑥, 5), (𝑦, 4) (𝑥, 5), (𝑦, 4)
• 𝑅𝐷!"#$% 5 = 𝑅𝐷!&'# 4 4 𝑥, 1 , 𝑦, 2 , 𝑥, 1
(𝑥, 5), (𝑦, 4) (𝑥, 5), (𝑦, 4)
• 𝑅𝐷!&'# 1 = (𝑅𝐷!"#$% 1 ∖ 𝑥, 5 , 𝑥, ? ) ∪ {𝑥, 1}
5 𝑥, 1 , 𝑥, 5 , 𝑦, 4
• 𝑅𝐷!&'# 2 = (𝑅𝐷!"#$% 2 ∖ 𝑦, 4 , 𝑦, ? ) ∪ {𝑦, 2} (𝑥, 5), (𝑦, 4)
• 𝑅𝐷!&'# 3 = 𝑅𝐷!"#$% 3
• 𝑅𝐷!&'# 4 = (𝑅𝐷!"#$% 4 ∖ 𝑦, 2 , 𝑦, ? ) ∪ {𝑦, 4}
• 𝑅𝐷!&'# 5 = (𝑅𝐷!"#$% 5 ∖ 𝑥, 1 , 𝑥, ? ) ∪ {𝑥, 5}
58
• Goal: for each statement, find variables that
are may be “live” at the exit from the
Live statement
• “live”: the variable is used before being
variables redefined
• Useful, e.g., for identifying dead code
analysis • Bug detection: dead assignments are
typically unexpected
• Optimization: remove dead code
59
Example
x is not live after this statement
60
Example
Both x and y are live after this statement
61
• Domain: all variables occuring in the code
Defining the • Direction: Backward
Analysis
• Meet operator: Union
• Because we care about whether a
variable may be used
62
• Transfer function:
𝐿𝑉!"#$% 𝑠 = 𝐿𝑉!&'# 𝑠 ∖ 𝑘𝑖𝑙𝑙 𝑠 ∪ 𝑔𝑒𝑛(𝑠)
• Backward analysis: Returns set of variables that
are live at entry of statement
Defining the • Function 𝑔𝑒𝑛(𝑠)
Analysis • All variables 𝑣 that are used in 𝑠
• Funtion 𝑘𝑖𝑙𝑙(𝑠)
• If 𝑠 assigns to 𝑥, then it kills 𝑥
• Otherwise: empty set
63
Defining the • Boundary condition: Final node starts with no
live variables
𝐿𝑉!&'# 𝑓𝑖𝑛𝑎𝑙𝑁𝑜𝑑𝑒 = ∅
analysis • Initially, all nodes have no live variables
64
Quiz
Compute the live variables
before and after every
statement
65
• Intra-procedural analysis:
• Reason about a function in isolation
Intra- • Inter-procedural analysis:
vs. • Reason about multiple functions
Inter-procedural • Calls and returns
• Data flow analyses considered so far: intra-
procedural
66
Inter- • One control flow graph per function
procedural • Connect call sites to entry node of
callee
control flow • Connect exit node back to call side
67
entry entry
x=1 [Link](y)
z = bar(5) z = bar(3) return y + 1
exit exit
68
• Arguments passed into call
• Propagate to formal parameters of callee
Propagating • Return value
• Propagate back to caller
information • Local variables
• Do not propagate into callee
• Instead, when call returned, continue
with state just before call
69
Future trends
70
How to create a program analysis?
71
Traditional • Manually crafted
• Years of work
program • Precise, logical reasoning
analysis • Heuristics to handle undecidability
• Challenged by large code bases
72
Insight: Lots of data about software
development to learn from
Neural New code,
execution,
etc.
software Source code
Execution traces
Machine
analysis
Documentation Predictive tool
learning
Bug reports
Etc.
Information
useful for
developer
73
Traditional vs. neural software analysis
• Manually crafted • Automatically
• Years of work learned within hours
• Precise, logical • Data-driven
reasoning prediction
• Heuristics to handel • Learn instead of
undecidability hard-code heuristics
• Challenged by large • Use big code to our
code bases benefit
74
Application • Type prediction
of neural • Bug detection
• Program repair
software • Code summarization
analysis • Code completion
75
Q&A
76