-
Notifications
You must be signed in to change notification settings - Fork 24
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add alias property #171
Add alias property #171
Conversation
* - [[NoAlias]] can be assigned to a pair of entities, iff no execution path exists where both entities refer to the same memory location. | ||
* | ||
* - [[MustAlias]] can be assigned to a pair of entities, iff both entities refer to the same memory location in every execution time at all times. | ||
* This implies that at every use site of one entity, it can be replaced with the other entity (if it is defined at the current location) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like the description here, but maybe it should be expanded a little more to be absolutely clear about the meaning? You may also include a small code example if it helps.
* It indicates that the two entities might refer to the same memory location but are not obligated to do so. | ||
* This serves as a default/fallback value when no other property can be guaranteed. | ||
* | ||
* An analysis may only return [[MustAlias]] or [[NoAlias]] if it can guarantee that the property holds true under any circumstances. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is usually not possible to ensure. Instead, analyses should try to be as sound as possible and should document possible unsoundness where possible. Some cases of unsoundness might also be mentioned here already.
* }}} | ||
* In this example, the formal parameter `a` and the local variable `b` are guaranteed to never refer to the same memory location, | ||
* as `b` is always assigned to a new object that the formal parameter can't possibly be pointing to since the object has not been created before the method call. | ||
* This ensures that the method's return value and the formal parameter never point to the same memory location. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a very interesting case actually. I agree that during the method call, they can never alias and that's probably what a user would be interested in. But typically, these values will be abstractly combined over all (context-insensitive) or at least some (context-sensitive) calls, which I guess by definition could make them alias if the return value of one invocation can be passed as the parameter of another invocation of that method. What does the literature say about this?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Typically, aliasing is defined via the overlapping of the memory locations. Even if you look at it with all calls being combined, it still shouldn't be an alias, because they still point to distinct memory locations, despite being created at the same position (in code). You could of course view aliasing as a "created at the same location in code (same new instruction)" but I don't see how that would be helpful, because it doesn't really guarantee any useful properties.
But I think we should maybe use a more straight-forward example without parameters here to avoid any unnecessary confusion.
* }}} | ||
* In this example, the local variable `a` and `b` are guaranteed to refer to the same memory location at all times, | ||
* because a is only assigned once and b is only defined once with the value of a. | ||
* This means that the return value of the method can be replaced with `a`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
True, but wouldn't the above definition imply that one could also replace a with b? Now, there is only one use site of a, in line 44, and if there were more they would have to be after line 44 and thus replacable (use sites before line 44 should make the two variables clearly MayAlias), but replacing a with b in line 44 obviously can't work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, but the definition (regarding replacement) above states that it is only applicable if the other entity (b in this case) is defined at that location, which is not given for the right-hand side of line 44.
Add a basic foundation for future alias analysis by defining the used properties. The available properties are:
The actual analysis, including test cases, will be added in future pull requests.