diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re index c87b55639..ed4f53a4f 100644 --- a/infer/src/IR/Pvar.re +++ b/infer/src/IR/Pvar.re @@ -27,6 +27,7 @@ type pvar_kind = | Callee_var Typ.Procname.t /** local variable belonging to a callee */ | Abduced_retvar Typ.Procname.t Location.t /** synthetic variable to represent return value */ | Abduced_ref_param Typ.Procname.t t Location.t + | Abduced_ref_param_val Typ.Procname.t Ident.t Location.t /** synthetic variable to represent param passed by reference */ | Global_var (translation_unit, bool, bool, bool) /** global variable: translation unit + is it compile constant? + is it POD? + is it a static @@ -70,6 +71,12 @@ let rec _pp f pv => { } else { F.fprintf f "%a$%a%a|abducedRefParam" Typ.Procname.pp n Location.pp l Mangled.pp name } + | Abduced_ref_param_val n id l => + if !Config.pp_simple { + F.fprintf f "%a|%a|abducedRefParamVal" (Ident.pp Pp.text) id Mangled.pp name + } else { + F.fprintf f "%a$%a%a|abducedRefParamVal" Typ.Procname.pp n Location.pp l Mangled.pp name + } | Global_var (translation_unit, is_const, is_pod, _) => F.fprintf f @@ -120,6 +127,14 @@ let pp_latex f pv => { (Mangled.to_string name) (Latex.pp_string Latex.Roman) "abducedRefParam" + | Abduced_ref_param_val _ => + F.fprintf + f + "%a_{%a}" + (Latex.pp_string Latex.Roman) + (Mangled.to_string name) + (Latex.pp_string Latex.Roman) + "abducedRefParamVal" | Global_var _ => Latex.pp_string Latex.Boldface f (Mangled.to_string name) | Seed_var => F.fprintf @@ -194,7 +209,8 @@ let get_simplified_name pv => { let is_abduced pv => switch pv.pv_kind { | Abduced_retvar _ - | Abduced_ref_param _ => true + | Abduced_ref_param _ + | Abduced_ref_param_val _ => true | _ => false }; @@ -291,6 +307,7 @@ let to_callee pname pvar => | Callee_var _ | Abduced_retvar _ | Abduced_ref_param _ + | Abduced_ref_param_val _ | Seed_var => L.d_str "Cannot convert pvar to callee: "; d pvar; @@ -353,6 +370,11 @@ let mk_abduced_ref_param (proc_name: Typ.Procname.t) (pv: t) (loc: Location.t) : {pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_ref_param proc_name pv loc} }; +let mk_abduced_ref_param_val (proc_name: Typ.Procname.t) (id: Ident.t) (loc: Location.t) :t => { + let name = Mangled.from_string ("$REF_PARAM_VAL_" ^ Typ.Procname.to_unique_id proc_name); + {pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_ref_param_val proc_name id loc} +}; + let get_translation_unit pvar => switch pvar.pv_kind { | Global_var (tu, _, _, _) => tu diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei index 0a05e75e3..22fec3e49 100644 --- a/infer/src/IR/Pvar.rei +++ b/infer/src/IR/Pvar.rei @@ -105,6 +105,10 @@ let mk: Mangled.t => Typ.Procname.t => t; let mk_abduced_ref_param: Typ.Procname.t => t => Location.t => t; +/** create an abduced variable for a parameter passed by reference */ +let mk_abduced_ref_param_val: Typ.Procname.t => Ident.t => Location.t => t; + + /** create an abduced return variable for a call to [proc_name] at [loc] */ let mk_abduced_ret: Typ.Procname.t => Location.t => t; diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 3760d7dcd..ca65f27e3 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1290,66 +1290,68 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call prop.Prop.sigma in Prop.normalize tenv (Prop.set prop ~sigma:sigma') in let add_actual_by_ref_to_footprint prop (actual, actual_typ, _) = - match actual with - | Exp.Lvar actual_pv -> - (* introduce a fresh program variable to allow abduction on the return value *) - let abduced_ref_pv = - Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc in - let already_has_abduced_retval p = - List.exists - ~f:(fun hpred -> match hpred with - | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced_ref_pv - | _ -> false) - p.Prop.sigma_fp in - (* prevent introducing multiple abduced retvals for a single call site in a loop *) - if already_has_abduced_retval prop then prop - else - if !Config.footprint then - let prop', abduced_strexp = - match actual_typ.Typ.desc with - | Typ.Tptr ({desc=Tstruct _} as typ, _) -> - (* for struct types passed by reference, do abduction on the fields of the - struct *) - add_struct_value_to_footprint tenv abduced_ref_pv typ prop - | Typ.Tptr (typ, _) -> - (* for pointer types passed by reference, do abduction directly on the pointer *) - let (prop', fresh_fp_var) = - add_to_footprint tenv abduced_ref_pv typ prop in - prop', Sil.Eexp (fresh_fp_var, Sil.Inone) - | _ -> - failwith - ("No need for abduction on non-pointer type " ^ - (Typ.to_string actual_typ)) in - (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) - let filtered_sigma = - List.map - ~f:(function - | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual -> - Sil.Hpointsto (lhs, abduced_strexp, typ_exp) - | hpred -> hpred) - prop'.Prop.sigma in - Prop.normalize tenv (Prop.set prop' ~sigma:filtered_sigma) - else - (* bind actual passed by ref to the abduced value pointed to by the synthetic pvar *) - let prop' = - let filtered_sigma = - List.filter - ~f:(function - | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual -> - false - | _ -> true) - prop.Prop.sigma in - Prop.normalize tenv (Prop.set prop ~sigma:filtered_sigma) in - List.fold - ~f:(fun p hpred -> - match hpred with - | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abduced_ref_pv -> - let new_hpred = Sil.Hpointsto (actual, rhs, texp) in - Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) - | _ -> p) - ~init:prop' - prop'.Prop.sigma - | _ -> assert false in + let abduced = match actual with + | Exp.Lvar actual_pv -> + Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc + | Exp.Var actual_id -> + Pvar.mk_abduced_ref_param_val callee_pname actual_id callee_loc + | _ -> assert false + in + let already_has_abduced_retval p = + List.exists + ~f:(fun hpred -> match hpred with + | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced + | _ -> false) + p.Prop.sigma_fp in + (* prevent introducing multiple abduced retvals for a single call site in a loop *) + if already_has_abduced_retval prop then prop + else + if !Config.footprint then + let prop', abduced_strexp = + match actual_typ.Typ.desc with + | Typ.Tptr ({desc=Tstruct _} as typ, _) -> + (* for struct types passed by reference, do abduction on the fields of the + struct *) + add_struct_value_to_footprint tenv abduced typ prop + | Typ.Tptr (typ, _) -> + (* for pointer types passed by reference, do abduction directly on the pointer *) + let (prop', fresh_fp_var) = + add_to_footprint tenv abduced typ prop in + prop', Sil.Eexp (fresh_fp_var, Sil.Inone) + | _ -> + failwith + ("No need for abduction on non-pointer type " ^ + (Typ.to_string actual_typ)) in + (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) + let filtered_sigma = + List.map + ~f:(function + | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual -> + Sil.Hpointsto (lhs, abduced_strexp, typ_exp) + | hpred -> hpred) + prop'.Prop.sigma in + Prop.normalize tenv (Prop.set prop' ~sigma:filtered_sigma) + else + (* bind actual passed by ref to the abduced value pointed to by the synthetic pvar *) + let prop' = + let filtered_sigma = + List.filter + ~f:(function + | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual -> + false + | _ -> true) + prop.Prop.sigma in + Prop.normalize tenv (Prop.set prop ~sigma:filtered_sigma) in + List.fold + ~f:(fun p hpred -> + match hpred with + | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abduced -> + let new_hpred = Sil.Hpointsto (actual, rhs, texp) in + Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) + | _ -> p) + ~init:prop' + prop'.Prop.sigma + in (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *) let havoc_actual_by_ref prop (actual, actual_typ, _) = let actual_pt_havocd_var = @@ -1435,10 +1437,29 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots actuals |> fst else prop in + let should_abduce_param_value pname = + let open Typ.Procname in + match pname with + | Java _ -> + (* FIXME (T19882766): we need to disable this for Java because it breaks too many tests *) + false + | ObjC_Cpp _ -> + (* FIXME: we need to work around a frontend hack for std::shared_ptr + * to silent some of the uninitialization warnings *) + if String.is_suffix ~suffix:"_std__shared_ptr" + (Typ.Procname.to_string callee_pname) then + false + else + true + | _ -> true + in let actuals_by_ref = List.filter_mapi ~f:(fun i actual -> match actual with | (Exp.Lvar _ as e, ({Typ.desc=Tptr _} as t)) -> Some (e, t, i) + | (Exp.Var _ as e, ({Typ.desc=Tptr _} as t)) + when should_abduce_param_value callee_pname -> + Some (e, t, i) | _ -> None) args in let has_nullable_annot = Annotations.ia_is_nullable ret_annots in diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index 022c57daa..ff5c11ec2 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -52,6 +52,8 @@ codetoanalyze/cpp/errors/numeric/min_max.cpp, max_int_div0, 0, DIVIDE_BY_ZERO, [ codetoanalyze/cpp/errors/numeric/min_max.cpp, min_X_div0, 2, DIVIDE_BY_ZERO, [start of procedure min_X_div0(),start of procedure X,return from a call to X_X,start of procedure X,return from a call to X_X] codetoanalyze/cpp/errors/numeric/min_max.cpp, min_int_div0, 0, DIVIDE_BY_ZERO, [start of procedure min_int_div0()] codetoanalyze/cpp/errors/overwrite_attribute/main.cpp, testSetIntValue, 3, DIVIDE_BY_ZERO, [start of procedure testSetIntValue(),start of procedure setIntValue(),return from a call to setIntValue] +codetoanalyze/cpp/errors/pointers/unintialized.cpp, known_ctor_dangling_bad, 2, DANGLING_POINTER_DEREFERENCE, [start of procedure known_ctor_dangling_bad(),start of procedure TestDangling,return from a call to TestDangling_TestDangling] +codetoanalyze/cpp/errors/pointers/unintialized.cpp, known_ctor_dangling_bad, 2, UNINITIALIZED_VALUE, [start of procedure known_ctor_dangling_bad(),start of procedure TestDangling,return from a call to TestDangling_TestDangling] codetoanalyze/cpp/errors/pointers/unintialized.cpp, uninitialized_dangling_bad, 2, DANGLING_POINTER_DEREFERENCE, [start of procedure uninitialized_dangling_bad()] codetoanalyze/cpp/errors/pointers/unintialized.cpp, uninitialized_dangling_bad, 2, UNINITIALIZED_VALUE, [start of procedure uninitialized_dangling_bad()] codetoanalyze/cpp/errors/resource_leaks/raii.cpp, resource_leak, 7, RESOURCE_LEAK, [start of procedure resource_leak(),Condition is false] diff --git a/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp b/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp index af1b90ffb..921445cb1 100644 --- a/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp @@ -15,3 +15,28 @@ void uninitialized_dangling_bad() { int* p; delete p; } + +struct TestDangling { + int* p; + // Field p is deliberately left uninitialized + TestDangling() {} + // This constructor is deliberately left unimplemented + // to make sure Infer treats undefined function conservatively + TestDangling(int); +}; + +int known_ctor_dangling_bad() { + auto t0 = new TestDangling(); + int ret = *(t0->p); // should report a dangling pointer dereference here as p + // is dangling + delete t0; + return ret; +} + +int unknown_ctor_assume_no_dangling_ok() { + auto t1 = new TestDangling(0); + int ret = + *(t1->p); // TestDangling(0) is not known so p may have been initialized + delete t1; + return ret; +} diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 3f22a78eb..c83d5069e 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/infer/tests/codetoanalyze/objc/errors/issues.exp @@ -13,7 +13,6 @@ codetoanalyze/objc/errors/npe/null_returned_by_method.m, NullReturnedByMethodA_t codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 2, MEMORY_LEAK, [start of procedure ProcdescMain(),Skipped call: function or method not found] codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 3, MEMORY_LEAK, [start of procedure ProcdescMain(),Skipped call: function or method not found] codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 1, MEMORY_LEAK, [start of procedure call_nslog()] -codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 2, MEMORY_LEAK, [start of procedure call_nslog(),Skipped call: function or method not found] codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 3, MEMORY_LEAK, [start of procedure call_nslog(),Skipped call: function or method not found] codetoanalyze/objc/errors/property/main.c, property_main, 2, MEMORY_LEAK, [start of procedure property_main(),Skipped call: function or method not found] codetoanalyze/objc/errors/property/main.c, property_main, 3, MEMORY_LEAK, [start of procedure property_main(),Skipped call: function or method not found]