pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] generalise "invalid" addresses as sets of attributes

Browse Source 
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
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 637018a330
commit 1c8143898e
4 changed files with 80 additions and 81 deletions
Show Stats Download Patch File Download Diff File

126
infer/src/checkers/PulseDomain.ml
Unescape View File

@ -144,38 +144,67 @@ end
meaningless on their own. *) meaningless on their own. *)
module AliasingDomain = AbstractDomain.Map (Var) (AbstractAddressDomain_JoinIsMin) 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 *) include module type of AbstractDomain.Map (AbstractAddress) (Attributes)
module InvalidAddressesDomain : sig
include AbstractDomain.S
val empty : astate val empty : astate
val add : AbstractAddress.t -> Invalidation.t -> astate -> astate val invalidate : AbstractAddress.t -> Invalidation.t -> astate -> astate
val fold :
(AbstractAddress.t -> Invalidation.t -> 'accum -> 'accum) -> astate -> 'accum -> 'accum
val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option
(** None denotes a valid location *) (** None denotes a valid location *)
end = struct 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 end
(** the domain *) (** 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 = let initial =
{ heap= Memory.empty { heap= Memory.empty
; stack= AliasingDomain.empty ; stack= AliasingDomain.empty
; invalids= ; attributes=
InvalidAddressesDomain.empty AttributesDomain.empty
(* TODO: this makes the analysis go a bit overboard with the Nullptr reports. *) (* TODO: this makes the analysis go a bit overboard with the Nullptr reports. *)
(* (* always recall that 0 is invalid *) (* (* 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 type astate = t
let piecewise_lessthan lhs rhs = 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 && AliasingDomain.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack
&& Memory.for_all && Memory.for_all
(fun addr_src edges -> (fun addr_src edges ->
@ -285,8 +314,8 @@ module Domain : AbstractDomain.S with type astate = t = struct
stack1 stack2) stack1 stack2)
let from_astate_union {heap= heap1; stack= stack1; invalids= invalids1} let from_astate_union {heap= heap1; stack= stack1; attributes= attributes1}
{heap= heap2; stack= stack2; invalids= invalids2} = {heap= heap2; stack= stack2; attributes= attributes2} =
let subst = AddressUF.create () in let subst = AddressUF.create () in
(* gather equalities from the stacks *) (* gather equalities from the stacks *)
populate_subst_from_stacks subst stack1 stack2 ; 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] *) common thanks to [AbstractAddressDomain_JoinIsMin] *)
let stack = AliasingDomain.join stack1 stack2 in let stack = AliasingDomain.join stack1 stack2 in
(* basically union *) (* basically union *)
let invalids = InvalidAddressesDomain.join invalids1 invalids2 in let attributes = AttributesDomain.join attributes1 attributes2 in
{subst; astate= {heap; stack; invalids}} {subst; astate= {heap; stack; attributes}}
(** compute new set of invalid addresses for a given join state *) (** compute new address attributes for a given join state *)
let to_invalids {subst; astate= {invalids= old_invalids} as astate} = 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 (* 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 reachable from stack variables it suffices to check if the address appears in either the
heap or the stack. *) heap or the stack. *)
@ -310,35 +339,30 @@ module Domain : AbstractDomain.S with type astate = t = struct
Memory.mem address astate.heap Memory.mem address astate.heap
|| AliasingDomain.exists (fun _ value -> AbstractAddress.equal value address) astate.stack || AliasingDomain.exists (fun _ value -> AbstractAddress.equal value address) astate.stack
in in
(* given a previously known invalid address [old_address], add the new address that let add_old_attribute astate old_address old_attribute new_attributes =
represents it to [new_invalids] *)
let add_old_invalid astate old_address old_invalid new_invalids =
(* the address has to make sense for the new heap *) (* the address has to make sense for the new heap *)
let repr = AddressUF.find subst old_address in let repr = AddressUF.find subst old_address in
let new_address = (repr :> AbstractAddress.t) in let new_address = (repr :> AbstractAddress.t) in
match InvalidAddressesDomain.get_invalidation new_address new_invalids with match AttributesDomain.find_opt new_address new_attributes with
| Some new_invalid -> | Some new_attribute ->
(* We have seen a representative of this address already: join. This can happen when (* We have seen a representative of this address already: join. *)
several previously invalid addresses correspond to the same representative in AttributesDomain.add new_address
[subst]. Doing the join of all known invalidation reasons to make results more (AttributesDomain.Attributes.join new_attribute old_attribute)
deterministic(?). *) new_attributes
InvalidAddressesDomain.add new_address
(Invalidation.join new_invalid old_invalid)
new_invalids
| None -> | 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) *) convergence) *)
if address_is_live astate new_address then 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 else
(* we can forget about the fact that this location is invalid since nothing can (* we can forget about the attributes for this address since nothing can refer to it
refer to it anymore *) anymore *)
new_invalids new_attributes
in in
InvalidAddressesDomain.fold AttributesDomain.fold
(fun old_address old_invalid new_invalids -> (fun old_address old_attribute new_attributes ->
add_old_invalid astate old_address old_invalid new_invalids ) add_old_attribute astate old_address old_attribute new_attributes )
old_invalids InvalidAddressesDomain.empty old_attributes AttributesDomain.empty
let rec normalize state = let rec normalize state =
@ -365,8 +389,8 @@ module Domain : AbstractDomain.S with type astate = t = struct
AddressUnionSet.pp set ) ; AddressUnionSet.pp set ) ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in
let invalids = to_invalids state in let attributes = to_attributes state in
{heap; stack; invalids} ) {heap; stack; attributes} )
else normalize {state with astate= {state.astate with heap}} else normalize {state with astate= {state.astate with heap}}
end end
@ -424,9 +448,9 @@ module Domain : AbstractDomain.S with type astate = t = struct
else join prev next else join prev next
let pp fmt {heap; stack; invalids} = let pp fmt {heap; stack; attributes} =
F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@;invalids=@[<hv>%a@];@]}" Memory.pp F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@;attributes=@[<hv>%a@];@]}"
heap AliasingDomain.pp stack InvalidAddressesDomain.pp invalids Memory.pp heap AliasingDomain.pp stack AttributesDomain.pp attributes
end end
(* {2 Access operations on the domain} *) (* {2 Access operations on the domain} *)
@ -469,15 +493,15 @@ module Diagnostic = struct
Invalidation.issue_type_of_cause invalidated_by Invalidation.issue_type_of_cause invalidated_by
end end
type 'a access_result = ('a, Diagnostic.t) result
(** operations on the domain *) (** operations on the domain *)
module Operations = struct module Operations = struct
open Result.Monad_infix open Result.Monad_infix
type 'a access_result = ('a, Diagnostic.t) result
(** Check that the address is not known to be invalid *) (** Check that the address is not known to be invalid *)
let check_addr_access actor address astate = 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 -> | Some invalidated_by ->
Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address}) Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address})
| None -> | None ->
@ -559,7 +583,7 @@ module Operations = struct
(** Add the given address to the set of know invalid addresses. *) (** Add the given address to the set of know invalid addresses. *)
let mark_invalid actor address astate = 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 = let havoc_var var astate =

