diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index ce49ae98c..c9df8e69b 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -97,7 +97,7 @@ type global_state = ; name_generator: Ident.NameGenerator.t ; proc_analysis_time: (Mtime.Span.t * string) option (** the time elapsed doing [status] so far *) - ; pulse_address_generator: PulseDomain.AbstractAddress.state + ; pulse_address_generator: PulseAbstractValue.state ; symexec_state: State.t } let save_global_state () = @@ -112,7 +112,7 @@ let save_global_state () = ; proc_analysis_time= Option.map !current_taskbar_status ~f:(fun (t0, status) -> (Mtime.span t0 (Mtime_clock.now ()), status) ) - ; pulse_address_generator= PulseDomain.AbstractAddress.get_state () + ; pulse_address_generator= PulseAbstractValue.get_state () ; symexec_state= State.save_state () } @@ -123,7 +123,7 @@ let restore_global_state st = BiabductionConfig.footprint := st.footprint_mode ; Printer.curr_html_formatter := st.html_formatter ; Ident.NameGenerator.set_current st.name_generator ; - PulseDomain.AbstractAddress.set_state st.pulse_address_generator ; + PulseAbstractValue.set_state st.pulse_address_generator ; State.restore_state st.symexec_state ; current_taskbar_status := Option.map st.proc_analysis_time ~f:(fun (suspended_span, status) -> diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index a75184a92..4720e8405 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -7,7 +7,6 @@ open! IStd module F = Format module L = Logging -module AbstractAddress = PulseDomain.AbstractAddress module BaseStack = PulseDomain.Stack open PulseBasicInterface @@ -16,11 +15,11 @@ let debug fmt = L.(debug Analysis Verbose fmt) (* An impurity analysis that relies on pulse to determine how the state changes *) -let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractAddress.t list option = +let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list option = match List.fold2 ~init:(Some []) ~f:(fun acc (_, (addr_dest_pre, _)) (_, (addr_dest_post, _)) -> - if AbstractAddress.equal addr_dest_pre addr_dest_post then + if AbstractValue.equal addr_dest_pre addr_dest_post then Option.map acc ~f:(fun acc -> addr_dest_pre :: acc) else None ) (PulseDomain.Memory.Edges.bindings edges_pre) @@ -62,11 +61,11 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t = | [] -> acc | addr :: addr_to_explore -> ( - if PulseDomain.AbstractAddressSet.mem addr visited then aux acc ~addr_to_explore ~visited + if AbstractValue.Set.mem addr visited then aux acc ~addr_to_explore ~visited else let cell_pre_opt = PulseDomain.Memory.find_opt addr pre_heap in let cell_post_opt = PulseDomain.Memory.find_opt addr post_heap in - let visited = PulseDomain.AbstractAddressSet.add addr visited in + let visited = AbstractValue.Set.add addr visited in match (cell_pre_opt, cell_post_opt) with | None, None -> aux acc ~addr_to_explore ~visited @@ -88,7 +87,7 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t = (add_invalid_and_modified ~check_empty:true attrs_post acc) ~addr_to_explore ~visited ) ) in - match aux [] ~addr_to_explore:[addr] ~visited:PulseDomain.AbstractAddressSet.empty with + match aux [] ~addr_to_explore:[addr] ~visited:AbstractValue.Set.empty with | [] -> acc | hd :: tl -> diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index c9620004b..bc9ab9de2 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -8,7 +8,6 @@ open! IStd module F = Format module L = Logging open Result.Monad_infix -module AbstractAddress = PulseDomain.AbstractAddress open PulseBasicInterface include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) @@ -218,7 +217,7 @@ module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFun let checker {Callbacks.exe_env; summary} = let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in let proc_data = ProcData.make summary tenv () in - AbstractAddress.init () ; + AbstractValue.init () ; let pdesc = Summary.get_proc_desc summary in let initial = DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial pdesc) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 9f45e4618..e8b74a62b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -7,7 +7,6 @@ open! IStd module F = Format module L = Logging -module AbstractAddress = PulseDomain.AbstractAddress module BaseStack = PulseDomain.Stack module BaseMemory = PulseDomain.Memory open PulseBasicInterface @@ -102,7 +101,7 @@ module Stack = struct | Some addr_hist -> (astate, addr_hist) | None -> - let addr = AbstractAddress.mk_fresh () in + let addr = AbstractValue.mk_fresh () in let addr_hist = (addr, origin) in let post_stack = BaseStack.add var addr_hist (astate.post :> base_domain).stack in let pre = @@ -182,7 +181,7 @@ module Memory = struct | Some addr_hist_dst -> (astate, addr_hist_dst) | None -> - let addr_dst = AbstractAddress.mk_fresh () in + let addr_dst = AbstractValue.mk_fresh () in let addr_hist_dst = (addr_dst, hist_src) in let post_heap = BaseMemory.add_edge addr_src access addr_hist_dst (astate.post :> base_domain).heap @@ -243,7 +242,7 @@ let mk_initial proc_desc = |> List.map ~f:(fun (mangled, _) -> let pvar = Pvar.mk mangled proc_name in ( Var.of_pvar pvar - , (AbstractAddress.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) ) + , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) ) in let initial_stack = List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack @@ -264,17 +263,13 @@ let discard_unreachable ({pre; post} as astate) = let pre_addresses = PulseDomain.reachable_addresses (pre :> PulseDomain.t) in let pre_old_heap = (pre :> PulseDomain.t).heap in let pre_new_heap = - BaseMemory.filter - (fun address -> PulseDomain.AbstractAddressSet.mem address pre_addresses) - pre_old_heap + BaseMemory.filter (fun address -> AbstractValue.Set.mem address pre_addresses) pre_old_heap in let post_addresses = PulseDomain.reachable_addresses (post :> PulseDomain.t) in - let all_addresses = PulseDomain.AbstractAddressSet.union pre_addresses post_addresses in + let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in let post_old_heap = (post :> PulseDomain.t).heap in let post_new_heap = - BaseMemory.filter - (fun address -> PulseDomain.AbstractAddressSet.mem address all_addresses) - post_old_heap + BaseMemory.filter (fun address -> AbstractValue.Set.mem address all_addresses) post_old_heap in if phys_equal pre_new_heap pre_old_heap && phys_equal post_new_heap post_old_heap then astate else @@ -345,8 +340,8 @@ module PrePost = struct (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call to the current state} *) - module AddressSet = PulseDomain.AbstractAddressSet - module AddressMap = PulseDomain.AbstractAddressMap + module AddressSet = AbstractValue.Set + module AddressMap = AbstractValue.Map (** raised when the pre/post pair and the current state disagree on the aliasing, i.e. some addresses that are distinct in the pre/post are aliased in the current state. Typically raised @@ -356,9 +351,9 @@ module PrePost = struct (** stuff we carry around when computing the result of applying one pre/post pair *) type call_state = { astate: t (** caller's abstract state computed so far *) - ; subst: (AbstractAddress.t * ValueHistory.t) AddressMap.t + ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t (** translation from callee addresses to caller addresses and their caller histories *) - ; rev_subst: AbstractAddress.t AddressMap.t + ; rev_subst: AbstractValue.t AddressMap.t (** the inverse translation from [subst] from caller addresses to callee addresses *) ; visited: AddressSet.t (** set of callee addresses that have been visited already @@ -373,9 +368,9 @@ module PrePost = struct "@[{ astate=@[%a@];@, subst=@[%a@];@, rev_subst=@[%a@];@, \ visited=@[%a@]@, }@]" pp astate - (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractAddress.pp fmt addr)) + (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) subst - (AddressMap.pp ~pp_value:AbstractAddress.pp) + (AddressMap.pp ~pp_value:AbstractValue.pp) rev_subst AddressSet.pp visited @@ -399,10 +394,10 @@ module PrePost = struct let visit call_state ~addr_callee ~addr_hist_caller = let addr_caller = fst addr_hist_caller in ( match AddressMap.find_opt addr_caller call_state.rev_subst with - | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') -> + | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') -> L.d_printfln "Huho, address %a in post already bound to %a, not %a@\nState=%a" - AbstractAddress.pp addr_caller AbstractAddress.pp addr_callee' AbstractAddress.pp - addr_callee pp_call_state call_state ; + AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee + pp_call_state call_state ; raise Aliasing | _ -> () ) ; @@ -466,7 +461,7 @@ module PrePost = struct has been instantiated with the corresponding [actual] into the current state [call_state.astate] *) let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = - L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp (fst actual) ; + L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ; (let open Option.Monad_infix in BaseStack.find_opt formal pre.PulseDomain.stack >>= fun (addr_formal_pre, _) -> @@ -489,7 +484,7 @@ module PrePost = struct TODO: can the traces be leveraged here? maybe easy to detect writes by looking at the post trace *) - AbstractAddress.equal addr_dest_pre addr_dest_post ) + AbstractValue.equal addr_dest_pre addr_dest_post ) edges_pre edges_post in if CommandLineOption.strict_mode then assert are_edges_equal ; @@ -544,7 +539,7 @@ module PrePost = struct let subst_find_or_new subst addr_callee ~default_hist_caller = match AddressMap.find_opt addr_callee subst with | None -> - let addr_hist_fresh = (AbstractAddress.mk_fresh (), default_hist_caller) in + let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) | Some addr_hist_caller -> (subst, addr_hist_caller) @@ -655,7 +650,7 @@ module PrePost = struct let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee ~addr_hist_caller call_state = - L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp (fst addr_hist_caller) ; + L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ; match visit call_state ~addr_callee ~addr_hist_caller with | `AlreadyVisited, call_state -> call_state @@ -685,7 +680,7 @@ module PrePost = struct let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = - L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp + L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp (fst actual) ; match let open Option.Monad_infix in @@ -721,7 +716,7 @@ module PrePost = struct | Some return_caller_hist -> return_caller_hist | None -> - ( AbstractAddress.mk_fresh () + ( AbstractValue.mk_fresh () , [ (* this could maybe include an event like "returned here" *) ] ) in let call_state = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 1d87d09df..3f08677d0 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -5,7 +5,6 @@ * LICENSE file in the root directory of this source tree. *) open! IStd -module AbstractAddress = PulseDomain.AbstractAddress open PulseBasicInterface (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition @@ -43,39 +42,39 @@ module Memory : sig module Access = PulseDomain.Memory.Access module Edges = PulseDomain.Memory.Edges - val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t + val add_attribute : AbstractValue.t -> Attribute.t -> t -> t val add_edge : - AbstractAddress.t * ValueHistory.t + AbstractValue.t * ValueHistory.t -> Access.t -> PulseDomain.AddrTracePair.t -> Location.t -> t -> t - val check_valid : unit Trace.t -> AbstractAddress.t -> t -> (t, Invalidation.t Trace.t) result + val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result - val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option + val find_opt : AbstractValue.t -> t -> PulseDomain.Memory.cell option - val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option + val find_edge_opt : AbstractValue.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option val set_cell : - AbstractAddress.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t + AbstractValue.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t - val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option - val is_std_vector_reserved : AbstractAddress.t -> t -> bool + val is_std_vector_reserved : AbstractValue.t -> t -> bool - val std_vector_reserve : AbstractAddress.t -> t -> t + val std_vector_reserve : AbstractValue.t -> t -> t val eval_edge : - AbstractAddress.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t + AbstractValue.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and returns what it points to or creates a fresh value if that edge didn't exist. *) - val get_constant : AbstractAddress.t -> t -> Const.t option + val get_constant : AbstractValue.t -> t -> Const.t option end val is_local : Var.t -> t -> bool @@ -94,9 +93,9 @@ module PrePost : sig -> Location.t -> t -> formals:Var.t list - -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> domain_t - -> (domain_t * (AbstractAddress.t * ValueHistory.t) option, PulseDiagnostic.t) result + -> (domain_t * (AbstractValue.t * ValueHistory.t) option, PulseDiagnostic.t) result (** return the abstract state after the call along with an optional return value *) end diff --git a/infer/src/pulse/PulseAbstractValue.ml b/infer/src/pulse/PulseAbstractValue.ml new file mode 100644 index 000000000..56b5d9c78 --- /dev/null +++ b/infer/src/pulse/PulseAbstractValue.ml @@ -0,0 +1,40 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd +module F = Format + +type t = int [@@deriving compare] + +let equal = [%compare.equal: t] + +let next_fresh = ref 1 + +let mk_fresh () = + let l = !next_fresh in + incr next_fresh ; l + + +let pp f l = F.fprintf f "v%d" l + +let init () = next_fresh := 1 + +type state = int + +let get_state () = !next_fresh + +let set_state counter = next_fresh := counter + +module PPKey = struct + type nonrec t = t + + let compare = compare + + let pp = pp +end + +module Set = PrettyPrintable.MakePPSet (PPKey) +module Map = PrettyPrintable.MakePPMap (PPKey) diff --git a/infer/src/pulse/PulseAbstractValue.mli b/infer/src/pulse/PulseAbstractValue.mli new file mode 100644 index 000000000..30a13c3ac --- /dev/null +++ b/infer/src/pulse/PulseAbstractValue.mli @@ -0,0 +1,30 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd +module F = Format + +(** An abstract value, eg an address in memory. *) + +type t = private int [@@deriving compare] + +val equal : t -> t -> bool + +val mk_fresh : unit -> t + +val pp : F.formatter -> t -> unit + +val init : unit -> unit + +type state + +val get_state : unit -> state + +val set_state : state -> unit + +module Set : PrettyPrintable.PPSet with type elt = t + +module Map : PrettyPrintable.PPMap with type key = t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 0dd6c70b2..6133f322e 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -10,18 +10,18 @@ module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory -(** Make sure we don't depend on {!AbstractAddress} to avoid attributes depending on - addresses. Otherwise they become a pain to handle when comparing memory states. +(** Make sure we don't depend on {!AbstractValue} to avoid attributes depending on + values. Otherwise they become a pain to handle when comparing memory states. - If you find you need to make attributes depend on {!AbstractAddress} then remember to modify + If you find you need to make attributes depend on {!AbstractValue} then remember to modify graph operations of {!PulseDomain} and the interprocedural operations in {!PulseAbductiveDomain} *) include struct [@@@warning "-60"] - module AbstractAddress = struct end + module AbstractValue = struct end - module PulseAbstractAddress = struct end + module PulseAbstractValue = struct end end module Attribute = struct diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 2fc6f5e52..e865d95a4 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -8,6 +8,7 @@ open! IStd (** Basic Pulse modules that are safe to use in any module *) +module AbstractValue = PulseAbstractValue module Attribute = PulseAttribute module Attributes = PulseAttribute.Attributes module CallEvent = PulseCallEvent diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index c072f80a9..95445d61a 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -11,63 +11,20 @@ open PulseBasicInterface (* {2 Abstract domain description } *) -(** An abstract address in memory. *) -module AbstractAddress : sig - type t = private int [@@deriving compare] - - val equal : t -> t -> bool - - val mk_fresh : unit -> t - - val pp : F.formatter -> t -> unit - - val init : unit -> unit - - type state - - val get_state : unit -> state - - val set_state : state -> unit -end = struct - type t = int [@@deriving compare] - - let equal = [%compare.equal: t] - - let next_fresh = ref 1 - - let mk_fresh () = - let l = !next_fresh in - incr next_fresh ; l - - - let pp f l = F.fprintf f "v%d" l - - let init () = next_fresh := 1 - - type state = int - - let get_state () = !next_fresh - - let set_state counter = next_fresh := counter -end - -module AbstractAddressSet = PrettyPrintable.MakePPSet (AbstractAddress) -module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress) - (* {3 Heap domain } *) module AddrTracePair = struct - type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] + type t = AbstractValue.t * ValueHistory.t [@@deriving compare] let pp f addr_trace = if Config.debug_level_analysis >= 3 then - Pp.pair ~fst:AbstractAddress.pp ~snd:ValueHistory.pp f addr_trace - else AbstractAddress.pp f (fst addr_trace) + Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace + else AbstractValue.pp f (fst addr_trace) end module Memory : sig module Access : sig - include PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t + include PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t val equal : t -> t -> bool end @@ -84,54 +41,54 @@ module Memory : sig val empty : t - val filter : (AbstractAddress.t -> bool) -> t -> t + val filter : (AbstractValue.t -> bool) -> t -> t - val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t + val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t - val find_opt : AbstractAddress.t -> t -> cell option + val find_opt : AbstractValue.t -> t -> cell option - val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc - val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t + val set_attrs : AbstractValue.t -> Attributes.t -> t -> t - val set_edges : AbstractAddress.t -> edges -> t -> t + val set_edges : AbstractValue.t -> edges -> t -> t - val set_cell : AbstractAddress.t -> cell -> t -> t + val set_cell : AbstractValue.t -> cell -> t -> t - val find_edges_opt : AbstractAddress.t -> t -> edges option + val find_edges_opt : AbstractValue.t -> t -> edges option - val mem_edges : AbstractAddress.t -> t -> bool + val mem_edges : AbstractValue.t -> t -> bool val pp_heap : F.formatter -> t -> unit val pp_attributes : F.formatter -> t -> unit - val register_address : AbstractAddress.t -> t -> t + val register_address : AbstractValue.t -> t -> t - val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t + val add_edge : AbstractValue.t -> Access.t -> AddrTracePair.t -> t -> t - val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option + val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrTracePair.t option - val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t + val add_attribute : AbstractValue.t -> Attribute.t -> t -> t - val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result + val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result - val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option - val get_constant : AbstractAddress.t -> t -> Const.t option + val get_constant : AbstractValue.t -> t -> Const.t option - val std_vector_reserve : AbstractAddress.t -> t -> t + val std_vector_reserve : AbstractValue.t -> t -> t - val is_std_vector_reserved : AbstractAddress.t -> t -> bool + val is_std_vector_reserved : AbstractValue.t -> t -> bool end = struct module Access = struct - type t = AbstractAddress.t HilExp.Access.t [@@deriving compare] + type t = AbstractValue.t HilExp.Access.t [@@deriving compare] let equal = [%compare.equal: t] - let pp = HilExp.Access.pp AbstractAddress.pp + let pp = HilExp.Access.pp AbstractValue.pp end module Edges = PrettyPrintable.MakePPMap (Access) @@ -142,7 +99,7 @@ end = struct type cell = edges * Attributes.t - module Graph = PrettyPrintable.MakePPMap (AbstractAddress) + module Graph = PrettyPrintable.MakePPMap (AbstractValue) type t = edges Graph.t * Attributes.t Graph.t @@ -184,7 +141,7 @@ end = struct let check_valid address memory = - L.d_printfln "Checking validity of %a" AbstractAddress.pp address ; + L.d_printfln "Checking validity of %a" AbstractValue.pp address ; match Graph.find_opt address (snd memory) |> Option.bind ~f:Attributes.get_invalid with | Some invalidation -> Error invalidation @@ -295,20 +252,20 @@ let empty = [rhs_to_lhs]) between the addresses of [lhs] and [rhs] such that [lhs_to_rhs(reachable(lhs)) = reachable(rhs)] (where addresses are reachable if they are reachable from stack variables). *) module GraphComparison = struct - module AddressMap = PrettyPrintable.MakePPMap (AbstractAddress) + module AddressMap = PrettyPrintable.MakePPMap (AbstractValue) (** translation between the abstract values on the LHS and the ones on the RHS *) type mapping = - { rhs_to_lhs: AbstractAddress.t AddressMap.t (** map from RHS values to LHS *) - ; lhs_to_rhs: AbstractAddress.t AddressMap.t (** inverse map from [rhs_to_lhs] *) } + { rhs_to_lhs: AbstractValue.t AddressMap.t (** map from RHS values to LHS *) + ; lhs_to_rhs: AbstractValue.t AddressMap.t (** inverse map from [rhs_to_lhs] *) } let empty_mapping = {rhs_to_lhs= AddressMap.empty; lhs_to_rhs= AddressMap.empty} let pp_mapping fmt {rhs_to_lhs; lhs_to_rhs} = F.fprintf fmt "@[{ rhs_to_lhs=@[%a@];@,lhs_to_rhs=@[%a@];@,}@]" - (AddressMap.pp ~pp_value:AbstractAddress.pp) + (AddressMap.pp ~pp_value:AbstractValue.pp) rhs_to_lhs - (AddressMap.pp ~pp_value:AbstractAddress.pp) + (AddressMap.pp ~pp_value:AbstractValue.pp) lhs_to_rhs @@ -316,13 +273,13 @@ module GraphComparison = struct let record_equal ~addr_lhs ~addr_rhs mapping = (* have we seen [addr_lhs] before?.. *) match AddressMap.find_opt addr_lhs mapping.lhs_to_rhs with - | Some addr_rhs' when not (AbstractAddress.equal addr_rhs addr_rhs') -> + | Some addr_rhs' when not (AbstractValue.equal addr_rhs addr_rhs') -> (* ...yes, but it was bound to another address *) L.d_printfln "Aliasing in LHS not in RHS: LHS address %a in current already bound to %a, not %a@\n\ State=%a" - AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs' AbstractAddress.pp addr_rhs - pp_mapping mapping ; + AbstractValue.pp addr_lhs AbstractValue.pp addr_rhs' AbstractValue.pp addr_rhs pp_mapping + mapping ; `AliasingLHS | Some _addr_rhs (* [_addr_rhs = addr_rhs] *) -> `AlreadyVisited @@ -335,7 +292,7 @@ module GraphComparison = struct L.d_printfln "Aliasing in RHS not in LHS: RHS address %a in current already bound to %a, not %a@\n\ State=%a" - AbstractAddress.pp addr_rhs AbstractAddress.pp addr_lhs' AbstractAddress.pp addr_lhs + AbstractValue.pp addr_rhs AbstractValue.pp addr_lhs' AbstractValue.pp addr_lhs pp_mapping mapping ; `AliasingRHS | None -> @@ -354,7 +311,7 @@ module GraphComparison = struct (** can we extend [mapping] so that the subgraph of [lhs] rooted at [addr_lhs] is isomorphic to the subgraph of [rhs] rooted at [addr_rhs]? *) let rec isograph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping = - L.d_printfln "%a<->%a@\n" AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs ; + L.d_printfln "%a<->%a@\n" AbstractValue.pp addr_lhs AbstractValue.pp addr_rhs ; match record_equal mapping ~addr_lhs ~addr_rhs with | `AlreadyVisited -> IsomorphicUpTo mapping @@ -449,12 +406,12 @@ module GraphVisit : sig -> t -> init:'accum -> f:( 'accum - -> AbstractAddress.t + -> AbstractValue.t -> Var.t -> Memory.Access.t list -> ('accum, 'final) Base.Continue_or_stop.t) -> finish:('accum -> 'final) - -> AbstractAddressSet.t * 'final + -> AbstractValue.Set.t * 'final (** Generic graph traversal of the memory starting from each variable in the stack that pass [var_filter], in order. Returns the result of folding over every address in the graph and the set of addresses that have been visited before [f] returned [Stop] or all reachable addresses @@ -464,9 +421,9 @@ end = struct open Base.Continue_or_stop let visit address visited = - if AbstractAddressSet.mem address visited then `AlreadyVisited + if AbstractValue.Set.mem address visited then `AlreadyVisited else - let visited = AbstractAddressSet.add address visited in + let visited = AbstractValue.Set.add address visited in `NotAlreadyVisited visited @@ -501,7 +458,7 @@ end = struct let fold ~var_filter astate ~init ~f ~finish = let finish (visited, accum) = (visited, finish accum) in - let init = (AbstractAddressSet.empty, init) in + let init = (AbstractValue.Set.empty, init) in Container.fold_until astate.stack ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) ~init ~finish ~f:(fun visited_accum (var, (address, _loc)) -> diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index f4d211175..56f7563ae 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -9,30 +9,8 @@ open! IStd module F = Format open PulseBasicInterface -module AbstractAddress : sig - type t = private int [@@deriving compare] - - val equal : t -> t -> bool - - val init : unit -> unit - - val pp : F.formatter -> t -> unit [@@warning "-32"] - - val mk_fresh : unit -> t - - type state - - val get_state : unit -> state - - val set_state : state -> unit -end - -module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddress.t - -module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t - module AddrTracePair : sig - type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] + type t = AbstractValue.t * ValueHistory.t [@@deriving compare] end module Stack : sig @@ -45,7 +23,7 @@ end module Memory : sig module Access : - PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t + PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t module Edges : PrettyPrintable.PPMap with type key = Access.t @@ -57,43 +35,43 @@ module Memory : sig type t - val filter : (AbstractAddress.t -> bool) -> t -> t + val filter : (AbstractValue.t -> bool) -> t -> t - val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t + val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t - val find_opt : AbstractAddress.t -> t -> cell option + val find_opt : AbstractValue.t -> t -> cell option - val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc - val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t + val set_attrs : AbstractValue.t -> Attributes.t -> t -> t - val set_edges : AbstractAddress.t -> edges -> t -> t + val set_edges : AbstractValue.t -> edges -> t -> t - val set_cell : AbstractAddress.t -> cell -> t -> t + val set_cell : AbstractValue.t -> cell -> t -> t - val find_edges_opt : AbstractAddress.t -> t -> edges option + val find_edges_opt : AbstractValue.t -> t -> edges option - val mem_edges : AbstractAddress.t -> t -> bool + val mem_edges : AbstractValue.t -> t -> bool - val register_address : AbstractAddress.t -> t -> t + val register_address : AbstractValue.t -> t -> t - val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t + val add_edge : AbstractValue.t -> Access.t -> AddrTracePair.t -> t -> t - val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option + val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrTracePair.t option - val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t + val add_attribute : AbstractValue.t -> Attribute.t -> t -> t - val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result + val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result - val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option - val get_constant : AbstractAddress.t -> t -> Const.t option + val get_constant : AbstractValue.t -> t -> Const.t option - val std_vector_reserve : AbstractAddress.t -> t -> t + val std_vector_reserve : AbstractValue.t -> t -> t - val is_std_vector_reserved : AbstractAddress.t -> t -> bool + val is_std_vector_reserved : AbstractValue.t -> t -> bool end type t = {heap: Memory.t; stack: Stack.t} @@ -102,7 +80,7 @@ val empty : t include AbstractDomain.NoJoin with type t := t -val reachable_addresses : t -> AbstractAddressSet.t +val reachable_addresses : t -> AbstractValue.Set.t (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from the stack variables *) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c8132323c..91f8e5168 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -6,7 +6,6 @@ *) open! IStd module L = Logging -module AbstractAddress = PulseDomain.AbstractAddress module Memory = PulseAbductiveDomain.Memory module Stack = PulseAbductiveDomain.Stack open Result.Monad_infix @@ -91,7 +90,7 @@ module Closures = struct let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in Some (address_captured, new_trace) ) in - let closure_addr_hist = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in + let closure_addr_hist = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in let fake_capture_edges = mk_capture_edges captured_addresses in let astate = Memory.set_cell closure_addr_hist @@ -144,16 +143,16 @@ let eval location exp0 astate = eval exp' astate | Const c -> (* TODO: make identical const the same address *) - let addr = AbstractAddress.mk_fresh () in + let addr = AbstractValue.mk_fresh () in let astate = Memory.add_attribute addr (Constant c) astate in Ok (astate, (addr, [])) | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> - Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) [])) + Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in eval exp0 astate -type eval_result = EvalConst of Const.t | EvalAddr of AbstractAddress.t +type eval_result = EvalConst of Const.t | EvalAddr of AbstractValue.t let eval_to_const location exp astate = match (exp : Exp.t) with @@ -222,14 +221,14 @@ let eval_deref location exp astate = let realloc_pvar pvar location astate = Stack.add (Var.of_pvar pvar) - (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)]) + (AbstractValue.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)]) astate let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate let havoc_id id loc_opt astate = - if Stack.mem (Var.of_id id) astate then write_id id (AbstractAddress.mk_fresh (), loc_opt) astate + if Stack.mem (Var.of_id id) astate then write_id id (AbstractValue.mk_fresh (), loc_opt) astate else astate @@ -247,11 +246,11 @@ let write_field location addr_trace_ref field addr_trace_obj astate = let havoc_deref location addr_trace trace_obj astate = - write_deref location ~ref:addr_trace ~obj:(AbstractAddress.mk_fresh (), trace_obj) astate + write_deref location ~ref:addr_trace ~obj:(AbstractValue.mk_fresh (), trace_obj) astate let havoc_field location addr_trace field trace_obj astate = - write_field location addr_trace field (AbstractAddress.mk_fresh (), trace_obj) astate + write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate let invalidate location cause addr_trace astate = @@ -290,7 +289,7 @@ let shallow_copy location addr_hist astate = | Some cell -> cell in - let copy = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in + let copy = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in (Memory.set_cell copy cell location astate, copy) @@ -298,7 +297,7 @@ let check_address_escape escape_location proc_desc address history astate = let is_assigned_to_global address astate = let points_to_address pointer address astate = Memory.find_edge_opt pointer Dereference astate - |> Option.exists ~f:(fun (pointee, _) -> AbstractAddress.equal pointee address) + |> Option.exists ~f:(fun (pointee, _) -> AbstractValue.equal pointee address) in Stack.exists (fun var (pointer, _) -> Var.is_global var && points_to_address pointer address astate) @@ -324,13 +323,13 @@ let check_address_escape escape_location proc_desc address history astate = IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) astate ~f:(fun (variable, (var_address, _)) -> if - AbstractAddress.equal var_address address + AbstractValue.equal var_address address && ( Var.is_cpp_temporary variable || Var.is_local_to_procedure proc_name variable && not (Procdesc.is_captured_var proc_desc variable) ) then ( L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable - AbstractAddress.pp address ; + AbstractValue.pp address ; Error (PulseDiagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) ) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 9c97a7aab..d7d09d777 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -6,7 +6,6 @@ *) open! IStd -module AbstractAddress = PulseDomain.AbstractAddress open PulseBasicInterface type t = PulseAbductiveDomain.t @@ -15,7 +14,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result module Closures : sig val check_captured_addresses : - Location.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result + Location.t -> AbstractValue.t -> t -> (t, PulseDiagnostic.t) result (** assert the validity of the addresses captured by the lambda *) end @@ -86,20 +85,20 @@ val shallow_copy : Location.t -> PulseDomain.AddrTracePair.t -> t - -> (t * (AbstractAddress.t * ValueHistory.t)) access_result + -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** returns the address of a new cell with the same edges as the original *) val remove_vars : Var.t list -> Location.t -> t -> t val check_address_escape : - Location.t -> Procdesc.t -> AbstractAddress.t -> ValueHistory.t -> t -> t access_result + Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result val call : caller_summary:Summary.t -> Location.t -> Typ.Procname.t -> ret:Ident.t * Typ.t - -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> t -> t list access_result (** perform an interprocedural call: apply the summary for the call proc name passed as argument if