From 37f943a3fa1e9395d8b8c025f050a999cbe22994 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Sat, 2 Jul 2016 13:38:01 -0700 Subject: [PATCH] unifying checking of temporary variables Reviewed By: jeremydubreil Differential Revision: D3473066 fbshipit-source-id: 871b878 --- infer/src/IR/Pvar.re | 20 +++++++++++++++ infer/src/IR/Pvar.rei | 4 +++ infer/src/backend/errdesc.ml | 29 ++++------------------ infer/src/backend/errdesc.mli | 6 ----- infer/src/backend/interproc.ml | 6 ++--- infer/src/checkers/idenv.ml | 4 +-- infer/src/checkers/repeatedCallsChecker.ml | 2 +- infer/src/eradicate/typeCheck.ml | 9 +++---- 8 files changed, 39 insertions(+), 41 deletions(-) diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re index b24a9ff7c..5f42567f5 100644 --- a/infer/src/IR/Pvar.re +++ b/infer/src/IR/Pvar.re @@ -260,6 +260,26 @@ let is_this pvar => Mangled.equal (get_name pvar) (Mangled.from_string "this"); let is_return pv => get_name pv == Ident.name_return; +/** return true if [pvar] is a temporary variable generated by the frontend */ +let is_frontend_tmp pvar => { + /* Check whether the program variable is a temporary one generated by the Clang frontend */ + let is_clang_tmp name => string_is_prefix "_tmp" name; + /* Check whether the program variable is a temporary one generated by sawja */ + let is_sawja_tmp name => + string_is_prefix "$irvar" name || string_is_prefix "$T" name || string_is_prefix "$bc" name; + let name = to_string pvar; + switch pvar.pv_kind { + | Local_var pname => + if (Procname.is_java pname) { + is_sawja_tmp name + } else { + is_clang_tmp name + } + | _ => false + } +}; + + /** Turn an ordinary program variable into a callee program variable */ let to_callee pname pvar => switch pvar.pv_kind { diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei index 1b7ad4108..26a772b1c 100644 --- a/infer/src/IR/Pvar.rei +++ b/infer/src/IR/Pvar.rei @@ -83,6 +83,10 @@ let is_return: t => bool; let is_this: t => bool; +/** return true if [pvar] is a temporary variable generated by the frontend */ +let is_frontend_tmp: t => bool; + + /** [mk name proc_name suffix] creates a program var with the given function name and suffix */ let mk: Mangled.t => Procname.t => t; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 494677e5c..992d874b0 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -194,25 +194,6 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option = else None | _ -> None -(** Check whether the program variable is a temporary one generated by CIL *) -let pvar_is_cil_tmp pvar = - Pvar.is_local pvar && - let name = Pvar.to_string pvar in - string_is_prefix "_tmp" name - -(** Check whether the program variable is a temporary one generated by sawja *) -let pvar_is_sawja_tmp pvar = - Pvar.is_local pvar && - let name = Pvar.to_string pvar in - string_is_prefix "$irvar" name || - string_is_prefix "$T" name || - string_is_prefix "$bc" name - -(** Check whether the program variable is a temporary generated by the front-end *) -let pvar_is_frontend_tmp pvar = - if !Config.curr_language = Config.Java then pvar_is_sawja_tmp pvar - else pvar_is_cil_tmp pvar - (** Find the Letderef instruction used to declare normal variable [id], and return the expression dereferenced to initialize [id] *) let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp option = @@ -288,7 +269,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = | Some de -> Some (Sil.Dderef de)) | Sil.Lvar pvar -> if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ()); - if pvar_is_frontend_tmp pvar then + if Pvar.is_frontend_tmp pvar then begin match find_program_variable_assignment node pvar with | None -> None @@ -361,7 +342,7 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = Some (Sil.Dconst c) | Sil.Lvar pv -> if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ()); - if pvar_is_frontend_tmp pv + if Pvar.is_frontend_tmp pv then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e else Some (Sil.Dpvaraddr pv) | Sil.Var id when Ident.is_normal id -> @@ -510,7 +491,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = let check_pvar pvar = (* check that pvar is local or global and has the same type as the leaked hpred *) (Pvar.is_local pvar || Pvar.is_global pvar) && - not (pvar_is_frontend_tmp pvar) && + not (Pvar.is_frontend_tmp pvar) && match hpred_typ_opt, find_typ_without_ptr prop pvar with | Some (Sil.Sizeof (t1, _, _)), Some (Sil.Sizeof (Typ.Tptr (t2_, _), _, _)) -> (try @@ -545,7 +526,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = | _ -> [] in let nullify_pvars = IList.flatten (IList.map get_nullify node_instrs) in let nullify_pvars_notmp = - IList.filter (fun pvar -> not (pvar_is_frontend_tmp pvar)) nullify_pvars in + IList.filter (fun pvar -> not (Pvar.is_frontend_tmp pvar)) nullify_pvars in value_str_from_pvars_vpath nullify_pvars_notmp vpath | Some (Sil.Set (lexp, _, _, _)) when vpath = None -> if verbose @@ -609,7 +590,7 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option = | Sil.Eexp (e, _) when Sil.exp_equal exp e -> let sigma' = (IList.rev_append sigma_acc' sigma_todo') in (match lexp with - | Sil.Lvar pv when not (pvar_is_frontend_tmp pv) -> + | Sil.Lvar pv when not (Pvar.is_frontend_tmp pv) -> let typo = match texp with | Sil.Sizeof (typ, _, _) -> Some typ | _ -> None in diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 83dc439e5..8fb453eb6 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -130,12 +130,6 @@ val explain_memory_access : Localise.deref_str -> 'a Prop.t -> Location.t -> Loc val explain_null_test_after_dereference : Sil.exp -> Cfg.Node.t -> int -> Location.t -> Localise.error_desc -(** Check whether the program variable is a temporary one generated by CIL *) -val pvar_is_cil_tmp : Pvar.t -> bool - -(** Check whether the program variable is a temporary generated by the front-end *) -val pvar_is_frontend_tmp : Pvar.t -> bool - (** Print a warning to the err stream at the given location (note: only prints in developer mode) *) val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index f8b7c05b0..6d99935ea 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -384,10 +384,10 @@ let check_assignement_guard node = match i with | Sil.Letderef _ -> true | _ -> false in - let is_cil_tmp e = + let is_frontend_tmp e = match e with | Sil.Lvar pv -> - Errdesc.pvar_is_cil_tmp pv + Pvar.is_frontend_tmp pv | _ -> false in let succs = Cfg.Node.get_succs node in let l_node = Cfg.Node.get_last_loc node in @@ -453,7 +453,7 @@ let check_assignement_guard node = (match set_instr_at_succs_loc with | [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*) - if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) then ( + 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 let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in diff --git a/infer/src/checkers/idenv.ml b/infer/src/checkers/idenv.ml index e5e9cbc15..2c60cc0ca 100644 --- a/infer/src/checkers/idenv.ml +++ b/infer/src/checkers/idenv.ml @@ -50,7 +50,7 @@ let expand_expr idenv e = match e with let expand_expr_temps idenv node _exp = let exp = expand_expr idenv _exp in match exp with - | Sil.Lvar pvar when Errdesc.pvar_is_frontend_tmp pvar -> + | Sil.Lvar pvar when Pvar.is_frontend_tmp pvar -> (match Errdesc.find_program_variable_assignment node pvar with | None -> exp | Some (_, id) -> @@ -61,5 +61,5 @@ let expand_expr_temps idenv node _exp = let exp_is_temp idenv e = match expand_expr idenv e with | Sil.Lvar pvar -> - Errdesc.pvar_is_frontend_tmp pvar + Pvar.is_frontend_tmp pvar | _ -> false diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index 501b6a356..51f20006c 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -113,7 +113,7 @@ struct let filter_arg (e, _) = match e with | Sil.Lvar pvar -> (* same temporary variable does not imply same value *) - not (Errdesc.pvar_is_frontend_tmp pvar) + not (Pvar.is_frontend_tmp pvar) | _ -> true in IList.for_all filter_arg args in diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 2fd4857f0..ed3e59429 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -117,7 +117,7 @@ module ComplexExpressions = struct | Sil.Dretcall _ -> case_not_handled () | Sil.Dpvar pv - | Sil.Dpvaraddr pv when not (Errdesc.pvar_is_frontend_tmp pv) -> + | Sil.Dpvaraddr pv when not (Pvar.is_frontend_tmp pv) -> Pvar.to_string pv | Sil.Dpvar _ | Sil.Dpvaraddr _ (* front-end variable -- this should not happen) *) -> @@ -328,8 +328,7 @@ let typecheck_instr Errdesc.find_normal_variable_funcall node' id <> None -> handle_function_call node' id | Sil.Lvar pvar when - ComplexExpressions.functions_idempotent () && - Errdesc.pvar_is_frontend_tmp pvar -> + ComplexExpressions.functions_idempotent () && Pvar.is_frontend_tmp pvar -> let frontend_variable_assignment = Errdesc.find_program_variable_assignment node pvar in begin @@ -441,7 +440,7 @@ let typecheck_instr let typestate' = handle_pvar typestate pvar in let curr_node = TypeErr.InstrRef.get_node instr_ref in let frontent_variable_assignment = - if Errdesc.pvar_is_frontend_tmp pvar + if Pvar.is_frontend_tmp pvar then Errdesc.find_program_variable_assignment curr_node pvar else None in match frontent_variable_assignment with @@ -1058,7 +1057,7 @@ let typecheck_instr let c' = Idenv.expand_expr idenv _cond in if not (Sil.exp_equal c' _cond) then normalize_cond _node c' else _node, c' - | Sil.Lvar pvar when Errdesc.pvar_is_frontend_tmp pvar -> + | Sil.Lvar pvar when Pvar.is_frontend_tmp pvar -> (match handle_assignment_in_condition pvar with | None -> (match Errdesc.find_program_variable_assignment _node pvar with