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

[AI] empty is not (necessarily) bottom

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D13358254

fbshipit-source-id: 7f5d7e409
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent 8a3592c34e
commit 764e9ee1be
21 changed files with 106 additions and 104 deletions
Show Stats Download Patch File Download Diff File

34
infer/src/absint/AbstractDomain.ml
Unescape View File

@ -43,9 +43,9 @@ end
module type WithBottom = sig module type WithBottom = sig
include S include S
val empty : t val bottom : t
val is_empty : t -> bool val is_bottom : t -> bool
end end
module type WithTop = sig module type WithTop = sig
@ -59,9 +59,9 @@ end
module BottomLifted (Domain : S) = struct module BottomLifted (Domain : S) = struct
type t = Domain.t bottom_lifted type t = Domain.t bottom_lifted
let empty = Bottom let bottom = Bottom
let is_empty = function Bottom -> true | NonBottom _ -> false let is_bottom = function Bottom -> true | NonBottom _ -> false
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
@ -194,9 +194,9 @@ end
module Flat (V : PrettyPrintable.PrintableEquatableType) = struct module Flat (V : PrettyPrintable.PrintableEquatableType) = struct
type t = Bot | V of V.t | Top type t = Bot | V of V.t | Top
let empty = Bot let bottom = Bot
let is_empty = function Bot -> true | _ -> false let is_bottom = function Bot -> true | _ -> false
let top = Top let top = Top
@ -249,6 +249,10 @@ end
module FiniteSetOfPPSet (S : PrettyPrintable.PPSet) = struct module FiniteSetOfPPSet (S : PrettyPrintable.PPSet) = struct
include S include S
let bottom = empty
let is_bottom = is_empty
let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset lhs rhs let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset lhs rhs
let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else union astate1 astate2 let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else union astate1 astate2
@ -292,6 +296,10 @@ module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
type value = ValueDomain.t type value = ValueDomain.t
let bottom = empty
let is_bottom = is_empty
(** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *) (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *)
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
@ -405,9 +413,9 @@ struct
type t = M.t type t = M.t
let empty = M.empty let bottom = M.empty
let is_empty = M.is_empty let is_bottom = M.is_empty
let ( <= ) = M.( <= ) let ( <= ) = M.( <= )
@ -449,9 +457,9 @@ end
module BooleanOr = struct module BooleanOr = struct
type t = bool type t = bool
let empty = false let bottom = false
let is_empty astate = not astate let is_bottom astate = not astate
let ( <= ) ~lhs ~rhs = (not lhs) || rhs let ( <= ) ~lhs ~rhs = (not lhs) || rhs
@ -474,11 +482,11 @@ module CountDomain (MaxCount : MaxCount) = struct
MaxCount.max MaxCount.max
let empty = 0 let bottom = 0
let is_top = Int.equal top let is_top = Int.equal top
let is_empty = Int.equal empty let is_bottom = Int.equal bottom
let ( <= ) ~lhs ~rhs = lhs <= rhs let ( <= ) ~lhs ~rhs = lhs <= rhs
@ -490,7 +498,7 @@ module CountDomain (MaxCount : MaxCount) = struct
let increment astate = if is_top astate then top else astate + 1 let increment astate = if is_top astate then top else astate + 1
let decrement astate = if is_empty astate then empty else astate - 1 let decrement astate = if is_bottom astate then bottom else astate - 1
let pp = Int.pp let pp = Int.pp
end end

8
infer/src/absint/AbstractDomain.mli
Unescape View File

@ -45,12 +45,10 @@ end
module type WithBottom = sig module type WithBottom = sig
include S include S
val empty : t val bottom : t
(** The bottom value of the domain. (** The bottom value of the domain. *)
Naming it empty instead of bottom helps to bind the empty
value for sets and maps to the natural definition for bottom *)
val is_empty : t -> bool val is_bottom : t -> bool
(** Return true if this is the bottom value *) (** Return true if this is the bottom value *)
end end

8
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -687,7 +687,7 @@ module Alias = struct
AliasRet.pp x.ret AliasRet.pp x.ret
let bot : t = {map= AliasMap.empty; ret= AliasRet.empty} let bot : t = {map= AliasMap.empty; ret= AliasRet.bottom}
let lift_map : (AliasMap.t -> AliasMap.t) -> t -> t = fun f a -> {a with map= f a.map} let lift_map : (AliasMap.t -> AliasMap.t) -> t -> t = fun f a -> {a with map= f a.map}
@ -736,7 +736,7 @@ module CoreVal = struct
let is_symbolic v = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v) let is_symbolic v = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v)
let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) let is_empty v = Itv.is_bottom (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v)
end end
module PruningExp = struct module PruningExp = struct
@ -1143,7 +1143,9 @@ module MemReach = struct
let add_heap : Loc.t -> Val.t -> t -> t = let add_heap : Loc.t -> Val.t -> t -> t =
fun x v m -> fun x v m ->
let v = let v =
let sym = if Itv.is_empty (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in let sym =
if Itv.is_bottom (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x
in
let offset_sym, size_sym = let offset_sym, size_sym =
if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot) if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot)
else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x) else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x)

2
infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
Unescape View File

