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.
git clone https://github.com/weihaoqu/program-analysis-bootcamp-studentfailwith "TODO" with your implementation.dune runtest modules/module4-abstract-interpretation/exercises/abstract-interpreterAbstract Interpreter
9. Exercise 5: Abstract Interpreter (Optional, 13 tests)
This exercise is optional. It builds a full abstract interpreter using OCaml functors. It's the most advanced exercise in this module. The lab covers similar ground with more guidance, so you can go directly to Lab 4 if you prefer.
Goal: Wire everything together — a generic interpreter parameterized by any
ABSTRACT_DOMAIN, with division-by-zero detection.
Time: ~25 minutes
Files to edit: exercises/abstract-interpreter/starter/abstract_interp.ml
Also provided: exercises/abstract-interpreter/starter/sample_analysis.ml
(test programs you can read to understand what the tests do)
Architecture
module Make (D : ABSTRACT_DOMAIN) = struct
module Env = MakeEnv(D)
val eval_expr : Env.t -> expr -> D.t
val transfer_stmt : Env.t -> stmt -> Env.t
val analyze_function : func_def -> Env.t
val check_div_by_zero : func_def -> (string * string) list
end
The file provides three built-in domains (SignDomain, ConstDomain,
IntervalDomain) so the tests can instantiate the functor with different
domains.
What to implement
| # | Function | Hint |
|---|---|---|
| 1 | eval_expr env expr | Pattern match on expr: IntLit n → D.alpha_int n (or your domain's abstraction), Var x → Env.lookup x env, BinOp → abstract_op, Call → D.top |
| 2 | transfer_stmt env stmt | Assign(x, e) → Env.update x (eval_expr env e) env; If → join both branches; While → fixpoint with widening |
| 3 | transfer_stmts env stmts | Fold transfer_stmt over the list |
| 4 | analyze_function func | Initialize params to D.top, transfer the body |
| 5 | check_div_by_zero func | Walk expressions, find BinOp(Div, _, denom) where denom could be zero |
The while loop fixpoint (hardest part)
1. Start with current env
2. Transfer the loop body to get env'
3. Widen: env'' = Env.widen env env'
4. If env'' = env (stable), stop — return env
5. Otherwise, repeat from step 2 with env''
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/abstract-interpreter/
Starter Files
Test Files
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.
git clone https://github.com/weihaoqu/program-analysis-bootcamp-studentfailwith "TODO" with your implementation.dune runtest modules/module4-abstract-interpretation/exercises/abstract-interpreterAbstract Interpreter
9. Exercise 5: Abstract Interpreter (Optional, 13 tests)
This exercise is optional. It builds a full abstract interpreter using OCaml functors. It's the most advanced exercise in this module. The lab covers similar ground with more guidance, so you can go directly to Lab 4 if you prefer.
Goal: Wire everything together — a generic interpreter parameterized by any
ABSTRACT_DOMAIN, with division-by-zero detection.
Time: ~25 minutes
Files to edit: exercises/abstract-interpreter/starter/abstract_interp.ml
Also provided: exercises/abstract-interpreter/starter/sample_analysis.ml
(test programs you can read to understand what the tests do)
Architecture
module Make (D : ABSTRACT_DOMAIN) = struct
module Env = MakeEnv(D)
val eval_expr : Env.t -> expr -> D.t
val transfer_stmt : Env.t -> stmt -> Env.t
val analyze_function : func_def -> Env.t
val check_div_by_zero : func_def -> (string * string) list
end
The file provides three built-in domains (SignDomain, ConstDomain,
IntervalDomain) so the tests can instantiate the functor with different
domains.
What to implement
| # | Function | Hint |
|---|---|---|
| 1 | eval_expr env expr | Pattern match on expr: IntLit n → D.alpha_int n (or your domain's abstraction), Var x → Env.lookup x env, BinOp → abstract_op, Call → D.top |
| 2 | transfer_stmt env stmt | Assign(x, e) → Env.update x (eval_expr env e) env; If → join both branches; While → fixpoint with widening |
| 3 | transfer_stmts env stmts | Fold transfer_stmt over the list |
| 4 | analyze_function func | Initialize params to D.top, transfer the body |
| 5 | check_div_by_zero func | Walk expressions, find BinOp(Div, _, denom) where denom could be zero |
The while loop fixpoint (hardest part)
1. Start with current env
2. Transfer the loop body to get env'
3. Widen: env'' = Env.widen env env'
4. If env'' = env (stable), stop — return env
5. Otherwise, repeat from step 2 with env''
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/abstract-interpreter/