From ad98ffa22bc08fa5ca27155af530df2067c2c335 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 18 Oct 2018 07:54:07 -0700 Subject: [PATCH] [pulse] more aggressive join Summary: Do the intersection of the heap and stack domains, and the union of the invalid location sets. This forgets invalid locations that appear only in one heap, unfortunately. We can start with this and improve later. Reviewed By: mbouaziz Differential Revision: D10445825 fbshipit-source-id: cc24460af --- infer/src/checkers/PulseDomain.ml | 40 +++++++++++++------ infer/src/checkers/PulseDomain.mli | 10 +++-- .../tests/codetoanalyze/cpp/pulse/issues.exp | 3 -- 3 files changed, 34 insertions(+), 19 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index ab483ed17..f86bcc70a 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -47,20 +47,40 @@ module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLoca let pp = AbstractLocation.pp end -module MemoryKey = struct - type t = AbstractLocation.t * AccessPath.access [@@deriving compare] +module Access = struct + type t = AccessPath.access [@@deriving compare] - let pp f k = Pp.pair ~fst:AbstractLocation.pp ~snd:AccessPath.pp_access f k + let pp = AccessPath.pp_access end -module MemoryDomain = AbstractDomain.Map (MemoryKey) (AbstractLocationDomain) -module AliasingDomain = AbstractDomain.Map (Var) (AbstractLocationDomain) +module MemoryEdges = AbstractDomain.InvertedMap (Access) (AbstractLocationDomain) + +module MemoryDomain = struct + include AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges) + + let add_edge loc_src access loc_end memory = + let edges = + match find_opt loc_src memory with Some edges -> edges | None -> MemoryEdges.empty + in + add loc_src (MemoryEdges.add access loc_end edges) memory + + + let find_edge_opt loc access memory = + let open Option.Monad_infix in + find_opt loc memory >>= MemoryEdges.find_opt access +end + +module AliasingDomain = AbstractDomain.InvertedMap (Var) (AbstractLocationDomain) module AbstractLocationsDomain = AbstractDomain.FiniteSet (AbstractLocation) module InvalidLocationsDomain = AbstractLocationsDomain type t = {heap: MemoryDomain.astate; stack: AliasingDomain.astate; invalids: InvalidLocationsDomain.astate} +let initial = + {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty} + + module Domain : AbstractDomain.S with type astate = t = struct type astate = t @@ -107,10 +127,6 @@ end include Domain -let initial = - {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty} - - module Diagnostic = struct (* TODO: more structured error type so that we can actually report something informative about the variables being accessed along with a trace *) @@ -140,15 +156,15 @@ let rec walk ~overwrite_last loc path astate = | [a], Some new_loc -> check_loc_access loc astate >>| fun astate -> - let heap = MemoryDomain.add (loc, a) new_loc astate.heap in + let heap = MemoryDomain.add_edge loc a new_loc astate.heap in ({astate with heap}, new_loc) | a :: path, _ -> ( check_loc_access loc astate >>= fun astate -> - match MemoryDomain.find_opt (loc, a) astate.heap with + match MemoryDomain.find_edge_opt loc a astate.heap with | None -> let loc' = AbstractLocation.mk_fresh () in - let heap = MemoryDomain.add (loc, a) loc' astate.heap in + let heap = MemoryDomain.add_edge loc a loc' astate.heap in let astate = {astate with heap} in walk ~overwrite_last loc' path astate | Some loc' -> diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index c5b3fa578..603affa3b 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -14,8 +14,8 @@ module AbstractLocation : sig val pp : F.formatter -> t -> unit end -module MemoryKey : sig - type t = AbstractLocation.t * AccessPath.access [@@deriving compare] +module Access : sig + type t = AccessPath.access [@@deriving compare] val pp : F.formatter -> t -> unit end @@ -24,9 +24,11 @@ module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLoca module AbstractLocationsDomain : module type of AbstractDomain.FiniteSet (AbstractLocation) -module MemoryDomain : module type of AbstractDomain.Map (MemoryKey) (AbstractLocationDomain) +module MemoryEdges : module type of AbstractDomain.InvertedMap (Access) (AbstractLocationDomain) -module AliasingDomain : module type of AbstractDomain.Map (Var) (AbstractLocationDomain) +module MemoryDomain : module type of AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges) + +module AliasingDomain : module type of AbstractDomain.InvertedMap (Var) (AbstractLocationDomain) module InvalidLocationsDomain : module type of AbstractLocationsDomain diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 5866ac513..5db7b8a7e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,6 +1,3 @@ -codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [] codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []