Closed sim642 closed 2 years ago
If the annotations added are incorrect, there's no way this is going to be idempotent. So this seems another instance of that other issue with adding annotations. If both: 1 the annotations are added correctly, and 2 the result is not idempotent. Then it would be interesting to see a small repro example. Otherwise, this can be closed in favour of the other existing issue.
The case of #155 is the odd one out here. I think all the other cases were such that if an unused function was correctly annotated with dead
by reanalyze, then on the second run it finds some variable inside that function as being dead. Which of course it also is, but it would be very inconvenient to add dead
annotations to everything inside a dead
-annotated function.
There's some logic that if a function is reported dead, then the values inside it are not reported.
Technically, if the function is annotated @dead
then it is not reported, so the logic does not apply.
So this is indeed a violation of idempotency.
I thought this was done for a reason, but not sure might be bad memory.
As an aside, in interactive use, you would annotate the function as @live
, which does not give this problem.
I think I now remember that idempotency is tested by running a ppx which deletes the entire function when annotated dead, so that's the sense in which it is idempotent. The values inside won't be reported as they disappear.
So in this sense, the process makes sense if one proceeds by either:
@live
, orI think this process is reasonable, so I'd be inclined to consider this as a non-issue.
So I would say that the issue is about documenting what the intended process is, rather than the current behaviour.
From the readme:
The main difference between @dead and @live is the transitive behaviour: @dead values don't keep alive values they use, while @live values do.
If the intended process only involves using @live
or deleting code (so no annotation is necessary at all), then the @dead
annotation shouldn't be used at all (other than the output of -write
I suppose). But the README also clearly describes usage for @dead
:
@dead
suppresses reporting on the value/type, but can also be used to force the analysis to consider a value as dead. Typically used to acknowledge cases of dead code you are not planning to address right now, but can be searched easily later.
According to that, there is legitimate reason for keeping @dead
annotations around. Blindly changing them to @live
just to avoid the non-idempotency issue creates further semantic confusion as the use for @live
is described for FFI, etc reasons.
I understand the difference of the two annotations as to their transitive behavior, but there's a subtlety in the phrase "values they use". For example, in the snippet from above:
let print_to_file (fileName: string) (fileAST: file) =
let oc = Stdlib.open_out fileName [@@dead "+oc"] in
dumpFile defaultCilPrinter oc fileName fileAST [@@dead "+print_to_file"]
It's about a dead function print_to_file
containing something dead (oc
). But the inner definition is dead by virtue of the outer one, so the annotation on it is excessive. This is why I think the dead code analysis should consider the situation of containment specially/differently.
Of course the situation would be different if oc
was outside print_to_file
and in that case I agree with the @dead
vs @live
distinction regarding transitivity of usage.
Or if in such dead containment case it is really expected to use the @dead
annotation on both (or even more if there are more inner definitions), then the idempotent/consistent behavior would be for -write
to add annotations to both on the first run when neither has any annotation.
It's pretty tempting to remove the entire concept of @dead
annotation and just suggest to comment-out the code.
Except, one loses the fact that annotated code still compiles and does not code rot while refactoring. Plus, the ppx has been used as a form of automatic dead code elimination when vendoring libraries or other code.
for -write to add annotations to both on the first run when neither has any annotation.
That would be pretty noisy.
Looks like proper idempotency is the way to go. It's only a minor code complication where dead-annotated declarations are not filtered out early on, but survive until it's time to report things. And they won't be reported but be used to silence inner reports.
This should take care of it: https://github.com/rescript-association/reanalyze/pull/160 There's not really a test for it, as tests run under the ppx, but seems to work.
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following.
Going through the following steps:
dune build @check @all
to get cmt files.reanalyze.exe -write -dce-cmt _build/default/
prints:dune build @check @all
to get cmt files with written attributes.reanalyze.exe -write -dce-cmt _build/default/
prints:Even though the first analysis adds dead code attributes, the second analysis just keeps on adding more. For example:
oc
, despite it being contained inprint_to_file
, which has the attribute from the first run:Everything inside dead-attributed definitions should be assumed dead by default, without getting additional warnings.