L12 - Control-Flow Graphs

Back to Program Verification Index | Previous: (y-11) Nondeterminism: Havoc and Assume | Next: (y-13) Predicate Transformers

Mental Model for Control-Flow Graphs (CFGs)

• Flattening Code: Real programs have nested structure (if inside while inside if). A CFG flattens this into a simple directed graph of locations and transitions.
• Edges are Statements: Every edge in the graph represents a single “primitive” operation (Assignment, Havoc, or Assume).
• Paths as Executions: A program execution is just a path from the Initial Location to the Exit Location.
• Verification Ready: Most automated tools (like Ultimate Automizer) convert code into a CFG before applying any verification algorithms.

Formal Definition of a CFG

A Control-Flow Graph is a tuple $G=(Loc,\Delta ,{\ell }_{\text{init}},{\ell }_{\text{ex}})$ where:

• $Loc$: A finite set of Locations (the nodes of the graph).
• $\Delta$: A set of Transitions $(\ell ,\text{stmt},{\ell }^{\prime })$. Each transition moves the program from one location to another by executing a statement.
• ${\ell }_{\text{init}}$: The starting point of the program.
• ${\ell }_{\text{ex}}$: The normal termination point of the program.

Types of Transition Statements

1. Assignments: x := expr or a[i] := expr.
2. Havoc: havoc x.
3. Assume: assume P.

---

Translating Boostan to CFG

Complex control structures are “desugared” into Assume statements and graph edges.

1. If-Then-Else

An if (B) {st1} else {st2} statement starting at ${\ell }_{\text{in}}$ and ending at ${\ell }_{\text{out}}$ becomes:

• True Branch: An edge $({\ell }_{\text{in}},\text{assume }B,{\ell }_1)$ where ${\ell }_1$ is the start of $s{t}_1$.
• False Branch: An edge $({\ell }_{\text{in}},\text{assume }\neg B,{\ell }_2)$ where ${\ell }_2$ is the start of $s{t}_2$.

2. While Loops

A while (B) {st} loop starting at ${\ell }_{\text{loop}}$ (the loop head) becomes:

• Entry Edge: An edge $({\ell }_{\text{loop}},\text{assume }B,{\ell }_{\text{body}})$ where ${\ell }_{\text{body}}$ is the start of the loop body.
• Back Edge: The body of the loop eventually leads back to ${\ell }_{\text{loop}}$.
• Exit Edge: An edge $({\ell }_{\text{loop}},\text{assume }\neg B,{\ell }_{\text{after}})$ where ${\ell }_{\text{after}}$ is the next statement after the loop.

3. Assert Statements (Error Locations)

To verify correctness, assert P is translated using a special Error Location (${\ell }_{\text{err}}$):

• If the assertion holds, the program continues normally to ${\ell }_{\text{next}}$.
• If the assertion fails, the program transitions to the error location.
• Formal Transition:
  • $({\ell }_{\text{curr}},\text{assume }P,{\ell }_{\text{next}})$
  • $({\ell }_{\text{curr}},\text{assume }\neg P,{\ell }_{\text{err}})$
• Goal: Prove that ${\ell }_{\text{err}}$ is unreachable from the start of the program.

---

Program Executions and Correctness

An Execution is a sequence of states $(s_0,s_1,\dots ,s_n)$ that follows a path of transitions $({\ell }_0,{\text{st}}_1,{\ell }_1,\dots ,{\text{st}}_n,{\ell }_n)$ in the graph.

---

Summary

1. CFGs simplify program analysis by turning structured code into a directed graph.
2. Locations represent points in the program execution; Edges represent atomic actions.
3. Complex Logic (if, while) is handled by branching with assume statements.
4. Verification becomes a graph-reachability problem: “Can we reach the error location?”
5. Tools prefer CFGs because they provide a uniform way to represent different programming languages.

Self-Check

1. What four components make up a CFG $G$, and what does each contribute?

Answer

$G=(Loc,\Delta ,{\ell }_{\text{init}},{\ell }_{\text{ex}})$. $Loc$ is the finite set of locations (nodes), $\Delta$ is the set of transition edges labelled with primitive statements (assignment, havoc, assume), ${\ell }_{\text{init}}$ is the unique entry, and ${\ell }_{\text{ex}}$ is the normal exit. Together they describe every execution as a path from ${\ell }_{\text{init}}$ to some terminal location.

2. How is if (B) { st1 } else { st2 } translated into a CFG?

Answer

The branching node has two outgoing edges from ${\ell }_{\text{in}}$: one labelled assume B leading to the start of $s{t}_1$, and one labelled assume !B leading to the start of $s{t}_2$. Both sub-CFGs merge at the join location ${\ell }_{\text{out}}$. The branch condition becomes an assume on each path.

3. How does a while (B) { st } loop appear as a CFG fragment?

Answer

A loop head ${\ell }_{\text{loop}}$ has two outgoing edges: assume B into the body ${\ell }_{\text{body}}$ and assume !B to the post-loop location ${\ell }_{\text{after}}$. The body’s CFG ends with a back-edge to ${\ell }_{\text{loop}}$. The loop unfolds into an arbitrary number of body traversals controlled by the guard.

4. How is assert P modeled in a CFG, and what does verification reduce to?

Answer

An assert at ${\ell }_{\text{curr}}$ creates two edges: assume P to ${\ell }_{\text{next}}$ (the assertion held) and assume !P to a special error location ${\ell }_{\text{err}}$ (the assertion failed). Verification reduces to showing ${\ell }_{\text{err}}$ is unreachable from ${\ell }_{\text{init}}$: no path of transitions leads there in some execution.

5. What is a program execution along a CFG path?

Answer

A sequence of states $(s_0,s_1,\dots ,s_n)$ that follows a path of transitions $({\ell }_0,s{t}_1,{\ell }_1,\dots ,s{t}_n,{\ell }_n)$, where each consecutive pair $(s_{i-1},s_i)$ lies in $[[s{t}_i]]$. The CFG path picks which transitions fire; the state sequence is the actual data witness that those transitions are individually executable.

---

Back to Program Verification Index | Previous: (y-11) Nondeterminism: Havoc and Assume | Next: (y-13) Predicate Transformers | (y) Return to Notes | (y) Return to Home