From 09242fc71156f9b1a8b07a26e899edbe0ba09368 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 24 Sep 2015 08:58:41 -0600 Subject: [PATCH] [Infer][backend] Refactoring attribute categories so as not to conflate resource and undefined attrs Summary: `get_resource_or_undef` attribute is weird and was causing problems for me in another diff. This diff refactors the attribute categories to make resource and undef separate. --- infer/src/backend/abs.ml | 10 ++++++---- infer/src/backend/errdesc.ml | 2 +- infer/src/backend/prop.ml | 5 ++++- infer/src/backend/prop.mli | 7 +++++-- infer/src/backend/rearrange.ml | 3 ++- infer/src/backend/sil.ml | 8 +++++--- infer/src/backend/sil.mli | 2 ++ infer/src/backend/symExec.ml | 8 ++++---- infer/src/backend/tabulation.ml | 14 ++++++++------ 9 files changed, 37 insertions(+), 22 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index fb4431b76..6d7fb2896 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1277,13 +1277,15 @@ let check_junk ?original_prop pname tenv prop = (* find the alloc attribute of one of the roots of hpred, if it exists *) let res = ref None in let do_entry e = - match Prop.get_resource_undef_attribute prop e with + match Prop.get_resource_attribute prop e with | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire }) as a) -> L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Const (Sil.Cattribute a)); L.d_ln (); res := Some a - | Some (Sil.Aundef _ as a) -> - res := Some a - | _ -> () in + | _ -> + (match Prop.get_undef_attribute prop e with + | Some (Sil.Aundef _ as a) -> + res := Some a + | _ -> ()) in list_iter do_entry entries; !res in L.d_decrease_indent 1; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 6852483fb..4c80becea 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -20,7 +20,7 @@ let pvar_to_string pvar = (** Check whether the hpred is a |-> representing a resource in the Racquire state *) let hpred_is_open_resource prop = function | Sil.Hpointsto(e, _, _) -> - (match Prop.get_resource_undef_attribute prop e with + (match Prop.get_resource_attribute prop e with | Some (Sil.Aresource { Sil.ra_kind = Sil.Racquire; Sil.ra_res = res }) -> Some res | _ -> None) | _ -> diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index d2de57100..32e984cdb 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1762,7 +1762,10 @@ let get_attribute prop exp category = atts) with Not_found -> None -let get_resource_undef_attribute prop exp = +let get_undef_attribute prop exp = + get_attribute prop exp Sil.ACundef + +let get_resource_attribute prop exp = get_attribute prop exp Sil.ACresource let get_taint_attribute prop exp = diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 47bbd25f1..7fbb2e36d 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -271,8 +271,11 @@ val atom_get_exp_attribute : atom -> (Sil.exp * Sil.attribute) option (** Get the attributes associated to the expression, if any *) val get_exp_attributes : 'a t -> exp -> attribute list -(** Get the resource attribute associated to the expression, if any, or undefined *) -val get_resource_undef_attribute : 'a t -> exp -> attribute option +(** Get the undef attribute associated to the expression, if any *) +val get_undef_attribute : 'a t -> exp -> attribute option + +(** Get the resource attribute associated to the expression, if any *) +val get_resource_attribute : 'a t -> exp -> attribute option (** Get the taint attribute associated to the expression, if any *) val get_taint_attribute : 'a t -> exp -> attribute option diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index afc5a9600..979bcd2fd 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -970,7 +970,8 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = !Config.report_nullable_inconsistency && !Config.curr_language = Config.Java && not (is_definitely_non_null root prop) && is_only_pt_by_nullable_fld_or_param root in let relevant_attributes_getters = [ - Prop.get_resource_undef_attribute; + Prop.get_resource_attribute; + Prop.get_undef_attribute; ] in let get_relevant_attributes exp = let rec fold_getters = function diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index b4a1ab381..e52f4d723 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -635,6 +635,8 @@ and attribute_category = | ACtaint | ACdiv0 | ACobjc_null + | ACundef + | ACretval (** Constants *) and const = @@ -1131,14 +1133,14 @@ let attribute_category_equal att1 att2 = let attribute_to_category att = match att with | Aresource _ - | Adangling _ - | Aretval _ - | Aundef _ -> ACresource + | Adangling _ -> ACresource | Ataint | Auntaint -> ACtaint | Aautorelease -> ACautorelease | Adiv0 _ -> ACdiv0 | Aobjc_null _ -> ACobjc_null + | Aretval _ -> ACretval + | Aundef _ -> ACundef let attr_is_undef = function | Aundef _ -> true diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index cbf323680..accba19c6 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -270,6 +270,8 @@ and attribute_category = | ACtaint | ACdiv0 | ACobjc_null + | ACundef + | ACretval (** Constants *) and const = diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index d83e969b2..19f0d947d 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -131,7 +131,7 @@ let rec apply_offlist lookup_inst := Some inst_curr; let alloc_attribute_opt = if inst_curr = Sil.Iinitial then None - else Prop.get_resource_undef_attribute p root_lexp in + else Prop.get_undef_attribute p root_lexp in let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in let err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) in let exn = (Exceptions.Uninitialized_value (err_desc, try assert false with Assert_failure x -> x)) in @@ -815,7 +815,7 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc else let res = Tabulation.exe_function_call tenv cfg ret_ids pdesc callee_pname loc actual_params pre path in let is_undef = - Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute pre receiver) in + Option.is_some (Prop.get_undef_attribute pre receiver) in if !Config.footprint && not is_undef then let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *) let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in @@ -1561,7 +1561,7 @@ module ModelBuiltins = struct let is_undefined_opt prop n_lexp = let is_undef = - Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute prop n_lexp) in + Option.is_some (Prop.get_undef_attribute prop n_lexp) in is_undef && (!Config.angelic_execution || !Config.optimistic_cast) (** Creates an object in the heap with a given type, when the object is not known to be null or when it doesn't @@ -1723,7 +1723,7 @@ module ModelBuiltins = struct (execute___instanceof_cast cfg pdesc instr tenv _prop path ret_ids args callee_pname loc false) let set_resource_attribute prop path n_lexp loc ra_res = - let prop' = match Prop.get_resource_undef_attribute prop n_lexp with + let prop' = match Prop.get_resource_attribute prop n_lexp with | Some (Sil.Aresource (_ as ra)) -> let check_attr_change att_old att_new = () in Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Aresource { ra with Sil.ra_res = ra_res }) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 5a7466b8c..b6e8cf5e5 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -264,12 +264,14 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = if Prop.has_dangling_uninit_attribute spec_pre e then Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) ) else if Sil.exp_equal e_sub Sil.exp_minus_one then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) - else match Prop.get_resource_undef_attribute actual_pre e_sub with - | Some (Sil.Aundef (s, loc, pos)) -> - Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) + else match Prop.get_resource_attribute actual_pre e_sub with | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) -> Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) - | _ -> None in + | _ -> + (match Prop.get_undef_attribute actual_pre e_sub with + | Some (Sil.Aundef (s, loc, pos)) -> + Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) + | _ -> None) in let check_hpred = function | Sil.Hpointsto (lexp, se, _) -> check_dereference (Sil.root_of_lexp lexp) se @@ -324,7 +326,7 @@ let check_path_errors_in_post caller_pname post post_path = Also, update any Aresource attributes to refer to the caller *) let post_process_post caller_pname callee_pname loc actual_pre ((post: Prop.exposed Prop.t), post_path) = - let actual_pre_has_freed_attribute e = match Prop.get_resource_undef_attribute actual_pre e with + let actual_pre_has_freed_attribute e = match Prop.get_resource_attribute actual_pre e with | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease })) -> true | _ -> false in let atom_update_alloc_attribute = function @@ -1087,7 +1089,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r let mark_id_as_retval (p, path) = (* check if the retval already has an important resource that should not be overwritten *) let has_important_resource_attr = - match Prop.get_resource_undef_attribute p ret_var with + match Prop.get_resource_attribute p ret_var with | Some (Sil.Aresource ({ Sil.ra_res = Sil.Rfile; })) -> true | _ -> false in if has_important_resource_attr then p, path