From 8081dbfbf1f7808a633ba4f222b4e399fc0ee5f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 28 Aug 2019 08:00:19 -0700 Subject: [PATCH] [pulse] Record the trace of the address written to Reviewed By: skcho Differential Revision: D17004433 fbshipit-source-id: 937319c27 --- infer/src/pulse/PulseAbductiveDomain.ml | 31 +++++++++++++++++++----- infer/src/pulse/PulseAbductiveDomain.mli | 5 ++-- infer/src/pulse/PulseDomain.ml | 26 ++++++++++++++------ infer/src/pulse/PulseDomain.mli | 4 ++- infer/src/pulse/PulseOperations.ml | 6 ++--- 5 files changed, 52 insertions(+), 20 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 0f5186f81..d5517555f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -168,10 +168,12 @@ module Memory = struct if phys_equal new_pre pre then astate else {astate with pre= new_pre} - let add_edge addr access new_addr_trace astate = + let add_edge addr access new_addr_trace loc astate = map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap - |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) ) + |> BaseMemory.add_attributes addr + (Attributes.singleton + (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc}))) ) let find_edge_opt address access astate = @@ -220,10 +222,12 @@ module Memory = struct let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap - let set_cell addr cell astate = + let set_cell addr cell loc astate = map_post_heap astate ~f:(fun heap -> BaseMemory.set_cell addr cell heap - |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) ) + |> BaseMemory.add_attributes addr + (Attributes.singleton + (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc}))) ) module Edges = BaseMemory.Edges @@ -582,7 +586,7 @@ module PrePost = struct {action= trace.action; f= Call proc_name; location} ; history= trace.history } | MustBeValid _ - | WrittenTo + | WrittenTo _ | AddressOfCppTemporary (_, _) | AddressOfStackVariable (_, _, _) | Closure _ @@ -617,8 +621,23 @@ module PrePost = struct (fun _ _ post_cell -> Some post_cell) post_edges_minus_pre translated_post_edges in + let written_to = + (let open Option.Monad_infix in + PulseDomain.Memory.find_opt addr_caller heap + >>= fun (_edges, attrs) -> + PulseDomain.Attributes.get_written_to attrs + >>| fun callee_action -> + PulseDomain.Attribute.WrittenTo + (PulseDomain.InterprocAction.ViaCall + {action= callee_action; f= Call callee_proc_name; location= call_loc})) + |> Option.value + ~default: + (PulseDomain.Attribute.WrittenTo + (PulseDomain.InterprocAction.Immediate {imm= (); location= call_loc})) + in PulseDomain.Memory.set_edges addr_caller edges_post_caller heap - |> PulseDomain.Memory.add_attributes addr_caller (PulseDomain.Attributes.singleton WrittenTo) + |> PulseDomain.Memory.add_attributes addr_caller + (PulseDomain.Attributes.singleton written_to) in let caller_post = Domain.make (call_state.astate.post :> base_domain).stack heap in {call_state with subst; astate= {call_state.astate with post= caller_post}} diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 4707daf05..4c25a6480 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -45,7 +45,8 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t - val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t + val add_edge : + AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> Location.t -> t -> t val check_valid : unit PulseDomain.InterprocAction.t @@ -57,7 +58,7 @@ module Memory : sig val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option - val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t + val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> Location.t -> t -> t val invalidate : AbstractAddress.t * PulseDomain.ValueHistory.t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 1f2e4a385..12f98ed0c 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -178,6 +178,8 @@ module InterprocAction = struct | ViaCall of {action: 'a t; f: call_event; location: Location.t} [@@deriving compare] + let dummy = Immediate {imm= (); location= Location.dummy} + let rec get_immediate = function | Immediate {imm; _} -> imm @@ -246,7 +248,7 @@ module Attribute = struct type t = | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t - | WrittenTo + | WrittenTo of unit InterprocAction.t | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t @@ -259,7 +261,7 @@ module Attribute = struct let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun "")) - let address_is_written_to_rank = Variants.to_rank WrittenTo + let written_to_rank = Variants.to_rank (WrittenTo InterprocAction.dummy) let address_of_stack_variable_rank = let pname = Typ.Procname.from_string_c_fun "" in @@ -274,9 +276,7 @@ module Attribute = struct {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []}) - let must_be_valid_rank = - Variants.to_rank (MustBeValid (Immediate {imm= (); location= Location.dummy})) - + let must_be_valid_rank = Variants.to_rank (MustBeValid InterprocAction.dummy) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve @@ -288,8 +288,11 @@ module Attribute = struct (InterprocAction.pp (fun _ () -> ())) action Location.pp (InterprocAction.to_outer_location action) - | WrittenTo -> - F.fprintf f "written" + | WrittenTo action -> + F.fprintf f "WrittenTo (written by %a @ %a)" + (InterprocAction.pp (fun _ () -> ())) + action Location.pp + (InterprocAction.to_outer_location action) | AddressOfCppTemporary (var, history) -> F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history | AddressOfStackVariable (var, history, location) -> @@ -317,6 +320,13 @@ module Attributes = struct action ) + let get_written_to attrs = + Set.find_rank attrs Attribute.written_to_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.WrittenTo action) = attr in + action ) + + let get_closure_proc_name attrs = Set.find_rank attrs Attribute.closure_rank |> Option.map ~f:(fun attr -> @@ -336,7 +346,7 @@ module Attributes = struct let is_modified attrs = - Option.is_some (Set.find_rank attrs Attribute.address_is_written_to_rank) + Option.is_some (Set.find_rank attrs Attribute.written_to_rank) || Option.is_some (Set.find_rank attrs Attribute.invalid_rank) diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 33f819e7b..07b4da2fe 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -83,7 +83,7 @@ module Attribute : sig type t = | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t - | WrittenTo + | WrittenTo of unit InterprocAction.t | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t @@ -96,6 +96,8 @@ module Attributes : sig val get_must_be_valid : t -> unit InterprocAction.t option + val get_written_to : t -> unit InterprocAction.t option + val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option val is_modified : t -> bool diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 8d563b5d7..840f1cb94 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -98,7 +98,7 @@ module Closures = struct let astate = Memory.set_cell closure_addr (fake_capture_edges, Attributes.singleton (Closure pname)) - astate + location astate in (astate, (closure_addr, (* TODO: trace *) [])) end @@ -178,7 +178,7 @@ let action_of_address location = InterprocAction.Immediate {imm= (); location} let write_access location addr_trace_ref access addr_trace_obj astate = let action = action_of_address location in check_addr_access action addr_trace_ref astate - >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj + >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj location let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = @@ -237,7 +237,7 @@ let shallow_copy location addr_hist astate = cell in let copy = AbstractAddress.mk_fresh () in - (Memory.set_cell copy cell astate, copy) + (Memory.set_cell copy cell location astate, copy) let check_address_escape escape_location proc_desc address history astate =