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

Move attributes from const to exp

Browse Source 
Summary:
Move attribute values from const to exp.  They are not constants, and
this reduces interdependence between Sil types.

Reviewed By: cristianoc

Differential Revision: D3548055

fbshipit-source-id: 31a9121
master
Josh Berdine 9 years ago committed by Facebook Github Bot 7
parent a379729e1f
commit a1b680c473
14 changed files with 65 additions and 46 deletions
Show Stats Download Patch File Download Diff File

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

@ -469,7 +469,6 @@ and const =
| Cfun of Procname.t /** function names */
| Cstr of string /** string constants */
| Cfloat of float /** float constants */
| Cattribute of attribute /** attribute used in disequalities to annotate a value */
| Cclass of Ident.name /** class constant */
| Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
and type of the surrounding Csu.t type */
@ -502,7 +501,9 @@ and exp =
The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof of Typ.t dynamic_length Subtype.t;
| Sizeof of Typ.t dynamic_length Subtype.t
/** attribute used in disequalities to annotate a value */
| Attribute of attribute;
/** Kind of prune instruction */
@ -981,7 +982,6 @@ let const_kind_equal c1 c2 => {
| Cfun _ => 2
| Cstr _ => 3
| Cfloat _ => 4
| Cattribute _ => 5
| Cclass _ => 7
| Cptr_to_fld _ => 8;
const_kind_number c1 == const_kind_number c2
@ -1078,9 +1078,6 @@ and const_compare (c1: const) (c2: const) :int =>
| (Cfloat f1, Cfloat f2) => float_compare f1 f2
| (Cfloat _, _) => (-1)
| (_, Cfloat _) => 1
| (Cattribute att1, Cattribute att2) => attribute_compare att1 att2
| (Cattribute _, _) => (-1)
| (_, Cattribute _) => 1
| (Cclass c1, Cclass c2) => Ident.name_compare c1 c2
| (Cclass _, _) => (-1)
| (_, Cclass _) => 1
@ -1204,6 +1201,9 @@ and exp_compare (e1: exp) (e2: exp) :int =>
Subtype.compare s1 s2
}
}
| (Attribute att1, Attribute att2) => attribute_compare att1 att2
| (Attribute _, _) => (-1)
| (_, Attribute _) => 1
};
let const_equal c1 c2 => const_compare c1 c2 == 0;
@ -1761,7 +1761,6 @@ and pp_const pe f =>
}
| Cstr s => F.fprintf f "\"%s\"" (String.escaped s)
| Cfloat v => F.fprintf f "%f" v
| Cattribute att => F.fprintf f "%s" (attribute_to_string pe att)
| Cclass c => F.fprintf f "%a" Ident.pp_name c
| Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn
/** Pretty print an expression. */
@ -1808,6 +1807,7 @@ and _pp_exp pe0 pp_t f e0 => {
| Sizeof t l s =>
let pp_len f l => Option.map_default (F.fprintf f "[%a]" pp_exp) () l;
F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s
| Attribute att => F.fprintf f "%s" (attribute_to_string pe att)
}
};
color_post_wrapper changed pe0 f
@ -1995,8 +1995,8 @@ let pp_atom pe0 f a => {
| PP_HTML => F.fprintf f "%a = %a" (pp_exp pe) e1 (pp_exp pe) e2
| PP_LATEX => F.fprintf f "%a{=}%a" (pp_exp pe) e1 (pp_exp pe) e2
}
| Aneq (Const (Cattribute _) as ea) e
| Aneq e (Const (Cattribute _) as ea) => F.fprintf f "%a(%a)" (pp_exp pe) ea (pp_exp pe) e
| Aneq (Attribute _ as ea) e
| Aneq e (Attribute _ as ea) => F.fprintf f "%a(%a)" (pp_exp pe) ea (pp_exp pe) e
| Aneq e1 e2 =>
switch pe.pe_kind {
| PP_TEXT
@ -2690,6 +2690,7 @@ let rec root_of_lexp lexp =>
| Lfield e _ _ => root_of_lexp e
| Lindex e _ => root_of_lexp e
| Sizeof _ => lexp
| Attribute _ => lexp
};
@ -2779,6 +2780,7 @@ let rec exp_fpv =
/* | Sizeof _ None _ => [] */
/* | Sizeof _ (Some l) _ => exp_fpv l */
| Sizeof _ _ _ => []
| Attribute _ => []
and exp_list_fpv el => IList.flatten (IList.map exp_fpv el);
let atom_fpv =
@ -2959,7 +2961,7 @@ let rec exp_fav_add fav =>
| Var id => fav ++ id
| Exn e => exp_fav_add fav e
| Closure {captured_vars} => IList.iter (fun (e, _, _) => exp_fav_add fav e) captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => ()
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => ()
| Cast _ e
| UnOp _ e _ => exp_fav_add fav e
| BinOp _ e1 e2 => {
@ -2975,7 +2977,8 @@ let rec exp_fav_add fav =>
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => () */
/* | Sizeof _ (Some l) _ => exp_fav_add fav l; */
| Sizeof _ _ _ => ();
| Sizeof _ _ _ => ()
| Attribute _ => ();
let exp_fav = fav_imperative_to_functional exp_fav_add;
@ -3382,7 +3385,7 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
} else {
Closure {...c, captured_vars}
}
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => exp
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => exp
| Cast t e =>
let e' = exp_sub_ids f e;
if (e' === e) {
@ -3431,6 +3434,7 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
}
| None => exp
}
| Attribute _ => exp
};
let rec apply_sub subst id =>
@ -4047,11 +4051,12 @@ let exp_get_vars exp => {
(fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
vars
captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => vars */
/* | Sizeof _ (Some l) _ => exp_get_vars_ l vars */
| Sizeof _ _ _ => vars
| Attribute _ => vars
};
exp_get_vars_ exp ([], [])
};
@ -4068,6 +4073,7 @@ let exp_get_offsets exp => {
| Exn _
| Closure _
| Lvar _
| Attribute _
| Sizeof _ None _ => offlist_past
| Sizeof _ (Some l) _ => f offlist_past l
| Cast _ sub_exp => f offlist_past sub_exp

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

@ -196,7 +196,6 @@ and const =
| Cfun of Procname.t /** function names */
| Cstr of string /** string constants */
| Cfloat of float /** float constants */
| Cattribute of attribute /** attribute used in disequalities to annotate a value */
| Cclass of Ident.name /** class constant */
| Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
and type of the surrounding Csu.t type */
@ -229,7 +228,9 @@ and exp =
The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof of Typ.t dynamic_length Subtype.t;
| Sizeof of Typ.t dynamic_length Subtype.t
/** attribute used in disequalities to annotate a value */
| Attribute of attribute;
/** Sets of expressions. */

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

@ -1093,7 +1093,7 @@ let check_junk ?original_prop pname tenv prop =
check_observer_is_unsubscribed_deallocation prop e;
match Prop.get_resource_attribute prop e with
| Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire }) as a) ->
L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Const (Sil.Cattribute a)); L.d_ln ();
L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Attribute a); L.d_ln ();
res := Some a
| _ ->
(match Prop.get_undef_attribute prop e with

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

@ -828,6 +828,8 @@ let rec exp_construct_fresh side e =
e
| Sil.Sizeof (typ, Some len, st) ->
Sil.Sizeof (typ, Some (exp_construct_fresh side len), st)
| Sil.Attribute _ ->
e
let strexp_construct_fresh side =
let f (e, inst_opt) = (exp_construct_fresh side e, inst_opt) in

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

@ -82,6 +82,8 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
(match exp_match base1 sub vars base2 with
| None -> None
| Some (sub', vars') -> exp_match idx1 sub' vars' idx2)
| Sil.Attribute _, _ | _, Sil.Attribute _ ->
check_equal sub vars e1 e2
let exp_list_match es1 sub vars es2 =
let f res_acc (e1, e2) = match res_acc with

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

@ -763,7 +763,8 @@ let execute_alloc mk can_return_null
evaluate_char_sizeof len
| Sil.Sizeof (Typ.Tarray (Typ.Tint ik, Some len), None, _) when Typ.ikind_is_char ik ->
evaluate_char_sizeof (Sil.Const (Sil.Cint len))
| Sil.Sizeof _ -> e in
| Sil.Sizeof _ -> e
| Sil.Attribute _ -> e in
let size_exp, procname = match args with
| [(Sil.Sizeof
(Typ.Tstruct

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

@ -827,7 +827,9 @@ let sym_eval abs e =
| Sil.Lindex (e1, e2) ->
let e1' = eval e1 in
let e2' = eval e2 in
Sil.Lindex(e1', e2') in
Sil.Lindex(e1', e2')
| Sil.Attribute _ ->
e in
let e' = eval e in
(* L.d_str "sym_eval "; Sil.d_exp e; L.d_str" --> "; Sil.d_exp e'; L.d_ln (); *)
e'
@ -1764,8 +1766,8 @@ let prop_reset_inst inst_map prop =
(** Return the exp and attribute marked in the atom if any, and return None otherwise *)
let atom_get_exp_attribute = function
| Sil.Aneq (Sil.Const (Sil.Cattribute att), e)
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att)) -> Some (e, att)
| Sil.Aneq (Sil.Attribute att, e)
| Sil.Aneq (e, Sil.Attribute att) -> Some (e, att)
| _ -> None
(** Check whether an atom is used to mark an attribute *)
@ -1777,8 +1779,8 @@ let get_exp_attributes prop exp =
let nexp = exp_normalize_prop prop exp in
let atom_get_attr attributes atom =
match atom with
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att))
| Sil.Aneq (Sil.Const (Sil.Cattribute att), e) when Sil.exp_equal e nexp -> att:: attributes
| Sil.Aneq (e, Sil.Attribute att)
| Sil.Aneq (Sil.Attribute att, e) when Sil.exp_equal e nexp -> att:: attributes
| _ -> attributes in
IList.fold_left atom_get_attr [] prop.pi
@ -1835,7 +1837,7 @@ let get_all_attributes prop =
(** Set an attribute associated to the expression *)
let set_exp_attribute prop exp att =
let exp_att = Sil.Const (Sil.Cattribute att) in
let exp_att = Sil.Attribute att in
conjoin_neq exp exp_att prop
(** Replace an attribute associated to the expression *)
@ -1843,13 +1845,13 @@ let add_or_replace_exp_attribute_check_changed check_attribute_change prop exp a
let nexp = exp_normalize_prop prop exp in
let found = ref false in
let atom_map a = match a with
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att_old))
| Sil.Aneq (Sil.Const (Sil.Cattribute att_old), e) ->
| Sil.Aneq (e, Sil.Attribute att_old)
| Sil.Aneq (Sil.Attribute att_old, e) ->
if Sil.exp_equal nexp e && (attributes_in_same_category att_old att) then
begin
found := true;
check_attribute_change att_old att;
let e1, e2 = exp_reorder e (Sil.Const (Sil.Cattribute att)) in
let e1, e2 = exp_reorder e (Sil.Attribute att) in
Sil.Aneq (e1, e2)
end
else a
@ -1875,8 +1877,8 @@ let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_po
(** Remove an attribute from all the atoms in the heap *)
let remove_attribute att prop =
let atom_remove atom pi = match atom with
| Sil.Aneq (_, Sil.Const (Sil.Cattribute att_old))
| Sil.Aneq (Sil.Const (Sil.Cattribute att_old), _) ->
| Sil.Aneq (_, Sil.Attribute att_old)
| Sil.Aneq (Sil.Attribute att_old, _) ->
if Sil.attribute_equal att_old att then
pi
else atom:: pi
@ -1887,8 +1889,8 @@ let remove_attribute att prop =
let remove_attribute_from_exp att prop exp =
let nexp = exp_normalize_prop prop exp in
let atom_remove atom pi = match atom with
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att_old))
| Sil.Aneq (Sil.Const (Sil.Cattribute att_old), e) ->
| Sil.Aneq (e, Sil.Attribute att_old)
| Sil.Aneq (Sil.Attribute att_old, e) ->
if Sil.attribute_equal att_old att && Sil.exp_equal nexp e then
pi
else atom:: pi
@ -1923,8 +1925,8 @@ let rec nullify_exp_with_objc_null prop exp =
(** Get all the attributes of the prop *)
let get_atoms_with_attribute att prop =
let atom_remove atom autoreleased_atoms = match atom with
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att_old))
| Sil.Aneq (Sil.Const (Sil.Cattribute att_old), e) ->
| Sil.Aneq (e, Sil.Attribute att_old)
| Sil.Aneq (Sil.Attribute att_old, e) ->
if Sil.attribute_equal att_old att then
e:: autoreleased_atoms
else autoreleased_atoms
@ -1939,10 +1941,10 @@ let attribute_map_resource prop f =
Sil.Aresource (f e ra)
| att -> att in
let atom_map a = match a with
| Sil.Aneq (e, Sil.Const (Sil.Cattribute att))
| Sil.Aneq (Sil.Const (Sil.Cattribute att), e) ->
| Sil.Aneq (e, Sil.Attribute att)
| Sil.Aneq (Sil.Attribute att, e) ->
let att' = attribute_map e att in
let e1, e2 = exp_reorder e (Sil.Const (Sil.Cattribute att')) in
let e1, e2 = exp_reorder e (Sil.Attribute att') in
Sil.Aneq (e1, e2)
| _ -> a in
let pi' = IList.map atom_map pi in
@ -1985,7 +1987,8 @@ let find_arithmetic_problem proc_node_session prop exp =
| Sil.Lfield (e, _, _) -> walk e
| Sil.Lindex (e1, e2) -> walk e1; walk e2
| Sil.Sizeof (_, None, _) -> ()
| Sil.Sizeof (_, Some len, _) -> walk len in
| Sil.Sizeof (_, Some len, _) -> walk len
| Sil.Attribute _ -> () in
walk exp;
try Some (Div0 (IList.find check_zero !exps_divided)), !res
with Not_found ->
@ -2280,6 +2283,7 @@ let rec exp_captured_ren ren = function
let e1' = exp_captured_ren ren e1 in
let e2' = exp_captured_ren ren e2 in
Sil.Lindex(e1', e2')
| Sil.Attribute _ as e -> e
let atom_captured_ren ren = function
| Sil.Aeq (e1, e2) ->

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

@ -28,7 +28,7 @@ let from_prop p = p
(** Return [true] if root node *)
let rec is_root = function
| Sil.Var id -> Ident.is_normal id
| Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Lvar _ -> true
| Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Lvar _ | Sil.Attribute _ -> true
| Sil.Cast (_, e) -> is_root e
| Sil.UnOp _ | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ | Sil.Sizeof _ -> false

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

@ -552,7 +552,7 @@ let check_zero e =
let is_root prop base_exp exp =
let rec f offlist_past e = match e with
| Sil.Var _ | Sil.Const _ | Sil.UnOp _ | Sil.BinOp _ | Sil.Exn _ | Sil.Closure _ | Sil.Lvar _
| Sil.Sizeof _ ->
| Sil.Sizeof _ | Sil.Attribute _ ->
if check_equal prop base_exp e
then Some offlist_past
else None

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

@ -764,7 +764,7 @@ let add_guarded_by_constraints prop lexp pdesc =
end
else
(* private method. add locked proof obligation to [pdesc] *)
let locked_attr = Sil.Const (Cattribute Alocked) in
let locked_attr = Sil.Attribute Alocked in
Prop.conjoin_neq ~footprint:true guarded_by_exp locked_attr prop
| _ ->
if not (proc_has_matching_annot pdesc guarded_by_str

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

@ -354,6 +354,8 @@ let rec prune ~positive condition prop =
assert false
| Sil.Closure _ ->
assert false
| Sil.Attribute _ ->
assert false
and prune_inter ~positive condition1 condition2 prop =
let res = ref Propset.empty in
@ -1401,7 +1403,7 @@ and check_untainted exp taint_kind caller_pname callee_pname prop =
| _ ->
if !Config.footprint then
let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
let untaint_attr = Sil.Const (Sil.Cattribute (Sil.Auntaint taint_info)) in
let untaint_attr = Sil.Attribute (Sil.Auntaint taint_info) in
(* add untained(n_lexp) to the footprint *)
Prop.conjoin_neq ~footprint:true exp untaint_attr prop
else prop

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

@ -385,13 +385,13 @@ let post_process_post
| Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease })) -> true
| _ -> false in
let atom_update_alloc_attribute = function
| Sil.Aneq (e , Sil.Const (Sil.Cattribute (Sil.Aresource ra)))
| Sil.Aneq (Sil.Const (Sil.Cattribute (Sil.Aresource ra)), e)
| Sil.Aneq (e , Sil.Attribute (Sil.Aresource ra))
| Sil.Aneq (Sil.Attribute (Sil.Aresource ra), e)
when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) ->
(* unless it was already freed before the call *)
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 c = Sil.Const (Sil.Cattribute (Sil.Aresource ra')) in
let c = Sil.Attribute (Sil.Aresource ra') in
Sil.Aneq (e, c)
| a -> a in
let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in

4
infer/src/checkers/addressTaken.ml
Unescape View File

@ -32,8 +32,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|> add_address_taken_pvars e2
| Sil.Exn _
| Sil.Closure _
| Sil.Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _)
| Var _ | Sizeof _ ->
| Sil.Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _)
| Sil.Var _ | Sil.Sizeof _ | Sil.Attribute _ ->
astate
let exec_instr astate _ _ = function

3
infer/src/checkers/checkers.ml
Unescape View File

@ -518,7 +518,8 @@ let callback_check_field_access { Callbacks.proc_desc } =
| Sil.Lindex (e1, e2) ->
do_exp is_read e1;
do_exp is_read e2
| Sil.Sizeof _ -> () in
| Sil.Sizeof _ -> ()
| Sil.Attribute _ -> () in
let do_read_exp = do_exp true in
let do_write_exp = do_exp false in
let do_instr _ = function

Write Preview
Loading…
Cancel
Save