[pulse] more efficient representation of attributes

Summary:
This ensures that each attribute type can only be present once per
address. Makes ~80x time improvement on pathological cases such as
Duff's device.

This introduces a new kind of Set in `PrettyPrintable`.

Reviewed By: mbouaziz

Differential Revision: D14645091

fbshipit-source-id: c7f9b760c
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent d57ed5086e
commit 3ce095a288

@ -16,7 +16,7 @@ Format.sprintf
(ocamlopt_flags (%s))
(libraries %s)
(modules All_infer_in_one_file)
(preprocess (pps ppx_compare ppx_sexp_conv -no-check))
(preprocess (pps ppx_compare ppx_sexp_conv ppx_variants_conv -no-check))
)
|}
(String.concat " " common_cflags)

@ -63,7 +63,7 @@ let stanzas =
(ocamlopt_flags (%s))
(libraries %s)
(modules :standard \ %s infertop)
(preprocess (pps ppx_compare ppx_sexp_conv -no-check))
(preprocess (pps ppx_compare ppx_sexp_conv ppx_variants_conv -no-check))
)
(documentation
@ -83,7 +83,7 @@ let stanzas =
(ocamlopt_flags (%s))
(libraries InferModules)
(modules %s)
(preprocess (pps ppx_compare ppx_sexp_conv -no-check))
(preprocess (pps ppx_compare ppx_sexp_conv ppx_variants_conv -no-check))
)
|}
(String.concat " " infer_binaries)
@ -97,7 +97,7 @@ let stanzas =
(flags (%s))
(libraries utop InferModules)
(modules Infertop)
(preprocess (pps ppx_compare ppx_sexp_conv -no-check))
(preprocess (pps ppx_compare ppx_sexp_conv ppx_variants_conv -no-check))
(link_flags (-linkall -warn-error -31))
)
|}

@ -73,10 +73,6 @@ let filter ~fold ~filter t ~init ~f =
let map ~f:g fold t ~init ~f = fold t ~init ~f:(fun acc item -> f acc (g item))
let fold_of_pervasives_fold ~fold collection ~init ~f =
fold (fun item accum -> f accum item) collection init
let fold_of_pervasives_map_fold ~fold collection ~init ~f =
fold (fun item value accum -> f accum (item, value)) collection init

