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

Refactor Prop ops on attributes into sub-module

Browse Source 
Summary: Just renaming and reordering.

Reviewed By: cristianoc

Differential Revision: D3683835

fbshipit-source-id: 526cf76
master
Josh Berdine 8 years ago committed by Facebook Github Bot 5
parent b7d70ff178
commit 4053d24bed
11 changed files with 306 additions and 292 deletions
Show Stats Download Patch File Download Diff File

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

@ -1029,11 +1029,11 @@ let cycle_has_weak_or_unretained_or_assign_field cycle =
do_cycle cycle do_cycle cycle
let check_observer_is_unsubscribed_deallocation prop e = let check_observer_is_unsubscribed_deallocation prop e =
let pvar_opt = match Prop.get_resource_attribute prop e with let pvar_opt = match Prop.Attribute.get_resource prop e with
| Some (Apred (Aresource ({ ra_vpath = Some (Dpvar pvar) }), _)) -> Some pvar | Some (Apred (Aresource ({ ra_vpath = Some (Dpvar pvar) }), _)) -> Some pvar
| _ -> None in | _ -> None in
let loc = State.get_loc () in let loc = State.get_loc () in
match Prop.get_observer_attribute prop e with match Prop.Attribute.get_observer prop e with
| Some (Apred (Aobserver, _)) -> | Some (Apred (Aobserver, _)) ->
(match pvar_opt with (match pvar_opt with
| Some pvar when Config.nsnotification_center_checker_backend -> | Some pvar when Config.nsnotification_center_checker_backend ->
@ -1099,12 +1099,12 @@ let check_junk ?original_prop pname tenv prop =
let res = ref None in let res = ref None in
let do_entry e = let do_entry e =
check_observer_is_unsubscribed_deallocation prop e; check_observer_is_unsubscribed_deallocation prop e;
match Prop.get_resource_attribute prop e with match Prop.Attribute.get_resource prop e with
| Some (Apred (Aresource ({ ra_kind = Racquire }) as a, _)) -> | Some (Apred (Aresource ({ ra_kind = Racquire }) as a, _)) ->
L.d_str "ATTRIBUTE: "; PredSymb.d_attribute a; L.d_ln (); L.d_str "ATTRIBUTE: "; PredSymb.d_attribute a; L.d_ln ();
res := Some a res := Some a
| _ -> | _ ->
(match Prop.get_undef_attribute prop e with (match Prop.Attribute.get_undef prop e with
| Some (Apred (Aundef _ as a, _)) -> | Some (Apred (Aundef _ as a, _)) ->
res := Some a res := Some a
| _ -> ()) in | _ -> ()) in

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

@ -1642,7 +1642,7 @@ let pi_partial_join mode
| None -> None | None -> None
| Some (a_res, a_op) -> | Some (a_res, a_op) ->
if mode = JoinState.Pre then join_atom_check_pre p_op a_op; if mode = JoinState.Pre then join_atom_check_pre p_op a_op;
if Prop.atom_is_attribute a then join_atom_check_attribute p_op a_op; if Prop.Attribute.atom_is a then join_atom_check_attribute p_op a_op;
if not (Prover.check_atom p_op a_op) then None if not (Prover.check_atom p_op a_op) then None
else begin else begin
match Prop.atom_exp_le_const a_op with match Prop.atom_exp_le_const a_op with

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

@ -55,7 +55,7 @@ let is_special_field class_names field_name_opt field =
(** Check whether the hpred is a |-> representing a resource in the Racquire state *) (** Check whether the hpred is a |-> representing a resource in the Racquire state *)
let hpred_is_open_resource prop = function let hpred_is_open_resource prop = function
| Sil.Hpointsto(e, _, _) -> | Sil.Hpointsto(e, _, _) ->
(match Prop.get_resource_attribute prop e with (match Prop.Attribute.get_resource prop e with
| Some (Apred (Aresource { ra_kind = Racquire; ra_res = res }, _)) -> Some res | Some (Apred (Aresource { ra_kind = Racquire; ra_res = res }, _)) -> Some res
| _ -> None) | _ -> None)
| _ -> | _ ->
@ -847,7 +847,7 @@ let create_dereference_desc
match de_opt with match de_opt with
| Some (DExp.Dpvar pvar) | Some (DExp.Dpvar pvar)
| Some (DExp.Dpvaraddr pvar) -> | Some (DExp.Dpvaraddr pvar) ->
(match Prop.get_objc_null_attribute prop (Exp.Lvar pvar) with (match Prop.Attribute.get_objc_null prop (Exp.Lvar pvar) with
| Some (Apred (Aobjc_null, [_; vfs])) -> | Some (Apred (Aobjc_null, [_; vfs])) ->
Localise.parameter_field_not_null_checked_desc desc vfs Localise.parameter_field_not_null_checked_desc desc vfs
| _ -> | _ ->
@ -1047,7 +1047,7 @@ let explain_dereference_as_caller_expression
if verbose then L.d_strln ("parameter number: " ^ string_of_int position); if verbose then L.d_strln ("parameter number: " ^ string_of_int position);
explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off
else else
if Prop.has_dangling_uninit_attribute spec_pre exp then if Prop.Attribute.has_dangling_uninit spec_pre exp then
Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc
else Localise.no_desc else Localise.no_desc
| None -> | None ->

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

@ -773,9 +773,9 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
| Procname.ObjC_Cpp _ -> | Procname.ObjC_Cpp _ ->
if (Procname.is_constructor pname) then if (Procname.is_constructor pname) then
Paths.PathSet.map (fun prop -> Paths.PathSet.map (fun prop ->
let prop = Prop.remove_resource_attribute Racquire Rfile prop in let prop = Prop.Attribute.remove_resource Racquire Rfile prop in
let prop = Prop.remove_resource_attribute Racquire (Rmemory Mmalloc) prop in let prop = Prop.Attribute.remove_resource Racquire (Rmemory Mmalloc) prop in
Prop.remove_resource_attribute Racquire (Rmemory Mobjc) prop Prop.Attribute.remove_resource Racquire (Rmemory Mobjc) prop
) pathset ) pathset
else pathset else pathset
| _ -> pathset in | _ -> pathset in

22
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -137,7 +137,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; }
let is_undefined_opt prop n_lexp = let is_undefined_opt prop n_lexp =
let is_undef = let is_undef =
Option.is_some (Prop.get_undef_attribute prop n_lexp) in Option.is_some (Prop.Attribute.get_undef prop n_lexp) in
is_undef && (Config.angelic_execution || Config.optimistic_cast) 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 (** Creates an object in the heap with a given type, when the object is not known to be null or when
@ -311,9 +311,9 @@ let execute___cast builtin_args
execute___instanceof_cast ~instof:false builtin_args execute___instanceof_cast ~instof:false builtin_args
let set_resource_attribute prop path n_lexp loc ra_res = let set_resource_attribute prop path n_lexp loc ra_res =
let prop' = match Prop.get_resource_attribute prop n_lexp with let prop' = match Prop.Attribute.get_resource prop n_lexp with
| Some (Apred (Aresource ra, _)) -> | Some (Apred (Aresource ra, _)) ->
Prop.add_or_replace_attribute prop (Apred (Aresource { ra with ra_res }, [n_lexp])) Prop.Attribute.add_or_replace prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
| _ -> | _ ->
let pname = PredSymb.mem_alloc_pname PredSymb.Mnew in let pname = PredSymb.mem_alloc_pname PredSymb.Mnew in
let ra = let ra =
@ -323,7 +323,7 @@ let set_resource_attribute prop path n_lexp loc ra_res =
ra_pname = pname; ra_pname = pname;
ra_loc = loc; ra_loc = loc;
ra_vpath = None } in ra_vpath = None } in
Prop.add_or_replace_attribute prop (Apred (Aresource ra, [n_lexp])) in Prop.Attribute.add_or_replace prop (Apred (Aresource ra, [n_lexp])) in
[(prop', path)] [(prop', path)]
(** Set the attibute of the value as file *) (** Set the attibute of the value as file *)
@ -545,7 +545,7 @@ let execute___set_autorelease_attribute
let prop = return_result lexp prop_ ret_ids in let prop = return_result lexp prop_ ret_ids in
if Config.objc_memory_model_on then if Config.objc_memory_model_on then
let n_lexp, prop = check_arith_norm_exp pname lexp prop in let n_lexp, prop = check_arith_norm_exp pname lexp prop in
let prop' = Prop.add_or_replace_attribute prop (Apred (Aautorelease, [n_lexp])) in let prop' = Prop.Attribute.add_or_replace prop (Apred (Aautorelease, [n_lexp])) in
[(prop', path)] [(prop', path)]
else execute___no_op prop path else execute___no_op prop path
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -555,8 +555,8 @@ let execute___release_autorelease_pool
({ Builtin.prop_; path; } as builtin_args) ({ Builtin.prop_; path; } as builtin_args)
: Builtin.ret_typ = : Builtin.ret_typ =
if Config.objc_memory_model_on then if Config.objc_memory_model_on then
let autoreleased_objects = Prop.get_atoms_with_attribute prop_ PredSymb.Aautorelease in let autoreleased_objects = Prop.Attribute.get_for_symb prop_ Aautorelease in
let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in let prop_without_attribute = Prop.Attribute.remove_for_attr prop_ Aautorelease in
let call_release res atom = let call_release res atom =
match res, atom with match res, atom with
| ((prop', path') :: _, Sil.Apred (_, exp :: _)) -> | ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
@ -582,12 +582,12 @@ let execute___release_autorelease_pool
let set_attr pdesc prop path exp attr = let set_attr pdesc prop path exp attr =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp pname exp prop in let n_lexp, prop = check_arith_norm_exp pname exp prop in
[(Prop.add_or_replace_attribute prop (Apred (attr, [n_lexp])), path)] [(Prop.Attribute.add_or_replace prop (Apred (attr, [n_lexp])), path)]
let delete_attr pdesc prop path exp attr = let delete_attr pdesc prop path exp attr =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp pname exp prop in let n_lexp, prop = check_arith_norm_exp pname exp prop in
[(Prop.remove_attribute_from_exp prop (Apred (attr, [n_lexp])), path)] [(Prop.Attribute.remove prop (Apred (attr, [n_lexp])), path)]
(** Set attibute att *) (** Set attibute att *)
@ -694,7 +694,7 @@ let _execute_free mk loc acc iter =
PredSymb.ra_vpath = None } in PredSymb.ra_vpath = None } in
(* mark value as freed *) (* mark value as freed *)
let p_res = let p_res =
Prop.add_or_replace_attribute_check_changed Prop.Attribute.add_or_replace_check_changed
Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, [lexp])) in Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, [lexp])) in
p_res :: acc p_res :: acc
| (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *) | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *)
@ -796,7 +796,7 @@ let execute_alloc mk can_return_null
PredSymb.ra_loc = loc; PredSymb.ra_loc = loc;
PredSymb.ra_vpath = None } in PredSymb.ra_vpath = None } in
(* mark value as allocated *) (* mark value as allocated *)
Prop.add_or_replace_attribute prop' (Apred (Aresource ra, [exp_new])) in Prop.Attribute.add_or_replace prop' (Apred (Aresource ra, [exp_new])) in
let prop_alloc = Prop.conjoin_eq (Exp.Var ret_id) exp_new prop_plus_ptsto in let prop_alloc = Prop.conjoin_eq (Exp.Var ret_id) exp_new prop_plus_ptsto in
if can_return_null then if can_return_null then
let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in

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

