From f16534f39071182eeea89f4f1f8929619cb9e7d9 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 5 Dec 2019 05:16:25 -0800 Subject: [PATCH] [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 --- infer/src/checkers/LithoDomain.ml | 30 +++++++++++++++++++++++++++++- infer/src/checkers/LithoDomain.mli | 18 +++++++++++++++++- 2 files changed, 46 insertions(+), 2 deletions(-) diff --git a/infer/src/checkers/LithoDomain.ml b/infer/src/checkers/LithoDomain.ml index 36fe9dc9a..6888cd3e7 100644 --- a/infer/src/checkers/LithoDomain.ml +++ b/infer/src/checkers/LithoDomain.ml @@ -37,7 +37,35 @@ module MethodCall = struct end 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 = fold diff --git a/infer/src/checkers/LithoDomain.mli b/infer/src/checkers/LithoDomain.mli index c6d9acaf4..24810d19a 100644 --- a/infer/src/checkers/LithoDomain.mli +++ b/infer/src/checkers/LithoDomain.mli @@ -31,7 +31,23 @@ end 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 (** Substitute each access path in the domain using [f_sub]. If [f_sub] returns None, the original