@ -515,7 +515,7 @@ module Make (Manager : Manager_S) = struct
module Sym = struct module Sym = struct
include AbstractDomain.Flat (Var) include AbstractDomain.Flat (Var)
let bot = empty let bot = bottom
let lift f x = v (f x) let lift f x = v (f x)

4
infer/src/checkers/IdAccessPathMapDomain.ml
Unescape View File

@ -11,6 +11,10 @@ module L = Logging
include (IdMap : module type of IdMap with type 'a t := 'a IdMap.t) include (IdMap : module type of IdMap with type 'a t := 'a IdMap.t)
let bottom = empty
let is_bottom = is_empty
type t = HilExp.AccessExpression.t IdMap.t type t = HilExp.AccessExpression.t IdMap.t
type value = HilExp.AccessExpression.t type value = HilExp.AccessExpression.t

6
infer/src/checkers/SinkTrace.ml
Unescape View File

@ -50,7 +50,7 @@ module Make (TraceElem : TraceElem.S) = struct
type sink_path = Passthroughs.t * (Sink.t * Passthroughs.t) list type sink_path = Passthroughs.t * (Sink.t * Passthroughs.t) list
let empty = let bottom =
let dummy_source = () in let dummy_source = () in
of_source dummy_source of_source dummy_source
@ -70,13 +70,13 @@ module Make (TraceElem : TraceElem.S) = struct
~f:(fun t_acc sink -> ~f:(fun t_acc sink ->
let callee_sink = Sink.with_callsite sink call_site in let callee_sink = Sink.with_callsite sink call_site in
add_sink callee_sink t_acc ) add_sink callee_sink t_acc )
~init:empty ~init:bottom
(Sinks.elements (sinks t)) (Sinks.elements (sinks t))
let of_sink sink = let of_sink sink =
let sinks = Sinks.add sink Sinks.empty in let sinks = Sinks.add sink Sinks.empty in
update_sinks empty sinks update_sinks bottom sinks
let get_reportable_sink_path sink ~trace_of_pname = let get_reportable_sink_path sink ~trace_of_pname =

8
infer/src/checkers/Siof.ml
Unescape View File

@ -113,7 +113,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let add_globals astate loc globals = let add_globals astate loc globals =
if GlobalVarSet.is_empty globals then astate if GlobalVarSet.is_empty globals then astate
else else
let trace = match fst astate with Bottom -> SiofTrace.empty | NonBottom t -> t in let trace = match fst astate with Bottom -> SiofTrace.bottom | NonBottom t -> t in
let is_dangerous = let is_dangerous =
(* filter out variables that are known to be already initialized *) (* filter out variables that are known to be already initialized *)
let initialized = snd astate in let initialized = snd astate in
@ -134,7 +134,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
get_globals pdesc e |> add_globals astate call_loc ) get_globals pdesc e |> add_globals astate call_loc )
let at_least_nonbottom = Domain.join (NonBottom SiofTrace.empty, Domain.VarNames.empty) let at_least_nonbottom = Domain.join (NonBottom SiofTrace.bottom, Domain.VarNames.empty)
let exec_instr astate {ProcData.pdesc} _ (instr : Sil.instr) = let exec_instr astate {ProcData.pdesc} _ (instr : Sil.instr) =
match instr with match instr with
@ -169,7 +169,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
then Some initialized_globals then Some initialized_globals
else None ) else None )
in in
Domain.join astate (NonBottom SiofTrace.empty, Domain.VarNames.of_list init) Domain.join astate (NonBottom SiofTrace.bottom, Domain.VarNames.of_list init)
| Call (_, Const (Cfun (ObjC_Cpp cpp_pname as callee_pname)), _ :: actuals_without_self, loc, _) | Call (_, Const (Cfun (ObjC_Cpp cpp_pname as callee_pname)), _ :: actuals_without_self, loc, _)
when Typ.Procname.is_constructor callee_pname && Typ.Procname.ObjC_Cpp.is_constexpr cpp_pname when Typ.Procname.is_constructor callee_pname && Typ.Procname.ObjC_Cpp.is_constexpr cpp_pname
-> ->
@ -228,7 +228,7 @@ let report_siof summary trace pdesc gname loc =
| Some (NonBottom summary, _) -> | Some (NonBottom summary, _) ->
summary summary
| _ -> | _ ->
SiofTrace.empty SiofTrace.bottom
in in
let report_one_path ((_, path) as trace) = let report_one_path ((_, path) as trace) =
let description = let description =

19
infer/src/checkers/Trace.ml
Unescape View File

