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

[pulse][10/9] carve out PulseBaseMemory

Browse Source 
Summary:
That module's interface was repeated twice to avoid exposing its
internals to PulseDomain itself. It's also quite long so it makes sense
to move it to its own file.

Reviewed By: ezgicicek

Differential Revision: D17977209

fbshipit-source-id: 56a2dac24
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent 1652144176
commit 2fd3f9a37b
7 changed files with 220 additions and 252 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/pulse/PulseAbductiveDomain.ml
Unescape View File

@ -7,10 +7,10 @@
open! IStd open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
open PulseBasicInterface
module BaseDomain = PulseBaseDomain module BaseDomain = PulseBaseDomain
module BaseStack = BaseDomain.Stack module BaseStack = BaseDomain.Stack
module BaseMemory = BaseDomain.Memory module BaseMemory = PulseBaseMemory
open PulseBasicInterface
(** signature common to the "normal" [Domain], representing the post at the current program point, (** signature common to the "normal" [Domain], representing the post at the current program point,
and the inverted [InvertedDomain], representing the inferred pre-condition*) and the inverted [InvertedDomain], representing the inferred pre-condition*)

11
infer/src/pulse/PulseAbductiveDomain.mli
Unescape View File

@ -7,6 +7,7 @@
open! IStd open! IStd
open PulseBasicInterface open PulseBasicInterface
module BaseDomain = PulseBaseDomain module BaseDomain = PulseBaseDomain
module BaseMemory = PulseBaseMemory
(* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition (* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition
when necessary when necessary
@ -37,11 +38,11 @@ module Stack : sig
val exists : (Var.t -> BaseDomain.Stack.value -> bool) -> t -> bool val exists : (Var.t -> BaseDomain.Stack.value -> bool) -> t -> bool
end 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 *) precondition *)
module Memory : sig module Memory : sig
module Access = BaseDomain.Memory.Access module Access = BaseMemory.Access
module Edges = BaseDomain.Memory.Edges module Edges = BaseMemory.Edges
val add_attribute : AbstractValue.t -> Attribute.t -> t -> t 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 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 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 val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t

190
infer/src/pulse/PulseBaseDomain.ml
Unescape View File

@ -8,11 +8,10 @@ open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
open PulseBasicInterface open PulseBasicInterface
module Memory = PulseBaseMemory
(* {2 Abstract domain description } *) (* {2 Abstract domain description } *)
(* {3 Heap domain } *)
module AddrHistPair = struct module AddrHistPair = struct
type t = AbstractValue.t * ValueHistory.t [@@deriving compare] type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
@ -22,193 +21,6 @@ module AddrHistPair = struct
else AbstractValue.pp f (fst addr_trace) else AbstractValue.pp f (fst addr_trace)
end 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. *) (** Stacks: map addresses of variables to values and initialisation location. *)
module Stack = struct module Stack = struct
module VarAddress = struct module VarAddress = struct

56
infer/src/pulse/PulseBaseDomain.mli
Unescape View File

@ -6,7 +6,6 @@
*) *)
open! IStd open! IStd
module F = Format
open PulseBasicInterface open PulseBasicInterface
module Stack : sig module Stack : sig
@ -18,60 +17,7 @@ module Stack : sig
val compare : t -> t -> int [@@warning "-32"] val compare : t -> t -> int [@@warning "-32"]
end end
module Memory : sig type t = {heap: PulseBaseMemory.t; stack: Stack.t}
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}
val empty : t val empty : t

142
infer/src/pulse/PulseBaseMemory.ml
Unescape View File

@ -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)

67
infer/src/pulse/PulseBaseMemory.mli
Unescape View File

@ -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

2
infer/src/pulse/PulseDomainInterface.ml
Unescape View File

@ -16,4 +16,4 @@ module Memory = AbductiveDomain.Memory
module BaseDomain = PulseBaseDomain module BaseDomain = PulseBaseDomain
module BaseStack = BaseDomain.Stack module BaseStack = BaseDomain.Stack
module BaseMemory = BaseDomain.Memory module BaseMemory = PulseBaseMemory

Write Preview
Loading…
Cancel
Save