[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

@@ -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 =

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)
+(** 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 "@[<v>{ rhs_to_lhs=@[<hv2>%a@];@,lhs_to_rhs=@[<hv2>%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
-         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
+          `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

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

infer/tests/codetoanalyze/cpp/pulse/join.cpp

@@ -8,6 +8,11 @@
 #include <stdlib.h>
 #include <vector>
 
+void basic_loop_count_ok(int n) {
+  for (int i = 0; i < n; i++) {
+  }
+}
+
 struct foo {
   int* val;
 };