@ -58,8 +58,6 @@ module type S = sig
; path_sink: Sink.t ; path_sink: Sink.t
; path_passthroughs: Passthroughs.t } ; path_passthroughs: Passthroughs.t }
val empty : t
val sources : t -> Sources.t val sources : t -> Sources.t
(** get the sources of the trace. *) (** get the sources of the trace. *)
@ -113,9 +111,6 @@ module type S = sig
val append : t -> t -> CallSite.t -> t val append : t -> t -> CallSite.t -> t
(** append the trace for given call site to the current caller trace *) (** append the trace for given call site to the current caller trace *)
val is_empty : t -> bool
(** return true if this trace has no source or sink data *)
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit
val pp_path : Typ.Procname.t -> F.formatter -> path -> unit val pp_path : Typ.Procname.t -> F.formatter -> path -> unit
@ -199,20 +194,20 @@ module Make (Spec : Spec) = struct
F.fprintf fmt " + Sanitizers(%a)" Sanitizers.pp sanitizers F.fprintf fmt " + Sanitizers(%a)" Sanitizers.pp sanitizers
in in
if Known.is_empty known then if Known.is_empty known then
if Footprint.is_empty footprint then F.pp_print_string fmt "{}" if Footprint.is_bottom footprint then F.pp_print_string fmt "{}"
else F.fprintf fmt "Footprint(%a)%a" Footprint.pp footprint pp_sanitizers sanitizers else F.fprintf fmt "Footprint(%a)%a" Footprint.pp footprint pp_sanitizers sanitizers
else else
F.fprintf fmt "%a + Footprint(%a)%a" Known.pp known Footprint.pp footprint pp_sanitizers F.fprintf fmt "%a + Footprint(%a)%a" Known.pp known Footprint.pp footprint pp_sanitizers
sanitizers sanitizers
let empty = {known= Known.empty; footprint= Footprint.empty; sanitizers= Sanitizers.empty} let empty = {known= Known.empty; footprint= Footprint.bottom; sanitizers= Sanitizers.empty}
(* note: empty known/footprint implies empty sanitizers *) (* note: empty known/footprint implies empty sanitizers *)
let is_empty {known; footprint} = Known.is_empty known && Footprint.BaseMap.is_empty footprint let is_empty {known; footprint} = Known.is_empty known && Footprint.is_bottom footprint
let of_footprint access_path = let of_footprint access_path =
let footprint = Footprint.add_trace access_path true Footprint.empty in let footprint = Footprint.add_trace access_path true Footprint.bottom in
{empty with footprint} {empty with footprint}
@ -276,7 +271,7 @@ module Make (Spec : Spec) = struct
let passthroughs t = t.passthroughs let passthroughs t = t.passthroughs
let is_empty t = let is_bottom t =
(* sources empty => sinks empty and passthroughs empty *) (* sources empty => sinks empty and passthroughs empty *)
Sources.is_empty t.sources Sources.is_empty t.sources
@ -497,7 +492,7 @@ module Make (Spec : Spec) = struct
(** compute caller_trace + callee_trace *) (** compute caller_trace + callee_trace *)
let append caller_trace callee_trace callee_site = let append caller_trace callee_trace callee_site =
if is_empty callee_trace then caller_trace if is_bottom callee_trace then caller_trace
else else
let sanitizers = let sanitizers =
Sources.Sanitizers.join callee_trace.sources.sanitizers caller_trace.sources.sanitizers Sources.Sanitizers.join callee_trace.sources.sanitizers caller_trace.sources.sanitizers
@ -544,7 +539,7 @@ module Make (Spec : Spec) = struct
{sources; sinks; passthroughs} {sources; sinks; passthroughs}
let empty = let bottom =
let sources = Sources.empty in let sources = Sources.empty in
let sinks = Sinks.empty in let sinks = Sinks.empty in
let passthroughs = Passthroughs.empty in let passthroughs = Passthroughs.empty in

7
infer/src/checkers/Trace.mli
Unescape View File

@ -23,6 +23,7 @@ end
module type S = sig module type S = sig
include Spec include Spec
(** bottom = this trace has no source or sink data *)
include AbstractDomain.WithBottom include AbstractDomain.WithBottom
module Sources : sig module Sources : sig
@ -66,9 +67,6 @@ module type S = sig
; path_sink: Sink.t ; path_sink: Sink.t
; path_passthroughs: Passthroughs.t } ; path_passthroughs: Passthroughs.t }
val empty : t
(** the empty trace *)
val sources : t -> Sources.t val sources : t -> Sources.t
(** get the sources of the trace. *) (** get the sources of the trace. *)
@ -124,9 +122,6 @@ module type S = sig
val append : t -> t -> CallSite.t -> t val append : t -> t -> CallSite.t -> t
(** append the trace for given call site to the current caller trace *) (** append the trace for given call site to the current caller trace *)
val is_empty : t -> bool
(** return true if this trace has no source or sink data *)
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit
val pp_path : Typ.Procname.t -> F.formatter -> path -> unit val pp_path : Typ.Procname.t -> F.formatter -> path -> unit

4
infer/src/checkers/accessPathDomains.ml
Unescape View File

@ -16,9 +16,9 @@ module Set = struct
let pp = APSet.pp let pp = APSet.pp
let empty = APSet.empty let bottom = APSet.empty
let is_empty = APSet.is_empty let is_bottom = APSet.is_empty
let normalize aps = let normalize aps =
APSet.filter APSet.filter

12
infer/src/checkers/accessTree.ml
Unescape View File

