[pulse] functional unknown functions

Summary:
Unknown functions may create false positives as well as false negatives
for Pulse. Let's consider that unknown functions behave "functionally",
or at least that a functional behaviour is a possible behaviour for
them: when called with the same parameter values, they should return the
same value.

This is implemented purely in the arithmetic domain by recording
`v_return = f_unknown(v1, v2, ..., vN)` for each call to unknown
functions `f_unknown` with values `v1`, `v2`, ..., `vN` (and return
`v_return`). The hope is that this will create more false negatives than
false positives, as several FPs have been observed on real code that
would be suppressed with this heuristic.

The other effect this has on reports is to record hypotheses made on the
return values of unknown functions into the "pruned" part of formulas,
which inhibits reporting on paths whose feasibility depends on the
return value of unknown functions (by making these issues latent
instead). This should allow us to control the amount of FPs until we
model more functions.

Reviewed By: skcho

Differential Revision: D27798275

fbshipit-source-id: d31cfb8b6
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 24b32c24f4
commit d285ee900b

@ -51,10 +51,11 @@ module PulseTransferFunctions = struct
let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in
PulseCallOperations.conservatively_initialize_args arg_values astate PulseCallOperations.conservatively_initialize_args arg_values astate
in in
[ Ok let<+> astate =
(ContinueProgram PulseCallOperations.unknown_call tenv path call_loc (SkippedUnknownCall call_exp) ~ret
(PulseCallOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret ~actuals ~formals_opt:None astate
~actuals ~formals_opt:None astate)) ] in
astate
(** has an object just gone out of scope? *) (** has an object just gone out of scope? *)

