From 4cdb65c237a3fc0837f5ccf99c7c860f08fffea7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 27 Mar 2019 10:22:31 -0700 Subject: [PATCH] [pulse] |- is now true only of isomorphic graphs Summary: Previously we would say that `lhs <= rhs` (or `lhs |- rhs`) when a mapping existed between the abstract addresses of `lhs` and `rhs` such that `mapping(lhs)` was a supergraph of `rhs`. In particular, we had that `x |-> x' * x' |-> x'' |- x |-> x'`. This is not entirely great, in particular once we get pairs of state representing footprint + current state. I'm not sure I have an extremely compelling argument why though, except that it's not the usual way we do implication in SL, but there wasn't a compelling argument for the previous state of affairs either. This changes `|-` to be true only when `mapping(lhs) = rhs` (modulo only considering the addresses reachable from the stack variables). Reviewed By: jberdine Differential Revision: D14568272 fbshipit-source-id: 1bb83950e --- infer/src/absint/TransferFunctions.ml | 70 ++++++---- infer/src/pulse/PulseDomain.ml | 130 +++++++++--------- .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 +- 3 files changed, 107 insertions(+), 97 deletions(-) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 9794e4e62..8c700ded0 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -83,7 +83,10 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct let elements disjuncts = List.map disjuncts ~f:(fun {astate} -> astate) - let pp f disjuncts = PrettyPrintable.pp_collection ~pp_item:pp_disjunct f disjuncts + let pp f disjuncts = + F.fprintf f "@[%d disjuncts:@;%a@]" (List.length disjuncts) + (PrettyPrintable.pp_collection ~pp_item:pp_disjunct) + disjuncts end type disjunct_t = Disjuncts.disjunct = {visited: bool; astate: TransferFunctions.Domain.t} @@ -91,15 +94,20 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct module Domain = struct 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 -> - TransferFunctions.Domain.( <= ) ~rhs:s_from.astate ~lhs:s_into.astate ) - |> not ) - in - List.rev_append s_from_not_in_intos s_intos + let rev_filter_not_over_approximated disjuncts ~not_in = + List.rev_filter disjuncts ~f:(fun disjunct -> + List.exists not_in ~f:(fun disj_not_in -> + TransferFunctions.Domain.( <= ) ~lhs:disjunct.astate ~rhs:disj_not_in.astate ) + |> not ) + + + (* Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping + states in [lhs]. *) + let join_up_to_imply lhs rhs = + let rev_rhs_not_in_lhs = rev_filter_not_over_approximated rhs ~not_in:lhs in + (* cheeky: this is only used in pulse, whose (<=) is actually a symmetric relation so there's + no need to filter out elements of [lhs] *) + List.rev_append rev_rhs_not_in_lhs lhs let join : t -> t -> t = @@ -108,14 +116,10 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct else match DConfig.join_policy with | `NeverJoin -> - rhs @ lhs + List.rev_append rhs lhs | `UnderApproximateAfter n -> let lhs_length = List.length lhs in - 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 + if lhs_length >= n then lhs else List.rev_append rhs lhs let set_visited b disjuncts = @@ -123,20 +127,29 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct else List.map disjuncts ~f:(fun disjunct -> {disjunct with visited= b}) - let rec ( <= ) ~lhs ~rhs = - if phys_equal lhs rhs then (* also takes care of the case [lhs = rhs = []] *) true - else - (* quick check: [lhs <= rhs] if [rhs] is [something @ lhs] *) - match rhs with [] -> false | _ :: rhs' -> ( <= ) ~lhs ~rhs:rhs' + (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on + abstract states to compare elements quickly *) + let rec is_trivial_subset disj ~of_ = + match (disj, of_) with + | [], _ -> + true + | x :: disj', y :: of' when phys_equal x.astate y.astate -> + is_trivial_subset disj' ~of_:of' + | _, _ :: of' -> + is_trivial_subset disj ~of_:of' + | _, [] -> + false + let ( <= ) ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs + let widen ~prev ~next ~num_iters = let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in if phys_equal prev next || num_iters > max_iter then set_visited false prev else - let prev = set_visited true prev in - let post = join prev next in - if ( <= ) ~lhs:post ~rhs:prev then set_visited false post else post + let visited_prev = set_visited true prev in + let post = join_up_to_imply visited_prev next in + if ( <= ) ~lhs:post ~rhs:prev then set_visited false prev else post let pp = Disjuncts.pp @@ -145,9 +158,12 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct let exec_instr pre_disjuncts extras node instr = List.fold pre_disjuncts ~init:[] ~f:(fun post_disjuncts pre_disjunct -> if pre_disjunct.visited then - (* SUBTLE: ignore pres that we know we have gone through already. This means that the - invariant map at that program point will be junk since they are going to miss some - states, but the overall result will still be ok because the loop heads are ok. *) + (* SUBTLE/WORST HACK EVER: ignore pres that we know we have gone through already. This + means that the invariant map at that program point will be junk since they are going to + miss some states, but the overall result will still be ok because the loop heads are + ok. + + This should really be implemented in {!AbstractInterpreter}. *) post_disjuncts else let disjuncts' = TransferFunctions.exec_instr pre_disjunct.astate extras node instr in diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 329bc77eb..f86aa1f1f 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -283,9 +283,9 @@ let initial = (** 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]. -*) + Given two states [lhs] and [rhs], try to find a bijection [lhs_to_rhs] (with inverse + [rhs_to_lhs]) between the addresses of [lhs] and [rhs] such that [lhs_to_rhs(reachable(lhs)) = + reachable(rhs)] (where addresses are reachable if they are reachable from stack variables). *) module GraphComparison = struct module AddressMap = PrettyPrintable.MakePPMap (AbstractAddress) @@ -339,101 +339,95 @@ module GraphComparison = struct `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] *) + type isograph_relation = + | NotIsomorphic (** no mapping was found that can make LHS the same as the RHS *) + | IsomorphicUpTo of mapping (** [mapping(lhs)] is isomorphic to [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 = + (** can we extend [mapping] so that the subgraph of [lhs] rooted at [addr_lhs] is isomorphic to + the subgraph of [rhs] rooted at [addr_rhs]? *) + let rec isograph_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 + IsomorphicUpTo mapping | `AliasingRHS | `AliasingLHS -> - NotASupergraph + NotIsomorphic | `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) -> + let get_non_empty_cell = function + | None -> + None + | Some (edges, attrs) when Memory.Edges.is_empty edges && Attributes.is_empty attrs -> + (* this can happen because of [register_address] or because we don't care to delete empty + edges when removing edges *) + None + | Some _ as some_cell -> + some_cell + in + let lhs_cell_opt = Memory.find_opt addr_lhs lhs.heap |> get_non_empty_cell in + let rhs_cell_opt = Memory.find_opt addr_rhs rhs.heap |> get_non_empty_cell in + match (lhs_cell_opt, rhs_cell_opt) with + | None, None -> + IsomorphicUpTo mapping + | Some _, None | None, Some _ -> + NotIsomorphic + | Some (edges_rhs, attrs_rhs), Some (edges_lhs, attrs_lhs) -> (* continue the comparison recursively on all edges and attributes *) - if Attributes.subset attrs_rhs attrs_lhs then + if Attributes.equal 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 ) ) + isograph_map_edges ~lhs ~edges_lhs:bindings_lhs ~rhs ~edges_rhs:bindings_rhs mapping + else NotIsomorphic ) - (** check that the supergraph relation can be extended for all edges *) - and supergraph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping = + (** check that the isograph relation can be extended for all edges *) + and isograph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping = match (edges_lhs, edges_rhs) with - | _, [] -> - (* more edges on the LHS => supergraph *) - Supergraph mapping + | [], [] -> + IsomorphicUpTo 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 -> + (* check isograph relation from the destination addresses *) + match isograph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping with + | IsomorphicUpTo 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 + isograph_map_edges ~lhs ~edges_lhs ~rhs ~edges_rhs mapping + | NotIsomorphic -> + NotIsomorphic ) + | _ :: _, _ :: _ | [], _ :: _ | _ :: _, [] -> + NotIsomorphic (** 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 + [stack_lhs] is a isograph 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 = + let rec isograph_map_from_stack ~lhs ~stack_lhs ~rhs ~stack_rhs mapping = match (stack_lhs, stack_rhs) with - | _, [] -> - Supergraph mapping + | [], [] -> + IsomorphicUpTo 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 = + match isograph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping with + | IsomorphicUpTo mapping -> + isograph_map_from_stack ~lhs ~stack_lhs ~rhs ~stack_rhs mapping + | NotIsomorphic -> + NotIsomorphic ) + | _ :: _, _ :: _ | [], _ :: _ | _ :: _, [] -> + NotIsomorphic + + + let isograph_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 + isograph_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 + let is_isograph ~lhs ~rhs mapping = + match isograph_map ~lhs ~rhs mapping with IsomorphicUpTo _ -> true | NotIsomorphic -> false end 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 + phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping let pp fmt {heap; stack} = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index abc606d0e..d446a7045 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,8 +1,8 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60 here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 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 35 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, []