@ -94,13 +94,13 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
type t = node BaseMap.t type t = node BaseMap.t
let empty = BaseMap.empty let bottom = BaseMap.empty
let is_empty = BaseMap.is_empty let is_bottom = BaseMap.is_empty
let make_node trace subtree = (trace, Subtree subtree) let make_node trace subtree = (trace, Subtree subtree)
let empty_node = make_node TraceDomain.empty AccessMap.empty let empty_node = make_node TraceDomain.bottom AccessMap.empty
let is_empty_tree = function Star -> false | Subtree node_map -> AccessMap.is_empty node_map let is_empty_tree = function Star -> false | Subtree node_map -> AccessMap.is_empty node_map
@ -108,9 +108,9 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
let make_starred_leaf trace = (trace, Star) let make_starred_leaf trace = (trace, Star)
let empty_normal_leaf = make_normal_leaf TraceDomain.empty let empty_normal_leaf = make_normal_leaf TraceDomain.bottom
let empty_starred_leaf = make_starred_leaf TraceDomain.empty let empty_starred_leaf = make_starred_leaf TraceDomain.bottom
(* no need to make it tail-recursive, trees shouldn't be big enough to blow up the call stack *) (* no need to make it tail-recursive, trees shouldn't be big enough to blow up the call stack *)
let rec node_depth (_, tree) = 1 + tree_depth tree let rec node_depth (_, tree) = 1 + tree_depth tree
@ -420,7 +420,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
| Star -> | Star ->
F.pp_print_char fmt '*' F.pp_print_char fmt '*'
in in
if not (TraceDomain.is_empty trace) then if not (TraceDomain.is_bottom trace) then
if not (is_empty_tree subtree) then if not (is_empty_tree subtree) then
F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree
else TraceDomain.pp fmt trace else TraceDomain.pp fmt trace

2
infer/src/checkers/classLoads.ml
Unescape View File

@ -134,7 +134,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
(* load the method's class *) (* load the method's class *)
let init = let init =
Typ.Procname.get_class_type_name proc_name Typ.Procname.get_class_type_name proc_name
|> Option.fold ~init:ClassLoadsDomain.empty ~f:(load_class proc_desc tenv loc) |> Option.fold ~init:ClassLoadsDomain.bottom ~f:(load_class proc_desc tenv loc)
in in
let post = Procdesc.fold_instrs proc_desc ~init ~f:(exec_instr proc_desc tenv) in let post = Procdesc.fold_instrs proc_desc ~init ~f:(exec_instr proc_desc tenv) in
report_loads proc_desc summary post ; report_loads proc_desc summary post ;

2
infer/src/checkers/purityDomain.ml
Unescape View File

@ -16,7 +16,7 @@ let contains_global modified_params = ModifiedParamIndices.mem global modified_p
let pure = AbstractDomain.Types.Bottom let pure = AbstractDomain.Types.Bottom
let is_pure = Domain.is_empty let is_pure = Domain.is_bottom
let impure modified_args = AbstractDomain.Types.NonBottom modified_args let impure modified_args = AbstractDomain.Types.NonBottom modified_args

8
infer/src/concurrency/RacerD.ml
Unescape View File

@ -576,7 +576,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
|> List.filter ~f:(fun (_, index) -> not (Int.equal 0 index)) |> List.filter ~f:(fun (_, index) -> not (Int.equal 0 index))
|> List.fold ~init ~f:add_conditional_owned_formal |> List.fold ~init ~f:add_conditional_owned_formal
in in
{RacerDDomain.empty with ownership; threads} {RacerDDomain.bottom with ownership; threads}
else else
(* add Owned(formal_index) predicates for each formal to indicate that each one is owned if (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if
it is owned in the caller *) it is owned in the caller *)
@ -584,7 +584,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
List.fold ~init:own_locals ~f:add_conditional_owned_formal List.fold ~init:own_locals ~f:add_conditional_owned_formal
(FormalMap.get_formals_indexes formal_map) (FormalMap.get_formals_indexes formal_map)
in in
{RacerDDomain.empty with ownership; threads} {RacerDDomain.bottom with ownership; threads}
in in
match Analyzer.compute_post proc_data ~initial with match Analyzer.compute_post proc_data ~initial with
| Some {threads; locks; accesses; ownership; attribute_map} -> | Some {threads; locks; accesses; ownership; attribute_map} ->
@ -730,9 +730,9 @@ let trace_of_pname orig_sink orig_pdesc callee_pname =
if Access.matches ~caller:orig_access ~callee:(PathDomain.Sink.kind snapshot.access) then if Access.matches ~caller:orig_access ~callee:(PathDomain.Sink.kind snapshot.access) then
PathDomain.add_sink snapshot.access acc PathDomain.add_sink snapshot.access acc
else acc ) else acc )
accesses PathDomain.empty accesses PathDomain.bottom
| _ -> | _ ->
PathDomain.empty PathDomain.bottom
let make_trace ~report_kind original_path pdesc = let make_trace ~report_kind original_path pdesc =