@ -32,6 +32,11 @@ let and_eq_int v i astate =
type operand = PathCondition.operand = type operand = PathCondition.operand =
| LiteralOperand of IntLit.t | LiteralOperand of IntLit.t
| AbstractValueOperand of AbstractValue.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 = let eval_binop binop_addr binop op_lhs op_rhs astate =
map_path_condition astate ~f:(fun phi -> map_path_condition astate ~f:(fun phi ->

@ -22,6 +22,9 @@ val and_eq_int :
type operand = PathCondition.operand = type operand = PathCondition.operand =
| LiteralOperand of IntLit.t | LiteralOperand of IntLit.t
| AbstractValueOperand of AbstractValue.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 : val eval_binop :
AbstractValue.t AbstractValue.t

@ -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 ) 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 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 = let rec havoc_fields ((_, history) as addr) typ astate =
match typ.Typ.desc with match typ.Typ.desc with
| Tstruct struct_name -> ( | Tstruct struct_name -> (
@ -36,13 +40,14 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
astate astate
in in
let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate =
(* We should not havoc when the corresponding formal is a (* We should not havoc when the corresponding formal is a pointer to const *)
pointer to const *)
match actual_typ.Typ.desc with match actual_typ.Typ.desc with
| Tptr (typ, _) | Tptr (typ, _)
when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) -> 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 is_functional := false ;
havoc'ing pointer parameters (which normally causes a [check_valid] call. *) (* 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 let fresh_value = AbstractValue.mk_fresh () in
Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate
|> havoc_fields actual typ |> havoc_fields actual typ
@ -50,8 +55,28 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
astate astate
in in
let add_skipped_proc astate = 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 match reason with
| CallEvent.SkippedKnownCall proc_name -> | SkippedKnownCall proc_name ->
AbductiveDomain.add_skipped_call proc_name AbductiveDomain.add_skipped_call proc_name
(Trace.Immediate {location= call_loc; history= []}) (Trace.Immediate {location= call_loc; history= []})
astate astate
@ -59,20 +84,17 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
astate astate
in in
let havoc_actuals_without_typ_info astate = let havoc_actuals_without_typ_info astate =
List.fold actuals List.fold actuals ~init:astate ~f:(fun astate actual_typ ->
~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) havoc_actual_if_ptr actual_typ None astate )
~init:astate
in in
L.d_printfln "skipping unknown procedure@." ; L.d_printfln "skipping unknown procedure" ;
( match formals_opt with ( match formals_opt with
| None -> | None ->
havoc_actuals_without_typ_info astate havoc_actuals_without_typ_info astate
| Some formals -> ( | Some formals -> (
match match
List.fold2 actuals formals List.fold2 actuals formals ~init:astate ~f:(fun astate actual_typ (_, formal_typ) ->
~f:(fun astate actual_typ (_, formal_typ) ->
havoc_actual_if_ptr actual_typ (Some formal_typ) astate ) havoc_actual_if_ptr actual_typ (Some formal_typ) astate )
~init:astate
with with
| Unequal_lengths -> | Unequal_lengths ->
L.d_printfln "ERROR: formals have length %d but actuals have length %d" 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 havoc_actuals_without_typ_info astate
| Ok result -> | Ok result ->
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 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, ...) *) (* no spec found for some reason (unknown function, ...) *)
L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; 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 arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in
let astate_unknown = let<*> astate_unknown =
conservatively_initialize_args arg_values astate 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 in
let callee_procdesc_opt = AnalysisCallbacks.get_proc_desc callee_pname in let callee_procdesc_opt = AnalysisCallbacks.get_proc_desc callee_pname in
Option.value_map callee_procdesc_opt Option.value_map callee_procdesc_opt

@ -28,13 +28,14 @@ val call :
val unknown_call : val unknown_call :
Tenv.t Tenv.t
-> PathContext.t
-> Location.t -> Location.t
-> CallEvent.t -> CallEvent.t
-> ret:Ident.t * Typ.t -> ret:Ident.t * Typ.t
-> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
-> formals_opt:(Pvar.t * Typ.t) list option -> formals_opt:(Pvar.t * Typ.t) list option
-> t -> t
-> t -> t AccessResult.t
(** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and (** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and
the return value as appropriate *) the return value as appropriate *)

@ -14,7 +14,29 @@ module Q = QSafeCapped
module Z = ZSafe module Z = ZSafe
open SatUnsat 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 *) (** Linear Arithmetic *)
module LinArith : sig module LinArith : sig
@ -194,6 +216,8 @@ module Term = struct
type t = type t =
| Const of Q.t | Const of Q.t
| Var of Var.t | Var of Var.t
| Procname of Procname.t
| FunctionApplication of {f: t; actuals: t list}
| Linear of LinArith.t | Linear of LinArith.t
| Add of t * t | Add of t * t
| Minus of t | Minus of t
@ -228,6 +252,10 @@ module Term = struct
false false
| Linear _ -> | Linear _ ->
false false
| Procname _ ->
false
| FunctionApplication _ ->
false
| Minus _ | Minus _
| BitNot _ | BitNot _
| Not _ | Not _
@ -259,6 +287,12 @@ module Term = struct
pp_var fmt v pp_var fmt v
| Const c -> | Const c ->
Q.pp_print fmt 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 -> | Linear l ->
F.fprintf fmt "[%a]" (LinArith.pp pp_var) l F.fprintf fmt "[%a]" (LinArith.pp pp_var) l
| Minus t -> | Minus t ->
@ -312,6 +346,9 @@ module Term = struct
Var v Var v
| LiteralOperand i -> | LiteralOperand i ->
IntLit.to_big_int i |> Q.of_bigint |> of_q 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 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. *) (** 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 = let fold_map_direct_subterms t ~init ~f =
match t with match t with
| Var _ | Const _ | Linear _ | IsInstanceOf _ -> (* no sub-terms *)
| Var _ | Const _ | Procname _ | Linear _ | IsInstanceOf _ ->
(init, t) (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 -> | Minus t_not | BitNot t_not | Not t_not ->
let acc, t_not' = f init t_not in let acc, t_not' = f init t_not in
let t' = let t' =
@ -389,6 +440,7 @@ module Term = struct
Not t_not' Not t_not'
in in
(acc, t') (acc, t')
(* two sub-terms *)
| Add (t1, t2) | Add (t1, t2)
| Mult (t1, t2) | Mult (t1, t2)
| Div (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 let t' = if phys_equal l l' then t else Linear l' in
(acc, t') (acc, t')
| Const _ | Const _
| Procname _
| FunctionApplication _
| Add _ | Add _
| Minus _ | Minus _
| LessThan _ | LessThan _
@ -540,7 +594,7 @@ module Term = struct
in in
let or_undef q_opt = Option.value ~default:Q.undef q_opt in let or_undef q_opt = Option.value ~default:Q.undef q_opt in
match t0 with match t0 with
| Const _ | Var _ | IsInstanceOf _ -> | Const _ | Var _ | IsInstanceOf _ | Procname _ | FunctionApplication _ ->
t0 t0
| Linear l -> | Linear l ->
LinArith.get_as_const l |> Option.value_map ~default:t0 ~f:(fun c -> Const c) 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 -> | Div (t, Const c) when Q.is_not_zero c ->
let+ l = aux_linearize t in let+ l = aux_linearize t in
LinArith.mult (Q.inv c) l LinArith.mult (Q.inv c) l
| Procname _
| FunctionApplication _
| Mult _ | Mult _
| Div _ | Div _
| Mod _ | Mod _

@ -25,7 +25,14 @@ val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
[@@warning "-32"] [@@warning "-32"]
(** only used for unit tests *) (** 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} *) (** {3 Build formulas} *)

@ -93,7 +93,7 @@ module Misc = struct
don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we
suspect are passed by reference. *) suspect are passed by reference. *)
let unknown_call skip_reason args : model = 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 = let actuals =
List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} ->
(actual, typ) ) (actual, typ) )
@ -102,9 +102,11 @@ module Misc = struct
AnalysisCallbacks.proc_resolve_attributes callee_procname AnalysisCallbacks.proc_resolve_attributes callee_procname
|> Option.map ~f:Pvar.get_pvar_formals |> Option.map ~f:Pvar.get_pvar_formals
in in
PulseCallOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt let<+> astate =
astate PulseCallOperations.unknown_call tenv path location (Model skip_reason) ~ret ~actuals
|> ok_continue ~formals_opt astate
in
astate
(** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a

@ -107,6 +107,12 @@ let and_eq_vars v1 v2 phi =
({is_unsat; bo_itvs; citvs; formula}, new_eqs) ({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 = let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi =
if phi.is_unsat then Unsat if phi.is_unsat then Unsat
else else
@ -251,15 +257,9 @@ let and_callee subst phi ~callee:phi_callee =
type operand = Formula.operand = type operand = Formula.operand =
| LiteralOperand of IntLit.t | LiteralOperand of IntLit.t
| AbstractValueOperand of AbstractValue.t | AbstractValueOperand of AbstractValue.t
| FunctionApplicationOperand of {f: Formula.function_symbol; actuals: AbstractValue.t list}
[@@deriving compare] [@@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 eval_citv_binop binop_addr bop op_lhs op_rhs citvs =
let citv_of_op op citvs = let citv_of_op op citvs =
match op with match op with
@ -267,6 +267,8 @@ let eval_citv_binop binop_addr bop op_lhs op_rhs citvs =
Some (CItv.equal_to i) Some (CItv.equal_to i)
| AbstractValueOperand v -> | AbstractValueOperand v ->
CItvs.find_opt v citvs CItvs.find_opt v citvs
| FunctionApplicationOperand _ ->
None
in in
match match
Option.both (citv_of_op op_lhs citvs) (citv_of_op op_rhs citvs) 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 = let bo_itv_of_op op bo_itvs =
match op with match op with
| LiteralOperand i -> | LiteralOperand i ->
Itv.ItvPure.of_int_lit i Some (Itv.ItvPure.of_int_lit i)
| AbstractValueOperand v -> | AbstractValueOperand v ->
BoItvs.find_or_default v bo_itvs Some (BoItvs.find_or_default v bo_itvs)
in | FunctionApplicationOperand _ ->
let bo_itv = None
Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs bo_itvs) (bo_itv_of_op op_rhs bo_itvs)
in 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 = 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 let eval_operand phi = function
| LiteralOperand i -> | 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 -> | 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 = 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 in
{phi with citvs} {phi with citvs}
in 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 = let+ phi =
Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' -> match Option.both bo_itv_lhs bo_itv_rhs with
prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) | 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 in
match Formula.prune_binop ~negated bop lhs_op rhs_op formula with match Formula.prune_binop ~negated bop lhs_op rhs_op formula with
| Unsat -> | Unsat ->

@ -53,10 +53,13 @@ val and_callee :
(** {2 Operations} *) (** {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] [@@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 val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t * new_eqs

@ -171,16 +171,20 @@ end = struct
let pp_predicate f (op, l, r) = 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 pp = Pp.seq ~sep:"" pp_predicate
let eliminate_exists ~keep constr = let eliminate_exists ~keep constr =
(* TODO(rgrigore): replace the current weak approximation *) (* TODO(rgrigore): replace the current weak approximation *)
let is_live_operand = let is_live_operand : PulseFormula.operand -> bool = function
PathCondition.( | LiteralOperand _ ->
function LiteralOperand _ -> true | AbstractValueOperand v -> AbstractValue.Set.mem v keep) true
| AbstractValueOperand v ->
AbstractValue.Set.mem v keep
| FunctionApplicationOperand _ ->
true
in in
let is_live_predicate (_op, l, r) = is_live_operand l && is_live_operand r in let is_live_predicate (_op, l, r) = is_live_operand l && is_live_operand r in
List.filter ~f:is_live_predicate constr List.filter ~f:is_live_predicate constr

@ -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, 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, 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, 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_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, 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] 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]

@ -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, 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, 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, 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_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, 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] 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]

