From 1c8143898e1ccf74d83a7452065474632a0209b2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 6 Nov 2018 07:19:29 -0800 Subject: [PATCH] [pulse] generalise "invalid" addresses as sets of attributes Summary: Instead of keeping at most one invalidation fact for each address, keep a set of them and call them "attributes". Keeping a set of invalidation facts is redundant since we always only want the smallest one, but makes the implementation simpler, especially once we add more kinds of attributes (used for modelling, see next diffs). Reviewed By: mbouaziz Differential Revision: D12939839 fbshipit-source-id: 4a54c2132 --- infer/src/checkers/PulseDomain.ml | 126 +++++++++++------- infer/src/checkers/PulseInvalidation.ml | 26 ---- infer/src/checkers/PulseInvalidation.mli | 3 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 6 +- 4 files changed, 80 insertions(+), 81 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index dd40b2aba..16ea0c844 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -144,38 +144,67 @@ end meaningless on their own. *) module AliasingDomain = AbstractDomain.Map (Var) (AbstractAddressDomain_JoinIsMin) -(* {3 Invalid addresses domain } *) +(** Attributes attached to addresses. This keeps track of which addresses are invalid, but is also + used by models for bookkeeping. *) +module AttributesDomain : sig + module Attributes : AbstractDomain.S -(** Locations known to be invalid for some reason *) -module InvalidAddressesDomain : sig - include AbstractDomain.S + include module type of AbstractDomain.Map (AbstractAddress) (Attributes) val empty : astate - val add : AbstractAddress.t -> Invalidation.t -> astate -> astate - - val fold : - (AbstractAddress.t -> Invalidation.t -> 'accum -> 'accum) -> astate -> 'accum -> 'accum + val invalidate : AbstractAddress.t -> Invalidation.t -> astate -> astate val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option (** None denotes a valid location *) end = struct - include AbstractDomain.Map (AbstractAddress) (Invalidation) + module Attribute = struct + (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more + efficient (only need to look at the first element in the set of attributes to know if an + address is invalid) *) + type t = Invalid of Invalidation.t [@@deriving compare] + + let pp f = function Invalid invalidation -> Invalidation.pp f invalidation + end + + module Attributes = AbstractDomain.FiniteSet (Attribute) + include AbstractDomain.Map (AbstractAddress) (Attributes) + + let add_attribute address attribute attribute_map = + let attributes = + match find_opt address attribute_map with + | Some old_attributes -> + Attributes.add attribute old_attributes + | None -> + Attributes.singleton attribute + in + add address attributes attribute_map - let get_invalidation address invalids = find_opt address invalids + + let invalidate address invalidation attribute_map = + add_attribute address (Attribute.Invalid invalidation) attribute_map + + + let get_invalidation address attribute_map = + (* Since we often want to find out whether an address is invalid this case is optimised. Since + [Invalid _] attributes are the smallest we can simply look at the first element to decide if + an address is invalid or not. *) + find_opt address attribute_map + |> Option.bind ~f:Attributes.min_elt_opt + |> Option.map ~f:(function Attribute.Invalid invalidation -> invalidation) end (** the domain *) -type t = {heap: Memory.t; stack: AliasingDomain.astate; invalids: InvalidAddressesDomain.astate} +type t = {heap: Memory.t; stack: AliasingDomain.astate; attributes: AttributesDomain.astate} let initial = { heap= Memory.empty ; stack= AliasingDomain.empty - ; invalids= - InvalidAddressesDomain.empty + ; attributes= + AttributesDomain.empty (* TODO: this makes the analysis go a bit overboard with the Nullptr reports. *) (* (* always recall that 0 is invalid *) - InvalidAddressesDomain.add AbstractAddress.nullptr Nullptr InvalidAddressesDomain.empty *) + AttributesDomain.add AbstractAddress.nullptr Nullptr AttributesDomain.empty *) } @@ -183,7 +212,7 @@ module Domain : AbstractDomain.S with type astate = t = struct type astate = t let piecewise_lessthan lhs rhs = - InvalidAddressesDomain.( <= ) ~lhs:lhs.invalids ~rhs:rhs.invalids + AttributesDomain.( <= ) ~lhs:lhs.attributes ~rhs:rhs.attributes && AliasingDomain.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Memory.for_all (fun addr_src edges -> @@ -285,8 +314,8 @@ module Domain : AbstractDomain.S with type astate = t = struct stack1 stack2) - let from_astate_union {heap= heap1; stack= stack1; invalids= invalids1} - {heap= heap2; stack= stack2; invalids= invalids2} = + let from_astate_union {heap= heap1; stack= stack1; attributes= attributes1} + {heap= heap2; stack= stack2; attributes= attributes2} = let subst = AddressUF.create () in (* gather equalities from the stacks *) populate_subst_from_stacks subst stack1 stack2 ; @@ -297,12 +326,12 @@ module Domain : AbstractDomain.S with type astate = t = struct common thanks to [AbstractAddressDomain_JoinIsMin] *) let stack = AliasingDomain.join stack1 stack2 in (* basically union *) - let invalids = InvalidAddressesDomain.join invalids1 invalids2 in - {subst; astate= {heap; stack; invalids}} + let attributes = AttributesDomain.join attributes1 attributes2 in + {subst; astate= {heap; stack; attributes}} - (** compute new set of invalid addresses for a given join state *) - let to_invalids {subst; astate= {invalids= old_invalids} as astate} = + (** compute new address attributes for a given join state *) + let to_attributes {subst; astate= {attributes= old_attributes} as astate} = (* Is the address reachable from the stack variables? Since the new heap only has addresses reachable from stack variables it suffices to check if the address appears in either the heap or the stack. *) @@ -310,35 +339,30 @@ module Domain : AbstractDomain.S with type astate = t = struct Memory.mem address astate.heap || AliasingDomain.exists (fun _ value -> AbstractAddress.equal value address) astate.stack in - (* given a previously known invalid address [old_address], add the new address that - represents it to [new_invalids] *) - let add_old_invalid astate old_address old_invalid new_invalids = + let add_old_attribute astate old_address old_attribute new_attributes = (* the address has to make sense for the new heap *) let repr = AddressUF.find subst old_address in let new_address = (repr :> AbstractAddress.t) in - match InvalidAddressesDomain.get_invalidation new_address new_invalids with - | Some new_invalid -> - (* We have seen a representative of this address already: join. This can happen when - several previously invalid addresses correspond to the same representative in - [subst]. Doing the join of all known invalidation reasons to make results more - deterministic(?). *) - InvalidAddressesDomain.add new_address - (Invalidation.join new_invalid old_invalid) - new_invalids + match AttributesDomain.find_opt new_address new_attributes with + | Some new_attribute -> + (* We have seen a representative of this address already: join. *) + AttributesDomain.add new_address + (AttributesDomain.Attributes.join new_attribute old_attribute) + new_attributes | None -> - (* only record the old invalidation fact if the address is still reachable (helps + (* only record the attributes fact if the address is still reachable (helps convergence) *) if address_is_live astate new_address then - InvalidAddressesDomain.add new_address old_invalid new_invalids + AttributesDomain.add new_address old_attribute new_attributes else - (* we can forget about the fact that this location is invalid since nothing can - refer to it anymore *) - new_invalids + (* we can forget about the attributes for this address since nothing can refer to it + anymore *) + new_attributes in - InvalidAddressesDomain.fold - (fun old_address old_invalid new_invalids -> - add_old_invalid astate old_address old_invalid new_invalids ) - old_invalids InvalidAddressesDomain.empty + AttributesDomain.fold + (fun old_address old_attribute new_attributes -> + add_old_attribute astate old_address old_attribute new_attributes ) + old_attributes AttributesDomain.empty let rec normalize state = @@ -365,8 +389,8 @@ module Domain : AbstractDomain.S with type astate = t = struct AddressUnionSet.pp set ) ; L.d_decrease_indent () ; let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in - let invalids = to_invalids state in - {heap; stack; invalids} ) + let attributes = to_attributes state in + {heap; stack; attributes} ) else normalize {state with astate= {state.astate with heap}} end @@ -424,9 +448,9 @@ module Domain : AbstractDomain.S with type astate = t = struct else join prev next - let pp fmt {heap; stack; invalids} = - F.fprintf fmt "{@[ heap=@[%a@];@;stack=@[%a@];@;invalids=@[%a@];@]}" Memory.pp - heap AliasingDomain.pp stack InvalidAddressesDomain.pp invalids + let pp fmt {heap; stack; attributes} = + F.fprintf fmt "{@[ heap=@[%a@];@;stack=@[%a@];@;attributes=@[%a@];@]}" + Memory.pp heap AliasingDomain.pp stack AttributesDomain.pp attributes end (* {2 Access operations on the domain} *) @@ -469,15 +493,15 @@ module Diagnostic = struct Invalidation.issue_type_of_cause invalidated_by end +type 'a access_result = ('a, Diagnostic.t) result + (** operations on the domain *) module Operations = struct open Result.Monad_infix - type 'a access_result = ('a, Diagnostic.t) result - (** Check that the address is not known to be invalid *) let check_addr_access actor address astate = - match InvalidAddressesDomain.get_invalidation address astate.invalids with + match AttributesDomain.get_invalidation address astate.attributes with | Some invalidated_by -> Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address}) | None -> @@ -559,7 +583,7 @@ module Operations = struct (** Add the given address to the set of know invalid addresses. *) let mark_invalid actor address astate = - {astate with invalids= InvalidAddressesDomain.add address actor astate.invalids} + {astate with attributes= AttributesDomain.invalidate address actor astate.attributes} let havoc_var var astate = diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml index b60f9468a..2a98b9730 100644 --- a/infer/src/checkers/PulseInvalidation.ml +++ b/infer/src/checkers/PulseInvalidation.ml @@ -6,7 +6,6 @@ *) open! IStd module F = Format -module L = Logging type t = | CFree of AccessExpression.t * Location.t @@ -54,28 +53,3 @@ let pp f = function | StdVectorPushBack (access_expr, location) -> F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a" AccessExpression.pp access_expr Location.pp location - - -module Domain : AbstractDomain.S with type astate = t = struct - type astate = t - - let pp = pp - - let join i1 i2 = - if [%compare.equal: t] i1 i2 then i1 - else - (* take the max, but it should be unusual for the same location to be invalidated in two - different ways *) - let kept, forgotten = if compare i1 i2 >= 0 then (i1, i2) else (i2, i1) in - L.debug Analysis Quiet - "forgetting about invalidation %a for address already invalidated by %a@\n" pp forgotten pp - kept ; - kept - - - let ( <= ) ~lhs ~rhs = compare lhs rhs <= 0 - - let widen ~prev ~next ~num_iters:_ = join prev next -end - -include Domain diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli index 9d1156b26..16104d01a 100644 --- a/infer/src/checkers/PulseInvalidation.mli +++ b/infer/src/checkers/PulseInvalidation.mli @@ -12,9 +12,10 @@ type t = | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t | Nullptr | StdVectorPushBack of AccessExpression.t * Location.t +[@@deriving compare] val issue_type_of_cause : t -> IssueType.t val get_location : t -> Location.t option -include AbstractDomain.S with type astate = t +val pp : Format.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 229bc12ba..2dc839565 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,6 +1,6 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 26, column 5 here,accessed `*(result)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]