pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[Infer][backend] Refactoring attribute categories so as not to conflate resource and undefined attrs

Browse Source 
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.
master
Sam Blackshear 9 years ago
parent 8c80856e97
commit 09242fc711
9 changed files with 37 additions and 22 deletions
Show Stats Download Patch File Download Diff File

6
infer/src/backend/abs.ml
Unescape View File

@ -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
| _ ->
(match Prop.get_undef_attribute prop e with
| Some (Sil.Aundef _ as a) ->
res := Some a
| _ -> () in
| _ -> ()) in
list_iter do_entry entries;
!res in
L.d_decrease_indent 1;

2
infer/src/backend/errdesc.ml
Unescape View File

@ -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)
| _ ->

5
infer/src/backend/prop.ml
Unescape View File

@ -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 =

7
infer/src/backend/prop.mli
Unescape View File

@ -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

3
infer/src/backend/rearrange.ml
Unescape View File

@ -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

8
infer/src/backend/sil.ml
Unescape View File

@ -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

2
infer/src/backend/sil.mli
Unescape View File

@ -270,6 +270,8 @@ and attribute_category =
| ACtaint
| ACdiv0
| ACobjc_null
| ACundef
| ACretval
(** Constants *)
and const =

8
infer/src/backend/symExec.ml
Unescape View File

@ -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 })

14
infer/src/backend/tabulation.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save