20
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -178,7 +178,7 @@ module LocksDomain = struct
not (is_empty astate) not (is_empty astate)
let lookup_count lock astate = try find lock astate with Caml.Not_found -> LockCount.empty let lookup_count lock astate = find_opt lock astate |> Option.value ~default:LockCount.bottom
let acquire_lock astate = let acquire_lock astate =
let count = lookup_count the_only_lock astate in let count = lookup_count the_only_lock astate in
@ -189,7 +189,7 @@ module LocksDomain = struct
let count = lookup_count the_only_lock astate in let count = lookup_count the_only_lock astate in
try try
let count' = LockCount.decrement count in let count' = LockCount.decrement count in
if LockCount.is_empty count' then remove the_only_lock astate if LockCount.is_bottom count' then remove the_only_lock astate
else add the_only_lock count' astate else add the_only_lock count' astate
with Caml.Not_found -> astate with Caml.Not_found -> astate
@ -198,13 +198,13 @@ module LocksDomain = struct
let caller_count = lookup_count the_only_lock caller_astate in let caller_count = lookup_count the_only_lock caller_astate in
let callee_count = lookup_count the_only_lock callee_astate in let callee_count = lookup_count the_only_lock callee_astate in
let sum = LockCount.add caller_count callee_count in let sum = LockCount.add caller_count callee_count in
if LockCount.is_empty sum then caller_astate else add the_only_lock sum caller_astate if LockCount.is_bottom sum then caller_astate else add the_only_lock sum caller_astate
end end
module ThreadsDomain = struct module ThreadsDomain = struct
type t = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare] type t = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare]
let empty = NoThread let bottom = NoThread
(* NoThread < AnyThreadButSelf < Any *) (* NoThread < AnyThreadButSelf < Any *)
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
@ -253,7 +253,7 @@ module ThreadsDomain = struct
match join astate1 astate2 with AnyThread -> true | NoThread | AnyThreadButSelf -> false match join astate1 astate2 with AnyThread -> true | NoThread | AnyThreadButSelf -> false
let is_empty = function NoThread -> true | _ -> false let is_bottom = function NoThread -> true | _ -> false
let is_any_but_self = function AnyThreadButSelf -> true | _ -> false let is_any_but_self = function AnyThreadButSelf -> true | _ -> false
@ -516,8 +516,8 @@ type t =
; ownership: OwnershipDomain.t ; ownership: OwnershipDomain.t
; attribute_map: AttributeMapDomain.t } ; attribute_map: AttributeMapDomain.t }
let empty = let bottom =
let threads = ThreadsDomain.empty in let threads = ThreadsDomain.bottom in
let locks = LocksDomain.empty in let locks = LocksDomain.empty in
let accesses = AccessDomain.empty in let accesses = AccessDomain.empty in
let ownership = OwnershipDomain.empty in let ownership = OwnershipDomain.empty in
@ -525,8 +525,8 @@ let empty =
{threads; locks; accesses; ownership; attribute_map} {threads; locks; accesses; ownership; attribute_map}
let is_empty {threads; locks; accesses; ownership; attribute_map} = let is_bottom {threads; locks; accesses; ownership; attribute_map} =
ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses ThreadsDomain.is_bottom threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses
&& OwnershipDomain.is_empty ownership && OwnershipDomain.is_empty ownership
&& AttributeMapDomain.is_empty attribute_map && AttributeMapDomain.is_empty attribute_map
@ -572,7 +572,7 @@ type summary =
; return_attributes: AttributeSetDomain.t } ; return_attributes: AttributeSetDomain.t }
let empty_summary = let empty_summary =
{ threads= ThreadsDomain.empty { threads= ThreadsDomain.bottom
; locks= LocksDomain.empty ; locks= LocksDomain.empty
; accesses= AccessDomain.empty ; accesses= AccessDomain.empty
; return_ownership= OwnershipAbstractValue.unowned ; return_ownership= OwnershipAbstractValue.unowned

8
infer/src/concurrency/starvation.ml
Unescape View File

@ -146,7 +146,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
let proc_data = ProcData.make proc_desc tenv formals in let proc_data = ProcData.make proc_desc tenv formals in
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
let initial = let initial =
if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.bottom
else else
let lock = let lock =
match pname with match pname with
@ -157,7 +157,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
| _ -> | _ ->
FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, []))
in in
StarvationDomain.acquire tenv StarvationDomain.empty loc (Option.to_list lock) StarvationDomain.acquire tenv StarvationDomain.bottom loc (Option.to_list lock)
in in
let initial = let initial =
ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.proc_resolve_attributes tenv ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.proc_resolve_attributes tenv
@ -399,7 +399,7 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' =
(* for each summary related to the endpoint, analyse and report on its pairs *) (* for each summary related to the endpoint, analyse and report on its pairs *)
fold_reportable_summaries env endpoint_class ~init:report_map fold_reportable_summaries env endpoint_class ~init:report_map
~f:(fun acc (endpoint_pname, {order= endp_order; ui= endp_ui}) -> ~f:(fun acc (endpoint_pname, {order= endp_order; ui= endp_ui}) ->
if UIThreadDomain.is_empty ui || UIThreadDomain.is_empty endp_ui then if UIThreadDomain.is_bottom ui || UIThreadDomain.is_bottom endp_ui then
OrderDomain.fold (report_endpoint_elem elem endpoint_pname) endp_order acc OrderDomain.fold (report_endpoint_elem elem endpoint_pname) endp_order acc
else acc ) ) else acc ) )
in in
@ -471,7 +471,7 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
fold_reportable_summaries env endpoint_class ~init:report_map fold_reportable_summaries env endpoint_class ~init:report_map
~f:(fun acc (endpoint_pname, {order; ui}) -> ~f:(fun acc (endpoint_pname, {order; ui}) ->
(* skip methods on ui thread, as they cannot run in parallel to us *) (* skip methods on ui thread, as they cannot run in parallel to us *)
if UIThreadDomain.is_empty ui then if UIThreadDomain.is_bottom ui then
OrderDomain.fold OrderDomain.fold
(report_remote_block ui_explain event endpoint_lock endpoint_pname) (report_remote_block ui_explain event endpoint_lock endpoint_pname)
order acc order acc

8
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -247,17 +247,17 @@ type t =
; order: OrderDomain.t ; order: OrderDomain.t
; ui: UIThreadDomain.t } ; ui: UIThreadDomain.t }
let empty = let bottom =
{ events= EventDomain.empty { events= EventDomain.empty
; guard_map= GuardToLockMap.empty ; guard_map= GuardToLockMap.empty
; lock_state= LockState.empty ; lock_state= LockState.empty
; order= OrderDomain.empty ; order= OrderDomain.empty
; ui= UIThreadDomain.empty } ; ui= UIThreadDomain.bottom }
let is_empty {events; guard_map; lock_state; order; ui} = let is_bottom {events; guard_map; lock_state; order; ui} =
EventDomain.is_empty events && GuardToLockMap.is_empty guard_map && OrderDomain.is_empty order EventDomain.is_empty events && GuardToLockMap.is_empty guard_map && OrderDomain.is_empty order
&& LockState.is_empty lock_state && UIThreadDomain.is_empty ui && LockState.is_empty lock_state && UIThreadDomain.is_bottom ui
let pp fmt {events; guard_map; lock_state; order; ui} = let pp fmt {events; guard_map; lock_state; order; ui} =

