From d7a4474d90253eb069d36e52f7464567a62009af Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 19 Jun 2015 16:09:42 -0600 Subject: [PATCH] [Infer][angelic] Adding angelic abduction on actuals passed by reference --- infer/src/backend/cfg.ml | 4 +- infer/src/backend/interproc.ml | 12 +- infer/src/backend/prop.ml | 10 + infer/src/backend/prop.mli | 4 + infer/src/backend/sil.ml | 48 +++- infer/src/backend/sil.mli | 9 +- infer/src/backend/symExec.ml | 251 ++++++++++-------- .../c/errors/null_dereference/angelism.c | 40 +++ infer/tests/endtoend/c/AngelismTest.java | 1 + 9 files changed, 249 insertions(+), 130 deletions(-) diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 8bf88a8d9..5e8cfd778 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -802,7 +802,7 @@ let remove_abducted_retvars p = let reach' = Sil.HpredSet.add hpred reach in let exps' = collect_exps exps rhs in (reach', exps') - | hpred -> reach, exps in + | _ -> reach, exps in let reach', exps' = list_fold_left add_hpred_if_reachable (reach, exps) sigma in if (Sil.HpredSet.cardinal reach) = (Sil.HpredSet.cardinal reach') then (reach, exps) else compute_reachable_hpreds_rec sigma (reach', exps') in @@ -815,7 +815,7 @@ let remove_abducted_retvars p = match hpred with | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> let abducted_pvars, normal_pvars = pvars in - if Sil.pvar_is_abducted_retvar pvar then pvar :: abducted_pvars, normal_pvars + if Sil.pvar_is_abducted pvar then pvar :: abducted_pvars, normal_pvars else abducted_pvars, pvar :: normal_pvars | _ -> pvars) ([], []) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 277f3f981..944227186 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -696,13 +696,11 @@ let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t = res let create_seed_vars sigma = - let sigma_seed = ref [] in - let hpred_add_seed = function - | Sil.Hpointsto (Sil.Lvar pv, se, typ) -> - sigma_seed := Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: !sigma_seed - | _ -> () in - list_iter hpred_add_seed sigma; - !sigma_seed + let hpred_add_seed sigma = function + | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) -> + Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma + | _ -> sigma in + list_fold_left hpred_add_seed [] sigma (** Initialize proposition for execution given formal and global parameters. The footprint is initialized according to the diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index cd95d3b49..9495f906f 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1769,6 +1769,16 @@ let add_or_replace_exp_attribute check_attribute_change prop exp att = if !found then replace_pi pi' prop else set_exp_attribute prop nexp att +(** mark Sil.Var's or Sil.Lvar's as undefined *) +let mark_vars_as_undefined prop vars_to_mark callee_pname loc path_pos = + let att_undef = Sil.Aundef (callee_pname, loc, path_pos) in + let mark_var_as_undefined exp prop = + let do_nothing _ _ = () in + match exp with + | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute do_nothing prop exp att_undef + | _ -> prop in + list_fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark + (** Remove an attribute from all the atoms in the heap *) let remove_attribute att prop = let atom_remove atom pi = match atom with diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 0d84692de..b922f31b8 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -291,6 +291,10 @@ val get_all_attributes : 'a t -> (exp * attribute) list (** Replace an attribute associated to the expression *) val add_or_replace_exp_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> exp -> attribute -> normal t +(** mark Sil.Var's or Sil.Lvar's as undefined *) +val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Sil.location -> + Sil.path_pos -> normal t + (** Remove an attribute from all the atoms in the heap *) val remove_attribute : Sil.attribute -> 'a t -> normal t diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 2a4b3dbf4..997638971 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -150,11 +150,13 @@ type pvar_kind = | Local_var of Procname.t (** local variable belonging to a function *) | Callee_var of Procname.t (** local variable belonging to a callee *) | Abducted_retvar of Procname.t * location (** synthetic variable to represent return value *) + | Abducted_ref_param of Procname.t * pvar * location + (** synthetic variable to represent param passed by reference *) | Global_var (** gloval variable *) | Seed_var (** variable used to store the initial value of formal parameters *) (** Names for program variables. *) -type pvar = { pv_name: Mangled.t; pv_kind: pvar_kind } +and pvar = { pv_name: Mangled.t; pv_kind: pvar_kind } (** Unary operations *) type unop = @@ -872,6 +874,11 @@ let has_objc_ref_counter hpred = list_exists is_objc_ref_counter_field fl | _ -> false +(** turn a *T into a T. fails if [typ] is not a pointer type *) +let typ_strip_ptr = function + | Tptr (t, _) -> t + | _ -> assert false + let pvar_get_name pv = pv.pv_name let pvar_to_string pv = Mangled.to_string pv.pv_name @@ -885,6 +892,12 @@ let pvar_get_simplified_name pv = | _ -> s) | _ -> s +(** Check if the pvar is an abucted return var or param passed by ref *) +let pvar_is_abducted pv = + match pv.pv_kind with + | Abducted_retvar _ | Abducted_ref_param _ -> true + | _ -> false + (** Turn a pvar into a seed pvar (which stored the initial value) *) let pvar_to_seed pv = { pv with pv_kind = Seed_var } @@ -900,12 +913,6 @@ let pvar_is_callee pv = | Callee_var _ -> true | _ -> false -(** Check if the pvar is an abucted return var *) -let pvar_is_abducted_retvar pv = - match pv.pv_kind with - | Abducted_retvar _ -> true - | _ -> false - (** Check if the pvar is a seed var *) let pvar_is_seed pv = match pv.pv_kind with @@ -942,24 +949,31 @@ let loc_compare loc1 loc2 = let loc_equal loc1 loc2 = loc_compare loc1 loc2 = 0 -let pv_kind_compare k1 k2 = match k1, k2 with +let rec pv_kind_compare k1 k2 = match k1, k2 with | Local_var n1, Local_var n2 -> Procname.compare n1 n2 | Local_var _, _ -> - 1 | _, Local_var _ -> 1 | Callee_var n1, Callee_var n2 -> Procname.compare n1 n2 | Callee_var _, _ -> - 1 + | _, Callee_var _ -> 1 | Abducted_retvar (p1, l1), Abducted_retvar (p2, l2) -> let n = Procname.compare p1 p2 in if n <> 0 then n else loc_compare l1 l2 | Abducted_retvar _, _ -> - 1 | _, Abducted_retvar _ -> 1 - | _, Callee_var _ -> 1 + | Abducted_ref_param (p1, pv1, l1), Abducted_ref_param (p2, pv2, l2) -> + let n = Procname.compare p1 p2 in + if n <> 0 then n else + let n = pvar_compare pv1 pv2 in + if n <> 0 then n else loc_compare l1 l2 + | Abducted_ref_param _, _ -> - 1 + | _, Abducted_ref_param _ -> 1 | Global_var, Global_var -> 0 | Global_var, _ -> - 1 | _, Global_var -> 1 | Seed_var, Seed_var -> 0 -let pvar_compare pv1 pv2 = +and pvar_compare pv1 pv2 = let n = Mangled.compare pv1.pv_name pv2.pv_name in if n <> 0 then n else pv_kind_compare pv1.pv_kind pv2.pv_kind @@ -1768,7 +1782,7 @@ let loc_to_string loc = (** Dump a location *) let d_loc (loc: location) = L.add_print_action (L.PTloc, Obj.repr loc) -let _pp_pvar f pv = +let rec _pp_pvar f pv = let name = pv.pv_name in match pv.pv_kind with | Local_var n -> @@ -1780,6 +1794,9 @@ let _pp_pvar f pv = | Abducted_retvar (n, l) -> if !Config.pp_simple then F.fprintf f "%a|abductedRetvar" Mangled.pp name else F.fprintf f "%a$%a%a|abductedRetvar" Procname.pp n pp_loc l Mangled.pp name + | Abducted_ref_param (n, pv, l) -> + if !Config.pp_simple then F.fprintf f "%a|%a|abductedRefParam" _pp_pvar pv Mangled.pp name + else F.fprintf f "%a$%a%a|abductedRefParam" Procname.pp n pp_loc l Mangled.pp name | Global_var -> F.fprintf f "#GB$%a" Mangled.pp name | Seed_var -> F.fprintf f "old_%a" Mangled.pp name @@ -1795,6 +1812,9 @@ let pp_pvar_latex f pv = | Abducted_retvar (n, l) -> F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) (Latex.pp_string Latex.Roman) "abductedRetvar" + | Abducted_ref_param (n, pv, l) -> + F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) + (Latex.pp_string Latex.Roman) "abductedRefParam" | Global_var -> Latex.pp_string Latex.Boldface f (Mangled.to_string name) | Seed_var -> @@ -3769,12 +3789,16 @@ let mk_pvar_abducted_ret (proc_name : Procname.t) (loc : location) : pvar = let name = Mangled.from_string ("$RET_" ^ (Procname.to_unique_id proc_name)) in { pv_name = name; pv_kind = Abducted_retvar (proc_name, loc) } +let mk_pvar_abducted_ref_param (proc_name : Procname.t) (pv : pvar) (loc : location) : pvar = + let name = Mangled.from_string ("$REF_PARAM_" ^ (Procname.to_unique_id proc_name)) in + { pv_name = name; pv_kind = Abducted_ref_param (proc_name, pv, loc) } + (** Turn an ordinary program variable into a callee program variable *) let pvar_to_callee pname pvar = match pvar.pv_kind with | Local_var _ -> { pvar with pv_kind = Callee_var pname } | Global_var -> pvar - | Callee_var _ | Abducted_retvar _ | Seed_var -> + | Callee_var _ | Abducted_retvar _ | Abducted_ref_param _ | Seed_var -> L.d_str "Cannot convert pvar to callee: "; d_pvar pvar; L.d_ln (); assert false diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 8906163da..dcf0fd862 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -592,6 +592,9 @@ val loc_equal : location -> location -> bool val path_pos_equal : path_pos -> path_pos -> bool +(** turn a *T into a T. fails if [typ] is not a pointer type *) +val typ_strip_ptr : typ -> typ + val pvar_get_name : pvar -> Mangled.t val pvar_to_string : pvar -> string @@ -602,8 +605,8 @@ val pvar_to_seed : pvar -> pvar (** Check if the pvar is a callee var *) val pvar_is_callee : pvar -> bool -(** Check if the pvar is an abducted return var *) -val pvar_is_abducted_retvar : pvar -> bool +(** Check if the pvar is an abducted return var or param passed by ref *) +val pvar_is_abducted : pvar -> bool (** Check if the pvar is a local var *) val pvar_is_local : pvar -> bool @@ -1324,6 +1327,8 @@ val mk_pvar_global : Mangled.t -> pvar (** create an abducted return variable for a call to [proc_name] at [loc] *) val mk_pvar_abducted_ret : Procname.t -> location -> pvar +val mk_pvar_abducted_ref_param : Procname.t -> pvar -> location -> pvar + (** Turn an ordinary program variable into a callee program variable *) val pvar_to_callee : Procname.t -> pvar -> pvar diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index e78a27d8c..006847e68 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -85,10 +85,6 @@ let check_block_retain_cycle cfg tenv pname _prop block_nullified = let _ = Abs.abstract_junk ~original_prop: _prop pname tenv _prop'' in () -let mark_id_as_undefined id prop att_undef = - let check_attr_change att_old att_new = () in - Prop.add_or_replace_exp_attribute check_attr_change prop (Sil.Var id) att_undef - (** Apply function [f] to the expression at position [offlist] in [strexp]. If not found, expand [strexp] and apply [f] to [None]. The routine should maintain the invariant that strexp and typ correspond to @@ -520,15 +516,12 @@ let call_should_be_skipped caller_pname callee_pname callee_pdesc = | None -> not (Cfg.Procdesc.is_defined callee_pdesc) (* treat calls with no specs as skip functions in angelic mode *) - (* TODO: turn angelic back on for C_CPP once we have abductive angelic analysis (t6935559) *) - || (!Config.angelic_execution && !Sil.curr_language <> Sil.C_CPP) + || !Config.angelic_execution | Some summary -> Specs.get_flag callee_pname proc_flag_skip <> None (* check skip flag *) || summary.Specs.attributes.Sil.is_abstract (* skip abstract methods *) (* treat calls with no specs as skip functions in angelic mode *) - (* TODO: turn angelic back on for C_CPP once we have abductive angelic analysis (t6935559) *) - || (!Config.angelic_execution && !Sil.curr_language <> Sil.C_CPP - && Specs.get_specs_from_payload summary == []) in + || (!Config.angelic_execution && Specs.get_specs_from_payload summary == []) in if !Config.intraprocedural then true else if should_skip () then (print_skip_warning (); true) else false @@ -1040,114 +1033,158 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl = let f plist instr = list_flatten (list_map (exe_instr instr) plist) in list_fold_left f ppl instrs +and add_to_footprint abducted_pv typ prop = + let abducted_lvar = Sil.Lvar abducted_pv in + let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in + let lvar_pt_fpvar = + let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in + Prop.mk_ptsto abducted_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in + let sigma_fp = Prop.get_sigma_footprint prop in + (Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop), fresh_fp_var) + +and add_constraints_on_retval pdesc prop ret_ids ret_type_option callee_pname = + if Procname.is_infer_undefined callee_pname then prop + else + match ret_ids, ret_type_option with + | [ret_id], Some ret_typ -> + (* To avoid obvious false positives, assume skip functions do not return null pointers *) + let add_ret_non_null ret_id ret_typ prop = + match ret_typ with + | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop + | _ -> prop in + let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *) + Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in + if !Config.angelic_execution && not (is_rec_call callee_pname) then + (* introduce a fresh program variable to allow abduction on the return value *) + let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in + let already_has_abducted_retval p = + list_exists + (fun hpred -> match hpred with + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv + | _ -> false) + (Prop.get_sigma_footprint p) in + (* prevent introducing multiple abducted retvals for a single call site in a loop *) + if already_has_abducted_retval prop then prop + else + if !Config.footprint then + let (prop', fresh_fp_var) = add_to_footprint abducted_ret_pv ret_typ prop in + let prop'' = Prop.conjoin_eq ~footprint:true (Sil.Var ret_id) fresh_fp_var prop' in + add_ret_non_null ret_id ret_typ prop'' + else + (* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *) + let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop = + let bind_exp prop = function + | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _) + when Sil.pvar_equal pv abducted_pvar -> + Prop.conjoin_eq exp_to_bind rhs prop + | _ -> prop in + list_fold_left bind_exp prop (Prop.get_sigma prop) in + (* bind return id to the abducted value pointed to by the pvar we introduced *) + bind_exp_to_abducted_val (Sil.Var ret_id) abducted_ret_pv prop + else add_ret_non_null ret_id ret_typ prop + | _ -> prop + +and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname = + (* replace an hpred of the form actual_var |-> _ with new_hpred in prop *) + let replace_actual_hpred actual_var new_hpred prop = + let sigma' = + list_map + (function + | Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual_var -> new_hpred + | hpred -> hpred) + (Prop.get_sigma prop) in + Prop.normalize (Prop.replace_sigma sigma' prop) in + if !Config.angelic_execution then + let add_actual_by_ref_to_footprint prop (actual, actual_typ) = + match actual with + | Sil.Lvar actual_pv -> + (* introduce a fresh program variable to allow abduction on the return value *) + let abducted_ref_pv = + Sil.mk_pvar_abducted_ref_param callee_pname actual_pv (State.get_loc ()) in + let already_has_abducted_retval p = + list_exists + (fun hpred -> match hpred with + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ref_pv + | _ -> false) + (Prop.get_sigma_footprint p) in + (* prevent introducing multiple abducted retvals for a single call site in a loop *) + if already_has_abducted_retval prop then prop + else + if !Config.footprint then + let (prop', fresh_fp_var) = + add_to_footprint abducted_ref_pv (Sil.typ_strip_ptr actual_typ) prop in + (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) + let filtered_sigma = + list_map + (function + | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual -> + Sil.Hpointsto (lhs, Sil.Eexp (fresh_fp_var, Sil.Inone), typ_exp) + | hpred -> hpred) + (Prop.get_sigma prop') in + Prop.normalize (Prop.replace_sigma filtered_sigma prop') + else + (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *) + let prop' = + let filtered_sigma = + list_filter + (function + | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual -> + false + | _ -> true) + (Prop.get_sigma prop) in + Prop.normalize (Prop.replace_sigma filtered_sigma prop) in + list_fold_left + (fun p hpred -> + match hpred with + | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Sil.pvar_equal pv abducted_ref_pv -> + let new_hpred = Sil.Hpointsto (actual, rhs, texp) in + Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p) + | _ -> p) + prop' + (Prop.get_sigma prop') + | _ -> assert false in + list_fold_left add_actual_by_ref_to_footprint prop actuals_by_ref + else + (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *) + let havoc_actual_by_ref (actual, actual_typ) prop = + let actual_pt_havocd_var = + let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in + let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, Sil.Subtype.subtypes) in + Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in + replace_actual_hpred actual actual_pt_havocd_var prop in + list_fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref + (** execute a call for an unknown or scan function *) and call_unknown_or_scan is_scan cfg pdesc tenv pre path ret_ids ret_type_option actual_pars callee_pname loc = - let instrs, undef_vars = (* instructions to set vars passed by reference to fresh ids *) - let gen_instrs = ref [] in - let gen_undef_vars = ref [] in - let add_instr instr = gen_instrs := instr :: !gen_instrs in - let add_undef_var var = gen_undef_vars := var :: !gen_undef_vars in - let type_is_not_structured = function - | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tenum _ -> true - | Sil.Tvar _ | Sil.Tstruct _ | Sil.Tarray _ -> false in - let expand_ptr_type t = match t with - | Sil.Tptr (Sil.Tvar tn, pk) -> - (match Sil.tenv_lookup tenv tn with - | Some typ -> Sil.Tptr (typ, pk) - | None -> t) - | _ -> t in - let do_actual_par (e, _t) = - let t = expand_ptr_type _t in - L.d_str "do_actual_par exp: "; Sil.d_exp e; L.d_str" typ: "; Sil.d_typ_full t; L.d_ln(); - match e, t with - | _, Sil.Tptr (Sil.Tint ik, pk) when is_scan && Sil.ikind_is_char ik -> (* scan case "%s" *) - let infer_get_array_size = Procname.from_string "__get_array_size" in - let instr1 = Sil.Call ([], Sil.Const (Sil.Cfun infer_get_array_size), [(e, Sil.Tptr (Sil.Tint ik, pk))], loc, Sil.cf_default) in - let id_fresh = Ident.create_fresh Ident.kprimed in - let instr2 = Sil.Letderef (id_fresh, e, t, loc) in - add_instr instr1; - add_instr instr2 - | Sil.Lvar _, Sil.Tptr (t', _) when type_is_not_structured t' -> - let id_fresh = Ident.create_fresh Ident.kprimed in - let instr = Sil.Set (e, t, Sil.Var id_fresh, loc) in - add_instr instr; - add_undef_var id_fresh - | Sil.Lvar _, Sil.Tptr ((Sil.Tstruct (ftal, sftal, _, _, _, _, _) as tstruct, _)) -> - let do_fld (f, typ, ann) = - let id_fresh = Ident.create_fresh Ident.kprimed in - let instr = Sil.Set (Sil.Lfield (e, f, tstruct), typ, Sil.Var id_fresh, loc) in - add_instr instr; - add_undef_var id_fresh in - list_iter do_fld ftal - | _ -> () in - list_iter do_actual_par actual_pars; - list_rev !gen_instrs, list_rev !gen_undef_vars in let remove_resource_att prop = let do_exp p (e, t) = let do_attribute q = function | Sil.Aresource _ as res -> - Prop.remove_attribute res q + Prop.remove_attribute res q | _ -> q in list_fold_left do_attribute p (Prop.get_exp_attributes p e) in list_fold_left do_exp prop actual_pars in - let prop = - if !Sil.curr_language <> Sil.Java || Procname.is_infer_undefined callee_pname then pre - else - let prop_no_res = remove_resource_att pre in - match ret_ids, ret_type_option with - | [ret_id], Some ret_typ -> - (* To avoid obvious false positives, assume skip functions do not return null pointers *) - let add_ret_non_null ret_id ret_typ prop = - match ret_typ with - | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop - | _ -> prop in - let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *) - Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in - if !Config.angelic_execution && not (is_rec_call callee_pname) then - (* introduce a fresh program variable to allow abduction on the return value *) - let ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in - let already_has_abducted_retval p = - list_exists - (fun hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv ret_pv - | _ -> false - ) - (Prop.get_sigma_footprint p) in - (* prevent introducing multiple abducted retvals for a single call site in a loop *) - if already_has_abducted_retval prop_no_res then prop_no_res - else - let ret_lvar = Sil.Lvar ret_pv in - let sizeof_exp = Sil.Sizeof (ret_typ, Sil.Subtype.subtypes) in - if !Config.footprint then - let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in - let retval_pt_fpvar = - Prop.mk_ptsto ret_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in - let sigma_fp = Prop.get_sigma_footprint prop_no_res in - let prop = Prop.replace_sigma_footprint (retval_pt_fpvar :: sigma_fp) prop_no_res in - let prop' = Prop.normalize prop in - let prop'' = Prop.conjoin_eq ~footprint: true (Sil.Var ret_id) fresh_fp_var prop' in - add_ret_non_null ret_id ret_typ prop'' - else - (* bind return id to the abducted value pointed to by the pvar we introduced *) - let bind_return_id prop = function - | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _) - when Sil.pvar_equal pv ret_pv -> - Prop.conjoin_eq (Sil.Var ret_id) rhs prop - | _ -> prop in - list_fold_left bind_return_id prop_no_res (Prop.get_sigma prop_no_res) - else add_ret_non_null ret_id ret_typ prop_no_res - | _ -> prop_no_res in - let after_ref_var_instrs = (* assign fresh values to vars passed by ref *) - let report_error = is_scan in - sym_exec_generated (not report_error) cfg tenv pdesc instrs [(prop, path)] in - let vars_to_mark_undefined = ret_ids @ undef_vars in - let att_undef = Sil.Aundef (callee_pname, loc, State.get_path_pos ()) in - let mark_undefined_vars p = (* add undefined attribute to returned vars and new values for vars passed by ref *) - list_fold_left (fun p id -> mark_id_as_undefined id p att_undef) p vars_to_mark_undefined in - if is_scan (* if scan function, don't mark values with undef attributes *) - then list_map (fun (p, path) -> (Tabulation.remove_constant_string_class p, path)) after_ref_var_instrs - else list_map (fun (p, path) -> (mark_undefined_vars p, path)) after_ref_var_instrs + let actuals_by_ref = + list_filter + (function + | Sil.Lvar _, _ -> true + | _ -> false) + actual_pars in + (* in Java, assume that skip functions close resources passed as params *) + let pre' = if !Sil.curr_language = Sil.Java then remove_resource_att pre else pre in + let pre'' = add_constraints_on_retval pdesc pre' ret_ids ret_type_option callee_pname in + let pre''' = add_constraints_on_actuals_by_ref pre'' actuals_by_ref callee_pname in + if is_scan (* if scan function, don't mark anything with undef attributes *) + then [(Tabulation.remove_constant_string_class pre''', path)] + else + (* otherwise, add undefined attribute to retvals and actuals passed by ref *) + let exps_to_mark = + let ret_exps = list_map (fun ret_id -> Sil.Var ret_id) ret_ids in + list_fold_left + (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in + let path_pos = State.get_path_pos () in + [(Prop.mark_vars_as_undefined pre''' exps_to_mark callee_pname loc path_pos, path)] (** Perform symbolic execution for a function call *) and sym_exe_call cfg pdesc tenv pre path ret_ids actual_pars callee_pdesc loc = diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/angelism.c b/infer/tests/codetoanalyze/c/errors/null_dereference/angelism.c index e66eeaf3d..a933fc387 100644 --- a/infer/tests/codetoanalyze/c/errors/null_dereference/angelism.c +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/angelism.c @@ -40,3 +40,43 @@ struct delicious *skip_external_function(void) { i = cake->yum; return cake; } + +void by_ref_actual_already_in_footprint(struct delicious *param) { + int i; + struct delicious * ret = bakery(¶m); + i = param->yum; +} + +void call_by_ref_actual_already_in_footprint_ok() { + by_ref_actual_already_in_footprint(NULL); // should not report a warning +} + +void by_ref_actual_already_in_footprint2(struct delicious *param) { + int i; + i = param->yum; // should not report a warning + struct delicious * ret = bakery(¶m); + i = param->yum; // should not report a warning +} + +void call_by_ref_actual_already_in_footprint_bad() { + by_ref_actual_already_in_footprint2(NULL); // should report a warning +} + +void passByRefTwice() { + struct delicious *param; + bakery2(¶m, ¶m); // should not report a warning + int i = param->yum; +} + +struct delicious * returnPassByRef2() { + struct delicious *param = NULL; + bakery(¶m); + int i = param->yum; // should not report a warning + return param; +} + +void returnPassByRefDeref() { + struct delicious *ret = returnPassByRef(); + ret->yum = 2; // should not report a warning + free(ret); +} diff --git a/infer/tests/endtoend/c/AngelismTest.java b/infer/tests/endtoend/c/AngelismTest.java index d31788ed5..c504e7471 100644 --- a/infer/tests/endtoend/c/AngelismTest.java +++ b/infer/tests/endtoend/c/AngelismTest.java @@ -37,6 +37,7 @@ public class AngelismTest { public void angelismTest() throws InterruptedException, IOException, InferException { String[] procedures = { "bake", + "call_by_ref_actual_already_in_footprint_bad" }; assertThat( "Results should contain null pointer dereference error",