> 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-foundation.md).

# DFA-Foundation

## Iterative Algorithm

Here is a classic iterative algorithm template for May & Forward analysis

![image-20240405093548478](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-b453317f6def8c8b36097308e7af8813af6e451a%2Fimage-20240405093548478.png?alt=media)

Let’s view it in another way

* Given a CFG with k nodes, the iterative algorithm updates OUT\[n] for every node n in each iteration.
* Assume the domain of the values in data flow analysis is V, let’s define a k-tuple: (OUT\[n1], OUT\[n2], …, OUT\[nk]) as an element of set (V1 × V2 … × Vk) denoted as Vk, to hold the values of the analysis after each iteration.
* Each iteration can be considered as taking an action to map an element of Vk to a new element of Vk, through applying the transfer functions and control-flow handing, abstracted as a function F: Vk → Vk
* Then the algorithm outputs a series of k-tuples iteratively until a k-tuple is the same as the last one in two consecutive iterations.

![image-20240405094013650](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-a8830849562863eb2c0756bc13e947e024fa97f5%2Fimage-20240405094013650.png?alt=media)

X is a fixed point of function F if `X = F(X)`

We say the iterative algorithm reaches a fixed point.

## Partial Order

### poset

![image-20240405094243100](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-dce0ea1e62de4e31d7501da984c94ee86d54f93b%2Fimage-20240405094243100.png?alt=media)

Some examples of poset:

* (S, ≤) , S is a set of integers
* (S, substring) , S is a set of English words
* (S, subset) , S is the power set of set {a,b,c}

### upper & lower bounds

![image-20240405094641615](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-8c9ab81423949e53c30031919ef27be5d8a80b03%2Fimage-20240405094641615.png?alt=media)

![image-20240405094725002](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-018ae9d46ac21d5aae671d0e064ed27367302b30%2Fimage-20240405094725002.png?alt=media)

![image-20240405094807219](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-240f5d674b1d06a116d8159258a6c8cdbdb34f05%2Fimage-20240405094807219.png?alt=media)

![image-20240405094956644](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-4def44beaf1416a522f575c8a042d1013cfc6643%2Fimage-20240405094956644.png?alt=media)

Obviously, as long as there is an upper bound or a lower bound, the corresponding lub and glb also exist.

## Lattice

![image-20240405095221142](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-73f0946e0586ba668766f7b471dca295bcf0fd3c%2Fimage-20240405095221142.png?alt=media)

Some examples of lattice:

* (S, ≤) , S is a set of integers
  * ⊔ means “max”
  * ⊓ means “min”
* (S, subset) , S is the power set of set {a,b,c}
  * ⊔ means ∪
  * ⊓ means ∩

### Semilattice

![image-20240405095649604](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-3c48dc9326500f871675ce77535287904974e7ee%2Fimage-20240405095649604.png?alt=media)

### Complete Lattice

![image-20240405095713765](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-6c6fc3d849d216977cba96a84011e5a61e3a669d%2Fimage-20240405095713765.png?alt=media)

Some examples of complete lattice:

* (S, ≤) , S is a set of integers
  * × not a complete lattice
  * it has no ⊔S（+∞）
* (S, subset) , S is the power set of set {a,b,c}
  * √

Note: the definition of bounds implies that the bounds are not necessarily in the subsets (but they must be in the lattice)

![image-20240405100122578](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-7c49a43934d3a28fd54dd5a0faa7677c1210b7dd%2Fimage-20240405100122578.png?alt=media)

A complete lattice is not necessarily a finite lattice!

### Product Lattice

![image-20240405101104252](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-e3992e3e542ffa562aafda0825cfd6c5ec2c5a18%2Fimage-20240405101104252.png?alt=media)

### DFA Framework via Lattice

![image-20240405101304929](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-69aaca4d99c4a317478b0ee9d9f399cf98625af4%2Fimage-20240405101304929.png?alt=media)

The IN and OUT of every node can be seen as a latice.（data flow value）

![image-20240405103624941](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-9ff8f990d5a6dc97aa3c58328c8853e75a6c5cb7%2Fimage-20240405103624941.png?alt=media)

![image-20240405103653446](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-11236d3fc3e6872a4fa89f3f826b9e1a5e7dff28%2Fimage-20240405103653446.png?alt=media)

![image-20240405103708296](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-5c6b79fb3e2a76298ede153235a157ad4f6efad1%2Fimage-20240405103708296.png?alt=media)

![image-20240405103733012](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-b9510558b56e35efad97514e0ba744a37af0657f%2Fimage-20240405103733012.png?alt=media)

Data flow analysis can be seen as iteratively applying transfer functions and meet/join operations on the values of a lattice

