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

Generalize predicates from unary to nary

Browse Source 
Summary:
Add support for nary predicates, not just unary ones.  Many operations
don't make much sense for nullary predicates, and are generally treated
as no-ops.  The first argument is treated specially, as the "anchor" of
the predicate application.  For example, adding or removing an attribute
uses the anchor to identify the atom to operate on.  Also, abstraction
and normalization operations treat the anchor specially.

Reviewed By: cristianoc

Differential Revision: D3669391

fbshipit-source-id: 3d142ea
master
Josh Berdine 8 years ago committed by Facebook Github Bot 8
parent b6544eace7
commit 4185bda8ba
15 changed files with 183 additions and 164 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/IR/Cfg.re
Unescape View File

@ -962,8 +962,8 @@ let remove_abducted_retvars p =>
fun fun
| Sil.Aeq lhs rhs | Sil.Aeq lhs rhs
| Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs
| Sil.Apred _ e | Sil.Apred _ es
| Sil.Anpred _ e => exp_contains e | Sil.Anpred _ es => IList.exists exp_contains es
) )
pi pi
}; };

37
infer/src/IR/Sil.re
Unescape View File

@ -85,7 +85,14 @@ type res_action = {
}; };
/** Attributes */ /** Attributes are nary function symbols that are applied to expression arguments in Apred and
Anpred atomic formulas. Many operations don't make much sense for nullary predicates, and are
generally treated as no-ops. The first argument is treated specially, as the "anchor" of the
predicate application. For example, adding or removing an attribute uses the anchor to identify
the atom to operate on. Also, abstraction and normalization operations treat the anchor
specially and maintain more information on it than other arguments. Therefore when attaching an
attribute to an expression, that expression should be the first argument, optionally followed by
additional related expressions. */
type attribute = type attribute =
| Aresource of res_action /** resource acquire/release */ | Aresource of res_action /** resource acquire/release */
| Aautorelease | Aautorelease
@ -203,8 +210,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
type atom = type atom =
| Aeq of exp exp /** equality */ | Aeq of exp exp /** equality */
| Aneq of exp exp /** disequality */ | Aneq of exp exp /** disequality */
| Apred of attribute exp /** predicate symbol applied to an exp */ | Apred of attribute (list exp) /** predicate symbol applied to exps */
| Anpred of attribute exp /** negated predicate symbol applied to an exp */; | Anpred of attribute (list exp) /** negated predicate symbol applied to exps */;
/** kind of lseg or dllseg predicates */ /** kind of lseg or dllseg predicates */
@ -705,21 +712,21 @@ let atom_compare a b =>
} }
| (Aneq _, _) => (-1) | (Aneq _, _) => (-1)
| (_, Aneq _) => 1 | (_, Aneq _) => 1
| (Apred a1 e1, Apred a2 e2) => | (Apred a1 es1, Apred a2 es2) =>
let n = attribute_compare a1 a2; let n = attribute_compare a1 a2;
if (n != 0) { if (n != 0) {
n n
} else { } else {
exp_compare e1 e2 IList.compare exp_compare es1 es2
} }
| (Apred _, _) => (-1) | (Apred _, _) => (-1)
| (_, Apred _) => 1 | (_, Apred _) => 1
| (Anpred a1 e1, Anpred a2 e2) => | (Anpred a1 es1, Anpred a2 es2) =>
let n = attribute_compare a1 a2; let n = attribute_compare a1 a2;
if (n != 0) { if (n != 0) {
n n
} else { } else {
exp_compare e1 e2 IList.compare exp_compare es1 es2
} }
} }
}; };
@ -1286,8 +1293,8 @@ let pp_atom pe0 f a => {
| PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2 | PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2
| PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2 | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2
} }
| Apred a e => F.fprintf f "%s(%a)" (attribute_to_string pe a) (pp_exp pe) e | Apred a es => F.fprintf f "%s(%a)" (attribute_to_string pe a) (pp_comma_seq (pp_exp pe)) es
| Anpred a e => F.fprintf f "!%s(%a)" (attribute_to_string pe a) (pp_exp pe) e | Anpred a es => F.fprintf f "!%s(%a)" (attribute_to_string pe a) (pp_comma_seq (pp_exp pe)) es
}; };
color_post_wrapper changed pe0 f color_post_wrapper changed pe0 f
}; };
@ -1942,8 +1949,8 @@ let atom_expmap (f: exp => exp) =>
fun fun
| Aeq e1 e2 => Aeq (f e1) (f e2) | Aeq e1 e2 => Aeq (f e1) (f e2)
| Aneq e1 e2 => Aneq (f e1) (f e2) | Aneq e1 e2 => Aneq (f e1) (f e2)
| Apred a e => Apred a (f e) | Apred a es => Apred a (IList.map f es)
| Anpred a e => Anpred a (f e); | Anpred a es => Anpred a (IList.map f es);
let atom_list_expmap (f: exp => exp) (alist: list atom) => IList.map (atom_expmap f) alist; let atom_list_expmap (f: exp => exp) (alist: list atom) => IList.map (atom_expmap f) alist;
@ -2080,8 +2087,8 @@ let atom_fpv =
fun fun
| Aeq e1 e2 => exp_fpv e1 @ exp_fpv e2 | Aeq e1 e2 => exp_fpv e1 @ exp_fpv e2
| Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2 | Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2
| Apred _ e | Apred _ es
| Anpred _ e => exp_fpv e; | Anpred _ es => IList.fold_left (fun fpv e => IList.rev_append (exp_fpv e) fpv) [] es;
let rec strexp_fpv = let rec strexp_fpv =
fun fun
@ -2292,8 +2299,8 @@ let atom_fav_add fav =>
exp_fav_add fav e1; exp_fav_add fav e1;
exp_fav_add fav e2 exp_fav_add fav e2
} }
| Apred _ e | Apred _ es
| Anpred _ e => exp_fav_add fav e; | Anpred _ es => IList.iter (fun e => exp_fav_add fav e) es;
let atom_fav = fav_imperative_to_functional atom_fav_add; let atom_fav = fav_imperative_to_functional atom_fav_add;

