INTERPROCEDURAL
ANALYSIS
with Infinite Domains in WALA
Marianna Rapoport
Ondřej Lhoták
Julian Dolby
Frank Tip
Data Flow Analysis in WALA
2
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
2
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
Abstract
interpretation
[Cousot, POPL’77]
com.ibm.wala.analysis.stackMachine
2
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
Abstract
interpretation
[Cousot, POPL’77]
com.ibm.wala.analysis.stackMachine
2
Context-Sensitive
f();
f() {
...
}
f();
3
Context-Sensitive
f();
f() {
...
}
f();
3
Context-Insensitive
f();
f() {
...
}
f();
4
Data Flow Analysis in WALA
5
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
Abstract
interpretation
[Cousot, POPL’77]
com.ibm.wala.analysis.stackMachine
5
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
Abstract
interpretation
[Cousot, POPL’77]
com.ibm.wala.analysis.stackMachine
IFDS
[Reps, POPL’95]
com.ibm.wala.dataflow.ifds
5
Data Flow Analysis in WALA
Fixed-point
iteration
[Kildall, POPL’73]
com.ibm.wala.fixpoint
Abstract
interpretation
[Cousot, POPL’77]
com.ibm.wala.analysis.stackMachine
IFDS
[Reps, POPL’95]
com.ibm.wala.dataflow.ifds
IDE
[Sagiv, TCS’96]
?
5
IFDS
•
Distributive
•
Interprocedural
context-sensitive
(f u g)(x) ⌘ f (x) u g(x)
O(ED3)
•
Finite
•
6
Subset
IFDS
•
Distributive
•
Interprocedural
context-sensitive
(f u g)(x) ⌘ f (x) u g(x)
O(ED3)
•
Finite
•
6
Subset
IFDS
•
Distributive
•
Interprocedural
context-sensitive
(f u g)(x) ⌘ f (x) u g(x)
O(ED3)
•
Finite
•
6
Subset
IDE
•
•
Interprocedural
context-sensitive
(f u g)(x) ⌘ f (x) u g(x)
O(ED3)
•
Distributive
Environment
7
What can we solve with IFDS?
int y = x + 1;
8
What can we solve with IFDS?
•
int y = x + 1;
8
Is y a constant?
What can we solve with IFDS?
int y = x + 1;
8
•
Is y a constant?
•
Is y a 1, 2, 3, or 4?
What can we solve with IFDS?
int y = x + 1;
8
•
Is y a constant?
•
Is y a 1, 2, 3, or 4?
•
What is the value of y?
What can we solve with IDE?
int y = x + 1;
9
•
Is y a constant?
•
Is y a 1, 2, 3, or 4?
•
What is the value of y?
Outline
•
IFDS algorithm
•
IDE algorithm
•
Solving IDE problems in WALA
10
IFDS
Interprocedural Finite Distributive Subset Framework
[Reps et al., POPL’95]
Linear Constant Propagation
int u = 1;
int v = u;
int w = u + 2;
int y = u + v;
12
int add3(int i) {
int j = i + 3;
return j;
}
void main() {
int x = 2;
int y = add3(x);
...
}
13
Control Flow Graph
start main()
start add3(int
int x = 2
i)
int j = i + 3
return j
int y = add3(x)
end add3(int
…
end main()
14
i)
Supergraph
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
15
i)
Supergraph
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
15
i)
Supergraph
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
15
i)
Supergraph
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
15
i)
Supergraph
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
15
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + 3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + j
3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int x = 2
call
int j = i + j
3
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
16
i)
Exploded Supergraph
0 i j
0 x y
start main()
start add3(int
int j = i + 3
int x = 2
call
return j
y = add3(x)
return y
i)
end add3(int
= add3(x)
…
end main()
17
i)
IDE
Interprocedural Distributive Environment Framework
[Sagiv et al., TCS’96]
19
IFDS
IDE
19
IFDS
IDE
does fact hold?
what value
corresponds to fact?
19
IFDS
IDE
does fact hold?
what value
corresponds to fact?
graph reachability
graph reachability
+ environment
19
IFDS
IDE
does fact hold?
what value
corresponds to fact?
graph reachability
graph reachability
+ environment
exploded supergraph
labeled
exploded supergraph
19
Defining IDE Problem
Lattice
>
...
2
1
0
?
20
1
2
...
Defining IDE Problem
Lattice
>
...
2
1
0
?
20
1
2
...
Defining IDE Problem
Lattice
>
...
2
1
0
?
20
1
2
...
Defining IDE Problem
Lattice
>
...
2
1
0
?
l 1 u l2
20
1
2
...
Defining IDE Problem
Micro Functions
0
int y = x + 3;
21
x
y
Defining IDE Problem
Micro Functions
0
int y = x + 3;
x
y
l.l + 3
21
Labeled
Exploded Supergraph
start main()
0
x
y
0
int x = 2
i
j
start add3(int
i)
int j = i + 3
call
y = add3(x)
return j
return
y = add3(x)
end add3(int
…
end main()
22
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
i
j
int x = 2
start add3(int
i)
int j = i + 3
l.l
y = add3(x)
return
y = add3(x)
+3
call
return j
end add3(int
…
end main()
22
i)
Labeled
Exploded Supergraph
start main()
x
0
y
0
i
j
int x = 2
y = add3(x)
+3
return
l.l
y = add3(x)
i)
int j = i + 3
l.2
call
start add3(int
return j
end add3(int
…
end main()
22
i)
Labeled
Exploded Supergraph
start main()
x
0
y
0
l.l
i
j
i)
l.l
int x = 2
int j = i + 3
l.l
l.l
l.2
+3
call
start add3(int
y = add3(x)
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
l.l
end main()
22
i)
Labeled
Exploded Supergraph
start main()
x
0
y
0
i
l.l
j
i)
l.l
int x = 2
int j = i + 3
l.l
l.l
l.2
+3
call
start add3(int
y = add3(x)
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
int x = 2
x
0
0
i
j
start add3(int
i)
l.l
l.l
int j = i + 3
l.l
l.l
l.2
+3
call
y
y = add3(x)
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
i
j
start add3(int
i)
l.l
int x = 2
int j = i + 3
y = add3(x)
+3
call
l.l
l.l
l.2
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
i
l.2
j
start add3(int
i)
l.l
int x = 2
int j = i + 3
l.l
+3
call
y = add3(x)
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
i
0
j
int x = 2
i)
int j = i + 3
l.l
l.2
+3
call
start add3(int
y = add3(x)
return j
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
j
i
int x = 2
call
start add3(int
i)
int j = i + 3
return j
y = add3(x)
l.5
l.l
return
end add3(int
y = add3(x)
…
l.l
end main()
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
i
j
int x = 2
start add3(int
i)
int j = i + 3
call
y = add3(x)
return j
return
y = add3(x)
end add3(int
…
l.l
end main()
23
l.5
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
int x = 2
i
j
start add3(int
int j = i + 3
call
y = add3(x)
return j
return
y = add3(x)
end add3(int
…
end main()
i)
l.5
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
int x = 2
i
j
start add3(int
int j = i + 3
call
y = add3(x)
return j
return
y = add3(x)
end add3(int
…
end main()
i)
( l . 5)>
23
i)
Labeled
Exploded Supergraph
start main()
0
x
y
0
int x = 2
i
j
start add3(int
int j = i + 3
call
y = add3(x)
return j
return
y = add3(x)
end add3(int
…
end main()
i)
( l . 5)> = 5
23
i)
Defining IDE Problem
Micro Functions
int x = 2;
int x = 1;
l.2
l.1
24
Defining IDE Problem
Micro Functions
int x = 2;
int x = 1;
l.2
l.1
( l . 2) u ( l . 1)
24
Defining IDE Problem
Micro Functions
int x = 2;
int x = 1;
l.2
l.1
( l . 2) u ( l . 1)
l.2 u 1
24
Defining IDE Problem
Micro Functions
int x = 2;
int x = 1;
l.2
l.1
( l . 2) u ( l . 1)
l.2 u 1
l.?
24
IDE in WALA
IDE in WALA
in Scala
class ConstantPropagationProblem extends IdeProblem
•
Value Lattice
•
Micro Functions
•
Flow Functions
•
Supergraph (WALA)
26
Copy Constant Propagation
int u = 1;
int v = u;
int w = u + 2;
int y = u + v;
27
Value Lattice
trait CpLatticeElem extends Lattice[CpLatticeElem] {
override def ⊓(n: CpLatticeElem): CpLatticeElem
}
28
Value Lattice
trait CpLatticeElem extends Lattice[CpLatticeElem] {
override def ⊓(n: CpLatticeElem): CpLatticeElem
}
case class Num(n: Int) extends CpLatticeElem {
override def ⊓(ln: CpLatticeElem): CpLatticeElem = ln match {
case Num(m) => if (n == m) ln else ⊥
case ⊥
=> ⊥
case
⊤
=> n
}
}
28
Value Lattice
trait CpLatticeElem extends Lattice[CpLatticeElem] {
override def ⊓(n: CpLatticeElem): CpLatticeElem
}
case class Num(n: Int) extends CpLatticeElem {
override def ⊓(ln: CpLatticeElem): CpLatticeElem = ln match {
case Num(m) => if (n == m) ln else ⊥
case ⊥
=> ⊥
case
=> n
⊤
}
}
case object
⊤
override def
extends CpLatticeElem {
⊓(n:
CpLatticeElem): CpLatticeElem = n
}
28
Value Lattice
trait CpLatticeElem extends Lattice[CpLatticeElem] {
override def ⊓(n: CpLatticeElem): CpLatticeElem
}
case class Num(n: Int) extends CpLatticeElem {
override def ⊓(ln: CpLatticeElem): CpLatticeElem = ln match {
case Num(m) => if (n == m) ln else ⊥
case ⊥
=> ⊥
case
=> n
⊤
}
}
case object
⊤
override def
extends CpLatticeElem {
⊓(n:
CpLatticeElem): CpLatticeElem = n
}
case object
⊥
override def
extends CpLatticeElem {
⊓(n:
CpLatticeElem): CpLatticeElem =
}
28
⊥
Micro Functions
application, composition, meet
•
29
Micro Functions
application, composition, meet
•
l.c
l.l u c
29
Micro Functions
application, composition, meet
•
l.c
l.l u c
case class CpFunction(c: LatticeElem, meet: Boolean)
extends MicroFunction
29
Micro Functions
application, composition, meet
•
l.c
CpFunction(c, false)
l.l u c
CpFunction(c, true)
case class CpFunction(c: LatticeElem, meet: Boolean)
extends MicroFunction
29
Micro Functions
case class CpFunction(
c: LatticeElem,
meet: Boolean
) extends MicroFunction {
}
30
Micro Functions
case class CpFunction(
c: LatticeElem,
meet: Boolean
) extends MicroFunction {
override def apply(arg: LatticeElem): LatticeElem =
if (meet) c ⊓ arg
else c
}
30
Micro Functions
case class CpFunction(
c: LatticeElem,
meet: Boolean
) extends MicroFunction {
override def apply(arg: LatticeElem): LatticeElem =
if (meet) c ⊓ arg
else c
override def
⊓(f: CpFunction): CpFunction
CpFunction(c ⊓ f.c, meet || f.meet)
}
30
=
Micro Functions
case class CpFunction(
c: LatticeElem,
meet: Boolean
) extends MicroFunction {
override def apply(arg: LatticeElem): LatticeElem =
if (meet) c ⊓ arg
else c
override def
⊓(f: CpFunction): CpFunction
CpFunction(c ⊓ f.c, meet || f.meet)
=
override def ◦(f: CpFunction): CpFunction =
if (meet) CpFunction(c ⊓ f.c, f.meet)
else this
}
30
Flow Functions
x
0
start
y
0
l.l
i
j
l.l
int x = 2
int j = i + 3
l.l
l.l
l.2
+3
call
start
y = add3(x)
return j
l.l
return
end
l.l
l.l
end
31
Flow Functions
0
x
int x = 2
call
y = add3(x)
32
l.2
l.l
y
Flow Functions
0
x
int x = 2
call
y = add3(x)
33
l.2
l.l
y
Flow Functions
call
return
34
Flow Functions
•
call-start
call
return
34
Flow Functions
•
call-start
•
end-return
call
return
34
Flow Functions
•
call-start
•
end-return
call
•
call-return
return
34
Flow Functions
•
call-start
•
end-return
call
•
call-return
•
default
return
34
Now You Can
35
Now You Can
•
IFDS ⟶ IDE
35
Now You Can
•
IFDS ⟶ IDE
•
IDE problems in WALA
Constant propagation
Type-state analysis
35
Now You Can
•
IFDS ⟶ IDE
•
IDE problems in WALA
Constant propagation
Type-state analysis
35
Now You Can
•
IFDS ⟶ IDE
•
IDE problems in WALA
Constant propagation
Type-state analysis
•
sophisticated
IFDS ⟶ special IDE
SPLLift [Bodden et al., PLDI’13] Correlated calls [Rapoport et al., SAS’15 (to appear)]
35
IDE for WALA
github.com/amaurremi/IDE
36