diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index cd3abdcef..1d93d49ae 100644 --- a/infer/src/backend/cfg.ml +++ b/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 - more code as unchanged if we ignored these details. *) - list_equal (fun i1 i2 -> Sil.instr_compare i1 i2) instrs1 instrs2 in + list_equal + (fun i1 i2 -> + 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 && diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 1bda871a4..52c2766bd 100644 --- a/infer/src/backend/config.ml +++ b/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 diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 999a61bd1..375d56d60 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/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 defined_procs files_changed_map + Procname.Map.add file_pname changed_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 diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 87f0c5c2d..6b4f22ade 100644 --- a/infer/src/backend/sil.ml +++ b/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) diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 937a384f8..40171fdd6 100644 --- a/infer/src/backend/sil.mli +++ b/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