@ -1774,193 +1774,197 @@ let prop_reset_inst inst_map prop =
replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop) replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop)
(** {2 Attributes} *) (** {2 Attributes} *)
module Attribute = struct
(** Return the exp and attribute marked in the atom if any, and return None otherwise *) (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
let atom_get_attribute atom = let atom_get atom =
match atom with match atom with
| Sil.Apred _ | Anpred _ -> Some atom | Sil.Apred _ | Anpred _ -> Some atom
| _ -> None | _ -> None
(** Check whether an atom is used to mark an attribute *)
let atom_is a =
atom_get a <> None
(** Add an attribute associated to the argument expressions *)
let add ?(footprint = false) ?(polarity = true) prop attr args =
prop_atom_and ~footprint prop
(if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
let attributes_in_same_category attr1 attr2 =
let cat1 = PredSymb.to_category attr1 in
let cat2 = PredSymb.to_category attr2 in
PredSymb.category_equal cat1 cat2
(** Replace an attribute associated to the expression *)
let add_or_replace_check_changed check_attribute_change prop atom0 =
match atom0 with
| Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps0 in
let nexp = IList.hd nexps in (* len nexps = len exps0 > 0 by match *)
let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
let atom_map = function
| Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
when Exp.equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0;
natom
| atom ->
atom in
let pi = get_pi prop in
let pi' = IList.map_changed atom_map pi in
if pi == pi'
then prop_atom_and prop natom
else replace_pi pi' prop
| _ ->
prop
let add_or_replace prop atom =
(* wrapper for the most common case: do nothing *)
let check_attr_changed = (fun _ _ -> ()) in
add_or_replace_check_changed check_attr_changed prop atom
(** Get all the attributes of the prop *)
let get_all prop =
let res = ref [] in
let do_atom a = match atom_get a with
| Some attr -> res := attr :: !res
| None -> () in
IList.iter do_atom prop.pi;
IList.rev !res
(** Get all the attributes of the prop *)
let get_for_symb prop att =
IList.filter (function
| Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att
| _ -> false
) (get_pi prop)
(** Get the attribute associated to the expression, if any *)
let get_for_exp prop exp =
let nexp = exp_normalize_prop prop exp in
let atom_get_attr attributes atom =
match atom with
| Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
| _ -> attributes in
IList.fold_left atom_get_attr [] prop.pi
let get prop exp category =
let atts = get_for_exp prop exp in
try
Some
(IList.find (function
| Sil.Apred (att, _) | Anpred (att, _) ->
PredSymb.category_equal (PredSymb.to_category att) category
| _ -> false
) atts)
with Not_found -> None
(** Check whether an atom is used to mark an attribute *) let get_undef prop exp =
let atom_is_attribute a = get prop exp ACundef
atom_get_attribute a <> None
(** Get the attribute associated to the expression, if any *) let get_resource prop exp =
let get_attributes prop exp = get prop exp ACresource
let nexp = exp_normalize_prop prop exp in
let atom_get_attr attributes atom =
match atom with
| Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
| _ -> attributes in
IList.fold_left atom_get_attr [] prop.pi
let attributes_in_same_category attr1 attr2 =
let cat1 = PredSymb.to_category attr1 in
let cat2 = PredSymb.to_category attr2 in
PredSymb.category_equal cat1 cat2
let get_attribute prop exp category =
let atts = get_attributes prop exp in
try
Some
(IList.find (function
| Sil.Apred (att, _) | Anpred (att, _) ->
PredSymb.category_equal (PredSymb.to_category att) category
| _ -> false
) atts)
with Not_found -> None
let get_undef_attribute prop exp =
get_attribute prop exp PredSymb.ACundef
let get_resource_attribute prop exp =
get_attribute prop exp PredSymb.ACresource
let get_taint_attribute prop exp =
get_attribute prop exp PredSymb.ACtaint
let get_autorelease_attribute prop exp =
get_attribute prop exp PredSymb.ACautorelease
let get_objc_null_attribute prop exp =
get_attribute prop exp PredSymb.ACobjc_null
let get_div0_attribute prop exp =
get_attribute prop exp PredSymb.ACdiv0
let get_observer_attribute prop exp =
get_attribute prop exp PredSymb.ACobserver
let get_retval_attribute prop exp =
get_attribute prop exp PredSymb.ACretval
let has_dangling_uninit_attribute prop exp =
let la = get_attributes prop exp in
IList.exists (function
| Sil.Apred (a, _) -> PredSymb.equal a (Adangling DAuninit)
| _ -> false
) la
(** Get all the attributes of the prop *)
let get_all_attributes prop =
let res = ref [] in
let do_atom a = match atom_get_attribute a with
| Some attr -> res := attr :: !res
| None -> () in
IList.iter do_atom prop.pi;
IList.rev !res
(** Set an attribute associated to the argument expressions *)
let set_attribute ?(footprint = false) ?(polarity = true) prop attr args =
prop_atom_and ~footprint prop
(if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
(** Replace an attribute associated to the expression *)
let add_or_replace_attribute_check_changed check_attribute_change prop atom0 =
match atom0 with
| Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps0 in
let nexp = IList.hd nexps in (* len nexps = len exps0 > 0 by match *)
let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
let atom_map = function
| Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
when Exp.equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0;
natom
| atom ->
atom in
let pi = get_pi prop in
let pi' = IList.map_changed atom_map pi in
if pi == pi'
then prop_atom_and prop natom
else replace_pi pi' prop
| _ ->
prop
let add_or_replace_attribute prop atom = let get_taint prop exp =
(* wrapper for the most common case: do nothing *) get prop exp ACtaint
let check_attr_changed = (fun _ _ -> ()) in
add_or_replace_attribute_check_changed check_attr_changed prop atom
(** mark Exp.Var's or Exp.Lvar's as undefined *) let get_autorelease prop exp =
let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos = get prop exp ACautorelease
let att_undef = PredSymb.Aundef (callee_pname, ret_annots, loc, path_pos) in
let mark_var_as_undefined exp prop =
match exp with
| Exp.Var _ | Lvar _ -> add_or_replace_attribute prop (Apred (att_undef, [exp]))
| _ -> prop in
IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
let filter_atoms ~f prop = let get_objc_null prop exp =
replace_pi (IList.filter f (get_pi prop)) prop get prop exp ACobjc_null
(** Remove an attribute from all the atoms in the heap *) let get_div0 prop exp =
let remove_attribute prop att0 = get prop exp ACdiv0
let f = function
| Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att)
| _ -> true in
filter_atoms ~f prop
let remove_resource_attribute ra_kind ra_res = let get_observer prop exp =
let f = function get prop exp ACobserver
| Sil.Apred (Aresource res_action, _) ->
PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0 let get_retval prop exp =
|| PredSymb.resource_compare res_action.ra_res ra_res <> 0 get prop exp ACretval
| _ -> true in
filter_atoms ~f let has_dangling_uninit prop exp =
let la = get_for_exp prop exp in
let remove_attribute_from_exp prop atom = IList.exists (function
match atom with | Sil.Apred (a, _) -> PredSymb.equal a (Adangling DAuninit)
| Sil.Apred (_, exps) | Anpred (_, exps) -> | _ -> false
let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in ) la
let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
let f a = not (Sil.atom_equal natom a) in let filter_atoms ~f prop =
filter_atoms ~f prop replace_pi (IList.filter f (get_pi prop)) prop
| _ ->
replace_pi (get_pi prop) prop let remove prop atom =
match atom with
(* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 = 0 *) | Sil.Apred (_, exps) | Anpred (_, exps) ->
let replace_objc_null prop lhs_exp rhs_exp = let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in
match get_objc_null_attribute prop rhs_exp, rhs_exp with let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
| Some atom, Exp.Var _ -> let f a = not (Sil.atom_equal natom a) in
let prop = remove_attribute_from_exp prop atom in filter_atoms ~f prop
let prop = conjoin_eq rhs_exp Exp.zero prop in | _ ->
let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in replace_pi (get_pi prop) prop
add_or_replace_attribute prop natom
| _ -> prop (** Remove an attribute from all the atoms in the heap *)
let remove_for_attr prop att0 =
let rec nullify_exp_with_objc_null prop exp = let f = function
match exp with | Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att)
| Exp.BinOp (_, exp1, exp2) -> | _ -> true in
let prop' = nullify_exp_with_objc_null prop exp1 in filter_atoms ~f prop
nullify_exp_with_objc_null prop' exp2
| Exp.UnOp (_, exp, _) -> let remove_resource ra_kind ra_res =
nullify_exp_with_objc_null prop exp let f = function
| Exp.Var _ -> | Sil.Apred (Aresource res_action, _) ->
(match get_objc_null_attribute prop exp with PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0
| Some atom -> || PredSymb.resource_compare res_action.ra_res ra_res <> 0
let prop' = remove_attribute_from_exp prop atom in | _ -> true in
conjoin_eq exp Exp.zero prop' filter_atoms ~f
| _ -> prop)
| _ -> prop (** Apply f to every resource attribute in the prop *)
let map_resource prop f =
(** Get all the attributes of the prop *) let attribute_map e = function
let get_atoms_with_attribute prop att = | PredSymb.Aresource ra -> PredSymb.Aresource (f e ra)
IList.filter (function | att -> att in
| Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att let atom_map = function
| _ -> false | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es)
) (get_pi prop) | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es)
| atom -> atom in
(** Apply f to every resource attribute in the prop *) replace_pi (IList.map atom_map (get_pi prop)) prop
let attribute_map_resource prop f =
let attribute_map e = function (* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 =
| PredSymb.Aresource ra -> PredSymb.Aresource (f e ra) 0 *)
| att -> att in let replace_objc_null prop lhs_exp rhs_exp =
let atom_map = function match get_objc_null prop rhs_exp, rhs_exp with
| Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es) | Some atom, Exp.Var _ ->
| Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es) let prop = remove prop atom in
| atom -> atom in let prop = conjoin_eq rhs_exp Exp.zero prop in
replace_pi (IList.map atom_map (get_pi prop)) prop let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
add_or_replace prop natom
| _ -> prop
let rec nullify_exp_with_objc_null prop exp =
match exp with
| Exp.BinOp (_, exp1, exp2) ->
let prop' = nullify_exp_with_objc_null prop exp1 in
nullify_exp_with_objc_null prop' exp2
| Exp.UnOp (_, exp, _) ->
nullify_exp_with_objc_null prop exp
| Exp.Var _ ->
(match get_objc_null prop exp with
| Some atom ->
let prop' = remove prop atom in
conjoin_eq exp Exp.zero prop'
| _ -> prop)
| _ -> prop
(** mark Exp.Var's or Exp.Lvar's as undefined *)
let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
let att_undef = PredSymb.Aundef (callee_pname, ret_annots, loc, path_pos) in
let mark_var_as_undefined exp prop =
match exp with
| Exp.Var _ | Lvar _ -> add_or_replace prop (Apred (att_undef, [exp]))
| _ -> prop in
IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
end
(** type for arithmetic problems *) (** type for arithmetic problems *)
type arith_problem = type arith_problem =
@ -1979,7 +1983,7 @@ let find_arithmetic_problem proc_node_session prop exp =
match exp_normalize_prop prop e with match exp_normalize_prop prop e with
| Exp.Const c when iszero_int_float c -> true | Exp.Const c when iszero_int_float c -> true
| _ -> | _ ->
res := add_or_replace_attribute !res (Apred (Adiv0 proc_node_session, [e])); res := Attribute.add_or_replace !res (Apred (Adiv0 proc_node_session, [e]));
false in false in
let rec walk = function let rec walk = function
| Exp.Var _ -> () | Exp.Var _ -> ()
@ -2038,7 +2042,7 @@ let deallocate_stack_vars p pvars =
begin begin
stack_vars_address_in_post := v :: !stack_vars_address_in_post; stack_vars_address_in_post := v :: !stack_vars_address_in_post;
let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
res := add_or_replace_attribute !res pred res := Attribute.add_or_replace !res pred
end in end in
IList.iter do_var !fresh_address_vars; IList.iter do_var !fresh_address_vars;
!res in !res in
@ -2837,7 +2841,7 @@ let find_equal_formal_path e prop =
match find_in_sigma e [] with match find_in_sigma e [] with
| Some vfs -> Some vfs | Some vfs -> Some vfs
| None -> | None ->
match get_objc_null_attribute prop e with match Attribute.get_objc_null prop e with
| Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
| _ -> None | _ -> None

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

