[litho] Add dummy memory type

Summary: This diff stack is to revise overall domain and semantics of litho checker. Some of the following diffs will not have visible changes until we replace the current checker with the new one.

Reviewed By: ezgicicek

Differential Revision: D18779592

fbshipit-source-id: d210d9bd1
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent bf0d1d8861
commit f16534f390

@ -37,7 +37,35 @@ module MethodCall = struct
end end
module CallSet = AbstractDomain.FiniteSet (MethodCall) module CallSet = AbstractDomain.FiniteSet (MethodCall)
include AbstractDomain.Map (LocalAccessPath) (CallSet) module OldDomain = AbstractDomain.Map (LocalAccessPath) (CallSet)
module NewDomain = struct
include AbstractDomain.Empty
end
include struct
include AbstractDomain.Pair (OldDomain) (NewDomain)
let lift f (o, _) = f o
let map_old f (o, n) = (f o, n)
let empty = (OldDomain.empty, ())
let add k v = map_old (OldDomain.add k v)
let remove k = map_old (OldDomain.remove k)
let bindings = lift OldDomain.bindings
let find k = lift (OldDomain.find k)
let mem k = lift (OldDomain.mem k)
let iter f = lift (OldDomain.iter f)
let fold f (o, _) init = OldDomain.fold f o init
end
let substitute ~(f_sub : LocalAccessPath.t -> LocalAccessPath.t option) astate = let substitute ~(f_sub : LocalAccessPath.t -> LocalAccessPath.t option) astate =
fold fold

@ -31,7 +31,23 @@ end
module CallSet : module type of AbstractDomain.FiniteSet (MethodCall) module CallSet : module type of AbstractDomain.FiniteSet (MethodCall)
include module type of AbstractDomain.Map (LocalAccessPath) (CallSet) module OldDomain : module type of AbstractDomain.Map (LocalAccessPath) (CallSet)
module NewDomain : module type of AbstractDomain.Empty
include module type of AbstractDomain.Pair (OldDomain) (NewDomain)
val empty : t
val add : LocalAccessPath.t -> CallSet.t -> t -> t
val remove : LocalAccessPath.t -> t -> t
val mem : LocalAccessPath.t -> t -> bool
val find : LocalAccessPath.t -> t -> CallSet.t
val bindings : t -> (LocalAccessPath.t * CallSet.t) list
val substitute : f_sub:(LocalAccessPath.t -> LocalAccessPath.t option) -> t -> t val substitute : f_sub:(LocalAccessPath.t -> LocalAccessPath.t option) -> t -> t
(** Substitute each access path in the domain using [f_sub]. If [f_sub] returns None, the original (** Substitute each access path in the domain using [f_sub]. If [f_sub] returns None, the original

Loading…
Cancel
Save