Open Calvin-L opened 12 months ago
Did some investigation on this one, and it looks like at least one issue is we do not have handling of postconditions when they impact temporary variables. We have special handling here for when a method is directly invoked on an expression that has a temporary variable:
We need to extend this logic to handle the case where a postcondition (via @EnsuresCalledMethods
) impacts a temp var. The built-in logic for handling post-conditions is around here:
@kelloggm do you think there's a way we could easily extend this logic with some method overrides? Otherwise we may need to do some copy-pasting.
If we have a ResourceLeakStore
or create one, we might be able to override CFAbstractStore#insertOrRefine
(which the postcondition code calls indirectly) so that it checks for temporary variables and also applies the insert/refine operation to those. As a bonus, that might also let us get rid of that special case you mentioned in ResourceLeakTransfer
.
The problem is going to be finding the appropriate tempvar. insertOrRefine
takes a JavaExpression
, but MustCallAnnotatedTypeFactory#getTempVar
operates on CFG Node
s. Going from Node
-> JavaExpression
is doable, but I don't think it's easy to go the other way (it may not be possible, but I'd need to do some more in-depth investigation).
Copy-pasting code from CFAbstractTransfer
is ugly, but it would definitely be easier. Another option would be write a new overridable method in CFAbstractTransfer
that allows subclasses to specify a set of nodes that a postcondition should also apply to (default: none).
With some more investigation, I'm not sure that our current implementation can handle this case without either a major refactoring, a new CFG API, or both. In particular, the core problem is the way that we track temporary variables.
Temporary variables are stored by the MustCallAnnotatedTypeFactory
in an IdentityHashMap
that is keyed on Tree
s. This means that to get a temporary variable, we need the associated Tree
object (which is the Tree
representing the expression). It is not possible (in our current implementation) to get a temporary variable for a given expression unless you can access either a Tree
or Node
that represents that expression: we don't keep any other kind of identifying information.
Even if we copy code from CFAbstractTransfer
, under the hood it is using JavaExpression
as the key into the store (i.e., the store is conceptually a map from JavaExpression
s to annotations/types). Effectively, it:
JavaExpression
. For example, this converts "#1"
to a JavaExpression
for "foo", if "foo" is the name of the parameterJavaExpression
in the storeAs far as I know (@smillst can confirm), there is no way to retrieve a Node
or Tree
associated with a JavaExpression
: JavaExpression
s are context-free. If it was possible, we'd need some kind of lookup (maybe via the CFG?), and it would necessarily need some kind of search logic - probably something conceptually similar to what we have in StringToJavaExpression
, but using the information in the target JavaExpression
+ some context to find a Tree
or Node
that matches.
In other words, we need to either:
JavaExpression
+ a context (e.g., in the form of a Node
) and returns the Node
from which the JavaExpression
must have been constructed. This would enable us to contemplate making the necessary changes to CFAbstractTransfer
to support this use case.JavaExpression
and a context. I'm not even sure how to begin to approach that problem (need to think a little more), but I don't think the solution is that different than building an RLC-specific version of the previous approach.Thanks for digging into this @kelloggm. One question:
converts and viewpoint adapts the argument to the postcondition annotation to get a JavaExpression. For example, this converts "#1" to a JavaExpression for "foo", if "foo" is the name of the parameter
At this step the logic must have a handle on the Tree
or Node
for the method invocation, correct? Is there hope of doing something like making a copy of this viewpoint adaptation logic to just give back the relevant actual parameter, rather than a JavaExpression
?
At this step the logic must have a handle on the Tree or Node for the method invocation, correct? Is there hope of doing something like making a copy of this viewpoint adaptation logic to just give back the relevant actual parameter, rather than a JavaExpression?
Yes, that's what the logic in StringToJavaExpression
that I alluded to does: it takes as input some kind of context (the MethodInvocationNode
whose postcondition is being processed) and then does something similar but not quite the same as what we need. I don't know this code very well, but I imagine we could write a similar kind of API that returns a Node
: that's what I'm suggesting in my first suggestion (1) at the end of my previous comment.
I guess what I don't understand from suggestion (1) is why it would take a JavaExpression
as an input? Shouldn't it take the same inputs as the viewpoint adaptation code, i.e., the "context" Node
and the post-condition annotation like "#1"
?
Sorry to come back to this much later.
I guess what I don't understand from suggestion (1) is why it would take a JavaExpression as an input? Shouldn't it take the same inputs as the viewpoint adaptation code, i.e., the "context" Node and the post-condition annotation like "#1"?
It could, but then we'd need to viewpoint adapt the "#1"
anyway to figure out what it refers to (which will give us a JavaExpression
), and we know that we'll already have the relevant JavaExpression
in hand. I think this is an implementation detail, though, and we'd have to implement it to see what works best.
The Resource Leak Checker does not accept this code:
this very similar code works:
However, that refactoring is not possible when
method
is a constructorclose
is a call tosuper(...)
orthis(...)
For example:
Below is a more complete set of tests that exercise a few variants of that pattern. The RLC reports false positives for test cases 3-7.