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

[IR] Simplify to single return id, with type

Browse Source 
Summary:
Change Sil.Call instruction to have only a single optional return
identifier, insted of a list.  Essentially none of the code handled
multiple return identifiers.  Also, add the type of the return
identitifier to Call instructions.

Reviewed By: sblackshear

Differential Revision: D3919358

fbshipit-source-id: d2d4f72
master
Josh Berdine 8 years ago committed by Facebook Github Bot 7
parent ae632e281a
commit c094a38d56
32 changed files with 323 additions and 277 deletions
Show Stats Download Patch File Download Diff File

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

@ -1175,7 +1175,7 @@ let save_attributes source_file cfg => {
/** Inline a synthetic (access or bridge) method. */ /** Inline a synthetic (access or bridge) method. */
let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr => { let inline_synthetic_method ret_id etl proc_desc loc_call :option Sil.instr => {
let modified = ref None; let modified = ref None;
let debug = false; let debug = false;
let found instr instr' => { let found instr instr' => {
@ -1186,15 +1186,16 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
} }
}; };
let do_instr _ instr => let do_instr _ instr =>
switch (instr, ret_ids, etl) { switch (instr, ret_id, etl) {
| ( | (
Sil.Load _ (Exp.Lfield (Exp.Var _) fn ft) bt _, Sil.Load _ (Exp.Lfield (Exp.Var _) fn ft) bt _,
[ret_id], Some (ret_id, _),
[(e1, _)] /* getter for fields */ [(e1, _)] /* getter for fields */
) => ) =>
let instr' = Sil.Load ret_id (Exp.Lfield e1 fn ft) bt loc_call; let instr' = Sil.Load ret_id (Exp.Lfield e1 fn ft) bt loc_call;
found instr instr' found instr instr'
| (Sil.Load _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, [ret_id], []) when Pvar.is_global pvar => | (Sil.Load _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, Some (ret_id, _), [])
when Pvar.is_global pvar =>
/* getter for static fields */ /* getter for static fields */
let instr' = Sil.Load ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call; let instr' = Sil.Load ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call;
found instr instr' found instr instr'
@ -1209,21 +1210,19 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
/* setter for static fields */ /* setter for static fields */
let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt e1 loc_call; let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt e1 loc_call;
found instr instr' found instr instr'
| (Sil.Call ret_ids' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) | (Sil.Call ret_id' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _)
when IList.length ret_ids == IList.length ret_ids' && IList.length etl' == IList.length etl => when ret_id == None == (ret_id' == None) && IList.length etl' == IList.length etl =>
let instr' = Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl loc_call cf; let instr' = Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc_call cf;
found instr instr' found instr instr'
| (Sil.Call ret_ids' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) | (Sil.Call ret_id' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _)
when when ret_id == None == (ret_id' == None) && IList.length etl' + 1 == IList.length etl =>
IList.length ret_ids == IList.length ret_ids' &&
IList.length etl' + 1 == IList.length etl =>
let etl1 = let etl1 =
switch (IList.rev etl) { switch (IList.rev etl) {
/* remove last element */ /* remove last element */
| [_, ...l] => IList.rev l | [_, ...l] => IList.rev l
| [] => assert false | [] => assert false
}; };
let instr' = Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl1 loc_call cf; let instr' = Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl1 loc_call cf;
found instr instr' found instr instr'
| _ => () | _ => ()
}; };
@ -1236,7 +1235,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
let proc_inline_synthetic_methods cfg proc_desc :unit => { let proc_inline_synthetic_methods cfg proc_desc :unit => {
let instr_inline_synthetic_method = let instr_inline_synthetic_method =
fun fun
| Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl loc _ => | Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc _ =>
switch (Procdesc.find_from_name cfg pn) { switch (Procdesc.find_from_name cfg pn) {
| Some pd => | Some pd =>
let is_access = Procname.java_is_access_method pn; let is_access = Procname.java_is_access_method pn;
@ -1244,7 +1243,7 @@ let proc_inline_synthetic_methods cfg proc_desc :unit => {
let is_synthetic = attributes.ProcAttributes.is_synthetic_method; let is_synthetic = attributes.ProcAttributes.is_synthetic_method;
let is_bridge = attributes.ProcAttributes.is_bridge_method; let is_bridge = attributes.ProcAttributes.is_bridge_method;
if (is_access || is_bridge || is_synthetic) { if (is_access || is_bridge || is_synthetic) {
inline_synthetic_method ret_ids etl pd loc inline_synthetic_method ret_id etl pd loc
} else { } else {
None None
} }

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

@ -50,10 +50,9 @@ type instr =
| Store of Exp.t Typ.t Exp.t Location.t | Store of Exp.t Typ.t Exp.t Location.t
/** prune the state based on [exp=1], the boolean indicates whether true branch */ /** prune the state based on [exp=1], the boolean indicates whether true branch */
| Prune of Exp.t Location.t bool if_kind | Prune of Exp.t Location.t bool if_kind
/** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction
[ret_id1..ret_idn = e_fun(arg_ts);] [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */
where n = 0 for void return and n > 1 for struct return */ | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t
| Call of (list Ident.t) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t
/** nullify stack variable */ /** nullify stack variable */
| Nullify of Pvar.t Location.t | Nullify of Pvar.t Location.t
| Abstract of Location.t /** apply abstraction */ | Abstract of Location.t /** apply abstraction */
@ -667,7 +666,7 @@ let instr_get_exps =
| Load id e _ _ => [Exp.Var id, e] | Load id e _ _ => [Exp.Var id, e]
| Store e1 _ e2 _ => [e1, e2] | Store e1 _ e2 _ => [e1, e2]
| Prune cond _ _ _ => [cond] | Prune cond _ _ _ => [cond]
| Call ret_ids e _ _ _ => [e, ...(IList.map (fun id => Exp.Var id)) ret_ids] | Call ret_id e _ _ _ => [e, ...Option.map_default (fun (id, _) => [Exp.Var id]) [] ret_id]
| Nullify pvar _ => [Exp.Lvar pvar] | Nullify pvar _ => [Exp.Lvar pvar]
| Abstract _ => [] | Abstract _ => []
| Remove_temps temps _ => IList.map (fun id => Exp.Var id) temps | Remove_temps temps _ => IList.map (fun id => Exp.Var id) temps
@ -684,10 +683,10 @@ let pp_instr pe0 f instr => {
F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (Typ.pp pe) t (pp_exp pe) e2 Location.pp loc F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (Typ.pp pe) t (pp_exp pe) e2 Location.pp loc
| Prune cond loc true_branch _ => | Prune cond loc true_branch _ =>
F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc
| Call ret_ids e arg_ts loc cf => | Call ret_id e arg_ts loc cf =>
switch ret_ids { switch ret_id {
| [] => () | None => ()
| _ => F.fprintf f "%a=" (pp_comma_seq (Ident.pp pe)) ret_ids | Some (id, _) => F.fprintf f "%a=" (Ident.pp pe) id
}; };
F.fprintf F.fprintf
f f
@ -2114,7 +2113,7 @@ let exp_sub (subst: subst) e => exp_sub_ids (apply_sub subst) e;
let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => { let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => {
let sub_id id => let sub_id id =>
switch (exp_sub_ids f (Var id)) { switch (exp_sub_ids f (Var id)) {
| Var id' => id' | Var id' when not (Ident.equal id id') => id'
| _ => id | _ => id
}; };
switch instr { switch instr {
@ -2139,12 +2138,17 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
} else { } else {
Store lhs_exp' typ rhs_exp' loc Store lhs_exp' typ rhs_exp' loc
} }
| Call ret_ids fun_exp actuals call_flags loc => | Call ret_id fun_exp actuals call_flags loc =>
let ret_ids' = let ret_id' =
if sub_id_binders { if sub_id_binders {
IList.map_changed sub_id ret_ids switch ret_id {
| Some (id, typ) =>
let id' = sub_id id;
Ident.equal id id' ? ret_id : Some (id', typ)
| None => None
}
} else { } else {
ret_ids ret_id
}; };
let fun_exp' = exp_sub_ids f fun_exp; let fun_exp' = exp_sub_ids f fun_exp;
let actuals' = let actuals' =
@ -2160,10 +2164,10 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
} }
) )
actuals; actuals;
if (ret_ids' === ret_ids && fun_exp' === fun_exp && actuals' === actuals) { if (ret_id' === ret_id && fun_exp' === fun_exp && actuals' === actuals) {
instr instr
} else { } else {
Call ret_ids' fun_exp' actuals' call_flags loc Call ret_id' fun_exp' actuals' call_flags loc
} }
| Prune exp loc true_branch if_kind => | Prune exp loc true_branch if_kind =>
let exp' = exp_sub_ids f exp; let exp' = exp_sub_ids f exp;
@ -2189,6 +2193,15 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
/** apply [subst] to all id's in [instr], including binder id's */ /** apply [subst] to all id's in [instr], including binder id's */
let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr; let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr;
let id_typ_compare (id1, typ1) (id2, typ2) => {
let n = Ident.compare id1 id2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
};
let exp_typ_compare (exp1, typ1) (exp2, typ2) => { let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
let n = Exp.compare exp1 exp2; let n = Exp.compare exp1 exp2;
if (n != 0) { if (n != 0) {
@ -2257,8 +2270,8 @@ let instr_compare instr1 instr2 =>
} }
| (Prune _, _) => (-1) | (Prune _, _) => (-1)
| (_, Prune _) => 1 | (_, Prune _) => 1
| (Call ret_ids1 e1 arg_ts1 loc1 cf1, Call ret_ids2 e2 arg_ts2 loc2 cf2) => | (Call ret_id1 e1 arg_ts1 loc1 cf1, Call ret_id2 e2 arg_ts2 loc2 cf2) =>
let n = IList.compare Ident.compare ret_ids1 ret_ids2; let n = opt_compare id_typ_compare ret_id1 ret_id2;
if (n != 0) { if (n != 0) {
n n
} else { } else {
@ -2416,6 +2429,22 @@ let exp_typ_compare_structural (e1, t1) (e2, t2) exp_map => {
the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
used in the procedure of [instr2] */ used in the procedure of [instr2] */
let instr_compare_structural instr1 instr2 exp_map => { let instr_compare_structural instr1 instr2 exp_map => {
let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map => {
let id_typ_compare_structural (id1, typ1) (id2, typ2) => {
let (n, exp_map) = exp_compare_structural (Var id1) (Var id2) exp_map;
if (n != 0) {
(n, exp_map)
} else {
(Typ.compare typ1 typ2, exp_map)
}
};
switch (id_typ1, id_typ2) {
| (Some it1, Some it2) => id_typ_compare_structural it1 it2
| (None, None) => (0, exp_map)
| (None, _) => ((-1), exp_map)
| (_, None) => (1, exp_map)
}
};
let id_list_compare_structural ids1 ids2 exp_map => { let id_list_compare_structural ids1 ids2 exp_map => {
let n = Pervasives.compare (IList.length ids1) (IList.length ids2); let n = Pervasives.compare (IList.length ids1) (IList.length ids2);
if (n != 0) { if (n != 0) {
@ -2478,7 +2507,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
}, },
exp_map exp_map
) )
| (Call ret_ids1 e1 arg_ts1 _ cf1, Call ret_ids2 e2 arg_ts2 _ cf2) => | (Call ret_id1 e1 arg_ts1 _ cf1, Call ret_id2 e2 arg_ts2 _ cf2) =>
let args_compare_structural args1 args2 exp_map => { let args_compare_structural args1 args2 exp_map => {
let n = Pervasives.compare (IList.length args1) (IList.length args2); let n = Pervasives.compare (IList.length args1) (IList.length args2);
if (n != 0) { if (n != 0) {
@ -2498,7 +2527,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
args2 args2
} }
}; };
let (n, exp_map) = id_list_compare_structural ret_ids1 ret_ids2 exp_map; let (n, exp_map) = id_typ_opt_compare_structural ret_id1 ret_id2 exp_map;
if (n != 0) { if (n != 0) {
(n, exp_map) (n, exp_map)
} else { } else {

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

@ -52,10 +52,9 @@ type instr =
| Store of Exp.t Typ.t Exp.t Location.t | Store of Exp.t Typ.t Exp.t Location.t
/** prune the state based on [exp=1], the boolean indicates whether true branch */ /** prune the state based on [exp=1], the boolean indicates whether true branch */
| Prune of Exp.t Location.t bool if_kind | Prune of Exp.t Location.t bool if_kind
/** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction
[ret_id1..ret_idn = e_fun(arg_ts);] [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */
where n = 0 for void return and n > 1 for struct return */ | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t
| Call of (list Ident.t) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t
/** nullify stack variable */ /** nullify stack variable */
| Nullify of Pvar.t Location.t | Nullify of Pvar.t Location.t
| Abstract of Location.t /** apply abstraction */ | Abstract of Location.t /** apply abstraction */

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

@ -17,7 +17,7 @@ type args = {
tenv : Tenv.t; tenv : Tenv.t;
prop_ : Prop.normal Prop.t; prop_ : Prop.normal Prop.t;
path : Paths.Path.t; path : Paths.Path.t;
ret_ids : Ident.t list; ret_id : (Ident.t * Typ.t) option;
args : (Exp.t * Typ.t) list; args : (Exp.t * Typ.t) list;
proc_name : Procname.t; proc_name : Procname.t;
loc : Location.t; loc : Location.t;

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

@ -17,7 +17,7 @@ type args = {
tenv : Tenv.t; tenv : Tenv.t;
prop_ : Prop.normal Prop.t; prop_ : Prop.normal Prop.t;
path : Paths.Path.t; path : Paths.Path.t;
ret_ids : Ident.t list; ret_id : (Ident.t * Typ.t) option;
args : (Exp.t * Typ.t) list; args : (Exp.t * Typ.t) list;
proc_name : Procname.t; proc_name : Procname.t;
loc : Location.t; loc : Location.t;

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

@ -138,7 +138,7 @@ let find_normal_variable_funcall
(node: Cfg.Node.t) (node: Cfg.Node.t)
(id: Ident.t): (Exp.t * (Exp.t list) * Location.t * CallFlags.t) option = (id: Ident.t): (Exp.t * (Exp.t list) * Location.t * CallFlags.t) option =
let find_declaration _ = function let find_declaration _ = function
| Sil.Call ([id0], fun_exp, args, loc, call_flags) when Ident.equal id id0 -> | Sil.Call (Some (id0, _), fun_exp, args, loc, call_flags) when Ident.equal id id0 ->
Some (fun_exp, IList.map fst args, loc, call_flags) Some (fun_exp, IList.map fst args, loc, call_flags)
| _ -> None in | _ -> None in
let res = find_in_node_or_preds node find_declaration in let res = find_in_node_or_preds node find_declaration in
@ -218,14 +218,14 @@ let rec _find_normal_variable_load tenv (seen : Exp.Set.t) node id : DExp.t opti
(L.d_str "find_normal_variable_load defining "; (L.d_str "find_normal_variable_load defining ";
Sil.d_exp e; L.d_ln ()); Sil.d_exp e; L.d_ln ());
_exp_lv_dexp tenv seen node e _exp_lv_dexp tenv seen node e
| Sil.Call ([id0], Exp.Const (Const.Cfun pn), (e, _):: _, _, _) | Sil.Call (Some (id0, _), Exp.Const (Const.Cfun pn), (e, _):: _, _, _)
when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") -> when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") ->
if verbose if verbose
then then
(L.d_str "find_normal_variable_load cast on "; (L.d_str "find_normal_variable_load cast on ";
Sil.d_exp e; L.d_ln ()); Sil.d_exp e; L.d_ln ());
_exp_rv_dexp tenv seen node e _exp_rv_dexp tenv seen node e
| Sil.Call ([id0], (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags) | Sil.Call (Some (id0, _), (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags)
when Ident.equal id id0 -> when Ident.equal id id0 ->
if verbose if verbose
then then

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

@ -20,9 +20,9 @@ let execute___no_op prop path: Builtin.ret_typ =
[(prop, path)] [(prop, path)]
(** model va_arg as always returning 0 *) (** model va_arg as always returning 0 *)
let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args; loc; } let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [_; _; (lexp3, typ3)], _ -> | [_; _; (lexp3, typ3)], _ ->
let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)] SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
@ -49,9 +49,9 @@ let extract_array_type typ =
| _ -> None | _ -> None
(** Return a result from a procedure call. *) (** Return a result from a procedure call. *)
let return_result tenv e prop ret_ids = let return_result tenv e prop ret_id =
match ret_ids with match ret_id with
| [ret_id] -> Prop.conjoin_eq tenv e (Exp.Var ret_id) prop | Some (ret_id, _) -> Prop.conjoin_eq tenv e (Exp.Var ret_id) prop
| _ -> prop | _ -> prop
(* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *) (* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *)
@ -85,28 +85,28 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
end end
(* Add an array in prop if it is not allocated.*) (* Add an array in prop if it is not allocated.*)
let execute___require_allocated_array { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___require_allocated_array { Builtin.tenv; pdesc; prop_; path; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when IList.length ret_ids <= 1 -> | [(lexp, typ)] ->
(match add_array_to_prop tenv pdesc prop_ lexp typ with (match add_array_to_prop tenv pdesc prop_ lexp typ with
| None -> [] | None -> []
| Some (_, prop) -> [(prop, path)]) | Some (_, prop) -> [(prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___get_array_length { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___get_array_length { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when IList.length ret_ids <= 1 -> | [(lexp, typ)] ->
(match add_array_to_prop tenv pdesc prop_ lexp typ with (match add_array_to_prop tenv pdesc prop_ lexp typ with
| None -> [] | None -> []
| Some (len, prop) -> [(return_result tenv len prop ret_ids, path)]) | Some (len, prop) -> [(return_result tenv len prop ret_id, path)])
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___set_array_length { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___set_array_length { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, typ); (len, _)], []-> | [(lexp, typ); (len, _)], None ->
(match add_array_to_prop tenv pdesc prop_ lexp typ with (match add_array_to_prop tenv pdesc prop_ lexp typ with
| None -> [] | None -> []
| Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *) | Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *)
@ -188,10 +188,10 @@ let create_type tenv n_lexp typ prop =
non_null_case non_null_case
else null_case @ non_null_case else null_case @ non_null_case
let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; } let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when IList.length ret_ids <= 1 -> | [(lexp, typ)] ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
let props = create_type tenv n_lexp typ prop in let props = create_type tenv n_lexp typ prop in
@ -203,9 +203,9 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
| _ -> false) prop.Prop.sigma in | _ -> false) prop.Prop.sigma in
match hpred with match hpred with
| Sil.Hpointsto(_, _, texp) -> | Sil.Hpointsto(_, _, texp) ->
(return_result tenv texp prop ret_ids), path (return_result tenv texp prop ret_id), path
| _ -> assert false | _ -> assert false
with Not_found -> (return_result tenv Exp.zero prop ret_ids), path with Not_found -> (return_result tenv Exp.zero prop ret_id), path
end in end in
(IList.map aux props) (IList.map aux props)
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -227,10 +227,10 @@ let replace_ptsto_texp tenv prop root_e texp =
Prop.normalize tenv prop'' Prop.normalize tenv prop''
let execute___instanceof_cast ~instof let execute___instanceof_cast ~instof
{ Builtin.pdesc; tenv; prop_; path; ret_ids; args; } { Builtin.pdesc; tenv; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(val1_, typ1); (texp2_, _)] when IList.length ret_ids <= 1 -> | [(val1_, typ1); (texp2_, _)] ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in
let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in
@ -247,7 +247,7 @@ let execute___instanceof_cast ~instof
__POS__ None texp1 texp2 val1 in __POS__ None texp1 texp2 val1 in
let exe_one_prop prop = let exe_one_prop prop =
if Exp.equal texp2 Exp.zero then if Exp.equal texp2 Exp.zero then
[(return_result tenv Exp.zero prop ret_ids, path)] [(return_result tenv Exp.zero prop ret_id, path)]
else else
begin begin
try try
@ -264,7 +264,7 @@ let execute___instanceof_cast ~instof
let prop' = let prop' =
if Exp.equal texp1 texp1' then prop if Exp.equal texp1 texp1' then prop
else replace_ptsto_texp tenv prop val1 texp1' in else replace_ptsto_texp tenv prop val1 texp1' in
[(return_result tenv res_e prop' ret_ids, path)] in [(return_result tenv res_e prop' ret_id, path)] in
if instof then (* instanceof *) if instof then (* instanceof *)
begin begin
let pos_res = mk_res pos_type_opt Exp.one in let pos_res = mk_res pos_type_opt Exp.one in
@ -295,7 +295,7 @@ let execute___instanceof_cast ~instof
end end
| _ -> [] | _ -> []
with Not_found -> with Not_found ->
[(return_result tenv val1 prop ret_ids, path)] [(return_result tenv val1 prop ret_id, path)]
end in end in
let props = create_type tenv val1 typ1 prop in let props = create_type tenv val1 typ1 prop in
IList.flatten (IList.map exe_one_prop props) IList.flatten (IList.map exe_one_prop props)
@ -326,9 +326,9 @@ let set_resource_attribute tenv prop path n_lexp loc ra_res =
[(prop', path)] [(prop', path)]
(** Set the attibute of the value as file *) (** Set the attibute of the value as file *)
let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, _)], _ -> | [(lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
@ -336,9 +336,9 @@ let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; ar
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as lock *) (** Set the attibute of the value as lock *)
let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, _)], _ -> | [(lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
@ -347,9 +347,9 @@ let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; ar
(** Set the resource attribute of the first real argument of method as ignore, the first argument is (** Set the resource attribute of the first real argument of method as ignore, the first argument is
assumed to be "this" *) assumed to be "this" *)
let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [_ ; (lexp, _)], _ -> | [_ ; (lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
@ -357,9 +357,9 @@ let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; re
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as memory *) (** Set the attibute of the value as memory *)
let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, _)], _ -> | [(lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
@ -368,9 +368,9 @@ let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; arg
(** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *) (** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *)
let execute___check_untainted let execute___check_untainted
{ Builtin.tenv; pdesc; prop_; path; ret_ids; args; proc_name = callee_pname; } { Builtin.tenv; pdesc; prop_; path; ret_id; args; proc_name = callee_pname; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, _)], _ -> | [(lexp, _)], _ ->
let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv caller_pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv caller_pname lexp prop_ in
@ -378,7 +378,7 @@ let execute___check_untainted
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** take a pointer to a struct, and return the value of a hidden field in the struct *) (** take a pointer to a struct, and return the value of a hidden field in the struct *)
let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
@ -386,7 +386,7 @@ let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_ids; args
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
let ret_val = ref None in let ret_val = ref None in
let return_val p = match !ret_val with let return_val p = match !ret_val with
| Some e -> return_result tenv e p ret_ids | Some e -> return_result tenv e p ret_id
| None -> p in | None -> p in
let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in
let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in
@ -483,12 +483,12 @@ let get_suppress_npe_flag args =
false, args' (* this is a CFRelease/CFRetain *) false, args' (* this is a CFRelease/CFRetain *)
| _ -> true, args | _ -> true, args
let execute___objc_retain_impl ({ Builtin.tenv; prop_; args; ret_ids; } as builtin_args) let execute___objc_retain_impl ({ Builtin.tenv; prop_; args; ret_id; } as builtin_args)
: Builtin.ret_typ = : Builtin.ret_typ =
let mask_errors, args' = get_suppress_npe_flag args in let mask_errors, args' = get_suppress_npe_flag args in
match args' with match args' with
| [(lexp, _)] -> | [(lexp, _)] ->
let prop = return_result tenv lexp prop_ ret_ids in let prop = return_result tenv lexp prop_ ret_id in
execute___objc_counter_update execute___objc_counter_update
~mask_errors (Binop.PlusA) (IntLit.one) ~mask_errors (Binop.PlusA) (IntLit.one)
{ builtin_args with Builtin.prop_ = prop; args = args'; } { builtin_args with Builtin.prop_ = prop; args = args'; }
@ -525,12 +525,12 @@ let execute___objc_release_cf builtin_args
(** Set the attibute of the value as objc autoreleased *) (** Set the attibute of the value as objc autoreleased *)
let execute___set_autorelease_attribute let execute___set_autorelease_attribute
{ Builtin.tenv; pdesc; prop_; path; ret_ids; args; } { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_id with
| [(lexp, _)], _ -> | [(lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let prop = return_result tenv lexp prop_ ret_ids in let prop = return_result tenv lexp prop_ ret_id in
if Config.objc_memory_model_on then if Config.objc_memory_model_on then
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop in
let prop' = Attribute.add_or_replace tenv prop (Apred (Aautorelease, [n_lexp])) in let prop' = Attribute.add_or_replace tenv prop (Apred (Aautorelease, [n_lexp])) in
@ -640,10 +640,10 @@ let execute___set_untaint_attribute
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(val1_, _); (texp2_, _)] when IList.length ret_ids <= 1 -> | [(val1_, _); (texp2_, _)] ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in
let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in
@ -654,9 +654,9 @@ let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_ids; args; }
match hpred, texp2 with match hpred, texp2 with
| Sil.Hpointsto (val1, _, _), Exp.Sizeof _ -> | Sil.Hpointsto (val1, _, _), Exp.Sizeof _ ->
let prop' = replace_ptsto_texp tenv prop val1 texp2 in let prop' = replace_ptsto_texp tenv prop val1 texp2 in
[(return_result tenv val1 prop' ret_ids, path)] [(return_result tenv val1 prop' ret_id, path)]
| _ -> [(return_result tenv val1 prop ret_ids, path)] | _ -> [(return_result tenv val1 prop ret_id, path)]
with Not_found -> [(return_result tenv val1 prop ret_ids, path)]) with Not_found -> [(return_result tenv val1 prop ret_id, path)])
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_abort { Builtin.proc_name; } let execute_abort { Builtin.proc_name; }
@ -731,7 +731,7 @@ let execute_free mk { Builtin.pdesc; instr; tenv; prop_; path; args; loc; }
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_alloc mk can_return_null let execute_alloc mk can_return_null
{ Builtin.pdesc; tenv; prop_; path; ret_ids; args; loc; } { Builtin.pdesc; tenv; prop_; path; ret_id; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let rec evaluate_char_sizeof e = match e with let rec evaluate_char_sizeof e = match e with
@ -760,8 +760,8 @@ let execute_alloc mk can_return_null
size_exp, pname size_exp, pname
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) in raise (Exceptions.Wrong_argument_number __POS__) in
let ret_id = match ret_ids with let ret_id = match ret_id with
| [ret_id] -> ret_id | Some (ret_id, _) -> ret_id
| _ -> Ident.create_fresh Ident.kprimed in | _ -> Ident.create_fresh Ident.kprimed in
let size_exp', prop = let size_exp', prop =
let n_size_exp, prop = check_arith_norm_exp tenv pname size_exp prop_ in let n_size_exp, prop = check_arith_norm_exp tenv pname size_exp prop_ in
@ -854,7 +854,7 @@ let execute_scan_function skip_n_arguments ({ Builtin.args } as call_args)
{ call_args with args = !varargs } { call_args with args = !varargs }
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(ret_exn, _)] -> | [(ret_exn, _)] ->
@ -863,23 +863,23 @@ let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_ids; args;
let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in
match n_ret_exn with match n_ret_exn with
| Exp.Exn exp -> | Exp.Exn exp ->
let prop_with_exn = return_result tenv exp prop ret_ids in let prop_with_exn = return_result tenv exp prop ret_id in
[(prop_with_exn, path)] [(prop_with_exn, path)]
| _ -> assert false | _ -> assert false
end end
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_return_first_argument { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute_return_first_argument { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| (arg1_, _):: _ -> | (arg1_, _):: _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in
let prop' = return_result tenv arg1 prop ret_ids in let prop' = return_result tenv arg1 prop ret_id in
[(prop', path)] [(prop', path)]
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_id; args; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp1, _); (lexp2, _); (lexp3, _)] -> | [(lexp1, _); (lexp2, _); (lexp3, _)] ->
@ -894,7 +894,7 @@ let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_ids; args; }
let parts = Str.split (Str.regexp_string str2) str1 in let parts = Str.split (Str.regexp_string str2) str1 in
let n_part = IList.nth parts n in let n_part = IList.nth parts n in
let res = Exp.Const (Const.Cstr n_part) in let res = Exp.Const (Const.Cstr n_part) in
[(return_result tenv res prop ret_ids, path)] [(return_result tenv res prop ret_id, path)]
with Not_found -> assert false) with Not_found -> assert false)
| _ -> [(prop, path)]) | _ -> [(prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -1140,7 +1140,7 @@ let _ = Builtin.register
let execute_objc_alloc_no_fail let execute_objc_alloc_no_fail
symb_state typ alloc_fun_opt symb_state typ alloc_fun_opt
{ Builtin.pdesc; tenv; ret_ids; loc; } = { Builtin.pdesc; tenv; ret_id; loc; } =
let alloc_fun = Exp.Const (Const.Cfun __objc_alloc_no_fail) in let alloc_fun = Exp.Const (Const.Cfun __objc_alloc_no_fail) in
let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in
let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in
@ -1150,7 +1150,7 @@ let execute_objc_alloc_no_fail
| None -> [] in | None -> [] in
let alloc_instr = let alloc_instr =
Sil.Call Sil.Call
(ret_ids, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in (ret_id, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in
SymExec.instrs tenv pdesc [alloc_instr] symb_state SymExec.instrs tenv pdesc [alloc_instr] symb_state
let mk_objc_class_method class_name method_name = let mk_objc_class_method class_name method_name =

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

@ -24,7 +24,7 @@ let add_dispatch_calls pdesc cg tenv =
let has_dispatch_call instrs = let has_dispatch_call instrs =
IList.exists instr_is_dispatch_call instrs in IList.exists instr_is_dispatch_call instrs in
let replace_dispatch_calls = function let replace_dispatch_calls = function
| Sil.Call (ret_ids, (Exp.Const (Const.Cfun callee_pname) as call_exp), | Sil.Call (ret_id, (Exp.Const (Const.Cfun callee_pname) as call_exp),
(((_, receiver_typ) :: _) as args), loc, call_flags) as instr (((_, receiver_typ) :: _) as args), loc, call_flags) as instr
when call_flags_is_dispatch call_flags -> when call_flags_is_dispatch call_flags ->
(* the frontend should not populate the list of targets *) (* the frontend should not populate the list of targets *)
@ -50,7 +50,7 @@ let add_dispatch_calls pdesc cg tenv =
(fun target_pname -> Cg.add_edge cg caller_pname target_pname) (fun target_pname -> Cg.add_edge cg caller_pname target_pname)
targets_to_add; targets_to_add;
let call_flags' = { call_flags with CallFlags.cf_targets = targets_to_add; } in let call_flags' = { call_flags with CallFlags.cf_targets = targets_to_add; } in
Sil.Call (ret_ids, call_exp, args, loc, call_flags') Sil.Call (ret_id, call_exp, args, loc, call_flags')
| [] -> instr) | [] -> instr)
| instr -> instr in | instr -> instr in
@ -136,12 +136,12 @@ module NullifyTransferFunctions = struct
let astate' = match instr with let astate' = match instr with
| Sil.Load (lhs_id, _, _, _) -> | Sil.Load (lhs_id, _, _, _) ->
VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify
| Sil.Call (lhs_ids, _, _, _, _) -> | Sil.Call (lhs_id, _, _, _, _) ->
let active_defs' = let active_defs' =
IList.fold_left Option.map_default
(fun acc id -> VarDomain.add (Var.of_id id) acc) (fun (id, _) -> VarDomain.add (Var.of_id id) active_defs)
active_defs active_defs
lhs_ids in lhs_id in
active_defs', to_nullify active_defs', to_nullify
| Sil.Store (Exp.Lvar lhs_pvar, _, _, _) -> | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) ->
VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify

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

@ -710,7 +710,7 @@ let call_constructor_url_update_args pname actual_params =
(* 2. We don't know, but obj could be null, we return both options, *) (* 2. We don't know, but obj could be null, we return both options, *)
(* (obj = null, res = null), (obj != null, res = [obj foo]) *) (* (obj = null, res = null), (obj != null, res = [obj foo]) *)
(* We want the same behavior even when we are going to skip the function. *) (* We want the same behavior even when we are going to skip the function. *)
let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_ids res = let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_id res =
let path_description = let path_description =
"Message " ^ "Message " ^
(Procname.to_simplified_string callee_pname) ^ (Procname.to_simplified_string callee_pname) ^
@ -728,8 +728,8 @@ let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname
Option.is_some (Attribute.get_objc_null tenv pre e) -> true Option.is_some (Attribute.get_objc_null tenv pre e) -> true
| _ -> false in | _ -> false in
let add_objc_null_attribute_or_nullify_result prop = let add_objc_null_attribute_or_nullify_result prop =
match ret_ids with match ret_id with
| [ret_id] -> ( | Some (ret_id, _) -> (
match Attribute.find_equal_formal_path tenv receiver prop with match Attribute.find_equal_formal_path tenv receiver prop with
| Some vfs -> | Some vfs ->
Attribute.add_or_replace tenv prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs])) Attribute.add_or_replace tenv prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
@ -766,10 +766,10 @@ let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname
(* This method handles ObjC instance method calls, in particular the fact that calling a method *) (* This method handles ObjC instance method calls, in particular the fact that calling a method *)
(* with nil returns nil. The exec_call function is either standard call execution or execution *) (* with nil returns nil. The exec_call function is either standard call execution or execution *)
(* of ObjC getters and setters using a builtin. *) (* of ObjC getters and setters using a builtin. *)
let handle_objc_instance_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname let handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname
loc path exec_call = loc path exec_call =
let res () = exec_call tenv ret_ids pdesc callee_pname loc actual_params pre path in let res () = exec_call tenv ret_id pdesc callee_pname loc actual_params pre path in
handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_ids res handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_id res
let normalize_params tenv pdesc prop actual_params = let normalize_params tenv pdesc prop actual_params =
let norm_arg (p, args) (e, t) = let norm_arg (p, args) (e, t) =
@ -1006,7 +1006,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
Sil.Call (ret, exp', par, loc, call_flags) in Sil.Call (ret, exp', par, loc, call_flags) in
instr' instr'
| _ -> _instr in | _ -> _instr in
let skip_call ?(is_objc_instance_method=false) prop path callee_pname ret_annots loc ret_ids let skip_call ?(is_objc_instance_method=false) prop path callee_pname ret_annots loc ret_id
ret_typ_opt actual_args = ret_typ_opt actual_args =
let skip_res () = let skip_res () =
let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
@ -1021,13 +1021,14 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
summary.Specs.stats.Specs.call_stats callee_pname loc summary.Specs.stats.Specs.call_stats callee_pname loc
(Specs.CallStats.CR_skip) !Config.footprint); (Specs.CallStats.CR_skip) !Config.footprint);
unknown_or_scan_call ~is_scan:false ret_typ_opt ret_annots Builtin.{ unknown_or_scan_call ~is_scan:false ret_typ_opt ret_annots Builtin.{
pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_ids; args= actual_args; pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_id; args= actual_args;
proc_name= callee_pname; loc; } in proc_name= callee_pname; loc; } in
if is_objc_instance_method then if is_objc_instance_method then
handle_objc_instance_method_call_or_skip tenv actual_args path callee_pname prop ret_ids skip_res handle_objc_instance_method_call_or_skip
tenv actual_args path callee_pname prop ret_id skip_res
else skip_res () in else skip_res () in
let call_args prop_ proc_name args ret_ids loc = { let call_args prop_ proc_name args ret_id loc = {
Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_ids; args; proc_name; loc; } in Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_id; args; proc_name; loc; } in
match instr with match instr with
| Sil.Load (id, rhs_exp, typ, loc) -> | Sil.Load (id, rhs_exp, typ, loc) ->
execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_ execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_
@ -1062,17 +1063,17 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
check_condition_always_true_false (); check_condition_always_true_false ();
let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in
ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop))
| Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), args, loc, _) | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), args, loc, _)
when Builtin.is_registered callee_pname -> when Builtin.is_registered callee_pname ->
let sym_exe_builtin = Builtin.get callee_pname in let sym_exe_builtin = Builtin.get callee_pname in
sym_exe_builtin (call_args prop_ callee_pname args ret_ids loc) sym_exe_builtin (call_args prop_ callee_pname args ret_id loc)
| Sil.Call (ret_ids, | Sil.Call (ret_id,
Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
actual_params, loc, call_flags) actual_params, loc, call_flags)
when Config.lazy_dynamic_dispatch -> when Config.lazy_dynamic_dispatch ->
let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in
let exec_skip_call skipped_pname ret_annots ret_type = let exec_skip_call skipped_pname ret_annots ret_type =
skip_call norm_prop path skipped_pname ret_annots loc ret_ids (Some ret_type) norm_args in skip_call norm_prop path skipped_pname ret_annots loc ret_id (Some ret_type) norm_args in
let resolved_pname, summary_opt = let resolved_pname, summary_opt =
resolve_and_analyze tenv current_pdesc norm_prop norm_args callee_pname call_flags in resolve_and_analyze tenv current_pdesc norm_prop norm_args callee_pname call_flags in
begin begin
@ -1086,10 +1087,10 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
exec_skip_call resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type exec_skip_call resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
| Some summary -> | Some summary ->
proc_call summary (call_args prop_ callee_pname norm_args ret_ids loc) proc_call summary (call_args prop_ callee_pname norm_args ret_id loc)
end end
| Sil.Call (ret_ids, | Sil.Call (ret_id,
Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
actual_params, loc, call_flags) -> actual_params, loc, call_flags) ->
do_error_checks tenv (Paths.Path.curr_node path) instr current_pname current_pdesc; do_error_checks tenv (Paths.Path.curr_node path) instr current_pname current_pdesc;
@ -1101,7 +1102,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let exec_one_pname pname = let exec_one_pname pname =
Ondemand.analyze_proc_name tenv ~propagate_exceptions:true current_pdesc pname; Ondemand.analyze_proc_name tenv ~propagate_exceptions:true current_pdesc pname;
let exec_skip_call ret_annots ret_type = let exec_skip_call ret_annots ret_type =
skip_call norm_prop path pname ret_annots loc ret_ids (Some ret_type) url_handled_args in skip_call norm_prop path pname ret_annots loc ret_id (Some ret_type) url_handled_args in
match Specs.get_summary pname with match Specs.get_summary pname with
| None -> | None ->
let ret_typ = Typ.java_proc_return_typ callee_pname_java in let ret_typ = Typ.java_proc_return_typ callee_pname_java in
@ -1112,10 +1113,10 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
exec_skip_call ret_annots proc_attrs.ProcAttributes.ret_type exec_skip_call ret_annots proc_attrs.ProcAttributes.ret_type
| Some summary -> | Some summary ->
proc_call summary (call_args norm_prop pname url_handled_args ret_ids loc) in proc_call summary (call_args norm_prop pname url_handled_args ret_id loc) in
IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames
| Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) ->
(* Generic fun call with known name *) (* Generic fun call with known name *)
let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in
let resolved_pname = let resolved_pname =
@ -1131,7 +1132,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let sentinel_result = let sentinel_result =
if !Config.curr_language = Config.Clang then if !Config.curr_language = Config.Clang then
check_variadic_sentinel_if_present check_variadic_sentinel_if_present
(call_args prop_r callee_pname actual_params ret_ids loc) (call_args prop_r callee_pname actual_params ret_id loc)
else [(prop_r, path)] in else [(prop_r, path)] in
let do_call (prop, path) = let do_call (prop, path) =
let summary = Specs.get_summary resolved_pname in let summary = Specs.get_summary resolved_pname in
@ -1157,7 +1158,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
match objc_property_accessor_ret_typ_opt with match objc_property_accessor_ret_typ_opt with
| Some (objc_property_accessor, ret_typ) -> | Some (objc_property_accessor, ret_typ) ->
handle_objc_instance_method_call handle_objc_instance_method_call
n_actual_params n_actual_params prop tenv ret_ids n_actual_params n_actual_params prop tenv ret_id
current_pdesc callee_pname loc path current_pdesc callee_pname loc path
(sym_exec_objc_accessor objc_property_accessor ret_typ) (sym_exec_objc_accessor objc_property_accessor ret_typ)
| None -> | None ->
@ -1171,13 +1172,13 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
match attrs_opt with match attrs_opt with
| Some attrs -> attrs.ProcAttributes.is_objc_instance_method | Some attrs -> attrs.ProcAttributes.is_objc_instance_method
| None -> false in | None -> false in
skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_ids skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_id
ret_typ_opt n_actual_params ret_typ_opt n_actual_params
else else
proc_call (Option.get summary) proc_call (Option.get summary)
(call_args prop resolved_pname n_actual_params ret_ids loc) in (call_args prop resolved_pname n_actual_params ret_id loc) in
IList.flatten (IList.map do_call sentinel_result) IList.flatten (IList.map do_call sentinel_result)
| Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (* Call via function pointer *) | Sil.Call (ret_id, fun_exp, actual_params, loc, call_flags) -> (* Call via function pointer *)
let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in
if call_flags.CallFlags.cf_is_objc_block then if call_flags.CallFlags.cf_is_objc_block then
Rearrange.check_call_to_objc_block_error tenv current_pdesc prop_r fun_exp loc; Rearrange.check_call_to_objc_block_error tenv current_pdesc prop_r fun_exp loc;
@ -1191,7 +1192,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
L.d_strln ", returning undefined value."; L.d_strln ", returning undefined value.";
let callee_pname = Procname.from_string_c_fun "__function_pointer__" in let callee_pname = Procname.from_string_c_fun "__function_pointer__" in
unknown_or_scan_call ~is_scan:false None Annot.Item.empty Builtin.{ unknown_or_scan_call ~is_scan:false None Annot.Item.empty Builtin.{
pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_ids; args= n_actual_params; pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_id; args= n_actual_params;
proc_name= callee_pname; loc; } proc_name= callee_pname; loc; }
end end
| Sil.Nullify (pvar, _) -> | Sil.Nullify (pvar, _) ->
@ -1381,7 +1382,7 @@ and check_untainted tenv exp taint_kind caller_pname callee_pname prop =
(** execute a call for an unknown or scan function *) (** execute a call for an unknown or scan function *)
and unknown_or_scan_call ~is_scan ret_type_option ret_annots and unknown_or_scan_call ~is_scan ret_type_option ret_annots
{ Builtin.tenv; pdesc; prop_= pre; path; ret_ids; { Builtin.tenv; pdesc; prop_= pre; path; ret_id;
args; proc_name= callee_pname; loc; instr; } = args; proc_name= callee_pname; loc; instr; } =
let remove_file_attribute prop = let remove_file_attribute prop =
let do_exp p (e, _) = let do_exp p (e, _) =
@ -1428,8 +1429,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
if Procname.is_java callee_pname if Procname.is_java callee_pname
then remove_file_attribute pre then remove_file_attribute pre
else pre in else pre in
let pre_2 = match ret_ids, ret_type_option with let pre_2 = match ret_id, ret_type_option with
| [ret_id], Some ret_typ -> | Some (ret_id, _), Some ret_typ ->
(* TODO(jjb): Should this use the type of ret_id, or ret_type from the procedure type? *)
add_constraints_on_retval tenv add_constraints_on_retval tenv
pdesc pre_1 (Exp.Var ret_id) ret_typ ~has_nullable_annot callee_pname loc pdesc pre_1 (Exp.Var ret_id) ret_typ ~has_nullable_annot callee_pname loc
| _ -> | _ ->
@ -1442,7 +1444,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
else else
(* otherwise, add undefined attribute to retvals and actuals passed by ref *) (* otherwise, add undefined attribute to retvals and actuals passed by ref *)
let exps_to_mark = let exps_to_mark =
let ret_exps = IList.map (fun ret_id -> Exp.Var ret_id) ret_ids in let ret_exps = Option.map_default (fun (id, _) -> [Exp.Var id]) [] ret_id in
IList.fold_left IList.fold_left
(fun exps_to_mark (exp, _, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in (fun exps_to_mark (exp, _, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in
let prop_with_undef_attr = let prop_with_undef_attr =
@ -1501,13 +1503,13 @@ and check_variadic_sentinel_if_present
let formals = callee_attributes.ProcAttributes.formals in let formals = callee_attributes.ProcAttributes.formals in
check_variadic_sentinel (IList.length formals) sentinel_arg builtin_args check_variadic_sentinel (IList.length formals) sentinel_arg builtin_args
and sym_exec_objc_getter field_name ret_typ tenv ret_ids pdesc pname loc args prop = and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args prop =
L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^ L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^
(Ident.fieldname_to_string field_name)^"."); (Ident.fieldname_to_string field_name)^".");
let ret_id = let ret_id =
match ret_ids with match ret_id with
| [ret_id] -> ret_id | Some (ret_id, _) -> ret_id
| _ -> assert false in | None -> assert false in
match args with match args with
| [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] -> | [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] ->
let field_access_exp = Exp.Lfield (lexp, field_name, typ) in let field_access_exp = Exp.Lfield (lexp, field_name, typ) in
@ -1524,7 +1526,7 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop =
execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_accessor property_accesor ret_typ tenv ret_ids pdesc _ loc args prop path and sym_exec_objc_accessor property_accesor ret_typ tenv ret_id pdesc _ loc args prop path
: Builtin.ret_typ = : Builtin.ret_typ =
let f_accessor = let f_accessor =
match property_accesor with match property_accesor with
@ -1533,25 +1535,24 @@ and sym_exec_objc_accessor property_accesor ret_typ tenv ret_ids pdesc _ loc arg
(* we want to execute in the context of the current procedure, not in the context of callee_pname, (* we want to execute in the context of the current procedure, not in the context of callee_pname,
since this is the procname of the setter/getter method *) since this is the procname of the setter/getter method *)
let cur_pname = Cfg.Procdesc.get_proc_name pdesc in let cur_pname = Cfg.Procdesc.get_proc_name pdesc in
f_accessor ret_typ tenv ret_ids pdesc cur_pname loc args prop f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop
|> IList.map (fun p -> (p, path)) |> IList.map (fun p -> (p, path))
(** Perform symbolic execution for a function call *) (** Perform symbolic execution for a function call *)
and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= actual_pars; loc; } = and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc; } =
let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
let callee_pname = Specs.get_proc_name summary in let callee_pname = Specs.get_proc_name summary in
let ret_typ = Specs.get_ret_type summary in let ret_typ = Specs.get_ret_type summary in
let check_return_value_ignored () = let check_return_value_ignored () =
(* check if the return value of the call is ignored, and issue a warning *) (* check if the return value of the call is ignored, and issue a warning *)
let is_ignored = match ret_typ, ret_ids with let is_ignored = match ret_typ, ret_id with
| Typ.Tvoid, _ -> false | Typ.Tvoid, _ -> false
| Typ.Tint _, _ when not (proc_is_defined callee_pname) -> | Typ.Tint _, _ when not (proc_is_defined callee_pname) ->
(* if the proc returns Tint and is not defined, *) (* if the proc returns Tint and is not defined, *)
(* don't report ignored return value *) (* don't report ignored return value *)
false false
| _, [] -> true | _, None -> true
| _, [id] -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id | _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in
| _ -> false in
if is_ignored if is_ignored
&& Specs.get_flag callee_pname proc_flag_ignore_return = None then && Specs.get_flag callee_pname proc_flag_ignore_return = None then
let err_desc = Localise.desc_return_value_ignored callee_pname loc in let err_desc = Localise.desc_return_value_ignored callee_pname loc in
@ -1593,11 +1594,11 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act
let callee_attrs = Specs.get_attributes summary in let callee_attrs = Specs.get_attributes summary in
if (!Config.curr_language <> Config.Java) && if (!Config.curr_language <> Config.Java) &&
(Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then
handle_objc_instance_method_call actual_pars actual_params pre tenv ret_ids pdesc handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc
callee_pname loc path (Tabulation.exe_function_call callee_attrs) callee_pname loc path (Tabulation.exe_function_call callee_attrs)
else (* non-objective-c method call. Standard tabulation *) else (* non-objective-c method call. Standard tabulation *)
Tabulation.exe_function_call Tabulation.exe_function_call
callee_attrs tenv ret_ids pdesc callee_pname loc actual_params pre path callee_attrs tenv ret_id pdesc callee_pname loc actual_params pre path
end end
(** perform symbolic execution for a single prop, and check for junk *) (** perform symbolic execution for a single prop, and check for junk *)

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

@ -671,7 +671,7 @@ let include_subtrace callee_pname =
(** combine the spec's post with a splitting and actual precondition *) (** combine the spec's post with a splitting and actual precondition *)
let combine tenv let combine tenv
ret_ids (posts: ('a Prop.t * Paths.Path.t) list) ret_id (posts: ('a Prop.t * Paths.Path.t) list)
actual_pre path_pre split actual_pre path_pre split
caller_pdesc callee_pname loc = caller_pdesc callee_pname loc =
let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in
@ -751,25 +751,27 @@ let combine tenv
match Prop.prop_iter_find iter filter with match Prop.prop_iter_find iter filter with
| None -> post_p2 | None -> post_p2
| Some iter' -> | Some iter' ->
match fst (Prop.prop_iter_current tenv iter') with match fst (Prop.prop_iter_current tenv iter'), ret_id with
| Sil.Hpointsto (_, Sil.Eexp (e', inst), _) when exp_is_exn e' -> | Sil.Hpointsto (_, Sil.Eexp (e', inst), _), _ when exp_is_exn e' ->
(* resuls is an exception: set in caller *) (* resuls is an exception: set in caller *)
let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in
prop_set_exn tenv caller_pname p (Sil.Eexp (e', inst)) prop_set_exn tenv caller_pname p (Sil.Eexp (e', inst))
| Sil.Hpointsto (_, Sil.Eexp (e', _), _) when IList.length ret_ids = 1 -> | Sil.Hpointsto (_, Sil.Eexp (e', _), _), Some (id, _) ->
let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in
Prop.conjoin_eq tenv e' (Exp.Var (IList.hd ret_ids)) p Prop.conjoin_eq tenv e' (Exp.Var id) p
| Sil.Hpointsto (_, Sil.Estruct (ftl, _), _) | Sil.Hpointsto (_, Sil.Estruct (ftl, _), _), _
when IList.length ftl = IList.length ret_ids -> when IList.length ftl = (if ret_id = None then 0 else 1) ->
(* TODO(jjb): Is this case dead? *)
let rec do_ftl_ids p = function let rec do_ftl_ids p = function
| [], [] -> p | [], None -> p
| (_, Sil.Eexp (e', _)):: ftl', ret_id:: ret_ids' -> | (_, Sil.Eexp (e', _)) :: ftl', Some (ret_id, _) ->
let p' = Prop.conjoin_eq tenv e' (Exp.Var ret_id) p in let p' = Prop.conjoin_eq tenv e' (Exp.Var ret_id) p in
do_ftl_ids p' (ftl', ret_ids') do_ftl_ids p' (ftl', None)
| _ -> p in | _ -> p in
let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in
do_ftl_ids p (ftl, ret_ids) do_ftl_ids p (ftl, ret_id)
| Sil.Hpointsto _ -> (* returning nothing or unexpected sexp, turning into nondet *) | Sil.Hpointsto _, _ ->
(* returning nothing or unexpected sexp, turning into nondet *)
Prop.prop_iter_remove_curr_then_to_prop tenv iter' Prop.prop_iter_remove_curr_then_to_prop tenv iter'
| _ -> assert false in | _ -> assert false in
let post_p4 = let post_p4 =
@ -875,9 +877,9 @@ let mk_actual_precondition tenv prop actual_params formal_params =
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
let mk_posts tenv ret_ids prop callee_pname callee_attrs posts = let mk_posts tenv ret_id prop callee_pname callee_attrs posts =
match ret_ids with match ret_id with
| [ret_id] -> | Some (ret_id, _) ->
let mk_getter_idempotent posts = let mk_getter_idempotent posts =
(* if we have seen a previous call to the same function, only use specs whose return value (* if we have seen a previous call to the same function, only use specs whose return value
is consistent with constraints on the return value of the previous call w.r.t to is consistent with constraints on the return value of the previous call w.r.t to
@ -1005,10 +1007,10 @@ let check_uninitialize_dangling_deref tenv callee_pname actual_pre sub formal_pa
(** Perform symbolic execution for a single spec *) (** Perform symbolic execution for a single spec *)
let exe_spec let exe_spec
tenv ret_ids (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre tenv ret_id (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre
(spec : Prop.exposed Specs.spec) actual_params formal_params : abduction_res = (spec : Prop.exposed Specs.spec) actual_params formal_params : abduction_res =
let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in
let posts = mk_posts tenv ret_ids prop callee_pname callee_attrs spec.Specs.posts in let posts = mk_posts tenv ret_id prop callee_pname callee_attrs spec.Specs.posts in
let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in
let spec_pre = let spec_pre =
mk_pre tenv (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname callee_attrs in mk_pre tenv (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname callee_attrs in
@ -1036,7 +1038,7 @@ let exe_spec
frame_fld missing_fld frame_typ missing_typ in frame_fld missing_fld frame_typ missing_typ in
let report_valid_res split = let report_valid_res split =
match combine tenv match combine tenv
ret_ids posts ret_id posts
actual_pre path_pre split actual_pre path_pre split
caller_pdesc callee_pname loc with caller_pdesc callee_pname loc with
| None -> Invalid_res Cannot_combine | None -> Invalid_res Cannot_combine
@ -1123,7 +1125,7 @@ let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t =
Prop.normalize tenv (Prop.set p ~pi_fp:(p.Prop.pi_fp @ new_footprint_atoms)) Prop.normalize tenv (Prop.set p ~pi_fp:(p.Prop.pi_fp @ new_footprint_atoms))
(** post-process the raw result of a function call *) (** post-process the raw result of a function call *)
let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc results = let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results =
let filter_valid_res = function let filter_valid_res = function
| Invalid_res _ -> false | Invalid_res _ -> false
| Valid_res _ -> true in | Valid_res _ -> true in
@ -1258,8 +1260,8 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc r
!Config.curr_language = Config.Java && !Config.curr_language = Config.Java &&
is_likely_getter callee_pname) is_likely_getter callee_pname)
|| returns_nullable ret_annot in || returns_nullable ret_annot in
match ret_ids with match ret_id with
| [ret_id] when should_add_ret_attr ()-> | Some (ret_id, _) when should_add_ret_attr () ->
(* add attribute to remember what function call a return id came from *) (* add attribute to remember what function call a return id came from *)
let ret_var = Exp.Var ret_id in let ret_var = Exp.Var ret_id in
let mark_id_as_retval (p, path) = let mark_id_as_retval (p, path) =
@ -1270,7 +1272,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc r
(** Execute the function call and return the list of results with return value *) (** Execute the function call and return the list of results with return value *)
let exe_function_call let exe_function_call
callee_attrs tenv ret_ids caller_pdesc callee_pname loc actual_params prop path = callee_attrs tenv ret_id caller_pdesc callee_pname loc actual_params prop path =
let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in
let trace_call res = let trace_call res =
match Specs.get_summary caller_pname with match Specs.get_summary caller_pname with
@ -1290,7 +1292,7 @@ let exe_function_call
let exe_one_spec (n, spec) = let exe_one_spec (n, spec) =
exe_spec exe_spec
tenv tenv
ret_ids ret_id
(n, nspecs) (n, nspecs)
caller_pdesc caller_pdesc
callee_pname callee_pname
@ -1302,7 +1304,7 @@ let exe_function_call
actual_params actual_params
formal_params in formal_params in
let results = IList.map exe_one_spec spec_list in let results = IList.map exe_one_spec spec_list in
exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc results exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results
(* (*
let check_splitting_precondition sub1 sub2 = let check_splitting_precondition sub1 sub2 =

4
infer/src/backend/tabulation.mli
Unescape View File

@ -44,6 +44,6 @@ val d_splitting : splitting -> unit
(** Execute the function call and return the list of results with return value *) (** Execute the function call and return the list of results with return value *)
val exe_function_call: val exe_function_call:
ProcAttributes.t -> Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> ProcAttributes.t -> Tenv.t -> (Ident.t * Typ.t) option -> Cfg.Procdesc.t -> Procname.t ->
(Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t -> Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t ->
(Prop.normal Prop.t * Paths.Path.t) list (Prop.normal Prop.t * Paths.Path.t) list

6
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -326,7 +326,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
Annot.Map.fold add_call_for_annot map astate Annot.Map.fold add_call_for_annot map astate
let exec_instr astate { ProcData.pdesc; tenv; } _ = function let exec_instr astate { ProcData.pdesc; tenv; } _ = function
| Sil.Call ([id], Const (Cfun callee_pname), _, _, _) | Sil.Call (Some (id, _), Const (Cfun callee_pname), _, _, _)
when is_unlikely callee_pname -> when is_unlikely callee_pname ->
Domain.add_tracking_var (Var.of_id id) astate Domain.add_tracking_var (Var.of_id id) astate
| Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) ->
@ -353,8 +353,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Sil.Prune (exp, _, _, _) | Sil.Prune (exp, _, _, _)
when prunes_tracking_var astate exp -> when prunes_tracking_var astate exp ->
Domain.stop_tracking astate Domain.stop_tracking astate
| Sil.Call (_::_, _, _, _, _) -> | Sil.Call (None, _, _, _, _) ->
failwith "Expecting a singleton for the return value" failwith "Expecting a return identifier"
| _ -> | _ ->
astate astate
end end

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

@ -455,7 +455,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
| Exp.Const (Const.Cclass n) -> Ident.name_to_string n | Exp.Const (Const.Cclass n) -> Ident.name_to_string n
| Exp.Lvar _ -> ( | Exp.Lvar _ -> (
let is_call_instr set call = match set, call with let is_call_instr set call = match set, call with
| Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (i2::[], _, _, _, _) | Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (Some (i2, _), _, _, _, _)
when Ident.equal i1 i2 -> true when Ident.equal i1 i2 -> true
| _ -> false in | _ -> false in
let is_set_instr = function let is_set_instr = function

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

@ -84,13 +84,13 @@ module ConstantFlow = Dataflow.MakeDF(struct
&& has_method pn "<init>" -> (* StringBuilder.<init> *) && has_method pn "<init>" -> (* StringBuilder.<init> *)
update (Exp.Var sb) (Some (Const.Cstr "")) constants update (Exp.Var sb) (Some (Const.Cstr "")) constants
| Sil.Call (i:: [], Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: [], _, _) | Sil.Call (Some (i, _), Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: [], _, _)
when has_class pn "java.lang.StringBuilder" when has_class pn "java.lang.StringBuilder"
&& has_method pn "toString" -> (* StringBuilder.toString *) && has_method pn "toString" -> (* StringBuilder.toString *)
update (Exp.Var i) (ConstantMap.find (Exp.Var i1) constants) constants update (Exp.Var i) (ConstantMap.find (Exp.Var i1) constants) constants
| Sil.Call | Sil.Call
(i:: [], Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: (Exp.Var i2, _):: [], _, _) (Some (i, _), Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: (Exp.Var i2, _):: [], _, _)
when has_class pn "java.lang.StringBuilder" when has_class pn "java.lang.StringBuilder"
&& has_method pn "append" -> (* StringBuilder.append *) && has_method pn "append" -> (* StringBuilder.append *)
(match (match

8
infer/src/checkers/copyPropagation.ml
Unescape View File

@ -97,13 +97,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Sil.Store (Var _, _, _, _) -> | Sil.Store (Var _, _, _, _) ->
(* *lhs = rhs. not a copy, and not a write to lhs *) (* *lhs = rhs. not a copy, and not a write to lhs *)
astate astate
| Sil.Call (ret_ids, _, actuals, _, _) -> | Sil.Call (ret_id, _, actuals, _, _) ->
let kill_ret_ids astate_acc id = let kill_ret_id (id,_) =
Domain.kill_copies_with_var (Var.of_id id) astate_acc in Domain.kill_copies_with_var (Var.of_id id) astate in
let kill_actuals_by_ref astate_acc = function let kill_actuals_by_ref astate_acc = function
| (Exp.Lvar pvar, Typ.Tptr _) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc | (Exp.Lvar pvar, Typ.Tptr _) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc
| _ -> astate_acc in | _ -> astate_acc in
let astate' = IList.fold_left kill_ret_ids astate ret_ids in let astate' = Option.map_default kill_ret_id astate ret_id in
if !Config.curr_language = Config.Java if !Config.curr_language = Config.Java
then astate' (* Java doesn't have pass-by-reference *) then astate' (* Java doesn't have pass-by-reference *)
else IList.fold_left kill_actuals_by_ref astate' actuals else IList.fold_left kill_actuals_by_ref astate' actuals

8
infer/src/checkers/liveness.ml
Unescape View File

@ -45,11 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|> exp_add_live rhs_exp |> exp_add_live rhs_exp
| Sil.Prune (exp, _, _, _) -> | Sil.Prune (exp, _, _, _) ->
exp_add_live exp astate exp_add_live exp astate
| Sil.Call (ret_ids, call_exp, params, _, _) -> | Sil.Call (ret_id, call_exp, params, _, _) ->
IList.fold_right Option.map_default (fun (ret_id, _) -> Domain.remove (Var.of_id ret_id) astate)
(fun ret_id astate_acc -> Domain.remove (Var.of_id ret_id) astate_acc) astate ret_id
ret_ids
astate
|> exp_add_live call_exp |> exp_add_live call_exp
|> IList.fold_right exp_add_live (IList.map fst params) |> IList.fold_right exp_add_live (IList.map fst params)
| Sil.Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> | Sil.Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->

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

@ -145,7 +145,7 @@ let get_vararg_type_names tenv
(* Is this the node creating ivar? *) (* Is this the node creating ivar? *)
let rec initializes_array instrs = let rec initializes_array instrs =
match instrs with match instrs with
| Sil.Call ([t1], Exp.Const (Const.Cfun pn), _, _, _):: | Sil.Call (Some (t1, _), Exp.Const (Const.Cfun pn), _, _, _)::
Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _):: is -> Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _):: is ->
(Pvar.equal ivar iv && Ident.equal t1 t2 && (Pvar.equal ivar iv && Ident.equal t1 t2 &&
Procname.equal pn (Procname.from_string_c_fun "__new_array")) Procname.equal pn (Procname.from_string_c_fun "__new_array"))

6
infer/src/checkers/repeatedCallsChecker.ml
Unescape View File

@ -118,10 +118,10 @@ struct
IList.for_all filter_arg args in IList.for_all filter_arg args in
match instr with match instr with
| Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), _, loc, call_flags) | Sil.Call (Some _ as ret_id, Exp.Const (Const.Cfun callee_pname), _, loc, call_flags)
when ret_ids <> [] && arguments_not_temp normalized_etl -> when arguments_not_temp normalized_etl ->
let instr_normalized_args = Sil.Call ( let instr_normalized_args = Sil.Call (
ret_ids, ret_id,
Exp.Const (Const.Cfun callee_pname), Exp.Const (Const.Cfun callee_pname),
normalized_etl, normalized_etl,
loc, loc,

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

@ -27,7 +27,7 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in
let mk_call procname e t = let mk_call procname e t =
let bi_retain = Exp.Const (Const.Cfun procname) in let bi_retain = Exp.Const (Const.Cfun procname) in
Sil.Call([], bi_retain, [(e, t)], loc, CallFlags.default) in Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in
match typ with match typ with
| Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl -> | Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl ->
(* for __strong e1 = e2 the semantics is*) (* for __strong e1 = e2 the semantics is*)

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

@ -82,10 +82,10 @@ struct
not (CTrans_utils.is_owning_name method_name) && not (CTrans_utils.is_owning_name method_name) &&
ObjcInterface_decl.is_pointer_to_objc_class typ then ObjcInterface_decl.is_pointer_to_objc_class typ then
let fname = ModelBuiltins.__set_autorelease_attribute in let fname = ModelBuiltins.__set_autorelease_attribute in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in
(* TODO(jjb): change ret_id to None? *)
let stmt_call = let stmt_call =
Sil.Call Sil.Call (ret_id, Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in
([ret_id], Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in
[stmt_call] [stmt_call]
else [] else []
@ -269,8 +269,8 @@ struct
let create_call_instr trans_state return_type function_sil params_sil sil_loc let create_call_instr trans_state return_type function_sil params_sil sil_loc
call_flags ~is_objc_method = call_flags ~is_objc_method =
let ret_id = if (Typ.equal return_type Typ.Tvoid) then [] let ret_id = if (Typ.equal return_type Typ.Tvoid) then None
else [Ident.create_fresh Ident.knormal] in else Some (Ident.create_fresh Ident.knormal, return_type) in
let ret_id', params, initd_exps, ret_exps = let ret_id', params, initd_exps, ret_exps =
(* Assumption: should_add_return_param will return true only for struct types *) (* Assumption: should_add_return_param will return true only for struct types *)
if CMethod_trans.should_add_return_param return_type ~is_objc_method then if CMethod_trans.should_add_return_param return_type ~is_objc_method then
@ -298,8 +298,8 @@ struct
(* value doesn't work good anyway. This may need to be revisited later*) (* value doesn't work good anyway. This may need to be revisited later*)
let ret_param = (var_exp, param_type) in let ret_param = (var_exp, param_type) in
let ret_exp = (var_exp, return_type) in let ret_exp = (var_exp, return_type) in
[], params_sil @ [ret_param], [var_exp], [ret_exp] None, params_sil @ [ret_param], [var_exp], [ret_exp]
else ret_id, params_sil, [], match ret_id with [x] -> [(Exp.Var x, return_type)] | _ -> [] in else ret_id, params_sil, [], match ret_id with Some (i,t) -> [(Exp.Var i, t)] | None -> [] in
let call_instr = Sil.Call (ret_id', function_sil, params, sil_loc, call_flags) in let call_instr = Sil.Call (ret_id', function_sil, params, sil_loc, call_flags) in
{ empty_res_trans with { empty_res_trans with
instrs = [call_instr]; instrs = [call_instr];
@ -1998,10 +1998,12 @@ struct
let context = trans_state.context in let context = trans_state.context in
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let fname = ModelBuiltins.__objc_release_autorelease_pool in let fname = ModelBuiltins.__objc_release_autorelease_pool in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in
(* TODO(jjb): change ret_id to None? *)
let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in
let stmt_call = let stmt_call =
Sil.Call([ret_id], (Exp.Const (Const.Cfun fname)), Sil.Call
(ret_id, (Exp.Const (Const.Cfun fname)),
autorelease_pool_vars, sil_loc, CallFlags.default) in autorelease_pool_vars, sil_loc, CallFlags.default) in
let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in
let call_node = create_node node_kind [stmt_call] sil_loc context in let call_node = create_node node_kind [stmt_call] sil_loc context in
@ -2162,7 +2164,7 @@ struct
let exp = extract_exp_from_list result_trans_param.exps let exp = extract_exp_from_list result_trans_param.exps
"WARNING: There should be one expression to delete. \n" in "WARNING: There should be one expression to delete. \n" in
let call_instr = let call_instr =
Sil.Call ([], Exp.Const (Const.Cfun fname), [exp], sil_loc, CallFlags.default) in Sil.Call (None, Exp.Const (Const.Cfun fname), [exp], sil_loc, CallFlags.default) in
let call_res_trans = { empty_res_trans with instrs = [call_instr] } in let call_res_trans = { empty_res_trans with instrs = [call_instr] } in
let all_res_trans = if false then let all_res_trans = if false then
(* FIXME (t10135167): call destructor on deleted pointer if it's not null *) (* FIXME (t10135167): call destructor on deleted pointer if it's not null *)
@ -2222,7 +2224,7 @@ struct
let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
let args = [exp; (sizeof_expr, Typ.Tvoid)] in let args = [exp; (sizeof_expr, Typ.Tvoid)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = Sil.Call ([ret_id], builtin, args, sil_loc, CallFlags.default) in let call = Sil.Call (Some (ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; } in let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; } in
let all_res_trans = [ res_trans_stmt; res_trans_dynamic_cast ] in let all_res_trans = [ res_trans_stmt; res_trans_dynamic_cast ] in
@ -2244,7 +2246,7 @@ struct
IList.map (exec_with_glvalue_as_reference instruction trans_state_param) stmts in IList.map (exec_with_glvalue_as_reference instruction trans_state_param) stmts in
let params = collect_exprs res_trans_subexpr_list in let params = collect_exprs res_trans_subexpr_list in
let sil_fun = Exp.Const (Const.Cfun pname) in let sil_fun = Exp.Const (Const.Cfun pname) in
let call_instr = Sil.Call ([], sil_fun, params, sil_loc, CallFlags.default) in let call_instr = Sil.Call (None, sil_fun, params, sil_loc, CallFlags.default) in
let res_trans_call = { empty_res_trans with let res_trans_call = { empty_res_trans with
instrs = [call_instr]; instrs = [call_instr];
exps = []; } in exps = []; } in
@ -2283,7 +2285,7 @@ struct
let ret_exp = Exp.Var ret_id in let ret_exp = Exp.Var ret_id in
let field_exp = Exp.Lfield (ret_exp, field_name, typ) in let field_exp = Exp.Lfield (ret_exp, field_name, typ) in
let args = [type_info_objc; (field_exp, Typ.Tvoid)] @ res_trans_subexpr.exps in let args = [type_info_objc; (field_exp, Typ.Tvoid)] @ res_trans_subexpr.exps in
let call_instr = Sil.Call ([ret_id], sil_fun, args, sil_loc, CallFlags.default) in let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in
let res_trans_call = { empty_res_trans with let res_trans_call = { empty_res_trans with
instrs = [call_instr]; instrs = [call_instr];
exps = [(ret_exp, typ)]; } in exps = [(ret_exp, typ)]; } in
@ -2306,7 +2308,7 @@ 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 ret_exp = Exp.Var ret_id in let ret_exp = Exp.Var ret_id in
let call_instr = Sil.Call ([ret_id], sil_fun, params, sil_loc, CallFlags.default) in let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, params, sil_loc, CallFlags.default) in
let res_trans_call = { empty_res_trans with let res_trans_call = { empty_res_trans with
instrs = [call_instr]; instrs = [call_instr];
exps = [(ret_exp, typ)]; } in exps = [(ret_exp, typ)]; } in

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

@ -307,8 +307,9 @@ let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt =
| None -> [] in | None -> [] in
let args = exp :: procname_arg in let args = exp :: procname_arg in
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, function_type) in
let stmt_call = let stmt_call =
Sil.Call([ret_id], Exp.Const (Const.Cfun fname), args, sil_loc, CallFlags.default) in Sil.Call (ret_id_typ, Exp.Const (Const.Cfun fname), args, sil_loc, CallFlags.default) in
(function_type, stmt_call, Exp.Var ret_id) (function_type, stmt_call, Exp.Var ret_id)
let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt = let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt =
@ -336,8 +337,9 @@ let objc_new_trans trans_state loc stmt_info cls_name function_type =
cls_name CFrontend_config.init Procname.ObjCInstanceMethod in cls_name CFrontend_config.init Procname.ObjCInstanceMethod in
CMethod_trans.create_external_procdesc trans_state.context.CContext.cfg pname is_instance None; CMethod_trans.create_external_procdesc trans_state.context.CContext.cfg pname is_instance None;
let args = [(alloc_ret_exp, alloc_ret_type)] in let args = [(alloc_ret_exp, alloc_ret_type)] in
let ret_id_typ = Some (init_ret_id, alloc_ret_type) in
let init_stmt_call = let init_stmt_call =
Sil.Call ([init_ret_id], Exp.Const (Const.Cfun pname), args, loc, call_flags) in Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, loc, call_flags) in
let instrs = [alloc_stmt_call; init_stmt_call] in let instrs = [alloc_stmt_call; init_stmt_call] in
let res_trans_tmp = { empty_res_trans with instrs = instrs } in let res_trans_tmp = { empty_res_trans with instrs = instrs } in
let res_trans = let res_trans =
@ -369,12 +371,13 @@ let cpp_new_trans sil_loc function_type size_exp_opt =
let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc = 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 typ = CTypes.remove_pointer_to_typ cast_to_typ in let typ = CTypes.remove_pointer_to_typ cast_to_typ in
let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in
let pname = ModelBuiltins.__objc_cast in let pname = ModelBuiltins.__objc_cast in
let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in
let stmt_call = let stmt_call =
Sil.Call ([ret_id], Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in
(stmt_call, Exp.Var ret_id) (stmt_call, Exp.Var ret_id)
let cast_trans exps sil_loc function_type pname = let cast_trans exps sil_loc function_type pname =
@ -439,7 +442,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
let trans_assertion_failure sil_loc context = let trans_assertion_failure sil_loc context =
let assert_fail_builtin = Exp.Const (Const.Cfun ModelBuiltins.__infer_fail) in let assert_fail_builtin = Exp.Const (Const.Cfun ModelBuiltins.__infer_fail) in
let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in
let call_instr = Sil.Call ([], assert_fail_builtin, args, sil_loc, CallFlags.default) in let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in
let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
and failure_node = and failure_node =
Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in

17
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -510,14 +510,14 @@ let typecheck_instr
typestate1 in typestate1 in
check_field_assign (); check_field_assign ();
typestate2 typestate2
| Sil.Call ([id], Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _)
when Procname.equal pn ModelBuiltins.__new || when Procname.equal pn ModelBuiltins.__new ||
Procname.equal pn ModelBuiltins.__new_array -> Procname.equal pn ModelBuiltins.__new_array ->
TypeState.add_id TypeState.add_id
id id
(typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc]) (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc])
typestate (* new never returns null *) typestate (* new never returns null *)
| Sil.Call ([id], Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _) | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _)
when Procname.equal pn ModelBuiltins.__cast -> when Procname.equal pn ModelBuiltins.__cast ->
typecheck_expr_for_errors typestate e loc; typecheck_expr_for_errors typestate e loc;
let e', typestate' = let e', typestate' =
@ -526,7 +526,7 @@ let typecheck_instr
TypeState.add_id id TypeState.add_id id
(typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc) (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc)
typestate' typestate'
| Sil.Call ([id], Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _)
when Procname.equal pn ModelBuiltins.__get_array_length -> when Procname.equal pn ModelBuiltins.__get_array_length ->
let (_, ta, _) = typecheck_expr let (_, ta, _) = typecheck_expr
find_canonical_duplicate find_canonical_duplicate
@ -561,7 +561,7 @@ let typecheck_instr
| Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn -> | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn ->
typestate (* skip othe builtins *) typestate (* skip othe builtins *)
| Sil.Call | Sil.Call
(ret_ids, (ret_id,
Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
etl_, etl_,
loc, loc,
@ -608,9 +608,9 @@ let typecheck_instr
Procname.java_is_anonymous_inner_class_constructor callee_pname in Procname.java_is_anonymous_inner_class_constructor callee_pname in
let do_return loc' typestate' = let do_return loc' typestate' =
match ret_ids with match ret_id with
| [] -> typestate' | None -> typestate'
| [id] -> | Some (id, _) ->
let (ia, ret_typ) = annotated_signature.Annotations.ret in let (ia, ret_typ) = annotated_signature.Annotations.ret in
let is_library = Specs.proc_is_library callee_attributes in let is_library = Specs.proc_is_library callee_attributes in
let origin = TypeOrigin.Proc let origin = TypeOrigin.Proc
@ -627,8 +627,7 @@ let typecheck_instr
TypeAnnotation.from_item_annotation ia origin, TypeAnnotation.from_item_annotation ia origin,
[loc'] [loc']
) )
typestate' typestate' in
| _ :: _ :: _ -> assert false in
(* Handle Preconditions.checkNotNull. *) (* Handle Preconditions.checkNotNull. *)
let do_preconditions_check_not_null parameter_num is_vararg typestate' = let do_preconditions_check_not_null parameter_num is_vararg typestate' =

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

@ -75,7 +75,7 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
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 (sizeof_typ, sizeof_len, Subtype.exact) in
let args = [(sizeof_exp, Typ.Tptr (ret_typ, Typ.Pk_pointer))] in let args = [(sizeof_exp, Typ.Tptr (ret_typ, Typ.Pk_pointer))] in
Sil.Call ([retval], 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)
(** find or create a Sil expression with type typ *) (** find or create a Sil expression with type typ *)
@ -166,14 +166,15 @@ and inhabit_constructor tenv constr_name (allocated_obj, obj_type) cfg env =
inhabit_args tenv non_receiver_formals cfg env in inhabit_args tenv non_receiver_formals cfg env in
let constr_instr = let constr_instr =
let fun_exp = fun_exp_from_name constr_name in let fun_exp = fun_exp_from_name constr_name in
Sil.Call ([], fun_exp, (allocated_obj, obj_type) :: args, env.pc, CallFlags.default) in Sil.Call (None, fun_exp, (allocated_obj, obj_type) :: args, env.pc, CallFlags.default) in
env_add_instr constr_instr env env_add_instr constr_instr env
with Not_found -> env with Not_found -> env
let inhabit_call_with_args procname procdesc args env = let inhabit_call_with_args procname procdesc args env =
let retval = let retval =
let is_void = Cfg.Procdesc.get_ret_type procdesc = Typ.Tvoid in let ret_typ = Cfg.Procdesc.get_ret_type procdesc in
if is_void then [] else [Ident.create_fresh Ident.knormal] in let is_void = ret_typ = Typ.Tvoid in
if is_void then None else Some (Ident.create_fresh Ident.knormal, ret_typ) in
let call_instr = let call_instr =
let fun_exp = fun_exp_from_name procname in let fun_exp = fun_exp_from_name procname in
let flags = let flags =

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

@ -454,8 +454,10 @@ let rec expression (context : JContext.t) pc expr =
let deref = create_sil_deref sil_ex array_typ_no_ptr loc in let deref = create_sil_deref sil_ex array_typ_no_ptr loc in
let args = [(sil_ex, type_of_ex)] in let args = [(sil_ex, type_of_ex)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let ret_typ = Typ.Tint IInt in
let call_instr = let call_instr =
Sil.Call ([ret_id], builtin_get_array_length, args, loc, CallFlags.default) in Sil.Call
(Some (ret_id, ret_typ), builtin_get_array_length, args, loc, CallFlags.default) in
(instrs @ [deref; call_instr], Exp.Var ret_id, type_of_expr) (instrs @ [deref; call_instr], Exp.Var ret_id, type_of_expr)
| JBir.Conv conv -> | JBir.Conv conv ->
let cast_ex = Exp.Cast (JTransType.cast_type conv, sil_ex) in let cast_ex = Exp.Cast (JTransType.cast_type conv, sil_ex) in
@ -475,7 +477,8 @@ let rec expression (context : JContext.t) pc expr =
| _ -> assert false) in | _ -> assert false) in
let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = Sil.Call([ret_id], builtin, args, loc, CallFlags.default) in let call =
Sil.Call (Some (ret_id, Tint IBool), builtin, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
(instrs @ [call], res_ex, type_of_expr) (instrs @ [call], res_ex, type_of_expr)
end end
@ -608,12 +611,13 @@ let method_invocation
| Some vt -> JTransType.value_type program tenv vt in | Some vt -> JTransType.value_type program tenv vt in
let call_ret_instrs sil_var = let call_ret_instrs sil_var =
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in let call_instr =
Sil.Call (Some (ret_id, return_type), callee_fun, call_args, loc, call_flags) in
let set_instr = Sil.Store (Exp.Lvar sil_var, return_type, Exp.Var ret_id, loc) in let set_instr = Sil.Store (Exp.Lvar sil_var, return_type, Exp.Var ret_id, loc) in
(instrs @ [call_instr; set_instr]) in (instrs @ [call_instr; set_instr]) in
match var_opt with match var_opt with
| None -> | None ->
let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in let call_instr = Sil.Call (None, callee_fun, call_args, loc, call_flags) in
instrs @ [call_instr] instrs @ [call_instr]
| Some var -> | Some var ->
let sil_var = JContext.set_pvar context var return_type in let sil_var = JContext.set_pvar context var return_type in
@ -628,7 +632,7 @@ let method_invocation
when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ -> when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ ->
let set_file_attr = let set_file_attr =
let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in
Sil.Call ([], set_builtin, [exp], loc, CallFlags.default) in Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in
(* Exceptions thrown in the constructor should prevent adding the resource attribute *) (* Exceptions thrown in the constructor should prevent adding the resource attribute *)
call_instrs @ [set_file_attr] call_instrs @ [set_file_attr]
@ -637,7 +641,7 @@ let method_invocation
when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ -> when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ ->
let set_mem_attr = let set_mem_attr =
let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in
Sil.Call ([], set_builtin, [exp], loc, CallFlags.default) in Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in
(* Exceptions thrown in the close method should not prevent the resource from being *) (* Exceptions thrown in the close method should not prevent the resource from being *)
(* considered as closed *) (* considered as closed *)
[set_mem_attr] @ call_instrs [set_mem_attr] @ call_instrs
@ -772,7 +776,7 @@ let assume_not_null loc sil_expr =
Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in
let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in
Sil.Call ([], builtin_infer_assume, call_args, loc, assume_call_flag) Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag)
let rec instruction (context : JContext.t) pc instr : translation = let rec instruction (context : JContext.t) pc instr : translation =
let cfg = JContext.get_cfg context in let cfg = JContext.get_cfg context in
@ -803,7 +807,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
let trans_monitor_enter_exit context expr pc loc builtin node_desc = let trans_monitor_enter_exit context expr pc loc builtin node_desc =
let instrs, sil_expr, sil_type = expression context pc expr in let instrs, sil_expr, sil_type = expression context pc expr in
let builtin_const = Exp.Const (Const.Cfun builtin) in let builtin_const = Exp.Const (Const.Cfun builtin) in
let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in let instr = Sil.Call (None, builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in
let typ_no_ptr = match sil_type with let typ_no_ptr = match sil_type with
| Typ.Tptr (typ, _) -> typ | Typ.Tptr (typ, _) -> typ
| _ -> sil_type in | _ -> sil_type in
@ -912,7 +916,8 @@ let rec instruction (context : JContext.t) pc instr : translation =
let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in let new_instr =
Sil.Call (Some (ret_id, class_type), builtin_new, args, loc, CallFlags.default) in
let constr_ms = JBasics.make_ms JConfig.constructor_name constr_type_list None in let constr_ms = JBasics.make_ms JConfig.constructor_name constr_type_list None in
let constr_procname, call_instrs = let constr_procname, call_instrs =
let ret_opt = Some (Exp.Var ret_id, class_type) in let ret_opt = Some (Exp.Var ret_id, class_type) in
@ -934,7 +939,9 @@ let rec instruction (context : JContext.t) pc instr : translation =
let (instrs, array_size) = get_array_length context pc expr_list content_type in let (instrs, array_size) = get_array_length context pc expr_list content_type in
let call_args = [(array_size, array_type)] in let call_args = [(array_size, array_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, CallFlags.default) in let call_instr =
Sil.Call
(Some (ret_id, array_type), builtin_new_array, call_args, loc, CallFlags.default) in
let set_instr = Sil.Store (Exp.Lvar array_name, array_type, Exp.Var ret_id, loc) in let set_instr = Sil.Store (Exp.Lvar array_name, array_type, Exp.Var ret_id, loc) in
let node_kind = Cfg.Node.Stmt_node "method_body" in let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind (instrs @ [call_instr; set_instr]) in let node = create_node node_kind (instrs @ [call_instr; set_instr]) in
@ -1002,7 +1009,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
| JBir.Check (JBir.CheckNullPointer expr) | JBir.Check (JBir.CheckNullPointer expr)
when Config.report_runtime_exceptions && is_this expr -> when Config.report_runtime_exceptions && is_this expr ->
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *) (* TODO #6509339: refactor the boilerplate code in the translation of JVM checks *)
let (instrs, sil_expr, _) = expression context pc expr in let (instrs, sil_expr, _) = expression context pc expr in
let this_not_null_node = let this_not_null_node =
create_node create_node
@ -1026,7 +1033,8 @@ let rec instruction (context : JContext.t) pc instr : translation =
let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in let new_instr =
Sil.Call (Some (ret_id, class_type), builtin_new, args, loc, CallFlags.default) in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs = let _, call_instrs =
let ret_opt = Some (Exp.Var ret_id, class_type) in let ret_opt = Some (Exp.Var ret_id, class_type) in
@ -1079,7 +1087,8 @@ let rec instruction (context : JContext.t) pc instr : translation =
let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in let new_instr =
Sil.Call (Some (ret_id, ret_type), builtin_new, args, loc, CallFlags.default) in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs = let _, call_instrs =
method_invocation method_invocation
@ -1101,7 +1110,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in
let check_cast = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in let check_cast = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in
let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in
let call = Sil.Call([ret_id], check_cast, args, loc, CallFlags.default) in let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
let is_instance_node = let is_instance_node =
let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in
@ -1118,7 +1127,8 @@ let rec instruction (context : JContext.t) pc instr : translation =
let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in let new_instr =
Sil.Call (Some (ret_id, ret_type), builtin_new, args, loc, CallFlags.default) in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs = let _, call_instrs =
method_invocation context loc pc None cce_cn constr_ms method_invocation context loc pc None cce_cn constr_ms

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

@ -43,7 +43,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let instr_unwrap_ret_val = let instr_unwrap_ret_val =
let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in
Sil.Call Sil.Call
([id_exn_val], unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc, CallFlags.default) in (Some (id_exn_val, ret_type), unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc,
CallFlags.default) in
create_node create_node
loc loc
Cfg.Node.exn_handler_kind Cfg.Node.exn_handler_kind
@ -72,7 +73,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let args = [ let args = [
(Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer)); (Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer));
(Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in (Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in
Sil.Call ([id_instanceof], instanceof_builtin, args, loc, CallFlags.default) in Sil.Call
(Some (id_instanceof, Tint IBool), instanceof_builtin, args, loc, CallFlags.default) in
let if_kind = Sil.Ik_switch in let if_kind = Sil.Ik_switch in
let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in
let instr_prune_false = let instr_prune_false =

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

@ -188,7 +188,8 @@ let translate_instr_static_field (context : JContext.t) callee_procdesc fs field
let callee_fun = Exp.Const (Const.Cfun callee_procname) in let callee_fun = Exp.Const (Const.Cfun callee_procname) in
let field_arg = Exp.Const (Const.Cstr (JBasics.fs_name fs)) in let field_arg = Exp.Const (Const.Cstr (JBasics.fs_name fs)) in
let call_instr = let call_instr =
Sil.Call ([ret_id], callee_fun, [field_arg, field_type], loc, CallFlags.default) in Sil.Call
(Some (ret_id, field_type), callee_fun, [field_arg, field_type], loc, CallFlags.default) in
Cg.add_edge cg caller_procname callee_procname; Cg.add_edge cg caller_procname callee_procname;
([call_instr], Exp.Var ret_id) ([call_instr], Exp.Var ret_id)

3
infer/src/llvm/lTrans.ml
Unescape View File

@ -97,7 +97,8 @@ let rec trans_annotated_instructions
end end
| Call (ret_var, func_var, typed_args) -> | Call (ret_var, func_var, typed_args) ->
let new_sil_instr = Sil.Call ( let new_sil_instr = Sil.Call (
[ident_of_variable ret_var], (* TODO: translate type of ret_var *)
Some (ident_of_variable ret_var, Tvoid),
Exp.Const (Const.Cfun (procname_of_function_variable func_var)), Exp.Const (Const.Cfun (procname_of_function_variable func_var)),
IList.map (fun (tp, arg) -> (trans_operand arg, trans_typ tp)) typed_args, IList.map (fun (tp, arg) -> (trans_operand arg, trans_typ tp)) typed_args,
location, CallFlags.default) in location, CallFlags.default) in

21
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -176,7 +176,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
{ astate with Domain.access_tree = access_tree'; } { astate with Domain.access_tree = access_tree'; }
let apply_summary let apply_summary
ret_ids ret_id
actuals actuals
summary summary
(astate_in : Domain.astate) (astate_in : Domain.astate)
@ -185,9 +185,8 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let callee_loc = CallSite.loc callee_site in let callee_loc = CallSite.loc callee_site in
let apply_return ret_ap = function let apply_return ret_ap = function
| [ret_id] -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap | Some (ret_id, _) -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap
| [] -> failwith "Have summary for retval, but no ret id to bind it to!" | None -> failwith "Have summary for retval, but no ret id to bind it to!" in
| _ -> failwith "Unimp: summaries for function with multiple return values" in
let get_actual_ap_trace formal_num formal_ap access_tree = let get_actual_ap_trace formal_num formal_ap access_tree =
let get_actual_ap formal_num = let get_actual_ap formal_num =
@ -226,7 +225,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let caller_ap_trace_opt = let caller_ap_trace_opt =
match in_out_summary.output with match in_out_summary.output with
| Out_return ret_ap -> | Out_return ret_ap ->
Some (apply_return ret_ap ret_ids, TraceDomain.initial) Some (apply_return ret_ap ret_id, TraceDomain.initial)
| Out_formal (formal_num, formal_ap) -> | Out_formal (formal_num, formal_ap) ->
get_actual_ap_trace formal_num formal_ap access_tree get_actual_ap_trace formal_num formal_ap access_tree
| Out_global global_ap -> | Out_global global_ap ->
@ -283,7 +282,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
| _ -> | _ ->
astate' astate'
end end
| Sil.Call ([ret_id], Const (Cfun callee_pname), args, loc, _) | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), args, loc, _)
when Builtin.is_registered callee_pname -> when Builtin.is_registered callee_pname ->
if Procname.equal callee_pname ModelBuiltins.__cast if Procname.equal callee_pname ModelBuiltins.__cast
then then
@ -298,7 +297,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
Location.pp loc Location.pp loc
else else
astate astate
| Sil.Call (ret_ids, Const (Cfun callee_pname), actuals, callee_loc, _) -> | Sil.Call (ret_id, Const (Cfun callee_pname), actuals, callee_loc, _) ->
let call_site = CallSite.make callee_pname callee_loc in let call_site = CallSite.make callee_pname callee_loc in
let astate_with_sink = let astate_with_sink =
@ -316,11 +315,11 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
failwith "Unimp: looking up return type for non-Java procedure" in failwith "Unimp: looking up return type for non-Java procedure" in
let astate_with_source = let astate_with_source =
match TraceDomain.Source.get call_site, ret_ids with match TraceDomain.Source.get call_site, ret_id with
| [(0, source)], [ret_id] -> | [(0, source)], Some (ret_id, _) ->
let access_tree = add_source source ret_id ret_typ astate_with_sink.access_tree in let access_tree = add_source source ret_id ret_typ astate_with_sink.access_tree in
{ astate_with_sink with access_tree; } { astate_with_sink with access_tree; }
| [], _ | _, [] -> | [], _ | _, None ->
astate_with_sink astate_with_sink
| _ -> | _ ->
(* this is allowed by SIL, but not currently used in any frontends *) (* this is allowed by SIL, but not currently used in any frontends *)
@ -329,7 +328,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let astate_with_summary = let astate_with_summary =
match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with
| Some summary -> | Some summary ->
apply_summary ret_ids actuals summary astate_with_source proc_data call_site apply_summary ret_id actuals summary astate_with_source proc_data call_site
| None -> | None ->
astate_with_source in astate_with_source in

22
infer/src/unit/BoundedCallTreeTests.ml
Unescape View File

@ -24,7 +24,7 @@ let tests =
let f_proc_name = Procname.from_string_c_fun "f" in let f_proc_name = Procname.from_string_c_fun "f" in
let g_proc_name = Procname.from_string_c_fun "g" in let g_proc_name = Procname.from_string_c_fun "g" in
let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in
let g_ret_ids = [(ident_of_str "r")] in let g_ret_id = Some (ident_of_str "r", Typ.Tint IInt) in
let class_name = "com.example.SomeClass" in let class_name = "com.example.SomeClass" in
let file_name = "SomeClass.java" in let file_name = "SomeClass.java" in
let trace = Stacktrace.make "java.lang.NullPointerException" let trace = Stacktrace.make "java.lang.NullPointerException"
@ -44,47 +44,47 @@ let tests =
let test_list_from_foo = [ let test_list_from_foo = [
"on_call_add_proc_name", "on_call_add_proc_name",
[ [
make_call ~procname:f_proc_name [] []; (* means f() *) make_call ~procname:f_proc_name None []; (* means f() *)
invariant "{ f }" invariant "{ f }"
]; ];
"on_call_add_proc_name_w_args", "on_call_add_proc_name_w_args",
[ [
make_call ~procname:g_proc_name g_ret_ids g_args; (* means r = a.g(1) *) make_call ~procname:g_proc_name g_ret_id g_args; (* means r = a.g(1) *)
invariant "{ g }" invariant "{ g }"
]; ];
"handle_two_proc_calls", "handle_two_proc_calls",
[ [
make_call ~procname:f_proc_name [] []; make_call ~procname:f_proc_name None [];
invariant "{ f }"; invariant "{ f }";
make_call ~procname:g_proc_name g_ret_ids g_args; make_call ~procname:g_proc_name g_ret_id g_args;
invariant "{ f, g }" invariant "{ f, g }"
]; ];
"dont_record_procs_twice", "dont_record_procs_twice",
[ [
make_call ~procname:f_proc_name [] []; make_call ~procname:f_proc_name None [];
invariant "{ f }"; invariant "{ f }";
make_call ~procname:f_proc_name [] []; make_call ~procname:f_proc_name None [];
invariant "{ f }" invariant "{ f }"
]; ];
] |> TestInterpreter.create_tests ~test_pname:caller_foo_name extras in ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name extras in
let test_list_from_bar = [ let test_list_from_bar = [
"on_call_anywhere_on_stack_add_proc_name", "on_call_anywhere_on_stack_add_proc_name",
[ [
make_call ~procname:f_proc_name [] []; (* means f() *) make_call ~procname:f_proc_name None []; (* means f() *)
invariant "{ f }" invariant "{ f }"
]; ];
] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras in ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras in
let test_list_from_baz = [ let test_list_from_baz = [
"ignore_procs_unrelated_to_trace", "ignore_procs_unrelated_to_trace",
[ [
make_call ~procname:f_proc_name [] []; (* means f() *) make_call ~procname:f_proc_name None []; (* means f() *)
invariant "{ }" invariant "{ }"
]; ];
] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras in ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras in
let test_list_multiple_traces_from_foo = [ let test_list_multiple_traces_from_foo = [
"on_call_add_proc_name_in_any_stack_1", "on_call_add_proc_name_in_any_stack_1",
[ [
make_call ~procname:f_proc_name [] []; (* means f() *) make_call ~procname:f_proc_name None []; (* means f() *)
invariant "{ f }" invariant "{ f }"
]; ];
] |> TestInterpreter.create_tests ] |> TestInterpreter.create_tests
@ -92,7 +92,7 @@ let tests =
let test_list_multiple_traces_from_bar = [ let test_list_multiple_traces_from_bar = [
"on_call_add_proc_name_in_any_stack_2", "on_call_add_proc_name_in_any_stack_2",
[ [
make_call ~procname:f_proc_name [] []; (* means f() *) make_call ~procname:f_proc_name None []; (* means f() *)
invariant "{ f }" invariant "{ f }"
]; ];
] |> TestInterpreter.create_tests ] |> TestInterpreter.create_tests

6
infer/src/unit/TaintTests.ml
Unescape View File

@ -115,13 +115,13 @@ let tests =
PrettyPrintable.pp_collection ~pp_item fmt (IList.rev trace_assocs) in PrettyPrintable.pp_collection ~pp_item fmt (IList.rev trace_assocs) in
let assign_to_source ret_str = let assign_to_source ret_str =
let procname = Procname.from_string_c_fun "SOURCE" in let procname = Procname.from_string_c_fun "SOURCE" in
make_call ~procname [ident_of_str ret_str] [] in make_call ~procname (Some (ident_of_str ret_str, dummy_typ)) [] in
let assign_to_non_source ret_str = let assign_to_non_source ret_str =
let procname = Procname.from_string_c_fun "NON-SOURCE" in let procname = Procname.from_string_c_fun "NON-SOURCE" in
make_call ~procname [ident_of_str ret_str] [] in make_call ~procname (Some (ident_of_str ret_str, dummy_typ)) [] in
let call_sink_with_exp exp = let call_sink_with_exp exp =
let procname = Procname.from_string_c_fun "SINK" in let procname = Procname.from_string_c_fun "SINK" in
make_call ~procname [] [(exp, dummy_typ)] in make_call ~procname None [(exp, dummy_typ)] in
let call_sink actual_str = let call_sink actual_str =
call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in
let assign_id_to_field root_str fld_str rhs_id_str = let assign_id_to_field root_str fld_str rhs_id_str =

14
infer/src/unit/analyzerTester.ml
Unescape View File

@ -90,9 +90,9 @@ module StructuredSil = struct
let make_set ~rhs_typ ~lhs_exp ~rhs_exp = let make_set ~rhs_typ ~lhs_exp ~rhs_exp =
Cmd (Sil.Store (lhs_exp, rhs_typ, rhs_exp, dummy_loc)) Cmd (Sil.Store (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
let make_call ?(procname=dummy_procname) ret_ids args = let make_call ?(procname=dummy_procname) ret_id args =
let call_exp = Exp.Const (Const.Cfun procname) in let call_exp = Exp.Const (Const.Cfun procname) in
Cmd (Sil.Call (ret_ids, call_exp, args, dummy_loc, CallFlags.default)) Cmd (Sil.Call (ret_id, call_exp, args, dummy_loc, CallFlags.default))
let make_store ~rhs_typ root_exp fld_str ~rhs_exp = let make_store ~rhs_typ root_exp fld_str ~rhs_exp =
let fld = AccessPathTestUtils.make_fieldname fld_str in let fld = AccessPathTestUtils.make_fieldname fld_str in
@ -124,7 +124,7 @@ module StructuredSil = struct
let cast_id_to_id lhs cast_typ rhs = let cast_id_to_id lhs cast_typ rhs =
let lhs_id = ident_of_str lhs in let lhs_id = ident_of_str lhs in
let rhs_id = Exp.Var (ident_of_str rhs) in let rhs_id = Exp.Var (ident_of_str rhs) in
make_call ~procname:ModelBuiltins.__cast [lhs_id] [rhs_id, cast_typ] make_call ~procname:ModelBuiltins.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ]
let var_assign_exp ~rhs_typ lhs rhs_exp = let var_assign_exp ~rhs_typ lhs rhs_exp =
let lhs_exp = var_of_str lhs in let lhs_exp = var_of_str lhs in
@ -146,13 +146,13 @@ module StructuredSil = struct
let rhs_exp = var_of_str rhs in let rhs_exp = var_of_str rhs in
make_set ~rhs_typ ~lhs_exp ~rhs_exp make_set ~rhs_typ ~lhs_exp ~rhs_exp
let call_unknown ret_id_strs arg_strs = let call_unknown ret_id_str_opt arg_strs =
let args = IList.map (fun param_str -> (var_of_str param_str, dummy_typ)) arg_strs in let args = IList.map (fun param_str -> (var_of_str param_str, dummy_typ)) arg_strs in
let ret_ids = IList.map ident_of_str ret_id_strs in let ret_id = Option.map (fun (str, typ) -> (ident_of_str str, typ)) ret_id_str_opt in
make_call ret_ids args make_call ret_id args
let call_unknown_no_ret arg_strs = let call_unknown_no_ret arg_strs =
call_unknown [] arg_strs call_unknown None arg_strs
end end
module Make module Make

2
infer/src/unit/livenessTests.ml
Unescape View File

@ -99,7 +99,7 @@ let tests =
"dead_after_call_with_retval", "dead_after_call_with_retval",
[ [
assert_empty; assert_empty;
call_unknown ["y"] []; call_unknown (Some ("y", Typ.Tint IInt)) [];
invariant "{ y$0 }"; invariant "{ y$0 }";
id_assign_id "x" "y"; id_assign_id "x" "y";
]; ];

Write Preview
Loading…
Cancel
Save