@ -280,78 +280,87 @@ val conjoin_eq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t
(** Conjoin [exp1]!=[exp2] with a symbolic heap [prop]. *) (** Conjoin [exp1]!=[exp2] with a symbolic heap [prop]. *)
val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t
(** Check whether an atom is used to mark an attribute *) module Attribute : sig
val atom_is_attribute : atom -> bool
(** Apply f to every resource attribute in the prop *) (** Check whether an atom is used to mark an attribute *)
val attribute_map_resource : val atom_is : atom -> bool
normal t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> normal t
(** Return the exp and attribute marked in the atom if any, and return None otherwise *) (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
val atom_get_attribute : atom -> atom option val atom_get : atom -> atom option
(** Get the attributes associated to the expression, if any *) (** Add an attribute associated to the argument expressions *)
val get_attributes : 'a t -> Exp.t -> atom list val add : ?footprint: bool -> ?polarity: bool -> normal t -> PredSymb.t -> Exp.t list -> normal t
(** Get the undef attribute associated to the expression, if any *) (** Replace an attribute associated to the expression *)
val get_undef_attribute : 'a t -> Exp.t -> atom option val add_or_replace : normal t -> atom -> normal t
(** Get the resource attribute associated to the expression, if any *) (** Replace an attribute associated to the expression, and call the given function with new and
val get_resource_attribute : 'a t -> Exp.t -> atom option old attributes if they changed. *)
val add_or_replace_check_changed :
(PredSymb.t -> PredSymb.t -> unit) -> normal t -> atom -> normal t
(** Get the taint attribute associated to the expression, if any *) (** Get all the attributes of the prop *)
val get_taint_attribute : 'a t -> Exp.t -> atom option val get_all : 'a t -> atom list
(** Get the autorelease attribute associated to the expression, if any *) (** Get the attributes associated to the expression, if any *)
val get_autorelease_attribute : 'a t -> Exp.t -> atom option val get_for_exp : 'a t -> Exp.t -> atom list
(** Get the div0 attribute associated to the expression, if any *) (** Retrieve all the atoms that contain a specific attribute *)
val get_div0_attribute : 'a t -> Exp.t -> atom option val get_for_symb : 'a t -> PredSymb.t -> Sil.atom list
(** Get the observer attribute associated to the expression, if any *) (** Get the autorelease attribute associated to the expression, if any *)
val get_observer_attribute : 'a t -> Exp.t -> atom option val get_autorelease : 'a t -> Exp.t -> atom option
(** Get the objc null attribute associated to the expression, if any *) (** Get the div0 attribute associated to the expression, if any *)
val get_objc_null_attribute : 'a t -> Exp.t -> atom option val get_div0 : 'a t -> Exp.t -> atom option
(** Get the retval null attribute associated to the expression, if any *) (** Get the objc null attribute associated to the expression, if any *)
val get_retval_attribute : 'a t -> Exp.t -> atom option val get_objc_null : 'a t -> Exp.t -> atom option
(** Get all the attributes of the prop *) (** Get the observer attribute associated to the expression, if any *)
val get_all_attributes : 'a t -> atom list val get_observer : 'a t -> Exp.t -> atom option
val has_dangling_uninit_attribute : 'a t -> Exp.t -> bool (** Get the resource attribute associated to the expression, if any *)
val get_resource : 'a t -> Exp.t -> atom option
(** Set an attribute associated to the argument expressions *) (** Get the retval null attribute associated to the expression, if any *)
val set_attribute : ?footprint: bool -> ?polarity: bool -> val get_retval : 'a t -> Exp.t -> atom option
normal t -> PredSymb.t -> Exp.t list -> normal t
val add_or_replace_attribute_check_changed : (** Get the taint attribute associated to the expression, if any *)
(PredSymb.t -> PredSymb.t -> unit) -> normal t -> atom -> normal t val get_taint : 'a t -> Exp.t -> atom option
(** Replace an attribute associated to the expression *) (** Get the undef attribute associated to the expression, if any *)
val add_or_replace_attribute : normal t -> atom -> normal t val get_undef : 'a t -> Exp.t -> atom option
(** mark Exp.Var's or Exp.Lvar's as undefined *) (** Test for existence of an Adangling DAuninit attribute associated to the exp *)
val mark_vars_as_undefined : normal t -> Exp.t list -> Procname.t -> Typ.item_annotation -> val has_dangling_uninit : 'a t -> Exp.t -> bool
Location.t -> PredSymb.path_pos -> normal t
(** Remove an attribute from all the atoms in the heap *) (** Remove an attribute *)
val remove_attribute : 'a t -> PredSymb.t -> normal t val remove : 'a t -> atom -> normal t
val remove_resource_attribute : PredSymb.res_act_kind -> PredSymb.resource -> 'a t -> normal t (** Remove all attributes for the given attr *)
val remove_for_attr : 'a t -> PredSymb.t -> normal t
(** [replace_objc_null lhs rhs]. (** Remove all attributes for the given resource and kind *)
If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *) val remove_resource : PredSymb.res_act_kind -> PredSymb.resource -> 'a t -> normal t
val replace_objc_null : normal t -> Exp.t -> Exp.t -> normal t
val nullify_exp_with_objc_null : normal t -> Exp.t -> normal t (** Apply f to every resource attribute in the prop *)
val map_resource : normal t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> normal t
(** Remove an attribute from an exp in the heap *) (** [replace_objc_null lhs rhs].
val remove_attribute_from_exp : 'a t -> atom -> normal t If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *)
val replace_objc_null : normal t -> Exp.t -> Exp.t -> normal t
(** Retrieve all the atoms that contain a specific attribute *) (** For each Var subexp of the argument with an Aobjc_null attribute,
val get_atoms_with_attribute : 'a t -> PredSymb.t -> Sil.atom list remove the attribute and conjoin an equality to zero. *)
val nullify_exp_with_objc_null : normal t -> Exp.t -> normal t
(** mark Exp.Var's or Exp.Lvar's as undefined *)
val mark_vars_as_undefined :
normal t -> Exp.t list -> Procname.t -> Typ.item_annotation -> Location.t ->
PredSymb.path_pos -> normal t
end
(** Return the sub part of [prop]. *) (** Return the sub part of [prop]. *)
val get_sub : 'a t -> subst val get_sub : 'a t -> subst

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

@ -746,7 +746,7 @@ let add_guarded_by_constraints prop lexp pdesc =
(function (function
| Sil.Apred (Alocked, _) -> true | Sil.Apred (Alocked, _) -> true
| _ -> false) | _ -> false)
(Prop.get_attributes prop guarded_by_exp) in (Prop.Attribute.get_for_exp prop guarded_by_exp) in
let should_warn pdesc = let should_warn pdesc =
(* adding this check implements "by reference" semantics for guarded-by rather than "by value" (* adding this check implements "by reference" semantics for guarded-by rather than "by value"
semantics. if this access is through a local L or field V.f semantics. if this access is through a local L or field V.f
@ -793,7 +793,7 @@ let add_guarded_by_constraints prop lexp pdesc =
end end
else else
(* private method. add locked proof obligation to [pdesc] *) (* private method. add locked proof obligation to [pdesc] *)
Prop.set_attribute ~footprint:true prop Alocked [guarded_by_exp] Prop.Attribute.add ~footprint:true prop Alocked [guarded_by_exp]
| _ -> | _ ->
if not (proc_has_matching_annot pdesc guarded_by_str if not (proc_has_matching_annot pdesc guarded_by_str
|| is_synchronized_on_class guarded_by_str) && should_warn pdesc || is_synchronized_on_class guarded_by_str) && should_warn pdesc
@ -1205,7 +1205,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
nullable_obj_str := Some (Procname.to_string pname); nullable_obj_str := Some (Procname.to_string pname);
true true
| _ -> false in | _ -> false in
IList.exists is_nullable_attr (Prop.get_attributes prop exp) in IList.exists is_nullable_attr (Prop.Attribute.get_for_exp prop exp) in
(* it's ok for a non-nullable local to point to deref_exp *) (* it's ok for a non-nullable local to point to deref_exp *)
is_nullable || Pvar.is_local pvar is_nullable || Pvar.is_local pvar
| Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
@ -1232,8 +1232,8 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
Config.report_nullable_inconsistency && not (is_definitely_non_null root prop) Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
&& is_only_pt_by_nullable_fld_or_param root in && is_only_pt_by_nullable_fld_or_param root in
let relevant_attributes_getters = [ let relevant_attributes_getters = [
Prop.get_resource_attribute; Prop.Attribute.get_resource;
Prop.get_undef_attribute; Prop.Attribute.get_undef;
] in ] in
let get_relevant_attributes exp = let get_relevant_attributes exp =
let rec fold_getters = function let rec fold_getters = function

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

@ -109,7 +109,7 @@ let rec apply_offlist
lookup_inst := Some inst_curr; lookup_inst := Some inst_curr;
let alloc_attribute_opt = let alloc_attribute_opt =
if inst_curr = Sil.Iinitial then None if inst_curr = Sil.Iinitial then None
else Prop.get_undef_attribute p root_lexp in else Prop.Attribute.get_undef p root_lexp in
let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt 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 err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) in
let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in
@ -484,7 +484,7 @@ let check_deallocate_static_memory prop_after =
let freed_desc = Errdesc.explain_deallocate_constant_string s ra in let freed_desc = Errdesc.explain_deallocate_constant_string s ra in
raise (Exceptions.Deallocate_static_memory freed_desc) raise (Exceptions.Deallocate_static_memory freed_desc)
| _ -> () in | _ -> () in
let exp_att_list = Prop.get_all_attributes prop_after in let exp_att_list = Prop.Attribute.get_all prop_after in
IList.iter check_deallocated_attribute exp_att_list; IList.iter check_deallocated_attribute exp_att_list;
prop_after prop_after
@ -731,14 +731,14 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
match actual_pars with match actual_pars with
| (e, _) :: _ | (e, _) :: _
when Exp.equal e Exp.zero || when Exp.equal e Exp.zero ||
Option.is_some (Prop.get_objc_null_attribute pre e) -> true Option.is_some (Prop.Attribute.get_objc_null pre e) -> true
| _ -> false in | _ -> false in
let add_objc_null_attribute_or_nullify_result prop = let add_objc_null_attribute_or_nullify_result prop =
match ret_ids with match ret_ids with
| [ret_id] -> ( | [ret_id] -> (
match Prop.find_equal_formal_path receiver prop with match Prop.find_equal_formal_path receiver prop with
| Some vfs -> | Some vfs ->
Prop.add_or_replace_attribute prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs])) Prop.Attribute.add_or_replace prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
| None -> | None ->
Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop
) )
@ -756,7 +756,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
so that in a NPE we can separate it into a different error type *) so that in a NPE we can separate it into a different error type *)
[(add_objc_null_attribute_or_nullify_result pre, path)] [(add_objc_null_attribute_or_nullify_result pre, path)]
else else
let is_undef = Option.is_some (Prop.get_undef_attribute pre receiver) in let is_undef = Option.is_some (Prop.Attribute.get_undef pre receiver) in
if !Config.footprint && not is_undef then if !Config.footprint && not is_undef then
let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *) 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 let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
| Typ.Tptr _ -> Prop.conjoin_neq exp Exp.zero prop | Typ.Tptr _ -> Prop.conjoin_neq exp Exp.zero prop
| _ -> prop in | _ -> prop in
let add_tainted_post ret_exp callee_pname prop = let add_tainted_post ret_exp callee_pname prop =
Prop.add_or_replace_attribute prop (Apred (Ataint callee_pname, [ret_exp])) in Prop.Attribute.add_or_replace prop (Apred (Ataint callee_pname, [ret_exp])) in
if Config.angelic_execution && not (is_rec_call callee_pname) then if Config.angelic_execution && not (is_rec_call callee_pname) then
(* introduce a fresh program variable to allow abduction on the return value *) (* introduce a fresh program variable to allow abduction on the return value *)
@ -872,7 +872,7 @@ let add_taint prop lhs_id rhs_exp pname tenv =
if Taint.has_taint_annotation fieldname struct_typ if Taint.has_taint_annotation fieldname struct_typ
then then
let taint_info = { PredSymb.taint_source = pname; taint_kind = Tk_unknown; } in let taint_info = { PredSymb.taint_source = pname; taint_kind = Tk_unknown; } in
Prop.add_or_replace_attribute prop (Apred (Ataint taint_info, [Exp.Var lhs_id])) Prop.Attribute.add_or_replace prop (Apred (Ataint taint_info, [Exp.Var lhs_id]))
else else
prop in prop in
match rhs_exp with match rhs_exp with
@ -903,7 +903,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
let prop' = Prop.prop_iter_to_prop iter' in let prop' = Prop.prop_iter_to_prop iter' in
let prop'' = let prop'' =
if lookup_uninitialized then if lookup_uninitialized then
Prop.add_or_replace_attribute prop' (Apred (Adangling DAuninit, [Exp.Var id])) Prop.Attribute.add_or_replace prop' (Apred (Adangling DAuninit, [Exp.Var id]))
else prop' in else prop' in
let prop''' = let prop''' =
if Config.taint_analysis if Config.taint_analysis
@ -936,7 +936,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
match callee_opt, atom with match callee_opt, atom with
| None, Sil.Apred (Aundef _, _) -> Some atom | None, Sil.Apred (Aundef _, _) -> Some atom
| _ -> callee_opt in | _ -> callee_opt in
IList.fold_left fold_undef_pname None (Prop.get_attributes prop exp) in IList.fold_left fold_undef_pname None (Prop.Attribute.get_for_exp prop exp) in
let prop' = let prop' =
if Config.angelic_execution then if Config.angelic_execution then
(* when we try to deref an undefined value, add it to the footprint *) (* when we try to deref an undefined value, add it to the footprint *)
@ -985,7 +985,7 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp
try try
let n_lhs_exp, prop_' = check_arith_norm_exp pname lhs_exp prop_ in let n_lhs_exp, prop_' = check_arith_norm_exp pname lhs_exp prop_ in
let n_rhs_exp, prop = check_arith_norm_exp pname rhs_exp prop_' in let n_rhs_exp, prop = check_arith_norm_exp pname rhs_exp prop_' in
let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in let prop = Prop.Attribute.replace_objc_null prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list) IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list)
@ -1045,7 +1045,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
execute_set current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_ execute_set current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_
|> ret_old_path |> ret_old_path
| Sil.Prune (cond, loc, true_branch, ik) -> | Sil.Prune (cond, loc, true_branch, ik) ->
let prop__ = Prop.nullify_exp_with_objc_null prop_ cond in let prop__ = Prop.Attribute.nullify_exp_with_objc_null prop_ cond in
let check_condition_always_true_false () = let check_condition_always_true_false () =
let report_condition_always_true_false i = let report_condition_always_true_false i =
let skip_loop = match ik with let skip_loop = match ik with
@ -1362,7 +1362,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref
and check_untainted exp taint_kind caller_pname callee_pname prop = and check_untainted exp taint_kind caller_pname callee_pname prop =
match Prop.get_taint_attribute prop exp with match Prop.Attribute.get_taint prop exp with
| Some (Apred (Ataint taint_info, _)) -> | Some (Apred (Ataint taint_info, _)) ->
let err_desc = let err_desc =
Errdesc.explain_tainted_value_reaching_sensitive_function Errdesc.explain_tainted_value_reaching_sensitive_function
@ -1375,12 +1375,12 @@ and check_untainted exp taint_kind caller_pname callee_pname prop =
Exceptions.Tainted_value_reaching_sensitive_function Exceptions.Tainted_value_reaching_sensitive_function
(err_desc, __POS__) in (err_desc, __POS__) in
Reporting.log_warning caller_pname exn; Reporting.log_warning caller_pname exn;
Prop.add_or_replace_attribute prop (Apred (Auntaint taint_info, [exp])) Prop.Attribute.add_or_replace prop (Apred (Auntaint taint_info, [exp]))
| _ -> | _ ->
if !Config.footprint then if !Config.footprint then
let taint_info = { PredSymb.taint_source = callee_pname; taint_kind; } in let taint_info = { PredSymb.taint_source = callee_pname; taint_kind; } in
(* add untained(n_lexp) to the footprint *) (* add untained(n_lexp) to the footprint *)
Prop.set_attribute ~footprint:true prop (Auntaint taint_info) [exp] Prop.Attribute.add ~footprint:true prop (Auntaint taint_info) [exp]
else prop else prop
(** execute a call for an unknown or scan function *) (** execute a call for an unknown or scan function *)
@ -1391,9 +1391,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
let do_exp p (e, _) = let do_exp p (e, _) =
let do_attribute q atom = let do_attribute q atom =
match atom with match atom with
| Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Prop.remove_attribute q res | Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Prop.Attribute.remove_for_attr q res
| _ -> q in | _ -> q in
IList.fold_left do_attribute p (Prop.get_attributes p e) in IList.fold_left do_attribute p (Prop.Attribute.get_for_exp p e) in
let filtered_args = let filtered_args =
match args, instr with match args, instr with
| _:: other_args, Sil.Call (_, _, _, _, { CallFlags.cf_virtual }) when cf_virtual -> | _:: other_args, Sil.Call (_, _, _, _, { CallFlags.cf_virtual }) when cf_virtual ->
@ -1451,7 +1451,8 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
(fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in
let prop_with_undef_attr = let prop_with_undef_attr =
let path_pos = State.get_path_pos () in let path_pos = State.get_path_pos () in
Prop.mark_vars_as_undefined pre_final exps_to_mark callee_pname ret_annots loc path_pos in Prop.Attribute.mark_vars_as_undefined
pre_final exps_to_mark callee_pname ret_annots loc path_pos in
[(prop_with_undef_attr, path)] [(prop_with_undef_attr, path)]
and check_variadic_sentinel and check_variadic_sentinel
@ -1640,7 +1641,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
let map_res_action e ra = (* update the vpath in resource attributes *) let map_res_action e ra = (* update the vpath in resource attributes *)
let vpath, _ = Errdesc.vpath_find p' e in let vpath, _ = Errdesc.vpath_find p' e in
{ ra with PredSymb.ra_vpath = vpath } in { ra with PredSymb.ra_vpath = vpath } in
Prop.attribute_map_resource p' map_res_action in Prop.Attribute.map_resource p' map_res_action in
p'', fav in p'', fav in
let post_process_result fav_normal p path = let post_process_result fav_normal p path =
let p' = prop_normal_to_primed fav_normal p in let p' = prop_normal_to_primed fav_normal p in

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

@ -313,15 +313,15 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
else else
(* Check if the dereferenced expr has the dangling uninitialized attribute. *) (* Check if the dereferenced expr has the dangling uninitialized attribute. *)
(* In that case it raise a dangling pointer dereferece *) (* In that case it raise a dangling pointer dereferece *)
if Prop.has_dangling_uninit_attribute spec_pre e then if Prop.Attribute.has_dangling_uninit spec_pre e then
Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some PredSymb.DAuninit)) ) Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some PredSymb.DAuninit)) )
else if Exp.equal e_sub Exp.minus_one else if Exp.equal e_sub Exp.minus_one
then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
else match Prop.get_resource_attribute actual_pre e_sub with else match Prop.Attribute.get_resource actual_pre e_sub with
| Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) -> | Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) ->
Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) Some (Deref_freed ra, desc true (Localise.deref_str_freed ra))
| _ -> | _ ->
(match Prop.get_undef_attribute actual_pre e_sub with (match Prop.Attribute.get_undef actual_pre e_sub with
| Some (Apred (Aundef (s, _, loc, pos), _)) -> | Some (Apred (Aundef (s, _, loc, pos), _)) ->
Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc)))
| _ -> None) in | _ -> None) in
@ -375,14 +375,14 @@ let check_path_errors_in_post caller_pname post post_path =
let pre_opt = State.get_normalized_pre (fun _ p -> p) (* Abs.abstract_no_symop *) in let pre_opt = State.get_normalized_pre (fun _ p -> p) (* Abs.abstract_no_symop *) in
Reporting.log_warning caller_pname ~pre: pre_opt exn Reporting.log_warning caller_pname ~pre: pre_opt exn
| _ -> () in | _ -> () in
IList.iter check_attr (Prop.get_all_attributes post) IList.iter check_attr (Prop.Attribute.get_all post)
(** Post process the instantiated post after the function call so that (** Post process the instantiated post after the function call so that
x.f |-> se becomes x |-> \{ f: se \}. x.f |-> se becomes x |-> \{ f: se \}.
Also, update any Aresource attributes to refer to the caller *) Also, update any Aresource attributes to refer to the caller *)
let post_process_post let post_process_post
caller_pname callee_pname loc actual_pre ((post: Prop.exposed Prop.t), post_path) = 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_attribute actual_pre e with let actual_pre_has_freed_attribute e = match Prop.Attribute.get_resource actual_pre e with
| Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true | Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true
| _ -> false in | _ -> false in
let atom_update_alloc_attribute = function let atom_update_alloc_attribute = function
@ -599,14 +599,14 @@ let prop_copy_footprint_pure p1 p2 =
Prop.replace_sigma_footprint Prop.replace_sigma_footprint
(Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in
let pi2 = Prop.get_pi p2' in let pi2 = Prop.get_pi p2' in
let pi2_attr, pi2_noattr = IList.partition Prop.atom_is_attribute pi2 in let pi2_attr, pi2_noattr = IList.partition Prop.Attribute.atom_is pi2 in
let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in
let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *)
(* if [atom] represents an attribute [att], add the attribure to [prop] *) (* if [atom] represents an attribute [att], add the attribure to [prop] *)
match Prop.atom_get_attribute atom with match Prop.Attribute.atom_get atom with
| None -> prop | None -> prop
| Some atom -> | Some atom ->
Prop.add_or_replace_attribute_check_changed check_attr_dealloc_mismatch prop atom in Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom in
IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
(** check if an expression is an exception *) (** check if an expression is an exception *)
@ -836,7 +836,7 @@ let check_taint_on_variadic_function callee_pname caller_pname actual_params cal
L.d_str "Paramters to be checked: [ "; L.d_str "Paramters to be checked: [ ";
IList.iter(fun (e,_) -> IList.iter(fun (e,_) ->
L.d_str (" " ^ (Sil.exp_to_string e) ^ " "); L.d_str (" " ^ (Sil.exp_to_string e) ^ " ");
match Prop.get_taint_attribute calling_prop e with match Prop.Attribute.get_taint calling_prop e with
| Some (Apred (Ataint taint_info, _)) -> | Some (Apred (Ataint taint_info, _)) ->
report_taint_error e taint_info callee_pname caller_pname calling_prop report_taint_error e taint_info callee_pname caller_pname calling_prop
| _ -> ()) actual_params'; | _ -> ()) actual_params';
@ -887,7 +887,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
| Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname -> | Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
Prover.check_disequal prop exp Exp.zero Prover.check_disequal prop exp Exp.zero
| _ -> false) | _ -> false)
(Prop.get_all_attributes prop) in (Prop.Attribute.get_all prop) in
if last_call_ret_non_null then if last_call_ret_non_null then
let returns_null prop = let returns_null prop =
IList.exists IList.exists
@ -904,7 +904,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
let taint_retval (prop, path) = let taint_retval (prop, path) =
let prop_normal = Prop.normalize prop in let prop_normal = Prop.normalize prop in
let prop' = let prop' =
Prop.add_or_replace_attribute prop_normal Prop.Attribute.add_or_replace prop_normal
(Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Exp.Var ret_id])) (Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Exp.Var ret_id]))
|> Prop.expose in |> Prop.expose in
(prop', path) in (prop', path) in
@ -936,7 +936,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
(* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of (* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of
attrs (we will flag errors on those exprs) *) attrs (we will flag errors on those exprs) *)
let collect_taint_untaint_exprs acc_map atom = let collect_taint_untaint_exprs acc_map atom =
match Prop.atom_get_attribute atom with match Prop.Attribute.atom_get atom with
| Some (Apred (Ataint _, [e])) -> | Some (Apred (Ataint _, [e])) ->
let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in
Exp.Map.add e (atom :: taint_atoms, untaint_atoms) acc_map Exp.Map.add e (atom :: taint_atoms, untaint_atoms) acc_map
@ -955,7 +955,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
the untaint atoms *) the untaint atoms *)
let report_taint_errors e (taint_atoms, _untaint_atoms) = let report_taint_errors e (taint_atoms, _untaint_atoms) =
let report_one_error taint_atom = let report_one_error taint_atom =
let taint_info = match Prop.atom_get_attribute taint_atom with let taint_info = match Prop.Attribute.atom_get taint_atom with
| Some (Apred (Ataint taint_info, _)) -> taint_info | Some (Apred (Ataint taint_info, _)) -> taint_info
| _ -> failwith "Expected to get taint attr on atom" in | _ -> failwith "Expected to get taint attr on atom" in
report_taint_error e taint_info callee_pname caller_pname calling_prop in report_taint_error e taint_info callee_pname caller_pname calling_prop in
@ -1109,7 +1109,7 @@ let quantify_path_idents_remove_constant_strings (prop: Prop.normal Prop.t) : Pr
(** Strengthen the footprint by adding pure facts from the current part *) (** Strengthen the footprint by adding pure facts from the current part *)
let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t =
let is_footprint_atom_not_attribute a = let is_footprint_atom_not_attribute a =
not (Prop.atom_is_attribute a) not (Prop.Attribute.atom_is a)
&& &&
let a_fav = Sil.atom_fav a in let a_fav = Sil.atom_fav a in
Sil.fav_for_all a_fav Ident.is_footprint in Sil.fav_for_all a_fav Ident.is_footprint in
@ -1262,7 +1262,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
let ret_var = Exp.Var ret_id in let ret_var = Exp.Var ret_id in
let mark_id_as_retval (p, path) = let mark_id_as_retval (p, path) =
let att_retval = PredSymb.Aretval (callee_pname, ret_annot) in let att_retval = PredSymb.Aretval (callee_pname, ret_annot) in
Prop.set_attribute p att_retval [ret_var], path in Prop.Attribute.add p att_retval [ret_var], path in
IList.map mark_id_as_retval res IList.map mark_id_as_retval res
| _ -> res | _ -> res

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

@ -379,6 +379,6 @@ let add_tainting_attribute att pvar_param prop =
when Pvar.equal pvar pvar_param -> when Pvar.equal pvar pvar_param ->
L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^ L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^
(Pvar.to_string pvar)); (Pvar.to_string pvar));
Prop.add_or_replace_attribute prop_acc (Apred (att, [rhs])) Prop.Attribute.add_or_replace prop_acc (Apred (att, [rhs]))
| _ -> prop_acc) | _ -> prop_acc)
prop (Prop.get_sigma prop) prop (Prop.get_sigma prop)

Write Preview
Loading…
Cancel
Save