diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 0bcb6bb1c..d68781dec 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -7,10 +7,10 @@ open! IStd module F = Format module L = Logging +open PulseBasicInterface module BaseDomain = PulseBaseDomain module BaseStack = BaseDomain.Stack -module BaseMemory = BaseDomain.Memory -open PulseBasicInterface +module BaseMemory = PulseBaseMemory (** signature common to the "normal" [Domain], representing the post at the current program point, and the inverted [InvertedDomain], representing the inferred pre-condition*) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index fc51f1e5d..2f6427849 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -7,6 +7,7 @@ open! IStd open PulseBasicInterface module BaseDomain = PulseBaseDomain +module BaseMemory = PulseBaseMemory (* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition when necessary @@ -37,11 +38,11 @@ module Stack : sig val exists : (Var.t -> BaseDomain.Stack.value -> bool) -> t -> bool end -(** memory operations like {!BaseDomain.Memory} but that also take care of propagating facts to the +(** memory operations like {!BaseMemory} but that also take care of propagating facts to the precondition *) module Memory : sig - module Access = BaseDomain.Memory.Access - module Edges = BaseDomain.Memory.Edges + module Access = BaseMemory.Access + module Edges = BaseMemory.Edges val add_attribute : AbstractValue.t -> Attribute.t -> t -> t @@ -55,11 +56,11 @@ module Memory : sig val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result - val find_opt : AbstractValue.t -> t -> BaseDomain.Memory.cell option + val find_opt : AbstractValue.t -> t -> BaseMemory.cell option val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option - val set_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.Memory.cell -> Location.t -> t -> t + val set_cell : AbstractValue.t * ValueHistory.t -> BaseMemory.cell -> Location.t -> t -> t val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index b13aa43ef..677d6cae7 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -8,11 +8,10 @@ open! IStd module F = Format module L = Logging open PulseBasicInterface +module Memory = PulseBaseMemory (* {2 Abstract domain description } *) -(* {3 Heap domain } *) - module AddrHistPair = struct type t = AbstractValue.t * ValueHistory.t [@@deriving compare] @@ -22,193 +21,6 @@ module AddrHistPair = struct else AbstractValue.pp f (fst addr_trace) end -module Memory : sig - module Access : sig - include PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t - - val equal : t -> t -> bool - end - - module Edges : PrettyPrintable.PPMap with type key = Access.t - - type edges = AddrHistPair.t Edges.t - - val pp_edges : F.formatter -> edges -> unit - - type cell = edges * Attributes.t - - type t - - val empty : t - - val filter : (AbstractValue.t -> bool) -> t -> t - - val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t - - val find_opt : AbstractValue.t -> t -> cell option - - val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc - - val set_attrs : AbstractValue.t -> Attributes.t -> t -> t - - val set_edges : AbstractValue.t -> edges -> t -> t - - val set_cell : AbstractValue.t -> cell -> t -> t - - val find_edges_opt : AbstractValue.t -> t -> edges option - - val mem_edges : AbstractValue.t -> t -> bool - - val pp_heap : F.formatter -> t -> unit - - val pp_attributes : F.formatter -> t -> unit - - val register_address : AbstractValue.t -> t -> t - - val add_edge : AbstractValue.t -> Access.t -> AddrHistPair.t -> t -> t - - val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrHistPair.t option - - val add_attribute : AbstractValue.t -> Attribute.t -> t -> t - - val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - - val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result - - val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option - - val get_constant : AbstractValue.t -> t -> Const.t option - - val std_vector_reserve : AbstractValue.t -> t -> t - - val is_std_vector_reserved : AbstractValue.t -> t -> bool -end = struct - module Access = struct - type t = AbstractValue.t HilExp.Access.t [@@deriving compare] - - let equal = [%compare.equal: t] - - let pp = HilExp.Access.pp AbstractValue.pp - end - - module Edges = PrettyPrintable.MakePPMap (Access) - - type edges = AddrHistPair.t Edges.t [@@deriving compare] - - let pp_edges = Edges.pp ~pp_value:AddrHistPair.pp - - type cell = edges * Attributes.t - - module Graph = PrettyPrintable.MakePPMap (AbstractValue) - - type t = edges Graph.t * Attributes.t Graph.t - - let pp_heap fmt (heap, _) = Graph.pp ~pp_value:pp_edges fmt heap - - let pp_attributes fmt (_, attrs) = Graph.pp ~pp_value:Attributes.pp fmt attrs - - let register_address addr memory = - if Graph.mem addr (fst memory) then memory - else (Graph.add addr Edges.empty (fst memory), snd memory) - - - (* {3 Helper functions to traverse the two maps at once } *) - - let add_edge addr_src access value memory = - let old_edges = Graph.find_opt addr_src (fst memory) |> Option.value ~default:Edges.empty in - let new_edges = Edges.add access value old_edges in - if phys_equal old_edges new_edges then memory - else (Graph.add addr_src new_edges (fst memory), snd memory) - - - let find_edge_opt addr access memory = - let open Option.Monad_infix in - Graph.find_opt addr (fst memory) >>= Edges.find_opt access - - - let add_attribute addr attribute memory = - match Graph.find_opt addr (snd memory) with - | None -> - (fst memory, Graph.add addr (Attributes.singleton attribute) (snd memory)) - | Some old_attrs -> - let new_attrs = Attributes.add old_attrs attribute in - (fst memory, Graph.add addr new_attrs (snd memory)) - - - let invalidate (address, history) invalid location memory = - let invalidation = Trace.Immediate {imm= invalid; location; history} in - add_attribute address (Attribute.Invalid invalidation) memory - - - let check_valid address memory = - 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 - | None -> - Ok () - - - let get_closure_proc_name address memory = - Graph.find_opt address (snd memory) - |> Option.bind ~f:(fun attributes -> Attributes.get_closure_proc_name attributes) - - - let get_constant address memory = - Graph.find_opt address (snd memory) - |> Option.bind ~f:(fun attributes -> Attributes.get_constant attributes) - - - let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory - - let is_std_vector_reserved address memory = - Graph.find_opt address (snd memory) - |> Option.value_map ~default:false ~f:(fun attributes -> - Attributes.is_std_vector_reserved attributes ) - - - (* {3 Monomorphic {!PPMap} interface as needed } *) - - let empty = (Graph.empty, Graph.empty) - - let find_edges_opt addr memory = Graph.find_opt addr (fst memory) - - let find_attrs_opt addr memory = Graph.find_opt addr (snd memory) - - let find_opt addr memory = - match (find_edges_opt addr memory, find_attrs_opt addr memory) with - | None, None -> - None - | edges_opt, attrs_opt -> - let edges = Option.value edges_opt ~default:Edges.empty in - let attrs = Option.value attrs_opt ~default:Attributes.empty in - Some (edges, attrs) - - - let fold_attrs f memory init = Graph.fold f (snd memory) init - - let set_attrs addr attrs memory = (fst memory, Graph.add addr attrs (snd memory)) - - let set_edges addr edges memory = (Graph.add addr edges (fst memory), snd memory) - - let set_cell addr (edges, attrs) memory = - (Graph.add addr edges (fst memory), Graph.add addr attrs (snd memory)) - - - let filter f memory = - let heap = Graph.filter (fun address _ -> f address) (fst memory) in - let attrs = Graph.filter (fun address _ -> f address) (snd memory) in - if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs) - - - let filter_heap f memory = - let heap = Graph.filter f (fst memory) in - if phys_equal heap (fst memory) then memory else (heap, snd memory) - - - let mem_edges addr memory = Graph.mem addr (fst memory) -end - (** Stacks: map addresses of variables to values and initialisation location. *) module Stack = struct module VarAddress = struct diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index ea91ba10e..1a0d22982 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -6,7 +6,6 @@ *) open! IStd -module F = Format open PulseBasicInterface module Stack : sig @@ -18,60 +17,7 @@ module Stack : sig val compare : t -> t -> int [@@warning "-32"] end -module Memory : sig - module Access : - PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t - - module Edges : PrettyPrintable.PPMap with type key = Access.t - - type edges = (AbstractValue.t * ValueHistory.t) Edges.t - - val pp_edges : F.formatter -> edges -> unit [@@warning "-32"] - - type cell = edges * Attributes.t - - type t - - val filter : (AbstractValue.t -> bool) -> t -> t - - val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t - - val find_opt : AbstractValue.t -> t -> cell option - - val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc - - val set_attrs : AbstractValue.t -> Attributes.t -> t -> t - - val set_edges : AbstractValue.t -> edges -> t -> t - - val set_cell : AbstractValue.t -> cell -> t -> t - - val find_edges_opt : AbstractValue.t -> t -> edges option - - val mem_edges : AbstractValue.t -> t -> bool - - val register_address : AbstractValue.t -> t -> t - - val add_edge : AbstractValue.t -> Access.t -> AbstractValue.t * ValueHistory.t -> t -> t - - val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option - - val add_attribute : AbstractValue.t -> Attribute.t -> t -> t - - val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - - val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result - - val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option - - val get_constant : AbstractValue.t -> t -> Const.t option - - val std_vector_reserve : AbstractValue.t -> t -> t - - val is_std_vector_reserved : AbstractValue.t -> t -> bool -end - -type t = {heap: Memory.t; stack: Stack.t} +type t = {heap: PulseBaseMemory.t; stack: Stack.t} val empty : t diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml new file mode 100644 index 000000000..a4b14fe11 --- /dev/null +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -0,0 +1,142 @@ +(* + * 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 +module L = Logging +open PulseBasicInterface + +(* {3 Heap domain } *) + +module Access = struct + type t = AbstractValue.t HilExp.Access.t [@@deriving compare] + + let equal = [%compare.equal: t] + + let pp = HilExp.Access.pp AbstractValue.pp +end + +module Edges = PrettyPrintable.MakePPMap (Access) + +type edges = (AbstractValue.t * ValueHistory.t) Edges.t [@@deriving compare] + +let pp_edges = + Edges.pp ~pp_value:(fun f addr_trace -> + if Config.debug_level_analysis >= 3 then + Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace + else AbstractValue.pp f (fst addr_trace) ) + + +type cell = edges * Attributes.t + +module Graph = PrettyPrintable.MakePPMap (AbstractValue) + +type t = edges Graph.t * Attributes.t Graph.t + +let pp_heap fmt (heap, _) = Graph.pp ~pp_value:pp_edges fmt heap + +let pp_attributes fmt (_, attrs) = Graph.pp ~pp_value:Attributes.pp fmt attrs + +let register_address addr memory = + if Graph.mem addr (fst memory) then memory + else (Graph.add addr Edges.empty (fst memory), snd memory) + + +(* {3 Helper functions to traverse the two maps at once } *) + +let add_edge addr_src access value memory = + let old_edges = Graph.find_opt addr_src (fst memory) |> Option.value ~default:Edges.empty in + let new_edges = Edges.add access value old_edges in + if phys_equal old_edges new_edges then memory + else (Graph.add addr_src new_edges (fst memory), snd memory) + + +let find_edge_opt addr access memory = + let open Option.Monad_infix in + Graph.find_opt addr (fst memory) >>= Edges.find_opt access + + +let add_attribute addr attribute memory = + match Graph.find_opt addr (snd memory) with + | None -> + (fst memory, Graph.add addr (Attributes.singleton attribute) (snd memory)) + | Some old_attrs -> + let new_attrs = Attributes.add old_attrs attribute in + (fst memory, Graph.add addr new_attrs (snd memory)) + + +let invalidate (address, history) invalid location memory = + let invalidation = Trace.Immediate {imm= invalid; location; history} in + add_attribute address (Attribute.Invalid invalidation) memory + + +let check_valid address memory = + 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 + | None -> + Ok () + + +let get_closure_proc_name address memory = + Graph.find_opt address (snd memory) + |> Option.bind ~f:(fun attributes -> Attributes.get_closure_proc_name attributes) + + +let get_constant address memory = + Graph.find_opt address (snd memory) + |> Option.bind ~f:(fun attributes -> Attributes.get_constant attributes) + + +let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory + +let is_std_vector_reserved address memory = + Graph.find_opt address (snd memory) + |> Option.value_map ~default:false ~f:(fun attributes -> + Attributes.is_std_vector_reserved attributes ) + + +(* {3 Monomorphic {!PPMap} interface as needed } *) + +let empty = (Graph.empty, Graph.empty) + +let find_edges_opt addr memory = Graph.find_opt addr (fst memory) + +let find_attrs_opt addr memory = Graph.find_opt addr (snd memory) + +let find_opt addr memory = + match (find_edges_opt addr memory, find_attrs_opt addr memory) with + | None, None -> + None + | edges_opt, attrs_opt -> + let edges = Option.value edges_opt ~default:Edges.empty in + let attrs = Option.value attrs_opt ~default:Attributes.empty in + Some (edges, attrs) + + +let fold_attrs f memory init = Graph.fold f (snd memory) init + +let set_attrs addr attrs memory = (fst memory, Graph.add addr attrs (snd memory)) + +let set_edges addr edges memory = (Graph.add addr edges (fst memory), snd memory) + +let set_cell addr (edges, attrs) memory = + (Graph.add addr edges (fst memory), Graph.add addr attrs (snd memory)) + + +let filter f memory = + let heap = Graph.filter (fun address _ -> f address) (fst memory) in + let attrs = Graph.filter (fun address _ -> f address) (snd memory) in + if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs) + + +let filter_heap f memory = + let heap = Graph.filter f (fst memory) in + if phys_equal heap (fst memory) then memory else (heap, snd memory) + + +let mem_edges addr memory = Graph.mem addr (fst memory) diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli new file mode 100644 index 000000000..5208e950d --- /dev/null +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -0,0 +1,67 @@ +(* + * 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 +open PulseBasicInterface + +module Access : sig + include PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t + + val equal : t -> t -> bool +end + +module Edges : PrettyPrintable.PPMap with type key = Access.t + +type edges = (AbstractValue.t * ValueHistory.t) Edges.t + +type cell = edges * Attributes.t + +type t + +val empty : t + +val filter : (AbstractValue.t -> bool) -> t -> t + +val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t + +val find_opt : AbstractValue.t -> t -> cell option + +val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + +val set_attrs : AbstractValue.t -> Attributes.t -> t -> t + +val set_edges : AbstractValue.t -> edges -> t -> t + +val set_cell : AbstractValue.t -> cell -> t -> t + +val find_edges_opt : AbstractValue.t -> t -> edges option + +val mem_edges : AbstractValue.t -> t -> bool + +val pp_heap : F.formatter -> t -> unit + +val pp_attributes : F.formatter -> t -> unit + +val register_address : AbstractValue.t -> t -> t + +val add_edge : AbstractValue.t -> Access.t -> AbstractValue.t * ValueHistory.t -> t -> t + +val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option + +val add_attribute : AbstractValue.t -> Attribute.t -> t -> t + +val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + +val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result + +val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option + +val get_constant : AbstractValue.t -> t -> Const.t option + +val std_vector_reserve : AbstractValue.t -> t -> t + +val is_std_vector_reserved : AbstractValue.t -> t -> bool diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml index 97d3c8c5c..df7ce774a 100644 --- a/infer/src/pulse/PulseDomainInterface.ml +++ b/infer/src/pulse/PulseDomainInterface.ml @@ -16,4 +16,4 @@ module Memory = AbductiveDomain.Memory module BaseDomain = PulseBaseDomain module BaseStack = BaseDomain.Stack -module BaseMemory = BaseDomain.Memory +module BaseMemory = PulseBaseMemory