Work on this exercise locally

This web app is a reference guide — you can read instructions, browse starter code, and view tests here. To actually complete the exercise, you need to work in your local development environment.

1Clone the repo: git clone https://github.com/weihaoqu/program-analysis-bootcamp-student
2Edit the starter file in your editor (VS Code, Vim, etc.) — replace failwith "TODO" with your implementation.
3Run the tests: dune runtest modules/module4-abstract-interpretation/exercises/constant-propagation

Constant Propagation

6. Exercise 2: Constant Propagation (23 tests)

Goal: Implement the flat constant lattice and an expression evaluator.

Time: ~20 minutes

Files to edit:

  • exercises/constant-propagation/starter/constant_domain.ml — the lattice
  • exercises/constant-propagation/starter/constant_eval.ml — expression evaluator

The flat constant lattice

              Top             "not a constant"
         /  |  |  |  \
  ... Const(-1) Const(0) Const(1) ...
         \  |  |  |  /
              Bot             "unreachable"

What to implement

In constant_domain.ml:

#FunctionHint
1–8bottom, top, join, meet, leq, equal, widen, to_stringSame pattern as sign, but values are Bot | Const of int | Top
9abstract_binop op a bIf both are Const, compute the concrete result. Handle Div by zero → Bot. Any TopTop, any BotBot
10abstract_unaryop op aNeg negates the constant, Not inverts (treat nonzero as true)

In constant_eval.ml:

#FunctionHint
1eval_expr env exprRecursively evaluate: IntLit n → Const n, Var x → lookup x in env, BinOp → abstract_binop, Call → Top (unknown function)

Run tests

dune runtest modules/module4-abstract-interpretation/exercises/constant-propagation/