4
infer/src/concurrency/starvationDomain.mli
Unescape View File

@ -59,7 +59,7 @@ end
module OrderDomain : ExplicitTrace.FiniteSet with type elt = Order.t module OrderDomain : ExplicitTrace.FiniteSet with type elt = Order.t
module LockState : AbstractDomain.WithBottom module LockState : AbstractDomain.WithTop
module UIThreadExplanationDomain : sig module UIThreadExplanationDomain : sig
include ExplicitTrace.TraceElem with type elem_t = string include ExplicitTrace.TraceElem with type elem_t = string
@ -71,7 +71,7 @@ module UIThreadDomain :
AbstractDomain.WithBottom AbstractDomain.WithBottom
with type t = UIThreadExplanationDomain.t AbstractDomain.Types.bottom_lifted with type t = UIThreadExplanationDomain.t AbstractDomain.Types.bottom_lifted
module GuardToLockMap : AbstractDomain.WithBottom module GuardToLockMap : AbstractDomain.WithTop
type t = type t =
{ events: EventDomain.t { events: EventDomain.t

24
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -58,7 +58,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
| Some (trace, _) -> | Some (trace, _) ->
trace trace
| None -> | None ->
TraceDomain.empty TraceDomain.bottom
let exp_get_node_ ~abstracted raw_access_path access_tree proc_data = let exp_get_node_ ~abstracted raw_access_path access_tree proc_data =
@ -130,13 +130,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let get_summary pname = let get_summary pname =
if Typ.Procname.equal pname (Procdesc.get_proc_name proc_data.pdesc) then if Typ.Procname.equal pname (Procdesc.get_proc_name proc_data.pdesc) then
(* read_summary will trigger ondemand analysis of the current proc. we don't want that. *) (* read_summary will trigger ondemand analysis of the current proc. we don't want that. *)
TaintDomain.empty TaintDomain.bottom
else else
match Payload.read proc_data.pdesc pname with match Payload.read proc_data.pdesc pname with
| Some summary -> | Some summary ->
TaintSpecification.of_summary_access_tree summary TaintSpecification.of_summary_access_tree summary
| None -> | None ->
TaintDomain.empty TaintDomain.bottom
in in
let get_caller_string caller_site = let get_caller_string caller_site =
let caller_pname = CallSite.pname caller_site in let caller_pname = CallSite.pname caller_site in
@ -333,7 +333,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
match HilExp.ignore_cast exp with match HilExp.ignore_cast exp with
| HilExp.AccessExpression actual_ae_raw | HilExp.AccessExpression actual_ae_raw
when not when not
(TraceDomain.Sources.Footprint.is_empty (TraceDomain.Sources.Footprint.is_bottom
(TraceDomain.sources actual_trace').footprint) -> (TraceDomain.sources actual_trace').footprint) ->
let actual_ap = let actual_ap =
AccessPath.Abs.Abstracted AccessPath.Abs.Abstracted
@ -427,7 +427,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
in in
let trace = instantiate_and_report callee_trace caller_trace access_tree_acc in let trace = instantiate_and_report callee_trace caller_trace access_tree_acc in
let pruned_trace = let pruned_trace =
if TraceDomain.Sources.Footprint.is_empty (TraceDomain.sources trace).footprint then if TraceDomain.Sources.Footprint.is_bottom (TraceDomain.sources trace).footprint then
(* empty footprint; nothing else can flow into these sinks. so don't track them *) (* empty footprint; nothing else can flow into these sinks. so don't track them *)
TraceDomain.update_sinks trace TraceDomain.Sinks.empty TraceDomain.update_sinks trace TraceDomain.Sinks.empty
else trace else trace
@ -552,14 +552,14 @@ module Make (TaintSpecification : TaintSpec.S) = struct
~f:should_taint_typ ~f:should_taint_typ
then TraceDomain.Sources.Footprint.add_trace access_path true acc then TraceDomain.Sources.Footprint.add_trace access_path true acc
else acc ) else acc )
sources.footprint TraceDomain.Sources.Footprint.empty sources.footprint TraceDomain.Sources.Footprint.bottom
in in
let filtered_sources = {sources with footprint= filtered_footprint} in let filtered_sources = {sources with footprint= filtered_footprint} in
if TraceDomain.Sources.is_empty filtered_sources then access_tree if TraceDomain.Sources.is_empty filtered_sources then access_tree
else else
let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in
let pruned_trace = let pruned_trace =
if TraceDomain.Sources.Footprint.is_empty filtered_footprint then if TraceDomain.Sources.Footprint.is_bottom filtered_footprint then
(* empty footprint; nothing else can flow into these sinks. so don't track them *) (* empty footprint; nothing else can flow into these sinks. so don't track them *)
TraceDomain.update_sinks trace' TraceDomain.Sinks.empty TraceDomain.update_sinks trace' TraceDomain.Sinks.empty
else trace' else trace'
@ -742,7 +742,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let passthroughs = passthroughs trace in let passthroughs = passthroughs trace in
let sinks = sinks trace in let sinks = sinks trace in
(* invariant 1: sinks with no footprint sources are dead and should be forgotten *) (* invariant 1: sinks with no footprint sources are dead and should be forgotten *)
if Sources.Footprint.is_empty footprint_sources && not (Sinks.is_empty sinks) then if Sources.Footprint.is_bottom footprint_sources && not (Sinks.is_empty sinks) then
Logging.die InternalError Logging.die InternalError
"Trace %a associated with %a tracks sinks even though no more sources can flow into \ "Trace %a associated with %a tracks sinks even though no more sources can flow into \
them" them"
@ -807,7 +807,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
directly with a formal. In Java this can't happen, so we only care if the formal flows to directly with a formal. In Java this can't happen, so we only care if the formal flows to
a sink *) a sink *)
( if is_java then TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) ( if is_java then TraceDomain.Sinks.is_empty (TraceDomain.sinks trace)
else TraceDomain.is_empty trace ) else TraceDomain.is_bottom trace )
&& &&
match tree with match tree with
| TaintDomain.Subtree subtree -> | TaintDomain.Subtree subtree ->
@ -827,7 +827,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
else else
let node' = let node' =
if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) then if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) then
(TraceDomain.empty, subtree) (TraceDomain.bottom, subtree)
else node else node
in in
AccessPath.BaseMap.add base node' acc AccessPath.BaseMap.add base node' acc
@ -844,7 +844,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
| None -> | None ->
(* base is a local var *) (* base is a local var *)
acc ) acc )
access_tree' TaintDomain.empty access_tree' TaintDomain.bottom
in in
if Config.developer_mode then check_invariants with_footprint_vars ; if Config.developer_mode then check_invariants with_footprint_vars ;
TaintSpecification.to_summary_access_tree with_footprint_vars TaintSpecification.to_summary_access_tree with_footprint_vars
@ -864,7 +864,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc
| None -> | None ->
acc ) acc )
~init:TaintDomain.empty ~init:TaintDomain.bottom
(TraceDomain.Source.get_tainted_formals pdesc tenv) (TraceDomain.Source.get_tainted_formals pdesc tenv)
in in
let initial = make_initial proc_desc in let initial = make_initial proc_desc in