@ -48,9 +48,6 @@ val filter :
val map : f:('a -> 'b) -> ('t, 'a, 'accum) Container.fold -> ('t, 'b, 'accum) Container.fold
val fold_of_pervasives_fold :
fold:(('a -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'a, 'accum) Container.fold
val fold_of_pervasives_map_fold :
fold:(('key -> 'value -> 'accum -> 'accum) -> 't -> 'accum -> 'accum)
-> ('t, 'key * 'value, 'accum) Container.fold

@ -197,3 +197,81 @@ end
module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) =
PPMonoMapOfPPMap (MakePPMap (Ord)) (Val)
module type PrintableRankedType = sig
include PrintableType
val equal : t -> t -> bool
val to_rank : t -> int
end
module type PPUniqRankSet = sig
type t
type elt
val add : t -> elt -> t
val empty : t
val equal : t -> t -> bool
val find_rank : t -> int -> elt option
val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum
val is_empty : t -> bool
val is_subset : t -> of_:t -> bool
val map : t -> f:(elt -> elt) -> t
val singleton : elt -> t
val union_prefer_left : t -> t -> t
val pp : F.formatter -> t -> unit
end
module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type elt = Val.t = struct
module Map = MakePPMonoMap (Int) (Val)
type t = Map.t
type elt = Val.t
let add map value = Map.add (Val.to_rank value) value map
let empty = Map.empty
let equal = Map.equal Val.equal
let find_rank m rank = Map.find_opt rank m
let fold map ~init ~f = Map.fold (fun _key value accum -> f accum value) map init
let is_empty = Map.is_empty
let is_subset m ~of_ =
Map.for_all
(fun rank value ->
match Map.find_opt rank of_ with None -> false | Some value' -> Val.equal value value' )
m
let map m ~f =
Map.mapi
(fun rank value ->
let value' = f value in
assert (Int.equal rank (Val.to_rank value')) ;
value' )
m
let pp = Map.pp
let singleton value = add Map.empty value
let union_prefer_left m1 m2 = Map.union (fun _rank value1 _value2 -> Some value1) m1 m2
end

@ -147,3 +147,44 @@ module PPMonoMapOfPPMap (M : PPMap) (Val : PrintableType) :
module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) :
PPMonoMap with type key = Ord.t and type value = Val.t
module type PrintableRankedType = sig
include PrintableType
val equal : t -> t -> bool
val to_rank : t -> int
end
(** set where at most one element of a given rank can be present *)
module type PPUniqRankSet = sig
type t
type elt
val add : t -> elt -> t
val empty : t
val equal : t -> t -> bool
val find_rank : t -> int -> elt option
val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum
val is_empty : t -> bool
val is_subset : t -> of_:t -> bool
val map : t -> f:(elt -> elt) -> t
val singleton : elt -> t
val union_prefer_left : t -> t -> t
(** in case an element with the same rank is present both in [lhs] and [rhs], keep the one from
[lhs] in [union_prefer_left lhs rhs] *)
val pp : F.formatter -> t -> unit
end
module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type elt = Val.t

@ -17,7 +17,7 @@ module BaseMemory = PulseDomain.Memory
module type BaseDomain = sig
(* private because the lattice is not the same for preconditions and postconditions so we don't
want to confuse them *)
type t = private PulseDomain.t [@@deriving compare]
type t = private PulseDomain.t
val empty : t
@ -54,7 +54,7 @@ end
module InvertedDomain : BaseDomain = struct
include BaseDomainCommon
type t = PulseDomain.t [@@deriving compare]
type t = PulseDomain.t
let empty = PulseDomain.empty
@ -68,7 +68,6 @@ end
type t =
{ post: Domain.t (** state at the current program point*)
; pre: InvertedDomain.t (** inferred pre at the current program point *) }
[@@deriving compare]
let pp f {post; pre} = F.fprintf f "@[<v>%a@;[%a]@]" Domain.pp post InvertedDomain.pp pre
@ -491,14 +490,16 @@ module PrePost = struct
delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state
in
let new_attrs =
let attrs_post = Attributes.map (add_call_to_attr callee_proc_name call_loc) attrs_post in
let attrs_post =
Attributes.map ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) attrs_post
in
match
PulseDomain.Memory.find_attrs_opt addr_caller (call_state.astate.post :> base_domain).heap
with
| None ->
attrs_post
| Some old_attrs_post ->
Attributes.union old_attrs_post attrs_post
Attributes.union_prefer_left old_attrs_post attrs_post
in
let subst, translated_post_edges =
PulseDomain.Memory.Edges.fold_map ~init:call_state.subst edges_post

@ -14,17 +14,33 @@ module Invalidation = PulseInvalidation
(** Purposefully declared before [AbstractAddress] to avoid attributes depending on
addresses. Otherwise they become a pain to handle when comparing memory states. *)
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 =
(* DO NOT MOVE, see toplevel comment *)
| Invalid of Invalidation.t PulseTrace.action
| MustBeValid of HilExp.AccessExpression.t PulseTrace.action
| AddressOfCppTemporary of Var.t * Location.t option
| Closure of Typ.Procname.t
| StdVectorReserve
[@@deriving compare]
[@@deriving compare, variants]
let equal = [%compare.equal: t]
let to_rank = Variants.to_rank
let invalid_rank =
Variants.to_rank (Invalid (Immediate {imm= Invalidation.Nullptr; location= Location.dummy}))
let must_be_valid_rank =
Variants.to_rank
(MustBeValid
(Immediate
{ imm=
HilExp.AccessExpression.base
(AccessPath.base_of_pvar (Pvar.mk_global Mangled.self) Typ.void)
; location= Location.dummy }))
let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
let pp f = function
| Invalid invalidation ->
@ -37,26 +53,33 @@ module Attribute = struct
| AddressOfCppTemporary (var, location_opt) ->
F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
| Closure pname ->
F.fprintf f "%a" Typ.Procname.pp pname
Typ.Procname.pp f pname
| StdVectorReserve ->
F.pp_print_string f "std::vector::reserve()"
end
module Attributes = struct
include AbstractDomain.FiniteSet (Attribute)
module Set = PrettyPrintable.MakePPUniqRankSet (Attribute)
let get_invalid attrs =
(* 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. *)
match min_elt_opt attrs with Some (Invalid invalidation) -> Some invalidation | _ -> None
Set.find_rank attrs Attribute.invalid_rank
|> Option.map ~f:(fun attr ->
let[@warning "-8"] (Attribute.Invalid invalidation) = attr in
invalidation )
let get_must_be_valid attrs =
find_first_opt (function MustBeValid _ -> true | _ -> false) attrs
Set.find_rank attrs Attribute.must_be_valid_rank
|> Option.map ~f:(fun attr ->
let[@warning "-8"] (Attribute.MustBeValid action) = attr in
action )
let is_std_vector_reserved attrs =
Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some
include Set
end
(** An abstract address in memory. *)
@ -126,7 +149,7 @@ module Memory : sig
type cell = edges * Attributes.t
type t [@@deriving compare]
type t
val empty : t
@ -174,11 +197,11 @@ end = struct
type edges = AddrTracePair.t Edges.t [@@deriving compare]
type cell = edges * Attributes.t [@@deriving compare]
type cell = edges * Attributes.t
module Graph = PrettyPrintable.MakePPMap (AbstractAddress)
type t = edges Graph.t * Attributes.t Graph.t [@@deriving compare]
type t = edges Graph.t * Attributes.t Graph.t
let pp =
Pp.pair
@ -218,17 +241,14 @@ end = struct
Graph.find_opt addr (fst memory) >>= Edges.find_opt access
(* TODO: maybe sets for attributes is overkill and a list would be better? *)
let add_attributes addr attrs memory =
if Attributes.is_empty attrs then memory
else
let old_attrs = Graph.find_opt addr (snd memory) |> Option.value ~default:Attributes.empty in
if phys_equal old_attrs attrs then memory
if phys_equal old_attrs attrs || Attributes.is_subset attrs ~of_:old_attrs then memory
else
let new_attrs = Attributes.union attrs old_attrs in
if phys_equal new_attrs old_attrs then
(* unlikely as [union] makes no effort to preserve physical equality *) memory
else (fst memory, Graph.add addr new_attrs (snd memory))
let new_attrs = Attributes.union_prefer_left attrs old_attrs in
(fst memory, Graph.add addr new_attrs (snd memory))
let add_attribute address attribute memory =
@ -240,6 +260,7 @@ end = struct
let check_valid address memory =
L.d_printfln "Checking validity of %a" AbstractAddress.pp address ;
match Graph.find_opt address (snd memory) |> Option.bind ~f:Attributes.get_invalid with
| Some invalidation ->
Error invalidation
@ -252,7 +273,7 @@ end = struct
let is_std_vector_reserved address memory =
Graph.find_opt address (snd memory)
|> Option.value_map ~default:false ~f:(fun attributes ->
Attributes.mem Attribute.StdVectorReserve attributes )
Attributes.is_std_vector_reserved attributes )
(* {3 Monomorphic {!PPMap} interface as needed } *)
@ -319,7 +340,7 @@ module Stack = struct
let compare = compare VarValue.compare
end
type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
type t = {heap: Memory.t; stack: Stack.t}
let empty =
{ heap=

@ -19,7 +19,7 @@ module Attribute : sig
end
module Attributes : sig
include PrettyPrintable.PPSet with type elt = Attribute.t
include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t
val get_must_be_valid : t -> HilExp.AccessExpression.t PulseTrace.action option
end
@ -71,7 +71,7 @@ module Memory : sig
type cell = edges * Attributes.t
type t [@@deriving compare]
type t
val filter : (AbstractAddress.t -> bool) -> t -> t
@ -104,7 +104,7 @@ module Memory : sig
val is_std_vector_reserved : AbstractAddress.t -> t -> bool
end
type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
type t = {heap: Memory.t; stack: Stack.t}
val empty : t

@ -213,8 +213,7 @@ let check_address_of_local_variable proc_desc address astate =
let check_address_of_cpp_temporary () =
Memory.find_opt address astate
|> Option.fold_result ~init:() ~f:(fun () (_, attrs) ->
IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
attrs ~f:(fun attr ->
IContainer.iter_result ~fold:Attributes.fold attrs ~f:(fun attr ->
match attr with
| Attribute.AddressOfCppTemporary (variable, location_opt) ->
let location = Option.value ~default:proc_location location_opt in
@ -307,8 +306,7 @@ module Closures = struct
| None ->
Ok astate
| Some (edges, attributes) ->
IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
attributes ~f:(function
IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function
| Attribute.Closure _ ->
IContainer.iter_result
~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges

@ -78,7 +78,7 @@ type 'a action =
let pp_action pp_immediate fmt = function
| Immediate {imm; _} ->
F.fprintf fmt "`%a`" pp_immediate imm
F.fprintf fmt "%a" pp_immediate imm
| ViaCall {proc_name; _} ->
F.fprintf fmt "call to `%a`" Typ.Procname.pp proc_name

@ -22,7 +22,7 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DE
codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed during call to `Simple::Simple` here,accessed `__param_0->f` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_destruct_pointer_contents_then_placement_new2_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `<placement new>(sizeof(use_after_destructor::S),&(s->f))`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::S` here,accessed `this->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_destruct_pointer_contents_then_placement_new2_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `<placement new>(sizeof(use_after_destructor::S),&(s->f))`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::S` here,accessed `*(this->f)` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `alias` here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by `delete` on `s` here,accessed `alias->f` here]

@ -84,3 +84,267 @@ void nested_loops3_ok(std::vector<BasicStruct>* c) {
(&b)->~BasicStruct();
}
}
void duff_switch_loop(char* to, char* from, unsigned int count) {
unsigned int rounds = (count + 127) / 128;
switch (count % 128) {
case 0:
do {
*to = *from++;
case 127:
*to = *from++;
case 126:
*to = *from++;
case 125:
*to = *from++;
case 124:
*to = *from++;
case 123:
*to = *from++;
case 122:
*to = *from++;
case 121:
*to = *from++;
case 120:
*to = *from++;
case 119:
*to = *from++;
case 118:
*to = *from++;
case 117:
*to = *from++;
case 116:
*to = *from++;
case 115:
*to = *from++;
case 114:
*to = *from++;
case 113:
*to = *from++;
case 112:
*to = *from++;
case 111:
*to = *from++;
case 110:
*to = *from++;
case 109:
*to = *from++;
case 108:
*to = *from++;
case 107:
*to = *from++;
case 106:
*to = *from++;
case 105:
*to = *from++;
case 104:
*to = *from++;
case 103:
*to = *from++;
case 102:
*to = *from++;
case 101:
*to = *from++;
case 100:
*to = *from++;
case 99:
*to = *from++;
case 98:
*to = *from++;
case 97:
*to = *from++;
case 96:
*to = *from++;
case 95:
*to = *from++;
case 94:
*to = *from++;
case 93:
*to = *from++;
case 92:
*to = *from++;
case 91:
*to = *from++;
case 90:
*to = *from++;
case 89:
*to = *from++;
case 88:
*to = *from++;
case 87:
*to = *from++;
case 86:
*to = *from++;
case 85:
*to = *from++;
case 84:
*to = *from++;
case 83:
*to = *from++;
case 82:
*to = *from++;
case 81:
*to = *from++;
case 80:
*to = *from++;
case 79:
*to = *from++;
case 78:
*to = *from++;
case 77:
*to = *from++;
case 76:
*to = *from++;
case 75:
*to = *from++;
case 74:
*to = *from++;
case 73:
*to = *from++;
case 72:
*to = *from++;
case 71:
*to = *from++;
case 70:
*to = *from++;
case 69:
*to = *from++;
case 68:
*to = *from++;
case 67:
*to = *from++;
case 66:
*to = *from++;
case 65:
*to = *from++;
case 64:
*to = *from++;
case 63:
*to = *from++;
case 62:
*to = *from++;
case 61:
*to = *from++;
case 60:
*to = *from++;
case 59:
*to = *from++;
case 58:
*to = *from++;
case 57:
*to = *from++;
case 56:
*to = *from++;
case 55:
*to = *from++;
case 54:
*to = *from++;
case 53:
*to = *from++;
case 52:
*to = *from++;
case 51:
*to = *from++;
case 50:
*to = *from++;
case 49:
*to = *from++;
case 48:
*to = *from++;
case 47:
*to = *from++;
case 46:
*to = *from++;
case 45:
*to = *from++;
case 44:
*to = *from++;
case 43:
*to = *from++;
case 42:
*to = *from++;
case 41:
*to = *from++;
case 40:
*to = *from++;
case 39:
*to = *from++;
case 38:
*to = *from++;
case 37:
*to = *from++;
case 36:
*to = *from++;
case 35:
*to = *from++;
case 34:
*to = *from++;
case 33:
*to = *from++;
case 32:
*to = *from++;
case 31:
*to = *from++;
case 30:
*to = *from++;
case 29:
*to = *from++;
case 28:
*to = *from++;
case 27:
*to = *from++;
case 26:
*to = *from++;
case 25:
*to = *from++;
case 24:
*to = *from++;
case 23:
*to = *from++;
case 22:
*to = *from++;
case 21:
*to = *from++;
case 20:
*to = *from++;
case 19:
*to = *from++;
case 18:
*to = *from++;
case 17:
*to = *from++;
case 16:
*to = *from++;
case 15:
*to = *from++;
case 14:
*to = *from++;
case 13:
*to = *from++;
case 12:
*to = *from++;
case 11:
*to = *from++;
case 10:
*to = *from++;
case 9:
*to = *from++;
case 8:
*to = *from++;
case 7:
*to = *from++;
case 6:
*to = *from++;
case 5:
*to = *from++;
case 4:
*to = *from++;
case 3:
*to = *from++;
case 2:
*to = *from++;
case 1:
*to = *from++;
} while (--rounds > 0);
}
}

Loading…
Cancel
Save