@ -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 = uni t
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_d ata. pd esc) in
let last_loc = Procdesc . Node . get_loc ( Procdesc . get_exit_node proc_d esc) 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 )