mukul-rathi / bolt

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

Check function/method call boundaries #98

Closed mukul-rathi closed 4 years ago

mukul-rathi commented 4 years ago

Check linearity / borrowing preserved across function / method call boundaries

If the param/return type requires linearity, then we need to check if argument / returned value is consumed or borrowed.

Additionally, for linear arguments, we need to make sure that they're not passed in multiple args or if we're calling a linear object method, that it is not passed as an argument.

  class Foo {
      region linear Bar;
      var int f : Bar;

     void test(Foo y){
     }
 }
function void test2(Foo x, Foo y){
}
void main() {
   let x = new Foo ();
   x.test(x); // not allowed!
   test2(x,x) // not allowed!
}

As you can see, these cause linearity to be violated.

mukul-rathi commented 4 years ago

Also look at args regions required - if we have a function access, then assume that all the regions needed for a variable access, unless params constrain region accesses.

When we return from a function, assume we need all capabilities / regions

mukul-rathi commented 4 years ago

Check if returned argument is linear() - if so make sure that unless we have consumed it, that the return type is "borrowed". If non-linear no need to do these checks