| Issue 14: | Handling of virtual permissions in constructors | |
| 1 person starred this issue and may be notified of changes. | Back to list |
Constructors can make virtual method calls (a discouraged practice in Java). Plural supports virtual permissions on constructors to this end, but it doesn't currently verify that these permissions are, in fact, available. There's a simple approach here: Split the required virtual permission from the initial unique frame permission before analyzing the constructor body. That ensures that, _if_ we're looking at the runtime type, we're satisfying the pre-condition. That's basically what we do for methods: At a virtual method call site, we split required frame and virtual permissions from the available (virtual) permissions for the receiver. But this is conservative if we're actually *not* looking at the runtime type. (We could be a little better if we only do this for concrete classes.) Also, constructors typically wouldn't check: We can't split off a required permission, e.g., full, from a unique and return the full _and_ the unique. We can fix this by only ensuring a pure frame permission, instead of a unique. But that's unsatisfying: At a "new ..." we'll get a full and a pure virtual permission for the new object. We could use explicit fractions to heal this. But the actual problem is: we only have a pure frame permission for checking the constructor, which in general might not be sufficient. I think another, more tool-challenging option would be to check constructors (of concrete classes) twice, once assuming the current frame is the virtual frame and once assuming that is *not* the case. - When assuming the virtual frame, we just start with a unique (frame) permission and ignore any required virtual permissions (like @Full above). Whenever virtual permissions for "this" are needed (in super- or regular method calls) we split them from that unique frame permission. In other words, we equate frame and virtual permissions into one, which I think is safe since all dynamically dispatched calls end up in the frame we're analyzing (per our assumption). At new ... sites, we only use ensured frame permissions and convert them into virtual permissions for the newly constructed object, thus the example, we get a unique out. No fraction or other magic is needed. This also allows us to completely ignore ensured virtual permissions (like @Full above). We could skip this pass if we're looking at a abstract class - When assuming *not* the virtual frame, we start with required virtual permissions and a unique frame permission and check the method body as usual. In other words, the tool already performs this pass. We could skip this pass if we're looking at a final class.
Jul 23, 2009
Project Member
#1
nels.bec...@gmail.com
Jul 24, 2009
Yes, this is fixed, and we even have some test cases for this, I think...
Status:
Fixed
|