mukul-rathi / bolt

Bolt is a language with in-built data-race freedom!
MIT License
546 stars 53 forks source link

Fully infer method capability annotations #140

Open mukul-rathi opened 4 years ago

mukul-rathi commented 4 years ago

Right now we annotate each method type-signature with capabilities used.

I think the method annotations could be inferred by constructing a method call graph for each class, and then generating constraints - if method M1 calls M2, then capabilities_used(M1) is a superset of capabilities_used(M2).

Then you solve the constraints to get the method annotations. There’s potentially a quadratic number of constraints (with respect to number of methods) but in theory doable. If we tried to infer parameter annotations as well, this call-graph based approach would most likely lead to far too many constraints and likely wouldn’t scale.