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

[clang] add sizeof static value to translation

Browse Source 
Summary:
Modify the type of `Exp.Sizeof ...` to include the value that the expression
evaluates to according to the compiler, or None if it cannot be known
statically.

Use this information in inferbo.

Mostly unused in the BiAbduction checker for now, although it could be useful
there too.

update-submodule: facebook-clang-plugins

Reviewed By: mbouaziz

Differential Revision: D4953634

fbshipit-source-id: be0999d
master
Jules Villard 8 years ago committed by Facebook Github Bot
parent 1c23876a4e
commit 1b0ee6fbc3
37 changed files with 368 additions and 286 deletions
Show Stats Download Patch File Download Diff File

2
facebook-clang-plugins

@ -1 +1 @@
Subproject commit 21d4222b325650c67944a4ad9cc2b72c7e37fefd Subproject commit 259d4e518b31b1d8c78c744c87b5bbe4ba775882

36
infer/src/IR/Exp.re
Unescape View File

@ -22,9 +22,18 @@ type _ident = Ident.t;
let compare__ident x y => Ident.compare y x; let compare__ident x y => Ident.compare y x;
type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare] type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)}
/** dynamically determined length of an array value, if any */ /** This records information about a [sizeof(typ)] expression.
and dynamic_length = option t [@@deriving compare]
[nbytes] represents the result of the evaluation of [sizeof(typ)] if it is statically known.
If [typ] is of the form [Tarray elt (Some static_length)], then [dynamic_length] is the number
of elements of type [elt] in the array. The [dynamic_length], tracked by symbolic execution, may
differ from the [static_length] obtained from the type definition, e.g. when an array is
over-allocated.
If [typ] is a struct type, the [dynamic_length] is that of the final extensible array, if any.*/
and sizeof_data = {typ: Typ.t, nbytes: option int, dynamic_length: option t, subtype: Subtype.t}
/** Program expressions. */ /** Program expressions. */
and t = and t =
/** Pure variable: it is not an lvalue */ /** Pure variable: it is not an lvalue */
@ -47,12 +56,8 @@ and t =
| Lfield t Fieldname.t Typ.t | Lfield t Fieldname.t Typ.t
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex t t | Lindex t t
/** A sizeof expression. [Sizeof (Tarray elt (Some static_length)) (Some dynamic_length)] | Sizeof sizeof_data
represents the size of an array value consisting of [dynamic_length] elements of type [elt]. [@@deriving compare];
The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof Typ.t dynamic_length Subtype.t;
let equal = [%compare.equal : t]; let equal = [%compare.equal : t];
@ -105,7 +110,7 @@ let is_zero =
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 {typ} => typ
| _ => Typ.unsome "texp_to_typ" default_opt; | _ => Typ.unsome "texp_to_typ" default_opt;
@ -200,10 +205,8 @@ let get_vars exp => {
init::vars init::vars
captured_vars captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */ /* TODO: Sizeof dynamic length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => vars */ | Sizeof _ => vars
/* | Sizeof _ (Some l) _ => get_vars_ l vars */
| Sizeof _ _ _ => vars
}; };
get_vars_ exp ([], []) get_vars_ exp ([], [])
}; };
@ -238,9 +241,10 @@ let rec pp_ pe pp_t f e => {
| 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 Fieldname.pp fld | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Fieldname.pp 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 l s => | Sizeof {typ, nbytes, dynamic_length, subtype} =>
let pp_len f l => Option.iter f::(F.fprintf f "[%a]" pp_exp) l; let pp_len f l => Option.iter f::(F.fprintf f "[%a]" pp_exp) l;
F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s let pp_size f size => Option.iter f::(Int.pp f) size;
F.fprintf f "sizeof(%a%a%a%a)" pp_t typ pp_size nbytes pp_len dynamic_length Subtype.pp subtype
} }
}; };

22
infer/src/IR/Exp.rei
Unescape View File