4
infer/src/unit/TaintTests.ml
Unescape View File

@ -89,7 +89,7 @@ let tests =
(* flatten access tree into list of access paths with associated traces *) (* flatten access tree into list of access paths with associated traces *)
let trace_assocs = let trace_assocs =
MockTaintAnalysis.TaintDomain.trace_fold MockTaintAnalysis.TaintDomain.trace_fold
(fun acc ap t -> if not (MockTrace.is_empty t) then (ap, t) :: acc else acc) (fun acc ap t -> if not (MockTrace.is_bottom t) then (ap, t) :: acc else acc)
(fst astate) [] (fst astate) []
in in
PrettyPrintable.pp_collection ~pp_item fmt (List.rev trace_assocs) PrettyPrintable.pp_collection ~pp_item fmt (List.rev trace_assocs)
@ -157,6 +157,6 @@ let tests =
, [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ] , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ]
|> TestInterpreter.create_tests ~pp_opt:pp_sparse |> TestInterpreter.create_tests ~pp_opt:pp_sparse
{formal_map= FormalMap.empty; summary= Summary.dummy} {formal_map= FormalMap.empty; summary= Summary.dummy}
~initial:(MockTaintAnalysis.Domain.empty, Bindings.empty) ~initial:(MockTaintAnalysis.Domain.bottom, Bindings.empty)
in in
"taint_test_suite" >::: test_list "taint_test_suite" >::: test_list

18
infer/src/unit/accessTreeTests.ml
Unescape View File

