From 4053d24bedceee2e77f043de1871b381831cd3a4 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 9 Aug 2016 03:37:15 -0700 Subject: [PATCH] Refactor Prop ops on attributes into sub-module Summary: Just renaming and reordering. Reviewed By: cristianoc Differential Revision: D3683835 fbshipit-source-id: 526cf76 --- infer/src/backend/abs.ml | 8 +- infer/src/backend/dom.ml | 2 +- infer/src/backend/errdesc.ml | 6 +- infer/src/backend/interproc.ml | 6 +- infer/src/backend/modelBuiltins.ml | 22 +- infer/src/backend/prop.ml | 368 +++++++++++++++-------------- infer/src/backend/prop.mli | 107 +++++---- infer/src/backend/rearrange.ml | 10 +- infer/src/backend/symExec.ml | 37 +-- infer/src/backend/tabulation.ml | 30 +-- infer/src/backend/taint.ml | 2 +- 11 files changed, 306 insertions(+), 292 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 2a6ccf2a5..d0c0f3217 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1029,11 +1029,11 @@ let cycle_has_weak_or_unretained_or_assign_field cycle = do_cycle cycle 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 | _ -> None 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, _)) -> (match pvar_opt with | 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 do_entry 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, _)) -> L.d_str "ATTRIBUTE: "; PredSymb.d_attribute a; L.d_ln (); res := Some a | _ -> - (match Prop.get_undef_attribute prop e with + (match Prop.Attribute.get_undef prop e with | Some (Apred (Aundef _ as a, _)) -> res := Some a | _ -> ()) in diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index e8a10d0ac..64f4bfc9e 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -1642,7 +1642,7 @@ let pi_partial_join mode | None -> None | Some (a_res, 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 else begin match Prop.atom_exp_le_const a_op with diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index a56803673..0c191d034 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -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 *) let hpred_is_open_resource prop = function | 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 | _ -> None) | _ -> @@ -847,7 +847,7 @@ let create_dereference_desc match de_opt with | Some (DExp.Dpvar 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])) -> 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); explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off 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 else Localise.no_desc | None -> diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 6514e0292..2b245e1f4 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -773,9 +773,9 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t | Procname.ObjC_Cpp _ -> if (Procname.is_constructor pname) then Paths.PathSet.map (fun prop -> - let prop = Prop.remove_resource_attribute Racquire Rfile prop in - let prop = Prop.remove_resource_attribute Racquire (Rmemory Mmalloc) prop in - Prop.remove_resource_attribute Racquire (Rmemory Mobjc) prop + let prop = Prop.Attribute.remove_resource Racquire Rfile prop in + let prop = Prop.Attribute.remove_resource Racquire (Rmemory Mmalloc) prop in + Prop.Attribute.remove_resource Racquire (Rmemory Mobjc) prop ) pathset else pathset | _ -> pathset in diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 27ee9f0ef..2cc51cd75 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -137,7 +137,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; } let is_undefined_opt prop n_lexp = 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) (** 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 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, _)) -> - 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 ra = @@ -323,7 +323,7 @@ let set_resource_attribute prop path n_lexp loc ra_res = ra_pname = pname; ra_loc = loc; 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)] (** 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 if Config.objc_memory_model_on then 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)] else execute___no_op prop path | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -555,8 +555,8 @@ let execute___release_autorelease_pool ({ Builtin.prop_; path; } as builtin_args) : Builtin.ret_typ = if Config.objc_memory_model_on then - let autoreleased_objects = Prop.get_atoms_with_attribute prop_ PredSymb.Aautorelease in - let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in + let autoreleased_objects = Prop.Attribute.get_for_symb prop_ Aautorelease in + let prop_without_attribute = Prop.Attribute.remove_for_attr prop_ Aautorelease in let call_release res atom = match res, atom with | ((prop', path') :: _, Sil.Apred (_, exp :: _)) -> @@ -582,12 +582,12 @@ let execute___release_autorelease_pool let set_attr pdesc prop path exp attr = let pname = Cfg.Procdesc.get_proc_name pdesc 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 pname = Cfg.Procdesc.get_proc_name pdesc 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 *) @@ -694,7 +694,7 @@ let _execute_free mk loc acc iter = PredSymb.ra_vpath = None } in (* mark value as freed *) 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 p_res :: acc | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *) @@ -796,7 +796,7 @@ let execute_alloc mk can_return_null PredSymb.ra_loc = loc; PredSymb.ra_vpath = None } in (* 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 if can_return_null then let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 03acd1b89..2656c35d4 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1774,193 +1774,197 @@ let prop_reset_inst inst_map prop = replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop) (** {2 Attributes} *) +module Attribute = struct -(** Return the exp and attribute marked in the atom if any, and return None otherwise *) -let atom_get_attribute atom = - match atom with - | Sil.Apred _ | Anpred _ -> Some atom - | _ -> None + (** Return the exp and attribute marked in the atom if any, and return None otherwise *) + let atom_get atom = + match atom with + | Sil.Apred _ | Anpred _ -> Some atom + | _ -> 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 atom_is_attribute a = - atom_get_attribute a <> None + let get_undef prop exp = + get prop exp ACundef -(** Get the attribute associated to the expression, if any *) -let get_attributes 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 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 get_resource prop exp = + get prop exp ACresource -let add_or_replace_attribute prop atom = - (* wrapper for the most common case: do nothing *) - let check_attr_changed = (fun _ _ -> ()) in - add_or_replace_attribute_check_changed check_attr_changed prop atom + let get_taint prop exp = + get prop exp ACtaint -(** 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_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 get_autorelease prop exp = + get prop exp ACautorelease -let filter_atoms ~f prop = - replace_pi (IList.filter f (get_pi prop)) prop + let get_objc_null prop exp = + get prop exp ACobjc_null -(** Remove an attribute from all the atoms in the heap *) -let remove_attribute prop att0 = - let f = function - | Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att) - | _ -> true in - filter_atoms ~f prop + let get_div0 prop exp = + get prop exp ACdiv0 -let remove_resource_attribute ra_kind ra_res = - let f = function - | Sil.Apred (Aresource res_action, _) -> - PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0 - || PredSymb.resource_compare res_action.ra_res ra_res <> 0 - | _ -> true in - filter_atoms ~f - -let remove_attribute_from_exp prop atom = - match atom with - | Sil.Apred (_, exps) | Anpred (_, exps) -> - let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in - let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in - let f a = not (Sil.atom_equal natom a) in - filter_atoms ~f prop - | _ -> - replace_pi (get_pi prop) prop - -(* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 = 0 *) -let replace_objc_null prop lhs_exp rhs_exp = - match get_objc_null_attribute prop rhs_exp, rhs_exp with - | Some atom, Exp.Var _ -> - let prop = remove_attribute_from_exp prop atom in - let prop = conjoin_eq rhs_exp Exp.zero prop in - let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in - add_or_replace_attribute 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_attribute prop exp with - | Some atom -> - let prop' = remove_attribute_from_exp prop atom in - conjoin_eq exp Exp.zero prop' - | _ -> prop) - | _ -> prop - -(** Get all the attributes of the prop *) -let get_atoms_with_attribute prop att = - IList.filter (function - | Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att - | _ -> false - ) (get_pi prop) - -(** Apply f to every resource attribute in the prop *) -let attribute_map_resource prop f = - let attribute_map e = function - | PredSymb.Aresource ra -> PredSymb.Aresource (f e ra) - | att -> att in - let atom_map = function - | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es) - | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es) - | atom -> atom in - replace_pi (IList.map atom_map (get_pi prop)) prop + let get_observer prop exp = + get prop exp ACobserver + + let get_retval prop exp = + get prop exp ACretval + + let has_dangling_uninit prop exp = + let la = get_for_exp prop exp in + IList.exists (function + | Sil.Apred (a, _) -> PredSymb.equal a (Adangling DAuninit) + | _ -> false + ) la + + let filter_atoms ~f prop = + replace_pi (IList.filter f (get_pi prop)) prop + + let remove prop atom = + match atom with + | Sil.Apred (_, exps) | Anpred (_, exps) -> + let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in + let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in + let f a = not (Sil.atom_equal natom a) in + filter_atoms ~f prop + | _ -> + replace_pi (get_pi prop) prop + + (** Remove an attribute from all the atoms in the heap *) + let remove_for_attr prop att0 = + let f = function + | Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att) + | _ -> true in + filter_atoms ~f prop + + let remove_resource ra_kind ra_res = + let f = function + | Sil.Apred (Aresource res_action, _) -> + PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0 + || PredSymb.resource_compare res_action.ra_res ra_res <> 0 + | _ -> true in + filter_atoms ~f + + (** Apply f to every resource attribute in the prop *) + let map_resource prop f = + let attribute_map e = function + | PredSymb.Aresource ra -> PredSymb.Aresource (f e ra) + | att -> att in + let atom_map = function + | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es) + | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es) + | atom -> atom in + replace_pi (IList.map atom_map (get_pi prop)) prop + + (* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 = + 0 *) + let replace_objc_null prop lhs_exp rhs_exp = + match get_objc_null prop rhs_exp, rhs_exp with + | Some atom, Exp.Var _ -> + let prop = remove prop atom in + let prop = conjoin_eq rhs_exp Exp.zero prop in + 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 arith_problem = @@ -1979,7 +1983,7 @@ let find_arithmetic_problem proc_node_session prop exp = match exp_normalize_prop prop e with | 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 let rec walk = function | Exp.Var _ -> () @@ -2038,7 +2042,7 @@ let deallocate_stack_vars p pvars = begin stack_vars_address_in_post := v :: !stack_vars_address_in_post; 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 IList.iter do_var !fresh_address_vars; !res in @@ -2837,7 +2841,7 @@ let find_equal_formal_path e prop = match find_in_sigma e [] with | Some vfs -> Some vfs | None -> - match get_objc_null_attribute prop e with + match Attribute.get_objc_null prop e with | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs | _ -> None diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 4b5e82261..15ad94049 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -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]. *) val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t -(** Check whether an atom is used to mark an attribute *) -val atom_is_attribute : atom -> bool +module Attribute : sig -(** Apply f to every resource attribute in the prop *) -val attribute_map_resource : - normal t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> normal t + (** Check whether an atom is used to mark an attribute *) + val atom_is : atom -> bool -(** Return the exp and attribute marked in the atom if any, and return None otherwise *) -val atom_get_attribute : atom -> atom option + (** Return the exp and attribute marked in the atom if any, and return None otherwise *) + val atom_get : atom -> atom option -(** Get the attributes associated to the expression, if any *) -val get_attributes : 'a t -> Exp.t -> atom list + (** Add an attribute associated to the argument expressions *) + 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 *) -val get_undef_attribute : 'a t -> Exp.t -> atom option + (** Replace an attribute associated to the expression *) + val add_or_replace : normal t -> atom -> normal t -(** Get the resource attribute associated to the expression, if any *) -val get_resource_attribute : 'a t -> Exp.t -> atom option + (** Replace an attribute associated to the expression, and call the given function with new and + 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 *) -val get_taint_attribute : 'a t -> Exp.t -> atom option + (** Get all the attributes of the prop *) + val get_all : 'a t -> atom list -(** Get the autorelease attribute associated to the expression, if any *) -val get_autorelease_attribute : 'a t -> Exp.t -> atom option + (** Get the attributes associated to the expression, if any *) + val get_for_exp : 'a t -> Exp.t -> atom list -(** Get the div0 attribute associated to the expression, if any *) -val get_div0_attribute : 'a t -> Exp.t -> atom option + (** Retrieve all the atoms that contain a specific attribute *) + val get_for_symb : 'a t -> PredSymb.t -> Sil.atom list -(** Get the observer attribute associated to the expression, if any *) -val get_observer_attribute : 'a t -> Exp.t -> atom option + (** Get the autorelease attribute associated to the expression, if any *) + val get_autorelease : 'a t -> Exp.t -> atom option -(** Get the objc null attribute associated to the expression, if any *) -val get_objc_null_attribute : 'a t -> Exp.t -> atom option + (** Get the div0 attribute associated to the expression, if any *) + val get_div0 : 'a t -> Exp.t -> atom option -(** Get the retval null attribute associated to the expression, if any *) -val get_retval_attribute : 'a t -> Exp.t -> atom option + (** Get the objc null attribute associated to the expression, if any *) + val get_objc_null : 'a t -> Exp.t -> atom option -(** Get all the attributes of the prop *) -val get_all_attributes : 'a t -> atom list + (** Get the observer attribute associated to the expression, if any *) + 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 *) -val set_attribute : ?footprint: bool -> ?polarity: bool -> - normal t -> PredSymb.t -> Exp.t list -> normal t + (** Get the retval null attribute associated to the expression, if any *) + val get_retval : 'a t -> Exp.t -> atom option -val add_or_replace_attribute_check_changed : - (PredSymb.t -> PredSymb.t -> unit) -> normal t -> atom -> normal t + (** Get the taint attribute associated to the expression, if any *) + val get_taint : 'a t -> Exp.t -> atom option -(** Replace an attribute associated to the expression *) -val add_or_replace_attribute : normal t -> atom -> normal t + (** Get the undef attribute associated to the expression, if any *) + val get_undef : 'a t -> Exp.t -> atom option -(** 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 + (** Test for existence of an Adangling DAuninit attribute associated to the exp *) + val has_dangling_uninit : 'a t -> Exp.t -> bool -(** Remove an attribute from all the atoms in the heap *) -val remove_attribute : 'a t -> PredSymb.t -> normal t + (** Remove an attribute *) + 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]. - 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 + (** Remove all attributes for the given resource and kind *) + val remove_resource : PredSymb.res_act_kind -> PredSymb.resource -> 'a 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 *) -val remove_attribute_from_exp : 'a t -> atom -> normal t + (** [replace_objc_null lhs rhs]. + 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 *) -val get_atoms_with_attribute : 'a t -> PredSymb.t -> Sil.atom list + (** For each Var subexp of the argument with an Aobjc_null attribute, + 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]. *) val get_sub : 'a t -> subst diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index f82de2021..0f6ba23e7 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -746,7 +746,7 @@ let add_guarded_by_constraints prop lexp pdesc = (function | Sil.Apred (Alocked, _) -> true | _ -> false) - (Prop.get_attributes prop guarded_by_exp) in + (Prop.Attribute.get_for_exp prop guarded_by_exp) in let should_warn pdesc = (* 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 @@ -793,7 +793,7 @@ let add_guarded_by_constraints prop lexp pdesc = end else (* 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 || 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); true | _ -> 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 *) is_nullable || Pvar.is_local pvar | 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) && is_only_pt_by_nullable_fld_or_param root in let relevant_attributes_getters = [ - Prop.get_resource_attribute; - Prop.get_undef_attribute; + Prop.Attribute.get_resource; + Prop.Attribute.get_undef; ] in let get_relevant_attributes exp = let rec fold_getters = function diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 81a10a557..9917821db 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -109,7 +109,7 @@ let rec apply_offlist lookup_inst := Some inst_curr; let alloc_attribute_opt = 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 err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) 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 raise (Exceptions.Deallocate_static_memory freed_desc) | _ -> () 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; 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 | (e, _) :: _ 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 let add_objc_null_attribute_or_nullify_result prop = match ret_ids with | [ret_id] -> ( match Prop.find_equal_formal_path receiver prop with | 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 -> 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 *) [(add_objc_null_attribute_or_nullify_result pre, path)] 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 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 @@ -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 | _ -> prop in 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 (* 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 then 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 prop in 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'' = 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 let prop''' = 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 | None, Sil.Apred (Aundef _, _) -> Some atom | _ -> 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' = if Config.angelic_execution then (* 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 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 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 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) @@ -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_ |> ret_old_path | 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 report_condition_always_true_false i = 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 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, _)) -> let err_desc = 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 (err_desc, __POS__) in 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 let taint_info = { PredSymb.taint_source = callee_pname; taint_kind; } in (* 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 (** 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_attribute q atom = 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 - 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 = match args, instr with | _:: 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 let prop_with_undef_attr = 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)] 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 vpath, _ = Errdesc.vpath_find p' e 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 let post_process_result fav_normal p path = let p' = prop_normal_to_primed fav_normal p in diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 34939eb57..4abd34bc4 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -313,15 +313,15 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = else (* Check if the dereferenced expr has the dangling uninitialized attribute. *) (* 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)) ) else if Exp.equal e_sub Exp.minus_one 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 (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 (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) | _ -> 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 Reporting.log_warning caller_pname ~pre: pre_opt exn | _ -> () 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 x.f |-> se becomes x |-> \{ f: se \}. 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_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 | _ -> false in let atom_update_alloc_attribute = function @@ -599,14 +599,14 @@ let prop_copy_footprint_pure p1 p2 = Prop.replace_sigma_footprint (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_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 replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) (* 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 | 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 (** 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: [ "; IList.iter(fun (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, _)) -> report_taint_error e taint_info callee_pname caller_pname calling_prop | _ -> ()) 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 -> Prover.check_disequal prop exp Exp.zero | _ -> false) - (Prop.get_all_attributes prop) in + (Prop.Attribute.get_all prop) in if last_call_ret_non_null then let returns_null prop = IList.exists @@ -904,7 +904,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = let taint_retval (prop, path) = let prop_normal = Prop.normalize prop in 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])) |> Prop.expose 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 attrs (we will flag errors on those exprs) *) 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])) -> 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 @@ -955,7 +955,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_ the untaint atoms *) let report_taint_errors e (taint_atoms, _untaint_atoms) = 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 | _ -> failwith "Expected to get taint attr on atom" 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 *) let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = 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 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 mark_id_as_retval (p, path) = 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 | _ -> res diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 339cfded9..a7949587b 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -379,6 +379,6 @@ let add_tainting_attribute att pvar_param prop = when Pvar.equal pvar pvar_param -> L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^ (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 (Prop.get_sigma prop)