From 007f057f3aaac173049c6e1d994518da0d668dd7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 3 Apr 2018 04:02:19 -0700 Subject: [PATCH] [reactive] kill the changed bit of procedure attributes Summary: This is unused, but the logic for keeping its value up to date was still alive and kicking. I don't know that making use of this flag would be easy: we could just use it in `Ondemand.should_analyze`, but it would be unsound because a procedure might need to be re-analysed becauese its dependencies have changed. Since there's not code to deal with that currently I think it's best to remove it and re-introduce it when we have some idea how to use it. Reviewed By: sblackshear, jeremydubreil Differential Revision: D7444179 fbshipit-source-id: 99a1ec5 --- infer/src/IR/Cfg.ml | 59 -------------- infer/src/IR/Cfg.mli | 4 - infer/src/IR/ProcAttributes.ml | 2 - infer/src/IR/ProcAttributes.mli | 1 - infer/src/IR/Sil.ml | 138 -------------------------------- infer/src/IR/Sil.mli | 5 -- infer/src/IR/SourceFiles.ml | 6 -- infer/src/base/Config.ml | 4 - infer/src/base/Config.mli | 2 - 9 files changed, 221 deletions(-) diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index b11d9130f..427bec53c 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -206,65 +206,6 @@ let inline_java_synthetic_methods cfg = Typ.Procname.Hash.iter f cfg -let mark_unchanged_pdescs ~cfg_old ~cfg_new = - let pdescs_eq (pd1: Procdesc.t) (pd2: Procdesc.t) = - (* map of exp names in pd1 -> exp names in pd2 *) - let exp_map = ref Exp.Map.empty in - (* map of node id's in pd1 -> node id's in pd2 *) - let node_map = ref Procdesc.NodeMap.empty in - (* formals are the same if their types are the same *) - let formals_eq formals1 formals2 = - List.equal ~equal:(fun (_, typ1) (_, typ2) -> Typ.equal typ1 typ2) formals1 formals2 - in - let nodes_eq n1s n2s = - (* 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: Procdesc.Node.t) (n2: Procdesc.Node.t) = - let compare_id (n1: Procdesc.Node.t) (n2: Procdesc.Node.t) = - try - let n1_mapping = Procdesc.NodeMap.find n1 !node_map in - Procdesc.Node.compare n1_mapping n2 - with Not_found -> - (* assume id's are equal and enforce by adding to [id_map] *) - node_map := Procdesc.NodeMap.add n1 n2 !node_map ; - 0 - in - let instrs_eq instrs1 instrs2 = - List.equal - ~equal:(fun i1 i2 -> - let n, exp_map' = Sil.compare_structural_instr i1 i2 !exp_map in - exp_map := exp_map' ; - Int.equal n 0 ) - instrs1 instrs2 - in - Int.equal (compare_id n1 n2) 0 - && List.equal ~equal:Procdesc.Node.equal (Procdesc.Node.get_succs n1) - (Procdesc.Node.get_succs n2) - && List.equal ~equal:Procdesc.Node.equal (Procdesc.Node.get_preds n1) - (Procdesc.Node.get_preds n2) - && instrs_eq (Procdesc.Node.get_instrs n1) (Procdesc.Node.get_instrs n2) - in - try List.for_all2_exn ~f:node_eq n1s n2s with Invalid_argument _ -> false - in - let att1 = Procdesc.get_attributes pd1 and att2 = Procdesc.get_attributes pd2 in - Bool.equal att1.is_defined att2.is_defined && Typ.equal att1.ret_type att2.ret_type - && formals_eq att1.formals att2.formals - && nodes_eq (Procdesc.get_nodes pd1) (Procdesc.get_nodes pd2) - in - let mark_pdesc_if_unchanged pname (new_pdesc: Procdesc.t) = - try - let old_pdesc = Typ.Procname.Hash.find cfg_old pname in - let changed = - (* in continue_capture mode keep the old changed bit *) - Config.continue_capture && (Procdesc.get_attributes old_pdesc).changed - || not (pdescs_eq old_pdesc new_pdesc) - in - (Procdesc.get_attributes new_pdesc).changed <- changed - with Not_found -> () - in - Typ.Procname.Hash.iter mark_pdesc_if_unchanged cfg_new - - let pp_proc_signatures fmt cfg = F.fprintf fmt "METHOD SIGNATURES@\n@." ; let sorted_procs = List.sort ~cmp:Procdesc.compare (get_all_proc_descs cfg) in diff --git a/infer/src/IR/Cfg.mli b/infer/src/IR/Cfg.mli index 361442b19..c05e54c8d 100644 --- a/infer/src/IR/Cfg.mli +++ b/infer/src/IR/Cfg.mli @@ -41,10 +41,6 @@ val save_attributes : SourceFile.t -> t -> unit val inline_java_synthetic_methods : t -> unit (** Inline the java synthetic methods in the cfg (in-place) *) -val mark_unchanged_pdescs : cfg_old:t -> cfg_new:t -> unit -(** compute the list of procedures added or changed in [cfg_new] over [cfg_old] and record the - [changed] attribute in-place in the new cfg. *) - val pp_proc_signatures : Format.formatter -> t -> unit module SQLite : SqliteUtils.Data with type t = t diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index dcc29f38d..4325a7c8d 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -69,7 +69,6 @@ type var_data = {name: Mangled.t; typ: Typ.t; attributes: var_attribute list} [@ type t = { access: PredSymb.access (** visibility access *) ; captured: (Mangled.t * Typ.t) list (** name and type of variables captured in blocks *) - ; mutable changed: bool (** true if proc has changed since last analysis *) ; mutable did_preanalysis: bool (** true if we performed preanalysis on the CFG for this proc *) ; err_log: Errlog.t (** Error log for the procedure *) ; exceptions: string list (** exceptions thrown by the procedure *) @@ -100,7 +99,6 @@ type t = let default proc_name = { access= PredSymb.Default ; captured= [] - ; changed= true ; did_preanalysis= false ; err_log= Errlog.empty () ; exceptions= [] diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index 1591d0736..2f7a64f80 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -47,7 +47,6 @@ type var_data = {name: Mangled.t; typ: Typ.t; attributes: var_attribute list} [@ type t = { access: PredSymb.access (** visibility access *) ; captured: (Mangled.t * Typ.t) list (** name and type of variables captured in blocks *) - ; mutable changed: bool (** true if proc has changed since last analysis *) ; mutable did_preanalysis: bool (** true if we performed preanalysis on the CFG for this proc *) ; err_log: Errlog.t (** Error log for the procedure *) ; exceptions: string list (** exceptions thrown by the procedure *) diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 8793548cb..ea368ff7b 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -1396,144 +1396,6 @@ let instr_sub_ids ~sub_id_binders f instr = (** apply [subst] to all id's in [instr], including binder id's *) let instr_sub (subst: subst) instr = instr_sub_ids ~sub_id_binders:true (apply_sub subst) instr -(** 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 = Exp.Map.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, Exp.Map.add e1 e2 exp_map) - in - match ((e1 : Exp.t), (e2 : Exp.t)) with - | Var _, Var _ -> - 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 [%compare : Typ.t option] 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 _, Lvar _ -> - 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 = Typ.Fieldname.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 compare_structural_instr instr1 instr2 exp_map = - let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map = - let id_typ_compare_structural (id1, typ1) (id2, typ2) = - let n, exp_map = exp_compare_structural (Var id1) (Var id2) exp_map in - if n <> 0 then (n, exp_map) else (Typ.compare typ1 typ2, exp_map) - in - match (id_typ1, id_typ2) with - | Some it1, Some it2 -> - id_typ_compare_structural it1 it2 - | None, None -> - (0, exp_map) - | None, _ -> - (-1, exp_map) - | _, None -> - (1, exp_map) - in - let id_list_compare_structural ids1 ids2 exp_map = - let n = Int.compare (List.length ids1) (List.length ids2) in - if n <> 0 then (n, exp_map) - else - List.fold2_exn - ~f:(fun (n, exp_map) id1 id2 -> - if n <> 0 then (n, exp_map) else exp_compare_structural (Var id1) (Var id2) exp_map ) - ~init:(0, exp_map) ids1 ids2 - in - match (instr1, instr2) with - | Load (id1, e1, t1, _), Load (id2, e2, t2, _) -> - 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) - | Store (e11, t1, e21, _), Store (e12, t2, e22, _) -> - 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, _, true_branch1, ik1), Prune (cond2, _, 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 compare_if_kind ik1 ik2 ) - , exp_map ) - | Call (ret_id1, e1, arg_ts1, _, cf1), Call (ret_id2, e2, arg_ts2, _, cf2) -> - let args_compare_structural args1 args2 exp_map = - let n = Int.compare (List.length args1) (List.length args2) in - if n <> 0 then (n, exp_map) - else - List.fold2_exn - ~f:(fun (n, exp_map) arg1 arg2 -> - if n <> 0 then (n, exp_map) else exp_typ_compare_structural arg1 arg2 exp_map ) - ~init:(0, exp_map) args1 args2 - in - let n, exp_map = id_typ_opt_compare_structural ret_id1 ret_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, exp_map) - else - let n, exp_map = args_compare_structural arg_ts1 arg_ts2 exp_map in - ((if n <> 0 then n else CallFlags.compare cf1 cf2), exp_map) - | Nullify (pvar1, _), Nullify (pvar2, _) -> - exp_compare_structural (Lvar pvar1) (Lvar pvar2) exp_map - | Abstract _, Abstract _ -> - (0, exp_map) - | Remove_temps (temps1, _), Remove_temps (temps2, _) -> - id_list_compare_structural temps1 temps2 exp_map - | Declare_locals (ptl1, _), Declare_locals (ptl2, _) -> - let n = Int.compare (List.length ptl1) (List.length ptl2) in - if n <> 0 then (n, exp_map) - else - List.fold2_exn - ~f:(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) ) - ~init:(0, exp_map) ptl1 ptl2 - | _ -> - (compare_instr instr1 instr2, exp_map) - - let atom_sub subst = atom_expmap (exp_sub subst) let hpred_sub subst = diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 5e2476b6e..1f801165e 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -57,11 +57,6 @@ type instr = val equal_instr : instr -> instr -> bool -val compare_structural_instr : instr -> instr -> Exp.t Exp.Map.t -> int * Exp.t Exp.Map.t -(** 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 skip_instr : instr val instr_is_auxiliary : instr -> bool diff --git a/infer/src/IR/SourceFiles.ml b/infer/src/IR/SourceFiles.ml index f03d370a8..bc6b1c7dc 100644 --- a/infer/src/IR/SourceFiles.ml +++ b/infer/src/IR/SourceFiles.ml @@ -18,12 +18,6 @@ let store_statement = let add source_file cfg tenv = Cfg.inline_java_synthetic_methods cfg ; - ( if Config.incremental_procs then - match Cfg.load source_file with - | Some cfg_old -> - Cfg.mark_unchanged_pdescs ~cfg_old ~cfg_new:cfg - | None -> - () ) ; (* NOTE: it's important to write attribute files to disk before writing cfgs to disk. OndemandCapture module relies on it - it uses existance of the cfg as a barrier to make sure that all attributes were written to disk (but not necessarily flushed) *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 78c7097b6..256cd38b4 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -192,10 +192,6 @@ let global_tenv_filename = ".global.tenv" (** If true, treat calls to no-arg getters as idempotent w.r.t non-nullness *) let idempotent_getters = true -(** If true, changes to code are checked at the procedure level; if false, at the file - level *) -let incremental_procs = true - (** Our Python script does its own argument parsing and will fail with this error on failure *) let infer_py_argparse_error_exit_code = 22 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 71a43b9b7..82b9b2520 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -117,8 +117,6 @@ val global_tenv_filename : string val idempotent_getters : bool -val incremental_procs : bool - val infer_py_argparse_error_exit_code : int val infer_top_results_dir_env_var : string