13
infer/src/IR/Sil.rei
Unescape View File

@ -73,7 +73,14 @@ type res_action = {
}; };
/** Attributes */ /** Attributes are nary function symbols that are applied to expression arguments in Apred and
Anpred atomic formulas. Many operations don't make much sense for nullary predicates, and are
generally treated as no-ops. The first argument is treated specially, as the "anchor" of the
predicate application. For example, adding or removing an attribute uses the anchor to identify
the atom to operate on. Also, abstraction and normalization operations treat the anchor
specially and maintain more information on it than other arguments. Therefore when attaching an
attribute to an expression, that expression should be the first argument, optionally followed by
additional related expressions. */
type attribute = type attribute =
| Aresource of res_action /** resource acquire/release */ | Aresource of res_action /** resource acquire/release */
| Aautorelease | Aautorelease
@ -197,8 +204,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
type atom = type atom =
| Aeq of exp exp /** equality */ | Aeq of exp exp /** equality */
| Aneq of exp exp /** disequality */ | Aneq of exp exp /** disequality */
| Apred of attribute exp /** predicate symbol applied to an exp */ | Apred of attribute (list exp) /** predicate symbol applied to exps */
| Anpred of attribute exp /** negated predicate symbol applied to an exp */; | Anpred of attribute (list exp) /** negated predicate symbol applied to exps */;
/** kind of lseg or dllseg predicates */ /** kind of lseg or dllseg predicates */

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

@ -788,7 +788,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
| Sil.Const _ -> a :: pi | Sil.Const _ -> a :: pi
| _ -> pi) | _ -> pi)
| Sil.Aneq (Var _, _) | Sil.Aneq (Var _, _)
| Sil.Apred (_, Var _) | Anpred (_, Var _) -> a :: pi | Sil.Apred (_, Var _ :: _) | Anpred (_, Var _ :: _) -> a :: pi
| Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> pi | Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> pi
) )
[] pi_filtered in [] pi_filtered in
@ -820,11 +820,11 @@ let abstract_gc p =
let no_fav_e1 = Sil.fav_is_empty fav_e1 in let no_fav_e1 = Sil.fav_is_empty fav_e1 in
let no_fav_e2 = Sil.fav_is_empty fav_e2 in let no_fav_e2 = Sil.fav_is_empty fav_e2 in
(no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ()) (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
| Sil.Apred (_, e) | Anpred (_, e) -> | (Sil.Apred _ | Anpred _) as a ->
let fav_e = Sil.exp_fav e in let fav_a = Sil.atom_fav a in
Sil.fav_is_empty fav_e Sil.fav_is_empty fav_a
|| ||
IList.intersect Ident.compare (Sil.fav_to_list fav_e) (Sil.fav_to_list fav_p_without_pi) in IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi) in
let new_pi = IList.filter strong_filter pi in let new_pi = IList.filter strong_filter pi in
let prop = Prop.normalize (Prop.replace_pi new_pi p) in let prop = Prop.normalize (Prop.replace_pi new_pi p) in
match Prop.prop_iter_create prop with match Prop.prop_iter_create prop with

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

@ -718,13 +718,13 @@ end = struct
when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
build_other_atoms (fun e0 -> Prop.mk_neq e0 e') side e build_other_atoms (fun e0 -> Prop.mk_neq e0 e') side e
| Sil.Apred (a, (Var id as e)) | Sil.Apred (a, (Var id as e) :: es)
when not (Ident.is_normal id) -> when not (Ident.is_normal id) && IList.for_all exp_contains_only_normal_ids es ->
build_other_atoms (fun e0 -> Prop.mk_pred a e0) side e build_other_atoms (fun e0 -> Prop.mk_pred a (e0 :: es)) side e
| Sil.Anpred (a, (Var id as e)) | Sil.Anpred (a, (Var id as e) :: es)
when not (Ident.is_normal id) -> when not (Ident.is_normal id) && IList.for_all exp_contains_only_normal_ids es ->
build_other_atoms (fun e0 -> Prop.mk_npred a e0) side e build_other_atoms (fun e0 -> Prop.mk_npred a (e0 :: es)) side e
| Sil.Aeq((Sil.Var id as e), e') | Sil.Aeq(e', (Sil.Var id as e)) | Sil.Aeq((Sil.Var id as e), e') | Sil.Aeq(e', (Sil.Var id as e))
when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
@ -1674,8 +1674,8 @@ let pi_partial_join mode
true true
| Sil.Aneq _ -> false | Sil.Aneq _ -> false
| Sil.Aeq _ as e -> Prop.atom_is_inequality e | Sil.Aeq _ as e -> Prop.atom_is_inequality e
| Sil.Apred (_, e) | Anpred (_, e) -> | Sil.Apred (_, es) | Anpred (_, es) ->
exp_is_const e in IList.for_all exp_is_const es in
begin begin
if Config.trace_join then begin if Config.trace_join then begin
L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln (); L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln ();

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

