From 9dbbd68472679fc6aaca6ced69e3560c45bbe8c0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 11 Apr 2019 03:55:46 -0700 Subject: [PATCH] [pulse] apply summaries to globals too Summary: Similarly to function parameters (and the return value), we need to apply the pre/post of a function call to the globals mentioned in its summary. - tigthen summaries further to remember only abducible variables in the post (as well as in the pre) - take globals into account when applying pre/post pairs Reviewed By: jberdine Differential Revision: D14780800 fbshipit-source-id: fc0d180bb --- infer/src/pulse/PulseAbductiveDomain.ml | 158 +++++++++++++----- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../cpp/pulse/use_after_free.cpp | 9 + 3 files changed, 122 insertions(+), 46 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 3279cb38c..5ec9f7645 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -266,10 +266,19 @@ module PrePost = struct type t = domain_t - let of_post astate = discard_unreachable astate + let filter_for_summary astate = + let post_stack = + BaseStack.filter + (fun var _ -> Var.is_return var || Stack.is_abducible astate var) + (astate.post :> PulseDomain.t).stack + in + {astate with post= Domain.update ~stack:post_stack astate.post} + - (* machinery to apply a pre/post pair corresponding to a function's summary in a function call to - the current state *) + let of_post astate = filter_for_summary astate |> discard_unreachable + + (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call + to the current state} *) module AddressSet = PulseDomain.AbstractAddressSet module AddressMap = PulseDomain.AbstractAddressMap @@ -305,6 +314,19 @@ module PrePost = struct rev_subst AddressSet.pp visited + let fold_globals_of_stack stack call_state ~f = + Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold) + stack ~init:call_state ~f:(fun call_state (var, stack_value) -> + if Var.is_global var then + let call_state, (addr_caller, _) = + let astate, var_value = Stack.materialize var call_state.astate in + if phys_equal astate call_state.astate then (call_state, var_value) + else ({call_state with astate}, var_value) + in + f ~stack_value ~addr_caller call_state + else Ok call_state ) + + let visit call_state ~addr_callee ~addr_caller = ( match AddressMap.find_opt addr_caller call_state.rev_subst with | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') -> @@ -328,7 +350,7 @@ module PrePost = struct F.fprintf f "POST:@\n @[%a@]@\n" PulseDomain.pp (post :> PulseDomain.t) - (* reading the pre from the current state *) + (* {3 reading the pre from the current state} *) (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in [call_state.astate] starting from address [addr_caller]. Report an error if some invalid @@ -404,34 +426,51 @@ module PrePost = struct edges_pre edges_post - let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals 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 call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. *) match - PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; - let r = - IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual -> - materialize_pre_from_actual callee_proc_name call_location - ~pre:(pre_post.pre :> PulseDomain.t) - ~formal ~actual call_state ) - in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - r + IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual -> + materialize_pre_from_actual callee_proc_name call_location + ~pre:(pre_post.pre :> PulseDomain.t) + ~formal ~actual call_state ) with - | Ok result -> - Some result | Unequal_lengths -> L.d_printfln "ERROR: formals have length %d but actuals have length %d" (List.length formals) (List.length actuals) ; None - | exception Aliasing -> - (* can't make sense of the pre-condition in the current context: give up on that particular - pre/post pair *) - None + | Ok result -> + Some result - (* applying the post to the current state *) + let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = + fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state + ~f:(fun ~stack_value:(addr_pre, loc_opt) ~addr_caller call_state -> + let trace = + Option.map loc_opt ~f:(fun loc -> PulseTrace.VariableDeclaration loc) |> Option.to_list + in + materialize_pre_from_address callee_proc_name call_location + ~pre:(pre_post.pre :> PulseDomain.t) + ~addr_pre ~addr_caller trace call_state ) + + + let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; + let r = + materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals + call_state + |> Option.map + ~f: + (Result.bind ~f:(fun call_state -> + materialize_pre_for_globals callee_proc_name call_location pre_post call_state )) + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + + + (* {3 applying the post to the current state} *) let subst_find_or_new subst addr_callee = match AddressMap.find_opt addr_callee subst with @@ -581,32 +620,51 @@ module PrePost = struct call_state - let apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state = - (* reset [visited] *) - let call_state_pre = {call_state with visited= AddressSet.empty} in + let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals + call_state = (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from formal_i in post)], deleting previous info when comparing pre and post shows a difference (TODO: record in the pre when a location is written to instead of just comparing values between pre and post since it's unreliable, eg replace value read in pre with same value in post but nuke other fields in the meantime? is that possible?). *) match - PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; - let r = - List.fold2 formals actuals ~init:call_state_pre ~f:(fun call_state formal actual -> - record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual - call_state ) - in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - r + List.fold2 formals 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 + ) with - | Ok call_state -> - record_post_for_return callee_proc_name call_location pre_post ~ret call_state - |> fun {astate} -> Some astate - | exception Aliasing -> - None | Unequal_lengths -> (* should have been checked before by [materialize_pre] *) assert false + | Ok call_state -> + Some call_state + + + let apply_post_for_globals callee_proc_name call_location pre_post call_state = + match + fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state + ~f:(fun ~stack_value:(addr_callee, _) ~addr_caller call_state -> + Ok + (record_post_for_address callee_proc_name call_location pre_post ~addr_callee + ~addr_caller call_state) ) + with + | Error _ -> + (* always return [Ok _] above *) assert false + | Ok call_state -> + call_state + + + let apply_post callee_proc_name call_location pre_post ~formals ~ret ~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 + |> Option.map ~f:(fun call_state -> + apply_post_for_globals callee_proc_name call_location pre_post call_state + |> record_post_for_return callee_proc_name call_location pre_post ~ret + |> fun {astate; _} -> astate ) + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff @@ -633,6 +691,10 @@ module PrePost = struct match materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state with + | exception Aliasing -> + (* can't make sense of the pre-condition in the current context: give up on that particular + pre/post pair *) + Ok astate | None -> (* couldn't apply the pre for some technical reason (as in: not by the fault of the programmer as far as we know) *) @@ -641,14 +703,18 @@ module PrePost = struct (* error: the function call requires to read some state known to be invalid *) error | Some (Ok call_state) -> ( - (* apply the postcondition *) - match - apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state - with - | None -> - (* same as when trying to apply the pre: give up for that pre/post pair and return the + (* reset [visited] *) + let call_state = {call_state with visited= AddressSet.empty} in + (* apply the postcondition *) + match + apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state + with + | exception Aliasing -> + Ok astate + | None -> + (* same as when trying to apply the pre: give up for that pre/post pair and return the original state *) - Ok astate - | Some astate_post -> - Ok astate_post ) + Ok astate + | Some astate_post -> + Ok astate_post ) end diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 33b6df5b2..14d95286f 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -31,6 +31,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_a codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed `*(s.f)` here,start of value trace,assigned to `this->f`,returned from call to `use_after_destructor::S::S()`] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed during call to `~S` here,accessed during call to `__infer_inner_destructor_~S` here,accessed `this->f` here,start of value trace,variable declared] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `&(c)` gone out of scope here,start of use after lifetime trace,accessed `pc->f` here,start of value trace,variable declared,assigned to `pc`] +codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `free_global_pointer_ok()` here,invalidated by call to `free()` on `global_pointer` here,start of use after lifetime trace,accessed during call to `free_global_pointer_ok()` here,accessed `global_pointer` here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `x` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `*(x)` here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::assign()` on `vec` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp index b0b4450b4..1d06bf0cb 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp @@ -15,3 +15,12 @@ int double_free_simple_bad(int* x) { free(x); free(x); } + +int* global_pointer; + +void free_global_pointer_ok() { free(global_pointer); } + +void double_free_global_bad() { + free_global_pointer_ok(); + free_global_pointer_ok(); +}