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

Extend Sizeof with final extensible array length

Browse Source 
Summary:
This diff extends Sizeof expressions with an optional expression for the
length of the final extensible array, if any.  For example, sizeof a
simple array `sizeof(t[n])` is represented by (modulo subtyping info)
`Sizeof t (Some n)`, and sizeof a struct whose final member is an array
`sizeof(struct s {... t[n] f})` is represented by `Sizeof (struct s
{... t[n] f}) (Some n)`.

This is an intermediate step toward eliminating expressions from types,
the redundancy between the length in the types and in the sizeof
expressions will be eliminated later.

Reviewed By: cristianoc

Differential Revision: D3358763

fbshipit-source-id: 2239bca
master
Josh Berdine 9 years ago committed by Facebook Github Bot 6
parent 5ed970efa9
commit a85a88d145
27 changed files with 306 additions and 200 deletions
Show Stats Download Patch File Download Diff File

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

@ -657,7 +657,7 @@ type dexp =
| Darray of dexp dexp | Darray of dexp dexp
| Dbinop of binop dexp dexp | Dbinop of binop dexp dexp
| Dconst of const | Dconst of const
| Dsizeof of typ Subtype.t | Dsizeof of typ (option exp) Subtype.t
| Dderef of dexp | Dderef of dexp
| Dfcall of dexp (list dexp) Location.t call_flags | Dfcall of dexp (list dexp) Location.t call_flags
| Darrow of dexp Ident.fieldname | Darrow of dexp Ident.fieldname
@ -769,8 +769,10 @@ and exp =
| Lfield of exp Ident.fieldname typ | Lfield of exp Ident.fieldname typ
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex of exp exp | Lindex of exp exp
/** A sizeof expression */ /** A sizeof expression. [Sizeof typ (Some len)] represents the size of a value of type [typ]
| Sizeof of typ Subtype.t; which ends in an extensible array of length [len]. The lengths in [Tarray] record the
statically determined lengths, while the lengths in [Sizeof] record the dynamic lengths. */
| Sizeof of typ (option exp) Subtype.t;
/** Kind of prune instruction */ /** Kind of prune instruction */
@ -937,7 +939,7 @@ let is_objc_ref_counter_field (fld, _, a) =>
let has_objc_ref_counter hpred => let has_objc_ref_counter hpred =>
switch hpred { switch hpred {
| Hpointsto _ _ (Sizeof (Tstruct struct_typ) _) => | Hpointsto _ _ (Sizeof (Tstruct struct_typ) _ _) =>
IList.exists is_objc_ref_counter_field struct_typ.instance_fields IList.exists is_objc_ref_counter_field struct_typ.instance_fields
| _ => false | _ => false
}; };
@ -1642,12 +1644,17 @@ and exp_compare (e1: exp) (e2: exp) :int =>
} }
| (Lindex _, _) => (-1) | (Lindex _, _) => (-1)
| (_, Lindex _) => 1 | (_, Lindex _) => 1
| (Sizeof t1 s1, Sizeof t2 s2) => | (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
let n = typ_compare t1 t2; let n = typ_compare t1 t2;
if (n != 0) { if (n != 0) {
n n
} else { } else {
Subtype.compare s1 s2 let n = opt_compare exp_compare l1 l2;
if (n != 0) {
n
} else {
Subtype.compare s1 s2
}
} }
}; };
@ -2190,7 +2197,7 @@ let rec dexp_to_string =
ampersand ^ s ampersand ^ s
} }
| Dunop op de => str_unop op ^ dexp_to_string de | Dunop op de => str_unop op ^ dexp_to_string de
| Dsizeof typ _ => pp_to_string (pp_typ_full pe_text) typ | Dsizeof typ _ _ => pp_to_string (pp_typ_full pe_text) typ
| Dunknown => "unknown" | Dunknown => "unknown"
| Dretcall de _ _ _ => "returned by " ^ dexp_to_string de | Dretcall de _ _ _ => "returned by " ^ dexp_to_string de
/** Pretty print a dexp. */ /** Pretty print a dexp. */
@ -2397,7 +2404,9 @@ and _pp_exp pe0 pp_t f e0 => {
| Lvar pv => Pvar.pp pe f pv | Lvar pv => Pvar.pp pe f pv
| Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld
| Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2 | Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2
| Sizeof t s => F.fprintf f "sizeof(%a%a)" pp_t t Subtype.pp s | 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
} }
}; };
color_post_wrapper changed pe0 f color_post_wrapper changed pe0 f
@ -2434,14 +2443,20 @@ let d_exp_list (el: list exp) => L.add_print_action (L.PTexp_list, Obj.repr el);
let pp_texp pe f => let pp_texp pe f =>
fun fun
| Sizeof t s => F.fprintf f "%a%a" (pp_typ pe) t Subtype.pp s | Sizeof t l s => {
let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l;
F.fprintf f "%a%a%a" (pp_typ pe) t pp_len l Subtype.pp s
}
| e => (pp_exp pe) f e; | e => (pp_exp pe) f e;
/** Pretty print a type with all the details. */ /** Pretty print a type with all the details. */
let pp_texp_full pe f => let pp_texp_full pe f =>
fun fun
| Sizeof t s => F.fprintf f "%a%a" (pp_typ_full pe) t Subtype.pp s | Sizeof t l s => {
let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l;
F.fprintf f "%a%a%a" (pp_typ_full pe) t pp_len l Subtype.pp s
}
| e => (_pp_exp pe) (pp_typ_full pe) f e; | e => (_pp_exp pe) (pp_typ_full pe) f e;
@ -3290,7 +3305,7 @@ let unsome_typ s =>
If not a sizeof, return the default type if given, otherwise raise an exception */ If not a sizeof, return the default type if given, otherwise raise an exception */
let texp_to_typ default_opt => let texp_to_typ default_opt =>
fun fun
| Sizeof t _ => t | Sizeof t _ _ => t
| _ => unsome_typ "texp_to_typ" default_opt; | _ => unsome_typ "texp_to_typ" default_opt;
@ -3416,7 +3431,10 @@ let rec exp_fpv =
| Lvar name => [name] | Lvar name => [name]
| Lfield e _ _ => exp_fpv e | Lfield e _ _ => exp_fpv e
| Lindex e1 e2 => exp_fpv e1 @ exp_fpv e2 | Lindex e1 e2 => exp_fpv e1 @ exp_fpv e2
| Sizeof _ => [] /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => [] */
/* | Sizeof _ (Some l) _ => exp_fpv l */
| Sizeof _ _ _ => []
and exp_list_fpv el => IList.flatten (IList.map exp_fpv el); and exp_list_fpv el => IList.flatten (IList.map exp_fpv el);
let atom_fpv = let atom_fpv =
@ -3611,7 +3629,10 @@ let rec exp_fav_add fav =>
exp_fav_add fav e1; exp_fav_add fav e1;
exp_fav_add fav e2 exp_fav_add fav e2
} }
| Sizeof _ => (); /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => () */
/* | Sizeof _ (Some l) _ => exp_fav_add fav l; */
| Sizeof _ _ _ => ();
let exp_fav = fav_imperative_to_functional exp_fav_add; let exp_fav = fav_imperative_to_functional exp_fav_add;
@ -4051,7 +4072,7 @@ and exp_sub (subst: subst) e =>
let e1' = exp_sub subst e1; let e1' = exp_sub subst e1;
let e2' = exp_sub subst e2; let e2' = exp_sub subst e2;
Lindex e1' e2' Lindex e1' e2'
| Sizeof t s => Sizeof (typ_sub subst t) s | Sizeof t l s => Sizeof (typ_sub subst t) (Option.map (exp_sub subst) l) s
}; };
let instr_sub (subst: subst) instr => { let instr_sub (subst: subst) instr => {
@ -4599,8 +4620,11 @@ let exp_get_vars exp => {
(fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc) (fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
vars vars
captured_vars captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => vars
| Sizeof _ => 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
}; };
exp_get_vars_ exp ([], []) exp_get_vars_ exp ([], [])
}; };
@ -4615,7 +4639,8 @@ let exp_get_offsets exp => {
| UnOp _ | UnOp _
| BinOp _ | BinOp _
| Lvar _ | Lvar _
| Sizeof _ => offlist_past | Sizeof _ None _ => offlist_past
| Sizeof _ (Some l) _ => f offlist_past l
| Cast _ sub_exp => f offlist_past sub_exp | Cast _ sub_exp => f offlist_past sub_exp
| Lfield sub_exp fldname typ => f [Off_fld fldname typ, ...offlist_past] sub_exp | Lfield sub_exp fldname typ => f [Off_fld fldname typ, ...offlist_past] sub_exp
| Lindex sub_exp e => f [Off_index e, ...offlist_past] sub_exp | Lindex sub_exp e => f [Off_index e, ...offlist_past] sub_exp

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

@ -230,7 +230,7 @@ type dexp =
| Darray of dexp dexp | Darray of dexp dexp
| Dbinop of binop dexp dexp | Dbinop of binop dexp dexp
| Dconst of const | Dconst of const
| Dsizeof of typ Subtype.t | Dsizeof of typ (option exp) Subtype.t
| Dderef of dexp | Dderef of dexp
| Dfcall of dexp (list dexp) Location.t call_flags | Dfcall of dexp (list dexp) Location.t call_flags
| Darrow of dexp Ident.fieldname | Darrow of dexp Ident.fieldname
@ -343,7 +343,7 @@ and exp =
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex of exp exp | Lindex of exp exp
/** A sizeof expression */ /** A sizeof expression */
| Sizeof of typ Subtype.t; | Sizeof of typ (option exp) Subtype.t;
let struct_typ_equal: struct_typ => struct_typ => bool; let struct_typ_equal: struct_typ => struct_typ => bool;
@ -539,7 +539,7 @@ type strexp =
and hpred = and hpred =
| Hpointsto of exp strexp exp | Hpointsto of exp strexp exp
/** represents [exp|->strexp:typexp] where [typexp] /** represents [exp|->strexp:typexp] where [typexp]
is an expression representing a type, e.h. [sizeof(t)]. */ is an expression representing a type, e.g. [sizeof(t)]. */
| Hlseg of lseg_kind hpara exp exp (list exp) | Hlseg of lseg_kind hpara exp exp (list exp)
/** higher - order predicate for singly - linked lists. /** higher - order predicate for singly - linked lists.
Should ensure that exp1!= exp2 implies that exp1 is allocated. Should ensure that exp1!= exp2 implies that exp1 is allocated.

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

@ -420,7 +420,7 @@ let typ_get_recursive_flds tenv typ_exp =
false false
in in
match typ_exp with match typ_exp with
| Sil.Sizeof (typ, _) -> | Sil.Sizeof (typ, _, _) ->
(match Tenv.expand_type tenv typ with (match Tenv.expand_type tenv typ with
| Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ -> [] | Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ -> []
| Sil.Tstruct { Sil.instance_fields } -> | Sil.Tstruct { Sil.instance_fields } ->
@ -903,14 +903,14 @@ let get_cycle root prop =
let visited' = (fst et_src):: visited in let visited' = (fst et_src):: visited in
let res = (match get_points_to e with let res = (match get_points_to e with
| None -> path, false | None -> path, false
| Some (Sil.Hpointsto(_, Sil.Estruct(fl, _), Sil.Sizeof(te, _))) -> | Some (Sil.Hpointsto(_, Sil.Estruct(fl, _), Sil.Sizeof(te, _, _))) ->
dfs e_root (e, te) ((et_src, f, e):: path) fl visited' dfs e_root (e, te) ((et_src, f, e):: path) fl visited'
| _ -> path, false (* check for lists *)) in | _ -> path, false (* check for lists *)) in
if snd res then res if snd res then res
else dfs e_root et_src path el' visited') in else dfs e_root et_src path el' visited') in
L.d_strln "Looking for cycle with root expression: "; Sil.d_hpred root; L.d_strln ""; L.d_strln "Looking for cycle with root expression: "; Sil.d_hpred root; L.d_strln "";
match root with match root with
| Sil.Hpointsto(e_root, Sil.Estruct(fl, _), Sil.Sizeof(te, _)) -> | Sil.Hpointsto(e_root, Sil.Estruct(fl, _), Sil.Sizeof(te, _, _)) ->
let se_root = Sil.Eexp(e_root, Sil.Inone) in let se_root = Sil.Eexp(e_root, Sil.Inone) in
(* start dfs with empty path and expr pointing to root *) (* start dfs with empty path and expr pointing to root *)
let (pot_cycle, res) = dfs se_root (se_root, te) [] fl [] in let (pot_cycle, res) = dfs se_root (se_root, te) [] fl [] in
@ -929,7 +929,7 @@ let get_cycle root prop =
let should_raise_objc_leak hpred = let should_raise_objc_leak hpred =
match hpred with match hpred with
| Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _), | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _),
Sil.Sizeof (typ, _)) Sil.Sizeof (typ, _, _))
when Ident.fieldname_is_hidden fn && Sil.Int.gt i Sil.Int.zero (* counter > 0 *) -> when Ident.fieldname_is_hidden fn && Sil.Int.gt i Sil.Int.zero (* counter > 0 *) ->
Mleak_buckets.should_raise_objc_leak typ Mleak_buckets.should_raise_objc_leak typ
| _ -> None | _ -> None
@ -949,7 +949,7 @@ let get_var_retain_cycle _prop =
| _ -> false in | _ -> false in
let is_hpred_block v h = let is_hpred_block v h =
match h, v with match h, v with
| Sil.Hpointsto (e, _, Sil.Sizeof(typ, _)), Sil.Eexp (e', _) | Sil.Hpointsto (e, _, Sil.Sizeof(typ, _, _)), Sil.Eexp (e', _)
when Sil.exp_equal e e' && Sil.is_block_type typ -> true when Sil.exp_equal e e' && Sil.is_block_type typ -> true
| _, _ -> false in | _, _ -> false in
let find v = let find v =
@ -967,7 +967,7 @@ let get_var_retain_cycle _prop =
| Some pvar -> [((sexp pvar, t), f, e')] | Some pvar -> [((sexp pvar, t), f, e')]
| _ -> (match find_block e with | _ -> (match find_block e with
| Some blk -> [((sexp blk, t), f, e')] | Some blk -> [((sexp blk, t), f, e')]
| _ -> [((sexp (Sil.Sizeof(t, Sil.Subtype.exact)), t), f, e')]) in | _ -> [((sexp (Sil.Sizeof (t, None, Sil.Subtype.exact)), t), f, e')]) in
(* returns the pvars of the first cycle we find in sigma. *) (* returns the pvars of the first cycle we find in sigma. *)
(* This is an heuristic that works if there is one cycle. *) (* This is an heuristic that works if there is one cycle. *)
(* In case there are more than one cycle we may return not necessarily*) (* In case there are more than one cycle we may return not necessarily*)

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

@ -332,7 +332,7 @@ let create_idmap sigma : idmap =
extend_idmap id { typ = t; alloc = true } idmap extend_idmap id { typ = t; alloc = true } idmap
| _ -> () in | _ -> () in
let do_hpred = function let do_hpred = function
| Sil.Hpointsto (e, se, Sil.Sizeof (typ, _)) -> | Sil.Hpointsto (e, se, Sil.Sizeof (typ, _, _)) ->
do_lhs_e e (Sil.Tptr (typ, Sil.Pk_pointer)); do_lhs_e e (Sil.Tptr (typ, Sil.Pk_pointer));
do_se se typ do_se se typ
| Sil.Hlseg (_, _, e, f, el) -> | Sil.Hlseg (_, _, e, f, el) ->
@ -427,7 +427,7 @@ let pp_texp_for_malloc fmt =
| Sil.Tarray (t, e) -> | Sil.Tarray (t, e) ->
Sil.Tarray (handle_arr_size t, e) in Sil.Tarray (handle_arr_size t, e) in
function function
| Sil.Sizeof (typ, _) -> | Sil.Sizeof (typ, _, _) ->
let typ' = handle_arr_size typ in let typ' = handle_arr_size typ in
F.fprintf fmt "sizeof(%a)" (pp_typ_c pe) typ' F.fprintf fmt "sizeof(%a)" (pp_typ_c pe) typ'
| e -> pp_exp_c pe fmt e | e -> pp_exp_c pe fmt e

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

@ -821,8 +821,10 @@ let rec exp_construct_fresh side e =
let e1' = exp_construct_fresh side e1 in let e1' = exp_construct_fresh side e1 in
let e2' = exp_construct_fresh side e2 in let e2' = exp_construct_fresh side e2 in
Sil.Lindex(e1', e2') Sil.Lindex(e1', e2')
| Sil.Sizeof _ -> | Sil.Sizeof (_, None, _) ->
e e
| Sil.Sizeof (typ, Some len, st) ->
Sil.Sizeof (typ, Some (exp_construct_fresh side len), st)
let strexp_construct_fresh side = let strexp_construct_fresh side =
let f (e, inst_opt) = (exp_construct_fresh side e, inst_opt) in let f (e, inst_opt) = (exp_construct_fresh side e, inst_opt) in
@ -948,12 +950,18 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp =
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
let e2'' = exp_partial_join e1' e2' in let e2'' = exp_partial_join e1' e2' in
Sil.Lindex(e1'', e2'') Sil.Lindex(e1'', e2'')
| Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
Sil.Sizeof (typ_partial_join t1 t2, Sil.Subtype.join st1 st2) Sil.Sizeof (typ_partial_join t1 t2, len_partial_join len1 len2, Sil.Subtype.join st1 st2)
| _ -> | _ ->
L.d_str "exp_partial_join no match "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); L.d_str "exp_partial_join no match "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln ();
raise IList.Fail raise IList.Fail
and len_partial_join len1 len2 =
match len1, len2 with
| None, _ -> len2
| _, None -> len1
| Some len1, Some len2 -> Some (size_partial_join len1 len2)
and size_partial_join size1 size2 = match size1, size2 with and size_partial_join size1 size2 = match size1, size2 with
| Sil.BinOp(Sil.PlusA, e1, Sil.Const c1), Sil.BinOp(Sil.PlusA, e2, Sil.Const c2) -> | Sil.BinOp(Sil.PlusA, e1, Sil.Const c1), Sil.BinOp(Sil.PlusA, e2, Sil.Const c2) ->
let e' = exp_partial_join e1 e2 in let e' = exp_partial_join e1 e2 in

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

@ -294,7 +294,7 @@ let rec dotty_mk_node pe sigma =
let n = !dotty_state_count in let n = !dotty_state_count in
incr dotty_state_count; incr dotty_state_count;
let do_hpred_lambda exp_color = function let do_hpred_lambda exp_color = function
| (Sil.Hpointsto (e, Sil.Earray(e', l, _), Sil.Sizeof(Sil.Tarray(t, _), _)), lambda) -> | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Sil.Sizeof (Sil.Tarray(t, _), _, _)), lambda) ->
incr dotty_state_count; (* increment once more n+1 is the box for the array *) incr dotty_state_count; (* increment once more n+1 is the box for the array *)
let e_color_str = color_to_str (exp_color e) in let e_color_str = color_to_str (exp_color e) in
let e_color_str'= color_to_str (exp_color e') in let e_color_str'= color_to_str (exp_color e') in
@ -673,7 +673,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) =
(* print a struct node *) (* print a struct node *)
let rec print_struct f pe e te l coo c = let rec print_struct f pe e te l coo c =
let print_type = match te with let print_type = match te with
| Sil.Sizeof (t, _) -> | Sil.Sizeof (t, _, _) ->
let str_t = Sil.typ_to_string t in let str_t = Sil.typ_to_string t in
(match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with (match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with
| [_; _] -> "BLOCK object" | [_; _] -> "BLOCK object"

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

@ -388,9 +388,9 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| Sil.Cast (_, e1) -> | Sil.Cast (_, e1) ->
if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
_exp_rv_dexp seen node e1 _exp_rv_dexp seen node e1
| Sil.Sizeof (typ, sub) -> | Sil.Sizeof (typ, len, sub) ->
if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dsizeof (typ, sub)) Some (Sil.Dsizeof (typ, len, sub))
| _ -> | _ ->
if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None None
@ -497,12 +497,12 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(Pvar.is_local pvar || Pvar.is_global pvar) && (Pvar.is_local pvar || Pvar.is_global pvar) &&
not (pvar_is_frontend_tmp pvar) && not (pvar_is_frontend_tmp pvar) &&
match hpred_typ_opt, find_typ_without_ptr prop pvar with match hpred_typ_opt, find_typ_without_ptr prop pvar with
| Some (Sil.Sizeof (t1, _)), Some (Sil.Sizeof (Sil.Tptr (_t2, _), _)) -> | Some (Sil.Sizeof (t1, _, _)), Some (Sil.Sizeof (Sil.Tptr (t2_, _), _, _)) ->
(try (try
let t2 = Tenv.expand_type tenv _t2 in let t2 = Tenv.expand_type tenv t2_ in
Sil.typ_equal t1 t2 Sil.typ_equal t1 t2
with exn when SymOp.exn_not_failure exn -> false) with exn when SymOp.exn_not_failure exn -> false)
| Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) | Some (Sil.Sizeof (Sil.Tint _, _, _)), Some (Sil.Sizeof (Sil.Tint _, _, _))
when is_file -> (* must be a file opened with "open" *) when is_file -> (* must be a file opened with "open" *)
true true
| _ -> false in | _ -> false in
@ -570,7 +570,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
(match lexp with (match lexp with
| Sil.Lvar pv -> | Sil.Lvar pv ->
let typo = match texp with let typo = match texp with
| Sil.Sizeof (Sil.Tstruct struct_typ, _) -> | Sil.Sizeof (Sil.Tstruct struct_typ, _, _) ->
(try (try
let _, t, _ = let _, t, _ =
IList.find (fun (f', _, _) -> IList.find (fun (f', _, _) ->
@ -596,7 +596,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
(match lexp with (match lexp with
| Sil.Lvar pv when not (pvar_is_frontend_tmp pv) -> | Sil.Lvar pv when not (pvar_is_frontend_tmp pv) ->
let typo = match texp with let typo = match texp with
| Sil.Sizeof (typ, _) -> Some typ | Sil.Sizeof (typ, _, _) -> Some typ
| _ -> None in | _ -> None in
Some (Sil.Dpvar pv), typo Some (Sil.Dpvar pv), typo
| Sil.Var id -> | Sil.Var id ->

5
infer/src/backend/iList.ml
Unescape View File

@ -28,6 +28,11 @@ let sort = List.sort
let stable_sort = List.stable_sort let stable_sort = List.stable_sort
let tl = List.tl let tl = List.tl
let rec last = function
| [] -> invalid_arg "IList.last"
| [x] -> x
| _ :: xs -> last xs
(** tail-recursive variant of List.fold_right *) (** tail-recursive variant of List.fold_right *)
let fold_right f l a = let fold_right f l a =
let g x y = f y x in let g x y = f y x in

3
infer/src/backend/iList.mli
Unescape View File

@ -64,6 +64,9 @@ val split : ('a * 'b) list -> 'a list * 'b list
val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
val tl : 'a list -> 'a list val tl : 'a list -> 'a list
(** last element, raises invalid_arg if empty *)
val last : 'a list -> 'a
(* Drops the first n elements from a list. *) (* Drops the first n elements from a list. *)
val drop_first : int -> 'a list -> 'a list val drop_first : int -> 'a list -> 'a list

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

@ -640,7 +640,7 @@ let report_context_leaks pname sigma tenv =
let context_exps = let context_exps =
IList.fold_left IList.fold_left
(fun exps hpred -> match hpred with (fun exps hpred -> match hpred with
| Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _)) | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _, _))
when AndroidFramework.is_context tenv struct_typ && when AndroidFramework.is_context tenv struct_typ &&
not (AndroidFramework.is_application tenv struct_typ) -> not (AndroidFramework.is_application tenv struct_typ) ->
(exp, struct_typ) :: exps (exp, struct_typ) :: exps
@ -807,8 +807,8 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
let sigma_new_formals = let sigma_new_formals =
let do_formal (pv, typ) = let do_formal (pv, typ) =
let texp = match !Config.curr_language with let texp = match !Config.curr_language with
| Config.Clang -> Sil.Sizeof (typ, Sil.Subtype.exact) | Config.Clang -> Sil.Sizeof (typ, None, Sil.Subtype.exact)
| Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in | Config.Java -> Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in
IList.map do_formal new_formals in IList.map do_formal new_formals in
let sigma_seed = let sigma_seed =

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

@ -687,7 +687,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
| Some (Sil.Sizeof (Sil.Tstruct | Some (Sil.Sizeof (Sil.Tstruct
{ Sil.csu = Csu.Class _; { Sil.csu = Csu.Class _;
Sil.struct_name = Some classname; Sil.struct_name = Some classname;
}, _)) -> }, _, _)) ->
" of type " ^ Mangled.to_string classname ^ " " " of type " ^ Mangled.to_string classname ^ " "
| _ -> " " in | _ -> " " in
let desc_str = let desc_str =
@ -772,7 +772,7 @@ let desc_retain_cycle prop cycle loc cycle_dotty =
else e_str in else e_str in
str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining "^e_str^"."^(Ident.fieldname_to_string f)^", "; str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining "^e_str^"."^(Ident.fieldname_to_string f)^", ";
ct:=!ct +1 ct:=!ct +1
| Sil.Eexp(Sil.Sizeof(typ, _), _) -> | Sil.Eexp (Sil.Sizeof (typ, _, _), _) ->
str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") an object of "^(Sil.typ_to_string typ)^" retaining another object via instance variable "^(Ident.fieldname_to_string f)^", "; str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") an object of "^(Sil.typ_to_string typ)^" retaining another object via instance variable "^(Ident.fieldname_to_string f)^", ";
ct:=!ct +1 ct:=!ct +1
| _ -> () in | _ -> () in

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

@ -76,7 +76,8 @@ let add_array_to_prop pdesc prop_ lexp typ =
let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in
let s = mk_empty_array_rearranged size in let s = mk_empty_array_rearranged size in
let hpred = let hpred =
Prop.mk_ptsto n_lexp s (Sil.Sizeof(Sil.Tarray(typ', size), Sil.Subtype.exact)) in Prop.mk_ptsto n_lexp s
(Sil.Sizeof (Sil.Tarray (typ', size), None, Sil.Subtype.exact)) in
let sigma = Prop.get_sigma prop in let sigma = Prop.get_sigma prop in
let sigma_fp = Prop.get_sigma_footprint prop in let sigma_fp = Prop.get_sigma_footprint prop in
let prop'= Prop.replace_sigma (hpred:: sigma) prop in let prop'= Prop.replace_sigma (hpred:: sigma) prop in
@ -157,13 +158,13 @@ let create_type tenv n_lexp typ prop =
| Sil.Tptr (typ', _) -> | Sil.Tptr (typ', _) ->
let sexp = Sil.Estruct ([], Sil.inst_none) in let sexp = Sil.Estruct ([], Sil.inst_none) in
let typ'' = Tenv.expand_type tenv typ' in let typ'' = Tenv.expand_type tenv typ' in
let texp = Sil.Sizeof (typ'', Sil.Subtype.subtypes) in let texp = Sil.Sizeof (typ'', None, Sil.Subtype.subtypes) in
let hpred = Prop.mk_ptsto n_lexp sexp texp in let hpred = Prop.mk_ptsto n_lexp sexp texp in
Some hpred Some hpred
| Sil.Tarray _ -> | Sil.Tarray _ ->
let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in
let sexp = mk_empty_array size in let sexp = mk_empty_array size in
let texp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in let texp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
let hpred = Prop.mk_ptsto n_lexp sexp texp in let hpred = Prop.mk_ptsto n_lexp sexp texp in
Some hpred Some hpred
| _ -> None in | _ -> None in
@ -569,7 +570,7 @@ let execute___release_autorelease_pool
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
| _ -> false) (Prop.get_sigma prop_) in | _ -> false) (Prop.get_sigma prop_) in
match hpred with match hpred with
| Sil.Hpointsto(_, _, Sil.Sizeof (typ, _)) -> | Sil.Hpointsto (_, _, Sil.Sizeof (typ, _, _)) ->
let res1 = let res1 =
execute___objc_release execute___objc_release
{ builtin_args with { builtin_args with
@ -668,7 +669,7 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1 | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
| _ -> false) (Prop.get_sigma prop) in | _ -> false) (Prop.get_sigma prop) in
match hpred, texp2 with match hpred, texp2 with
| Sil.Hpointsto(val1, _, _), Sil.Sizeof (_, _) -> | Sil.Hpointsto (val1, _, _), Sil.Sizeof _ ->
let prop' = replace_ptsto_texp prop val1 texp2 in let prop' = replace_ptsto_texp prop val1 texp2 in
[(return_result val1 prop' ret_ids, path)] [(return_result val1 prop' ret_ids, path)]
| _ -> [(return_result val1 prop ret_ids, path)] | _ -> [(return_result val1 prop ret_ids, path)]
@ -760,19 +761,22 @@ let execute_alloc mk can_return_null
| Sil.BinOp (bop, e1', e2') -> | Sil.BinOp (bop, e1', e2') ->
Sil.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2') Sil.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2')
| Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e | Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e
| Sil.Sizeof (Sil.Tarray(Sil.Tint ik, size), _) when Sil.ikind_is_char ik -> | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, _), Some len, _) when Sil.ikind_is_char ik ->
evaluate_char_sizeof size evaluate_char_sizeof len
| Sil.Sizeof (Sil.Tarray (Sil.Tint ik, len), None, _) when Sil.ikind_is_char ik ->
evaluate_char_sizeof len
| Sil.Sizeof _ -> e in | Sil.Sizeof _ -> e in
let handle_sizeof_exp size_exp = let handle_sizeof_exp len =
Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size_exp), Sil.Subtype.exact) in Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, len), Some len, Sil.Subtype.exact) in
let size_exp, procname = match args with let size_exp, procname = match args with
| [(Sil.Sizeof (Sil.Tstruct | [(Sil.Sizeof
{ Sil.csu = Csu.Class Csu.Objc; struct_name = Some c } as s, subt), _)] -> (Sil.Tstruct
{ Sil.csu = Csu.Class Csu.Objc; struct_name = Some c } as s, len, subt), _)] ->
let struct_type = let struct_type =
match AttributesTable.get_correct_type_from_objc_class_name c with match AttributesTable.get_correct_type_from_objc_class_name c with
| Some struct_type -> struct_type | Some struct_type -> struct_type
| None -> s in | None -> s in
Sil.Sizeof (struct_type, subt), pname Sil.Sizeof (struct_type, len, subt), pname
| [(size_exp, _)] -> (* for malloc and __new *) | [(size_exp, _)] -> (* for malloc and __new *)
size_exp, Sil.mem_alloc_pname mk size_exp, Sil.mem_alloc_pname mk
| [(size_exp, _); (Sil.Const (Sil.Cfun pname), _)] -> | [(size_exp, _); (Sil.Const (Sil.Cfun pname), _)] ->
@ -822,7 +826,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
| Sil.Hpointsto (e, _, _) -> Sil.exp_equal e n_lexp | Sil.Hpointsto (e, _, _) -> Sil.exp_equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in | _ -> false) (Prop.get_sigma prop) in
match hpred with match hpred with
| Sil.Hpointsto (_, _, Sil.Sizeof (dynamic_type, _)) -> dynamic_type | Sil.Hpointsto (_, _, Sil.Sizeof (dynamic_type, _, _)) -> dynamic_type
| _ -> typ | _ -> typ
with Not_found -> typ in with Not_found -> typ in
let typ_string = Sil.typ_to_string typ in let typ_string = Sil.typ_to_string typ in
@ -1157,7 +1161,7 @@ let execute_objc_alloc_no_fail
{ Builtin.pdesc; tenv; ret_ids; loc; } = { Builtin.pdesc; tenv; ret_ids; loc; } =
let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in
let ptr_typ = Sil.Tptr (typ, Sil.Pk_pointer) in let ptr_typ = Sil.Tptr (typ, Sil.Pk_pointer) in
let sizeof_typ = Sil.Sizeof (typ, Sil.Subtype.exact) in let sizeof_typ = Sil.Sizeof (typ, None, Sil.Subtype.exact) in
let alloc_fun_exp = let alloc_fun_exp =
match alloc_fun_opt with match alloc_fun_opt with
| Some pname -> [Sil.Const (Sil.Cfun pname), Sil.Tvoid] | Some pname -> [Sil.Const (Sil.Cfun pname), Sil.Tvoid]

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

@ -456,9 +456,10 @@ let sym_eval abs e =
Sil.Const (Sil.Cclosure { c with captured_vars; }) Sil.Const (Sil.Cclosure { c with captured_vars; })
| Sil.Const _ -> | Sil.Const _ ->
e e
| Sil.Sizeof (Sil.Tarray (Sil.Tint ik, e), _) | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, l), None, _)
| Sil.Sizeof (Sil.Tarray (Sil.Tint ik, _), Some l, _)
when Sil.ikind_is_char ik && !Config.curr_language <> Config.Java -> when Sil.ikind_is_char ik && !Config.curr_language <> Config.Java ->
eval e eval l
| Sil.Sizeof _ -> | Sil.Sizeof _ ->
e e
| Sil.Cast (_, e1) -> | Sil.Cast (_, e1) ->
@ -593,7 +594,7 @@ let sym_eval abs e =
eval (Sil.BinOp (Sil.PlusPI, e11, e2')) eval (Sil.BinOp (Sil.PlusPI, e11, e2'))
| Sil.BinOp | Sil.BinOp
(Sil.PlusA, (Sil.PlusA,
(Sil.Sizeof (Sil.Tstruct struct_typ, _) as e1), (Sil.Sizeof (Sil.Tstruct struct_typ, None, _) as e1),
e2) -> e2) ->
(* pattern for extensible structs given a struct declatead as struct s { ... t arr[n] ... }, (* pattern for extensible structs given a struct declatead as struct s { ... t arr[n] ... },
allocation pattern malloc(sizeof(struct s) + k * siezof(t)) turn it into allocation pattern malloc(sizeof(struct s) + k * siezof(t)) turn it into
@ -603,13 +604,13 @@ let sym_eval abs e =
let instance_fields = struct_typ.Sil.instance_fields in let instance_fields = struct_typ.Sil.instance_fields in
(match IList.rev instance_fields, e2' with (match IList.rev instance_fields, e2' with
(fname, Sil.Tarray (typ, size), _) :: ltfa, (fname, Sil.Tarray (typ, size), _) :: ltfa,
Sil.BinOp(Sil.Mult, num_elem, Sil.Sizeof (texp, st)) Sil.BinOp(Sil.Mult, num_elem, Sil.Sizeof (texp, None, st))
when instance_fields != [] && Sil.typ_equal typ texp -> when instance_fields != [] && Sil.typ_equal typ texp ->
let size' = Sil.BinOp(Sil.PlusA, size, num_elem) in let size' = Sil.BinOp(Sil.PlusA, size, num_elem) in
let ltfa' = (fname, Sil.Tarray(typ, size'), Sil.item_annotation_empty) :: ltfa in let ltfa' = (fname, Sil.Tarray(typ, size'), Sil.item_annotation_empty) :: ltfa in
let struct_typ' = let struct_typ' =
{ struct_typ with Sil.instance_fields = IList.rev ltfa' } in { struct_typ with Sil.instance_fields = IList.rev ltfa' } in
Sil.Sizeof (Sil.Tstruct struct_typ', st) Sil.Sizeof (Sil.Tstruct struct_typ', None, st)
| _ -> Sil.BinOp(Sil.PlusA, e1', e2')) | _ -> Sil.BinOp(Sil.PlusA, e1', e2'))
| Sil.BinOp (Sil.PlusA as oplus, e1, e2) | Sil.BinOp (Sil.PlusA as oplus, e1, e2)
| Sil.BinOp (Sil.PlusPI as oplus, e1, e2) -> | Sil.BinOp (Sil.PlusPI as oplus, e1, e2) ->
@ -625,6 +626,19 @@ let sym_eval abs e =
| _ -> Sil.BinOp (ominus, x, y) in | _ -> Sil.BinOp (ominus, x, y) in
begin begin
match e1', e2' with match e1', e2' with
| Sil.Sizeof (typ, Some len1, st),
Sil.BinOp (Sil.Mult, len2, Sil.Sizeof (elt, None, _))
when isPlusA
&& (match typ with
| Sil.Tarray (elt2, _) ->
Sil.typ_equal elt elt2
| Sil.Tstruct {instance_fields= _::_ as flds} ->
Sil.typ_equal elt (snd3 (IList.last flds))
| _ ->
false) ->
(* pattern for extensible structs:
sizeof(struct s {... t[l]}) + k * sizeof(elt)) = sizeof(struct s {... t[l + k]}) *)
Sil.Sizeof (typ, Some (len1 +++ len2), st)
| Sil.Const c, _ when iszero_int_float c -> | Sil.Const c, _ when iszero_int_float c ->
e2' e2'
| _, Sil.Const c when iszero_int_float c -> | _, Sil.Const c when iszero_int_float c ->
@ -691,13 +705,6 @@ let sym_eval abs e =
| Sil.BinOp (Sil.MinusPP, e1, e2) -> | Sil.BinOp (Sil.MinusPP, e1, e2) ->
if abs then Sil.exp_get_undefined false if abs then Sil.exp_get_undefined false
else Sil.BinOp (Sil.MinusPP, eval e1, eval e2) else Sil.BinOp (Sil.MinusPP, eval e1, eval e2)
| Sil.BinOp (Sil.Mult, esize, Sil.Sizeof (t, st))
| Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st), esize) ->
begin
match eval esize, eval (Sil.Sizeof (t, st)) with
| Sil.Const (Sil.Cint i), e' when Sil.Int.isone i -> e'
| esize', e' -> Sil.BinOp(Sil.Mult, esize', e')
end
| Sil.BinOp (Sil.Mult, e1, e2) -> | Sil.BinOp (Sil.Mult, e1, e2) ->
let e1' = eval e1 in let e1' = eval e1 in
let e2' = eval e2 in let e2' = eval e2 in
@ -721,6 +728,9 @@ let sym_eval abs e =
Sil.exp_float (v *. w) Sil.exp_float (v *. w)
| Sil.Var _, Sil.Var _ -> | Sil.Var _, Sil.Var _ ->
Sil.BinOp(Sil.Mult, e1', e2') Sil.BinOp(Sil.Mult, e1', e2')
| _, Sil.Sizeof _
| Sil.Sizeof _, _ ->
Sil.BinOp(Sil.Mult, e1', e2')
| _, _ -> | _, _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp(Sil.Mult, e1', e2') if abs then Sil.exp_get_undefined false else Sil.BinOp(Sil.Mult, e1', e2')
end end
@ -739,10 +749,11 @@ let sym_eval abs e =
Sil.exp_int (Sil.Int.div n m) Sil.exp_int (Sil.Int.div n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) -> | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_float (v /.w) Sil.exp_float (v /.w)
| Sil.Sizeof(Sil.Tarray(typ, size), _), Sil.Sizeof(_typ, _) | Sil.Sizeof (Sil.Tarray (elt, _), Some len, _), Sil.Sizeof (elt2, None, _)
(* pattern: sizeof(arr) / sizeof(arr[0]) = size of arr *) | Sil.Sizeof (Sil.Tarray (elt, len), None, _), Sil.Sizeof (elt2, None, _)
when Sil.typ_equal _typ typ -> (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
size when Sil.typ_equal elt elt2 ->
len
| _ -> | _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Div, e1', e2') if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Div, e1', e2')
end end
@ -842,7 +853,8 @@ let exp_normalize sub exp =
else sym_eval false exp' else sym_eval false exp'
let rec texp_normalize sub exp = match exp with let rec texp_normalize sub exp = match exp with
| Sil.Sizeof (typ, st) -> Sil.Sizeof (typ_normalize sub typ, st) | Sil.Sizeof (typ, len, st) ->
Sil.Sizeof (typ_normalize sub typ, Option.map (exp_normalize sub) len, st)
| _ -> exp_normalize sub exp | _ -> exp_normalize sub exp
(* NOTE: usage of == operator in flds_norm and typ_normalize is intended*) (* NOTE: usage of == operator in flds_norm and typ_normalize is intended*)
@ -1141,7 +1153,7 @@ let rec strexp_normalize sub se =
end end
(** 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 *)
let rec create_strexp_of_type tenvo struct_init_mode typ inst = let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
let init_value () = let init_value () =
let create_fresh_var () = let create_fresh_var () =
let fresh_id = let fresh_id =
@ -1154,24 +1166,30 @@ let rec create_strexp_of_type tenvo struct_init_mode typ inst =
| _ -> Sil.exp_zero | _ -> Sil.exp_zero
else else
create_fresh_var () in create_fresh_var () in
match typ with match typ, len with
| Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ -> | (Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _), None ->
Sil.Eexp (init_value (), inst) Sil.Eexp (init_value (), inst)
| Sil.Tstruct { Sil.instance_fields } -> | Sil.Tstruct { Sil.instance_fields }, _ -> (
begin match struct_init_mode with
match struct_init_mode with | No_init ->
| No_init -> Sil.Estruct ([], inst) Sil.Estruct ([], inst)
| Fld_init -> | Fld_init ->
let f (fld, t, a) = (* pass len as an accumulator, so that it is passed to create_strexp_of_type for the last
if Sil.is_objc_ref_counter_field (fld, t, a) then field, but always return None so that only the last field receives len *)
(fld, Sil.Eexp (Sil.exp_one, inst)) let f (fld, t, a) (flds, len) =
else if Sil.is_objc_ref_counter_field (fld, t, a) then
(fld, create_strexp_of_type tenvo struct_init_mode t inst) in ((fld, Sil.Eexp (Sil.exp_one, inst)) :: flds, None)
Sil.Estruct (IList.map f instance_fields, inst) else
end ((fld, create_strexp_of_type tenvo struct_init_mode t len inst) :: flds, None) in
| Sil.Tarray (_, size) -> let flds, _ = IList.fold_right f instance_fields ([], len) in
Sil.Estruct (flds, inst)
)
| Sil.Tarray (_, size), None ->
Sil.Earray (size, [], inst) Sil.Earray (size, [], inst)
| Sil.Tvar _ -> | Sil.Tarray _, Some len ->
Sil.Earray (len, [], inst)
| Sil.Tvar _, _
| (Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _), Some _ ->
assert false assert false
(** Sil.Construct a pointsto. *) (** Sil.Construct a pointsto. *)
@ -1185,8 +1203,8 @@ let mk_ptsto lexp sexp te =
initialize the fields of structs with fresh variables. *) initialize the fields of structs with fresh variables. *)
let mk_ptsto_exp tenvo struct_init_mode (exp, te, expo) inst : Sil.hpred = let mk_ptsto_exp tenvo struct_init_mode (exp, te, expo) inst : Sil.hpred =
let default_strexp () = match te with let default_strexp () = match te with
| Sil.Sizeof (typ, _) -> | Sil.Sizeof (typ, len, _) ->
create_strexp_of_type tenvo struct_init_mode typ inst create_strexp_of_type tenvo struct_init_mode typ len inst
| Sil.Var _ -> | Sil.Var _ ->
Sil.Estruct ([], inst) Sil.Estruct ([], inst)
| te -> | te ->
@ -1214,19 +1232,24 @@ let rec hpred_normalize sub hpred =
let normalized_cnt = strexp_normalize sub cnt in let normalized_cnt = strexp_normalize sub cnt in
let normalized_te = texp_normalize sub te in let normalized_te = texp_normalize sub te in
begin match normalized_cnt, normalized_te with begin match normalized_cnt, normalized_te with
| Sil.Earray (Sil.Sizeof (t, st1), [], inst), Sil.Sizeof (Sil.Tarray _, _) -> | Sil.Earray (Sil.Sizeof _ as size, [], inst), Sil.Sizeof (Sil.Tarray _, _, _) ->
(* check for an empty array whose size expression is (Sizeof type), and turn the array (* check for an empty array whose size expression is (Sizeof type), and turn the array
into a strexp of the given type *) into a strexp of the given type *)
let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (t, st1), None) inst in let hpred' = mk_ptsto_exp None Fld_init (root, size, None) inst in
replace_hpred hpred' replace_hpred hpred'
| Sil.Earray (Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st1), x), esel, inst), | ( Sil.Earray (Sil.BinOp (Sil.Mult, Sil.Sizeof (t, None, st1), x), esel, inst)
Sil.Sizeof (Sil.Tarray _, _) | Sil.Earray (Sil.BinOp (Sil.Mult, x, Sil.Sizeof (t, None, st1)), esel, inst)),
| Sil.Earray (Sil.BinOp(Sil.Mult, x, Sil.Sizeof (t, st1)), esel, inst), Sil.Sizeof (Sil.Tarray (elt, _) as arr, _, _)
Sil.Sizeof (Sil.Tarray _, _) -> when Sil.typ_equal t elt ->
(* check for an array whose size expression is n * (Sizeof type), and turn the array let len = Some x in
into a strexp of the given type *) let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (arr, len, st1), None) inst in
let hpred' = replace_hpred (replace_array_contents hpred' esel)
mk_ptsto_exp None Fld_init (root, Sil.Sizeof (Sil.Tarray(t, x), st1), None) inst in | ( Sil.Earray (Sil.BinOp (Sil.Mult, Sil.Sizeof (t, Some len, st1), x), esel, inst)
| Sil.Earray (Sil.BinOp (Sil.Mult, x, Sil.Sizeof (t, Some len, st1)), esel, inst)),
Sil.Sizeof (Sil.Tarray (elt, _) as arr, _, _)
when Sil.typ_equal t elt ->
let len = Some (Sil.BinOp(Sil.Mult, x, len)) in
let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (arr, len, st1), None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| _ -> Sil.Hpointsto (normalized_root, normalized_cnt, normalized_te) | _ -> Sil.Hpointsto (normalized_root, normalized_cnt, normalized_te)
end end
@ -1337,7 +1360,8 @@ let rec pi_sorted_remove_redundant = function
let sigma_get_unsigned_exps sigma = let sigma_get_unsigned_exps sigma =
let uexps = ref [] in let uexps = ref [] in
let do_hpred = function let do_hpred = function
| Sil.Hpointsto(_, Sil.Eexp(e, _), Sil.Sizeof (Sil.Tint ik, _)) when Sil.ikind_is_unsigned ik -> | Sil.Hpointsto (_, Sil.Eexp (e, _), Sil.Sizeof (Sil.Tint ik, _, _))
when Sil.ikind_is_unsigned ik ->
uexps := e :: !uexps uexps := e :: !uexps
| _ -> () in | _ -> () in
IList.iter do_hpred sigma; IList.iter do_hpred sigma;
@ -1622,13 +1646,13 @@ let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
| (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e | (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e
| _ -> false in | _ -> false in
let extend_path hpred (snk_exp, path, reachable_hpreds) = match hpred with let extend_path hpred (snk_exp, path, reachable_hpreds) = match hpred with
| Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Sil.Sizeof (typ, _)) -> | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Sil.Sizeof (typ, _, _)) ->
(try (try
let fld, _ = IList.find (fun fld -> strexp_matches snk_exp fld) flds in let fld, _ = IList.find (fun fld -> strexp_matches snk_exp fld) flds in
let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
(lhs, (Some fld, typ) :: path, reachable_hpreds') (lhs, (Some fld, typ) :: path, reachable_hpreds')
with Not_found -> (snk_exp, path, reachable_hpreds)) with Not_found -> (snk_exp, path, reachable_hpreds))
| Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Sil.Sizeof (typ, _)) -> | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Sil.Sizeof (typ, _, _)) ->
if IList.exists (fun pair -> strexp_matches snk_exp pair) elems if IList.exists (fun pair -> strexp_matches snk_exp pair) elems
then then
let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
@ -2039,7 +2063,8 @@ let find_arithmetic_problem proc_node_session prop exp =
| Sil.Lvar _ -> () | Sil.Lvar _ -> ()
| Sil.Lfield (e, _, _) -> walk e | Sil.Lfield (e, _, _) -> walk e
| Sil.Lindex (e1, e2) -> walk e1; walk e2 | Sil.Lindex (e1, e2) -> walk e1; walk e2
| Sil.Sizeof _ -> () in | Sil.Sizeof (_, None, _) -> ()
| Sil.Sizeof (_, Some len, _) -> walk len in
walk exp; walk exp;
try Some (Div0 (IList.find check_zero !exps_divided)), !res try Some (Div0 (IList.find check_zero !exps_divided)), !res
with Not_found -> with Not_found ->
@ -2320,7 +2345,8 @@ let rec exp_captured_ren ren = function
| Sil.Var id -> Sil.Var (ident_captured_ren ren id) | Sil.Var id -> Sil.Var (ident_captured_ren ren id)
| Sil.Const (Sil.Cexn e) -> Sil.Const (Sil.Cexn (exp_captured_ren ren e)) | Sil.Const (Sil.Cexn e) -> Sil.Const (Sil.Cexn (exp_captured_ren ren e))
| Sil.Const _ as e -> e | Sil.Const _ as e -> e
| Sil.Sizeof (t, st) -> Sil.Sizeof (typ_captured_ren ren t, st) | Sil.Sizeof (t, len, st) ->
Sil.Sizeof (typ_captured_ren ren t, Option.map (exp_captured_ren ren) len, st)
| Sil.Cast (t, e) -> Sil.Cast (t, exp_captured_ren ren e) | Sil.Cast (t, e) -> Sil.Cast (t, exp_captured_ren ren e)
| Sil.UnOp (op, e, topt) -> | Sil.UnOp (op, e, topt) ->
let topt' = match topt with let topt' = match topt with

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

@ -221,7 +221,8 @@ val mk_neq : exp -> exp -> atom
val mk_eq : exp -> exp -> atom val mk_eq : exp -> exp -> 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: Tenv.t option -> struct_init_mode -> Sil.typ -> Sil.inst -> Sil.strexp val create_strexp_of_type :
Tenv.t option -> struct_init_mode -> Sil.typ -> Sil.exp option -> Sil.inst -> Sil.strexp
(** Construct a pointsto. *) (** Construct a pointsto. *)
val mk_ptsto : exp -> strexp -> exp -> hpred val mk_ptsto : exp -> strexp -> exp -> hpred

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

@ -371,7 +371,7 @@ end = struct
let add_lt_minus1_e e = let add_lt_minus1_e e =
lts := (Sil.exp_minus_one, e)::!lts in lts := (Sil.exp_minus_one, e)::!lts in
let texp_is_unsigned = function let texp_is_unsigned = function
| Sil.Sizeof (Sil.Tint ik, _) -> Sil.ikind_is_unsigned ik | Sil.Sizeof (Sil.Tint ik, _, _) -> Sil.ikind_is_unsigned ik
| _ -> false in | _ -> false in
let strexp_lt_minus1 = function let strexp_lt_minus1 = function
| Sil.Eexp (e, _) -> add_lt_minus1_e e | Sil.Eexp (e, _) -> add_lt_minus1_e e
@ -415,7 +415,8 @@ end = struct
(* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *) (* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
match e1, e2 with match e1, e2 with
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.leq n1 n2 | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.leq n1 n2
| Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, _), Sil.Sizeof (t2, _)), Sil.Const(Sil.Cint n2) | Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, None, _), Sil.Sizeof (t2, None, _)),
Sil.Const(Sil.Cint n2)
when Sil.Int.isminusone n2 && type_size_comparable t1 t2 -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *) when Sil.Int.isminusone n2 && type_size_comparable t1 t2 -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
check_type_size_lt t1 t2 check_type_size_lt t1 t2
| e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n |- e <= n] *) | e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n |- e <= n] *)
@ -1423,8 +1424,9 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
| Sil.Hpointsto (Sil.Lfield (e, fld, typ_fld), se, t) -> | Sil.Hpointsto (Sil.Lfield (e, fld, typ_fld), se, t) ->
let t' = match t, typ_fld with let t' = match t, typ_fld with
| _, Sil.Tstruct _ -> (* the struct type of fld is known *) | _, Sil.Tstruct _ -> (* the struct type of fld is known *)
Sil.Sizeof (typ_fld, Sil.Subtype.exact) Sil.Sizeof (typ_fld, None, Sil.Subtype.exact)
| Sil.Sizeof (t1, st), _ -> (* the struct type of fld is not known -- typically Tvoid *) | Sil.Sizeof (t1, len, st), _ ->
(* the struct type of fld is not known -- typically Tvoid *)
Sil.Sizeof Sil.Sizeof
(Sil.Tstruct (Sil.Tstruct
{ Sil.instance_fields = [(fld, t1, Sil.item_annotation_empty)]; { Sil.instance_fields = [(fld, t1, Sil.item_annotation_empty)];
@ -1434,18 +1436,18 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
Sil.superclasses = []; Sil.superclasses = [];
Sil.def_methods = []; Sil.def_methods = [];
Sil.struct_annotations = Sil.item_annotation_empty; Sil.struct_annotations = Sil.item_annotation_empty;
}, st) }, len, st)
(* None as we don't know the stuct name *) (* None as we don't know the stuct name *)
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
let hpred' = Sil.Hpointsto (e, Sil.Estruct ([(fld, se)], Sil.inst_none), t') in let hpred' = Sil.Hpointsto (e, Sil.Estruct ([(fld, se)], Sil.inst_none), t') in
expand true true hpred' expand true true hpred'
| Sil.Hpointsto (Sil.Lindex (e, ind), se, t) -> | Sil.Hpointsto (Sil.Lindex (e, ind), se, t) ->
let size = Sil.exp_get_undefined false in let clen = Sil.exp_get_undefined false in
let t' = match t with let t' = match t with
| Sil.Sizeof (_t, st) -> | Sil.Sizeof (t_, vlen, st) ->
Sil.Sizeof (Sil.Tarray (_t, size), st) Sil.Sizeof (Sil.Tarray (t_, clen), vlen, st)
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
let hpred' = Sil.Hpointsto (e, Sil.Earray (size, [(ind, se)], Sil.inst_none), t') in let hpred' = Sil.Hpointsto (e, Sil.Earray (clen, [(ind, se)], Sil.inst_none), t') in
expand true true hpred' expand true true hpred'
| Sil.Hpointsto (Sil.BinOp (Sil.PlusPI, e1, e2), Sil.Earray (size, esel, inst), t) -> | Sil.Hpointsto (Sil.BinOp (Sil.PlusPI, e1, e2), Sil.Earray (size, esel, inst), t) ->
let shift_exp e = Sil.BinOp (Sil.PlusA, e, e2) in let shift_exp e = Sil.BinOp (Sil.PlusA, e, e2) in
@ -1587,17 +1589,17 @@ struct
case, if they are possible *) case, if they are possible *)
let subtype_case_analysis tenv texp1 texp2 = let subtype_case_analysis tenv texp1 texp2 =
match texp1, texp2 with match texp1, texp2 with
| Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
begin begin
let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in
let pos_type_opt = match pos_opt with let pos_type_opt = match pos_opt with
| None -> None | None -> None
| Some st1' -> | Some st1' ->
let t1' = if check_subtype tenv t1 t2 then t1 else t2 in let t1', len1' = if check_subtype tenv t1 t2 then t1, len1 else t2, len2 in
Some (Sil.Sizeof (t1', st1')) in Some (Sil.Sizeof (t1', len1', st1')) in
let neg_type_opt = match neg_opt with let neg_type_opt = match neg_opt with
| None -> None | None -> None
| Some st1' -> Some (Sil.Sizeof (t1, st1')) in | Some st1' -> Some (Sil.Sizeof (t1, len1, st1')) in
pos_type_opt, neg_type_opt pos_type_opt, neg_type_opt
end end
| _ -> (* don't know, consider both possibilities *) | _ -> (* don't know, consider both possibilities *)
@ -1606,7 +1608,7 @@ end
let cast_exception tenv texp1 texp2 e1 subs = let cast_exception tenv texp1 texp2 e1 subs =
let _ = match texp1, texp2 with let _ = match texp1, texp2 with
| Sil.Sizeof (t1, _), Sil.Sizeof (t2, st2) -> | Sil.Sizeof (t1, _, _), Sil.Sizeof (t2, _, st2) ->
if Config.developer_mode || if Config.developer_mode ||
(Sil.Subtype.is_cast st2 && (Sil.Subtype.is_cast st2 &&
not (Subtyping_check.check_subtype tenv t1 t2)) then not (Subtyping_check.check_subtype tenv t1 t2)) then
@ -1636,8 +1638,10 @@ let get_overrides_of tenv supertype pname =
(** Check the equality of two types ignoring flags in the subtyping components *) (** Check the equality of two types ignoring flags in the subtyping components *)
let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
| Sil.Sizeof(t1, st1), Sil.Sizeof (t2, st2) -> | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
Sil.typ_equal t1 t2 && Sil.Subtype.equal_modulo_flag st1 st2 Sil.typ_equal t1 t2
&& (opt_equal Sil.exp_equal len1 len2)
&& Sil.Subtype.equal_modulo_flag st1 st2
| _ -> Sil.exp_equal texp1 texp2 | _ -> Sil.exp_equal texp1 texp2
(** check implication between type expressions *) (** check implication between type expressions *)
@ -1646,13 +1650,13 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
(* classes and arrays in Java, and just classes in C++ and ObjC *) (* classes and arrays in Java, and just classes in C++ and ObjC *)
let types_subject_to_dynamic_cast = let types_subject_to_dynamic_cast =
match texp1, texp2 with match texp1, texp2 with
| Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _) | Sil.Sizeof ((Sil.Tstruct _) as typ1, _, _), Sil.Sizeof (Sil.Tstruct _, _, _)
| Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _) | Sil.Sizeof ((Sil.Tarray _) as typ1, _, _), Sil.Sizeof (Sil.Tarray _, _, _)
| Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _) | Sil.Sizeof ((Sil.Tarray _) as typ1, _, _), Sil.Sizeof (Sil.Tstruct _, _, _)
| Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _) | Sil.Sizeof ((Sil.Tstruct _) as typ1, _, _), Sil.Sizeof (Sil.Tarray _, _, _)
when is_java_class typ1 -> true when is_java_class typ1 -> true
| Sil.Sizeof (typ1, _), Sil.Sizeof (typ2, _) -> | Sil.Sizeof (typ1, _, _), Sil.Sizeof (typ2, _, _) ->
(Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2) || (Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2) ||
(Sil.is_objc_class typ1 && Sil.is_objc_class typ2) (Sil.is_objc_class typ1 && Sil.is_objc_class typ2)
| _ -> false in | _ -> false in
@ -1706,24 +1710,25 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
let type_rhs e = let type_rhs e =
let sub_opt = ref None in let sub_opt = ref None in
let filter = function let filter = function
| Sil.Hpointsto(e', _, Sil.Sizeof(t, sub)) when Sil.exp_equal e' e -> | Sil.Hpointsto(e', _, Sil.Sizeof(t, len, sub)) when Sil.exp_equal e' e ->
sub_opt := Some (t, sub); sub_opt := Some (t, len, sub);
true true
| _ -> false in | _ -> false in
if IList.exists filter sigma2 then !sub_opt else None in if IList.exists filter sigma2 then !sub_opt else None in
let add_subtype () = match texp1, texp2, se1, se2 with let add_subtype () = match texp1, texp2, se1, se2 with
| Sil.Sizeof(Sil.Tptr (_t1, _), _), Sil.Sizeof(Sil.Tptr (_t2, _), _), | Sil.Sizeof (Sil.Tptr (t1_, _), None, _), Sil.Sizeof (Sil.Tptr (t2_, _), None, _),
Sil.Eexp(e1', _), Sil.Eexp(e2', _) Sil.Eexp (e1', _), Sil.Eexp (e2', _)
when not (is_allocated_lhs e1') -> when not (is_allocated_lhs e1') ->
begin begin
let t1, t2 = Tenv.expand_type tenv _t1, Tenv.expand_type tenv _t2 in let t1, t2 = Tenv.expand_type tenv t1_, Tenv.expand_type tenv t2_ in
match type_rhs e2' with match type_rhs e2' with
| Some (t2_ptsto , sub2) -> | Some (t2_ptsto, len2, sub2) ->
if not (Sil.typ_equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2 if not (Sil.typ_equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2
then begin then begin
let pos_type_opt, _ = let pos_type_opt, _ =
Subtyping_check.subtype_case_analysis tenv Subtyping_check.subtype_case_analysis tenv
(Sil.Sizeof (t1, Sil.Subtype.subtypes)) (Sil.Sizeof (t2_ptsto, sub2)) in (Sil.Sizeof (t1, None, Sil.Subtype.subtypes))
(Sil.Sizeof (t2_ptsto, len2, sub2)) in
match pos_type_opt with match pos_type_opt with
| Some t1_noptr -> | Some t1_noptr ->
ProverState.add_frame_typ (e1', t1_noptr); ProverState.add_frame_typ (e1', t1_noptr);
@ -1936,13 +1941,13 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
| _ -> None) | _ -> None)
| _ -> None in | _ -> None in
let mk_constant_string_hpred s = (* create an hpred from a constant string *) let mk_constant_string_hpred s = (* create an hpred from a constant string *)
let size = Sil.exp_int (Sil.Int.of_int (1 + String.length s)) in let len = Sil.exp_int (Sil.Int.of_int (1 + String.length s)) in
let root = Sil.Const (Sil.Cstr s) in let root = Sil.Const (Sil.Cstr s) in
let sexp = let sexp =
let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in
match !Config.curr_language with match !Config.curr_language with
| Config.Clang -> | Config.Clang ->
Sil.Earray (size, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none) Sil.Earray (len, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
| Config.Java -> | Config.Java ->
let mk_fld_sexp s = let mk_fld_sexp s =
let fld = Ident.create_fieldname (Mangled.from_string s) 0 in let fld = Ident.create_fieldname (Mangled.from_string s) 0 in
@ -1952,14 +1957,15 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
Sil.Estruct (IList.map mk_fld_sexp fields, Sil.inst_none) in Sil.Estruct (IList.map mk_fld_sexp fields, Sil.inst_none) in
let const_string_texp = let const_string_texp =
match !Config.curr_language with match !Config.curr_language with
| Config.Clang -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact) | Config.Clang ->
Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, len), Some len, Sil.Subtype.exact)
| Config.Java -> | Config.Java ->
let object_type = let object_type =
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in
let typ = match Tenv.lookup tenv object_type with let typ = match Tenv.lookup tenv object_type with
| Some typ -> typ | Some typ -> typ
| None -> assert false in | None -> assert false in
Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in Sil.Sizeof (Sil.Tstruct typ, None, Sil.Subtype.exact) in
Sil.Hpointsto (root, sexp, const_string_texp) in Sil.Hpointsto (root, sexp, const_string_texp) in
let mk_constant_class_hpred s = (* creat an hpred from a constant class *) let mk_constant_class_hpred s = (* creat an hpred from a constant class *)
let root = Sil.Const (Sil.Cclass (Ident.string_to_name s)) in let root = Sil.Const (Sil.Cclass (Ident.string_to_name s)) in
@ -1971,7 +1977,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let typ = match Tenv.lookup tenv class_type with let typ = match Tenv.lookup tenv class_type with
| Some typ -> typ | Some typ -> typ
| None -> assert false in | None -> assert false in
Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in Sil.Sizeof (Sil.Tstruct typ, None, Sil.Subtype.exact) in
Sil.Hpointsto (root, sexp, class_texp) in Sil.Hpointsto (root, sexp, class_texp) in
try try
(match move_primed_lhs_from_front subs sigma2 with (match move_primed_lhs_from_front subs sigma2 with

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

@ -392,10 +392,11 @@ let strexp_extend_values
let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in
IList.filter check_not_inconsistent atoms_se_typ_list in IList.filter check_not_inconsistent atoms_se_typ_list in
if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values"; if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values";
let st = match te with let len, st = match te with
| Sil.Sizeof(_, st) -> st | Sil.Sizeof(_, len, st) -> (len, st)
| _ -> Sil.Subtype.exact in | _ -> None, Sil.Subtype.exact in
IList.map (fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Sil.Sizeof (typ', st))) atoms_se_typ_list_filtered IList.map (fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Sil.Sizeof (typ', len, st)))
atoms_se_typ_list_filtered
let collect_root_offset exp = let collect_root_offset exp =
let root = Sil.root_of_lexp exp in let root = Sil.root_of_lexp exp in
@ -430,17 +431,17 @@ let mk_ptsto_exp_footprint
| Sil.Lvar pvar, [], Sil.Tfun _ -> | Sil.Lvar pvar, [], Sil.Tfun _ ->
let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
let fun_exp = Sil.Const (Sil.Cfun fun_name) in let fun_exp = Sil.Const (Sil.Cfun fun_name) in
([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, st))) ([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, None, st)))
| _, [], Sil.Tfun _ -> | _, [], Sil.Tfun _ ->
let atoms, se, t = let atoms, se, t =
create_struct_values create_struct_values
pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in
(atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, st))) (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, None, st)))
| _ -> | _ ->
let atoms, se, t = let atoms, se, t =
create_struct_values create_struct_values
pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in
(atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, st))) in (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, None, st))) in
let atoms, ptsto_foot = create_ptsto true off_foot in let atoms, ptsto_foot = create_ptsto true off_foot in
let sub = Sil.sub_of_list eqs in let sub = Sil.sub_of_list eqs in
let ptsto = Sil.hpred_sub sub ptsto_foot in let ptsto = Sil.hpred_sub sub ptsto_foot in
@ -709,7 +710,7 @@ let add_guarded_by_constraints prop lexp pdesc =
| _ -> | _ ->
prop_acc in prop_acc in
let hpred_check_flds prop_acc = function let hpred_check_flds prop_acc = function
| Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _)) -> | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _, _)) ->
IList.fold_left (check_fld_locks typ) prop_acc flds IList.fold_left (check_fld_locks typ) prop_acc flds
| _ -> | _ ->
prop_acc in prop_acc in
@ -926,7 +927,7 @@ let type_at_offset texp off =
strip_offset off' typ' strip_offset off' typ'
| _ -> None in | _ -> None in
match texp with match texp with
| Sil.Sizeof(typ, _) -> | Sil.Sizeof(typ, _, _) ->
strip_offset off typ strip_offset off typ
| _ -> None | _ -> None
@ -1080,7 +1081,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
IList.exists is_nullable_attr (Prop.get_exp_attributes prop exp) in IList.exists is_nullable_attr (Prop.get_exp_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, _, _)) ->
let fld_is_nullable fld = let fld_is_nullable fld =
match Annotations.get_field_type_and_annotation fld typ with match Annotations.get_field_type_and_annotation fld typ with
| Some (_, annot) -> Annotations.ia_is_nullable annot | Some (_, annot) -> Annotations.ia_is_nullable annot

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

@ -128,7 +128,7 @@ let rec apply_offlist
else else
begin begin
L.d_strln "WARNING: struct assignment treated as nondeterministic assignment"; L.d_strln "WARNING: struct assignment treated as nondeterministic assignment";
(f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ inst, typ, None) (f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None inst, typ, None)
end end
| [], Sil.Earray _ -> | [], Sil.Earray _ ->
let offlist' = (Sil.Off_index Sil.exp_zero):: offlist in let offlist' = (Sil.Off_index Sil.exp_zero):: offlist in
@ -213,7 +213,7 @@ let rec apply_offlist
Finally, before running this function, the tool should run strexp_extend_value Finally, before running this function, the tool should run strexp_extend_value
in rearrange.ml for the same se and offlist, so that all the necessary in rearrange.ml for the same se and offlist, so that all the necessary
extensions of se are done before this function. *) extensions of se are done before this function. *)
let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id = let ptsto_lookup pdesc tenv p (lexp, se, typ, len, st) offlist id =
let f = let f =
function Some exp -> exp | None -> Sil.Var id in function Some exp -> exp | None -> Sil.Var id in
let fp_root = let fp_root =
@ -226,7 +226,7 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id =
match !lookup_inst with match !lookup_inst with
| Some (Sil.Iinitial | Sil.Ialloc | Sil.Ilookup) -> true | Some (Sil.Iinitial | Sil.Ialloc | Sil.Ilookup) -> true
| _ -> false in | _ -> false in
let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', st)) in let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', len, st)) in
(e', ptsto', pred_insts_op', lookup_uninitialized) (e', ptsto', pred_insts_op', lookup_uninitialized)
(** [ptsto_update p (lexp,se,typ) offlist exp] takes (** [ptsto_update p (lexp,se,typ) offlist exp] takes
@ -240,7 +240,7 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id =
the tool should run strexp_extend_value in rearrange.ml for the same the tool should run strexp_extend_value in rearrange.ml for the same
se and offlist, so that all the necessary extensions of se are done se and offlist, so that all the necessary extensions of se are done
before this function. *) before this function. *)
let ptsto_update pdesc tenv p (lexp, se, typ, st) offlist exp = let ptsto_update pdesc tenv p (lexp, se, typ, len, st) offlist exp =
let f _ = exp in let f _ = exp in
let fp_root = let fp_root =
match lexp with Sil.Var id -> Ident.is_footprint id | _ -> false in match lexp with Sil.Var id -> Ident.is_footprint id | _ -> false in
@ -249,7 +249,7 @@ let ptsto_update pdesc tenv p (lexp, se, typ, st) offlist exp =
let pos = State.get_path_pos () in let pos = State.get_path_pos () in
apply_offlist apply_offlist
pdesc tenv p fp_root true (lexp, se, typ) offlist f (State.get_inst_update pos) lookup_inst in pdesc tenv p fp_root true (lexp, se, typ) offlist f (State.get_inst_update pos) lookup_inst in
let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', st)) in let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', len, st)) in
(ptsto', pred_insts_op') (ptsto', pred_insts_op')
let update_iter iter pi sigma = let update_iter iter pi sigma =
@ -526,8 +526,8 @@ let resolve_typename prop receiver_exp =
| _ :: hpreds -> loop hpreds in | _ :: hpreds -> loop hpreds in
loop (Prop.get_sigma prop) in loop (Prop.get_sigma prop) in
match typexp_opt with match typexp_opt with
| Some (Sil.Sizeof (Sil.Tstruct { Sil.struct_name = None }, _)) -> None | Some (Sil.Sizeof (Sil.Tstruct { Sil.struct_name = None }, _, _)) -> None
| Some (Sil.Sizeof (Sil.Tstruct { Sil.csu = Csu.Class ck; struct_name = Some name }, _)) -> | Some (Sil.Sizeof (Sil.Tstruct { Sil.csu = Csu.Class ck; struct_name = Some name }, _, _)) ->
Some (Typename.TN_csu (Csu.Class ck, name)) Some (Typename.TN_csu (Csu.Class ck, name))
| _ -> None | _ -> None
@ -777,7 +777,7 @@ let do_error_checks node_opt instr pname pdesc = match node_opt with
let add_strexp_to_footprint strexp abducted_pv typ prop = let add_strexp_to_footprint strexp abducted_pv typ prop =
let abducted_lvar = Sil.Lvar abducted_pv in let abducted_lvar = Sil.Lvar abducted_pv in
let lvar_pt_fpvar = let lvar_pt_fpvar =
let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in let sizeof_exp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
Prop.mk_ptsto abducted_lvar strexp sizeof_exp in Prop.mk_ptsto abducted_lvar strexp sizeof_exp in
let sigma_fp = Prop.get_sigma_footprint prop in let sigma_fp = Prop.get_sigma_footprint prop in
Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop) Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop)
@ -793,7 +793,7 @@ let add_to_footprint abducted_pv typ prop =
footprint. we can get rid of this special case if we fix the abduction on struct values *) footprint. we can get rid of this special case if we fix the abduction on struct values *)
let add_struct_value_to_footprint tenv abducted_pv typ prop = let add_struct_value_to_footprint tenv abducted_pv typ prop =
let struct_strexp = let struct_strexp =
Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ Sil.inst_none in Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None Sil.inst_none in
let prop' = add_strexp_to_footprint struct_strexp abducted_pv typ prop in let prop' = add_strexp_to_footprint struct_strexp abducted_pv typ prop in
prop', struct_strexp prop', struct_strexp
@ -876,9 +876,9 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
let iter_ren = Prop.prop_iter_make_id_primed id iter in let iter_ren = Prop.prop_iter_make_id_primed id iter in
let prop_ren = Prop.prop_iter_to_prop iter_ren in let prop_ren = Prop.prop_iter_to_prop iter_ren in
match Prop.prop_iter_current iter_ren with match Prop.prop_iter_current iter_ren with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) -> | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, len, st)), offlist) ->
let contents, new_ptsto, pred_insts_op, lookup_uninitialized = let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
ptsto_lookup pdesc tenv prop_ren (lexp, strexp, typ, st) offlist id in ptsto_lookup pdesc tenv prop_ren (lexp, strexp, typ, len, st) offlist id in
let update acc (pi, sigma) = let update acc (pi, sigma) =
let pi' = Sil.Aeq (Sil.Var(id), contents):: pi in let pi' = Sil.Aeq (Sil.Var(id), contents):: pi in
let sigma' = new_ptsto:: sigma in let sigma' = new_ptsto:: sigma in
@ -948,14 +948,14 @@ let load_ret_annots pname =
let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ = let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_set_ pdesc tenv rhs_exp acc_in iter = let execute_set_ pdesc tenv rhs_exp acc_in iter =
let (lexp, strexp, typ, st, offlist) = let (lexp, strexp, typ, len, st, offlist) =
match Prop.prop_iter_current iter with match Prop.prop_iter_current iter with
| (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) -> | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, len, st)), offlist) ->
(lexp, strexp, typ, st, offlist) (lexp, strexp, typ, len, st, offlist)
| _ -> assert false in | _ -> assert false in
let p = Prop.prop_iter_to_prop iter in let p = Prop.prop_iter_to_prop iter in
let new_ptsto, pred_insts_op = let new_ptsto, pred_insts_op =
ptsto_update pdesc tenv p (lexp, strexp, typ, st) offlist rhs_exp in ptsto_update pdesc tenv p (lexp, strexp, typ, len, st) offlist rhs_exp in
let update acc (pi, sigma) = let update acc (pi, sigma) =
let sigma' = new_ptsto:: sigma in let sigma' = new_ptsto:: sigma in
let iter' = update_iter iter pi sigma' in let iter' = update_iter iter pi sigma' in
@ -1058,7 +1058,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let lhs_is_ns_ptr () = let lhs_is_ns_ptr () =
IList.exists IList.exists
(function (function
| Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _)) -> | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _, _)) ->
Sil.exp_equal exp lhs_normal && is_nsnumber typ Sil.exp_equal exp lhs_normal && is_nsnumber typ
| _ -> false) | _ -> false)
(Prop.get_sigma prop__) in (Prop.get_sigma prop__) in
@ -1242,7 +1242,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
ret_old_path [Prop.exist_quantify (Sil.fav_from_list temps) prop_] ret_old_path [Prop.exist_quantify (Sil.fav_from_list temps) prop_]
| Sil.Declare_locals (ptl, _) -> | Sil.Declare_locals (ptl, _) ->
let sigma_locals = let sigma_locals =
let add_None (x, y) = (x, Sil.Sizeof (y, Sil.Subtype.exact), None) in let add_None (x, y) = (x, Sil.Sizeof (y, None, Sil.Subtype.exact), None) in
let sigma_locals () = let sigma_locals () =
IList.map IList.map
(Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial) (Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial)
@ -1353,7 +1353,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let havoc_actual_by_ref (actual, actual_typ) prop = let havoc_actual_by_ref (actual, actual_typ) prop =
let actual_pt_havocd_var = let actual_pt_havocd_var =
let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in
let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, Sil.Subtype.subtypes) in let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, None, Sil.Subtype.subtypes) in
Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in
replace_actual_hpred actual actual_pt_havocd_var prop in replace_actual_hpred actual actual_pt_havocd_var prop in
IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref

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

@ -473,8 +473,8 @@ let texp_star texp1 texp2 =
if ftal_sub instance_fields1 instance_fields2 then t2 else t1 if ftal_sub instance_fields1 instance_fields2 then t2 else t1
| _ -> t1 in | _ -> t1 in
match texp1, texp2 with match texp1, texp2 with
| Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, _, st2) ->
Sil.Sizeof (typ_star t1 t2, Sil.Subtype.join st1 st2) Sil.Sizeof (typ_star t1 t2, len1, Sil.Subtype.join st1 st2)
| _ -> | _ ->
texp1 texp1
@ -629,7 +629,7 @@ let prop_get_exn_name pname prop =
let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in
let rec search_exn e = function let rec search_exn e = function
| [] -> None | [] -> None
| Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct { Sil.struct_name = Some name }, _)) :: _ | Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct { Sil.struct_name = Some name }, _, _)) :: _
when Sil.exp_equal e1 e -> when Sil.exp_equal e1 e ->
Some (Typename.TN_csu (Csu.Class Csu.Java, name)) Some (Typename.TN_csu (Csu.Class Csu.Java, name))
| _ :: tl -> search_exn e tl in | _ :: tl -> search_exn e tl in
@ -868,7 +868,7 @@ let mk_actual_precondition prop actual_params formal_params =
Prop.mk_ptsto Prop.mk_ptsto
(Sil.Lvar formal_var) (Sil.Lvar formal_var)
(Sil.Eexp (actual_e, Sil.inst_actual_precondition)) (Sil.Eexp (actual_e, Sil.inst_actual_precondition))
(Sil.Sizeof (actual_t, Sil.Subtype.exact)) in (Sil.Sizeof (actual_t, None, Sil.Subtype.exact)) in
let instantiated_formals = IList.map mk_instantiation formals_actuals in let instantiated_formals = IList.map mk_instantiation formals_actuals in
let actual_pre = Prop.prop_sigma_star prop instantiated_formals in let actual_pre = Prop.prop_sigma_star prop instantiated_formals in
Prop.normalize actual_pre Prop.normalize actual_pre

11
infer/src/backend/utils.ml
Unescape View File

@ -48,6 +48,13 @@ let opt_equal cmp x1 x2 = match x1, x2 with
| None, Some _ -> false | None, Some _ -> false
| Some y1, Some y2 -> cmp y1 y2 | Some y1, Some y2 -> cmp y1 y2
let opt_compare cmp x1 x2 =
match x1, x2 with
| Some y1, Some y2 -> cmp y1 y2
| None, None -> 0
| None, _ -> -1
| _, None -> 1
(** Efficient comparison for integers *) (** Efficient comparison for integers *)
let int_compare (i: int) (j: int) = i - j let int_compare (i: int) (j: int) = i - j
@ -64,6 +71,10 @@ let triple_compare compare compare' compare'' (x1, y1, z1) (x2, y2, z2) =
if n <> 0 then n else let n = compare' y1 y2 in if n <> 0 then n else let n = compare' y1 y2 in
if n <> 0 then n else compare'' z1 z2 if n <> 0 then n else compare'' z1 z2
let fst3 (x,_,_) = x
let snd3 (_,x,_) = x
let trd3 (_,_,x) = x
(** {2 Useful Modules} *) (** {2 Useful Modules} *)
(** Set of integers *) (** Set of integers *)

12
infer/src/backend/utils.mli
Unescape View File

@ -44,6 +44,9 @@ val int_equal : int -> int -> bool
(** Extend and equality function to an option type. *) (** Extend and equality function to an option type. *)
val opt_equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool val opt_equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
(** Comparison of option type. *)
val opt_compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
(** Generic comparison of pairs given a compare function for each element of the pair. *) (** Generic comparison of pairs given a compare function for each element of the pair. *)
val pair_compare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a * 'c) -> ('b * 'd) -> int val pair_compare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a * 'c) -> ('b * 'd) -> int
@ -59,6 +62,15 @@ val string_equal : string -> string -> bool
(** Comparison for floats *) (** Comparison for floats *)
val float_compare : float -> float -> int val float_compare : float -> float -> int
(** Return the first component of a triple. *)
val fst3 : 'a * 'b * 'c -> 'a
(** Return the second component of a triple. *)
val snd3 : 'a * 'b * 'c -> 'b
(** Return the third component of a triple. *)
val trd3 : 'a * 'b * 'c -> 'c
(** {2 Useful Modules} *) (** {2 Useful Modules} *)
(** Set of integers *) (** Set of integers *)

9
infer/src/clang/cTrans.ml
Unescape View File

@ -216,7 +216,7 @@ struct
CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in
let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in
{ empty_res_trans with { empty_res_trans with
exps = [(Sil.Sizeof(expanded_type, Sil.Subtype.exact), Sil.Tint Sil.IULong)] } exps = [(Sil.Sizeof(expanded_type, None, Sil.Subtype.exact), Sil.Tint Sil.IULong)] }
let add_reference_if_glvalue typ expr_info = let add_reference_if_glvalue typ expr_info =
(* glvalue definition per C++11:*) (* glvalue definition per C++11:*)
@ -426,7 +426,8 @@ struct
match tp with match tp with
| Some tp -> CTypes_decl.type_ptr_to_sil_type tenv tp | Some tp -> CTypes_decl.type_ptr_to_sil_type tenv tp
| None -> typ in (* Some default type since the type is missing *) | None -> typ in (* Some default type since the type is missing *)
{ empty_res_trans with exps = [(Sil.Sizeof(sizeof_typ, Sil.Subtype.exact), sizeof_typ)]} { empty_res_trans with
exps = [(Sil.Sizeof (sizeof_typ, None, Sil.Subtype.exact), sizeof_typ)] }
| k -> Printing.log_stats | k -> Printing.log_stats
"\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \ "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \
%s . Expression ignored, returned -1... \n" %s . Expression ignored, returned -1... \n"
@ -2189,7 +2190,7 @@ struct
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let cast_type = CTypes_decl.type_ptr_to_sil_type tenv cast_type_ptr in let cast_type = CTypes_decl.type_ptr_to_sil_type tenv cast_type_ptr in
let sizeof_expr = match cast_type with let sizeof_expr = match cast_type with
| Sil.Tptr (typ, _) -> Sil.Sizeof (typ, subtypes) | Sil.Tptr (typ, _) -> Sil.Sizeof (typ, None, subtypes)
| _ -> assert false in | _ -> assert false in
let builtin = Sil.Const (Sil.Cfun ModelBuiltins.__cast) in let builtin = Sil.Const (Sil.Cfun ModelBuiltins.__cast) in
let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
@ -2247,7 +2248,7 @@ struct
let fun_name = ModelBuiltins.__cxx_typeid in let fun_name = ModelBuiltins.__cxx_typeid in
let sil_fun = Sil.Const (Sil.Cfun fun_name) in let sil_fun = Sil.Const (Sil.Cfun fun_name) in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let type_info_objc = (Sil.Sizeof (typ, Sil.Subtype.exact), Sil.Tvoid) in let type_info_objc = (Sil.Sizeof (typ, None, Sil.Subtype.exact), Sil.Tvoid) in
let field_name_decl = Ast_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in let field_name_decl = Ast_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in
let field_name = General_utils.mk_class_field_name field_name_decl in let field_name = General_utils.mk_class_field_name field_name_decl in
let ret_exp = Sil.Var ret_id in let ret_exp = Sil.Var ret_id in

4
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -296,7 +296,7 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam
function_type, styp function_type, styp
| _ -> Sil.Tptr (function_type, Sil.Pk_pointer), function_type in | _ -> Sil.Tptr (function_type, Sil.Pk_pointer), function_type in
let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in
let sizeof_exp_ = Sil.Sizeof (function_type_np, Sil.Subtype.exact) in let sizeof_exp_ = Sil.Sizeof (function_type_np, None, Sil.Subtype.exact) in
let sizeof_exp = match size_exp_opt with let sizeof_exp = match size_exp_opt with
| Some exp -> Sil.BinOp (Sil.Mult, sizeof_exp_, exp) | Some exp -> Sil.BinOp (Sil.Mult, sizeof_exp_, exp)
| None -> sizeof_exp_ in | None -> sizeof_exp_ in
@ -366,7 +366,7 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc =
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let typ = CTypes.remove_pointer_to_typ cast_to_typ in let typ = CTypes.remove_pointer_to_typ cast_to_typ in
let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in
let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, None, Sil.Subtype.exact) in
let pname = ModelBuiltins.__objc_cast in let pname = ModelBuiltins.__objc_cast in
let args = [(exp, cast_from_typ); (sizeof_exp, Sil.Tint Sil.IULong)] in let args = [(exp, cast_from_typ); (sizeof_exp, Sil.Tint Sil.IULong)] in
let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in

2
infer/src/eradicate/eradicateChecks.ml
Unescape View File

@ -140,7 +140,7 @@ let check_condition case_zero find_canonical_duplicate curr_pname
Mangled.equal c throwable_class Mangled.equal c throwable_class
| _ -> false in | _ -> false in
let do_instr = function let do_instr = function
| Sil.Call (_, Sil.Const (Sil.Cfun pn), [_; (Sil.Sizeof(t, _), _)], _, _) when | Sil.Call (_, Sil.Const (Sil.Cfun pn), [_; (Sil.Sizeof(t, _, _), _)], _, _) when
Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t -> Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t ->
throwable_found := true throwable_found := true
| _ -> () in | _ -> () in

8
infer/src/harness/inhabit.ml
Unescape View File

@ -68,12 +68,12 @@ let get_non_receiver_formals formals = tl_or_empty formals
(** create Sil corresponding to x = new typ() or x = new typ[]. For ordinary allocation, sizeof_typ (** create Sil corresponding to x = new typ() or x = new typ[]. For ordinary allocation, sizeof_typ
* and ret_typ should be the same, but arrays are slightly odd in that sizeof_typ will have a size * and ret_typ should be the same, but arrays are slightly odd in that sizeof_typ will have a size
* component but the size component of ret_typ is always -1. *) * component but the size component of ret_typ is always -1. *)
let inhabit_alloc sizeof_typ ret_typ alloc_kind env = let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
let retval = Ident.create_fresh Ident.knormal in let retval = Ident.create_fresh Ident.knormal in
let inhabited_exp = Sil.Var retval in let inhabited_exp = Sil.Var retval in
let call_instr = let call_instr =
let fun_new = fun_exp_from_name alloc_kind in let fun_new = fun_exp_from_name alloc_kind in
let sizeof_exp = Sil.Sizeof (sizeof_typ, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (sizeof_typ, sizeof_len, Sil.Subtype.exact) in
let args = [(sizeof_exp, Sil.Tptr (ret_typ, Sil.Pk_pointer))] in let args = [(sizeof_exp, Sil.Tptr (ret_typ, Sil.Pk_pointer))] in
Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in
(inhabited_exp, env_add_instr call_instr env) (inhabited_exp, env_add_instr call_instr env)
@ -87,11 +87,11 @@ let rec inhabit_typ typ cfg env =
| Sil.Tptr (Sil.Tarray (inner_typ, Sil.Const (Sil.Cint _)), Sil.Pk_pointer) -> | Sil.Tptr (Sil.Tarray (inner_typ, Sil.Const (Sil.Cint _)), Sil.Pk_pointer) ->
let arr_size = Sil.Const (Sil.Cint (Sil.Int.one)) in let arr_size = Sil.Const (Sil.Cint (Sil.Int.one)) in
let arr_typ = Sil.Tarray (inner_typ, arr_size) in let arr_typ = Sil.Tarray (inner_typ, arr_size) in
inhabit_alloc arr_typ typ ModelBuiltins.__new_array env inhabit_alloc arr_typ (Some arr_size) typ ModelBuiltins.__new_array env
| Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ -> | Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ ->
(* TODO (t4575417): this case does not work correctly for enums, but they are currently (* TODO (t4575417): this case does not work correctly for enums, but they are currently
* broken in Infer anyway (see t4592290) *) * broken in Infer anyway (see t4592290) *)
let (allocated_obj_exp, env) = inhabit_alloc typ typ ModelBuiltins.__new env in let (allocated_obj_exp, env) = inhabit_alloc typ None typ ModelBuiltins.__new env in
(* select methods that are constructors and won't force us into infinite recursion because (* select methods that are constructors and won't force us into infinite recursion because
* we are already inhabiting one of their argument types *) * we are already inhabiting one of their argument types *)
let get_all_suitable_constructors typ = match typ with let get_all_suitable_constructors typ = match typ with

17
infer/src/java/jTrans.ml
Unescape View File

@ -645,10 +645,11 @@ let get_array_size context pc expr_list content_type =
| (other_instrs, other_exprs) -> | (other_instrs, other_exprs) ->
(instrs@other_instrs, sil_size_expr:: other_exprs) in (instrs@other_instrs, sil_size_expr:: other_exprs) in
let (instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in let (instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in
let get_array_type sil_size_expr content_type = let get_array_type_len sil_size_expr (content_type, _) =
Sil.Tarray (content_type, sil_size_expr) in (Sil.Tarray (content_type, sil_size_expr), Some sil_size_expr) in
let array_type = (IList.fold_right get_array_type sil_size_exprs content_type) in let array_type, array_len =
let array_size = Sil.Sizeof (array_type, Sil.Subtype.exact) in IList.fold_right get_array_type_len sil_size_exprs (content_type, None) in
let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in
(instrs, array_size) (instrs, array_size)
module Int = module Int =
@ -902,7 +903,7 @@ let rec instruction context pc instr : translation =
let builtin_new = Sil.Const (Sil.Cfun ModelBuiltins.__new) in let builtin_new = Sil.Const (Sil.Cfun ModelBuiltins.__new) in
let class_type = JTransType.get_class_type program tenv cn in let class_type = JTransType.get_class_type program tenv cn in
let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in
let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@ -1016,7 +1017,7 @@ let rec instruction context pc instr : translation =
and npe_cn = JBasics.make_cn JConfig.npe_cl in and npe_cn = JBasics.make_cn JConfig.npe_cl in
let class_type = JTransType.get_class_type program tenv npe_cn let class_type = JTransType.get_class_type program tenv npe_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv npe_cn in and class_type_np = JTransType.get_class_type_no_pointer program tenv npe_cn in
let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@ -1069,7 +1070,7 @@ let rec instruction context pc instr : translation =
let out_of_bound_cn = JBasics.make_cn JConfig.out_of_bound_cl in let out_of_bound_cn = JBasics.make_cn JConfig.out_of_bound_cl in
let class_type = JTransType.get_class_type program tenv out_of_bound_cn let class_type = JTransType.get_class_type program tenv out_of_bound_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv out_of_bound_cn in and class_type_np = JTransType.get_class_type_no_pointer program tenv out_of_bound_cn in
let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@ -1108,7 +1109,7 @@ let rec instruction context pc instr : translation =
and cce_cn = JBasics.make_cn JConfig.cce_cl in and cce_cn = JBasics.make_cn JConfig.cce_cl in
let class_type = JTransType.get_class_type program tenv cce_cn let class_type = JTransType.get_class_type program tenv cce_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv cce_cn in and class_type_np = JTransType.get_class_type_no_pointer program tenv cce_cn in
let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in

4
infer/src/java/jTransExn.ml
Unescape View File

@ -67,7 +67,9 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
let id_instanceof = Ident.create_fresh Ident.knormal in let id_instanceof = Ident.create_fresh Ident.knormal in
let instr_call_instanceof = let instr_call_instanceof =
let instanceof_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in let instanceof_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
let args = [(Sil.Var id_exn_val, Sil.Tptr(exn_type, Sil.Pk_pointer)); (Sil.Sizeof (exn_type, Sil.Subtype.exact), Sil.Tvoid)] in let args = [
(Sil.Var id_exn_val, Sil.Tptr(exn_type, Sil.Pk_pointer));
(Sil.Sizeof (exn_type, None, Sil.Subtype.exact), Sil.Tvoid)] in
Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in
let if_kind = Sil.Ik_switch in let if_kind = Sil.Ik_switch in
let instr_prune_true = Sil.Prune (Sil.Var id_instanceof, loc, true, if_kind) in let instr_prune_true = Sil.Prune (Sil.Var id_instanceof, loc, true, if_kind) in

8
infer/src/java/jTransType.ml
Unescape View File

@ -397,11 +397,11 @@ and value_type program tenv vt =
(** Translate object types into Sil.Sizeof expressions *) (** Translate object types into Sil.Sizeof expressions *)
let sizeof_of_object_type program tenv ot subtypes = let sizeof_of_object_type program tenv ot subtypes =
match object_type program tenv ot with match object_type program tenv ot with
| Sil.Tptr (Sil.Tarray (vtyp, s), Sil.Pk_pointer) -> | Sil.Tptr (Sil.Tarray (vtyp, len), Sil.Pk_pointer) ->
let typ = (Sil.Tarray (vtyp, s)) in let typ = (Sil.Tarray (vtyp, len)) in
Sil.Sizeof (typ, subtypes) Sil.Sizeof (typ, Some len, subtypes)
| Sil.Tptr (typ, _) -> | Sil.Tptr (typ, _) ->
Sil.Sizeof (typ, subtypes) Sil.Sizeof (typ, None, subtypes)
| _ -> | _ ->
raise (Type_tranlsation_error "Pointer or array type expected in tenv") raise (Type_tranlsation_error "Pointer or array type expected in tenv")

Write Preview
Loading…
Cancel
Save