[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

@@ -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 "@[<v>%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 )
+    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 )
-      in
-      List.rev_append s_from_not_in_intos s_intos
+
+
+    (* 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

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
+  (** 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 supergraph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping =
+  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
+        let get_non_empty_cell = function
           | 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) ->
+              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} =

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, []