From 363d69430d8a66c3b58d17d9e57aa9d664a08490 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 8 Mar 2019 10:49:25 -0800 Subject: [PATCH] [ai][pulse] use subgraph-based implication between states Summary: When joining two lists of disjuncts we try to ensure there isn't a state that under-approximates another already in the list. This helps reduce the number of disjuncts that are generated by conditionals and loops. Before we would always just add more disjuncts unless they were physically equal but now we do a subgraph computation to assess under-approximation. We only do this half-heartedly for now however, only taking into consideration the "new" disjuncts vs the "old" ones. It probably makes sense to do a full quadratic search to minimise the number of disjuncts from time to time but this isn't done here. Reviewed By: mbouaziz Differential Revision: D14258482 fbshipit-source-id: c2dad4889 --- infer/src/absint/TransferFunctions.ml | 11 +- infer/src/checkers/PulseDomain.ml | 187 +++++++++++++++--- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- infer/tests/codetoanalyze/cpp/pulse/join.cpp | 5 + 4 files changed, 177 insertions(+), 28 deletions(-) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index fb2169fcd..bc5c79a5b 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -82,9 +82,12 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct type t = Disjuncts.t let join_normalize_into s_froms ~into:s_intos = + (* ignore states in [s_froms] that are under-approximated in [s_intos] *) let s_from_not_in_intos = List.rev_filter s_froms ~f:(fun s_from -> - List.exists s_intos ~f:(fun s_into -> phys_equal s_from s_into) |> not ) + List.exists s_intos ~f:(fun s_into -> + TransferFunctions.Domain.( <= ) ~rhs:s_from ~lhs:s_into ) + |> not ) in List.rev_append s_from_not_in_intos s_intos @@ -98,7 +101,11 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct rhs @ lhs | `UnderApproximateAfter n -> let lhs_length = List.length lhs in - if lhs_length >= n then lhs else join_normalize_into rhs ~into:lhs + if lhs_length >= n then lhs + else + (* do not add states from [rhs] (assumed to be the *new* states in the case of a loop) + that are already implied by some state in the [lhs] *) + join_normalize_into rhs ~into:lhs let rec ( <= ) ~lhs ~rhs = diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 875f0f7a1..7b78300f7 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -6,6 +6,7 @@ *) open! IStd module F = Format +module L = Logging module Invalidation = PulseInvalidation (* {2 Abstract domain description } *) @@ -77,8 +78,11 @@ module AddrTracePair = struct end module Memory : sig - module Access : - PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t + module Access : sig + include PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t + + val equal : t -> t -> bool + end module Edges : PrettyPrintable.PPMap with type key = Access.t @@ -94,8 +98,6 @@ module Memory : sig val find_opt : AbstractAddress.t -> t -> cell option - val for_all : (AbstractAddress.t -> cell -> bool) -> t -> bool - val set_cell : AbstractAddress.t -> cell -> t -> t val pp : F.formatter -> t -> unit @@ -120,6 +122,8 @@ end = struct module Access = struct type t = AbstractAddress.t HilExp.Access.t [@@deriving compare] + let equal = [%compare.equal: t] + let pp = HilExp.Access.pp AbstractAddress.pp end @@ -217,8 +221,6 @@ end = struct let find_opt = Graph.find_opt - let for_all = Graph.for_all - let set_cell = Graph.add let filter = Graph.filter @@ -278,28 +280,162 @@ let initial = ; stack= Stack.empty } -let piecewise_lessthan lhs rhs = - Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack - && Memory.for_all - (fun addr_src (edges_lhs, attrs_lhs) -> - let edges_rhs_opt, attrs_rhs = - let cell = Memory.find_opt addr_src rhs.heap in - (Option.map ~f:fst cell, Option.value_map ~default:Attributes.empty ~f:snd cell) - in - Memory.Edges.for_all - (fun access_lhs (addr_dst, _) -> - Option.bind edges_rhs_opt ~f:(fun edges_rhs -> - Memory.Edges.find_opt access_lhs edges_rhs ) - |> Option.exists ~f:(fun (addr_dst_rhs, _) -> - AbstractAddress.equal addr_dst_rhs addr_dst ) ) - edges_lhs - && Attributes.( <= ) ~lhs:attrs_lhs ~rhs:attrs_rhs ) - lhs.heap - +(** comparison between two elements of the domain to determine the [<=] relation + + Given two states [lhs] and [rhs], try to find a bijection [lhs_to_rhs]/[rhs_to_lhs] between the + addresses of [lhs] and [rhs] such that [lhs_to_rhs(lhs)] contains (is a supergraph of) [rhs]. +*) +module GraphComparison = struct + module AddressMap = PrettyPrintable.MakePPMap (AbstractAddress) + + (** translation between the abstract values on the LHS and the ones on the RHS *) + type mapping = + { rhs_to_lhs: AbstractAddress.t AddressMap.t (** map from RHS values to LHS *) + ; lhs_to_rhs: AbstractAddress.t AddressMap.t (** inverse map from [rhs_to_lhs] *) } + + let empty_mapping = {rhs_to_lhs= AddressMap.empty; lhs_to_rhs= AddressMap.empty} + + let pp_mapping fmt {rhs_to_lhs; lhs_to_rhs} = + F.fprintf fmt "@[{ rhs_to_lhs=@[%a@];@,lhs_to_rhs=@[%a@];@,}@]" + (AddressMap.pp ~pp_value:AbstractAddress.pp) + rhs_to_lhs + (AddressMap.pp ~pp_value:AbstractAddress.pp) + lhs_to_rhs + + + (** try to add the fact that [addr_lhs] corresponds to [addr_rhs] to the [mapping] *) + let record_equal ~addr_lhs ~addr_rhs mapping = + (* have we seen [addr_lhs] before?.. *) + match AddressMap.find_opt addr_lhs mapping.lhs_to_rhs with + | Some addr_rhs' when not (AbstractAddress.equal addr_rhs addr_rhs') -> + (* ...yes, but it was bound to another address *) + L.d_printfln + "Aliasing in LHS not in RHS: LHS address %a in current already bound to %a, not %a@\n\ + State=%a" + AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs' AbstractAddress.pp addr_rhs + pp_mapping mapping ; + `AliasingLHS + | Some _addr_rhs (* [_addr_rhs = addr_rhs] *) -> + `AlreadyVisited + | None -> ( + (* ...and have we seen [addr_rhs] before?.. *) + match AddressMap.find_opt addr_rhs mapping.rhs_to_lhs with + | Some addr_lhs' -> + (* ...yes, but it was bound to another address: [addr_lhs' != addr_lhs] otherwise we would + have found [addr_lhs] in the [lhs_to_rhs] map above *) + L.d_printfln + "Aliasing in RHS not in LHS: RHS address %a in current already bound to %a, not %a@\n\ + State=%a" + AbstractAddress.pp addr_rhs AbstractAddress.pp addr_lhs' AbstractAddress.pp addr_lhs + pp_mapping mapping ; + `AliasingRHS + | None -> + (* [addr_rhs] and [addr_lhs] are both new, record that they correspond to each other *) + let mapping' = + { rhs_to_lhs= AddressMap.add addr_rhs addr_lhs mapping.rhs_to_lhs + ; lhs_to_rhs= AddressMap.add addr_lhs addr_rhs mapping.lhs_to_rhs } + in + `NotAlreadyVisited mapping' ) + + + type supergraph_relation = + | NotASupergraph (** no mapping was found that can make LHS bigger than RHS *) + | Supergraph of mapping (** [mapping(lhs)] is a supergraph of [rhs] *) + + (** can we extend [mapping] so that the subgraph of [lhs] rooted at [addr_lhs] is a supergraph of + the subgraph of [rhs] rooted at [addr_rhs]? *) + let rec supergraph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping = + L.d_printfln "%a<->%a@\n" AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs ; + match record_equal mapping ~addr_lhs ~addr_rhs with + | `AlreadyVisited -> + Supergraph mapping + | `AliasingRHS | `AliasingLHS -> + NotASupergraph + | `NotAlreadyVisited mapping -> ( + match Memory.find_opt addr_rhs rhs.heap with + | None -> + (* nothing on the RHS: nothing more to check *) + Supergraph mapping + | Some (edges_rhs, attrs_rhs) -> ( + match Memory.find_opt addr_lhs lhs.heap with + | None -> + (* [RHS] is not a subgraph of [LHS] unless [addr_rhs] has no attributes and no edges + (could happen because of [register_address] or because we don't care to delete empty + edges when removing edges) *) + if Memory.Edges.is_empty edges_rhs && Attributes.is_empty attrs_rhs then + Supergraph mapping + else NotASupergraph + | Some (edges_lhs, attrs_lhs) -> + (* continue the comparison recursively on all edges and attributes *) + if Attributes.subset attrs_rhs attrs_lhs then + let bindings_lhs = Memory.Edges.bindings edges_lhs in + let bindings_rhs = Memory.Edges.bindings edges_rhs in + supergraph_map_edges ~lhs ~edges_lhs:bindings_lhs ~rhs ~edges_rhs:bindings_rhs + mapping + else NotASupergraph ) ) + + + (** check that the supergraph relation can be extended for all edges *) + and supergraph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping = + match (edges_lhs, edges_rhs) with + | _, [] -> + (* more edges on the LHS => supergraph *) + Supergraph mapping + | (a_lhs, (addr_lhs, _trace_lhs)) :: edges_lhs, (a_rhs, (addr_rhs, _trace_rhs)) :: edges_rhs + when Memory.Access.equal a_lhs a_rhs -> ( + (* check supergraph relation from the destination addresses *) + match supergraph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping with + | Supergraph mapping -> + (* ok: continue with the other edges *) + supergraph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping + | NotASupergraph -> + NotASupergraph ) + | (a_lhs, _) :: edges_lhs, (a_rhs, _) :: _ when Memory.Access.compare a_lhs a_rhs < 0 -> + (* [a_lhs] is not present on the RHS: that's ok: the LHS knows more than the RHS *) + supergraph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping + | _, _ :: _ -> + (* [a_rhs] is not present on the LHS: that's not ok: the RHS knows more than the LHS *) + NotASupergraph + + + (** check that the memory graph induced by the addresses in [lhs] reachable from the variables in + [stack_lhs] is a supergraph of the same graph in [rhs] starting from [stack_rhs], up to some + [mapping] *) + let rec supergraph_map_from_stack ~lhs ~stack_lhs ~rhs ~stack_rhs mapping = + match (stack_lhs, stack_rhs) with + | _, [] -> + Supergraph mapping + | ( (var_lhs, (addr_lhs, _trace_lhs)) :: stack_lhs + , (var_rhs, (addr_rhs, _trace_rhs)) :: stack_rhs ) + when Var.equal var_lhs var_rhs -> ( + match supergraph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping with + | Supergraph mapping -> + supergraph_map_from_stack ~lhs ~stack_lhs ~rhs ~stack_rhs mapping + | NotASupergraph -> + NotASupergraph ) + | (var_lhs, _) :: stack_lhs, (var_rhs, _) :: _ when Var.compare var_lhs var_rhs < 0 -> + (* [var_lhs] is not present on the RHS: that's ok: the LHS knows more than the RHS *) + supergraph_map_from_stack ~lhs ~stack_lhs ~rhs ~stack_rhs mapping + | _, _ :: _ -> + NotASupergraph + + + let supergraph_map ~lhs ~rhs mapping = + let stack_lhs = Stack.bindings lhs.stack in + let stack_rhs = Stack.bindings rhs.stack in + supergraph_map_from_stack ~lhs ~rhs ~stack_lhs ~stack_rhs mapping + + + let is_supergraph ~lhs ~rhs mapping = + match supergraph_map ~lhs ~rhs mapping with Supergraph _ -> true | NotASupergraph -> false +end let join _ _ = (* not implemented: use disjunctive domain instead *) assert false -let ( <= ) ~lhs ~rhs = phys_equal lhs rhs || piecewise_lessthan lhs rhs +let ( <= ) ~lhs ~rhs = + (* [lhs] implies [rhs] if it knows more facts than [rhs] *) + phys_equal lhs rhs || GraphComparison.is_supergraph ~lhs ~rhs GraphComparison.empty_mapping + let widen ~prev:_ ~next:_ ~num_iters:_ = (* not implemented: use disjunctive domain instead *) assert false @@ -354,3 +490,4 @@ end = struct end include GraphGC +include GraphComparison diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 571a15739..bc7711c3b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -2,7 +2,7 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70 here,accessed `ptr` here] codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 29 here,accessed `&(f)` here] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 20 here,accessed `&(f)` here] -codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 25 here,accessed `*(result)` here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 30 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/cpp/pulse/join.cpp b/infer/tests/codetoanalyze/cpp/pulse/join.cpp index a25dff9dd..7352944aa 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/join.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/join.cpp @@ -8,6 +8,11 @@ #include #include +void basic_loop_count_ok(int n) { + for (int i = 0; i < n; i++) { + } +} + struct foo { int* val; };