26
infer/src/checkers/PulseInvalidation.ml
Unescape View File

@ -6,7 +6,6 @@
*) *)
open! IStd open! IStd
module F = Format module F = Format
module L = Logging
type t = type t =
| CFree of AccessExpression.t * Location.t | CFree of AccessExpression.t * Location.t
@ -54,28 +53,3 @@ let pp f = function
| StdVectorPushBack (access_expr, location) -> | StdVectorPushBack (access_expr, location) ->
F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a" F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a"
AccessExpression.pp access_expr Location.pp location 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

3
infer/src/checkers/PulseInvalidation.mli
Unescape View File

@ -12,9 +12,10 @@ type t =
| CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t
| Nullptr | Nullptr
| StdVectorPushBack of AccessExpression.t * Location.t | StdVectorPushBack of AccessExpression.t * Location.t
[@@deriving compare]
val issue_type_of_cause : t -> IssueType.t val issue_type_of_cause : t -> IssueType.t
val get_location : t -> Location.t option val get_location : t -> Location.t option
include AbstractDomain.S with type astate = t val pp : Format.formatter -> t -> unit

6
infer/tests/codetoanalyze/cpp/pulse/issues.exp
Unescape View File

@ -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_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 70, column 7 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 26, column 5 here,accessed `*(result)` 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/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_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] 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]

Write Preview
Loading…
Cancel
Save