Skip to content
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 manual section on RLC inference #6340

Merged
merged 16 commits into from
Jan 28, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions docs/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@ Method, constructor, lambda, and method reference type inference has been
greatly improved. The `-AconservativeUninferredTypeArguments` option is
no longer necessary and has been removed.

A specialized inference algorithm for the Resource Leak Checker runs
automatically as part of whole-program inference.

**Implementation details:**

**Closed issues:**
Expand Down
17 changes: 7 additions & 10 deletions docs/manual/resource-leak-checker.tex
Original file line number Diff line number Diff line change
Expand Up @@ -632,16 +632,13 @@
then verify the code using a method other than the Resource Leak Checker.


%% TODO: Uncomment when the feature is ready to be publicized.
% \sectionAndLabel{Resource Leak Checker Annotation Inference Algorithm}{resource-leak-checker-inference-algo}
%
% We are developing a special inference mechanism to infer annotations for
% the Resource Leak Checker. By default, this mechanism operates when the
% -Ainfer flag is enabled. To utilize the whole-program inference mechanism outlined in
% section \ref{whole-program-inference} in addition to this mechanism for the Resource
% Leak Checker and its sub-checkers, you should provide the \<-AenableWpiForRlc> flag.
%
% The paper \href={https://arxiv.org/pdf/2306.11953.pdf}{Automatic Inference of Resource Leak Specifications}, published at OOPSLA 2023, gives more details on the inference algorithm. Currently, only the first phase of the algorithm described in the paper is available, and the complete implementation will be available soon.
\sectionAndLabel{Resource Leak Checker annotation inference algorithm}{resource-leak-checker-inference-algo}

The Resource Leak Checker uses a specialized algorithm to infer annotations
when whole program inference (WPI, Section~\ref{whole-program-inference})
is enabled. The algorithm is described in the paper ``Inference of
Resource Management Specifications''~\cite{ShadabGTEKLLS2023} (OOPSLA 2023,
\myurl{https://homes.cs.washington.edu/~mernst/pubs/resource-inference-oopsla2023-abstract.html}).


% LocalWords: de subchecker OutputStream MustCall MustCallUnknown RAII Un
Expand Down