@ -313,7 +313,7 @@ let execute___cast 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.get_resource_attribute prop n_lexp with
| Some (Apred (Aresource ra, _)) -> | Some (Apred (Aresource ra, _)) ->
Prop.add_or_replace_exp_attribute prop (Apred (Aresource { ra with ra_res }, n_lexp)) Prop.add_or_replace_attribute prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
| _ -> | _ ->
let pname = Sil.mem_alloc_pname Sil.Mnew in let pname = Sil.mem_alloc_pname Sil.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_exp_attribute prop (Apred (Aresource ra, n_lexp)) in Prop.add_or_replace_attribute 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_exp_attribute prop (Apred (Aautorelease, n_lexp)) in let prop' = Prop.add_or_replace_attribute 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,11 +555,11 @@ 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 Sil.Aautorelease prop_ in let autoreleased_objects = Prop.get_atoms_with_attribute prop_ Sil.Aautorelease in
let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in
let call_release res exp = let call_release res atom =
match res with match res, atom with
| (prop', path'):: _ -> | ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
(try (try
let hpred = IList.find (function let hpred = IList.find (function
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
@ -575,19 +575,19 @@ let execute___release_autorelease_pool
res1 res1
| _ -> res | _ -> res
with Not_found -> res) with Not_found -> res)
| [] -> res in | _ -> res in
IList.fold_left call_release [(prop_without_attribute, path)] autoreleased_objects IList.fold_left call_release [(prop_without_attribute, path)] autoreleased_objects
else execute___no_op prop_ path else execute___no_op prop_ path
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_exp_attribute prop (Apred (attr, n_lexp)), path)] [(Prop.add_or_replace_attribute 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.remove_attribute_from_exp prop (Apred (attr, [n_lexp])), path)]
(** Set attibute att *) (** Set attibute att *)
@ -694,8 +694,8 @@ let _execute_free mk loc acc iter =
Sil.ra_vpath = None } in Sil.ra_vpath = None } in
(* mark value as freed *) (* mark value as freed *)
let p_res = let p_res =
Prop.add_or_replace_exp_attribute_check_changed Prop.add_or_replace_attribute_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 *)
| _ -> assert false (* should not happen *) | _ -> assert false (* should not happen *)
@ -796,7 +796,7 @@ let execute_alloc mk can_return_null
Sil.ra_loc = loc; Sil.ra_loc = loc;
Sil.ra_vpath = None } in Sil.ra_vpath = None } in
(* mark value as allocated *) (* mark value as allocated *)
Prop.add_or_replace_exp_attribute prop' (Apred (Aresource ra, exp_new)) in Prop.add_or_replace_attribute prop' (Apred (Aresource ra, [exp_new])) in
let prop_alloc = Prop.conjoin_eq (Sil.Var ret_id) exp_new prop_plus_ptsto in let prop_alloc = Prop.conjoin_eq (Sil.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 (Sil.Var ret_id) Sil.exp_zero prop in let prop_null = Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop in

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

@ -1034,10 +1034,10 @@ let atom_normalize sub a0 =
handle_boolean_operation true e1 e2 handle_boolean_operation true e1 e2
| Sil.Aneq (e1, e2) -> | Sil.Aneq (e1, e2) ->
handle_boolean_operation false e1 e2 handle_boolean_operation false e1 e2
| Sil.Apred (a, e) -> | Sil.Apred (a, es) ->
Sil.Apred (a, exp_normalize sub e) Sil.Apred (a, IList.map (fun e -> exp_normalize sub e) es)
| Sil.Anpred (a, e) -> | Sil.Anpred (a, es) ->
Sil.Anpred (a, exp_normalize sub e) in Sil.Anpred (a, IList.map (fun e -> exp_normalize sub e) es) in
if atom_is_inequality a' then inequality_normalize a' else a' if atom_is_inequality a' then inequality_normalize a' else a'
(** Negate an atom *) (** Negate an atom *)
@ -1048,8 +1048,8 @@ let atom_negate = function
mk_inequality (Sil.exp_le e2 e1) mk_inequality (Sil.exp_le e2 e1)
| Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2) | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
| Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2) | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
| Sil.Apred (a, e) -> Sil.Anpred (a, e) | Sil.Apred (a, es) -> Sil.Anpred (a, es)
| Sil.Anpred (a, e) -> Sil.Apred (a, e) | Sil.Anpred (a, es) -> Sil.Apred (a, es)
let rec strexp_normalize sub se = let rec strexp_normalize sub se =
match se with match se with
@ -1475,10 +1475,10 @@ let mk_neq e1 e2 = mk_atom (Aneq (e1, e2))
let mk_eq e1 e2 = mk_atom (Aeq (e1, e2)) let mk_eq e1 e2 = mk_atom (Aeq (e1, e2))
(** Construct a pred. *) (** Construct a pred. *)
let mk_pred a e = mk_atom (Apred (a, e)) let mk_pred a es = mk_atom (Apred (a, es))
(** Construct a negated pred. *) (** Construct a negated pred. *)
let mk_npred a e = mk_atom (Anpred (a, e)) let mk_npred a es = mk_atom (Anpred (a, es))
(** Construct a points-to predicate for a single program variable. (** Construct a points-to predicate for a single program variable.
If [expand_structs] is true, initialize the fields of structs with fresh variables. *) If [expand_structs] is true, initialize the fields of structs with fresh variables. *)
@ -1613,7 +1613,7 @@ let compute_reachable_atoms pi exps =
IList.filter IList.filter
(function (function
| Sil.Aeq (lhs, rhs) | Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs | Sil.Aeq (lhs, rhs) | Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs
| Sil.Apred (_, e) | Anpred (_, e) -> exp_contains e) | Sil.Apred (_, es) | Anpred (_, es) -> IList.exists exp_contains es)
pi pi
(** Eliminates all empty lsegs from sigma, and collect equalities (** Eliminates all empty lsegs from sigma, and collect equalities
@ -1776,21 +1776,21 @@ let prop_reset_inst inst_map prop =
(** {2 Attributes} *) (** {2 Attributes} *)
(** 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_exp_attribute atom = let atom_get_attribute 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 *) (** Check whether an atom is used to mark an attribute *)
let atom_is_attribute a = let atom_is_attribute a =
atom_get_exp_attribute a <> None atom_get_attribute a <> None
(** Get the attribute associated to the expression, if any *) (** Get the attribute associated to the expression, if any *)
let get_exp_attributes prop exp = let get_attributes prop exp =
let nexp = exp_normalize_prop prop exp in let nexp = exp_normalize_prop prop exp in
let atom_get_attr attributes atom = let atom_get_attr attributes atom =
match atom with match atom with
| Sil.Apred (_, e) | Anpred (_, e) when Sil.exp_equal e nexp -> atom :: attributes | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Sil.exp_equal nexp es -> atom :: attributes
| _ -> attributes in | _ -> attributes in
IList.fold_left atom_get_attr [] prop.pi IList.fold_left atom_get_attr [] prop.pi
@ -1800,7 +1800,7 @@ let attributes_in_same_category attr1 attr2 =
Sil.attribute_category_equal cat1 cat2 Sil.attribute_category_equal cat1 cat2
let get_attribute prop exp category = let get_attribute prop exp category =
let atts = get_exp_attributes prop exp in let atts = get_attributes prop exp in
try try
Some Some
(IList.find (function (IList.find (function
@ -1835,7 +1835,7 @@ let get_retval_attribute prop exp =
get_attribute prop exp Sil.ACretval get_attribute prop exp Sil.ACretval
let has_dangling_uninit_attribute prop exp = let has_dangling_uninit_attribute prop exp =
let la = get_exp_attributes prop exp in let la = get_attributes prop exp in
IList.exists (function IList.exists (function
| Sil.Apred (a, _) -> Sil.attribute_equal a (Adangling DAuninit) | Sil.Apred (a, _) -> Sil.attribute_equal a (Adangling DAuninit)
| _ -> false | _ -> false
@ -1844,49 +1844,50 @@ let has_dangling_uninit_attribute prop exp =
(** Get all the attributes of the prop *) (** Get all the attributes of the prop *)
let get_all_attributes prop = let get_all_attributes prop =
let res = ref [] in let res = ref [] in
let do_atom a = match atom_get_exp_attribute a with let do_atom a = match atom_get_attribute a with
| Some attr -> res := attr :: !res | Some attr -> res := attr :: !res
| None -> () in | None -> () in
IList.iter do_atom prop.pi; IList.iter do_atom prop.pi;
IList.rev !res IList.rev !res
(** Set an attribute associated to the expression *) (** Set an attribute associated to the argument expressions *)
let set_exp_attribute ?(footprint = false) ?(polarity = true) prop attr exp = let set_attribute ?(footprint = false) ?(polarity = true) prop attr args =
prop_atom_and ~footprint prop prop_atom_and ~footprint prop
(if polarity then Sil.Apred (attr, exp) else Sil.Anpred (attr, exp)) (if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
(** Replace an attribute associated to the expression *) (** Replace an attribute associated to the expression *)
let add_or_replace_exp_attribute_check_changed check_attribute_change prop atom0 = let add_or_replace_attribute_check_changed check_attribute_change prop atom0 =
match atom0 with match atom0 with
| Sil.Apred (att0, exp0) | Anpred (att0, exp0) -> | Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
let nexp = exp_normalize_prop prop exp0 in let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps0 in
let atom = Sil.atom_replace_exp [(exp0, nexp)] atom0 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 let atom_map = function
| Sil.Apred (att, exp) | Anpred (att, exp) | Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
when Sil.exp_equal nexp exp && attributes_in_same_category att att0 -> when Sil.exp_equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0; check_attribute_change att att0;
atom natom
| a -> | atom ->
a in atom in
let pi = get_pi prop in let pi = get_pi prop in
let pi' = IList.map_changed atom_map pi in let pi' = IList.map_changed atom_map pi in
if pi == pi' if pi == pi'
then prop_atom_and prop atom then prop_atom_and prop natom
else replace_pi pi' prop else replace_pi pi' prop
| _ -> | _ ->
prop prop
let add_or_replace_exp_attribute prop atom = let add_or_replace_attribute prop atom =
(* wrapper for the most common case: do nothing *) (* wrapper for the most common case: do nothing *)
let check_attr_changed = (fun _ _ -> ()) in let check_attr_changed = (fun _ _ -> ()) in
add_or_replace_exp_attribute_check_changed check_attr_changed prop atom add_or_replace_attribute_check_changed check_attr_changed prop atom
(** mark Sil.Var's or Sil.Lvar's as undefined *) (** mark Sil.Var's or Sil.Lvar's as undefined *)
let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos = let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in
let mark_var_as_undefined exp prop = let mark_var_as_undefined exp prop =
match exp with match exp with
| Sil.Var _ | Lvar _ -> add_or_replace_exp_attribute prop (Apred (att_undef, exp)) | Sil.Var _ | Lvar _ -> add_or_replace_attribute prop (Apred (att_undef, [exp]))
| _ -> prop in | _ -> prop in
IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
@ -1910,9 +1911,9 @@ let remove_resource_attribute ra_kind ra_res =
let remove_attribute_from_exp prop atom = let remove_attribute_from_exp prop atom =
match atom with match atom with
| Sil.Apred (_, exp) | Anpred (_, exp) -> | Sil.Apred (_, exps) | Anpred (_, exps) ->
let nexp = exp_normalize_prop prop exp in let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in
let natom = Sil.atom_replace_exp [(exp,nexp)] atom in let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
let f a = not (Sil.atom_equal natom a) in let f a = not (Sil.atom_equal natom a) in
filter_atoms ~f prop filter_atoms ~f prop
| _ -> | _ ->
@ -1925,7 +1926,7 @@ let replace_objc_null prop lhs_exp rhs_exp =
let prop = remove_attribute_from_exp prop atom in let prop = remove_attribute_from_exp prop atom in
let prop = conjoin_eq rhs_exp Sil.exp_zero prop in let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
add_or_replace_exp_attribute prop natom add_or_replace_attribute prop natom
| _ -> prop | _ -> prop
let rec nullify_exp_with_objc_null prop exp = let rec nullify_exp_with_objc_null prop exp =
@ -1944,14 +1945,11 @@ let rec nullify_exp_with_objc_null prop exp =
| _ -> prop | _ -> prop
(** Get all the attributes of the prop *) (** Get all the attributes of the prop *)
let get_atoms_with_attribute att prop = let get_atoms_with_attribute prop att =
let atom_remove atom autoreleased_atoms = match atom with IList.filter (function
| Sil.Apred (att_old, e) | Anpred (att_old, e) -> | Sil.Apred (att', _) | Anpred (att', _) -> Sil.attribute_equal att' att
if Sil.attribute_equal att_old att then | _ -> false
e:: autoreleased_atoms ) (get_pi prop)
else autoreleased_atoms
| _ -> autoreleased_atoms in
IList.fold_right atom_remove (get_pi prop) []
(** Apply f to every resource attribute in the prop *) (** Apply f to every resource attribute in the prop *)
let attribute_map_resource prop f = let attribute_map_resource prop f =
@ -1959,8 +1957,8 @@ let attribute_map_resource prop f =
| Sil.Aresource ra -> Sil.Aresource (f e ra) | Sil.Aresource ra -> Sil.Aresource (f e ra)
| att -> att in | att -> att in
let atom_map = function let atom_map = function
| Sil.Apred (att, e) -> Sil.Apred (attribute_map e att, e) | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es)
| Sil.Anpred (att, e) -> Sil.Anpred (attribute_map e att, e) | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es)
| atom -> atom in | atom -> atom in
replace_pi (IList.map atom_map (get_pi prop)) prop replace_pi (IList.map atom_map (get_pi prop)) prop
@ -1981,7 +1979,7 @@ let find_arithmetic_problem proc_node_session prop exp =
match exp_normalize_prop prop e with match exp_normalize_prop prop e with
| Sil.Const c when iszero_int_float c -> true | Sil.Const c when iszero_int_float c -> true
| _ -> | _ ->
res := add_or_replace_exp_attribute !res (Apred (Adiv0 proc_node_session, e)); res := add_or_replace_attribute !res (Apred (Adiv0 proc_node_session, [e]));
false in false in
let rec walk = function let rec walk = function
| Sil.Var _ -> () | Sil.Var _ -> ()
@ -2039,7 +2037,8 @@ let deallocate_stack_vars p pvars =
if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *) if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
begin begin
stack_vars_address_in_post := v :: !stack_vars_address_in_post; stack_vars_address_in_post := v :: !stack_vars_address_in_post;
res := add_or_replace_exp_attribute !res (Apred (Adangling DAaddr_stack_var, Var freshv)) let pred = Sil.Apred (Adangling DAaddr_stack_var, [Sil.Var freshv]) in
res := add_or_replace_attribute !res pred
end in end in
IList.iter do_var !fresh_address_vars; IList.iter do_var !fresh_address_vars;
!res in !res in
@ -2301,10 +2300,10 @@ let atom_captured_ren ren = function
Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2) Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2)
| Sil.Aneq (e1, e2) -> | Sil.Aneq (e1, e2) ->
Sil.Aneq (exp_captured_ren ren e1, exp_captured_ren ren e2) Sil.Aneq (exp_captured_ren ren e1, exp_captured_ren ren e2)
| Sil.Apred (a, e) -> | Sil.Apred (a, es) ->
Sil.Apred (a, exp_captured_ren ren e) Sil.Apred (a, IList.map (fun e -> exp_captured_ren ren e) es)
| Sil.Anpred (a, e) -> | Sil.Anpred (a, es) ->
Sil.Anpred (a, exp_captured_ren ren e) Sil.Anpred (a, IList.map (fun e -> exp_captured_ren ren e) es)
let rec strexp_captured_ren ren = function let rec strexp_captured_ren ren = function
| Sil.Eexp (e, inst) -> | Sil.Eexp (e, inst) ->

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

@ -223,10 +223,10 @@ val mk_neq : exp -> exp -> atom
val mk_eq : exp -> exp -> atom val mk_eq : exp -> exp -> atom
(** Construct a positive pred. *) (** Construct a positive pred. *)
val mk_pred : attribute -> exp -> atom val mk_pred : attribute -> exp list -> atom
(** Construct a negative pred. *) (** Construct a negative pred. *)
val mk_npred : attribute -> exp -> atom val mk_npred : attribute -> exp list -> atom
(** create a strexp of the given type, populating the structures if [expand_structs] is true *) (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
val create_strexp_of_type : val create_strexp_of_type :
@ -285,10 +285,10 @@ val atom_is_attribute : atom -> bool
val attribute_map_resource : normal t -> (Sil.exp -> Sil.res_action -> Sil.res_action) -> normal t val attribute_map_resource : normal t -> (Sil.exp -> Sil.res_action -> Sil.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_exp_attribute : atom -> atom option val atom_get_attribute : atom -> atom option
(** Get the attributes associated to the expression, if any *) (** Get the attributes associated to the expression, if any *)
val get_exp_attributes : 'a t -> exp -> atom list val get_attributes : 'a t -> exp -> atom list
(** Get the undef attribute associated to the expression, if any *) (** Get the undef attribute associated to the expression, if any *)
val get_undef_attribute : 'a t -> exp -> atom option val get_undef_attribute : 'a t -> exp -> atom option
@ -319,15 +319,15 @@ val get_all_attributes : 'a t -> atom list
val has_dangling_uninit_attribute : 'a t -> exp -> bool val has_dangling_uninit_attribute : 'a t -> exp -> bool
(** Set an attribute associated to the expression *) (** Set an attribute associated to the argument expressions *)
val set_exp_attribute : ?footprint: bool -> ?polarity: bool -> val set_attribute : ?footprint: bool -> ?polarity: bool ->
normal t -> attribute -> exp -> normal t normal t -> attribute -> exp list -> normal t
val add_or_replace_exp_attribute_check_changed : val add_or_replace_attribute_check_changed :
(Sil.attribute -> Sil.attribute -> unit) -> normal t -> atom -> normal t (Sil.attribute -> Sil.attribute -> unit) -> normal t -> atom -> normal t
(** Replace an attribute associated to the expression *) (** Replace an attribute associated to the expression *)
val add_or_replace_exp_attribute : normal t -> atom -> normal t val add_or_replace_attribute : normal t -> atom -> normal t
(** mark Sil.Var's or Sil.Lvar's as undefined *) (** mark Sil.Var's or Sil.Lvar's as undefined *)
val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Typ.item_annotation -> val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Typ.item_annotation ->
@ -347,8 +347,8 @@ val nullify_exp_with_objc_null : normal t -> exp -> normal t
(** Remove an attribute from an exp in the heap *) (** Remove an attribute from an exp in the heap *)
val remove_attribute_from_exp : 'a t -> atom -> normal t val remove_attribute_from_exp : 'a t -> atom -> normal t
(** Retireve all the atoms in the heap that contain a specific attribute *) (** Retrieve all the atoms that contain a specific attribute *)
val get_atoms_with_attribute : Sil.attribute -> 'a t -> Sil.exp list val get_atoms_with_attribute : 'a t -> Sil.attribute -> Sil.atom list
(** Return the sub part of [prop]. *) (** Return the sub part of [prop]. *)
val get_sub : 'a t -> subst val get_sub : 'a t -> subst

38
infer/src/backend/propgraph.ml
Unescape View File

@ -44,13 +44,14 @@ let edge_is_hpred = function
(** Return the source of the edge *) (** Return the source of the edge *)
let edge_get_source = function let edge_get_source = function
| Ehpred (Sil.Hpointsto(e, _, _)) -> e | Ehpred (Sil.Hpointsto(e, _, _)) -> Some e
| Ehpred (Sil.Hlseg(_, _, e, _, _)) -> e | Ehpred (Sil.Hlseg(_, _, e, _, _)) -> Some e
| Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> e1 (* only one direction supported for now *) | Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> Some e1 (* only one direction supported for now *)
| Eatom (Sil.Aeq (e1, _)) -> e1 | Eatom (Sil.Aeq (e1, _)) -> Some e1
| Eatom (Sil.Aneq (e1, _)) -> e1 | Eatom (Sil.Aneq (e1, _)) -> Some e1
| Eatom (Sil.Apred (_, e) | Anpred (_, e)) -> e | Eatom (Sil.Apred (_, e :: _) | Anpred (_, e :: _)) -> Some e
| Esub_entry (x, _) -> Sil.Var x | Eatom (Sil.Apred (_, []) | Anpred (_, [])) -> None
| Esub_entry (x, _) -> Some (Sil.Var x)
(** Return the successor nodes of the edge *) (** Return the successor nodes of the edge *)
let edge_get_succs = function let edge_get_succs = function
@ -74,7 +75,11 @@ let edge_from_source g n footprint_part is_hpred =
if is_hpred if is_hpred
then IList.map (fun hpred -> Ehpred hpred ) (get_sigma footprint_part g) then IList.map (fun hpred -> Ehpred hpred ) (get_sigma footprint_part g)
else IList.map (fun a -> Eatom a) (get_pi footprint_part g) @ IList.map (fun entry -> Esub_entry entry) (get_subl footprint_part g) in else IList.map (fun a -> Eatom a) (get_pi footprint_part g) @ IList.map (fun entry -> Esub_entry entry) (get_subl footprint_part g) in
match IList.filter (fun hpred -> Sil.exp_equal n (edge_get_source hpred)) edges with let starts_from hpred =
match edge_get_source hpred with
| Some e -> Sil.exp_equal n e
| None -> false in
match IList.filter starts_from edges with
| [] -> None | [] -> None
| edge:: _ -> Some edge | edge:: _ -> Some edge
@ -159,10 +164,9 @@ let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list = match olded
compute_exp_diff e1 e2 compute_exp_diff e1 e2
| Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) -> | Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) ->
compute_exp_diff e1 e2 compute_exp_diff e1 e2
| Eatom (Sil.Apred (_, e1)), Eatom (Sil.Apred (_, e2)) -> | Eatom (Sil.Apred (_, es1)), Eatom (Sil.Apred (_, es2))
compute_exp_diff e1 e2 | Eatom (Sil.Anpred (_, es1)), Eatom (Sil.Anpred (_, es2)) ->
| Eatom (Sil.Anpred (_, e1)), Eatom (Sil.Anpred (_, e2)) -> IList.flatten (try IList.map2 compute_exp_diff es1 es2 with IList.Fail -> [])
compute_exp_diff e1 e2
| Esub_entry (_, e1), Esub_entry (_, e2) -> | Esub_entry (_, e1), Esub_entry (_, e2) ->
compute_exp_diff e1 e2 compute_exp_diff e1 e2
| _ -> [Obj.repr newedge] | _ -> [Obj.repr newedge]
@ -173,8 +177,10 @@ let compute_diff default_color oldgraph newgraph : diff =
let newedges = get_edges footprint_part newgraph in let newedges = get_edges footprint_part newgraph in
let changed = ref [] in let changed = ref [] in
let build_changed edge = let build_changed edge =
if not (contains_edge footprint_part oldgraph edge) then begin if not (contains_edge footprint_part oldgraph edge) then
match edge_from_source oldgraph (edge_get_source edge) footprint_part (edge_is_hpred edge) with match edge_get_source edge with
| Some source -> (
match edge_from_source oldgraph source footprint_part (edge_is_hpred edge) with
| None -> | None ->
let changed_obj = match edge with let changed_obj = match edge with
| Ehpred hpred -> Obj.repr hpred | Ehpred hpred -> Obj.repr hpred
@ -182,7 +188,9 @@ let compute_diff default_color oldgraph newgraph : diff =
| Esub_entry entry -> Obj.repr entry in | Esub_entry entry -> Obj.repr entry in
changed := changed_obj :: !changed changed := changed_obj :: !changed
| Some oldedge -> changed := compute_edge_diff oldedge edge @ !changed | Some oldedge -> changed := compute_edge_diff oldedge edge @ !changed
end in )
| None ->
() in
IList.iter build_changed newedges; IList.iter build_changed newedges;
let colormap (o: Obj.t) = let colormap (o: Obj.t) =
if IList.exists (fun x -> x == o) !changed then Red if IList.exists (fun x -> x == o) !changed then Red

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

@ -28,7 +28,7 @@ val is_root : node -> bool
val nodes_connected : node -> node -> bool val nodes_connected : node -> node -> bool
(** Return the source of the edge *) (** Return the source of the edge *)
val edge_get_source : edge -> node val edge_get_source : edge -> node option
(** Return the successor nodes of the edge *) (** Return the successor nodes of the edge *)
val edge_get_succs : edge -> node list val edge_get_succs : edge -> node list

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

@ -2109,14 +2109,12 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
imply_atom calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in)); imply_atom calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in));
pre_check_pure_implication calc_missing subs pi1 pi2' pre_check_pure_implication calc_missing subs pi1 pi2'
) )
| Sil.Aeq _ :: pi2' -> (* must be an inequality *) | (Sil.Aneq (e, _) | Apred (_, e :: _) | Anpred (_, e :: _)) :: _
pre_check_pure_implication calc_missing subs pi1 pi2' when not calc_missing && (match e with Var v -> not (Ident.is_primed v) | _ -> true) ->
| (Sil.Aneq (e, _) | Apred (_, e) | Anpred (_, e)) :: pi2' ->
if calc_missing || (match e with Var v -> Ident.is_primed v | _ -> false) then
pre_check_pure_implication calc_missing subs pi1 pi2'
else
raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var", raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var",
(Sil.sub_empty, Sil.sub_empty), EXC_FALSE)) (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
| (Sil.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
pre_check_pure_implication calc_missing subs pi1 pi2'
(** Perform the array bound checks delayed (to instantiate variables) by the prover. (** Perform the array bound checks delayed (to instantiate variables) by the prover.
If there is a provable violation of the array bounds, set the prover status to Bounds_check If there is a provable violation of the array bounds, set the prover status to Bounds_check

6
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_exp_attributes prop guarded_by_exp) in (Prop.get_attributes 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_exp_attribute ~footprint:true prop Alocked guarded_by_exp Prop.set_attribute ~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_exp_attributes prop exp) in IList.exists is_nullable_attr (Prop.get_attributes 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, _), Sil.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _, _)) ->

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

@ -476,11 +476,11 @@ let check_already_dereferenced pname cond prop =
raising an exception in that case *) raising an exception in that case *)
let check_deallocate_static_memory prop_after = let check_deallocate_static_memory prop_after =
let check_deallocated_attribute = function let check_deallocated_attribute = function
| Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Lvar pv) | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), [Lvar pv])
when Pvar.is_local pv || Pvar.is_global pv -> when Pvar.is_local pv || Pvar.is_global pv ->
let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in
raise (Exceptions.Deallocate_stack_variable freed_desc) raise (Exceptions.Deallocate_stack_variable freed_desc)
| Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Const (Cstr s)) -> | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), [Const (Cstr s)]) ->
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
@ -738,7 +738,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
| [ret_id] -> ( | [ret_id] -> (
match Prop.find_equal_formal_path receiver prop with match Prop.find_equal_formal_path receiver prop with
| Some (v,fs) -> | Some (v,fs) ->
Prop.add_or_replace_exp_attribute prop (Apred (Aobjc_null (v,fs), Var ret_id)) Prop.add_or_replace_attribute prop (Apred (Aobjc_null (v,fs), [Sil.Var ret_id]))
| None -> | None ->
Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop
) )
@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
| Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop | Typ.Tptr _ -> Prop.conjoin_neq exp Sil.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_exp_attribute prop (Apred (Ataint callee_pname, ret_exp)) in Prop.add_or_replace_attribute 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 = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in let taint_info = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in
Prop.add_or_replace_exp_attribute prop (Apred (Ataint taint_info, Var lhs_id)) Prop.add_or_replace_attribute prop (Apred (Ataint taint_info, [Sil.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_exp_attribute prop' (Apred (Adangling DAuninit, Var id)) Prop.add_or_replace_attribute prop' (Apred (Adangling DAuninit, [Sil.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_exp_attributes prop exp) in IList.fold_left fold_undef_pname None (Prop.get_attributes 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 *)
@ -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_exp_attribute prop (Apred (Auntaint taint_info, exp)) Prop.add_or_replace_attribute prop (Apred (Auntaint taint_info, [exp]))
| _ -> | _ ->
if !Config.footprint then if !Config.footprint then
let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
(* add untained(n_lexp) to the footprint *) (* add untained(n_lexp) to the footprint *)
Prop.set_exp_attribute ~footprint:true prop (Auntaint taint_info) exp Prop.set_attribute ~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 *)
@ -1393,7 +1393,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
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.remove_attribute q res
| _ -> q in | _ -> q in
IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in IList.fold_left do_attribute p (Prop.get_attributes 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 ->

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

@ -362,7 +362,7 @@ let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list =
let check_path_errors_in_post caller_pname post post_path = let check_path_errors_in_post caller_pname post post_path =
let check_attr atom = let check_attr atom =
match atom with match atom with
| Sil.Apred (Adiv0 path_pos, e) -> | Sil.Apred (Adiv0 path_pos, [e]) ->
if Prover.check_zero e then if Prover.check_zero e then
let desc = Errdesc.explain_divide_by_zero e (State.get_node ()) (State.get_loc ()) in let desc = Errdesc.explain_divide_by_zero e (State.get_node ()) (State.get_loc ()) in
let new_path, path_pos_opt = let new_path, path_pos_opt =
@ -386,12 +386,12 @@ let post_process_post
| 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
| Sil.Apred (Aresource ra, e) | Sil.Apred (Aresource ra, [e])
when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) -> when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) ->
(* unless it was already freed before the call *) (* unless it was already freed before the call *)
let vpath, _ = Errdesc.vpath_find post e in let vpath, _ = Errdesc.vpath_find post e in
let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in
Sil.Apred (Aresource ra', e) Sil.Apred (Aresource ra', [e])
| a -> a in | a -> a in
let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in
let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in
@ -603,10 +603,10 @@ let prop_copy_footprint_pure p1 p2 =
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_exp_attribute atom with match Prop.atom_get_attribute atom with
| None -> prop | None -> prop
| Some atom -> | Some atom ->
Prop.add_or_replace_exp_attribute_check_changed check_attr_dealloc_mismatch prop atom in Prop.add_or_replace_attribute_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 *)
@ -884,7 +884,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
let last_call_ret_non_null = let last_call_ret_non_null =
IList.exists IList.exists
(function (function
| 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 Sil.exp_zero Prover.check_disequal prop exp Sil.exp_zero
| _ -> false) | _ -> false)
(Prop.get_all_attributes prop) in (Prop.get_all_attributes prop) in
@ -904,8 +904,8 @@ 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_exp_attribute prop_normal Prop.add_or_replace_attribute prop_normal
(Apred (Ataint { taint_source = callee_pname; taint_kind; }, Var ret_id)) (Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Sil.Var ret_id]))
|> Prop.expose in |> Prop.expose in
(prop', path) in (prop', path) in
IList.map taint_retval posts IList.map taint_retval posts
@ -936,11 +936,11 @@ 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_exp_attribute atom with match Prop.atom_get_attribute atom with
| Some (Apred (Ataint _, e)) -> | Some (Apred (Ataint _, [e])) ->
let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map
| Some (Apred (Auntaint _, e)) -> | Some (Apred (Auntaint _, [e])) ->
let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map
| _ -> acc_map in | _ -> acc_map in
@ -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_exp_attribute taint_atom with let taint_info = match Prop.atom_get_attribute 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
@ -1262,7 +1262,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
let ret_var = Sil.Var ret_id in let ret_var = Sil.Var ret_id in
let mark_id_as_retval (p, path) = let mark_id_as_retval (p, path) =
let att_retval = Sil.Aretval (callee_pname, ret_annot) in let att_retval = Sil.Aretval (callee_pname, ret_annot) in
Prop.set_exp_attribute p att_retval ret_var, path in Prop.set_attribute 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_exp_attribute prop_acc (Apred (att, rhs)) Prop.add_or_replace_attribute prop_acc (Apred (att, [rhs]))
| _ -> prop_acc) | _ -> prop_acc)
prop (Prop.get_sigma prop) prop (Prop.get_sigma prop)

Write Preview
Loading…
Cancel
Save