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; };