From 244384f605d6315b46ad2c9de3c3063b12f2d68a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 26 May 2020 03:46:52 -0700 Subject: [PATCH] [labs] brush up labs Summary: - fix compilation errors due to bitrot - ensure they don't happen again by adding dune files - make a quick pass through the README Reviewed By: skcho Differential Revision: D21684760 fbshipit-source-id: c541f9376 --- infer/src/IR/AccessPath.ml | 27 +++++++++++ infer/src/IR/AccessPath.mli | 6 +++ .../labs/00_dummy_checker/ResourceLeaks.ml | 43 ++++++++--------- .../labs/00_dummy_checker/ResourceLeaks.mli | 3 +- infer/src/labs/00_dummy_checker/dune | 13 +++++ .../labs/01_integer_domain/ResourceLeaks.ml | 42 +++++++---------- .../labs/01_integer_domain/ResourceLeaks.mli | 3 +- infer/src/labs/01_integer_domain/dune | 13 +++++ .../src/labs/02_domain_join/ResourceLeaks.ml | 42 +++++++---------- .../src/labs/02_domain_join/ResourceLeaks.mli | 3 +- infer/src/labs/02_domain_join/dune | 13 +++++ infer/src/labs/03_domain_top/ResourceLeaks.ml | 42 +++++++---------- .../src/labs/03_domain_top/ResourceLeaks.mli | 3 +- infer/src/labs/03_domain_top/dune | 13 +++++ .../labs/04_interprocedural/ResourceLeaks.ml | 47 +++++++------------ .../labs/04_interprocedural/ResourceLeaks.mli | 3 +- infer/src/labs/04_interprocedural/dune | 13 +++++ .../ResourceLeakDomain.ml | 6 ++- .../ResourceLeakDomain.mli | 4 +- .../ResourceLeaks.ml | 44 +++++++---------- .../ResourceLeaks.mli | 3 +- .../labs/05_access_paths_interprocedural/dune | 13 +++++ infer/src/labs/README.md | 2 + infer/src/labs/ResourceLeaks.mli | 3 +- 24 files changed, 236 insertions(+), 168 deletions(-) create mode 100644 infer/src/labs/00_dummy_checker/dune create mode 100644 infer/src/labs/01_integer_domain/dune create mode 100644 infer/src/labs/02_domain_join/dune create mode 100644 infer/src/labs/03_domain_top/dune create mode 100644 infer/src/labs/04_interprocedural/dune create mode 100644 infer/src/labs/05_access_paths_interprocedural/dune diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml index db10b88fa..db877d756 100644 --- a/infer/src/IR/AccessPath.ml +++ b/infer/src/IR/AccessPath.ml @@ -118,6 +118,33 @@ module Raw = struct let append (base, old_accesses) new_accesses = (base, old_accesses @ new_accesses) + + let rec chop_prefix_path ~prefix:path1 path2 = + if phys_equal path1 path2 then Some [] + else + match (path1, path2) with + | [], remaining -> + Some remaining + | _, [] -> + None + | access1 :: prefix, access2 :: rest when equal_access access1 access2 -> + chop_prefix_path ~prefix rest + | _ -> + None + + + let chop_prefix ~prefix:((base1, path1) as ap1) ((base2, path2) as ap2) = + if phys_equal ap1 ap2 then Some [] + else if equal_base base1 base2 then chop_prefix_path ~prefix:path1 path2 + else None + + + let replace_prefix ~prefix ~replace_with access_path = + match chop_prefix ~prefix access_path with + | Some remaining_accesses -> + Some (append replace_with remaining_accesses) + | None -> + None end module Abs = struct diff --git a/infer/src/IR/AccessPath.mli b/infer/src/IR/AccessPath.mli index f4ee5e8a4..495d8aba2 100644 --- a/infer/src/IR/AccessPath.mli +++ b/infer/src/IR/AccessPath.mli @@ -40,6 +40,9 @@ val append : t -> access list -> t (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) +(* used in infer/src/labs/ *) +val replace_prefix : prefix:t -> replace_with:t -> t -> t option [@@warning "-32"] + val equal_base : base -> base -> bool val pp : Format.formatter -> t -> unit @@ -48,6 +51,9 @@ val pp_base : Format.formatter -> base -> unit val pp_access : Format.formatter -> access -> unit +(* used in infer/src/labs/ *) +val pp_access_list : Format.formatter -> access list -> unit [@@warning "-32"] + module Abs : sig type raw = t diff --git a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml index 6faced69e..4494bc443 100644 --- a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml +++ b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,8 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc= _; tenv= _} _ (instr : HilInstr.t) - = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ + (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct _callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) @@ -67,7 +61,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -82,16 +76,17 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak _post _summary (_proc_data : unit ProcData.t) = () - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} post = + let change_me = false in + if change_me then + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in + let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message + + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/00_dummy_checker/ResourceLeaks.mli b/infer/src/labs/00_dummy_checker/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/00_dummy_checker/ResourceLeaks.mli +++ b/infer/src/labs/00_dummy_checker/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/00_dummy_checker/dune b/infer/src/labs/00_dummy_checker/dune new file mode 100644 index 000000000..66e213c54 --- /dev/null +++ b/infer/src/labs/00_dummy_checker/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs00) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/01_integer_domain/ResourceLeaks.ml b/infer/src/labs/01_integer_domain/ResourceLeaks.ml index 1ebcdafd6..cbe120f2c 100644 --- a/infer/src/labs/01_integer_domain/ResourceLeaks.ml +++ b/infer/src/labs/01_integer_domain/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc= _; tenv} _ (instr : HilInstr.t) = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) + = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) @@ -69,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -84,21 +79,16 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak post summary (proc_data : unit ProcData.t) = +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} post = if ResourceLeakDomain.has_leak post then - let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.lab_resource_leak message - - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message + + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/01_integer_domain/ResourceLeaks.mli b/infer/src/labs/01_integer_domain/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/01_integer_domain/ResourceLeaks.mli +++ b/infer/src/labs/01_integer_domain/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/01_integer_domain/dune b/infer/src/labs/01_integer_domain/dune new file mode 100644 index 000000000..5cab37515 --- /dev/null +++ b/infer/src/labs/01_integer_domain/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs01) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/02_domain_join/ResourceLeaks.ml b/infer/src/labs/02_domain_join/ResourceLeaks.ml index 1ebcdafd6..cbe120f2c 100644 --- a/infer/src/labs/02_domain_join/ResourceLeaks.ml +++ b/infer/src/labs/02_domain_join/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc= _; tenv} _ (instr : HilInstr.t) = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) + = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) @@ -69,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -84,21 +79,16 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak post summary (proc_data : unit ProcData.t) = +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} post = if ResourceLeakDomain.has_leak post then - let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.lab_resource_leak message - - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message + + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/02_domain_join/ResourceLeaks.mli b/infer/src/labs/02_domain_join/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/02_domain_join/ResourceLeaks.mli +++ b/infer/src/labs/02_domain_join/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/02_domain_join/dune b/infer/src/labs/02_domain_join/dune new file mode 100644 index 000000000..79b3a35ca --- /dev/null +++ b/infer/src/labs/02_domain_join/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs02) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/03_domain_top/ResourceLeaks.ml b/infer/src/labs/03_domain_top/ResourceLeaks.ml index 1ebcdafd6..cbe120f2c 100644 --- a/infer/src/labs/03_domain_top/ResourceLeaks.ml +++ b/infer/src/labs/03_domain_top/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc= _; tenv} _ (instr : HilInstr.t) = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) + = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) @@ -69,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -84,21 +79,16 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak post summary (proc_data : unit ProcData.t) = +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} post = if ResourceLeakDomain.has_leak post then - let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.lab_resource_leak message - - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message + + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/03_domain_top/ResourceLeaks.mli b/infer/src/labs/03_domain_top/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/03_domain_top/ResourceLeaks.mli +++ b/infer/src/labs/03_domain_top/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/03_domain_top/dune b/infer/src/labs/03_domain_top/dune new file mode 100644 index 000000000..00ca51a45 --- /dev/null +++ b/infer/src/labs/03_domain_top/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs03) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/04_interprocedural/ResourceLeaks.ml b/infer/src/labs/04_interprocedural/ResourceLeaks.ml index c1a741769..d84c459c2 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/04_interprocedural/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> ( if @@ -62,10 +56,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else if releases_resource tenv callee_procname then ResourceLeakDomain.release_resource astate else - match Payload.read pdesc callee_procname with - | Some summary -> + match analyze_dependency callee_procname with + | Some (_callee_proc_desc, callee_summary) -> (* interprocedural analysis produced a summary: use it *) - ResourceLeakDomain.apply_summary ~summary astate + ResourceLeakDomain.apply_summary ~summary:callee_summary astate | None -> (* No summary for [callee_procname]; it's native code or missing for some reason *) astate ) @@ -83,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -98,21 +92,16 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak post summary (proc_data : unit ProcData.t) = +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} post = if ResourceLeakDomain.has_leak post then - let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.lab_resource_leak message - - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message + + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/04_interprocedural/ResourceLeaks.mli b/infer/src/labs/04_interprocedural/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeaks.mli +++ b/infer/src/labs/04_interprocedural/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/04_interprocedural/dune b/infer/src/labs/04_interprocedural/dune new file mode 100644 index 000000000..9d3cd4421 --- /dev/null +++ b/infer/src/labs/04_interprocedural/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs04) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml index a2a6dd680..ad806f0bc 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml @@ -63,7 +63,9 @@ let release_resource access_path held = let assign lhs_access_path rhs_access_path held = let one_binding access_path count held = - match AccessPath.replace_prefix ~prefix:rhs_access_path lhs_access_path access_path with + match + AccessPath.replace_prefix ~prefix:rhs_access_path ~replace_with:access_path lhs_access_path + with | Some base_access_path -> ResourcesHeld.add base_access_path count held | None -> @@ -141,7 +143,7 @@ module Summary = struct held ResourcesFromFormals.empty - let apply ~summary ~return ~actuals held = + let apply ~callee:summary ~return ~actuals held = let apply_one (base, accesses) callee_count held = let access_path_opt = match (base : InterfaceAccessPath.base) with diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.mli b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.mli index 78e771a9b..7ff9904bb 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.mli +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.mli @@ -22,9 +22,11 @@ val has_leak : FormalMap.t -> t -> bool type summary module Summary : sig - val apply : summary:summary -> return:AccessPath.base -> actuals:HilExp.t list -> t -> t + val apply : callee:summary -> return:AccessPath.base -> actuals:HilExp.t list -> t -> t val make : FormalMap.t -> t -> summary val pp : Format.formatter -> summary -> unit + + type t = summary end diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml index d2750f9e0..96a355553 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.summary - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = ResourceLeakDomain.Summary.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) = + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ (instr : HilInstr.t) = match instr with | Call (_return, Direct callee_procname, HilExp.AccessExpression allocated :: _, _, _loc) when acquires_resource tenv callee_procname -> @@ -69,10 +63,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> astate ) | Call (return, Direct callee_procname, actuals, _, _loc) -> ( - match Payload.read pdesc callee_procname with - | Some summary -> + match analyze_dependency callee_procname with + | Some (_callee_proc_desc, callee_summary) -> (* interprocedural analysis produced a summary: use it *) - ResourceLeakDomain.Summary.apply ~summary ~return ~actuals astate + ResourceLeakDomain.Summary.apply ~callee:callee_summary ~return ~actuals astate | None -> (* No summary for [callee_procname]; it's native code or missing for some reason *) astate ) @@ -90,7 +84,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr - | ExitScope _ -> + | Metadata _ -> astate @@ -105,22 +99,18 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak post summary formal_map (proc_data : unit ProcData.t) = +let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} formal_map post = if ResourceLeakDomain.has_leak formal_map post then - let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in + let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_desc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.lab_resource_leak message + Reporting.log_error proc_desc err_log ~loc:last_loc ResourceLeakLabExercise + IssueType.lab_resource_leak message -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = - let proc_data = ProcData.make proc_desc tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with - | Some post -> +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.map result ~f:(fun post -> let formal_map = FormalMap.make proc_desc in - report_if_leak post summary formal_map proc_data ; - Payload.update_summary (ResourceLeakDomain.Summary.make formal_map post) summary - | None -> - L.(die InternalError) - "Analyzer failed to compute post for %a" Procname.pp - (Procdesc.get_proc_name proc_data.pdesc) + report_if_leak analysis_data formal_map post ; + ResourceLeakDomain.Summary.make formal_map post ) diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.mli b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.mli index 489676eb8..bffb4e479 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.mli +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option diff --git a/infer/src/labs/05_access_paths_interprocedural/dune b/infer/src/labs/05_access_paths_interprocedural/dune new file mode 100644 index 000000000..94ced83d2 --- /dev/null +++ b/infer/src/labs/05_access_paths_interprocedural/dune @@ -0,0 +1,13 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name Labs05) + (flags + (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated + -open IBase -open Absint)) + (libraries core IStdlib ATDGenerated IBase IR Absint) + (preprocess (pps ppx_compare)) +) diff --git a/infer/src/labs/README.md b/infer/src/labs/README.md index 59a5d0c50..11031224e 100644 --- a/infer/src/labs/README.md +++ b/infer/src/labs/README.md @@ -4,6 +4,8 @@ This is a lab exercise designed to take the participant through the basics of us The files to work on are [ResourceLeaks.ml](./ResourceLeaks.ml) and [ResourceLeakDomain.ml](./ResourceLeakDomain.ml), and their corresponding .mli files. +The solutions to the exercises can also be found in this directory, each in their own directory. For example, the solution for Section 2 of this lab can be found in [02_domain_join/](./02_domain_join/). + ## (0) Quick Start ### (a) With Docker... diff --git a/infer/src/labs/ResourceLeaks.mli b/infer/src/labs/ResourceLeaks.mli index f1f7daeaf..bffb4e479 100644 --- a/infer/src/labs/ResourceLeaks.mli +++ b/infer/src/labs/ResourceLeaks.mli @@ -7,4 +7,5 @@ open! IStd -val checker : ResourceLeakDomain.t InterproceduralAnalysis.t -> ResourceLeakDomain.t option +val checker : + ResourceLeakDomain.summary InterproceduralAnalysis.t -> ResourceLeakDomain.summary option