@ -140,3 +140,26 @@ void report_correct_error_among_multiple_bad() {
// the trace should complain about the first access inside the callee // the trace should complain about the first access inside the callee
several_dereferences_ok(p, p, p); 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;
}
}

@ -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_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, 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/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_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, 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<int>::operator=`,in call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional<int>::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [in call to `folly::Optional<int>::operator=`,in call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional<int>::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, 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/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_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_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_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] 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]

@ -267,10 +267,12 @@ public class NullPointerExceptions {
param.toString(); param.toString();
} }
native boolean test(); native boolean test1();
native boolean test2();
Object getObj() { Object getObj() {
if (test()) { if (test1()) {
return new Object(); return new Object();
} else { } else {
return null; return null;
@ -278,32 +280,36 @@ public class NullPointerExceptions {
} }
Boolean getBool() { Boolean getBool() {
if (test()) { if (test2()) {
return new Boolean(true); return new Boolean(true);
} else { } else {
return null; return null;
} }
} }
void FP_derefGetterAfterCheckShouldNotCauseNPE() { void derefGetterAfterCheckShouldNotCauseNPE() {
if (getObj() != null) { if (getObj() != null) {
getObj().toString(); getObj().toString();
} }
} }
void FP_derefBoxedGetterAfterCheckShouldNotCauseNPE() { void derefBoxedGetterAfterCheckShouldNotCauseNPE() {
boolean b = getBool() != null && getBool(); boolean b = getBool() != null && getBool();
} }
static void FP_derefNonThisGetterAfterCheckShouldNotCauseNPE() { static void derefNonThisGetterAfterCheckShouldNotCauseNPE() {
NullPointerExceptions c = new NullPointerExceptions(); NullPointerExceptions c = new NullPointerExceptions();
if (c.getObj() != null) { if (c.getObj() != null) {
c.getObj().toString(); c.getObj().toString();
} }
} }
void badCheckShouldCauseNPE() { // latent because we don't know if test1() can return "true"
if (getBool() != null) getObj().toString(); // arguably should be reported?
void badCheckShouldCauseNPE_latent() {
if (getBool() != null) {
getObj().toString();
}
} }
void nullPointerExceptionArrayLength() { void nullPointerExceptionArrayLength() {

@ -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.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/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$$$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_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_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_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, 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.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.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.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.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] 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]

@ -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.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/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$$$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_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, 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.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.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.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.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] 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]

Loading…
Cancel
Save