[Infer][incremental] structural comparison of instructions, nodes, expressions

Summary:
Procdesc comparison can be fragile because internal variable names
and source positions in a procedure can vary even if the procedure stays exactly the
same. This diff makes pdesc comparisons less fragile by defining structural comparsions
over instructions, nodes and expressions. These structural comparsions work by lazily
creating a mapping between names in the two procdesc's that and checking that the mapped
names are used consistently.

infer/src/backend/cfg.ml

@@ -76,17 +76,35 @@ module Node = struct
   (** compute the list of procedures added or changed in [cfg_new] over [cfg_old] *)
   let mark_unchanged_pdescs cfg_new cfg_old =
     let pdescs_eq pd1 pd2 =
+      (* map of exp names in pd1 -> exp names in pd2 *)
+      let exp_map = ref Sil.ExpMap.empty in
+      (* map of node id's in pd1 -> node id's in pd2 *)
+      let id_map = ref IntMap.empty in
       (* formals are the same if their types are the same *)
       let formals_eq formals1 formals2 =
         list_equal (fun (_, typ1) (_, typ2) -> Sil.typ_compare typ1 typ2) formals1 formals2 in
       let nodes_eq n1s n2s =
-        (* nodes are the same if they have the same id, instructions, and succs/preds *)
+        (* nodes are the same if they have the same id, instructions, and succs/preds up to renaming
+           with [exp_map] and [id_map] *)
         let node_eq n1 n2 =
