4. Exercise 2: Dataflow Framework (11 tests)

Goal: Implement a powerset lattice (sets of strings) and a generic iterative fixpoint solver that works for both forward and backward analyses.

Time: ~30 minutes

Files to edit:

• exercises/dataflow-framework/starter/lattice.ml -- powerset lattice operations
• exercises/dataflow-framework/starter/dataflow.ml -- iterative fixpoint solver

The powerset lattice

     {a, b, c}        <- top (the full universe)
      / | \
  {a,b} {a,c} {b,c}
    / \  / \  / \
   {a} {b}  {c}
     \  |  /
       {}              <- bottom (empty set)

What to implement (in order)

In lattice.ml:

#	Function	Hint
1	bottom	The empty set: StringSet.empty
2	top	The universe: !universe (dereference the ref)
3	join a b	Set union: StringSet.union
4	meet a b	Set intersection: StringSet.inter
5	equal a b	Set equality: StringSet.equal
6	to_string s	Format as {a, b, c} -- use StringSet.elements and String.concat

In dataflow.ml:

#	Function	Hint
7	solve analysis cfg	Implement the iterative worklist algorithm (see below)

The fixpoint algorithm

Forward case:
  1. Initialize IN[B] = OUT[B] = analysis.init for every block B
  2. Repeat until nothing changes:
       For each block B:
         IN[B]  = merge over all predecessors P: OUT[P]
         OUT[B] = transfer(B, IN[B])
  3. Return (label, IN[B], OUT[B]) for each block

Backward case:
  Swap the roles of IN/OUT and predecessors/successors:
    OUT[B] = merge over all successors S: IN[S]
    IN[B]  = transfer(B, OUT[B])

Hint: Use StringMap to store the IN and OUT values for each block. In each iteration, check whether any value changed using analysis.equal. When nothing changes, you have reached the fixpoint.

Run tests

dune runtest modules/module3-static-analysis/exercises/dataflow-framework/

Starter output:

Fatal error: exception Failure("TODO: return the least element of the powerset lattice")

This fatal error occurs because the bottom value is evaluated at module load time. The test runner crashes immediately before it can show per-test results. Once you implement bottom (and the other lattice functions), you will start seeing per-test output like ........EEE as the solver tests remain TODO.

---