> For the complete documentation index, see [llms.txt](https://p4d0rn.gitbook.io/java/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://p4d0rn.gitbook.io/java/code-inspector/theory/static-analysis/dfa.md).
# DFA
## Overview of DFA
DFA：Data Flow Analysis
How application-specific data flows through the nodes and edges of CFG（source code->IR->CFG）
> most static analyzer tends to may analysis
>
> * may analysis
> * outputs information that may be true (over-approximation)
> * must analysis
> * outputs information that must be true (under-approximation)
different data-flow analysis applications have
different data abstraction and
different flow safe-approximation strategies and
different transfer functions and control-flow handlings
> e.g., determine the sgin of a variable
>
> data abstraction：+、-、0、unknown、undefined
>
> transfer function：+ op + = + , + op - = -
>
> control-flow handlings：union the signs at merges
## Preliminaries of DFA
### Input and Output States
* Each execution of an IR statement transforms an input state to a new output state
* The input/output state is associated with the program point before/after the statement
* 
> In each data-flow analysis application, we associate with every program point a data-flow value that represents an abstraction of the set of all possible program states that can be observed for that point.
>
> 
DFA is to find a solution to a set of safe-approximation-directed constraints on the IN\[s]’s and OUT\[s]’s for all statements
* constraints based on semantics of statements（transfer function）
* constraints based on the flows of control
### Transfer Function
### Control Flow
## Reaching Definitions analysis
> A definition d at program point p reaches a point q if there is path from p to q such that d is not “killed” along that path
* A definition of a variable v is a statement that assigns a value to v
* how to be “killed”: new definition of v
Reaching definitions can be used to detect possible undefined variables.
> e.g., introduce a dummy definition for each variable v at the entry of CFG, and if the dummy definition of v reaches a point p where v is used, then v may be used before definition (as undefined reaches v)
So reaching definitions analysis is may analysis.
(不放过动态运行时所有可能的路径)
### Abstraction
The definitions of all the variables in a program can be represented by bit vectors.
### Safe-Approximation
#### Transfer Function
> genB：definitions generated in this BB.
>
> killB: new definition D in this BB kills other definitions
>
> The definitions in genB can reach the program point at OUT\[B] and those in killB can't reach the program point at OUT\[B]
>
> obviously, same variables in definition bit vectors can not exist at the same time.
#### Control Flow
reaching definition is a may analysis.So here use union(∪) as the meet operator.
#### Algorithm
For Example:
CFG above can be transfered to pseudo-code below.
```
D1
D2
do {
D3
D4
if(condition){
D5
D6
} else {
D7
break
}
} while(condition)
D8
```
* Iteration 0 —— init
* Iteration 1
IN\[B1] = 0000 0000 = OUT\[Entry]
OUT\[B1] = 1100 0000 generate D1、D2
IN\[B2] = 1100 0000 = OUT\[B1] ∪ OUT\[B4]
OUT\[B2] = 1011 0000 generate D3、D4，kill D2
IN\[B3] = 1011 0000 = OUT\[B2]
OUT\[B3] = 0011 0010 generate D7，kill D1
IN\[B4] = 1011 0000 = OUT\[B2]
OUT\[B4] = 0011 1100 generate D5、D6，kill D1
IN\[B5] = 0011 1110 = OUT\[B4] ∪ OUT\[B3]
OUT\[B5] = 0011 1011 generate D8, kill D6
* Iteration 2
IN\[B1] = 0000 0000 = OUT\[Entry]
OUT\[B1] = 1100 0000 generate D1、D2
IN\[B2] = 1111 1100 = OUT\[B1] ∪ OUT\[B4]
OUT\[B2] = 1011 1100 generate D3、D4，kill D2
IN\[B3] = 1011 1100 = OUT\[B2]
OUT\[B3] = 0011 0110 generate D7，kill D1、D5
IN\[B4] = 1011 1100 = OUT\[B2]
OUT\[B4] = 0011 1100 generate D5、D6，kill D1、D7、D8
IN\[B5] = 0011 1110 = OUT\[B4] ∪ OUT\[B3]
OUT\[B5] = 0011 1011 generate D8, kill D6
* Iteration 3
IN\[B1] = 0000 0000 = OUT\[Entry]
OUT\[B1] = 1100 0000 generate D1、D2
IN\[B2] = 1111 1100 = OUT\[B1] ∪ OUT\[B4]
OUT\[B2] = 1011 1100 generate D3、D4，kill D2
IN\[B3] = 1011 1100 = OUT\[B2]
OUT\[B3] = 0011 0110 generate D7，kill D1、D5
IN\[B4] = 1011 1100 = OUT\[B2]
OUT\[B4] = 0011 1100 generate D5、D6，kill D1、D7、D8
IN\[B5] = 0011 1110 = OUT\[B4] ∪ OUT\[B3]
OUT\[B5] = 0011 1011 generate D8, kill D6
The final result is the green part which means definitions can reach this point in the program.
> Why this iterative algorithm can finally stop?
>
> 
>
> INs will not change if OUTs do not change
>
> OUTs will not change if INs do not change
>
> Reach a fixed point. Also related with monotonicity
## Live Variables Analysis
Live variables analysis tells whether the value of variable v at program point p could be used along some path in CFG starting at p.If so, v is live at p; otherwise, v is dead at p.
> information of live variables can be used for register allocations.
>
> e.g., all registers are full and we need to use one, then we should favor using a register with a dead value.
### Abstraction
All variables in a program can be represented by bit vectors.
### Safe-Approximation
redefinition will break the path. forwards analysis requires record of previous state, so we use **backwards analysis**
One live path will be ok, so we use **may analysis**
#### Control Flow
#### Transfer Function
> useB：variables used before redefined in B
>
> defB：variables redefined in B
>
> OUT\[B]：variables live coming out of B
note: we focus on the live state of variables at some program point.
#### Algorithm
* Iteration 0 —— init
* Iteration 1
IN\[Exit] = 000 0000
OUT\[B5] = 000 0000 = IN\[Exit]
IN\[B5] = 000 1000 use p, redefine z
OUT\[B3] = 000 1000 = IN\[B5]
IN\[B3] = 100 1000 use x
OUT\[B4] = 000 1000 = IN\[B5] ∪ IN\[B2]
IN\[B4] = 010 1000 use y, redefine x、q
OUT\[B2] = 110 1000 = IN\[B3] ∪ IN\[B4]
IN\[B2] = 100 1001 use k, redefine m、y
OUT\[B1] = 100 1001 = IN\[B2]
IN\[B1] = 001 1101 use p、q、z, redefine x、y
* Iteration 2
IN\[Exit] = 000 0000
OUT\[B5] = 000 0000 = IN\[Exit]
IN\[B5] = 000 1000 use p, redefine z
OUT\[B3] = 000 1000 = IN\[B5]
IN\[B3] = 100 1000 use x
OUT\[B4] = 100 1001 = IN\[B5] ∪ IN\[B2]
IN\[B4] = 010 1001 use y, redefine x、q
OUT\[B2] = 110 1001 = IN\[B3] ∪ IN\[B4]
IN\[B2] = 100 1001 use k, redefine m、y
OUT\[B1] = 100 1001 = IN\[B2]
IN\[B1] = 001 1101 use p、q、z, redefine x、y
* Iteration 3
IN\[Exit] = 000 0000
OUT\[B5] = 000 0000 = IN\[Exit]
IN\[B5] = 000 1000 use p, redefine z
OUT\[B3] = 000 1000 = IN\[B5]
IN\[B3] = 100 1000 use x
OUT\[B4] = 100 1001 = IN\[B5] ∪ IN\[B2]
IN\[B4] = 010 1001 use y, redefine x、q
OUT\[B2] = 110 1001 = IN\[B3] ∪ IN\[B4]
IN\[B2] = 100 1001 use k, redefine m、y
OUT\[B1] = 100 1001 = IN\[B2]
IN\[B1] = 001 1101 use p、q、z, redefine x、y
The final result is the green part which means variable is live along the path(can be used in future) from this program point
## Available Expressions Analysis
An expression `x op y` is available at program point p if
1. all paths from the entry to p must pass through the evaluation of `x op y`
2. after the last evaluation of `x op y`, there is no redefinition of x or y
> available expressions can be used for detecting global common subexpressions.
### Abstraction
All the expressions in a program can be represented by bit vectors.
### Safe-Approximation
#### Transfer Function
#### Control Flow
All paths from entry to point p must pass through the evaluation of `x op y`，so we use must analysis
for safety of the analysis, it may report an expression as unavailable even if it is truly available.（用于编译器优化，不能优化错误的内容, under-approximation）
#### Algorithm
* Iteration 0 —— init
* Iteration 1
OUT\[Entry] = 00000
IN\[B1] = 00000
OUT\[B1] = 10000 generate E1
IN\[B2] = 10000 OUT\[B1] ∩ OUT\[B4]
OUT\[B2] = 01010 generate E2、E4，kill E1
IN\[B3] = 01010 = OUT\[B2]
OUT\[B3] = 00011 generate E5，kill E2
IN\[B4] = 01010 = OUT\[B2]
OUT\[B4] = 01110 generate E3、E4
IN\[B5] = 00010 = OUT\[B3] ∩ OUT\[B4]
OUT\[B5] = 01010 generate E4、E2，kill E3
* Iteration 2
OUT\[Entry] = 00000
IN\[B1] = 00000
OUT\[B1] = 10000 generate E1
IN\[B2] = 00000 OUT\[B1] ∩ OUT\[B4]
OUT\[B2] = 01010 generate E2、E4，kill E1
IN\[B3] = 01010 = OUT\[B2]
OUT\[B3] = 00011 generate E5，kill E2
IN\[B4] = 01010 = OUT\[B2]
OUT\[B4] = 01110 generate E3、E4
IN\[B5] = 00010 = OUT\[B3] ∩ OUT\[B4]
OUT\[B5] = 01010 generate E4、E2，kill E3
## Summary
