diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 1449f04fc..566f8ea9d 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -51,10 +51,11 @@ module PulseTransferFunctions = struct let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in PulseCallOperations.conservatively_initialize_args arg_values astate in - [ Ok - (ContinueProgram - (PulseCallOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret - ~actuals ~formals_opt:None astate)) ] + let<+> astate = + PulseCallOperations.unknown_call tenv path call_loc (SkippedUnknownCall call_exp) ~ret + ~actuals ~formals_opt:None astate + in + astate (** has an object just gone out of scope? *) diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index d6e826152..154c1c9b0 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -32,6 +32,11 @@ let and_eq_int v i astate = type operand = PathCondition.operand = | LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + | FunctionApplicationOperand of {f: PulseFormula.function_symbol; actuals: AbstractValue.t list} + +let and_equal op1 op2 astate = + map_path_condition astate ~f:(fun phi -> PathCondition.and_equal op1 op2 phi) + let eval_binop binop_addr binop op_lhs op_rhs astate = map_path_condition astate ~f:(fun phi -> diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 1fdc04c2f..5f489c3fc 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -22,6 +22,9 @@ val and_eq_int : type operand = PathCondition.operand = | LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + | FunctionApplicationOperand of {f: PulseFormula.function_symbol; actuals: AbstractValue.t list} + +val and_equal : operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t val eval_binop : AbstractValue.t diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 8b4d6ea47..8773a6d23 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -18,9 +18,13 @@ let is_ptr_to_const formal_typ_opt = match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false ) -let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = +let unknown_call tenv path call_loc (reason : CallEvent.t) ~ret ~actuals ~formals_opt astate = let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in - let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in + let ret_val = AbstractValue.mk_fresh () in + let astate = PulseOperations.write_id (fst ret) (ret_val, [event]) astate in + (* set to [false] if we think the procedure called does not behave "functionally", i.e. return the + same value for the same inputs *) + let is_functional = ref true in let rec havoc_fields ((_, history) as addr) typ astate = match typ.Typ.desc with | Tstruct struct_name -> ( @@ -36,13 +40,14 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = astate in let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = - (* We should not havoc when the corresponding formal is a - pointer to const *) + (* We should not havoc when the corresponding formal is a pointer to const *) match actual_typ.Typ.desc with | Tptr (typ, _) when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) -> - (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when - havoc'ing pointer parameters (which normally causes a [check_valid] call. *) + is_functional := false ; + (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid + raising issues when havoc'ing pointer parameters (which normally causes a [check_valid] + call. *) let fresh_value = AbstractValue.mk_fresh () in Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate |> havoc_fields actual typ @@ -50,8 +55,28 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = astate in let add_skipped_proc astate = + let* astate, f = + match reason with + | Call _ | Model _ -> + Ok (astate, None) + | SkippedKnownCall proc_name -> + Ok (astate, Some (PulseFormula.Procname proc_name)) + | SkippedUnknownCall e -> + let+ astate, (v, _) = PulseOperations.eval path Read call_loc e astate in + (astate, Some (PulseFormula.Unknown v)) + in + let+ astate = + match f with + | None -> + Ok astate + | Some f -> + PulseArithmetic.and_equal (AbstractValueOperand ret_val) + (FunctionApplicationOperand + {f; actuals= List.map ~f:(fun ((actual_val, _hist), _typ) -> actual_val) actuals}) + astate + in match reason with - | CallEvent.SkippedKnownCall proc_name -> + | SkippedKnownCall proc_name -> AbductiveDomain.add_skipped_call proc_name (Trace.Immediate {location= call_loc; history= []}) astate @@ -59,20 +84,17 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = astate in let havoc_actuals_without_typ_info astate = - List.fold actuals - ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) - ~init:astate + List.fold actuals ~init:astate ~f:(fun astate actual_typ -> + havoc_actual_if_ptr actual_typ None astate ) in - L.d_printfln "skipping unknown procedure@." ; + L.d_printfln "skipping unknown procedure" ; ( match formals_opt with | None -> havoc_actuals_without_typ_info astate | Some formals -> ( match - List.fold2 actuals formals - ~f:(fun astate actual_typ (_, formal_typ) -> + List.fold2 actuals formals ~init:astate ~f:(fun astate actual_typ (_, formal_typ) -> havoc_actual_if_ptr actual_typ (Some formal_typ) astate ) - ~init:astate with | Unequal_lengths -> L.d_printfln "ERROR: formals have length %d but actuals have length %d" @@ -80,7 +102,7 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = havoc_actuals_without_typ_info astate | Ok result -> result ) ) - |> havoc_ret ret |> add_skipped_proc + |> add_skipped_proc let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret @@ -269,9 +291,10 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary. (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in - let astate_unknown = + let<*> astate_unknown = conservatively_initialize_args arg_values astate - |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt + |> unknown_call tenv path call_loc (SkippedKnownCall callee_pname) ~ret ~actuals + ~formals_opt in let callee_procdesc_opt = AnalysisCallbacks.get_proc_desc callee_pname in Option.value_map callee_procdesc_opt diff --git a/infer/src/pulse/PulseCallOperations.mli b/infer/src/pulse/PulseCallOperations.mli index c8ed96304..ea27c01b3 100644 --- a/infer/src/pulse/PulseCallOperations.mli +++ b/infer/src/pulse/PulseCallOperations.mli @@ -28,13 +28,14 @@ val call : val unknown_call : Tenv.t + -> PathContext.t -> Location.t -> CallEvent.t -> ret:Ident.t * Typ.t -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> formals_opt:(Pvar.t * Typ.t) list option -> t - -> t + -> t AccessResult.t (** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate *) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 28232a7be..5796fcab0 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -14,7 +14,29 @@ module Q = QSafeCapped module Z = ZSafe open SatUnsat -type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t +type function_symbol = Unknown of Var.t | Procname of Procname.t +[@@deriving compare, equal, yojson_of] + +let pp_function_symbol fmt = function + | Unknown v -> + Var.pp fmt v + | Procname proc_name -> + Procname.pp fmt proc_name + + +type operand = + | LiteralOperand of IntLit.t + | AbstractValueOperand of Var.t + | FunctionApplicationOperand of {f: function_symbol; actuals: Var.t list} + +let pp_operand fmt = function + | LiteralOperand i -> + IntLit.pp fmt i + | AbstractValueOperand v -> + Var.pp fmt v + | FunctionApplicationOperand {f; actuals} -> + F.fprintf fmt "%a(%a)" pp_function_symbol f (Pp.seq ~sep:"," Var.pp) actuals + (** Linear Arithmetic *) module LinArith : sig @@ -194,6 +216,8 @@ module Term = struct type t = | Const of Q.t | Var of Var.t + | Procname of Procname.t + | FunctionApplication of {f: t; actuals: t list} | Linear of LinArith.t | Add of t * t | Minus of t @@ -228,6 +252,10 @@ module Term = struct false | Linear _ -> false + | Procname _ -> + false + | FunctionApplication _ -> + false | Minus _ | BitNot _ | Not _ @@ -259,6 +287,12 @@ module Term = struct pp_var fmt v | Const c -> Q.pp_print fmt c + | Procname proc_name -> + Procname.pp fmt proc_name + | FunctionApplication {f; actuals} -> + F.fprintf fmt "%a(%a)" (pp_paren pp_var ~needs_paren) f + (Pp.seq ~sep:"," (pp_paren pp_var ~needs_paren)) + actuals | Linear l -> F.fprintf fmt "[%a]" (LinArith.pp pp_var) l | Minus t -> @@ -312,6 +346,9 @@ module Term = struct Var v | LiteralOperand i -> IntLit.to_big_int i |> Q.of_bigint |> of_q + | FunctionApplicationOperand {f; actuals} -> + let f = match f with Unknown v -> Var v | Procname proc_name -> Procname proc_name in + FunctionApplication {f; actuals= List.map actuals ~f:(fun v -> Var v)} let of_subst_target = function QSubst q -> of_q q | VarSubst v -> Var v | LinSubst l -> Linear l @@ -373,8 +410,22 @@ module Term = struct (** Fold [f] on the strict sub-terms of [t], if any. Preserve physical equality if [f] does. *) let fold_map_direct_subterms t ~init ~f = match t with - | Var _ | Const _ | Linear _ | IsInstanceOf _ -> + (* no sub-terms *) + | Var _ | Const _ | Procname _ | Linear _ | IsInstanceOf _ -> (init, t) + (* list of sub-terms *) + | FunctionApplication {f= t_f; actuals} -> + let acc, t_f' = f init t_f in + let changed = ref (not (phys_equal t_f t_f')) in + let acc, actuals' = + List.fold_map actuals ~init:acc ~f:(fun acc actual -> + let acc, actual' = f acc actual in + changed := !changed || not (phys_equal actual actual') ; + (acc, actual') ) + in + let t' = if !changed then FunctionApplication {f= t_f'; actuals= actuals'} else t in + (acc, t') + (* one sub-term *) | Minus t_not | BitNot t_not | Not t_not -> let acc, t_not' = f init t_not in let t' = @@ -389,6 +440,7 @@ module Term = struct Not t_not' in (acc, t') + (* two sub-terms *) | Add (t1, t2) | Mult (t1, t2) | Div (t1, t2) @@ -486,6 +538,8 @@ module Term = struct let t' = if phys_equal l l' then t else Linear l' in (acc, t') | Const _ + | Procname _ + | FunctionApplication _ | Add _ | Minus _ | LessThan _ @@ -540,7 +594,7 @@ module Term = struct in let or_undef q_opt = Option.value ~default:Q.undef q_opt in match t0 with - | Const _ | Var _ | IsInstanceOf _ -> + | Const _ | Var _ | IsInstanceOf _ | Procname _ | FunctionApplication _ -> t0 | Linear l -> LinArith.get_as_const l |> Option.value_map ~default:t0 ~f:(fun c -> Const c) @@ -719,6 +773,8 @@ module Term = struct | Div (t, Const c) when Q.is_not_zero c -> let+ l = aux_linearize t in LinArith.mult (Q.inv c) l + | Procname _ + | FunctionApplication _ | Mult _ | Div _ | Mod _ diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index a9da5eb92..1d4d3b4ec 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -25,7 +25,14 @@ val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit [@@warning "-32"] (** only used for unit tests *) -type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t +type function_symbol = Unknown of Var.t | Procname of Procname.t [@@deriving compare] + +type operand = + | LiteralOperand of IntLit.t + | AbstractValueOperand of Var.t + | FunctionApplicationOperand of {f: function_symbol; actuals: Var.t list} + +val pp_operand : F.formatter -> operand -> unit (** {3 Build formulas} *) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index ad51f8313..823a4c4c8 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -93,7 +93,7 @@ module Misc = struct don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we suspect are passed by reference. *) let unknown_call skip_reason args : model = - fun {analysis_data= {tenv}; callee_procname; location; ret} astate -> + fun {analysis_data= {tenv}; path; callee_procname; location; ret} astate -> let actuals = List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> (actual, typ) ) @@ -102,9 +102,11 @@ module Misc = struct AnalysisCallbacks.proc_resolve_attributes callee_procname |> Option.map ~f:Pvar.get_pvar_formals in - PulseCallOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt - astate - |> ok_continue + let<+> astate = + PulseCallOperations.unknown_call tenv path location (Model skip_reason) ~ret ~actuals + ~formals_opt astate + in + astate (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 21c881e3b..474dd10fc 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -107,6 +107,12 @@ let and_eq_vars v1 v2 phi = ({is_unsat; bo_itvs; citvs; formula}, new_eqs) +let and_equal op1 op2 phi = + let+ {is_unsat; bo_itvs; citvs; formula} = phi in + let+| formula, new_eqs = Formula.and_equal op1 op2 formula in + ({is_unsat; bo_itvs; citvs; formula}, new_eqs) + + let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi = if phi.is_unsat then Unsat else @@ -251,15 +257,9 @@ let and_callee subst phi ~callee:phi_callee = type operand = Formula.operand = | LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + | FunctionApplicationOperand of {f: Formula.function_symbol; actuals: AbstractValue.t list} [@@deriving compare] -let pp_operand f = function - | LiteralOperand i -> - IntLit.pp f i - | AbstractValueOperand v -> - AbstractValue.pp f v - - let eval_citv_binop binop_addr bop op_lhs op_rhs citvs = let citv_of_op op citvs = match op with @@ -267,6 +267,8 @@ let eval_citv_binop binop_addr bop op_lhs op_rhs citvs = Some (CItv.equal_to i) | AbstractValueOperand v -> CItvs.find_opt v citvs + | FunctionApplicationOperand _ -> + None in match Option.both (citv_of_op op_lhs citvs) (citv_of_op op_rhs citvs) @@ -282,14 +284,18 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs = let bo_itv_of_op op bo_itvs = match op with | LiteralOperand i -> - Itv.ItvPure.of_int_lit i + Some (Itv.ItvPure.of_int_lit i) | AbstractValueOperand v -> - BoItvs.find_or_default v bo_itvs - in - let bo_itv = - Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs bo_itvs) (bo_itv_of_op op_rhs bo_itvs) + Some (BoItvs.find_or_default v bo_itvs) + | FunctionApplicationOperand _ -> + None in - BoItvs.add binop_addr bo_itv bo_itvs + match Option.both (bo_itv_of_op op_lhs bo_itvs) (bo_itv_of_op op_rhs bo_itvs) with + | Some (bo_lhs, bo_rhs) -> + let bo_itv = Itv.ItvPure.arith_binop bop bo_lhs bo_rhs in + BoItvs.add binop_addr bo_itv bo_itvs + | None -> + bo_itvs let eval_binop binop_addr binop op_lhs op_rhs phi = @@ -347,9 +353,11 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi = let eval_operand phi = function | LiteralOperand i -> - (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i) + (None, Some (CItv.equal_to i), Some (Itv.ItvPure.of_int_lit i)) | AbstractValueOperand v -> - (Some v, CItvs.find_opt v phi.citvs, BoItvs.find_or_default v phi.bo_itvs) + (Some v, CItvs.find_opt v phi.citvs, Some (BoItvs.find_or_default v phi.bo_itvs)) + | FunctionApplicationOperand _ -> + (None, None, None) let record_citv_abduced addr_opt arith_opt citvs = @@ -377,23 +385,29 @@ let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formul in {phi with citvs} in - let is_unsat = - match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with - | False -> - not negated - | True -> - negated - | Top -> - false - | Bottom -> - true - in - if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ; - let+ phi = {phi with is_unsat} in - let+ phi = prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi in let+ phi = - Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' -> - prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) + match Option.both bo_itv_lhs bo_itv_rhs with + | None -> + phi + | Some (bo_itv_lhs, bo_itv_rhs) -> + let is_unsat = + match + Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean + with + | False -> + not negated + | True -> + negated + | Top -> + false + | Bottom -> + true + in + if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ; + let phi = {phi with is_unsat} in + let phi = prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi in + Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' -> + prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) in match Formula.prune_binop ~negated bop lhs_op rhs_op formula with | Unsat -> diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 44f0116c4..f623c4b9d 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -53,10 +53,13 @@ val and_callee : (** {2 Operations} *) -type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t +type operand = PulseFormula.operand = + | LiteralOperand of IntLit.t + | AbstractValueOperand of AbstractValue.t + | FunctionApplicationOperand of {f: PulseFormula.function_symbol; actuals: AbstractValue.t list} [@@deriving compare] -val pp_operand : Formatter.t -> operand -> unit +val and_equal : operand -> operand -> t -> t * new_eqs val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t * new_eqs diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 98cd95ff9..c55fea687 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -171,16 +171,20 @@ end = struct let pp_predicate f (op, l, r) = - Format.fprintf f "@[%a%a%a@]" PathCondition.pp_operand l Binop.pp op PathCondition.pp_operand r + Format.fprintf f "@[%a%a%a@]" PulseFormula.pp_operand l Binop.pp op PulseFormula.pp_operand r let pp = Pp.seq ~sep:"∧" pp_predicate let eliminate_exists ~keep constr = (* TODO(rgrigore): replace the current weak approximation *) - let is_live_operand = - PathCondition.( - function LiteralOperand _ -> true | AbstractValueOperand v -> AbstractValue.Set.mem v keep) + let is_live_operand : PulseFormula.operand -> bool = function + | LiteralOperand _ -> + true + | AbstractValueOperand v -> + AbstractValue.Set.mem v keep + | FunctionApplicationOperand _ -> + true in let is_live_predicate (_op, l, r) = is_live_operand l && is_live_operand r in List.filter ~f:is_live_predicate constr diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index fd7175038..fec0414ab 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -39,6 +39,8 @@ codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERRO codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `z` of several_dereferences_ok,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl index 065197421..d3caea2a8 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl @@ -42,6 +42,8 @@ codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERRO codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index ed7cf0920..986247af6 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -140,3 +140,26 @@ void report_correct_error_among_multiple_bad() { // the trace should complain about the first access inside the callee several_dereferences_ok(p, p, p); } + +int unknown(int x); + +void unknown_is_functional_ok() { + int* p = NULL; + if (unknown(10) != unknown(10)) { + *p = 42; + } +} + +void unknown_with_different_values_bad() { + int* p = NULL; + if (unknown(32) != unknown(52)) { + *p = 42; + } +} + +void unknown_from_parameters_latent(int x) { + int* p = NULL; + if (unknown(x) == 999) { + *p = 42; + } +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 8841d307b..e3b300f54 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -65,7 +65,6 @@ codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, FP_smart_pointer, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [in call to `Node::getShared`,in call to `folly::Optional::Optional(=None)` (modelled),is optional empty,return from call to `Node::getShared`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, FP_std_value_or_check_value_ok, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [in call to `std::optional::optional(=nullopt)` (modelled),is optional empty,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, FP_value_or_check_value_ok, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [in call to `folly::Optional::Optional(=None)` (modelled),is optional empty,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [in call to `folly::Optional::operator=`,in call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional::operator=`,invalid access occurs here] @@ -84,7 +83,7 @@ codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 4, OPTIONAL_EMPTY_ACCESS, codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,null pointer dereference part of the trace starts here,in call to `may_return_null`,is the null pointer,returned,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `may_return_null`,is the null pointer,returned,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,in call to `WrapsB::WrapsB`,allocated by call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `getwrapperHeap`,in call to `WrapsB::WrapsB`,allocated by call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,in call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,in call to `WrapsB::getb`,parameter `this` of WrapsB::getb,returned,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here] -codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,in call to `getwrapperStack`,variable `b` declared here,in call to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,in call to `getwrapperStack`,variable `b` declared here,in call to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here] diff --git a/infer/tests/codetoanalyze/java/pulse/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/pulse/NullPointerExceptions.java index 0732ab821..ca46419d3 100644 --- a/infer/tests/codetoanalyze/java/pulse/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/pulse/NullPointerExceptions.java @@ -267,10 +267,12 @@ public class NullPointerExceptions { param.toString(); } - native boolean test(); + native boolean test1(); + + native boolean test2(); Object getObj() { - if (test()) { + if (test1()) { return new Object(); } else { return null; @@ -278,32 +280,36 @@ public class NullPointerExceptions { } Boolean getBool() { - if (test()) { + if (test2()) { return new Boolean(true); } else { return null; } } - void FP_derefGetterAfterCheckShouldNotCauseNPE() { + void derefGetterAfterCheckShouldNotCauseNPE() { if (getObj() != null) { getObj().toString(); } } - void FP_derefBoxedGetterAfterCheckShouldNotCauseNPE() { + void derefBoxedGetterAfterCheckShouldNotCauseNPE() { boolean b = getBool() != null && getBool(); } - static void FP_derefNonThisGetterAfterCheckShouldNotCauseNPE() { + static void derefNonThisGetterAfterCheckShouldNotCauseNPE() { NullPointerExceptions c = new NullPointerExceptions(); if (c.getObj() != null) { c.getObj().toString(); } } - void badCheckShouldCauseNPE() { - if (getBool() != null) getObj().toString(); + // latent because we don't know if test1() can return "true" + // arguably should be reported? + void badCheckShouldCauseNPE_latent() { + if (getBool() != null) { + getObj().toString(); + } } void nullPointerExceptionArrayLength() { diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 8ee7f19c3..5d12ff627 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -35,16 +35,13 @@ codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.clearCausesE codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.getElementNPEBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object Lists.getElement(List)`,is the null pointer,assigned,returned,return from call to `Object Lists.getElement(List)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.removeElementBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefBoxedGetterAfterCheckShouldNotCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Boolean NullPointerExceptions.getBool()`,is the null pointer,returned,return from call to `Boolean NullPointerExceptions.getBool()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefGetterAfterCheckShouldNotCauseNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefNonThisGetterAfterCheckShouldNotCauseNPE():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_otherSinkWithNeverNullSource():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `T SomeLibrary.get()`,is the null pointer,assigned,returned,return from call to `T SomeLibrary.get()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_sinkWithNeverNullSource():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `T NeverNullSource.get()`,is the null pointer,assigned,returned,return from call to `T NeverNullSource.get()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.NPEvalueOfFromHashmapBad(java.util.HashMap,int):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Map.get()` (modelled),is the null pointer,assigned,in call to `cast` (modelled),invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE_latent():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNull():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.derefUndefinedCallee()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.derefUndefinedCallee()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Object NullPointerExceptions.nullableRet(boolean)`,is the null pointer,returned,return from call to `Object NullPointerExceptions.nullableRet(boolean)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,is the null pointer,returned,return from call to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl b/infer/tests/codetoanalyze/java/pulse/issues.exp-isl index 353bfce99..bc6277a06 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp-isl @@ -31,14 +31,11 @@ codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.addInvalidat codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.clearCausesEmptinessNPEBad(java.util.List):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.removeElementBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefBoxedGetterAfterCheckShouldNotCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Boolean NullPointerExceptions.getBool()`,is the null pointer,returned,return from call to `Boolean NullPointerExceptions.getBool()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefGetterAfterCheckShouldNotCauseNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefNonThisGetterAfterCheckShouldNotCauseNPE():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.NPEvalueOfFromHashmapBad(java.util.HashMap,int):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Map.get()` (modelled),is the null pointer,assigned,in call to `cast` (modelled),invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE_latent():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Object NullPointerExceptions.getObj()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNull():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `Object NullPointerExceptions.derefUndefinedCallee()`,is the null pointer,returned,return from call to `Object NullPointerExceptions.derefUndefinedCallee()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,in call to `Object NullPointerExceptions.nullableRet(boolean)`,is the null pointer,returned,return from call to `Object NullPointerExceptions.nullableRet(boolean)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]