From 27150cb7d3d0dc3b37b631e023fb3e4ac5e6c14d Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 9 Dec 2020 11:21:56 -0800 Subject: [PATCH] [pulse] not-completely-broken interprocedural arrays Summary: Address a long-standing embarassing TODO in a minimal way: array indices are values and when applying a summary we didn't actually bother translating callee values to caller values. Fix that in a simple way by just using the current mapping between callee and caller values and otherwise freshen callee values to avoid clashes with caller values. Reviewed By: ezgicicek Differential Revision: D25424013 fbshipit-source-id: 03ca59b9f --- infer/src/pulse/PulseBaseMemory.ml | 2 + infer/src/pulse/PulseBaseMemory.mli | 2 + infer/src/pulse/PulseInterproc.ml | 73 +++++++++++++++++++---------- 3 files changed, 52 insertions(+), 25 deletions(-) diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 9c1b8cb26..26c8c00db 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -26,6 +26,8 @@ module Access = struct access end +module AccessSet = Caml.Set.Make (Access) + module AddrTrace = struct type t = AbstractValue.t * ValueHistory.t [@@deriving compare, yojson_of] diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index b17bec9bb..9815b9b45 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -14,6 +14,8 @@ module Access : sig val equal : t -> t -> bool end +module AccessSet : Caml.Set.S with type elt = Access.t + module AddrTrace : sig type t = AbstractValue.t * ValueHistory.t end diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 7ee3fed2d..68a489873 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -151,6 +151,16 @@ let subst_find_or_new subst addr_callee ~default_hist_caller = (subst, addr_hist_caller) +let translate_access_to_caller subst (access_callee : BaseMemory.Access.t) : _ * BaseMemory.Access.t + = + match access_callee with + | ArrayAccess (typ, val_callee) -> + let subst, (val_caller, _) = subst_find_or_new subst val_callee ~default_hist_caller:[] in + (subst, ArrayAccess (typ, val_caller)) + | FieldAccess _ | TakeAddress | Dereference -> + (subst, access_callee) + + (* {3 reading the pre from the current state} *) let add_call_to_trace proc_name call_location caller_history in_call = @@ -171,11 +181,12 @@ let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_p Ok call_state | Some edges_pre -> Container.fold_result ~fold:Memory.Edges.fold ~init:call_state edges_pre - ~f:(fun call_state (access, (addr_pre_dest, _)) -> + ~f:(fun call_state (access_callee, (addr_pre_dest, _)) -> + let subst, access_caller = translate_access_to_caller call_state.subst access_callee in let astate, addr_hist_dest_caller = - Memory.eval_edge addr_hist_caller access call_state.astate + Memory.eval_edge addr_hist_caller access_caller call_state.astate in - let call_state = {call_state with astate} in + let call_state = {call_state with astate; subst} in materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ) ) @@ -311,17 +322,24 @@ let delete_edges_in_callee_pre_from_caller ~edges_pre_opt addr_caller call_state BaseMemory.find_opt addr_caller (call_state.astate.AbductiveDomain.post :> BaseDomain.t).heap with | None -> - BaseMemory.Edges.empty + (call_state.subst, BaseMemory.Edges.empty) | Some old_post_edges -> ( match edges_pre_opt with | None -> - old_post_edges + (call_state.subst, old_post_edges) | Some edges_pre -> - (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the - whole [cell_pre] beforehand so that [Edges.merge] makes sense. *) - BaseMemory.Edges.filter old_post_edges ~f:(fun (access, _) -> - (* delete edge if some edge for the same access exists in the pre *) - not (BaseMemory.Edges.mem edges_pre access) ) ) + let subst, translated_accesses_pre = + BaseMemory.Edges.fold ~init:(call_state.subst, BaseMemory.AccessSet.empty) edges_pre + ~f:(fun (subst, accesses) (access_callee, _) -> + let subst, access = translate_access_to_caller subst access_callee in + (subst, BaseMemory.AccessSet.add access accesses) ) + in + let post_edges = + BaseMemory.Edges.filter old_post_edges ~f:(fun (access_caller, _) -> + (* delete edge if some edge for the same access exists in the pre *) + not (BaseMemory.AccessSet.mem access_caller translated_accesses_pre) ) + in + (subst, post_edges) ) let record_post_cell callee_proc_name call_loc ~edges_pre_opt @@ -334,26 +352,31 @@ let record_post_cell callee_proc_name call_loc ~edges_pre_opt {call_state with astate} in let subst, translated_post_edges = - BaseMemory.Edges.fold_map ~init:call_state.subst edges_callee_post - ~f:(fun subst (addr_callee, trace_post) -> + BaseMemory.Edges.fold ~init:(call_state.subst, BaseMemory.Edges.empty) edges_callee_post + ~f:(fun (subst, translated_edges) (access_callee, (addr_callee, trace_post)) -> let subst, (addr_curr, hist_curr) = subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller in - ( subst - , ( addr_curr - , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post} - :: hist_curr ) ) ) + let subst, access = translate_access_to_caller subst access_callee in + let translated_edges = + BaseMemory.Edges.add access + ( addr_curr + , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post} + :: hist_curr ) + translated_edges + in + (subst, translated_edges) ) in - let astate = - let post_edges_minus_pre = - delete_edges_in_callee_pre_from_caller ~edges_pre_opt addr_caller call_state - in - let edges_post_caller = - BaseMemory.Edges.union_left_biased translated_post_edges post_edges_minus_pre - in - AbductiveDomain.set_post_edges addr_caller edges_post_caller call_state.astate + let call_state = {call_state with subst} in + let subst, post_edges_minus_pre = + delete_edges_in_callee_pre_from_caller ~edges_pre_opt addr_caller call_state in - {call_state with subst; astate} + let edges_post_caller = + BaseMemory.Edges.union_left_biased translated_post_edges post_edges_minus_pre + in + { call_state with + subst + ; astate= AbductiveDomain.set_post_edges addr_caller edges_post_caller call_state.astate } let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; _} as pre_post)