From d850492ffe729c9cdbff8741e7910f14bc3a9ea1 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 4 Aug 2017 10:37:23 -0700 Subject: [PATCH] [cleanup] kill condition_is_assignment check Summary: This is unused, as far as I can tell. If we want to revive it, we can do it in AL or as a simple checker; it certainly doesn't require the full might of bi-abduction. Reviewed By: jeremydubreil Differential Revision: D5556325 fbshipit-source-id: e3895c2 --- infer/src/IR/Exceptions.ml | 4 -- infer/src/IR/Exceptions.mli | 2 - infer/src/IR/Localise.ml | 7 --- infer/src/IR/Localise.mli | 4 -- infer/src/backend/errdesc.ml | 3 - infer/src/backend/errdesc.mli | 3 - infer/src/backend/interproc.ml | 101 --------------------------------- 7 files changed, 124 deletions(-) diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 609161d2a..e29f22af1 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -63,8 +63,6 @@ exception Codequery of Localise.error_desc exception Comparing_floats_for_equality of Localise.error_desc * L.ml_loc -exception Condition_is_assignment of Localise.error_desc * L.ml_loc - exception Condition_always_true_false of Localise.error_desc * bool * L.ml_loc exception Context_leak of Localise.error_desc * L.ml_loc @@ -219,8 +217,6 @@ let recognize_exception exn = (name, desc, Some ml_loc, Exn_user, Medium, None, Nocat) | Custom_error (error_msg, desc) -> (Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker) - | Condition_is_assignment (desc, ml_loc) - -> (Localise.condition_is_assignment, desc, Some ml_loc, Exn_user, Medium, None, Nocat) | Dangling_pointer_dereference (dko, desc, ml_loc) -> let visibility = match dko with diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 1cc57d366..c8e850cb0 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -63,8 +63,6 @@ exception Comparing_floats_for_equality of Localise.error_desc * Logging.ml_loc exception Condition_always_true_false of Localise.error_desc * bool * Logging.ml_loc -exception Condition_is_assignment of Localise.error_desc * Logging.ml_loc - exception Context_leak of Localise.error_desc * Logging.ml_loc exception Custom_error of string * Localise.error_desc diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index a3bc43570..2f3e95725 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -71,8 +71,6 @@ let condition_always_false = from_string "CONDITION_ALWAYS_FALSE" let condition_always_true = from_string "CONDITION_ALWAYS_TRUE" -let condition_is_assignment = from_string "CONDITION_IS_ASSIGNMENT" - let context_leak = from_string "CONTEXT_LEAK" let dangling_pointer_dereference = from_string "DANGLING_POINTER_DEREFERENCE" @@ -829,11 +827,6 @@ let desc_comparing_floats_for_equality loc = let tags = Tags.create () in {no_desc with descriptions= [("Comparing floats for equality " ^ at_line tags loc)]; tags= !tags} -let desc_condition_is_assignment loc = - let tags = Tags.create () in - { no_desc with - descriptions= [("Boolean condition is an assignment " ^ at_line tags loc)]; tags= !tags } - let desc_condition_always_true_false i cond_str_opt loc = let tags = Tags.create () in let value = match cond_str_opt with None -> "" | Some s -> s in diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 36060f3e9..8960b1cf0 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -63,8 +63,6 @@ val condition_always_false : t val condition_always_true : t -val condition_is_assignment : t - val context_leak : t val dangling_pointer_dereference : t @@ -315,8 +313,6 @@ val desc_class_cast_exception : val desc_comparing_floats_for_equality : Location.t -> error_desc -val desc_condition_is_assignment : Location.t -> error_desc - val desc_condition_always_true_false : IntLit.t -> string option -> Location.t -> error_desc val desc_unreachable_code_after : Location.t -> error_desc diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index db71effb5..b9f333ff0 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -1146,9 +1146,6 @@ let explain_frontend_warning loc = Localise.desc_frontend_warning loc (** explain a comparing floats for equality *) let explain_comparing_floats_for_equality loc = Localise.desc_comparing_floats_for_equality loc -(** explain a condition is an assignment *) -let explain_condition_is_assignment loc = Localise.desc_condition_is_assignment loc - (** explain a condition which is always true or false *) let explain_condition_always_true_false tenv i cond node loc = let cond_str_opt = diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index c27e9d375..14d201e1b 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -85,9 +85,6 @@ val explain_return_expression_required : Location.t -> Typ.t -> Localise.error_d val explain_comparing_floats_for_equality : Location.t -> Localise.error_desc (** explain a comparing floats for equality *) -val explain_condition_is_assignment : Location.t -> Localise.error_desc -(** explain a condition is an assignment *) - val explain_condition_always_true_false : Tenv.t -> IntLit.t -> Exp.t -> Procdesc.Node.t -> Location.t -> Localise.error_desc (** explain a condition which is always true or false *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index e0fce0a0a..aac48b616 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -351,113 +351,12 @@ let instrs_get_normal_vars instrs = in List.iter ~f:do_instr instrs ; Sil.fav_filter_ident fav Ident.is_normal ; Sil.fav_to_list fav -(* checks that boolean conditions on a conditional are assignment *) -(* The check is done as follows: we check that the successors or a node that make an *) -(* set instruction are prune nodes, they are all at the same location and the condition on*) -(* which they prune is the variable (or the negation) which was set in the set instruction *) -(* we exclude function calls: if (g(x,y)) ....*) -(* we check that prune nodes have simple guards: a var or its negation*) -let check_assignement_guard pdesc node = - let pname = Procdesc.get_proc_name pdesc in - let verbose = false in - let node_contains_call n = - let instrs = Procdesc.Node.get_instrs n in - let is_call = function Sil.Call _ -> true | _ -> false in - List.exists ~f:is_call instrs - in - let is_set_instr i = match i with Sil.Store _ -> true | _ -> false in - let is_prune_instr i = match i with Sil.Prune _ -> true | _ -> false in - let is_load_instr i = match i with Sil.Load _ -> true | _ -> false in - let is_frontend_tmp e = match e with Exp.Lvar pv -> Pvar.is_frontend_tmp pv | _ -> false in - let succs = Procdesc.Node.get_succs node in - let l_node = Procdesc.Node.get_last_loc node in - (* e is prune if in all successors prune nodes we have for some temp n$1: *) - (* n$1=*&e;Prune(n$1) or n$1=*&e;Prune(!n$1) *) - let is_prune_exp e = - let prune_var n = - let ins = Procdesc.Node.get_instrs n in - let pi = List.filter ~f:is_prune_instr ins in - let leti = List.filter ~f:is_load_instr ins in - match (pi, leti) with - | [(Sil.Prune (Exp.Var e1, _, _, _))], [(Sil.Load (e2, e', _, _))] - | [(Sil.Prune (Exp.UnOp (Unop.LNot, Exp.Var e1, _), _, _, _))], [(Sil.Load (e2, e', _, _))] - when Ident.equal e1 e2 - -> if verbose then L.d_strln ("Found " ^ Exp.to_string e' ^ " as prune var") ; - [e'] - | _ - -> [] - in - let prune_vars = List.concat_map ~f:(fun n -> prune_var n) succs in - List.for_all ~f:(fun e' -> Exp.equal e' e) prune_vars - in - let succs_loc = List.map ~f:(fun n -> Procdesc.Node.get_loc n) succs in - let succs_are_all_prune_nodes () = - List.for_all - ~f:(fun n -> - match Procdesc.Node.get_kind n with Procdesc.Node.Prune_node _ -> true | _ -> false) - succs - in - let succs_same_loc_as_node () = - if verbose then ( - L.d_str ("LOCATION NODE: line: " ^ string_of_int l_node.Location.line) ; - L.d_strln " " ) ; - List.for_all - ~f:(fun l -> - if verbose then ( - L.d_str ("LOCATION l: line: " ^ string_of_int l.Location.line) ; - L.d_strln " " ) ; - Location.equal l l_node) - succs_loc - in - (* check that the guards of the succs are a var or its negation *) - let succs_have_simple_guards () = - let check_instr = function - | Sil.Prune (Exp.Var _, _, _, _) - -> true - | Sil.Prune (Exp.UnOp (Unop.LNot, Exp.Var _, _), _, _, _) - -> true - | Sil.Prune _ - -> false - | _ - -> true - in - let check_guard n = List.for_all ~f:check_instr (Procdesc.Node.get_instrs n) in - List.for_all ~f:check_guard succs - in - if Config.curr_language_is Config.Clang && succs_are_all_prune_nodes () - && succs_same_loc_as_node () && succs_have_simple_guards () - then ( - let instr = Procdesc.Node.get_instrs node in - match succs_loc with - (* at this point all successors are at the same location, so we can take the first*) - | loc_succ :: _ - -> ( - let set_instr_at_succs_loc = - List.filter - ~f:(fun i -> Location.equal (Sil.instr_get_loc i) loc_succ && is_set_instr i) - instr - in - match set_instr_at_succs_loc with - | [(Sil.Store (e, _, _, _))] - -> (* we now check if e is the same expression used to prune*) - if is_prune_exp e && not (node_contains_call node && is_frontend_tmp e) then - let desc = Errdesc.explain_condition_is_assignment l_node in - let exn = Exceptions.Condition_is_assignment (desc, __POS__) in - Reporting.log_warning_deprecated pname ~loc:l_node exn - else () - | _ - -> () ) - | _ - -> if verbose then L.d_strln "NOT FOUND loc_succ" ) - else () - (** Perform symbolic execution for a node starting from an initial prop *) let do_symbolic_execution pdesc handle_exn tenv (node: Procdesc.Node.t) (prop: Prop.normal Prop.t) (path: Paths.Path.t) = State.mark_execution_start node ; (* build the const map lazily *) State.set_const_map (ConstantPropagation.build_const_map tenv pdesc) ; - check_assignement_guard pdesc node ; let instrs = Procdesc.Node.get_instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) Ident.update_name_generator (instrs_get_normal_vars instrs) ;