@ -229,7 +229,7 @@ let tests =
|> Domain.BaseMap.singleton x_base |> Domain.BaseMap.singleton x_base
in in
Domain.assert_trees_equal Domain.assert_trees_equal
(Domain.add_trace xF_star added_trace Domain.empty) (Domain.add_trace xF_star added_trace Domain.bottom)
xF_star_tree_added_trace ; xF_star_tree_added_trace ;
(* add starred path when base present *) (* add starred path when base present *)
Domain.assert_trees_equal Domain.assert_trees_equal
@ -421,7 +421,7 @@ let tests =
in in
let depth_test = let depth_test =
let depth_test_ _ = let depth_test_ _ =
assert_equal (Domain.depth Domain.empty) 0 ; assert_equal (Domain.depth Domain.bottom) 0 ;
assert_equal (Domain.depth x_base_tree) 1 ; assert_equal (Domain.depth x_base_tree) 1 ;
assert_equal (Domain.depth x_y_base_tree) 1 ; assert_equal (Domain.depth x_y_base_tree) 1 ;
assert_equal (Domain.depth xFG_tree) 3 ; assert_equal (Domain.depth xFG_tree) 3 ;
@ -445,13 +445,13 @@ let tests =
let x_tree = Max1.BaseMap.singleton x_base (Max1.make_normal_leaf x_trace) in let x_tree = Max1.BaseMap.singleton x_base (Max1.make_normal_leaf x_trace) in
let x_star_tree = Max1.BaseMap.singleton x_base (Max1.make_starred_leaf x_trace) in let x_star_tree = Max1.BaseMap.singleton x_base (Max1.make_starred_leaf x_trace) in
(* adding (x.f, "x") to a tree with max height 1 should yield x |-> ("x", * ) *) (* adding (x.f, "x") to a tree with max height 1 should yield x |-> ("x", * ) *)
Max1.assert_trees_equal (Max1.add_trace xF x_trace Max1.empty) x_star_tree ; Max1.assert_trees_equal (Max1.add_trace xF x_trace Max1.bottom) x_star_tree ;
(* same, but with (x.f.g, "x") *) (* same, but with (x.f.g, "x") *)
Max1.assert_trees_equal (Max1.add_trace xFG x_trace Max1.empty) x_star_tree ; Max1.assert_trees_equal (Max1.add_trace xFG x_trace Max1.bottom) x_star_tree ;
(* adding node (f, "x") via access path x should also yield the same tree *) (* adding node (f, "x") via access path x should also yield the same tree *)
Max1.assert_trees_equal (Max1.add_node x f_node Max1.empty) x_star_tree ; Max1.assert_trees_equal (Max1.add_node x f_node Max1.bottom) x_star_tree ;
(* adding (x, "x") shouldn't add stars *) (* adding (x, "x") shouldn't add stars *)
Max1.assert_trees_equal (Max1.add_trace x x_trace Max1.empty) x_tree ; Max1.assert_trees_equal (Max1.add_trace x x_trace Max1.bottom) x_tree ;
let module Max2 = MakeTree (struct let module Max2 = MakeTree (struct
let max_depth = 2 let max_depth = 2
@ -474,9 +474,9 @@ let tests =
let xF_tree = Max2.BaseMap.singleton x_base f_node in let xF_tree = Max2.BaseMap.singleton x_base f_node in
let xF_star_tree = Max2.BaseMap.singleton x_base f_star_node in let xF_star_tree = Max2.BaseMap.singleton x_base f_star_node in
(* adding x.f to an empty tree should't add stars... *) (* adding x.f to an empty tree should't add stars... *)
Max2.assert_trees_equal (Max2.add_trace xF x_trace Max2.empty) xF_tree ; Max2.assert_trees_equal (Max2.add_trace xF x_trace Max2.bottom) xF_tree ;
(* ... but adding x.f.g should *) (* ... but adding x.f.g should *)
Max2.assert_trees_equal (Max2.add_trace xFG x_trace Max2.empty) xF_star_tree ; Max2.assert_trees_equal (Max2.add_trace xFG x_trace Max2.bottom) xF_star_tree ;
(* adding the node (f.g, "x") to a tree with x should produce the same result *) (* adding the node (f.g, "x") to a tree with x should produce the same result *)
Max2.assert_trees_equal (Max2.add_node x fG_node x_tree) xF_star_tree Max2.assert_trees_equal (Max2.add_node x fG_node x_tree) xF_star_tree
in in
@ -505,7 +505,7 @@ let tests =
let xG_tree = Max1.BaseMap.singleton x_base g_node in let xG_tree = Max1.BaseMap.singleton x_base g_node in
let x_star_tree = Max1.BaseMap.singleton x_base star_node in let x_star_tree = Max1.BaseMap.singleton x_base star_node in
(* adding x.f to a tree containing just x should work *) (* adding x.f to a tree containing just x should work *)
Max1.assert_trees_equal (Max1.add_trace xF y_trace Max1.empty) xF_tree ; Max1.assert_trees_equal (Max1.add_trace xF y_trace Max1.bottom) xF_tree ;
(* but adding x.g to a tree containing x.f should create a star *) (* but adding x.g to a tree containing x.f should create a star *)
Max1.assert_trees_equal (Max1.add_trace xG z_trace xF_tree) x_star_tree ; Max1.assert_trees_equal (Max1.add_trace xG z_trace xF_tree) x_star_tree ;
(* joining the x.f and x.g trees should also create a star *) (* joining the x.f and x.g trees should also create a star *)

Write Preview
Loading…
Cancel
Save