From d2f8028e77511e99b7315454da61ec95350259dc Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Tue, 21 Jul 2020 01:42:49 -0700 Subject: [PATCH] [preanalysis] Adding a preanalysis to resolve local closures Summary: This will allow all the analyses to be able to call closures without any special treatment: we transform the call to variables that point to closures into normal function calls. We treat only ObjC blocks at the moment, with C++ lambdas to be done as a next step. We aimed to achieve certain results in Pulse (see tests: avoid memory leaks and NPEs FPs) while also keeping the biabduction analysis working as before. We also checked that for the examples analyzed Pulse behaves like the correct semantics of ObjC programs with blocks. Reviewed By: jvillard Differential Revision: D22547333 fbshipit-source-id: efe56ed51 --- infer/src/backend/ClosuresSubstitution.ml | 122 ++++++++++++++++++ infer/src/backend/Devirtualizer.ml | 2 +- infer/src/backend/preanal.ml | 2 + .../codetoanalyze/objc/biabduction/issues.exp | 2 +- .../objc/performance/cost-issues.exp | 2 +- .../objc/pulse/MemoryLeaksInBlocks.m | 2 +- .../codetoanalyze/objc/pulse/NPEBlocks.m | 36 ++++++ .../tests/codetoanalyze/objc/pulse/issues.exp | 3 +- 8 files changed, 166 insertions(+), 5 deletions(-) create mode 100644 infer/src/backend/ClosuresSubstitution.ml create mode 100644 infer/tests/codetoanalyze/objc/pulse/NPEBlocks.m diff --git a/infer/src/backend/ClosuresSubstitution.ml b/infer/src/backend/ClosuresSubstitution.ml new file mode 100644 index 000000000..93da6e18a --- /dev/null +++ b/infer/src/backend/ClosuresSubstitution.ml @@ -0,0 +1,122 @@ +(* + * 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. + *) + +open! IStd +module L = Logging + +(** value domain, with the following concretization function [gamma]: + + {[ + gamma(VDom.top) = { any value } + gamma(VDom.v Closure) = { a closure } + gamma(VDom.bot) = emptyset + ]} *) +module ExpClosure = struct + type t = Exp.closure + + let pp fmt closure = Exp.pp fmt (Exp.Closure closure) + + let equal closure1 closure2 = Exp.equal (Exp.Closure closure1) (Exp.Closure closure2) +end + +module VDom = AbstractDomain.Flat (ExpClosure) +module CFG = ProcCfg.Normal +module Domain = AbstractDomain.Map (Var) (VDom) + +let get_var (astate : Domain.t) (v : Var.t) : VDom.t = + match Domain.find_opt v astate with Some ab -> ab | None -> VDom.bottom + + +let rec eval_expr (astate : Domain.t) (expr : Exp.t) : VDom.t = + match expr with + | Var id -> + get_var astate (Var.of_id id) + | Closure c when Exp.is_objc_block_closure expr -> + VDom.v c + | Closure _ (* TODO: implement for C++ lambdas *) -> + VDom.top + | Cast (_, e) -> + eval_expr astate e + | Lvar v -> + get_var astate (Var.of_pvar v) + | UnOp _ | BinOp _ | Exn _ | Const _ | Lfield _ | Lindex _ | Sizeof _ -> + VDom.top + + +let eval_instr (astate : Domain.t) (instr : Sil.instr) : Domain.t = + match instr with + | Load {id} when Ident.is_none id -> + astate + | Load {id; e} -> + let aval = eval_expr astate e in + Domain.add (Var.of_id id) aval astate + | Store {e1= Lvar pvar; e2} -> + let aval = eval_expr astate e2 in + Domain.add (Var.of_pvar pvar) aval astate + | Store _ | Prune _ | Metadata _ | Call _ -> + astate + + +module TransferFunctions = struct + module CFG = CFG + module Domain = Domain + + type analysis_data = unit + + let exec_instr astate _ _node instr = eval_instr astate instr + + let pp_session_name node fmt = + Format.fprintf fmt "Closures Substitution %a" CFG.Node.pp_id (CFG.Node.id node) +end + +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions) + +let get_invariant_at_node (map : Analyzer.invariant_map) node : Domain.t = + match Analyzer.InvariantMap.find_opt (Procdesc.Node.get_id node) map with + | Some abstate -> + abstate.pre + | None -> + Domain.bottom + + +let replace_instr node (astate : Domain.t) (instr : Sil.instr) : Sil.instr = + let kind = `ExecNode in + let pp_name fmt = Format.pp_print_string fmt "Closure Substitution" in + NodePrinter.with_session (CFG.Node.underlying_node node) ~kind ~pp_name ~f:(fun () -> + match instr with + | Call (ret_id_typ, Var id, actual_params, loc, call_flags) -> ( + L.d_printfln "call %a " (Sil.pp_instr Pp.text ~print_types:true) instr ; + let aval = eval_expr astate (Var id) in + match VDom.get aval with + | None -> + L.d_printfln "(no closure found)" ; + instr + | Some c -> + L.d_printfln "found closure %a for variable %a\n" Exp.pp (Exp.Closure c) Ident.pp id ; + let captured_values = + List.map ~f:(fun (id_exp, _, typ, _) -> (id_exp, typ)) c.captured_vars + in + let actual_params = actual_params @ captured_values in + let new_instr = + Sil.Call (ret_id_typ, Const (Cfun c.name), actual_params, loc, call_flags) + in + L.d_printfln "replaced by call %a " (Sil.pp_instr Pp.text ~print_types:true) new_instr ; + new_instr ) + | _ -> + instr ) + + +let process summary = + let pdesc = Summary.get_proc_desc summary in + let node_cfg = CFG.from_pdesc pdesc in + let map = Analyzer.exec_cfg node_cfg ~initial:Domain.empty () in + let update_context = eval_instr in + let context_at_node node = get_invariant_at_node map node in + let _has_changed : bool = + Procdesc.replace_instrs_using_context pdesc ~f:replace_instr ~update_context ~context_at_node + in + () diff --git a/infer/src/backend/Devirtualizer.ml b/infer/src/backend/Devirtualizer.ml index 89cee6fd3..5f8a929bf 100644 --- a/infer/src/backend/Devirtualizer.ml +++ b/infer/src/backend/Devirtualizer.ml @@ -8,7 +8,6 @@ open! IStd module L = Logging -module VDom = AbstractDomain.Flat (JavaClassName) (** value domain, with the following concretization function [gamma]: {[ @@ -16,6 +15,7 @@ module VDom = AbstractDomain.Flat (JavaClassName) gamma(VDom.v A) = { any ref of exact class A } gamma(VDom.bot) = emptyset ]} *) +module VDom = AbstractDomain.Flat (JavaClassName) module CFG = ProcCfg.Normal module Domain = AbstractDomain.Map (Var) (VDom) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 009d29c36..201a8b840 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -377,6 +377,8 @@ let do_preanalysis exe_env pdesc = if Procname.is_java proc_name then InlineJavaSyntheticMethods.process pdesc ; if Config.function_pointer_specialization && not (Procname.is_java proc_name) then FunctionPointerSubstitution.process pdesc ; + (* NOTE: It is important that this preanalysis stays before Liveness *) + if not (Procname.is_java proc_name) then ClosuresSubstitution.process summary ; Liveness.process summary tenv ; AddAbstractionInstructions.process pdesc ; if Procname.is_java proc_name then Devirtualizer.process summary tenv ; diff --git a/infer/tests/codetoanalyze/objc/biabduction/issues.exp b/infer/tests/codetoanalyze/objc/biabduction/issues.exp index 84396119c..1e89199b7 100644 --- a/infer/tests/codetoanalyze/objc/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/objc/biabduction/issues.exp @@ -17,7 +17,7 @@ codetoanalyze/objc/biabduction/warnings/ParameterNotNullableExample.m, FBAudioRe codetoanalyze/objc/biabduction/warnings/ParameterNotNullableExample.m, FBAudioRecorder.init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init] codetoanalyze/objc/biabduction/warnings/ParameterNotNullableExample.m, FBAudioRecorder.test, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure test,Message recordState with receiver nil returns nil.] codetoanalyze/objc/shared/block/BlockVar.m, BlockVar.blockPostBad, 5, NULL_DEREFERENCE, B5, ERROR, [start of procedure blockPostBad,start of procedure block,return from a call to objc_blockBlockVar.blockPostBad_2] -codetoanalyze/objc/shared/block/BlockVar.m, BlockVar.capturedNullDeref, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure capturedNullDeref,start of procedure block] +codetoanalyze/objc/shared/block/BlockVar.m, BlockVar.capturedNullDeref, 5, NULL_DEREFERENCE, B5, ERROR, [start of procedure capturedNullDeref,start of procedure block] codetoanalyze/objc/shared/block/BlockVar.m, BlockVar.navigateToURLInBackground, 8, NULL_DEREFERENCE, B1, ERROR, [start of procedure navigateToURLInBackground,start of procedure block,start of procedure test,return from a call to BlockVar.test,return from a call to objc_blockBlockVar.navigateToURLInBackground_1,Taking true branch] codetoanalyze/objc/shared/block/block.m, main1, 30, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure main1(),start of procedure block,start of procedure block,return from a call to objc_blockobjc_blockmain1_2_3,return from a call to objc_blockmain1_2,start of procedure block,return from a call to objc_blockmain1_1] codetoanalyze/objc/shared/block/block_no_args.m, Block_no_args.m, 10, NULL_DEREFERENCE, B1, ERROR, [start of procedure m,start of procedure block,return from a call to objc_blockBlock_no_args.m_1,Taking true branch] diff --git a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp index 0d5428687..785cfc91d 100644 --- a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp @@ -72,7 +72,7 @@ codetoanalyze/objc/performance/araii.m, Araii.dealloc, 4, OnUIThread:false, [] codetoanalyze/objc/performance/araii.m, Araii.initWithBuffer, 15, OnUIThread:false, [] codetoanalyze/objc/performance/araii.m, Araii.setBuffer:, 4, OnUIThread:false, [] codetoanalyze/objc/performance/araii.m, memory_leak_raii_main, 18, OnUIThread:false, [] -codetoanalyze/objc/performance/block.m, block_multiply_array_linear_FN, 6, OnUIThread:false, [] +codetoanalyze/objc/performance/block.m, block_multiply_array_linear_FN, 22, OnUIThread:false, [] codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_FN_1, 17, OnUIThread:false, [] codetoanalyze/objc/performance/break.m, break_constant_FP, 8 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), OnUIThread:false, [{1+max(0, p)},Call to break_loop,Loop,{p},Call to break_loop,Loop] codetoanalyze/objc/performance/break.m, break_loop, 5 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), OnUIThread:false, [{1+max(0, p)},Loop,{p},Loop] diff --git a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m index d16a23930..1bd6025bc 100644 --- a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m +++ b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m @@ -17,7 +17,7 @@ int block_captured_var_leak_bad() { return blk(); } -int block_free_ok_FP() { +int block_free_ok() { int* x = malloc(sizeof(int)); *x = 2; int (^blk)(void) = ^() { diff --git a/infer/tests/codetoanalyze/objc/pulse/NPEBlocks.m b/infer/tests/codetoanalyze/objc/pulse/NPEBlocks.m new file mode 100644 index 000000000..2027c00f3 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/NPEBlocks.m @@ -0,0 +1,36 @@ +/* + * 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. + */ + +#include + +@interface Singleton : NSObject + +@property int x; + +@end + +@implementation Singleton + +// Common FP in Pulse NPEs, this requires block specialization +- (int)dispatch_once_no_npe_good_FP { + static Singleton* a = nil; + static dispatch_once_t onceToken; + dispatch_once(&onceToken, ^{ + a = [[Singleton alloc] init]; + }); + return a->_x; +} + +@end + +int captured_npe_bad() { + int* x = NULL; + int (^my_block)(void) = ^() { + return *x; + }; + return my_block(); +} diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 49ec14266..76a36f945 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -7,6 +7,7 @@ codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 1, MEMOR codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 6, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_free_ok_FP, 8, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,when calling `objc_blockcaptured_npe_bad_2` here,parameter `x` of objc_blockcaptured_npe_bad_2,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest.use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]