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/sign-latticeSign Lattice
5. Exercise 1: Sign Lattice (20 tests)
Goal: Implement the 5-element sign domain and abstract arithmetic.
Time: ~20 minutes
File to edit: exercises/sign-lattice/starter/sign_domain.ml
The sign lattice
Top "could be anything"
/ | \
Neg Zero Pos "definitely negative / zero / positive"
\ | /
Bot "unreachable"
What to implement (in order)
| # | Function | Hint |
|---|---|---|
| 1 | bottom | Return Bot |
| 2 | top | Return Top |
| 3 | join a b | Least upper bound — if a = b return it, otherwise Top (handle Bot/Top first) |
| 4 | meet a b | Greatest lower bound — dual of join |
| 5 | leq a b | a ⊑ b means join a b = b (or: Bot ⊑ everything, everything ⊑ Top) |
| 6 | equal a b | Structural equality |
| 7 | widen a b | For finite domains, widen = join |
| 8 | to_string | "Bot", "Neg", "Zero", "Pos", "Top" |
| 9 | alpha_int n | n > 0 → Pos, n = 0 → Zero, n < 0 → Neg |
| 10–14 | abstract_neg, abstract_add, abstract_sub, abstract_mul, abstract_div | See the arithmetic tables in the slides |
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/sign-lattice/
Hint for arithmetic: Handle Bot first (anything with Bot returns Bot),
then Top cases, then the 9 concrete combinations (Neg/Zero/Pos × Neg/Zero/Pos).
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/sign-latticeSign Lattice
5. Exercise 1: Sign Lattice (20 tests)
Goal: Implement the 5-element sign domain and abstract arithmetic.
Time: ~20 minutes
File to edit: exercises/sign-lattice/starter/sign_domain.ml
The sign lattice
Top "could be anything"
/ | \
Neg Zero Pos "definitely negative / zero / positive"
\ | /
Bot "unreachable"
What to implement (in order)
| # | Function | Hint |
|---|---|---|
| 1 | bottom | Return Bot |
| 2 | top | Return Top |
| 3 | join a b | Least upper bound — if a = b return it, otherwise Top (handle Bot/Top first) |
| 4 | meet a b | Greatest lower bound — dual of join |
| 5 | leq a b | a ⊑ b means join a b = b (or: Bot ⊑ everything, everything ⊑ Top) |
| 6 | equal a b | Structural equality |
| 7 | widen a b | For finite domains, widen = join |
| 8 | to_string | "Bot", "Neg", "Zero", "Pos", "Top" |
| 9 | alpha_int n | n > 0 → Pos, n = 0 → Zero, n < 0 → Neg |
| 10–14 | abstract_neg, abstract_add, abstract_sub, abstract_mul, abstract_div | See the arithmetic tables in the slides |
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/sign-lattice/
Hint for arithmetic: Handle Bot first (anything with Bot returns Bot),
then Top cases, then the 9 concrete combinations (Neg/Zero/Pos × Neg/Zero/Pos).