diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index b34dfba85..d78456db0 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -302,23 +302,29 @@ end let mk_initial proc_desc = (* HACK: save the formals in the stacks of the pre and the post to remember which local variables correspond to formals *) - let formals = + let formals_and_captured = let proc_name = Procdesc.get_proc_name proc_desc in let location = Procdesc.get_loc proc_desc in - Procdesc.get_formals proc_desc - |> List.map ~f:(fun (mangled, _) -> - let pvar = Pvar.mk mangled proc_name in - ( Var.of_pvar pvar - , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) ) + let init_var mangled = + let pvar = Pvar.mk mangled proc_name in + (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)])) + in + let formals = + Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, _) -> init_var mangled) + in + let captured = + Procdesc.get_captured proc_desc |> List.map ~f:(fun (mangled, _, _) -> init_var mangled) + in + captured @ formals in let initial_stack = - List.fold formals ~init:(PreDomain.empty :> BaseDomain.t).stack + List.fold formals_and_captured ~init:(PreDomain.empty :> BaseDomain.t).stack ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack) in let pre = let initial_heap = - List.fold formals ~init:(PreDomain.empty :> base_domain).heap ~f:(fun heap (_, (addr, _)) -> - BaseMemory.register_address addr heap ) + List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).heap + ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap) in PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty in diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index b211dc2b7..26178cc62 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -167,6 +167,15 @@ let is_cell_read_only ~edges_pre_opt ~cell_post:(_, attrs_post) = match edges_pre_opt with None -> false | Some _ -> not (Attributes.is_modified attrs_post) +let materialize_pre_for_captured_vars callee_proc_name call_location pre_post + ~captured_vars_with_actuals call_state = + List.fold_result captured_vars_with_actuals ~init:call_state + ~f:(fun call_state (formal, actual) -> + materialize_pre_from_actual callee_proc_name call_location + ~pre:(pre_post.AbductiveDomain.pre :> BaseDomain.t) + ~formal ~actual call_state ) + + let materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state = (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then @@ -245,13 +254,16 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st call_state.subst call_state -let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = +let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals + ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; let r = let open IResult.Let_syntax in (* first make as large a mapping as we can between callee values and caller values... *) materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state + >>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post + ~captured_vars_with_actuals >>= materialize_pre_for_globals callee_proc_name call_location pre_post >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in terms of the caller's values *) @@ -417,6 +429,12 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~ call_state +let apply_post_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals + call_state = + List.fold captured_vars_with_actuals ~init:call_state ~f:(fun call_state (formal, actual) -> + record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state ) + + let apply_post_for_globals callee_proc_name call_location pre_post call_state = match fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack @@ -457,10 +475,13 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state = {call_state with astate} -let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = +let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals + call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state + |> apply_post_for_captured_vars callee_proc_name call_location pre_post + ~captured_vars_with_actuals |> apply_post_for_globals callee_proc_name call_location pre_post |> record_post_for_return callee_proc_name call_location pre_post |> fun (call_state, return_caller) -> @@ -514,7 +535,8 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call the noise that this will introduce since we don't care about values. For instance, if the pre is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is to bake in some value analysis. *) -let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~formals ~actuals astate = +let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post + ~captured_vars_with_actuals ~formals ~actuals astate = L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name (Pp.seq ~sep:"," Var.pp) formals pp pre_post ; let empty_call_state = @@ -522,7 +544,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~forma in (* read the precondition *) match - materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state + materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals + ~actuals empty_call_state with | exception Contradiction reason -> (* can't make sense of the pre-condition in the current context: give up on that particular @@ -540,7 +563,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~forma (* reset [visited] *) let call_state = {call_state with astate; visited= AddressSet.empty} in (* apply the postcondition *) - apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state + apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals + ~actuals call_state with | Ok post -> Ok (Some post) diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index e1817fe28..b1079946c 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/infer/src/pulse/PulseInterproc.mli @@ -12,6 +12,7 @@ val apply_prepost : Procname.t -> Location.t -> callee_prepost:PulseAbductiveDomain.t + -> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list -> formals:Var.t list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> PulseAbductiveDomain.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index f025e34e6..f382f7d60 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -69,14 +69,9 @@ module Closures = struct let record location pname captured astate = let captured_addresses = - List.rev_filter_map captured - ~f:(fun (captured_as, (address_captured, trace_captured), mode) -> - match mode with - | Pvar.ByValue -> - None - | Pvar.ByReference -> - let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in - Some (address_captured, new_trace) ) + List.filter_map captured ~f:(fun (captured_as, (address_captured, trace_captured), mode) -> + let new_trace = ValueHistory.Capture {captured_as; mode; location} :: trace_captured in + Some (address_captured, new_trace) ) in let closure_addr_hist = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in let fake_capture_edges = mk_capture_edges captured_addresses in @@ -440,9 +435,11 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = |> havoc_ret ret |> add_skipped_proc -let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals astate = +let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals + ~actuals astate = let apply callee_prepost ~f = - PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~formals ~actuals astate + PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals + ~formals ~actuals astate >>| function | None -> (* couldn't apply pre/post pair *) None @@ -468,6 +465,26 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals apply astate ~f:(fun astate -> ExitProgram astate) +let get_captured_actuals location ~captured_vars ~actual_closure astate = + let* astate, this_value_addr = eval_access location actual_closure Dereference astate in + let+ _, astate, captured_vars_with_actuals = + List.fold_result captured_vars ~init:(0, astate, []) + ~f:(fun (id, astate, captured) (var, mode) -> + let* astate, field = + eval_access location this_value_addr (FieldAccess (Closures.mk_fake_field ~id)) astate + in + let+ astate, captured_actual = + match mode with + | Pvar.ByReference -> + eval_access location field Dereference astate + | Pvar.ByValue -> + Ok (astate, field) + in + (id + 1, astate, (var, captured_actual) :: captured) ) + in + (astate, captured_vars_with_actuals) + + let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) : (ExecutionDomain.t list, Diagnostic.t * t) result = match callee_data with @@ -476,6 +493,21 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : Procdesc.get_formals callee_proc_desc |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) in + let captured_vars = + Procdesc.get_captured callee_proc_desc + |> List.map ~f:(fun (mangled, _, mode) -> + let pvar = Pvar.mk mangled callee_pname in + (Var.of_pvar pvar, mode) ) + in + let* astate, captured_vars_with_actuals = + match actuals with + | (actual_closure, _) :: _ + when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> + (* Assumption: the first parameter will be a closure *) + get_captured_actuals call_loc ~captured_vars ~actual_closure astate + | _ -> + Ok (astate, []) + in let is_blacklist = Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex -> Str.string_match regex (Procname.to_string callee_pname) 0 ) @@ -485,7 +517,8 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : ~f:(fun posts callee_exec_state -> (* apply all pre/post specs *) match - apply_callee callee_pname call_loc callee_exec_state ~formals ~actuals ~ret astate + apply_callee callee_pname call_loc callee_exec_state ~captured_vars_with_actuals + ~formals ~actuals ~ret astate with | Ok None -> (* couldn't apply pre/post pair *) diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index b149026c1..3d9c94ecf 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -12,7 +12,7 @@ type event = | Allocation of {f: CallEvent.t; location: Location.t} | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} - | Capture of {captured_as: Pvar.t; location: Location.t} + | Capture of {captured_as: Pvar.t; mode: Pvar.capture_mode; location: Location.t} | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t @@ -33,8 +33,10 @@ let pp_event_no_location fmt event = F.fprintf fmt "passed as argument to %a" CallEvent.pp f | Allocation {f} -> F.fprintf fmt "allocated by call to %a" CallEvent.pp f - | Capture {captured_as; location= _} -> - F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as + | Capture {captured_as; mode; location= _} -> + F.fprintf fmt "value captured by %s as `%a`" + (Pvar.string_of_capture_mode mode) + Pvar.pp_value_non_verbose captured_as | Conditional {is_then_branch; if_kind; location= _} -> F.fprintf fmt "expression in %s condition is %b" (Sil.if_kind_to_string if_kind) is_then_branch diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index d685dbfad..56db0dc5e 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -12,7 +12,7 @@ type event = | Allocation of {f: CallEvent.t; location: Location.t} | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} - | Capture of {captured_as: Pvar.t; location: Location.t} + | Capture of {captured_as: Pvar.t; mode: Pvar.capture_mode; location: Location.t} | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index 44a0ba098..f39061f84 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -170,3 +170,84 @@ void function_assign_null_ok() { std::function f = [] { return 1; }; f = nullptr; } + +void capture_by_value_ok() { + int value = 5; + auto f = [value]() -> int* { return new int(value); }; + value++; + int* p = f(); + int* q = nullptr; + if (*p != 5) { + *q = 42; + } +} + +void capture_by_value_bad() { + int value = 5; + auto f = [value]() -> int* { return new int(value); }; + value++; + int* p = f(); + int* q = nullptr; + if (*p == 5) { + *q = 42; + } +} + +void capture_by_ref_ok() { + int value = 5; + auto f = [&value]() -> int* { return new int(value); }; + value++; + int* p = f(); + int* q = nullptr; + if (*p != 6) { + *q = 42; + } +} + +void capture_by_ref_bad() { + int value = 5; + auto f = [&value]() -> int* { return new int(value); }; + value++; + int* p = f(); + int* q = nullptr; + if (*p == 6) { + *q = 42; + } +} + +S* update_inside_lambda_capture_and_init(S* s) { + S* object = nullptr; + auto f = [& o = object](S* s) { o = s; }; + f(s); + return object; +} + +int update_inside_lambda_capture_and_init_ok(S* param_s) { + return update_inside_lambda_capture_and_init(param_s)->f; +} + +S* update_inside_lambda_capture_only(S* s) { + S* object = nullptr; + /* FIXME: clang AST gives us `S*` for variable `object` in the + lambda's body, hence the translation misses one dereference */ + auto f = [&object](S* s) { object = s; }; + f(s); + return object; +} + +int update_inside_lambda_capture_only_ok_FP(S* param_s) { + return update_inside_lambda_capture_only(param_s)->f; +} + +void call_argument(std::function f, S* s) { f(s); } + +S* update_inside_lambda_as_argument(S* s) { + S* object = nullptr; + auto f = [& o = object](S* s) { o = s; }; + call_argument(f, s); + return object; +} + +int update_inside_lambda_as_argument_ok_FP(S* param_s) { + return update_inside_lambda_as_argument(param_s)->f; +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 19931d647..9b2f2765c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -7,9 +7,13 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, capture_by_ref_bad, 7, 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/cpp/pulse/closures.cpp, capture_by_value_bad, 7, 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/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by by ref as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by by ref as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by by ref as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `update_inside_lambda_as_argument`,return from call to `update_inside_lambda_as_argument`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_capture_only_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_capture_only` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `update_inside_lambda_capture_only`,return from call to `update_inside_lambda_capture_only`,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs here]