@ -15,9 +15,18 @@ module L = Logging;
module F = Format; module F = Format;
type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare] type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)}
/** dynamically determined length of an array value, if any */ /** This records information about a [sizeof(typ)] expression.
and dynamic_length = option t [@@deriving compare]
[nbytes] represents the result of the evaluation of [sizeof(typ)] if it is statically known.
If [typ] is of the form [Tarray elt (Some static_length)], then [dynamic_length] is the number
of elements of type [elt] in the array. The [dynamic_length], tracked by symbolic execution, may
differ from the [static_length] obtained from the type definition, e.g. when an array is
over-allocated.
If [typ] is a struct type, the [dynamic_length] is that of the final extensible array, if any.*/
and sizeof_data = {typ: Typ.t, nbytes: option int, dynamic_length: option t, subtype: Subtype.t}
/** Program expressions. */ /** Program expressions. */
and t = and t =
/** Pure variable: it is not an lvalue */ /** Pure variable: it is not an lvalue */
@ -40,12 +49,7 @@ and t =
| Lfield t Fieldname.t Typ.t | Lfield t Fieldname.t Typ.t
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex t t | Lindex t t
/** A sizeof expression. [Sizeof (Tarray elt (Some static_length)) (Some dynamic_length)] | Sizeof sizeof_data
represents the size of an array value consisting of [dynamic_length] elements of type [elt].
The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof Typ.t dynamic_length Subtype.t
[@@deriving compare]; [@@deriving compare];

4
infer/src/IR/HilExp.ml
Unescape View File

@ -76,8 +76,8 @@ let rec of_sil ~f_resolve_id (exp : Exp.t) typ = match exp with
Constant c Constant c
| Cast (cast_typ, e) -> | Cast (cast_typ, e) ->
Cast (cast_typ, of_sil ~f_resolve_id e typ) Cast (cast_typ, of_sil ~f_resolve_id e typ)
| Sizeof (sizeof_typ, dynamic_length, _) -> | Sizeof {typ; dynamic_length} ->
Sizeof (sizeof_typ, Option.map ~f:(fun e -> of_sil ~f_resolve_id e typ) dynamic_length) Sizeof (typ, Option.map ~f:(fun e -> of_sil ~f_resolve_id e typ) dynamic_length)
| Closure closure -> | Closure closure ->
let environment = let environment =
List.map List.map

2
infer/src/IR/HilInstr.ml
Unescape View File

@ -61,7 +61,7 @@ let of_sil ~f_resolve_id (instr : Sil.instr) =
when Pvar.is_ssa_frontend_tmp lhs_pvar -> when Pvar.is_ssa_frontend_tmp lhs_pvar ->
analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc
| Call (Some (ret_id, _), Const (Cfun callee_pname), | Call (Some (ret_id, _), Const (Cfun callee_pname),
(target_exp, _) :: (Sizeof (cast_typ, _, _), _) :: _ , loc, _) (target_exp, _) :: (Sizeof {typ=cast_typ}, _) :: _ , loc, _)
when Typ.Procname.equal callee_pname BuiltinDecl.__cast -> when Typ.Procname.equal callee_pname BuiltinDecl.__cast ->
analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc
| Store (lhs_exp, typ, rhs_exp, loc) -> | Store (lhs_exp, typ, rhs_exp, loc) ->

4
infer/src/IR/Localise.ml
Unescape View File

@ -771,7 +771,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
MF.monospaced_to_string s, " to ", " on " in MF.monospaced_to_string s, " to ", " on " in
let typ_str = let typ_str =
match hpred_type_opt with match hpred_type_opt with
| Some (Exp.Sizeof ({desc=Tstruct name}, _, _)) when Typ.Name.is_class name -> | Some (Exp.Sizeof {typ={desc=Tstruct name}}) when Typ.Name.is_class name ->
" of type " ^ MF.monospaced_to_string (Typ.Name.name name) ^ " " " of type " ^ MF.monospaced_to_string (Typ.Name.name name) ^ " "
| _ -> " " in | _ -> " " in
let desc_str = let desc_str =
@ -861,7 +861,7 @@ let desc_retain_cycle cycle loc cycle_dotty =
str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining " ^ str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining " ^
MF.monospaced_to_string (e_str^"."^(Fieldname.to_string f))^", "; MF.monospaced_to_string (e_str^"."^(Fieldname.to_string f))^", ";
ct:=!ct +1 ct:=!ct +1
| Sil.Eexp (Exp.Sizeof (typ, _, _), _) -> | Sil.Eexp (Exp.Sizeof {typ}, _) ->
let step = let step =
" (" ^ (string_of_int !ct) ^ ") an object of " ^ " (" ^ (string_of_int !ct) ^ ") an object of " ^
MF.monospaced_to_string (Typ.to_string typ) ^ MF.monospaced_to_string (Typ.to_string typ) ^

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

@ -229,7 +229,7 @@ let hpred_get_lhs h =>
/** {2 Comparision and Inspection Functions} */ /** {2 Comparision and Inspection Functions} */
let has_objc_ref_counter tenv hpred => let has_objc_ref_counter tenv hpred =>
switch hpred { switch hpred {
| Hpointsto _ _ (Sizeof {desc: Tstruct name} _ _) => | Hpointsto _ _ (Sizeof {typ: {desc: Tstruct name}}) =>
switch (Tenv.lookup tenv name) { switch (Tenv.lookup tenv name) {
| Some {fields} => List.exists f::Typ.Struct.is_objc_ref_counter_field fields | Some {fields} => List.exists f::Typ.Struct.is_objc_ref_counter_field fields
| _ => false | _ => false
@ -383,9 +383,11 @@ let d_exp_list (el: list Exp.t) => L.add_print_action (L.PTexp_list, Obj.repr el
let pp_texp pe f => let pp_texp pe f =>
fun fun
| Exp.Sizeof t l s => { | Exp.Sizeof {typ, nbytes, dynamic_length, subtype} => {
let pp_len f l => Option.iter f::(F.fprintf f "[%a]" (pp_exp_printenv pe)) l; let pp_len f l => Option.iter f::(F.fprintf f "[%a]" (pp_exp_printenv pe)) l;
F.fprintf f "%a%a%a" (Typ.pp pe) t pp_len l Subtype.pp s let pp_size f size => Option.iter f::(Int.pp f) size;
F.fprintf
f "%a%a%a%a" (Typ.pp pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp subtype
} }
| e => (pp_exp_printenv pe) f e; | e => (pp_exp_printenv pe) f e;
@ -393,9 +395,11 @@ let pp_texp pe f =>
/** 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
| Exp.Sizeof t l s => { | Exp.Sizeof {typ, nbytes, dynamic_length, subtype} => {
let pp_len f l => Option.iter f::(F.fprintf f "[%a]" (pp_exp_printenv pe)) l; let pp_len f l => Option.iter f::(F.fprintf f "[%a]" (pp_exp_printenv pe)) l;
F.fprintf f "%a%a%a" (Typ.pp_full pe) t pp_len l Subtype.pp s let pp_size f size => Option.iter f::(Int.pp f) size;
F.fprintf
f "%a%a%a%a" (Typ.pp_full pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp subtype
} }
| e => Exp.pp_printenv pe Typ.pp_full f e; | e => Exp.pp_printenv pe Typ.pp_full f e;
@ -1246,9 +1250,7 @@ let rec exp_fpv e =>
| 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
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */ /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => [] */ | Sizeof _ => []
/* | Sizeof _ (Some l) _ => exp_fpv l */
| Sizeof _ _ _ => []
}; };
let exp_list_fpv el => List.concat_map f::exp_fpv el; let exp_list_fpv el => List.concat_map f::exp_fpv el;
@ -1443,9 +1445,7 @@ let rec exp_fav_add fav e =>
exp_fav_add fav e1; exp_fav_add fav e1;
exp_fav_add fav e2 exp_fav_add fav e2
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */ /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => () */ | Sizeof _ => ()
/* | 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;
@ -1878,17 +1878,14 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
} else { } else {
Exp.Lindex e1' e2' Exp.Lindex e1' e2'
} }
| Sizeof t l_opt s => | Sizeof ({dynamic_length: Some l} as sizeof_data) =>
switch l_opt { let l' = exp_sub_ids f l;
| Some l => if (phys_equal l' l) {
let l' = exp_sub_ids f l; exp
if (phys_equal l' l) { } else {
exp Exp.Sizeof {...sizeof_data, dynamic_length: Some l'}
} else {
Exp.Sizeof t (Some l') s
}
| None => exp
} }
| Sizeof {dynamic_length: None} => exp
}; };
let rec apply_sub subst id => let rec apply_sub subst id =>
@ -2353,8 +2350,8 @@ let exp_get_offsets exp => {
| Exn _ | Exn _
| Closure _ | Closure _
| Lvar _ | Lvar _
| Sizeof _ None _ => offlist_past | Sizeof {dynamic_length: None} => offlist_past
| Sizeof _ (Some l) _ => f offlist_past l | Sizeof {dynamic_length: 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

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

@ -243,8 +243,8 @@ let find_arithmetic_problem tenv proc_node_session prop exp =
| Exp.Lvar _ -> () | Exp.Lvar _ -> ()
| Exp.Lfield (e, _, _) -> walk e | Exp.Lfield (e, _, _) -> walk e
| Exp.Lindex (e1, e2) -> walk e1; walk e2 | Exp.Lindex (e1, e2) -> walk e1; walk e2
| Exp.Sizeof (_, None, _) -> () | Exp.Sizeof {dynamic_length=None} -> ()
| Exp.Sizeof (_, Some len, _) -> walk len in | Exp.Sizeof {dynamic_length=Some len} -> walk len in
walk exp; walk exp;
let problem_opt = let problem_opt =
match (List.find ~f:check_zero !exps_divided, !uminus_unsigned) with match (List.find ~f:check_zero !exps_divided, !uminus_unsigned) with

35
infer/src/backend/BuiltinDefn.ml
Unescape View File

@ -79,7 +79,8 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
let len = Exp.Var (Ident.create_fresh Ident.kfootprint) in let len = Exp.Var (Ident.create_fresh Ident.kfootprint) in
let s = mk_empty_array_rearranged len in let s = mk_empty_array_rearranged len in
let hpred = let hpred =
Prop.mk_ptsto tenv n_lexp s (Exp.Sizeof (arr_typ, Some len, Subtype.exact)) in Prop.mk_ptsto tenv n_lexp s (Exp.Sizeof {typ=arr_typ; nbytes=None;
dynamic_length=None; subtype=Subtype.exact}) in
let sigma = prop.Prop.sigma in let sigma = prop.Prop.sigma in
let sigma_fp = prop.Prop.sigma_fp in let sigma_fp = prop.Prop.sigma_fp in
let prop'= Prop.set prop ~sigma:(hpred:: sigma) in let prop'= Prop.set prop ~sigma:(hpred:: sigma) in
@ -158,13 +159,15 @@ let create_type tenv n_lexp typ prop =
match typ.Typ.desc with match typ.Typ.desc with
| Typ.Tptr (typ', _) -> | Typ.Tptr (typ', _) ->
let sexp = Sil.Estruct ([], Sil.inst_none) in let sexp = Sil.Estruct ([], Sil.inst_none) in
let texp = Exp.Sizeof (typ', None, Subtype.subtypes) in let texp = Exp.Sizeof {typ=typ'; nbytes=None;
dynamic_length=None; subtype=Subtype.subtypes} in
let hpred = Prop.mk_ptsto tenv n_lexp sexp texp in let hpred = Prop.mk_ptsto tenv n_lexp sexp texp in
Some hpred Some hpred
| Typ.Tarray _ -> | Typ.Tarray _ ->
let len = Exp.Var (Ident.create_fresh Ident.kfootprint) in let len = Exp.Var (Ident.create_fresh Ident.kfootprint) in
let sexp = mk_empty_array len in let sexp = mk_empty_array len in
let texp = Exp.Sizeof (typ, None, Subtype.subtypes) in let texp = Exp.Sizeof {typ; nbytes=None;
dynamic_length=None; subtype=Subtype.subtypes} in
let hpred = Prop.mk_ptsto tenv n_lexp sexp texp in let hpred = Prop.mk_ptsto tenv n_lexp sexp texp in
Some hpred Some hpred
| _ -> None in | _ -> None in
@ -553,7 +556,7 @@ let execute___release_autorelease_pool
| Sil.Hpointsto(e1, _, _) -> Exp.equal e1 exp | Sil.Hpointsto(e1, _, _) -> Exp.equal e1 exp
| _ -> false) prop_.Prop.sigma |> | _ -> false) prop_.Prop.sigma |>
Option.value_map ~f:(function Option.value_map ~f:(function
| Sil.Hpointsto (_, _, Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, _, Exp.Sizeof {typ}) ->
let res1 = let res1 =
execute___objc_release execute___objc_release
{ builtin_args with { builtin_args with
@ -750,18 +753,19 @@ let execute_alloc mk can_return_null
Exp.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2') Exp.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2')
| Exp.Exn _ | Exp.Closure _ | Exp.Const _ | Exp.Cast _ | Exp.Lvar _ | Exp.Lfield _ | Exp.Exn _ | Exp.Closure _ | Exp.Const _ | Exp.Cast _ | Exp.Lvar _ | Exp.Lfield _
| Exp.Lindex _ -> e | Exp.Lindex _ -> e
| Exp.Sizeof ({Typ.desc=Tarray ({Typ.desc=Tint ik}, _)}, Some len, _) when Typ.ikind_is_char ik -> | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, _)}; dynamic_length=Some len}
when Typ.ikind_is_char ik ->
evaluate_char_sizeof len evaluate_char_sizeof len
| Exp.Sizeof ({Typ.desc=Tarray ({Typ.desc=Tint ik}, Some len)}, None, _) when Typ.ikind_is_char ik -> | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, Some len)}; dynamic_length=None}
when Typ.ikind_is_char ik ->
evaluate_char_sizeof (Exp.Const (Const.Cint len)) evaluate_char_sizeof (Exp.Const (Const.Cint len))
| Exp.Sizeof _ -> e in | Exp.Sizeof _ -> e in
let size_exp, procname = match args with let size_exp, procname = match args with
| [(Exp.Sizeof ({Typ.desc=Tstruct (ObjcClass _ as name)} as s, len, subt), _)] -> | [(Exp.Sizeof ({typ={Typ.desc=Tstruct (ObjcClass _ as name)}} as sizeof_data) as e, _)] ->
let struct_type = let e' = match AttributesTable.get_correct_type_from_objc_class_name name with
match AttributesTable.get_correct_type_from_objc_class_name name with | Some struct_type -> Exp.Sizeof {sizeof_data with typ=struct_type}
| Some struct_type -> struct_type | None -> e in
| None -> s in e', pname
Exp.Sizeof (struct_type, len, subt), pname
| [(size_exp, _)] -> (* for malloc and __new *) | [(size_exp, _)] -> (* for malloc and __new *)
size_exp, PredSymb.mem_alloc_pname mk size_exp, PredSymb.mem_alloc_pname mk
| [(size_exp, _); (Exp.Const (Const.Cfun pname), _)] -> | [(size_exp, _); (Exp.Const (Const.Cfun pname), _)] ->
@ -776,7 +780,8 @@ let execute_alloc mk can_return_null
let n_size_exp' = evaluate_char_sizeof n_size_exp in let n_size_exp' = evaluate_char_sizeof n_size_exp in
Prop.exp_normalize_prop tenv prop n_size_exp', prop in Prop.exp_normalize_prop tenv prop n_size_exp', prop in
let cnt_te = let cnt_te =
Exp.Sizeof (Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None)), Some size_exp', Subtype.exact) in Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None));
nbytes=None; dynamic_length=Some size_exp'; subtype=Subtype.exact} in
let id_new = Ident.create_fresh Ident.kprimed in let id_new = Ident.create_fresh Ident.kprimed in
let exp_new = Exp.Var id_new in let exp_new = Exp.Var id_new in
let ptsto_new = let ptsto_new =
@ -811,7 +816,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
| Sil.Hpointsto (e, _, _) -> Exp.equal e n_lexp | Sil.Hpointsto (e, _, _) -> Exp.equal e n_lexp
| _ -> false) prop.Prop.sigma |> | _ -> false) prop.Prop.sigma |>
Option.value_map ~f:(function Option.value_map ~f:(function
| Sil.Hpointsto (_, _, Exp.Sizeof (dynamic_type, _, _)) -> dynamic_type | Sil.Hpointsto (_, _, Exp.Sizeof {typ}) -> typ
| _ -> typ_ | _ -> typ_
) )
~default:typ_ in ~default:typ_ in
@ -954,7 +959,7 @@ let execute_objc_alloc_no_fail
{ Builtin.pdesc; tenv; ret_id; loc; } = { Builtin.pdesc; tenv; ret_id; loc; } =
let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in
let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in
let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_typ = Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact} in
let alloc_fun_exp = let alloc_fun_exp =
match alloc_fun_opt with match alloc_fun_opt with
| Some pname -> [Exp.Const (Const.Cfun pname), Typ.mk Tvoid] | Some pname -> [Exp.Const (Const.Cfun pname), Typ.mk Tvoid]

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

@ -416,7 +416,7 @@ let typ_get_recursive_flds tenv typ_exp =
false false
in in
match typ_exp with match typ_exp with
| Exp.Sizeof (typ, _, _) -> ( | Exp.Sizeof {typ} -> (
match typ.desc with match typ.desc with
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
@ -900,14 +900,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, _), Exp.Sizeof (te, _, _))) -> | Some (Sil.Hpointsto (_, Sil.Estruct (fl, _), Exp.Sizeof {typ=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, _), Exp.Sizeof (te, _, _)) -> | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ=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
@ -926,7 +926,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( (Exp.Const (Const.Cint i)), _)):: _, _), | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Exp.Const (Const.Cint i)), _)):: _, _),
Exp.Sizeof (typ, _, _)) Exp.Sizeof {typ})
when Fieldname.is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) -> when Fieldname.is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) ->
Mleak_buckets.should_raise_objc_leak typ Mleak_buckets.should_raise_objc_leak typ
| _ -> None | _ -> None
@ -946,7 +946,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, _, Exp.Sizeof (typ, _, _)), Sil.Eexp (e', _) | Sil.Hpointsto (e, _, Exp.Sizeof {typ}), Sil.Eexp (e', _)
when Exp.equal e e' && Typ.is_block_type typ -> true when Exp.equal e e' && Typ.is_block_type typ -> true
| _, _ -> false in | _, _ -> false in
let find v = let find v =
@ -962,7 +962,9 @@ 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 (Exp.Sizeof (t, None, Subtype.exact)), t), f, e')]) in | _ ->
let sizeof = {Exp.typ=t; nbytes=None; dynamic_length=None; subtype=Subtype.exact} in
[((sexp (Exp.Sizeof sizeof), 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

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

@ -834,10 +834,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
Exp.Lindex(e1', e2') Exp.Lindex(e1', e2')
| Exp.Sizeof (_, None, _) -> | Exp.Sizeof {dynamic_length=None} ->
e e
| Exp.Sizeof (typ, Some len, st) -> | Exp.Sizeof ({dynamic_length=Some len} as sizeof) ->
Exp.Sizeof (typ, Some (exp_construct_fresh side len), st) Exp.Sizeof {sizeof with dynamic_length=Some (exp_construct_fresh side len)}
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
@ -971,9 +971,16 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t =
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
Exp.Lindex(e1'', e2'') Exp.Lindex(e1'', e2'')
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, len2, st2) -> | Exp.Sizeof {typ=t1; nbytes=nbytes1; dynamic_length=len1; subtype=st1},
Exp.Sizeof Exp.Sizeof {typ=t2; nbytes=nbytes2; dynamic_length=len2; subtype=st2} ->
(typ_partial_join t1 t2, dynamic_length_partial_join len1 len2, Subtype.join st1 st2) (* forget the static sizes if they differ *)
let nbytes_join i1 i2 = if Int.equal i1 i2 then Some i1 else None in
Exp.Sizeof {
typ=typ_partial_join t1 t2;
nbytes=option_partial_join nbytes_join nbytes1 nbytes2;
dynamic_length=dynamic_length_partial_join len1 len2;
subtype=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 Sil.JoinFail raise Sil.JoinFail

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

@ -298,11 +298,13 @@ 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, _), Exp.Sizeof ({Typ.desc=Tarray (t, _)}, _, _)), lambda) -> | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ={Typ.desc=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
[Dotpointsto((mk_coordinate n lambda), e, e_color_str); Dotarray((mk_coordinate (n + 1) lambda), e, e', l, t, e_color_str')] [Dotpointsto((mk_coordinate n lambda), e, e_color_str);
Dotarray((mk_coordinate (n + 1) lambda), e, e', l, t, e_color_str')]
| (Sil.Hpointsto (e, Sil.Estruct (l, _), te), lambda) -> | (Sil.Hpointsto (e, Sil.Estruct (l, _), te), lambda) ->
incr dotty_state_count; (* increment once more n+1 is the box for the struct *) incr dotty_state_count; (* increment once more n+1 is the box for the struct *)
let e_color_str = color_to_str (exp_color e) in let e_color_str = color_to_str (exp_color e) in
@ -692,8 +694,8 @@ 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
| Exp.Sizeof (t, _, _) -> | Exp.Sizeof {typ} ->
let str_t = Typ.to_string t in let str_t = Typ.to_string typ 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"
| _ -> str_t) | _ -> str_t)

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

@ -407,9 +407,9 @@ and _exp_rv_dexp tenv (_seen : Exp.Set.t) node e : DExp.t option =
| Exp.Cast (_, e1) -> | Exp.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 tenv seen node e1 _exp_rv_dexp tenv seen node e1
| Exp.Sizeof (typ, len, sub) -> | Exp.Sizeof {typ; dynamic_length; subtype} ->
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 (DExp.Dsizeof (typ, Option.bind len (_exp_rv_dexp tenv seen node), sub)) Some (DExp.Dsizeof (typ, Option.bind dynamic_length (_exp_rv_dexp tenv seen node), subtype))
| _ -> | _ ->
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
@ -511,9 +511,9 @@ 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 (Exp.Sizeof (t1, _, _)), Some (Exp.Sizeof ({Typ.desc=Tptr (t2, _)}, _, _)) -> | Some (Exp.Sizeof {typ=t1}), Some (Exp.Sizeof {typ={Typ.desc=Tptr (t2, _)}}) ->
Typ.equal t1 t2 Typ.equal t1 t2
| Some (Exp.Sizeof ({Typ.desc=Tint _}, _, _)), Some (Exp.Sizeof ({Typ.desc=Tint _}, _, _)) | Some (Exp.Sizeof {typ={Typ.desc=Tint _}}), Some (Exp.Sizeof {typ={Typ.desc=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
@ -581,7 +581,7 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option =
(match lexp with (match lexp with
| Exp.Lvar pv -> | Exp.Lvar pv ->
let typo = match texp with let typo = match texp with
| Exp.Sizeof ({Typ.desc=Tstruct name}, _, _) -> ( | Exp.Sizeof {typ={Typ.desc=Tstruct name}} -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some {fields} -> | Some {fields} ->
List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) fields |> List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) fields |>
@ -607,7 +607,7 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option =
(match lexp with (match lexp with
| Exp.Lvar pv when not (Pvar.is_frontend_tmp pv) -> | Exp.Lvar pv when not (Pvar.is_frontend_tmp pv) ->
let typo = match texp with let typo = match texp with
| Exp.Sizeof (typ, _, _) -> Some typ | Exp.Sizeof {typ} -> Some typ
| _ -> None in | _ -> None in
Some (DExp.Dpvar pv), typo Some (DExp.Dpvar pv), typo
| Exp.Var id -> | Exp.Var id ->

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

@ -621,13 +621,13 @@ let get_fld_typ_path_opt src_exps sink_exp_ reachable_hpreds_ =
| Sil.Eexp (e, _) -> Exp.equal target_exp e | Sil.Eexp (e, _) -> Exp.equal target_exp e
| _ -> false in | _ -> false in
let extend_path hpred (sink_exp, path, reachable_hpreds) = match hpred with let extend_path hpred (sink_exp, path, reachable_hpreds) = match hpred with
| Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Exp.Sizeof {typ}) ->
List.find ~f:(function _, se -> strexp_matches sink_exp se) flds |> List.find ~f:(function _, se -> strexp_matches sink_exp se) flds |>
Option.value_map ~f:(function fld, _ -> Option.value_map ~f:(function fld, _ ->
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'))
~default:(sink_exp, path, reachable_hpreds) ~default:(sink_exp, path, reachable_hpreds)
| Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Exp.Sizeof {typ}) ->
if List.exists ~f:(function _, se -> strexp_matches sink_exp se) elems if List.exists ~f:(function _, se -> strexp_matches sink_exp se) elems
then then
let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
@ -672,7 +672,7 @@ let report_context_leaks pname sigma tenv =
let context_exps = let context_exps =
List.fold List.fold
~f:(fun exps hpred -> match hpred with ~f:(fun exps hpred -> match hpred with
| Sil.Hpointsto (_, Eexp (exp, _), Sizeof ({desc=Tptr ({desc=Tstruct name}, _)}, _, _)) | Sil.Hpointsto (_, Eexp (exp, _), Sizeof {typ={desc=Tptr ({desc=Tstruct name}, _)}})
when not (Exp.is_null_literal exp) when not (Exp.is_null_literal exp)
&& AndroidFramework.is_context tenv name && AndroidFramework.is_context tenv name
&& not (AndroidFramework.is_application tenv name) -> && not (AndroidFramework.is_application tenv name) ->
@ -853,8 +853,10 @@ 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 -> Exp.Sizeof (typ, None, Subtype.exact) | Config.Clang ->
| Config.Java -> Exp.Sizeof (typ, None, Subtype.subtypes) in Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact}
| Config.Java ->
Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.subtypes} in
Prop.mk_ptsto_lvar tenv Prop.Fld_init Sil.inst_formal (pv, texp, None) in Prop.mk_ptsto_lvar tenv Prop.Fld_init Sil.inst_formal (pv, texp, None) in
List.map ~f:do_formal new_formals in List.map ~f:do_formal new_formals in
let sigma_seed = let sigma_seed =

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

@ -529,7 +529,7 @@ let rec pi_sorted_remove_redundant (pi : pi) = match pi with
let sigma_get_unsigned_exps sigma = let sigma_get_unsigned_exps sigma =
let uexps = ref [] in let uexps = ref [] in
let do_hpred (hpred : Sil.hpred) = match hpred with let do_hpred (hpred : Sil.hpred) = match hpred with
| Hpointsto (_, Eexp (e, _), Sizeof ({desc=Tint ik}, _, _)) | Hpointsto (_, Eexp (e, _), Sizeof {typ={desc=Tint ik}})
when Typ.ikind_is_unsigned ik -> when Typ.ikind_is_unsigned ik ->
uexps := e :: !uexps uexps := e :: !uexps
| _ -> () in | _ -> () in
@ -712,10 +712,10 @@ module Normalize = struct
Closure { c with captured_vars; } Closure { c with captured_vars; }
| Const _ -> | Const _ ->
e e
| Sizeof ({desc=Tarray ({desc=Tint ik}, _)}, Some l, _) | Sizeof {typ={desc=Tarray ({desc=Tint ik}, _)}; dynamic_length=Some l}
when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang ->
eval l eval l
| Sizeof ({desc=Tarray ({desc=Tint ik}, Some l)}, _, _) | Sizeof {typ={desc=Tarray ({desc=Tint ik}, Some l)}}
when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang ->
Const (Cint l) Const (Cint l)
| Sizeof _ -> | Sizeof _ ->
@ -876,11 +876,11 @@ module Normalize = struct
match e1', e2' with match e1', e2' with
(* pattern for arrays and extensible structs: (* pattern for arrays and extensible structs:
sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *) sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *)
| Sizeof (typ, len1_opt, st), | Sizeof ({typ; dynamic_length=len1_opt} as sizeof_data),
BinOp (Mult, len2, Sizeof (elt, None, _)) BinOp (Mult, len2, Sizeof {typ=elt; dynamic_length=None})
when isPlusA && (extensible_array_element_typ_equal elt typ) -> when isPlusA && (extensible_array_element_typ_equal elt typ) ->
let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
Sizeof (typ, Some len, st) Sizeof {sizeof_data with dynamic_length=Some len}
| Const c, _ when Const.iszero_int_float c -> | Const c, _ when Const.iszero_int_float c ->
e2' e2'
| _, Const c when Const.iszero_int_float c -> | _, Const c when Const.iszero_int_float c ->
@ -991,11 +991,13 @@ module Normalize = struct
Exp.int (IntLit.div n m) Exp.int (IntLit.div n m)
| Const (Cfloat v), Const (Cfloat w) -> | Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v /.w) Exp.float (v /.w)
| Sizeof ({desc=Tarray (elt, _)}, Some len, _), Sizeof (elt2, None, _) | Sizeof {typ={desc=Tarray (elt, _)}; dynamic_length=Some len},
Sizeof {typ=elt2; dynamic_length=None}
(* pattern: sizeof(elt[len]) / sizeof(elt) = len *) (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
when Typ.equal elt elt2 -> when Typ.equal elt elt2 ->
len len
| Sizeof ({desc=Tarray (elt, Some len)}, None, _), Sizeof (elt2, None, _) | Sizeof {typ={desc=Tarray (elt, Some len)}; dynamic_length=None},
Sizeof {typ=elt2; dynamic_length=None}
(* pattern: sizeof(elt[len]) / sizeof(elt) = len *) (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
when Typ.equal elt elt2 -> when Typ.equal elt elt2 ->
Const (Cint len) Const (Cint len)
@ -1101,8 +1103,9 @@ module Normalize = struct
else sym_eval tenv false exp' else sym_eval tenv false exp'
let texp_normalize tenv sub (exp : Exp.t) : Exp.t = match exp with let texp_normalize tenv sub (exp : Exp.t) : Exp.t = match exp with
| Sizeof (typ, len, st) -> | Sizeof ({dynamic_length} as sizeof_data) ->
Sizeof (typ, Option.map ~f:(exp_normalize tenv sub) len, st) Sizeof {sizeof_data with
dynamic_length=Option.map ~f:(exp_normalize tenv sub) dynamic_length}
| _ -> | _ ->
exp_normalize tenv sub exp exp_normalize tenv sub exp
@ -1348,8 +1351,8 @@ module Normalize = struct
initialize the fields of structs with fresh variables. *) initialize the fields of structs with fresh variables. *)
let mk_ptsto_exp tenv struct_init_mode (exp, (te : Exp.t), expo) inst : Sil.hpred = let mk_ptsto_exp tenv struct_init_mode (exp, (te : Exp.t), expo) inst : Sil.hpred =
let default_strexp () : Sil.strexp = match te with let default_strexp () : Sil.strexp = match te with
| Sizeof (typ, len, _) -> | Sizeof {typ; dynamic_length} ->
create_strexp_of_type tenv struct_init_mode typ len inst create_strexp_of_type tenv struct_init_mode typ dynamic_length inst
| Var _ -> | Var _ ->
Estruct ([], inst) Estruct ([], inst)
| te -> | te ->
@ -1372,30 +1375,37 @@ module Normalize = struct
let normalized_cnt = strexp_normalize tenv sub cnt in let normalized_cnt = strexp_normalize tenv sub cnt in
let normalized_te = texp_normalize tenv sub te in let normalized_te = texp_normalize tenv sub te in
begin match normalized_cnt, normalized_te with begin match normalized_cnt, normalized_te with
| Earray (Exp.Sizeof _ as size, [], inst), Sizeof ({desc=Tarray _}, _, _) -> | Earray (Exp.Sizeof _ as size, [], inst), Sizeof {typ={desc=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 tenv Fld_init (root, size, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in
replace_hpred hpred' replace_hpred hpred'
| Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst), | Earray (BinOp (Mult, Sizeof {typ=t; dynamic_length=None; subtype=st1}, x), esel, inst),
Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt -> Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal t elt ->
let len = Some x in let dynamic_length = Some x in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length; subtype=st1} in
let hpred' =
mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst), | Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length=None; subtype}), esel, inst),
Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt -> Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt ->
let len = Some x in let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length=Some x; subtype} in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let hpred' =
mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst), | Earray (BinOp (Mult, Sizeof {typ; dynamic_length=Some len; subtype}, x), esel, inst),
Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt -> Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt ->
let len = Some (Exp.BinOp(Mult, x, len)) in let sizeof_data = {Exp.typ=arr; nbytes=None;
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in dynamic_length=Some (Exp.BinOp(Mult, x, len)); subtype} in
let hpred' =
mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst), | Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length=Some len; subtype}), esel, inst),
Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt -> Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt ->
let len = Some (Exp.BinOp(Mult, x, len)) in let sizeof_data = {Exp.typ=arr; nbytes=None;
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in dynamic_length=Some (Exp.BinOp(Mult, x, len)); subtype} in
let hpred' =
mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| _ -> | _ ->
Hpointsto (normalized_root, normalized_cnt, normalized_te) Hpointsto (normalized_root, normalized_cnt, normalized_te)
@ -1986,8 +1996,8 @@ let rec exp_captured_ren ren (e : Exp.t) : Exp.t = match e with
e (* TODO: why captured vars not renamed? *) e (* TODO: why captured vars not renamed? *)
| Const _ -> | Const _ ->
e e
| Sizeof (t, len, st) -> | Sizeof ({dynamic_length} as sizeof_data) ->
Sizeof (t, Option.map ~f:(exp_captured_ren ren) len, st) Sizeof {sizeof_data with dynamic_length=Option.map ~f:(exp_captured_ren ren) dynamic_length}
| Cast (t, e) -> | Cast (t, e) ->
Cast (t, exp_captured_ren ren e) Cast (t, exp_captured_ren ren e)
| UnOp (op, e, topt) -> | UnOp (op, e, topt) ->

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

@ -383,7 +383,7 @@ end = struct
| Some {Typ.desc=Tint ik} -> Typ.ikind_is_unsigned ik | Some {Typ.desc=Tint ik} -> Typ.ikind_is_unsigned ik
| _ -> false in | _ -> false in
let type_of_texp = function let type_of_texp = function
| Exp.Sizeof (t, _, _) -> Some t | Exp.Sizeof {typ} -> Some typ
| _ -> None in | _ -> None in
let texp_is_unsigned texp = type_opt_is_unsigned @@ type_of_texp texp in let texp_is_unsigned texp = type_opt_is_unsigned @@ type_of_texp texp in
let strexp_lt_minus1 = function let strexp_lt_minus1 = function
@ -436,7 +436,9 @@ 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
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) -> IntLit.leq n1 n2 | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) -> IntLit.leq n1 n2
| Exp.BinOp (Binop.MinusA, Exp.Sizeof (t1, None, _), Exp.Sizeof (t2, None, _)), | Exp.BinOp (Binop.MinusA,
Exp.Sizeof {typ=t1; dynamic_length=None},
Exp.Sizeof {typ=t2; dynamic_length=None}),
Exp.Const(Const.Cint n2) Exp.Const(Const.Cint n2)
when IntLit.isminusone n2 && type_size_comparable t1 t2 -> when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
(* [ sizeof(t1) - sizeof(t2) <= -1 ] *) (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
@ -1220,9 +1222,11 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA, e2, e1)) do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA, e2, e1))
| Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 -> | Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 ->
do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA, e2, e1)) do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA, e2, e1))
| Exp.Sizeof (t1, None, st1), Exp.Sizeof (t2, None, st2) | Exp.Sizeof {typ=t1; dynamic_length=None; subtype=st1},
Exp.Sizeof {typ=t2; dynamic_length=None; subtype=st2}
when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 -> subs when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 -> subs
| Exp.Sizeof (t1, Some d1, st1), Exp.Sizeof (t2, Some d2, st2) | Exp.Sizeof {typ=t1; dynamic_length=Some d1; subtype=st1},
Exp.Sizeof {typ=t2; dynamic_length=Some d2; subtype=st2}
when Typ.equal t1 t2 && Exp.equal d1 d2 && Subtype.equal_modulo_flag st1 st2 -> subs when Typ.equal t1 t2 && Exp.equal d1 d2 && Subtype.equal_modulo_flag st1 st2 -> subs
| e', Exp.Const (Const.Cint n) | e', Exp.Const (Const.Cint n)
when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero -> when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero ->
@ -1504,7 +1508,8 @@ let expand_hpred_pointer =
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some _ -> | Some _ ->
(* type of struct at adr_base is known *) (* type of struct at adr_base is known *)
Some (Exp.Sizeof (adr_typ, None, Subtype.exact)) Some (Exp.Sizeof {typ=adr_typ; nbytes=None;
dynamic_length=None; subtype=Subtype.exact})
| None -> None | None -> None
) )
| _ -> None | _ -> None
@ -1512,14 +1517,14 @@ let expand_hpred_pointer =
| Some se -> se | Some se -> se
| None -> | None ->
match cnt_texp with match cnt_texp with
| Sizeof (cnt_typ, len, st) -> | Sizeof ({typ=cnt_typ} as sizeof_data) ->
(* type of struct at adr_base is unknown (typically Tvoid), but (* type of struct at adr_base is unknown (typically Tvoid), but
type of contents is known, so construct struct type for single fld:cnt_typ *) type of contents is known, so construct struct type for single fld:cnt_typ *)
let name = Typ.Name.C.from_string ("counterfeit" ^ string_of_int !count) in let name = Typ.Name.C.from_string ("counterfeit" ^ string_of_int !count) in
incr count ; incr count ;
let fields = [(fld, cnt_typ, Annot.Item.empty)] in let fields = [(fld, cnt_typ, Annot.Item.empty)] in
ignore (Tenv.mk_struct tenv ~fields name) ; ignore (Tenv.mk_struct tenv ~fields name) ;
Exp.Sizeof (Typ.mk (Tstruct name), len, st) Exp.Sizeof {sizeof_data with typ=Typ.mk (Tstruct name)}
| _ -> | _ ->
(* type of struct at adr_base and of contents are both unknown: give up *) (* type of struct at adr_base and of contents are both unknown: give up *)
raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
@ -1527,10 +1532,11 @@ let expand_hpred_pointer =
expand true true hpred' expand true true hpred'
| Sil.Hpointsto (Exp.Lindex (e, ind), se, t) -> | Sil.Hpointsto (Exp.Lindex (e, ind), se, t) ->
let t' = match t with let t' = match t with
| Exp.Sizeof (t_, len, st) -> Exp.Sizeof (Typ.mk (Tarray (t_, None)), len, st) | Exp.Sizeof ({typ=t_} as sizeof_data) ->
Exp.Sizeof {sizeof_data with typ=Typ.mk (Tarray (t_, None))}
| _ -> 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 len = match t' with let len = match t' with
| Exp.Sizeof (_, Some len, _) -> len | Exp.Sizeof {dynamic_length=Some len} -> len
| _ -> Exp.get_undefined false in | _ -> Exp.get_undefined false in
let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
expand true true hpred' expand true true hpred'
@ -1611,26 +1617,27 @@ 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
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, len2, st2) -> | Exp.Sizeof sizeof1, Exp.Sizeof sizeof2 ->
begin let pos_opt, neg_opt = case_analysis_type tenv
let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in (sizeof1.typ, sizeof1.subtype) (sizeof2.typ, sizeof2.subtype) in
let pos_type_opt = match pos_opt with let pos_type_opt = match pos_opt with
| None -> None | None -> None
| Some st1' -> | Some subtype ->
let t1', len1' = if check_subtype tenv t1 t2 then t1, len1 else t2, len2 in if check_subtype tenv sizeof1.typ sizeof2.typ then
Some (Exp.Sizeof (t1', len1', st1')) in Some (Exp.Sizeof {sizeof1 with subtype})
let neg_type_opt = match neg_opt with else
| None -> None Some (Exp.Sizeof {sizeof2 with subtype}) in
| Some st1' -> Some (Exp.Sizeof (t1, len1, st1')) in let neg_type_opt = match neg_opt with
pos_type_opt, neg_type_opt | None -> None
end | Some subtype -> Some (Exp.Sizeof {sizeof1 with subtype}) in
pos_type_opt, neg_type_opt
| _ -> (* don't know, consider both possibilities *) | _ -> (* don't know, consider both possibilities *)
Some texp1, Some texp1 Some texp1, Some texp1
end 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
| Exp.Sizeof (t1, _, _), Exp.Sizeof (t2, _, st2) -> | Exp.Sizeof {typ=t1}, Exp.Sizeof {typ=t2; subtype=st2} ->
if Config.developer_mode || if Config.developer_mode ||
(Subtype.is_cast st2 && (Subtype.is_cast st2 &&
not (Subtyping_check.check_subtype tenv t1 t2)) then not (Subtyping_check.check_subtype tenv t1 t2)) then
@ -1666,7 +1673,8 @@ 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
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, len2, st2) -> | Exp.Sizeof {typ=t1; dynamic_length=len1; subtype=st1},
Exp.Sizeof {typ=t2; dynamic_length=len2; subtype=st2} ->
[%compare.equal: Typ.t * Exp.t option] (t1, len1) (t2, len2) [%compare.equal: Typ.t * Exp.t option] (t1, len1) (t2, len2)
&& Subtype.equal_modulo_flag st1 st2 && Subtype.equal_modulo_flag st1 st2
| _ -> Exp.equal texp1 texp2 | _ -> Exp.equal texp1 texp2
@ -1677,7 +1685,7 @@ 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
| Exp.Sizeof (typ1, _, _), Exp.Sizeof (typ2, _, _) -> ( | Exp.Sizeof {typ=typ1}, Exp.Sizeof {typ=typ2} -> (
match typ1.desc, typ2.desc with match typ1.desc, typ2.desc with
| (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) -> | (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) ->
is_java_class tenv typ1 is_java_class tenv typ1
@ -1737,24 +1745,26 @@ 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', _, Exp.Sizeof(t, len, sub)) when Exp.equal e' e -> | Sil.Hpointsto(e', _, Exp.Sizeof sizeof_data) when Exp.equal e' e ->
sub_opt := Some (t, len, sub); sub_opt := Some sizeof_data;
true true
| _ -> false in | _ -> false in
if List.exists ~f:filter sigma2 then !sub_opt else None in if List.exists ~f: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
| Exp.Sizeof ({desc=Tptr (t1, _)}, None, _), Exp.Sizeof ({desc=Tptr (t2, _)}, None, _), | Exp.Sizeof {typ={desc=Tptr (t1, _)}; dynamic_length=None},
Exp.Sizeof {typ={desc=Tptr (t2, _)}; dynamic_length=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
match type_rhs e2' with match type_rhs e2' with
| Some (t2_ptsto, len2, sub2) -> | Some sizeof_data2 ->
if not (Typ.equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2 if not (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
(Exp.Sizeof (t1, None, Subtype.subtypes)) (Exp.Sizeof {typ=t1; nbytes=None;
(Exp.Sizeof (t2_ptsto, len2, sub2)) in dynamic_length=None; subtype=Subtype.subtypes})
(Exp.Sizeof sizeof_data2) 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);
@ -1984,15 +1994,18 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let fld = Fieldname.Java.from_string s in let fld = Fieldname.Java.from_string s in
let se = Sil.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in let se = Sil.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in
(fld, se) in (fld, se) in
let fields = ["java.lang.String.count"; "java.lang.String.hash"; "java.lang.String.offset"; "java.lang.String.value"] in let fields = ["java.lang.String.count"; "java.lang.String.hash";
"java.lang.String.offset"; "java.lang.String.value"] in
Sil.Estruct (List.map ~f:mk_fld_sexp fields, Sil.inst_none) in Sil.Estruct (List.map ~f: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 -> | Config.Clang ->
Exp.Sizeof (Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len)), None, Subtype.exact) Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len));
nbytes=None; dynamic_length=None; subtype=Subtype.exact}
| Config.Java -> | Config.Java ->
let object_type = Typ.Name.Java.from_string "java.lang.String" in let object_type = Typ.Name.Java.from_string "java.lang.String" in
Exp.Sizeof (Typ.mk (Tstruct object_type), None, Subtype.exact) in Exp.Sizeof {typ=Typ.mk (Tstruct object_type);
nbytes=None; dynamic_length=None; subtype=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 = Exp.Const (Const.Cclass (Ident.string_to_name s)) in let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in
@ -2002,7 +2015,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in
let class_texp = let class_texp =
let class_type = Typ.Name.Java.from_string "java.lang.Class" in let class_type = Typ.Name.Java.from_string "java.lang.Class" in
Exp.Sizeof (Typ.mk (Tstruct class_type), None, Subtype.exact) in Exp.Sizeof {typ=Typ.mk (Tstruct class_type);
nbytes=None; dynamic_length=None; subtype=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

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

@ -408,10 +408,11 @@ let strexp_extend_values
let check_not_inconsistent (atoms, _, _) = not (List.exists ~f:check_neg_atom atoms) in let check_not_inconsistent (atoms, _, _) = not (List.exists ~f:check_neg_atom atoms) in
List.filter ~f:check_not_inconsistent atoms_se_typ_list in List.filter ~f: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 len, st = match te with let sizeof_data = match te with
| Exp.Sizeof(_, len, st) -> (len, st) | Exp.Sizeof sizeof_data -> sizeof_data
| _ -> None, Subtype.exact in | _ -> {Exp.typ=Typ.mk Typ.Tvoid; nbytes=None; dynamic_length=None; subtype=Subtype.exact} in
List.map ~f:(fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Exp.Sizeof (typ', len, st))) List.map ~f:(fun (atoms', se', typ') ->
(laundry_atoms @ atoms', se', Exp.Sizeof { sizeof_data with typ=typ'}))
atoms_se_typ_list_filtered atoms_se_typ_list_filtered
let collect_root_offset exp = let collect_root_offset exp =
@ -440,24 +441,27 @@ let mk_ptsto_exp_footprint
end end
end; end;
let off_foot, eqs = laundry_offset_for_footprint max_stamp off in let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
let st = match !Config.curr_language with let subtype = match !Config.curr_language with
| Config.Clang -> Subtype.exact | Config.Clang -> Subtype.exact
| Config.Java -> Subtype.subtypes in | Config.Java -> Subtype.subtypes in
let create_ptsto footprint_part off0 = match root, off0, typ.Typ.desc with let create_ptsto footprint_part off0 = match root, off0, typ.Typ.desc with
| Exp.Lvar pvar, [], Typ.Tfun _ -> | Exp.Lvar pvar, [], Typ.Tfun _ ->
let fun_name = Typ.Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in let fun_name = Typ.Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
let fun_exp = Exp.Const (Const.Cfun fun_name) in let fun_exp = Exp.Const (Const.Cfun fun_name) in
([], Prop.mk_ptsto tenv root (Sil.Eexp (fun_exp, inst)) (Exp.Sizeof (typ, None, st))) ([], Prop.mk_ptsto tenv root (Sil.Eexp (fun_exp, inst))
(Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype}))
| _, [], Typ.Tfun _ -> | _, [], Typ.Tfun _ ->
let atoms, se, t = let atoms, se, typ =
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 tenv root se (Exp.Sizeof (t, None, st))) (atoms, Prop.mk_ptsto tenv root se
(Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype}))
| _ -> | _ ->
let atoms, se, t = let atoms, se, typ =
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 tenv root se (Exp.Sizeof (t, None, st))) in (atoms, Prop.mk_ptsto tenv root se
(Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype})) 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
@ -748,7 +752,8 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
| Some (Sil.Eexp (matching_exp, _), _) -> | Some (Sil.Eexp (matching_exp, _), _) ->
List.find_map List.find_map
~f:(function ~f:(function
| Sil.Hpointsto (lhs_exp, Estruct (matching_flds, _), Sizeof (fld_typ, _, _)) | Sil.Hpointsto (lhs_exp, Estruct (matching_flds, _),
Sizeof {typ=fld_typ})
when Exp.equal lhs_exp matching_exp -> when Exp.equal lhs_exp matching_exp ->
get_fld_strexp_and_typ get_fld_strexp_and_typ
fld_typ (is_guarded_by_fld field_part) matching_flds fld_typ (is_guarded_by_fld field_part) matching_flds
@ -761,37 +766,38 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
| _ -> | _ ->
None in None in
List.find_map List.find_map ~f:(fun hpred -> (match hpred with
~f:(function [@warning "-57"] (* FIXME: silenced warning may be legit *) | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _,
| Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _)) Exp.Sizeof {typ})
| Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _),
Exp.Sizeof {typ})
when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) -> when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) ->
Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ) Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ)
| Sil.Hpointsto (_, Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Estruct (flds, _), Exp.Sizeof {typ}) ->
begin begin
(* first, try to find a field that exactly matches the guarded-by string *) (* first, try to find a field that exactly matches the guarded-by string *)
match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with
| None when guarded_by_str_is_this guarded_by_str0 -> | None when guarded_by_str_is_this guarded_by_str0 ->
(* if the guarded-by string is "OuterClass.this", look for "this$n" for some n. (* if the guarded-by string is "OuterClass.this", look for "this$n" for some n.
note that this is a bit sketchy when there are mutliple this$n's, but there's note that this is a bit sketchy when there are mutliple this$n's, but there's
nothing we can do to disambiguate them. *) nothing we can do to disambiguate them. *)
get_fld_strexp_and_typ get_fld_strexp_and_typ
typ typ
(fun f _ -> Fieldname.java_is_outer_instance f) (fun f _ -> Fieldname.java_is_outer_instance f)
flds flds
| None -> | None ->
(* can't find an exact match. try a different convention. *) (* can't find an exact match. try a different convention. *)
match_on_field_type typ flds match_on_field_type typ flds
| Some _ as res_opt -> | Some _ as res_opt ->
res_opt res_opt
end end
| Sil.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof {typ})
when (guarded_by_str_is_current_class_this guarded_by_str0 pname || when (guarded_by_str_is_current_class_this guarded_by_str0 pname ||
guarded_by_str_is_super_class_this guarded_by_str0 pname guarded_by_str_is_super_class_this guarded_by_str0 pname
) && Pvar.is_this pvar -> ) && Pvar.is_this pvar ->
Some (rhs_exp, typ) Some (rhs_exp, typ)
| _ -> | _ ->
None) None) [@warning "-57"] (* FIXME: silenced warning may be legit *))
sigma in sigma in
(* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *) (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *)
let enforce_guarded_access_ accessed_fld guarded_by_str prop = let enforce_guarded_access_ accessed_fld guarded_by_str prop =
@ -910,7 +916,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
| Sil.Eexp (exp, _) when Exp.equal exp lexp -> enforce_guarded_access fld typ prop_acc | Sil.Eexp (exp, _) when Exp.equal exp lexp -> enforce_guarded_access fld typ prop_acc
| _ -> 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}) ->
List.fold ~f:(check_fld_locks typ) ~init:prop_acc flds List.fold ~f:(check_fld_locks typ) ~init:prop_acc flds
| _ -> | _ ->
prop_acc in prop_acc in
@ -1144,8 +1150,7 @@ let type_at_offset tenv texp off =
strip_offset off' typ' strip_offset off' typ'
| _ -> None in | _ -> None in
match texp with match texp with
| Exp.Sizeof(typ, _, _) -> | Exp.Sizeof {typ} -> strip_offset off typ
strip_offset off typ
| _ -> None | _ -> None
(** Check that the size of a type coming from an instruction does not exceed the size of the type from the pointsto predicate (** Check that the size of a type coming from an instruction does not exceed the size of the type from the pointsto predicate
@ -1339,7 +1344,7 @@ let is_only_pt_by_fld_or_param_with_annot
if Option.is_some procname_str_opt then obj_str := procname_str_opt; if Option.is_some procname_str_opt then obj_str := procname_str_opt;
(* it's ok for a local with no annotation to point to deref_exp *) (* it's ok for a local with no annotation to point to deref_exp *)
var_has_annotation || Option.is_some procname_str_opt || Pvar.is_local pvar var_has_annotation || Option.is_some procname_str_opt || Pvar.is_local pvar
| Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof {typ}) ->
List.for_all ~f:(is_strexp_pt_fld_with_annot tenv obj_str is_annotation typ deref_exp) flds List.for_all ~f:(is_strexp_pt_fld_with_annot tenv obj_str is_annotation typ deref_exp) flds
| _ -> true in | _ -> true in
if List.for_all ~f:is_pt_by_fld_or_param_with_annot prop.Prop.sigma && !obj_str <> None if List.for_all ~f:is_pt_by_fld_or_param_with_annot prop.Prop.sigma && !obj_str <> None

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

@ -209,7 +209,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, len, st) offlist id = let ptsto_lookup pdesc tenv p (lexp, se, sizeof) offlist id =
let f = let f =
function Some exp -> exp | None -> Exp.Var id in function Some exp -> exp | None -> Exp.Var id in
let fp_root = let fp_root =
@ -217,12 +217,12 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, len, st) offlist id =
let lookup_inst = ref None in let lookup_inst = ref None in
let e', se', typ', pred_insts_op' = let e', se', typ', pred_insts_op' =
apply_offlist apply_offlist
pdesc tenv p fp_root false (lexp, se, typ) offlist f Sil.inst_lookup lookup_inst in pdesc tenv p fp_root false (lexp, se, sizeof.Exp.typ) offlist f Sil.inst_lookup lookup_inst in
let lookup_uninitialized = (* true if we have looked up an uninitialized value *) let lookup_uninitialized = (* true if we have looked up an uninitialized value *)
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 tenv lexp se' (Exp.Sizeof (typ', len, st)) in let ptsto' = Prop.mk_ptsto tenv lexp se' (Exp.Sizeof {sizeof with typ=typ'}) 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
@ -236,7 +236,7 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, len, 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, len, st) offlist exp = let ptsto_update pdesc tenv p (lexp, se, sizeof) offlist exp =
let f _ = exp in let f _ = exp in
let fp_root = let fp_root =
match lexp with Exp.Var id -> Ident.is_footprint id | _ -> false in match lexp with Exp.Var id -> Ident.is_footprint id | _ -> false in
@ -244,8 +244,9 @@ let ptsto_update pdesc tenv p (lexp, se, typ, len, st) offlist exp =
let _, se', typ', pred_insts_op' = let _, se', typ', pred_insts_op' =
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, sizeof.Exp.typ) offlist f
let ptsto' = Prop.mk_ptsto tenv lexp se' (Exp.Sizeof (typ', len, st)) in (State.get_inst_update pos) lookup_inst in
let ptsto' = Prop.mk_ptsto tenv lexp se' (Exp.Sizeof {sizeof with typ=typ'}) in
(ptsto', pred_insts_op') (ptsto', pred_insts_op')
let update_iter iter pi sigma = let update_iter iter pi sigma =
@ -520,7 +521,7 @@ let resolve_typename prop receiver_exp =
| _ :: hpreds -> loop hpreds in | _ :: hpreds -> loop hpreds in
loop prop.Prop.sigma in loop prop.Prop.sigma in
match typexp_opt with match typexp_opt with
| Some (Exp.Sizeof ({desc=Tstruct name}, _, _)) -> Some name | Some (Exp.Sizeof {typ={desc=Tstruct name}}) -> Some name
| _ -> None | _ -> None
(** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal (** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
@ -809,7 +810,7 @@ let do_error_checks tenv node_opt instr pname pdesc = match node_opt with
let add_strexp_to_footprint tenv strexp abduced_pv typ prop = let add_strexp_to_footprint tenv strexp abduced_pv typ prop =
let abduced_lvar = Exp.Lvar abduced_pv in let abduced_lvar = Exp.Lvar abduced_pv in
let lvar_pt_fpvar = let lvar_pt_fpvar =
let sizeof_exp = Exp.Sizeof (typ, None, Subtype.subtypes) in let sizeof_exp = Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.subtypes} in
Prop.mk_ptsto tenv abduced_lvar strexp sizeof_exp in Prop.mk_ptsto tenv abduced_lvar strexp sizeof_exp in
let sigma_fp = prop.Prop.sigma_fp in let sigma_fp = prop.Prop.sigma_fp in
Prop.normalize tenv (Prop.set prop ~sigma_fp:(lvar_pt_fpvar :: sigma_fp)) Prop.normalize tenv (Prop.set prop ~sigma_fp:(lvar_pt_fpvar :: sigma_fp))
@ -905,9 +906,9 @@ let execute_load ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc
let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in
let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in
match Prop.prop_iter_current tenv iter_ren with match Prop.prop_iter_current tenv iter_ren with
| (Sil.Hpointsto(lexp, strexp, Exp.Sizeof (typ, len, st)), offlist) -> | (Sil.Hpointsto(lexp, strexp, Exp.Sizeof sizeof_data), 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, len, st) offlist id in ptsto_lookup pdesc tenv prop_ren (lexp, strexp, sizeof_data) offlist id in
let update acc (pi, sigma) = let update acc (pi, sigma) =
let pi' = Sil.Aeq (Exp.Var(id), contents):: pi in let pi' = Sil.Aeq (Exp.Var(id), contents):: pi in
let sigma' = new_ptsto:: sigma in let sigma' = new_ptsto:: sigma in
@ -978,14 +979,14 @@ let load_ret_annots pname =
let execute_store ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ = let execute_store ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_store_ pdesc tenv rhs_exp acc_in iter = let execute_store_ pdesc tenv rhs_exp acc_in iter =
let (lexp, strexp, typ, len, st, offlist) = let (lexp, strexp, sizeof, offlist) =
match Prop.prop_iter_current tenv iter with match Prop.prop_iter_current tenv iter with
| (Sil.Hpointsto(lexp, strexp, Exp.Sizeof (typ, len, st)), offlist) -> | (Sil.Hpointsto(lexp, strexp, Exp.Sizeof sizeof), offlist) ->
(lexp, strexp, typ, len, st, offlist) (lexp, strexp, sizeof, offlist)
| _ -> assert false in | _ -> assert false in
let p = Prop.prop_iter_to_prop tenv iter in let p = Prop.prop_iter_to_prop tenv iter in
let new_ptsto, pred_insts_op = let new_ptsto, pred_insts_op =
ptsto_update pdesc tenv p (lexp, strexp, typ, len, st) offlist rhs_exp in ptsto_update pdesc tenv p (lexp, strexp, sizeof) 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
@ -1250,7 +1251,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
ret_old_path [Prop.exist_quantify tenv (Sil.fav_from_list temps) prop_] ret_old_path [Prop.exist_quantify tenv (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, Exp.Sizeof (y, None, Subtype.exact), None) in let add_None (x, typ) =
(x, Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact}, None) in
let sigma_locals () = let sigma_locals () =
List.map List.map
~f:(Prop.mk_ptsto_lvar tenv Prop.Fld_init Sil.inst_initial) ~f:(Prop.mk_ptsto_lvar tenv Prop.Fld_init Sil.inst_initial)
@ -1357,7 +1359,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let havoc_actual_by_ref prop (actual, actual_typ, _) = let havoc_actual_by_ref prop (actual, actual_typ, _) =
let actual_pt_havocd_var = let actual_pt_havocd_var =
let havocd_var = Exp.Var (Ident.create_fresh Ident.kprimed) in let havocd_var = Exp.Var (Ident.create_fresh Ident.kprimed) in
let sizeof_exp = Exp.Sizeof (Typ.strip_ptr actual_typ, None, Subtype.subtypes) in let sizeof_exp = Exp.Sizeof {typ=Typ.strip_ptr actual_typ; nbytes=None;
dynamic_length=None; subtype=Subtype.subtypes} in
Prop.mk_ptsto tenv actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in Prop.mk_ptsto tenv 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
let do_actual_by_ref = let do_actual_by_ref =

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

@ -482,8 +482,8 @@ let texp_star tenv texp1 texp2 =
| _ -> | _ ->
t1 in t1 in
match texp1, texp2 with match texp1, texp2 with
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, _, st2) -> | Exp.Sizeof ({typ=t1; subtype=st1} as sizeof1), Exp.Sizeof {typ=t2; subtype=st2} ->
Exp.Sizeof (typ_star t1 t2, len1, Subtype.join st1 st2) Exp.Sizeof {sizeof1 with typ=typ_star t1 t2; subtype=Subtype.join st1 st2}
| _ -> | _ ->
texp1 texp1
@ -634,7 +634,7 @@ let prop_get_exn_name pname prop =
let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
let rec search_exn e = function let rec search_exn e = function
| [] -> None | [] -> None
| Sil.Hpointsto (e1, _, Sizeof ({desc=Tstruct name}, _, _)) :: _ | Sil.Hpointsto (e1, _, Sizeof {typ={desc=Tstruct name}}) :: _
when Exp.equal e1 e -> when Exp.equal e1 e ->
Some name Some name
| _ :: tl -> search_exn e tl in | _ :: tl -> search_exn e tl in
@ -882,7 +882,7 @@ let mk_actual_precondition tenv prop actual_params formal_params =
Prop.mk_ptsto tenv Prop.mk_ptsto tenv
(Exp.Lvar formal_var) (Exp.Lvar formal_var)
(Sil.Eexp (actual_e, Sil.inst_actual_precondition)) (Sil.Eexp (actual_e, Sil.inst_actual_precondition))
(Exp.Sizeof (actual_t, None, Subtype.exact)) in (Exp.Sizeof {typ=actual_t; nbytes=None; dynamic_length=None; subtype=Subtype.exact}) in
let instantiated_formals = List.map ~f:mk_instantiation formals_actuals in let instantiated_formals = List.map ~f: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 tenv actual_pre Prop.normalize tenv actual_pre

16
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -36,12 +36,12 @@ struct
type extras = Typ.Procname.t -> Procdesc.t option type extras = Typ.Procname.t -> Procdesc.t option
(* NOTE: heuristic *) (* NOTE: heuristic *)
let get_malloc_info : Exp.t -> Typ.t * Exp.t let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t
= function = function
| Exp.BinOp (Binop.Mult, Exp.Sizeof (typ, _, _), size) | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length)
| Exp.BinOp (Binop.Mult, size, Exp.Sizeof (typ, _, _)) -> (typ, size) | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> (typ, nbytes, length)
| Exp.Sizeof (typ, _, _) -> (typ, Exp.one) | Exp.Sizeof {typ; nbytes} -> (typ, nbytes, Exp.one)
| x -> (Typ.mk (Tint Typ.IChar), x) | x -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x)
let model_malloc let model_malloc
: Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
@ -56,9 +56,9 @@ struct
Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem
| _ -> mem | _ -> mem
in in
let (typ, size) = get_malloc_info (List.hd_exn params |> fst) in let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in
let size = Sem.eval size mem (CFG.loc node) |> Dom.Val.get_itv in let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in
let v = Sem.eval_array_alloc pname node typ Itv.zero size 0 1 in let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
mem mem
|> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.add_stack (Loc.of_id id) v
|> set_uninitialized typ (Dom.Val.get_array_locs v) |> set_uninitialized typ (Dom.Val.get_array_locs v)

23
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -76,15 +76,18 @@ struct
must_alias e1 e2 m && Fieldname.equal fld1 fld2 must_alias e1 e2 m && Fieldname.equal fld1 fld2
| Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) ->
must_alias e11 e21 m && must_alias e12 e22 m must_alias e11 e21 m && must_alias e12 e22 m
| Exp.Sizeof (t1, dynlen1, subt1), Exp.Sizeof (t2, dynlen2, subt2) -> | Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} ->
Int.equal nbytes1 nbytes2
| Exp.Sizeof {typ=t1; dynamic_length=dynlen1; subtype=subt1},
Exp.Sizeof {typ=t2; dynamic_length=dynlen2; subtype=subt2} ->
Typ.equal t1 t2 Typ.equal t1 t2
&& must_alias_opt dynlen1 dynlen2 m && must_alias_opt dynlen1 dynlen2 m
&& Int.equal (Subtype.compare subt1 subt2) 0 && Int.equal (Subtype.compare subt1 subt2) 0
| _, _ -> false | _, _ -> false
and must_alias_opt : Exp.dynamic_length -> Exp.dynamic_length -> Mem.astate -> bool and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool
= fun dynlen1 dynlen2 m -> = fun e1_opt e2_opt m ->
match dynlen1, dynlen2 with match e1_opt, e2_opt with
| Some e1, Some e2 -> must_alias e1 e2 m | Some e1, Some e2 -> must_alias e1 e2 m
| None, None -> true | None, None -> true
| _, _ -> false | _, _ -> false
@ -163,7 +166,8 @@ struct
(* if nested array, add the array blk *) (* if nested array, add the array blk *)
let arr = Mem.find_heap_set ploc mem in let arr = Mem.find_heap_set ploc mem in
Val.join (Val.of_pow_loc ploc) arr Val.join (Val.of_pow_loc ploc) arr
| Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ) | Exp.Sizeof {nbytes=Some size} -> Val.of_int size
| Exp.Sizeof {typ; nbytes=None} -> Val.of_int (sizeof typ)
| Exp.Exn _ | Exp.Exn _
| Exp.Closure _ -> Val.top_itv | Exp.Closure _ -> Val.top_itv
@ -219,10 +223,13 @@ struct
|> Allocsite.make |> Allocsite.make
let eval_array_alloc let eval_array_alloc
: Typ.Procname.t -> CFG.node -> Typ.t -> Itv.t -> Itv.t -> int -> int -> Val.t : Typ.Procname.t -> CFG.node -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int -> Val.t
= fun pdesc node typ offset size inst_num dimension -> = fun pdesc node typ ?stride:stride0 offset size inst_num dimension ->
let allocsite = get_allocsite pdesc node inst_num dimension in let allocsite = get_allocsite pdesc node inst_num dimension in
let stride = sizeof typ |> Itv.of_int in let int_stride = match stride0 with
| None -> sizeof typ
| Some stride -> stride in
let stride = Itv.of_int int_stride in
ArrayBlk.make allocsite offset size stride ArrayBlk.make allocsite offset size stride
|> Val.of_array_blk |> Val.of_array_blk

2
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -558,7 +558,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
end end
| Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname),
(target_exp, target_typ) :: (Exp.Sizeof (cast_typ, _, _), _) :: _ , _, _) (target_exp, target_typ) :: (Exp.Sizeof {typ=cast_typ}, _) :: _ , _, _)
when Typ.Procname.equal callee_pname BuiltinDecl.__cast -> when Typ.Procname.equal callee_pname BuiltinDecl.__cast ->
let lhs_access_path = AccessPath.of_id ret_id (Typ.mk (Tptr (cast_typ, Pk_pointer))) in let lhs_access_path = AccessPath.of_id ret_id (Typ.mk (Tptr (cast_typ, Pk_pointer))) in
let attribute_map = let attribute_map =

2
infer/src/clang/ast_expressions.ml
Unescape View File

@ -401,7 +401,7 @@ let translate_block_enumerate block_name stmt_info stmt_list ei =
let parameter = Clang_ast_t.UnaryExprOrTypeTraitExpr let parameter = Clang_ast_t.UnaryExprOrTypeTraitExpr
((fresh_stmt_info stmt_info), [], ((fresh_stmt_info stmt_info), [],
make_general_expr_info create_unsigned_long_type `RValue `Ordinary, make_general_expr_info create_unsigned_long_type `RValue `Ordinary,
{ Clang_ast_t.uttei_kind = `SizeOf; Clang_ast_t.uttei_qual_type = type_opt}) in { Clang_ast_t.uttei_kind = `SizeOf 1; Clang_ast_t.uttei_qual_type = type_opt}) in
let pointer = di.Clang_ast_t.di_pointer in let pointer = di.Clang_ast_t.di_pointer in
let stmt_info = fresh_stmt_info stmt_info in let stmt_info = fresh_stmt_info stmt_info in
let malloc_name = CAst_utils.make_name_decl CFrontend_config.malloc in let malloc_name = CAst_utils.make_name_decl CFrontend_config.malloc in

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

@ -209,7 +209,8 @@ struct
with Self.SelfClassException class_name -> with Self.SelfClassException class_name ->
let typ = Typ.mk (Tstruct class_name) in let typ = Typ.mk (Tstruct class_name) in
{ empty_res_trans with { empty_res_trans with
exps = [Exp.Sizeof (typ, None, Subtype.exact), Typ.mk (Tint IULong)] } exps = [Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact},
Typ.mk (Tint IULong)] }
let add_reference_if_glvalue (typ : Typ.t) expr_info = let add_reference_if_glvalue (typ : Typ.t) expr_info =
(* glvalue definition per C++11:*) (* glvalue definition per C++11:*)
@ -414,7 +415,7 @@ struct
let tenv = trans_state.context.CContext.tenv in let tenv = trans_state.context.CContext.tenv in
let typ = CType_decl.qual_type_to_sil_type tenv expr_info.Clang_ast_t.ei_qual_type in let typ = CType_decl.qual_type_to_sil_type tenv expr_info.Clang_ast_t.ei_qual_type in
match unary_expr_or_type_trait_expr_info.Clang_ast_t.uttei_kind with match unary_expr_or_type_trait_expr_info.Clang_ast_t.uttei_kind with
| `SizeOf -> | `SizeOf nbytes0 ->
let qt_opt = let qt_opt =
CAst_utils.type_from_unary_expr_or_type_trait_expr_info CAst_utils.type_from_unary_expr_or_type_trait_expr_info
unary_expr_or_type_trait_expr_info in unary_expr_or_type_trait_expr_info in
@ -422,8 +423,14 @@ struct
match qt_opt with match qt_opt with
| Some qt -> CType_decl.qual_type_to_sil_type tenv qt | Some qt -> CType_decl.qual_type_to_sil_type tenv qt
| None -> typ (* Some default type since the type is missing *) in | None -> typ (* Some default type since the type is missing *) in
{ empty_res_trans with let nbytes = if nbytes0 < 0 then
exps = [(Exp.Sizeof (sizeof_typ, None, Subtype.exact), sizeof_typ)] } (* nbytes < 0 when the sizeof cannot be statically determined *)
None
else
Some nbytes0 in
let sizeof_data =
{Exp.typ=sizeof_typ; nbytes; dynamic_length=None; subtype=Subtype.exact} in
{ empty_res_trans with exps = [(Exp.Sizeof sizeof_data, sizeof_typ)] }
| k -> Logging.out | k -> Logging.out
"\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"
@ -2219,12 +2226,12 @@ struct
let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
let trans_state' = { trans_state_pri with succ_nodes = [] } in let trans_state' = { trans_state_pri with succ_nodes = [] } in
let context = trans_state.context in let context = trans_state.context in
let subtypes = Subtype.subtypes_cast in let subtype = Subtype.subtypes_cast in
let tenv = context.CContext.tenv in let tenv = context.CContext.tenv in
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 = CType_decl.qual_type_to_sil_type tenv cast_qual_type in let cast_type = CType_decl.qual_type_to_sil_type tenv cast_qual_type in
let sizeof_expr = match cast_type.desc with let sizeof_expr = match cast_type.desc with
| Typ.Tptr (typ, _) -> Exp.Sizeof (typ, None, subtypes) | Typ.Tptr (typ, _) -> Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype}
| _ -> assert false in | _ -> assert false in
let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in
let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
@ -2288,7 +2295,8 @@ struct
let sil_fun = Exp.Const (Const.Cfun fun_name) in let sil_fun = Exp.Const (Const.Cfun fun_name) in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let void_typ = Typ.mk Tvoid in let void_typ = Typ.mk Tvoid in
let type_info_objc = (Exp.Sizeof (typ, None, Subtype.exact), void_typ) in let type_info_objc = (Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact},
void_typ) in
let field_name_decl = CAst_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in let field_name_decl = CAst_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in
let field_name = CGeneral_utils.mk_class_field_name field_name_decl in let field_name = CGeneral_utils.mk_class_field_name field_name_decl in
let ret_exp = Exp.Var ret_id in let ret_exp = Exp.Var ret_id in

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

@ -301,7 +301,8 @@ let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt =
| Tptr (styp, Typ.Pk_objc_autoreleasing) -> | Tptr (styp, Typ.Pk_objc_autoreleasing) ->
function_type, styp function_type, styp
| _ -> CType.add_pointer_to_typ function_type, function_type in | _ -> CType.add_pointer_to_typ function_type, function_type in
let sizeof_exp_ = Exp.Sizeof (function_type_np, None, Subtype.exact) in let sizeof_exp_ = Exp.Sizeof {typ=function_type_np; nbytes=None;
dynamic_length=None; subtype=Subtype.exact} in
let sizeof_exp = match size_exp_opt with let sizeof_exp = match size_exp_opt with
| Some exp -> Exp.BinOp (Binop.Mult, sizeof_exp_, exp) | Some exp -> Exp.BinOp (Binop.Mult, sizeof_exp_, exp)
| None -> sizeof_exp_ in | None -> sizeof_exp_ in
@ -377,7 +378,7 @@ let create_cast_instrs 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 ret_id_typ = Some (ret_id, cast_to_typ) in let ret_id_typ = Some (ret_id, cast_to_typ) in
let typ = CType.remove_pointer_to_typ cast_to_typ in let typ = CType.remove_pointer_to_typ cast_to_typ in
let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype=Subtype.exact} in
let pname = BuiltinDecl.__objc_cast in let pname = BuiltinDecl.__objc_cast in
let args = [(exp, cast_from_typ); (sizeof_exp, Typ.mk (Tint Typ.IULong))] in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.mk (Tint Typ.IULong))] in
let stmt_call = let stmt_call =

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

@ -122,8 +122,8 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pdesc
String.equal (Typ.Name.name name) "java.lang.Throwable" String.equal (Typ.Name.name name) "java.lang.Throwable"
| _ -> false in | _ -> false in
let do_instr = function let do_instr = function
| Sil.Call (_, Exp.Const (Const.Cfun pn), [_; (Exp.Sizeof(t, _, _), _)], _, _) when | Sil.Call (_, Exp.Const (Const.Cfun pn), [_; (Exp.Sizeof {typ}, _)], _, _) when
Typ.Procname.equal pn BuiltinDecl.__instanceof && typ_is_throwable t -> Typ.Procname.equal pn BuiltinDecl.__instanceof && typ_is_throwable typ ->
throwable_found := true throwable_found := true
| _ -> () in | _ -> () in
let do_node n = let do_node n =

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

@ -73,7 +73,8 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
let inhabited_exp = Exp.Var retval in let inhabited_exp = Exp.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 = Exp.Sizeof (sizeof_typ, sizeof_len, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ=sizeof_typ; nbytes=None;
dynamic_length=sizeof_len; subtype=Subtype.exact} in
let args = [(sizeof_exp, Typ.mk (Tptr (ret_typ, Typ.Pk_pointer)))] in let args = [(sizeof_exp, Typ.mk (Tptr (ret_typ, Typ.Pk_pointer)))] in
Sil.Call (Some (retval, ret_typ), fun_new, args, env.pc, cf_alloc) in Sil.Call (Some (retval, ret_typ), fun_new, args, env.pc, cf_alloc) in
(inhabited_exp, env_add_instr call_instr env) (inhabited_exp, env_add_instr call_instr env)

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

@ -624,7 +624,8 @@ let get_array_length context pc expr_list content_type =
(Typ.mk (Tarray (content_type, None)), Some sil_len_expr) in (Typ.mk (Tarray (content_type, None)), Some sil_len_expr) in
let array_type, array_len = let array_type, array_len =
List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None) in List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None) in
let array_size = Exp.Sizeof (array_type, array_len, Subtype.exact) in let array_size = Exp.Sizeof {typ=array_type; nbytes=None;
dynamic_length=array_len; subtype=Subtype.exact} in
(instrs, array_size) (instrs, array_size)
let detect_loop entry_pc impl = let detect_loop entry_pc impl =
@ -816,7 +817,8 @@ let rec instruction (context : JContext.t) pc instr : translation =
let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__new) in let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__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 = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ=class_type_np; nbytes=None;
dynamic_length=None; subtype=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 = let new_instr =
@ -930,7 +932,8 @@ let rec instruction (context : JContext.t) 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 = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ=class_type_np; nbytes=None;
dynamic_length=None; subtype=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 = let new_instr =
@ -984,7 +987,8 @@ let rec instruction (context : JContext.t) 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 = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ=class_type_np; nbytes=None;
dynamic_length=None; subtype=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 = let new_instr =
@ -1024,7 +1028,8 @@ let rec instruction (context : JContext.t) 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 = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof {typ=class_type_np; nbytes=None;
dynamic_length=None; subtype=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 = let new_instr =

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

@ -72,7 +72,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
let args = [ let args = [
(Exp.Var id_exn_val, Typ.mk (Tptr(exn_type, Typ.Pk_pointer))); (Exp.Var id_exn_val, Typ.mk (Tptr(exn_type, Typ.Pk_pointer)));
(Exp.Sizeof (exn_type, None, Subtype.exact), Typ.mk Tvoid)] in (Exp.Sizeof {typ=exn_type; nbytes=None; dynamic_length=None; subtype=Subtype.exact},
Typ.mk Tvoid)] in
Sil.Call Sil.Call
(Some (id_instanceof, Typ.mk (Tint IBool)), instanceof_builtin, args, loc, CallFlags.default) in (Some (id_instanceof, Typ.mk (Tint IBool)), instanceof_builtin, args, loc, CallFlags.default) in
let if_kind = Sil.Ik_switch in let if_kind = Sil.Ik_switch in

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

@ -374,10 +374,10 @@ and value_type program tenv vt =
(** Translate object types into Exp.Sizeof expressions *) (** Translate object types into Exp.Sizeof expressions *)
let sizeof_of_object_type program tenv ot subtypes = let sizeof_of_object_type program tenv ot subtype =
match (object_type program tenv ot).Typ.desc with match (object_type program tenv ot).Typ.desc with
| Typ.Tptr (typ, _) -> | Typ.Tptr (typ, _) ->
Exp.Sizeof (typ, None, subtypes) Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype}
| _ -> | _ ->
raise (Type_tranlsation_error "Pointer or array type expected in tenv") raise (Type_tranlsation_error "Pointer or array type expected in tenv")

14
infer/tests/codetoanalyze/c/bufferoverrun/Makefile
Unescape View File

@ -15,18 +15,6 @@ CLANG_OPTIONS = -c
INFER_OPTIONS = -F --project-root $(TESTS_DIR) --no-failures-allowed INFER_OPTIONS = -F --project-root $(TESTS_DIR) --no-failures-allowed
INFERPRINT_OPTIONS = --issues-tests INFERPRINT_OPTIONS = --issues-tests
SOURCES = \ SOURCES = $(wildcard *.c)
trivial.c \
function_call.c \
for_loop.c \
while_loop.c \
do_while.c \
nested_loop.c \
nested_loop_with_label.c \
break_continue_return.c \
goto_loop.c \
inf_loop.c \
prune_constant.c \
prune_alias.c \
include $(TESTS_DIR)/clang.make include $(TESTS_DIR)/clang.make

1
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -8,5 +8,6 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offse
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5]
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:13:5]
codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10]

15
infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c
Unescape View File

@ -0,0 +1,15 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
void eval_sizeof_bad() {
if (sizeof(long long) < 10000) {
// always true
int a[0];
a[1]; // report
}
}

4
infer/tests/codetoanalyze/objc/shared/block/block-it.m.dot
Unescape View File

@ -121,7 +121,7 @@ digraph iCFG {
"array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_16" -> "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_5" ; "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_16" -> "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_5" ;
"array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_17" [label="17: DeclStmt \n n$18=_fun_malloc_no_fail(sizeof(signed char):signed char) [line 21]\n *&stop:_Bool*=n$18 [line 21]\n " shape="box"] "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_17" [label="17: DeclStmt \n n$18=_fun_malloc_no_fail(sizeof(signed char1):signed char) [line 21]\n *&stop:_Bool*=n$18 [line 21]\n " shape="box"]
"array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_17" -> "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_16" ; "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_17" -> "array#MyBlock#instance.8be6e5b5e968d186440e1931c9eb40de_16" ;
@ -202,7 +202,7 @@ digraph iCFG {
"array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_16" -> "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_5" ; "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_16" -> "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_5" ;
"array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_17" [label="17: DeclStmt \n n$40=_fun_malloc_no_fail(sizeof(_Bool):_Bool) [line 48]\n *&stop:_Bool*=n$40 [line 48]\n " shape="box"] "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_17" [label="17: DeclStmt \n n$40=_fun_malloc_no_fail(sizeof(_Bool8):_Bool) [line 48]\n *&stop:_Bool*=n$40 [line 48]\n " shape="box"]
"array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_17" -> "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_16" ; "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_17" -> "array_trans#MyBlock#instance.13289a590560d0628a3ae5174e716a32_16" ;

2
infer/tests/codetoanalyze/objc/shared/category_procdesc/main.c.dot
Unescape View File

@ -11,7 +11,7 @@ digraph iCFG {
"CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_3" -> "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_2" ; "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_3" -> "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_2" ;
"CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_4" [label="4: DeclStmt \n n$0=_fun_malloc_no_fail(sizeof(int):int) [line 16]\n *&x:int*=n$0 [line 16]\n " shape="box"] "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_4" [label="4: DeclStmt \n n$0=_fun_malloc_no_fail(sizeof(int32):int) [line 16]\n *&x:int*=n$0 [line 16]\n " shape="box"]
"CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_4" -> "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_3" ; "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_4" -> "CategoryProcdescMain.ae2ee334c26ccbf8ee413efe5d896611_3" ;

6
infer/tests/codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m.dot
Unescape View File

@ -173,7 +173,7 @@ digraph iCFG {
"regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_4" -> "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_3" ; "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_4" -> "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_3" ;
"regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_5" [label="5: DeclStmt \n n$39=_fun_malloc_no_fail(sizeof(int):int) [line 88]\n *&x:int*=n$39 [line 88]\n " shape="box"] "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_5" [label="5: DeclStmt \n n$39=_fun_malloc_no_fail(sizeof(int32):int) [line 88]\n *&x:int*=n$39 [line 88]\n " shape="box"]
"regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_5" -> "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_4" ; "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_5" -> "regularLeak#MemoryLeakExample#instance.939a892cee505c3459f2d889292f218b_4" ;
@ -196,7 +196,7 @@ digraph iCFG {
"blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_5" -> "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_4" ; "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_5" -> "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_4" ;
"blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_6" [label="6: DeclStmt \n n$48=_fun_malloc_no_fail(sizeof(int):int) [line 94]\n *&x:int*=n$48 [line 94]\n " shape="box"] "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_6" [label="6: DeclStmt \n n$48=_fun_malloc_no_fail(sizeof(int32):int) [line 94]\n *&x:int*=n$48 [line 94]\n " shape="box"]
"blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_6" -> "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_5" ; "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_6" -> "blockCapturedVarLeak#MemoryLeakExample#instance.53bb018bc84d6a696dc756e20b5b3f52_5" ;
@ -219,7 +219,7 @@ digraph iCFG {
"blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_5" -> "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_4" ; "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_5" -> "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_4" ;
"blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_6" [label="6: DeclStmt \n n$59=_fun_malloc_no_fail(sizeof(int):int) [line 103]\n *&x:int*=n$59 [line 103]\n " shape="box"] "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_6" [label="6: DeclStmt \n n$59=_fun_malloc_no_fail(sizeof(int32):int) [line 103]\n *&x:int*=n$59 [line 103]\n " shape="box"]
"blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_6" -> "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_5" ; "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_6" -> "blockFreeNoLeakTODO#MemoryLeakExample#instance.745cca07ccdb517734d79c9d7a1eaed8_5" ;

2
infer/tests/codetoanalyze/objc/shared/npe/npe_malloc.m.dot
Unescape View File

@ -15,7 +15,7 @@ digraph iCFG {
"test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_4" -> "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_3" ; "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_4" -> "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_3" ;
"test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_5" [label="5: DeclStmt \n n$2=_fun_malloc_no_fail(sizeof(Person):Person) [line 25]\n *&person:Person*=n$2 [line 25]\n " shape="box"] "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_5" [label="5: DeclStmt \n n$2=_fun_malloc_no_fail(sizeof(Person64):Person) [line 25]\n *&person:Person*=n$2 [line 25]\n " shape="box"]
"test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_5" -> "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_4" ; "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_5" -> "test#NpeMallocC#instance.736ba93f935cc64d6e9c549cc16c07a7_4" ;

Write Preview
Loading…
Cancel
Save