Allow analyses to not have their own bottom element but rely on Deadcode for that
Nobody has claimed this yet.
- Dominant language
- OCaml
- Stars
- 252
- Forks
- 90
- Avg merge
- 4d 1m
- Merged PRs (30d)
- 19
Description
For #1977, we would have liked for threadJoins to not have its own bottom element, as all threads being must-joined is equivalent to unreachability, which should be represented by the bottom element of the DeadcodeLifter.
However, MCP explicitly creates S.D.bot () abstract elements when an analysis does raise Deadcode, which means any analysis that raises deadcode has to have it's own bottom element.
Getting rid of this would allow us to do some more simplications to the domain of the locals in threadJoins and potentially elsewhere.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start at src/analyses/mCP.ml around lines 110-114 and trace how raising Deadcode creates S.D.bot () abstract elements. Compare that behavior with DeadcodeLifter and the threadJoins domain. Done means analyses can rely on Deadcode's bottom element without requiring their own bottom element, while preserving the intended unreachability representation.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- ocaml
- Domain
- devtools
- Issue type
- Refactor
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100