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]