### Monotonicity

![image-20240405104548572](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-dc1d4fa264e4195d8019416429ef4f6890292d07%2Fimage-20240405104548572.png?alt=media)

### Fixed Point Theorem

![image-20240405104608361](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-8acdf28794eb5c742d091cfb50362cb8572ca238%2Fimage-20240405104608361.png?alt=media)

Proof：

![image-20240405111438552](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-a407f641dc19f3633de7e6a6ef4ea7c1569c6cba%2Fimage-20240405111438552.png?alt=media)

![image-20240405111741958](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-5bf51f3c17895b6b409ddafbc2d2816628cc9b3b%2Fimage-20240405111741958.png?alt=media)

## Relate to Iterative Algorithm

![image-20240405120423891](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-acce22b92a757e4ae9850c81e236cb73f71add3a%2Fimage-20240405120423891.png?alt=media)

two conditions of fixed point theorem:

* L is finite
* f is monotonic

If a product lattice Lk is a product of complete(and finite) lattices, i.e., (L, L, …, L), then Lk is also complete (and finite) =》 L is a finite and complete lattice

In each iteration, it is equivalent to think that we apply function F which consists of

* transfer function fi: L → L for every node
* join/meet function ⊔/⊓: L×L×L... → L for control-flow influence

How to prove function F is monotonic?

first, transfer function is obviously monotonic(Gen/Kill function is monotonic, IN/OUT never shrinks)

next, prove that ⊔/⊓ is monotonic

![image-20240405120943340](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-d92fd0202e060353a45712df02f7c82b222ba7e3%2Fimage-20240405120943340.png?alt=media)

When will the algorithm reach the fixed point?

![image-20240405121202416](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-1bcd04d4fb9cdef78392759b2b947b0a5bfd4bd0%2Fimage-20240405121202416.png?alt=media)

To sum up, we can draw these conclusions:

1. the iterative algorithm is guaranteed to terminate（reach the fixed point）
2. There may be more than one solution, but our solution is the best one（least/greatest fixed point）
3. Worst case of iterations: lattice height × nodes num in CFG

### May & Must analysis

What is the meaning of top and bottom?

Take *Reaching Definition* for example：

Suppose there is a scenario where the program checks the *undefine error*. We set a dummy definition for each variable, which means that the variable is undefined. Obviously, they should be set to a value of 0 at first, indicating that all undefined variable will not reach this program point. This is an unsafe result because there may be some undefined variables. This is bottom.

For the top, the values are all 1 which means that all definitions may reach. This is a safe but useless result.

We need the fixed point to stay at the safe area and close to the Truth as long as possible. That is, we need the optimal solution.（least/greatest fixed point）

![image-20240405125725741](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-472a43494a02baff96785a166de39b13efdbb533%2Fimage-20240405125725741.png?alt=media)

## MOP

How precise is our solution?

MOP: Meet Over All Paths

![image-20240405143022516](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-6023ee039ca117bb5363d9114298ff5923123850%2Fimage-20240405143022516.png?alt=media)

MOP is only a conceptual metric, as it is not practical to enumerate all paths (there may be path explosions).

![image-20240405143044398](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-58e705b1e3e58dfdbaccbc57f09c1c871d81d1dd%2Fimage-20240405143044398.png?alt=media)

![image-20240405143115949](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-7b86ec9729b729eec52d44975d1380b6bbf248f5%2Fimage-20240405143115949.png?alt=media)

Bit-vector or Gen/Kill problems(set union/intersection for join/meet) are distributive.

But some analyses are not distributive

## Constant Propagation

Given a variable x at program point p, determine whether x is guaranteed to hold a constant value at p.

The OUT of each node in CFG, includes a set of pairs (x, v) where x is a variable and v is the value held by x after that node

![image-20240405143505512](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-9c20fcaa72a15f8498f8ff6635c2ce81f313500c%2Fimage-20240405143505512.png?alt=media)

![image-20240405143531481](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-d02ba29347f1f92d24c9106b1da7e4a77f3f2f20%2Fimage-20240405143531481.png?alt=media)

![image-20240405143627014](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-35afd538bf51fe25675f8a6cfd7b75e2a9c7715f%2Fimage-20240405143627014.png?alt=media)

## Worklist algorithm

an optimization of Iterative Algorithm.

As iteration goes on in the iterative algorithm, we need to apply F to every node even if one node’s OUT changes.

![image-20240405144258241](https://1239337109-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2HLPOkuOfb7iyCzDJ8vA%2Fuploads%2Fgit-blob-33342f4c2f48491798d061b9727f30221f037baf%2Fimage-20240405144258241.png?alt=media)