Move extern inits, global inits and otherfuns spawning into constraint system
Nobody has claimed this yet.
- Dominant language
- OCaml
- Stars
- 252
- Forks
- 90
- Avg merge
- 4d 1m
- Merged PRs (30d)
- 19
Description
Currently extern inits, global inits and otherfuns spawning is done by manually simulating transfer function calls with degenerate ctx:
https://github.com/goblint/analyzer/blob/20f3a7d6285a35c7c7d5c2f6206e280a73b83c25/src/framework/control.ml#L175-L349
In my experience, time and time again, this has been causing issues because:
1.ctxs are degenerate – some outright crash, others have behavior which doesn't match the one available during solving;
2. it somewhat duplicates what FromSpec does;
3. it misses some nontrivial things that would happen during actual solving – e.g. main is unaware of otherfuns having been spawned at all;
4. it's extremely error prone and hard to maintain.
The sensible thing would be to do all these things within the constraint system and let the solver evaluate them.
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 with src/framework/control.ml, especially the linked lines 175-349, to understand the current manual spawning and degenerate ctx handling. Trace how the constraint system and solver are involved; done means extern inits, global inits, and otherfuns spawning are handled within the constraint system rather than by the current manual simulation.
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
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100