Move Prop.Attribute to toplevel

Summary:
This diff lifts the Prop.Attribute module out of Prop.  This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches.  Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.

Reviewed By: cristianoc

Differential Revision: D3684523

fbshipit-source-id: f37af8b
master
Josh Berdine 8 years ago committed by Facebook Github Bot 5
parent 60496f2ae4
commit 3896b10265

@ -987,7 +987,7 @@ let remove_abducted_retvars p =>
)
([], [])
(Prop.get_sigma p);
let (_, p') = Prop.deallocate_stack_vars p abducteds;
let (_, p') = Attribute.deallocate_stack_vars p abducteds;
let normal_pvar_set =
IList.fold_left
(fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set)
@ -1009,7 +1009,7 @@ let remove_locals (curr_f: Procdesc.t) p => {
names_of_block_locals @ names_of_locals @ names_of_static_locals
| _ => names_of_locals
};
let (removed, p') = Prop.deallocate_stack_vars p names_of_locals';
let (removed, p') = Attribute.deallocate_stack_vars p names_of_locals';
(
removed,
if Config.angelic_execution {
@ -1023,7 +1023,7 @@ let remove_locals (curr_f: Procdesc.t) p => {
let remove_formals (curr_f: Procdesc.t) p => {
let pname = Procdesc.get_proc_name curr_f;
let formal_vars = IList.map (fun (n, _) => Pvar.mk n pname) (Procdesc.get_formals curr_f);
Prop.deallocate_stack_vars p formal_vars
Attribute.deallocate_stack_vars p formal_vars
};
@ -1031,7 +1031,7 @@ let remove_formals (curr_f: Procdesc.t) p => {
let remove_ret (curr_f: Procdesc.t) (p: Prop.t Prop.normal) => {
let pname = Procdesc.get_proc_name curr_f;
let name_of_ret = Procdesc.get_ret_var curr_f;
let (_, p') = Prop.deallocate_stack_vars p [Pvar.to_callee pname name_of_ret];
let (_, p') = Attribute.deallocate_stack_vars p [Pvar.to_callee pname name_of_ret];
p'
};

@ -82,3 +82,21 @@ let pp pe f =>
| Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn;
let to_string c => pp_to_string (pp pe_text) c;
let iszero_int_float =
fun
| Cint i => IntLit.iszero i
| Cfloat 0.0 => true
| _ => false;
let isone_int_float =
fun
| Cint i => IntLit.isone i
| Cfloat 1.0 => true
| _ => false;
let isminusone_int_float =
fun
| Cint i => IntLit.isminusone i
| Cfloat (-1.0) => true
| _ => false;

@ -43,3 +43,9 @@ let kind_equal: t => t => bool;
let pp: printenv => F.formatter => t => unit;
let to_string: t => string;
let iszero_int_float: t => bool;
let isone_int_float: t => bool;
let isminusone_int_float: t => bool;

@ -0,0 +1,327 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
(** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *)
module L = Logging
module F = Format
(** Check whether an atom is used to mark an attribute *)
let is_pred atom =
match atom with
| Sil.Apred _ | Anpred _ -> true
| _ -> false
(** Add an attribute associated to the argument expressions *)
let add ?(footprint = false) ?(polarity = true) prop attr args =
Prop.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 -> Prop.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 = Prop.get_pi prop in
let pi' = IList.map_changed atom_map pi in
if pi == pi'
then Prop.prop_atom_and prop natom
else Prop.normalize (Prop.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: 'a Prop.t) =
let res = ref [] in
let do_atom a = if is_pred a then res := a :: !res in
IList.iter do_atom (Prop.get_pi prop);
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
) (Prop.get_pi prop)
(** Get the attribute associated to the expression, if any *)
let get_for_exp (prop: 'a Prop.t) exp =
let nexp = Prop.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.get_pi prop)
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
let get_undef prop exp =
get prop exp ACundef
let get_resource prop exp =
get prop exp ACresource
let get_taint prop exp =
get prop exp ACtaint
let get_autorelease prop exp =
get prop exp ACautorelease
let get_objc_null prop exp =
get prop exp ACobjc_null
let get_div0 prop exp =
get prop exp ACdiv0
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 =
let pi0 = Prop.get_pi prop in
let pi1 = IList.filter_changed f pi0 in
if pi1 == pi0 then
prop
else
Prop.normalize (Prop.replace_pi pi1 prop)
let remove prop atom =
match atom with
| Sil.Apred (_, exps) | Anpred (_, exps) ->
let nexps = IList.map (fun e -> Prop.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
| _ ->
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
let pi0 = Prop.get_pi prop in
let pi1 = IList.map_changed atom_map pi0 in
if pi1 == pi0 then
prop
else
Prop.normalize (Prop.replace_pi pi1 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 = 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
Prop.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
(** type for arithmetic problems *)
type arith_problem =
(* division by zero *)
| Div0 of Exp.t
(* unary minus of unsigned type applied to the given expression *)
| UminusUnsigned of Exp.t * Typ.t
(** Look for an arithmetic problem in [exp] *)
let find_arithmetic_problem proc_node_session prop exp =
let exps_divided = ref [] in
let uminus_unsigned = ref [] in
let res = ref prop in
let check_zero e =
match Prop.exp_normalize_prop prop e with
| Exp.Const c when Const.iszero_int_float c -> true
| _ ->
res := add_or_replace !res (Apred (Adiv0 proc_node_session, [e]));
false in
let rec walk = function
| Exp.Var _ -> ()
| Exp.UnOp (Unop.Neg, e, Some (
(Typ.Tint
(Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) ->
uminus_unsigned := (e, typ) :: !uminus_unsigned
| Exp.UnOp(_, e, _) -> walk e
| Exp.BinOp(op, e1, e2) ->
if op = Binop.Div || op = Binop.Mod then exps_divided := e2 :: !exps_divided;
walk e1; walk e2
| Exp.Exn _ -> ()
| Exp.Closure _ -> ()
| Exp.Const _ -> ()
| Exp.Cast (_, e) -> walk e
| Exp.Lvar _ -> ()
| Exp.Lfield (e, _, _) -> walk e
| Exp.Lindex (e1, e2) -> walk e1; walk e2
| Exp.Sizeof (_, None, _) -> ()
| Exp.Sizeof (_, Some len, _) -> walk len in
walk exp;
try Some (Div0 (IList.find check_zero !exps_divided)), !res
with Not_found ->
(match !uminus_unsigned with
| (e, t):: _ -> Some (UminusUnsigned (e, t)), !res
| _ -> None, !res)
(** Deallocate the stack variables in [pvars], and replace them by normal variables.
Return the list of stack variables whose address was still present after deallocation. *)
let deallocate_stack_vars (p: 'a Prop.t) pvars =
let filter = function
| Sil.Hpointsto (Exp.Lvar v, _, _) ->
IList.exists (Pvar.equal v) pvars
| _ -> false in
let sigma_stack, sigma_other = IList.partition filter (Prop.get_sigma p) in
let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *)
let stack_vars_address_in_post = ref [] in (* stack vars whose address is still present *)
let exp_replace = IList.map (function
| Sil.Hpointsto (Exp.Lvar v, _, _) ->
let freshv = Ident.create_fresh Ident.kprimed in
fresh_address_vars := (v, freshv) :: !fresh_address_vars;
(Exp.Lvar v, Exp.Var freshv)
| _ -> assert false) sigma_stack in
let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list (Prop.get_sub p)) in
let pi = IList.map (Sil.atom_replace_exp exp_replace) ((Prop.get_pi p) @ pi1) in
let p' =
Prop.normalize
(Prop.replace_sub Sil.sub_empty
(Prop.replace_sigma (Prop.sigma_replace_exp exp_replace sigma_other) p)) in
let p'' =
let res = ref p' in
let p'_fav = Prop.prop_fav p' in
let do_var (v, freshv) =
if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
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 !res pred
end in
IList.iter do_var !fresh_address_vars;
!res in
!stack_vars_address_in_post, IList.fold_left Prop.prop_atom_and p'' pi
(** Input of this method is an exp in a prop. Output is a formal variable or path from a
formal variable that is equal to the expression,
or the OBJC_NULL attribute of the expression. *)
let find_equal_formal_path e prop =
let rec find_in_sigma e seen_hpreds =
IList.fold_right (
fun hpred res ->
if IList.mem Sil.hpred_equal hpred seen_hpreds then None
else
let seen_hpreds = hpred :: seen_hpreds in
match res with
| Some _ -> res
| None ->
match hpred with
| Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
when Exp.equal exp2 e &&
(Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
Some (Exp.Lvar pvar1)
| Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
IList.fold_right (fun (field, strexp) res ->
match res with
| Some _ -> res
| None ->
match strexp with
| Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
(match find_in_sigma exp1 seen_hpreds with
| Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
| None -> None)
| _ -> None) fields None
| _ -> None) (Prop.get_sigma prop) None in
match find_in_sigma e [] with
| Some vfs -> Some vfs
| None ->
match get_objc_null prop e with
| Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
| _ -> None

@ -0,0 +1,113 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
(** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *)
module L = Logging
module F = Format
(** Check whether an atom is used to mark an attribute *)
val is_pred : Sil.atom -> bool
(** Add an attribute associated to the argument expressions *)
val add : ?footprint: bool -> ?polarity: bool ->
Prop.normal Prop.t -> PredSymb.t -> Exp.t list -> Prop.normal Prop.t
(** Replace an attribute associated to the expression *)
val add_or_replace : Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
(** 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) -> Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
(** Get all the attributes of the prop *)
val get_all : 'a Prop.t -> Sil.atom list
(** Get the attributes associated to the expression, if any *)
val get_for_exp : 'a Prop.t -> Exp.t -> Sil.atom list
(** Retrieve all the atoms that contain a specific attribute *)
val get_for_symb : 'a Prop.t -> PredSymb.t -> Sil.atom list
(** Get the autorelease attribute associated to the expression, if any *)
val get_autorelease : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the div0 attribute associated to the expression, if any *)
val get_div0 : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the objc null attribute associated to the expression, if any *)
val get_objc_null : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the observer attribute associated to the expression, if any *)
val get_observer : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the resource attribute associated to the expression, if any *)
val get_resource : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the retval null attribute associated to the expression, if any *)
val get_retval : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the taint attribute associated to the expression, if any *)
val get_taint : 'a Prop.t -> Exp.t -> Sil.atom option
(** Get the undef attribute associated to the expression, if any *)
val get_undef : 'a Prop.t -> Exp.t -> Sil.atom option
(** Test for existence of an Adangling DAuninit attribute associated to the exp *)
val has_dangling_uninit : 'a Prop.t -> Exp.t -> bool
(** Remove an attribute *)
val remove : Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
(** Remove all attributes for the given attr *)
val remove_for_attr : Prop.normal Prop.t -> PredSymb.t -> Prop.normal Prop.t
(** Remove all attributes for the given resource and kind *)
val remove_resource :
PredSymb.res_act_kind -> PredSymb.resource -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Apply f to every resource attribute in the prop *)
val map_resource :
Prop.normal Prop.t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> Prop.normal Prop.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 : Prop.normal Prop.t -> Exp.t -> Exp.t -> Prop.normal Prop.t
(** 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 : Prop.normal Prop.t -> Exp.t -> Prop.normal Prop.t
(** mark Exp.Var's or Exp.Lvar's as undefined *)
val mark_vars_as_undefined :
Prop.normal Prop.t -> Exp.t list -> Procname.t -> Typ.item_annotation -> Location.t ->
PredSymb.path_pos -> Prop.normal Prop.t
(** type for arithmetic problems *)
type arith_problem =
(* division by zero *)
| Div0 of Exp.t
(* unary minus of unsigned type applied to the given expression *)
| UminusUnsigned of Exp.t * Typ.t
(** Look for an arithmetic problem in [exp] *)
val find_arithmetic_problem :
PredSymb.path_pos -> Prop.normal Prop.t -> Exp.t -> arith_problem option * Prop.normal Prop.t
(** Deallocate the stack variables in [pvars], and replace them by normal variables.
Return the list of stack variables whose address was still present after deallocation. *)
val deallocate_stack_vars : Prop.normal Prop.t -> Pvar.t list -> Pvar.t list * Prop.normal Prop.t
val find_equal_formal_path : Exp.t -> 'a Prop.t -> Exp.t option

@ -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.Attribute.get_resource prop e with
let pvar_opt = match 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.Attribute.get_observer prop e with
match 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.Attribute.get_resource prop e with
match 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.Attribute.get_undef prop e with
(match Attribute.get_undef prop e with
| Some (Apred (Aundef _ as a, _)) ->
res := Some a
| _ -> ()) in

@ -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.Attribute.is_pred a then join_atom_check_attribute p_op a_op;
if Attribute.is_pred 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

@ -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.Attribute.get_resource prop e with
(match 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.Attribute.get_objc_null prop (Exp.Lvar pvar) with
(match 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.Attribute.has_dangling_uninit spec_pre exp then
if 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 ->

@ -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.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
Attribute.remove_resource Racquire (Rmemory Mobjc)
(Attribute.remove_resource Racquire (Rmemory Mmalloc)
(Attribute.remove_resource Racquire Rfile prop))
) pathset
else pathset
| _ -> pathset in

@ -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.Attribute.get_undef prop n_lexp) in
Option.is_some (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.Attribute.get_resource prop n_lexp with
let prop' = match Attribute.get_resource prop n_lexp with
| Some (Apred (Aresource ra, _)) ->
Prop.Attribute.add_or_replace prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
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.Attribute.add_or_replace prop (Apred (Aresource ra, [n_lexp])) in
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.Attribute.add_or_replace prop (Apred (Aautorelease, [n_lexp])) in
let 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.Attribute.get_for_symb prop_ Aautorelease in
let prop_without_attribute = Prop.Attribute.remove_for_attr prop_ Aautorelease in
let autoreleased_objects = Attribute.get_for_symb prop_ Aautorelease in
let prop_without_attribute = 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.Attribute.add_or_replace prop (Apred (attr, [n_lexp])), path)]
[(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.Attribute.remove prop (Apred (attr, [n_lexp])), path)]
[(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.Attribute.add_or_replace_check_changed
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.Attribute.add_or_replace prop' (Apred (Aresource ra, [exp_new])) in
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

@ -430,21 +430,6 @@ let sub_normalize sub =
let (--) = IntLit.sub
let (++) = IntLit.add
let iszero_int_float = function
| Const.Cint i -> IntLit.iszero i
| Const.Cfloat 0.0 -> true
| _ -> false
let isone_int_float = function
| Const.Cint i -> IntLit.isone i
| Const.Cfloat 1.0 -> true
| _ -> false
let isminusone_int_float = function
| Const.Cint i -> IntLit.isminusone i
| Const.Cfloat (-1.0) -> true
| _ -> false
let sym_eval abs e =
let rec eval e =
(* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *)
@ -622,9 +607,9 @@ let sym_eval abs e =
when isPlusA && (extensible_array_element_typ_equal elt typ) ->
let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
Exp.Sizeof (typ, Some len, st)
| Exp.Const c, _ when iszero_int_float c ->
| Exp.Const c, _ when Const.iszero_int_float c ->
e2'
| _, Exp.Const c when iszero_int_float c ->
| _, Exp.Const c when Const.iszero_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Exp.int (n ++ m)
@ -666,9 +651,9 @@ let sym_eval abs e =
if Exp.equal e1' e2' then Exp.zero
else begin
match e1', e2' with
| Exp.Const c, _ when iszero_int_float c ->
| Exp.Const c, _ when Const.iszero_int_float c ->
eval (Exp.UnOp(Unop.Neg, e2', None))
| _, Exp.Const c when iszero_int_float c ->
| _, Exp.Const c when Const.iszero_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Exp.int (n -- m)
@ -693,17 +678,17 @@ let sym_eval abs e =
let e2' = eval e2 in
begin
match e1', e2' with
| Exp.Const c, _ when iszero_int_float c ->
| Exp.Const c, _ when Const.iszero_int_float c ->
Exp.zero
| Exp.Const c, _ when isone_int_float c ->
| Exp.Const c, _ when Const.isone_int_float c ->
e2'
| Exp.Const c, _ when isminusone_int_float c ->
| Exp.Const c, _ when Const.isminusone_int_float c ->
eval (Exp.UnOp (Unop.Neg, e2', None))
| _, Exp.Const c when iszero_int_float c ->
| _, Exp.Const c when Const.iszero_int_float c ->
Exp.zero
| _, Exp.Const c when isone_int_float c ->
| _, Exp.Const c when Const.isone_int_float c ->
e1'
| _, Exp.Const c when isminusone_int_float c ->
| _, Exp.Const c when Const.isminusone_int_float c ->
eval (Exp.UnOp (Unop.Neg, e1', None))
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Exp.int (IntLit.mul n m)
@ -722,11 +707,11 @@ let sym_eval abs e =
let e2' = eval e2 in
begin
match e1', e2' with
| _, Exp.Const c when iszero_int_float c ->
| _, Exp.Const c when Const.iszero_int_float c ->
Exp.get_undefined false
| Exp.Const c, _ when iszero_int_float c ->
| Exp.Const c, _ when Const.iszero_int_float c ->
e1'
| _, Exp.Const c when isone_int_float c ->
| _, Exp.Const c when Const.isone_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Exp.int (IntLit.div n m)
@ -1773,275 +1758,6 @@ let prop_reset_inst inst_map prop =
let sigma_fp' = IList.map (Sil.hpred_instmap inst_map) (get_sigma_footprint prop) in
replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop)
(** {2 Attributes} *)
module Attribute = struct
(** Check whether an atom is used to mark an attribute *)
let is_pred atom =
match atom with
| Sil.Apred _ | Anpred _ -> true
| _ -> false
(** 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 = if is_pred a then res := a :: !res 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
let get_undef prop exp =
get prop exp ACundef
let get_resource prop exp =
get prop exp ACresource
let get_taint prop exp =
get prop exp ACtaint
let get_autorelease prop exp =
get prop exp ACautorelease
let get_objc_null prop exp =
get prop exp ACobjc_null
let get_div0 prop exp =
get prop exp ACdiv0
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 =
(* division by zero *)
| Div0 of Exp.t
(* unary minus of unsigned type applied to the given expression *)
| UminusUnsigned of Exp.t * Typ.t
(** Look for an arithmetic problem in [exp] *)
let find_arithmetic_problem proc_node_session prop exp =
let exps_divided = ref [] in
let uminus_unsigned = ref [] in
let res = ref prop in
let check_zero e =
match exp_normalize_prop prop e with
| Exp.Const c when iszero_int_float c -> true
| _ ->
res := Attribute.add_or_replace !res (Apred (Adiv0 proc_node_session, [e]));
false in
let rec walk = function
| Exp.Var _ -> ()
| Exp.UnOp (Unop.Neg, e, Some (
(Typ.Tint
(Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) ->
uminus_unsigned := (e, typ) :: !uminus_unsigned
| Exp.UnOp(_, e, _) -> walk e
| Exp.BinOp(op, e1, e2) ->
if op = Binop.Div || op = Binop.Mod then exps_divided := e2 :: !exps_divided;
walk e1; walk e2
| Exp.Exn _ -> ()
| Exp.Closure _ -> ()
| Exp.Const _ -> ()
| Exp.Cast (_, e) -> walk e
| Exp.Lvar _ -> ()
| Exp.Lfield (e, _, _) -> walk e
| Exp.Lindex (e1, e2) -> walk e1; walk e2
| Exp.Sizeof (_, None, _) -> ()
| Exp.Sizeof (_, Some len, _) -> walk len in
walk exp;
try Some (Div0 (IList.find check_zero !exps_divided)), !res
with Not_found ->
(match !uminus_unsigned with
| (e, t):: _ -> Some (UminusUnsigned (e, t)), !res
| _ -> None, !res)
(** Deallocate the stack variables in [pvars], and replace them by normal variables.
Return the list of stack variables whose address was still present after deallocation. *)
let deallocate_stack_vars p pvars =
let filter = function
| Sil.Hpointsto (Exp.Lvar v, _, _) ->
IList.exists (Pvar.equal v) pvars
| _ -> false in
let sigma_stack, sigma_other = IList.partition filter p.sigma in
let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *)
let stack_vars_address_in_post = ref [] in (* stack vars whose address is still present *)
let exp_replace = IList.map (function
| Sil.Hpointsto (Exp.Lvar v, _, _) ->
let freshv = Ident.create_fresh Ident.kprimed in
fresh_address_vars := (v, freshv) :: !fresh_address_vars;
(Exp.Lvar v, Exp.Var freshv)
| _ -> assert false) sigma_stack in
let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list p.sub) in
let pi = IList.map (Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in
let p' =
{ p with
sub = Sil.sub_empty;
pi = [];
sigma = sigma_replace_exp exp_replace sigma_other } in
let p'' =
let res = ref p' in
let p'_fav = prop_fav p' in
let do_var (v, freshv) =
if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
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 := Attribute.add_or_replace !res pred
end in
IList.iter do_var !fresh_address_vars;
!res in
!stack_vars_address_in_post, IList.fold_left prop_atom_and p'' pi
(** {1 Functions for transforming footprints into propositions.} *)
@ -2802,43 +2518,6 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
((id:: idl1@idl2, stml1@instrs2), Exp.Var id)
end
(** Input of this method is an exp in a prop. Output is a formal variable or path from a
formal variable that is equal to the expression,
or the OBJC_NULL attribute of the expression. *)
let find_equal_formal_path e prop =
let rec find_in_sigma e seen_hpreds =
IList.fold_right (
fun hpred res ->
if IList.mem Sil.hpred_equal hpred seen_hpreds then None
else
let seen_hpreds = hpred :: seen_hpreds in
match res with
| Some _ -> res
| None ->
match hpred with
| Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
when Exp.equal exp2 e &&
(Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
Some (Exp.Lvar pvar1)
| Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
IList.fold_right (fun (field, strexp) res ->
match res with
| Some _ -> res
| None ->
match strexp with
| Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
(match find_in_sigma exp1 seen_hpreds with
| Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
| None -> None)
| _ -> None) fields None
| _ -> None) (get_sigma prop) None in
match find_in_sigma e [] with
| Some vfs -> Some vfs
| None ->
match Attribute.get_objc_null prop e with
| Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
| _ -> None
(** translate an if-then-else expression *)
let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =
match sym_eval false e1 with

@ -160,18 +160,6 @@ val atom_const_lt_exp : Sil.atom -> (IntLit.t * Exp.t) option
(** Negate an atom *)
val atom_negate : Sil.atom -> Sil.atom
(** type for arithmetic problems *)
type arith_problem =
(* division by zero *)
| Div0 of Exp.t
(* unary minus of unsigned type applied to the given expression *)
| UminusUnsigned of Exp.t * Typ.t
(** Look for an arithmetic problem in [exp] *)
val find_arithmetic_problem :
PredSymb.path_pos -> normal t -> Exp.t -> arith_problem option * normal t
(** Normalize [exp] using the pure part of [prop]. Later, we should
change this such that the normalization exposes offsets of [exp]
as much as possible. *)
@ -280,85 +268,6 @@ 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
module Attribute : sig
(** Check whether an atom is used to mark an attribute *)
val is_pred : atom -> bool
(** Add an attribute associated to the argument expressions *)
val add : ?footprint: bool -> ?polarity: bool -> normal t -> PredSymb.t -> Exp.t list -> normal t
(** Replace an attribute associated to the expression *)
val add_or_replace : normal t -> atom -> normal t
(** 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 all the attributes of the prop *)
val get_all : 'a t -> atom list
(** Get the attributes associated to the expression, if any *)
val get_for_exp : 'a t -> Exp.t -> atom list
(** Retrieve all the atoms that contain a specific attribute *)
val get_for_symb : 'a t -> PredSymb.t -> Sil.atom list
(** Get the autorelease attribute associated to the expression, if any *)
val get_autorelease : '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 objc null attribute associated to the expression, if any *)
val get_objc_null : 'a t -> Exp.t -> atom option
(** Get the observer attribute associated to the expression, if any *)
val get_observer : 'a t -> Exp.t -> atom option
(** Get the resource attribute associated to the expression, if any *)
val get_resource : 'a t -> Exp.t -> atom option
(** Get the retval null attribute associated to the expression, if any *)
val get_retval : 'a t -> Exp.t -> atom option
(** Get the taint attribute associated to the expression, if any *)
val get_taint : 'a t -> Exp.t -> atom option
(** Get the undef attribute associated to the expression, if any *)
val get_undef : 'a t -> Exp.t -> atom option
(** Test for existence of an Adangling DAuninit attribute associated to the exp *)
val has_dangling_uninit : 'a t -> Exp.t -> bool
(** Remove an attribute *)
val remove : 'a t -> atom -> normal t
(** Remove all attributes for the given attr *)
val remove_for_attr : 'a t -> PredSymb.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
(** Apply f to every resource attribute in the prop *)
val map_resource : normal t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> 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
(** 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
@ -377,10 +286,6 @@ val get_pi_footprint : 'a t -> atom list
(** Return the sigma part of the footprint of [prop] *)
val get_sigma_footprint : 'a t -> hpred list
(** Deallocate the stack variables in [pvars], and replace them by normal variables.
Return the list of stack variables whose address was still present after deallocation. *)
val deallocate_stack_vars : normal t -> Pvar.t list -> Pvar.t list * normal t
(** Canonicalize the names of primed variables. *)
val prop_rename_primed_footprint_vars : normal t -> normal t
@ -506,8 +411,6 @@ val prop_iter_make_id_primed : Ident.t -> 'a prop_iter -> 'a prop_iter
(** Collect garbage fields. *)
val prop_iter_gc_fields : unit prop_iter -> unit prop_iter
val find_equal_formal_path : Exp.t -> 'a t -> Exp.t option
(** return the set of subexpressions of [strexp] *)
val strexp_get_exps : Sil.strexp -> Exp.Set.t

@ -746,7 +746,7 @@ let add_guarded_by_constraints prop lexp pdesc =
(function
| Sil.Apred (Alocked, _) -> true
| _ -> false)
(Prop.Attribute.get_for_exp prop guarded_by_exp) in
(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.Attribute.add ~footprint:true prop Alocked [guarded_by_exp]
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.Attribute.get_for_exp prop exp) in
IList.exists is_nullable_attr (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.Attribute.get_resource;
Prop.Attribute.get_undef;
Attribute.get_resource;
Attribute.get_undef;
] in
let get_relevant_attributes exp =
let rec fold_getters = function

@ -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.Attribute.get_undef p root_lexp in
else 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
@ -418,14 +418,14 @@ let check_constant_string_dereference lexp =
(** Normalize an expression and check for arithmetic problems *)
let check_arith_norm_exp pname exp prop =
match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
| Some (Prop.Div0 div), prop' ->
match Attribute.find_arithmetic_problem (State.get_path_pos ()) prop exp with
| Some (Attribute.Div0 div), prop' ->
let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
let exn = Exceptions.Divide_by_zero (desc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn;
Prop.exp_normalize_prop prop exp, prop'
| Some (Prop.UminusUnsigned (e, typ)), prop' ->
| Some (Attribute.UminusUnsigned (e, typ)), prop' ->
let desc =
Errdesc.explain_unary_minus_applied_to_unsigned_expression
e typ (State.get_node ()) (State.get_loc ()) 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.Attribute.get_all prop_after in
let exp_att_list = 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.Attribute.get_objc_null pre e) -> true
Option.is_some (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
match Attribute.find_equal_formal_path receiver prop with
| Some vfs ->
Prop.Attribute.add_or_replace prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
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.Attribute.get_undef pre receiver) in
let is_undef = Option.is_some (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.Attribute.add_or_replace prop (Apred (Ataint callee_pname, [ret_exp])) in
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.Attribute.add_or_replace prop (Apred (Ataint taint_info, [Exp.Var lhs_id]))
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.Attribute.add_or_replace prop' (Apred (Adangling DAuninit, [Exp.Var id]))
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.Attribute.get_for_exp prop exp) in
IList.fold_left fold_undef_pname None (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.Attribute.replace_objc_null prop n_lhs_exp n_rhs_exp in
let 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.Attribute.nullify_exp_with_objc_null prop_ cond in
let 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.Attribute.get_taint prop exp with
match 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.Attribute.add_or_replace prop (Apred (Auntaint taint_info, [exp]))
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.Attribute.add ~footprint:true prop (Auntaint taint_info) [exp]
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.Attribute.remove_for_attr q res
| Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Attribute.remove_for_attr q res
| _ -> q in
IList.fold_left do_attribute p (Prop.Attribute.get_for_exp p e) in
IList.fold_left do_attribute p (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,7 @@ 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.Attribute.mark_vars_as_undefined
Attribute.mark_vars_as_undefined
pre_final exps_to_mark callee_pname ret_annots loc path_pos in
[(prop_with_undef_attr, path)]
@ -1641,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
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

@ -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.Attribute.has_dangling_uninit spec_pre e then
if 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.Attribute.get_resource actual_pre e_sub with
else match 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.Attribute.get_undef actual_pre e_sub with
(match 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.Attribute.get_all post)
IList.iter check_attr (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.Attribute.get_resource actual_pre e with
let actual_pre_has_freed_attribute e = match Attribute.get_resource actual_pre e with
| Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true
| _ -> false in
let atom_update_alloc_attribute = function
@ -599,12 +599,12 @@ 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.Attribute.is_pred pi2 in
let pi2_attr, pi2_noattr = IList.partition Attribute.is_pred 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] *)
if Prop.Attribute.is_pred atom then
Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom
if Attribute.is_pred atom then
Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom
else
prop in
IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
@ -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.Attribute.get_taint calling_prop e with
match 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.Attribute.get_all prop) in
(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.Attribute.add_or_replace prop_normal
Attribute.add_or_replace prop_normal
(Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Exp.Var ret_id]))
|> Prop.expose in
(prop', path) 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.Attribute.is_pred a)
not (Attribute.is_pred 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.Attribute.add p att_retval [ret_var], path in
Attribute.add p att_retval [ret_var], path in
IList.map mark_id_as_retval res
| _ -> res

@ -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.Attribute.add_or_replace prop_acc (Apred (att, [rhs]))
Attribute.add_or_replace prop_acc (Apred (att, [rhs]))
| _ -> prop_acc)
prop (Prop.get_sigma prop)

Loading…
Cancel
Save