-          let id_compare n1 n2 = Pervasives.compare n1.nd_id n2.nd_id in
+          let id_compare n1 n2 =
+            let id1, id2 = n1.nd_id, n2.nd_id in
+            try
+              let id1_mapping = IntMap.find id1 !id_map in
+              Pervasives.compare id1_mapping id2
+            with
+              Not_found ->
+                (* assume id's are equal and enforce by adding to [id_map] *)
+                id_map := IntMap.add id1 id2 !id_map;
+                0 in
           let instrs_eq instrs1 instrs2 =
-            (* TODO (t7941664) : Sil.instr_compare looks at locs and variable names. we could mark
+            list_equal
-               more code as unchanged if we ignored these details. *)
+              (fun i1 i2 ->
-            list_equal (fun i1 i2 -> Sil.instr_compare i1 i2) instrs1 instrs2 in
+                 let n, exp_map' = Sil.instr_compare_structural i1 i2 !exp_map in
+                 exp_map := exp_map';
+                 n)
+              instrs1
+              instrs2 in
           id_compare n1 n2 = 0 &&
           list_equal id_compare n1.nd_succs n2.nd_succs &&
           list_equal id_compare n1.nd_preds n2.nd_preds &&

infer/src/backend/config.ml

@@ -182,7 +182,7 @@ let idempotent_getters = ref true
 let in_child_process = ref false
 
 (** if true, changes to code are checked at the procedure level; if false, at the file level *)
-let incremental_procs = ref false
+let incremental_procs = ref true
 
 (** Flag to activate intraprocedural-only analysis *)
 let intraprocedural = ref false

infer/src/backend/inferanalyze.ml

@@ -697,8 +697,7 @@ let compute_files_changed_map _exe_env (source_dirs : DB.source_dir list) exclud
         else cg_get_changed_procs exe_env source_dir cg in
       if changed_procs != [] then
         let file_pname = source_file_to_pname (Cg.get_source cg) in
-        let defined_procs = Cg.get_defined_nodes cg in
+        Procname.Map.add file_pname changed_procs files_changed_map
-        Procname.Map.add file_pname defined_procs files_changed_map
       else files_changed_map in
     list_fold_left cg_get_files_changed files_changed_map cg_list in
   let exe_env = Exe_env.freeze _exe_env in

infer/src/backend/sil.ml

@@ -3564,6 +3564,131 @@ let instr_compare instr1 instr2 = match instr1, instr2 with
       let n = exp_compare e1 e2 in
       if n <> 0 then n else loc_compare loc1 loc2
 
+(** compare expressions from different procedures without considering loc's, ident's, and pvar's.
+    the [exp_map] param gives a mapping of names used in the procedure of [e1] to names used in the
+    procedure of [e2] *)
+let rec exp_compare_structural e1 e2 exp_map =
+  let compare_exps_with_map e1 e2 exp_map =
+    try
+      let e1_mapping = ExpMap.find e1 exp_map in
+      exp_compare e1_mapping e2, exp_map
+    with Not_found ->
+      (* assume e1 and e2 equal, enforce by adding to [exp_map] *)
+      0, ExpMap.add e1 e2 exp_map in
+  match (e1, e2) with
+  | Var id1, Var id2 -> compare_exps_with_map e1 e2 exp_map
+  | UnOp (o1, e1, to1), UnOp (o2, e2, to2) ->
+      let n = unop_compare o1 o2 in
+      if n <> 0 then n, exp_map
+      else
+        let n, exp_map = exp_compare_structural e1 e2  exp_map in
+        (if n <> 0 then n else typ_opt_compare to1 to2), exp_map
+  | BinOp (o1, e1, f1), BinOp (o2, e2, f2) ->
+      let n = binop_compare o1 o2 in
+      if n <> 0 then n, exp_map
+      else
+        let n, exp_map = exp_compare_structural e1 e2 exp_map in
+        if n <> 0 then n, exp_map
+        else exp_compare_structural f1 f2 exp_map
+  | Cast (t1, e1), Cast(t2, e2) ->
+      let n, exp_map = exp_compare_structural e1 e2 exp_map in
+      (if n <> 0 then n else typ_compare t1 t2), exp_map
+  | Lvar i1, Lvar i2 -> compare_exps_with_map e1 e2 exp_map
+  | Lfield (e1, f1, t1), Lfield (e2, f2, t2) ->
+      let n, exp_map = exp_compare_structural e1 e2 exp_map in
+      (if n <> 0 then n
+       else
+         let n = fld_compare f1 f2 in
+         if n <> 0 then n else typ_compare t1 t2), exp_map
+  | Lindex (e1, f1), Lindex (e2, f2) ->
+      let n, exp_map = exp_compare_structural e1 e2 exp_map in
+      if n <> 0 then n, exp_map
+      else exp_compare_structural f1 f2 exp_map
+  | _ -> exp_compare e1 e2, exp_map
+
+let exp_typ_compare_structural (e1, t1) (e2, t2) exp_map =
+  let n, exp_map = exp_compare_structural e1 e2 exp_map in
+  (if n <> 0 then n else typ_compare t1 t2), exp_map
+
+(** compare instructions from different procedures without considering loc's, ident's, and pvar's.
+    the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
+    used in the procedure of [instr2] *)
+let instr_compare_structural instr1 instr2 exp_map =
+  let id_list_compare_structural ids1 ids2 exp_map =
+    let n = Pervasives.compare (list_length ids1) (list_length ids2) in
+    if n <> 0 then n, exp_map
+    else
+      list_fold_left2
+        (fun (n, exp_map) id1 id2 ->
+           if n <> 0 then (n, exp_map)
+           else exp_compare_structural (Var id1) (Var id2) exp_map)
+        (0, exp_map)
+        ids1
+        ids2 in
+  match instr1, instr2 with
+  | Letderef (id1, e1, t1, loc1), Letderef (id2, e2, t2, loc2) ->
+      let n, exp_map = exp_compare_structural (Var id1) (Var id2) exp_map in
+      if n <> 0 then n, exp_map
+      else
+        let n, exp_map = exp_compare_structural e1 e2 exp_map in
+        (if n <> 0 then n else typ_compare t1 t2), exp_map
+  | Set (e11, t1, e21, loc1), Set (e12, t2, e22, loc2) ->
+      let n, exp_map = exp_compare_structural e11 e12 exp_map in
+      if n <> 0 then n, exp_map
+      else
+        let n = typ_compare t1 t2 in
+        if n <> 0 then n, exp_map
+        else exp_compare_structural e21 e22 exp_map
+  | Prune (cond1, loc1, true_branch1, ik1), Prune (cond2, loc2, true_branch2, ik2) ->
+      let n, exp_map = exp_compare_structural cond1 cond2 exp_map in
+      (if n <> 0 then n
+       else let n = bool_compare true_branch1 true_branch2 in
+         if n <> 0 then n
+         else Pervasives.compare ik1 ik2), exp_map
+  | Call (ret_ids1, e1, arg_ts1, loc1, cf1), Call (ret_ids2, e2, arg_ts2, loc2, cf2) ->
+      let args_compare_structural args1 args2 exp_map =
+        let n = Pervasives.compare (list_length args1) (list_length args2) in
+        if n <> 0 then n, exp_map
+        else
+          list_fold_left2
+            (fun (n, exp_map) arg1 arg2 ->
+               if n <> 0 then (n, exp_map)
+               else exp_typ_compare_structural arg1 arg2 exp_map)
+            (0, exp_map)
+            args1
+            args2 in
+      let n, exp_map = id_list_compare_structural ret_ids1 ret_ids2 exp_map in
+      if n <> 0 then n, exp_map
+      else let n, exp_map = exp_compare_structural e1 e2 exp_map in
+        if n <> 0 then n, exp_map
+        else
+          let n, exp_map = args_compare_structural arg_ts1 arg_ts2 exp_map in
+          (if n <> 0 then n else call_flags_compare cf1 cf2), exp_map
+  | Nullify (pvar1, loc1, deallocate1), Nullify (pvar2, loc2, deallocate2) ->
+      let n, exp_map = exp_compare_structural (Lvar pvar1) (Lvar pvar2) exp_map in
+      (if n <> 0 then n else bool_compare deallocate1 deallocate2), exp_map
+  | Abstract loc1, Abstract loc2 -> 0, exp_map
+  | Remove_temps (temps1, loc1), Remove_temps (temps2, loc2) ->
+      id_list_compare_structural temps1 temps2 exp_map
+  | Stackop (stackop1, loc1), Stackop (stackop2, loc2) ->
+      Pervasives.compare stackop1 stackop2, exp_map
+  | Declare_locals (ptl1, loc1), Declare_locals (ptl2, loc2) ->
+      let n = Pervasives.compare (list_length ptl1) (list_length ptl2) in
+      if n <> 0 then n, exp_map
+      else
+        list_fold_left2
+          (fun (n, exp_map) (pv1, t1) (pv2, t2) ->
+             if n <> 0 then (n, exp_map)
+             else
+               let n, exp_map = exp_compare_structural (Lvar pv1) (Lvar pv2) exp_map in
+               if n <> 0 then n, exp_map else typ_compare t1 t2, exp_map)
+          (0, exp_map)
+          ptl1
+          ptl2
+  | Goto_node (e1, loc1), Goto_node (e2, loc2) ->
+      exp_compare_structural e1 e2 exp_map
+  | _ -> instr_compare instr1 instr2, exp_map
+
 let atom_sub subst =
   atom_expmap (exp_sub subst)
 

infer/src/backend/sil.mli

@@ -739,6 +739,11 @@ val exp_typ_compare : (exp * typ) -> (exp * typ) -> int
 
 val instr_compare : instr -> instr -> int
 
+(** compare instructions from different procedures without considering loc's, ident's, and pvar's.
+    the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
+    used in the procedure of [instr2] *)
+val instr_compare_structural : instr -> instr -> exp ExpMap.t -> (int * exp ExpMap.t)
+
 val exp_list_compare : exp list -> exp list -> int
 
 val exp_list_equal : exp list -> exp list -> bool