From ceb0062cdda51900ded95544f06679a4018536e4 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 20 Nov 2017 11:20:16 -0800 Subject: [PATCH] [cleanup] kill constant propagation pass in bi-abduction Reviewed By: jeremydubreil Differential Revision: D6321725 fbshipit-source-id: 03a2782 --- infer/src/backend/buckets.ml | 7 - infer/src/backend/interproc.ml | 3 - infer/src/backend/state.ml | 12 +- infer/src/backend/state.mli | 8 -- infer/src/checkers/constantPropagation.ml | 146 --------------------- infer/src/checkers/constantPropagation.mli | 15 --- 6 files changed, 2 insertions(+), 189 deletions(-) delete mode 100644 infer/src/checkers/constantPropagation.ml delete mode 100644 infer/src/checkers/constantPropagation.mli diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index 0d0166d0b..822002ca4 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -97,12 +97,6 @@ let check_access access_opt de_opt = IntLit.iszero n | Exp.Cast (_, e) -> exp_is_null e - | Exp.Var _ | Exp.Lvar _ -> ( - match State.get_const_map () node exp with - | Some Const.Cint n -> - IntLit.iszero n - | _ -> - false ) | _ -> false in @@ -154,4 +148,3 @@ let classify_access desc access_opt de_opt is_nullable = let default_bucket = if is_nullable then Localise.BucketLevel.b1 else Localise.BucketLevel.b5 in let bucket = check_access access_opt de_opt |> Option.value ~default:default_bucket in Localise.error_desc_set_bucket desc bucket - diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 7deba01a1..58ff1cdbd 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -381,10 +381,7 @@ let instrs_get_normal_vars instrs = (** Perform symbolic execution for a node starting from an initial prop *) let do_symbolic_execution proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.node) (prop: Prop.normal Prop.t) (path: Paths.Path.t) = - let pdesc = ProcCfg.Exceptional.proc_desc proc_cfg in State.mark_execution_start node ; - (* build the const map lazily *) - State.set_const_map (ConstantPropagation.build_const_map tenv pdesc) ; let instrs = ProcCfg.Exceptional.instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) Ident.update_name_generator (instrs_get_normal_vars instrs) ; diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 2f67a310e..3405c1268 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -15,8 +15,6 @@ open! IStd module L = Logging module F = Format -type const_map = Procdesc.Node.t -> Exp.t -> Const.t option - (** failure statistics for symbolic execution on a given node *) type failure_stats = { mutable instr_fail: int @@ -33,8 +31,7 @@ type failure_stats = module NodeHash = Procdesc.NodeHash type t = - { mutable const_map: const_map (** Constant map for the procedure *) - ; mutable diverging_states_node: Paths.PathSet.t + { mutable diverging_states_node: Paths.PathSet.t (** Diverging states since the last reset for the node *) ; mutable diverging_states_proc: Paths.PathSet.t (** Diverging states since the last reset for the procedure *) @@ -47,8 +44,7 @@ type t = ; failure_map: failure_stats NodeHash.t (** Map visited nodes to failure statistics *) } let initial () = - { const_map= (fun _ _ -> None) - ; diverging_states_node= Paths.PathSet.empty + { diverging_states_node= Paths.PathSet.empty ; diverging_states_proc= Paths.PathSet.empty ; last_instr= None ; last_node= Procdesc.Node.dummy None @@ -355,7 +351,3 @@ let set_node (node: Procdesc.Node.t) = let set_session (session: int) = !gs.last_session <- session - -let get_const_map () = !gs.const_map - -let set_const_map const_map' = !gs.const_map <- const_map' diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index 39a93758d..68e529545 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -18,11 +18,6 @@ type t val add_diverging_states : Paths.PathSet.t -> unit (** Add diverging states *) -type const_map = Procdesc.Node.t -> Exp.t -> Const.t option - -val get_const_map : unit -> const_map -(** Get the constant map for the current procedure. *) - val get_diverging_states_node : unit -> Paths.PathSet.t (** Get the diverging states for the node *) @@ -104,9 +99,6 @@ val restore_state : t -> unit val save_state : unit -> t (** Return the old state, and revert the current state to the initial one. *) -val set_const_map : const_map -> unit -(** Set the constant map for the current procedure. *) - val set_instr : Sil.instr -> unit (** Set last instruction seen in symbolic execution *) diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml deleted file mode 100644 index 0b5b95610..000000000 --- a/infer/src/checkers/constantPropagation.ml +++ /dev/null @@ -1,146 +0,0 @@ -(* - * Copyright (c) 2014 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd -module L = Logging - -let string_widening_limit = 1000 - -let verbose = false - -(* Merge two constant maps by adding keys as necessary *) -let merge_values _ c1_opt c2_opt = - match (c1_opt, c2_opt) with - | Some Some c1, Some Some c2 when Const.equal c1 c2 -> - Some (Some c1) - | Some c, None | None, Some c -> - Some c - | _ -> - Some None - - -module ConstantMap = Exp.Map - -(** Dataflow struct *) -module ConstantFlow = Dataflow.MakeDF (struct - type t = Const.t option ConstantMap.t [@@deriving compare] - - let equal = [%compare.equal : t] - - let pp fmt constants = - let pp_key fmt = Exp.pp fmt in - let print_kv k = function - | Some v -> - Format.fprintf fmt " %a -> %a@." pp_key k (Const.pp Pp.text) v - | _ -> - Format.fprintf fmt " %a -> None@." pp_key k - in - Format.fprintf fmt "[@." ; - ConstantMap.iter print_kv constants ; - Format.fprintf fmt "]@." - - - let join = ConstantMap.merge merge_values - - let proc_throws _ = Dataflow.DontKnow - - let do_node _ node constants = - let do_instr constants instr = - try - let update key value constants = - ConstantMap.merge merge_values constants (ConstantMap.add key value ConstantMap.empty) - in - let has_class pn name = - match pn with - | Typ.Procname.Java pn_java -> - String.equal (Typ.Procname.java_get_class_name pn_java) name - | _ -> - false - in - let has_method pn name = - match pn with - | Typ.Procname.Java pn_java -> - String.equal (Typ.Procname.java_get_method pn_java) name - | _ -> - false - in - match instr with - | Sil.Load (i, Exp.Lvar p, _, _) -> - (* tmp = var *) - update (Exp.Var i) (ConstantMap.find (Exp.Lvar p) constants) constants - | Sil.Store (Exp.Lvar p, _, Exp.Const c, _) -> - (* var = const *) - update (Exp.Lvar p) (Some c) constants - | Sil.Store (Exp.Lvar p, _, Exp.Var i, _) -> - (* var = tmp *) - update (Exp.Lvar p) (ConstantMap.find (Exp.Var i) constants) constants - (* Handle propagation of string with StringBuilder. Does not handle null case *) - | Sil.Call (_, Exp.Const Const.Cfun pn, [(Exp.Var sb, _)], _, _) - when has_class pn "java.lang.StringBuilder" && has_method pn "" -> - (* StringBuilder. *) - update (Exp.Var sb) (Some (Const.Cstr "")) constants - | Sil.Call (Some (i, _), Exp.Const Const.Cfun pn, [(Exp.Var i1, _)], _, _) - when has_class pn "java.lang.StringBuilder" && has_method pn "toString" -> - (* StringBuilder.toString *) - update (Exp.Var i) (ConstantMap.find (Exp.Var i1) constants) constants - | Sil.Call (Some (i, _), Exp.Const Const.Cfun pn, [(Exp.Var i1, _); (Exp.Var i2, _)], _, _) - when has_class pn "java.lang.StringBuilder" && has_method pn "append" -> ( - match - (* StringBuilder.append *) - (ConstantMap.find (Exp.Var i1) constants, ConstantMap.find (Exp.Var i2) constants) - with - | Some Const.Cstr s1, Some Const.Cstr s2 -> - let s = s1 ^ s2 in - let u = - if String.length s < string_widening_limit then Some (Const.Cstr s) else None - in - update (Exp.Var i) u constants - | _ -> - constants ) - | _ -> - constants - with Not_found -> constants - in - if verbose then ( - L.(debug Analysis Verbose) "Node %i:" (Procdesc.Node.get_id node :> int) ; - L.(debug Analysis Verbose) "%a" pp constants ; - List.iter - ~f:(fun instr -> L.(debug Analysis Verbose) "%a@." (Sil.pp_instr Pp.text) instr) - (Procdesc.Node.get_instrs node) ) ; - let constants = List.fold ~f:do_instr ~init:constants (Procdesc.Node.get_instrs node) in - if verbose then L.(debug Analysis Verbose) "%a@\n@." pp constants ; - ([constants], [constants]) - -end) - -let run tenv proc_desc = - let transitions = ConstantFlow.run tenv proc_desc ConstantMap.empty in - let get_constants node = - match transitions node with - | ConstantFlow.Transition (_, post_states, _) -> - ConstantFlow.join post_states ConstantMap.empty - | ConstantFlow.Dead_state -> - ConstantMap.empty - in - get_constants - - -type const_map = Procdesc.Node.t -> Exp.t -> Const.t option - -(** Build a const map lazily. *) -let build_const_map tenv pdesc = - let const_map = lazy (run tenv pdesc) in - let f node exp = - try - let map = Lazy.force const_map node in - ConstantMap.find exp map - with Not_found -> None - in - f - diff --git a/infer/src/checkers/constantPropagation.mli b/infer/src/checkers/constantPropagation.mli deleted file mode 100644 index 4a4ba33e4..000000000 --- a/infer/src/checkers/constantPropagation.mli +++ /dev/null @@ -1,15 +0,0 @@ -(* - * Copyright (c) 2014 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -type const_map = Procdesc.Node.t -> Exp.t -> Const.t option - -val build_const_map : Tenv.t -> Procdesc.t -> const_map -(** Build a const map lazily. *)