[pulse][2/2] generate latent issues when null is allocated

Summary:
See updated tests and code comments: this changes many arithmetic
operations to detect when a contradiction "p|->- * p=0" is about to be
detected, and generate a latent issue instead. It's hacky but it does
what we want. Many APIs change because of this so there's some code
churn but the overall end result is not much worse thanks to monadic
operators.

Reviewed By: skcho

Differential Revision: D26918553

fbshipit-source-id: da2abc652
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 8a1213962e
commit 55871dd285

@ -131,8 +131,8 @@ module PulseTransferFunctions = struct
astate
let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc} as analysis_data) ret call_exp
actuals call_loc flags astate =
let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ret
call_exp actuals call_loc flags astate =
(* evaluate all actuals *)
let<*> astate, rev_func_args =
List.fold_result actuals ~init:(astate, [])
@ -204,7 +204,7 @@ module PulseTransferFunctions = struct
| Error _ as err ->
Some err
| Ok exec_state ->
PulseSummary.force_exit_program tenv proc_desc exec_state
PulseSummary.force_exit_program tenv proc_desc err_log exec_state
|> Option.map ~f:(fun exec_state -> Ok exec_state) )
else exec_states_res
@ -429,7 +429,7 @@ let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data
let updated_posts =
PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts
in
let summary = PulseSummary.of_posts tenv proc_desc updated_posts in
let summary = PulseSummary.of_posts tenv proc_desc err_log updated_posts in
report_topl_errors proc_desc err_log summary ;
Some summary )
| None ->

@ -673,12 +673,13 @@ let invalidate_locals pdesc astate : t =
type summary = t [@@deriving compare, equal, yojson_of]
let is_allocated stack_allocations {post; pre} v =
let is_heap_allocated {post; pre} v =
BaseMemory.is_allocated (post :> BaseDomain.t).heap v
|| BaseMemory.is_allocated (pre :> BaseDomain.t).heap v
|| AbstractValue.Set.mem v (Lazy.force stack_allocations)
let is_stack_allocated stack_allocations v = AbstractValue.Set.mem v (Lazy.force stack_allocations)
let subst_var_in_post subst astate =
let open SatUnsat.Import in
let+ post = PostDomain.subst_var subst astate.post in
@ -695,23 +696,55 @@ let get_stack_allocated {post} =
let incorporate_new_eqs astate new_eqs =
let stack_allocations = lazy (get_stack_allocated astate) in
List.fold_until new_eqs ~init:astate
~finish:(fun astate -> Sat astate)
~f:(fun astate (new_eq : PulseFormula.new_eq) ->
List.fold_until new_eqs ~init:(astate, None)
~finish:(fun astate_error -> Sat astate_error)
~f:(fun (astate, error) (new_eq : PulseFormula.new_eq) ->
match new_eq with
| Equal (v1, v2) when AbstractValue.equal v1 v2 ->
Continue astate
Continue (astate, error)
| Equal (v1, v2) -> (
match subst_var_in_post (v1, v2) astate with
| Unsat ->
Stop Unsat
| Sat astate' ->
Continue astate' )
| EqZero v when is_allocated stack_allocations astate v ->
Continue (astate', error) )
| EqZero v when is_stack_allocated stack_allocations v ->
L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ;
Stop Unsat
| EqZero v when is_heap_allocated astate v -> (
(* We want to detect when we know [v|->-] and [v=0] together. This is a contradiction, but
can also be the sign that there is a real issue. Consider:
foo(p) {
if(p) {}
*p = 42;
}
This creates two paths:
p=0 /\ p|->-
p0 /\ p|->-
We could discard the first one straight away because it's equivalent to false, but
the second one will also get discarded when calling this foo(0) because it will fail
the p0 condition, creating FNs. Thus, we create a latent issue instead to report
on foo(0) calls.
An alternative design that would be less hacky would be to detect this situation when
adding pointers from null values, but we'd need to know what values are null at all
times. This would require normalizing the arithmetic part at each step, which is too
expensive. *)
L.d_printfln "Potential ERROR: %a = 0 but is allocated" AbstractValue.pp v ;
match BaseAddressAttributes.get_must_be_valid v (astate.pre :> base_domain).attrs with
| None ->
(* we don't know why [v|->-] is in the state, weird and probably cannot happen; drop
the path because we won't be able to give a sensible error *)
L.d_printfln "Not clear why %a should be allocated in the first place, giving up"
AbstractValue.pp v ;
Stop Unsat
| Some must_be_valid ->
Stop (Sat (astate, Some (v, must_be_valid))) )
| EqZero _ (* [v] not allocated *) ->
Continue astate )
Continue (astate, error) )
(** it's a good idea to normalize the path condition before calling this function *)
@ -766,10 +799,16 @@ let summary_of_post tenv pdesc astate =
in
let* () = if is_unsat then Unsat else Sat () in
let astate = {astate with path_condition} in
let* astate = incorporate_new_eqs astate new_eqs in
let* astate, error = incorporate_new_eqs astate new_eqs in
let* astate, new_eqs = filter_for_summary tenv astate in
let+ astate = incorporate_new_eqs astate new_eqs in
invalidate_locals pdesc astate
let+ astate, error =
match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error)
in
match error with
| None ->
Ok (invalidate_locals pdesc astate)
| Some (address, must_be_valid) ->
Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))
let get_pre {pre} = (pre :> BaseDomain.t)
@ -778,13 +817,15 @@ let get_post {post} = (post :> BaseDomain.t)
(* re-exported for mli *)
let incorporate_new_eqs new_eqs astate =
if PathCondition.is_unsat_cheap astate.path_condition then astate
if PathCondition.is_unsat_cheap astate.path_condition then Ok astate
else
match incorporate_new_eqs astate new_eqs with
| Unsat ->
{astate with path_condition= PathCondition.false_}
| Sat astate ->
astate
Ok {astate with path_condition= PathCondition.false_}
| Sat (astate, None) ->
Ok astate
| Sat (astate, Some (address, must_be_valid)) ->
Error (`PotentialInvalidAccess (astate, address, must_be_valid))
module Topl = struct

@ -186,7 +186,12 @@ type summary = private t [@@deriving compare, equal, yojson_of]
val skipped_calls_match_pattern : summary -> bool
val summary_of_post : Tenv.t -> Procdesc.t -> t -> summary SatUnsat.t
val summary_of_post :
Tenv.t
-> Procdesc.t
-> t
-> (summary, [> `PotentialInvalidAccessSummary of summary * AbstractValue.t * Trace.t]) result
SatUnsat.t
(** trim the state down to just the procedure's interface (formals and globals), and simplify and
normalize the state *)
@ -196,7 +201,10 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t
(** directly set the edges and attributes for the given address, bypassing abduction altogether *)
val incorporate_new_eqs : PathCondition.new_eqs -> t -> t
val incorporate_new_eqs :
PathCondition.new_eqs
-> t
-> (t, [> `PotentialInvalidAccess of t * AbstractValue.t * Trace.t]) result
(** Check that the new equalities discovered are compatible with the current pre and post heaps,
e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
and [y] being allocated separately. In those cases, the resulting path condition is

@ -10,9 +10,39 @@ open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain
type 'astate error =
| PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
| PotentialInvalidAccessSummary of
{astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result
type 'a t = ('a, AbductiveDomain.t) base_t
type 'astate abductive_error =
[ `ISLError of 'astate
| `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t
| `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ]
let of_abductive_error = function
| `ISLError astate ->
ISLError astate
| `PotentialInvalidAccess (astate, address, must_be_valid) ->
PotentialInvalidAccess {astate; address; must_be_valid}
| `PotentialInvalidAccessSummary (astate, address, must_be_valid) ->
PotentialInvalidAccessSummary {astate; address; must_be_valid}
let of_abductive_result abductive_result = Result.map_error abductive_result ~f:of_abductive_error
let of_abductive_access_result access_trace abductive_result =
Result.map_error abductive_result ~f:(function
| `InvalidAccess (invalidation, invalidation_trace, astate) ->
ReportableError
{ astate
; diagnostic=
AccessToInvalidAddress
{calling_context= []; invalidation; invalidation_trace; access_trace} }
| (`ISLError _ | `PotentialInvalidAccess _ | `PotentialInvalidAccessSummary _) as error ->
of_abductive_error error )

@ -0,0 +1,37 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain
type 'astate error =
| PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
| PotentialInvalidAccessSummary of
{astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result
type 'a t = ('a, AbductiveDomain.t) base_t
(** Intermediate datatype since {!AbductiveDomain} cannot refer to this module without creating a
circular dependency. *)
type 'astate abductive_error =
[ `ISLError of 'astate
| `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t
| `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ]
val of_abductive_error : 'astate abductive_error -> 'astate error
val of_abductive_result : ('a, 'astate abductive_error) result -> ('a, 'astate) base_t
val of_abductive_access_result :
Trace.t
-> ('a, [`InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result
-> ('a, 'astate) base_t

@ -8,10 +8,13 @@
open! IStd
open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain
module AccessResult = PulseAccessResult
let map_path_condition ~f astate =
let phi, new_eqs = f astate.AbductiveDomain.path_condition in
AbductiveDomain.set_path_condition phi astate |> AbductiveDomain.incorporate_new_eqs new_eqs
AbductiveDomain.set_path_condition phi astate
|> AbductiveDomain.incorporate_new_eqs new_eqs
|> AccessResult.of_abductive_result
let and_nonnegative v astate =

@ -8,32 +8,48 @@
open! IStd
open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain
module AccessResult = PulseAccessResult
(** Wrapper around {!PathCondition} that operates on {!AbductiveDomain.t}. *)
val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
val and_eq_int : AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t
val and_eq_int :
AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
type operand = PathCondition.operand =
| LiteralOperand of IntLit.t
| AbstractValueOperand of AbstractValue.t
val eval_binop :
AbstractValue.t -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t
AbstractValue.t
-> Binop.t
-> operand
-> operand
-> AbductiveDomain.t
-> AbductiveDomain.t AccessResult.t
val eval_unop :
AbstractValue.t -> Unop.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
AbstractValue.t
-> Unop.t
-> AbstractValue.t
-> AbductiveDomain.t
-> AbductiveDomain.t AccessResult.t
val prune_binop :
negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t
negated:bool
-> Binop.t
-> operand
-> operand
-> AbductiveDomain.t
-> AbductiveDomain.t AccessResult.t
val prune_eq_zero : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
val prune_eq_zero : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
(** helper function wrapping [prune_binop] *)
val prune_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
val prune_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
(** helper function wrapping [prune_binop] *)
val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
@ -43,4 +59,8 @@ val is_unsat_cheap : AbductiveDomain.t -> bool
val has_no_assumptions : AbductiveDomain.t -> bool
val and_equal_instanceof :
AbstractValue.t -> AbstractValue.t -> Typ.t -> AbductiveDomain.t -> AbductiveDomain.t
AbstractValue.t
-> AbstractValue.t
-> Typ.t
-> AbductiveDomain.t
-> AbductiveDomain.t AccessResult.t

@ -262,6 +262,7 @@ let add_call_to_attributes proc_name call_location caller_history attrs =
let conjoin_callee_arith pre_post call_state =
let open IResult.Let_syntax in
L.d_printfln "applying callee path condition: (%a)[%a]" PathCondition.pp
pre_post.AbductiveDomain.path_condition
(AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr))
@ -270,13 +271,19 @@ let conjoin_callee_arith pre_post call_state =
PathCondition.and_callee call_state.subst call_state.astate.path_condition
~callee:pre_post.AbductiveDomain.path_condition
in
if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
else
let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in
let astate = AbductiveDomain.incorporate_new_eqs new_eqs astate in
if PathCondition.is_unsat_cheap astate.path_condition then raise (Contradiction PathCondition)
let+ astate =
AbductiveDomain.incorporate_new_eqs new_eqs astate |> AccessResult.of_abductive_result
in
if PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition then
raise (Contradiction PathCondition)
else {call_state with astate; subst}
let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =
let open IResult.Let_syntax in
let one_address_sat callee_attrs (addr_caller, caller_history) call_state =
let attrs_caller =
add_call_to_attributes callee_proc_name call_location caller_history callee_attrs
@ -284,7 +291,7 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st
let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in
if phys_equal astate call_state.astate then call_state else {call_state with astate}
in
let call_state = conjoin_callee_arith pre_post call_state in
let+ call_state = conjoin_callee_arith pre_post call_state in
(* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *)
if Config.pulse_isl then
AddressMap.fold
@ -337,7 +344,7 @@ let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_
>>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post
~captured_vars_with_actuals
>>= materialize_pre_for_globals callee_proc_name call_location pre_post
>>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in
>>= (* ...then relational arithmetic constraints in the callee's attributes will make sense in
terms of the caller's values *)
apply_arithmetic_constraints callee_proc_name call_location pre_post
in
@ -576,18 +583,22 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state =
let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals
call_state =
let open IResult.Let_syntax in
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
let r =
let call_state, return_caller =
apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state
|> apply_post_for_captured_vars callee_proc_name call_location pre_post
~captured_vars_with_actuals
|> apply_post_for_globals callee_proc_name call_location pre_post
|> record_post_for_return callee_proc_name call_location pre_post
|> fun (call_state, return_caller) ->
in
let+ call_state =
record_post_remaining_attributes callee_proc_name call_location pre_post call_state
|> record_skipped_calls callee_proc_name call_location pre_post
|> conjoin_callee_arith pre_post
|> fun call_state -> (call_state, return_caller)
in
(call_state, return_caller)
in
PerfEvent.(log (fun logger -> log_end_event logger ())) ;
r
@ -728,7 +739,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p
let pre_astate = astate in
let call_state = {call_state with astate; visited= AddressSet.empty} in
(* apply the postcondition *)
let call_state, return_caller =
let* call_state, return_caller =
apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
~actuals call_state
in

@ -50,19 +50,24 @@ module Misc = struct
let early_exit : model =
fun {tenv; proc_desc} ~callee_procname:_ _ ~ret:_ astate ->
match AbductiveDomain.summary_of_post tenv proc_desc astate with
let open SatUnsat.Import in
match
AbductiveDomain.summary_of_post tenv proc_desc astate >>| AccessResult.of_abductive_result
with
| Unsat ->
[]
| Sat astate ->
| Sat (Ok astate) ->
[Ok (ExitProgram astate)]
| Sat (Error _ as error) ->
[error]
let return_int : Int64.t -> model =
fun i64 _ ~callee_procname:_ _location ~ret:(ret_id, _) astate ->
let i = IntLit.of_int64 i64 in
let ret_addr = AbstractValue.Constants.get_int i in
let astate = PulseArithmetic.and_eq_int ret_addr i astate in
PulseOperations.write_id ret_id (ret_addr, []) astate |> ok_continue
let<+> astate = PulseArithmetic.and_eq_int ret_addr i astate in
PulseOperations.write_id ret_id (ret_addr, []) astate
let return_positive ~desc : model =
@ -70,16 +75,15 @@ module Misc = struct
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let ret_addr = AbstractValue.mk_fresh () in
let ret_value = (ret_addr, [event]) in
let<+> astate = PulseArithmetic.and_positive ret_addr astate in
PulseOperations.write_id ret_id ret_value astate
|> PulseArithmetic.and_positive ret_addr
|> ok_continue
let return_unknown_size : model =
fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate ->
let ret_addr = AbstractValue.mk_fresh () in
let astate = PulseArithmetic.and_nonnegative ret_addr astate in
PulseOperations.write_id ret_id (ret_addr, []) astate |> ok_continue
let<+> astate = PulseArithmetic.and_nonnegative ret_addr astate in
PulseOperations.write_id ret_id (ret_addr, []) astate
(** Pretend the function call is a call to an "unknown" function, i.e. a function for which we
@ -121,7 +125,7 @@ module Misc = struct
match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
in
let astates_alloc =
let astate = PulseArithmetic.and_positive (fst deleted_access) astate in
let<*> astate = PulseArithmetic.and_positive (fst deleted_access) astate in
if Config.pulse_isl then
PulseOperations.invalidate_biad_isl location invalidation deleted_access astate
|> List.map ~f:(fun result ->
@ -131,7 +135,7 @@ module Misc = struct
let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in
astate
in
let astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in
let<*> astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in
Ok (ContinueProgram astate_zero) :: astates_alloc
@ -149,9 +153,8 @@ module Misc = struct
This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *)
astate
in
let<+> astate = PulseArithmetic.and_positive ret_addr astate in
PulseOperations.write_id ret_id ret_value astate
|> PulseArithmetic.and_positive ret_addr
|> ok_continue
let alloc_not_null_call_ev ~desc arg =
@ -177,15 +180,15 @@ module C = struct
(ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
in
let astate = PulseOperations.write_id ret_id ret_value astate in
let astate_alloc =
PulseArithmetic.and_positive ret_addr astate
|> PulseOperations.allocate callee_procname location ret_value
let<*> astate_alloc =
PulseOperations.allocate callee_procname location ret_value astate
|> set_uninitialized tenv size_exp_opt location ret_addr
|> PulseArithmetic.and_positive ret_addr
in
let result_null =
let+ astate_null =
PulseArithmetic.and_eq_int ret_addr IntLit.zero astate
|> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value
>>= PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value
in
ContinueProgram astate_null
in
@ -199,12 +202,12 @@ module C = struct
(ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
in
let astate = PulseOperations.write_id ret_id ret_value astate in
let astate =
let<+> astate =
PulseOperations.allocate callee_procname location ret_value astate
|> PulseArithmetic.and_positive ret_addr
|> set_uninitialized tenv size_exp_opt location ret_addr
|> PulseArithmetic.and_positive ret_addr
in
ok_continue astate
astate
let malloc size_exp = malloc_common ~size_exp_opt:(Some size_exp)
@ -277,7 +280,7 @@ module Optional = struct
let assign_none this ~desc : model =
fun _ ~callee_procname:_ location ~ret:_ astate ->
let<*> astate, value = assign_value_fresh location this ~desc astate in
let astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in
let<*> astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in
let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in
astate
@ -285,8 +288,9 @@ module Optional = struct
let assign_value this _value ~desc : model =
fun _ ~callee_procname:_ location ~ret:_ astate ->
(* TODO: call the copy constructor of a value *)
let<+> astate, value = assign_value_fresh location this ~desc astate in
PulseArithmetic.and_positive (fst value) astate
let<*> astate, value = assign_value_fresh location this ~desc astate in
let<+> astate = PulseArithmetic.and_positive (fst value) astate in
astate
let assign_optional_value this init ~desc : model =
@ -319,10 +323,10 @@ module Optional = struct
let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in
let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in
let astate = PulseOperations.write_id ret_id ret_value astate in
let astate_non_empty = PulseArithmetic.prune_positive value_addr astate in
let astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in
let astate_empty = PulseArithmetic.prune_eq_zero value_addr astate in
let astate_false = PulseArithmetic.prune_eq_zero ret_addr astate_empty in
let<*> astate_non_empty = PulseArithmetic.prune_positive value_addr astate in
let<*> astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in
let<*> astate_empty = PulseArithmetic.prune_eq_zero value_addr astate in
let<*> astate_false = PulseArithmetic.prune_eq_zero ret_addr astate_empty in
[Ok (ContinueProgram astate_false); Ok (ContinueProgram astate_true)]
@ -331,7 +335,7 @@ module Optional = struct
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let<*> astate, value_addr = to_internal_value_deref Read location optional astate in
let value_update_hist = (fst value_addr, event :: snd value_addr) in
let astate_value_addr =
let<*> astate_value_addr =
PulseOperations.write_id ret_id value_update_hist astate
|> PulseArithmetic.prune_positive (fst value_addr)
in
@ -339,8 +343,8 @@ module Optional = struct
let<*> astate_null =
PulseOperations.write_id ret_id nullptr astate
|> PulseArithmetic.prune_eq_zero (fst value_addr)
|> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero
|> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr
>>= PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero
>>= PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr
in
[Ok (ContinueProgram astate_value_addr); Ok (ContinueProgram astate_null)]
@ -349,7 +353,7 @@ module Optional = struct
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let<*> astate, value_addr = to_internal_value_deref Read location optional astate in
let astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in
let<*> astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in
let<*> astate_non_empty, value =
PulseOperations.eval_access Read location value_addr Dereference astate_non_empty
in
@ -359,7 +363,7 @@ module Optional = struct
PulseOperations.eval_access Read location default Dereference astate
in
let default_value_hist = (default_val, event :: default_hist) in
let astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in
let<*> astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in
let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in
[Ok (ContinueProgram astate_value); Ok (ContinueProgram astate_default)]
end
@ -409,7 +413,7 @@ module StdAtomicInteger = struct
let arith_bop prepost location event ret_id bop this operand astate =
let* astate, int_addr, (old_int, hist) = load_backing_int location this astate in
let bop_addr = AbstractValue.mk_fresh () in
let astate =
let* astate =
PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate
in
let+ astate =
@ -718,14 +722,14 @@ module GenericArrayBackedCollectionIterator = struct
| `NotEqual ->
(IntLit.zero, IntLit.one)
in
let astate_equal =
let<*> astate_equal =
PulseArithmetic.and_eq_int ret_val ret_val_equal astate
|> PulseArithmetic.prune_binop ~negated:false Eq (AbstractValueOperand index_lhs)
>>= PulseArithmetic.prune_binop ~negated:false Eq (AbstractValueOperand index_lhs)
(AbstractValueOperand index_rhs)
in
let astate_notequal =
let<*> astate_notequal =
PulseArithmetic.and_eq_int ret_val ret_val_notequal astate
|> PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs)
>>= PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs)
(AbstractValueOperand index_rhs)
in
[Ok (ContinueProgram astate_equal); Ok (ContinueProgram astate_notequal)]
@ -858,7 +862,7 @@ module StdVector = struct
let pointer_hist = event :: snd iter in
let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in
let index_zero = AbstractValue.mk_fresh () in
let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
let<*> astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
let<*> astate, ((arr_addr, _) as arr) =
GenericArrayBackedCollection.eval Read location vector astate
in
@ -932,10 +936,11 @@ module Java = struct
let res_addr = AbstractValue.mk_fresh () in
match typeexpr with
| Exp.Sizeof {typ} ->
let<+> astate =
PulseArithmetic.and_equal_instanceof res_addr argv typ astate
|> PulseArithmetic.prune_positive argv
|> PulseOperations.write_id ret_id (res_addr, event :: hist)
|> ok_continue
>>= PulseArithmetic.prune_positive argv
in
PulseOperations.write_id ret_id (res_addr, event :: hist) astate
(* The type expr is sometimes a Var expr but this is not expected.
This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *)
| _ ->
@ -1002,10 +1007,12 @@ module JavaCollection = struct
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model "Collections.isEmpty"; location; in_call= []} in
let fresh_elem = AbstractValue.mk_fresh () in
let<+> astate =
PulseArithmetic.prune_positive address astate
|> PulseArithmetic.and_eq_int fresh_elem IntLit.zero
|> PulseOperations.write_id ret_id (fresh_elem, event :: hist)
|> ok_continue
>>= PulseArithmetic.and_eq_int fresh_elem IntLit.zero
>>| PulseOperations.write_id ret_id (fresh_elem, event :: hist)
in
astate
end
module JavaInteger = struct
@ -1045,11 +1052,11 @@ module JavaInteger = struct
let<*> astate, _int_addr1, (int1, hist) = load_backing_int location this astate in
let<*> astate, _int_addr2, (int2, _) = load_backing_int location arg astate in
let binop_addr = AbstractValue.mk_fresh () in
let astate =
let<+> astate =
PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1)
(AbstractValueOperand int2) astate
in
PulseOperations.write_id ret_id (binop_addr, hist) astate |> ok_continue
PulseOperations.write_id ret_id (binop_addr, hist) astate
let int_val this : model =
@ -1070,13 +1077,14 @@ module JavaPreconditions = struct
let check_not_null (address, hist) : model =
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model "Preconditions.checkNotNull"; location; in_call= []} in
let astate = PulseArithmetic.prune_positive address astate in
PulseOperations.write_id ret_id (address, event :: hist) astate |> ok_continue
let<+> astate = PulseArithmetic.prune_positive address astate in
PulseOperations.write_id ret_id (address, event :: hist) astate
let check_state_argument (address, _) : model =
fun _ ~callee_procname:_ _ ~ret:_ astate ->
PulseArithmetic.prune_positive address astate |> ok_continue
let<+> astate = PulseArithmetic.prune_positive address astate in
astate
end
module Android = struct
@ -1085,12 +1093,12 @@ module Android = struct
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let ret_val = AbstractValue.mk_fresh () in
let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in
let astate_equal_zero =
let<*> astate_equal_zero =
PulseArithmetic.and_eq_int ret_val IntLit.zero astate
|> PulseArithmetic.prune_positive address
>>= PulseArithmetic.prune_positive address
in
let astate_not_zero =
PulseArithmetic.and_eq_int ret_val IntLit.one astate |> PulseArithmetic.prune_eq_zero address
let<*> astate_not_zero =
PulseArithmetic.and_eq_int ret_val IntLit.one astate >>= PulseArithmetic.prune_eq_zero address
in
[Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)]
end

@ -19,7 +19,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate =
let location = Procdesc.get_loc proc_desc in
let self = mk_objc_self_pvar proc_desc in
let* astate, self_value = PulseOperations.eval_deref location (Lvar self) astate in
let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in
let* astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in
let ret_var = Procdesc.get_ret_var proc_desc in
let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in
PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate
@ -52,7 +52,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
match astate with
| ContinueProgram astate ->
let result =
let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in
PulseArithmetic.prune_positive (fst value) astate
in
PulseReport.report_result tenv proc_desc err_log result

@ -28,6 +28,9 @@ module Import = struct
| ISLLatentMemoryError of AbductiveDomain.summary
type 'astate base_error = 'astate AccessResult.error =
| PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
| PotentialInvalidAccessSummary of
{astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate
@ -70,17 +73,8 @@ let check_and_abduce_addr_access_isl access_mode location (address, history) ?(n
astate =
let access_trace = Trace.Immediate {location; history} in
AddressAttributes.check_valid_isl access_trace address ~null_noop astate
|> List.map ~f:(function
| Error (`InvalidAccess (invalidation, invalidation_trace, astate)) ->
Error
(ReportableError
{ diagnostic=
Diagnostic.AccessToInvalidAddress
{calling_context= []; invalidation; invalidation_trace; access_trace}
; astate })
| Error (`ISLError astate) ->
Error (ISLError astate)
| Ok astate -> (
|> List.map ~f:(fun access_result ->
let* astate = AccessResult.of_abductive_access_result access_trace access_result in
match access_mode with
| Read ->
AddressAttributes.check_initialized access_trace address astate
@ -93,7 +87,7 @@ let check_and_abduce_addr_access_isl access_mode location (address, history) ?(n
| Write ->
Ok (AbductiveDomain.initialize address astate)
| NoAccess ->
Ok astate ) )
Ok astate )
module Closures = struct
@ -214,25 +208,28 @@ let eval mode location exp0 astate =
eval mode exp' astate
| Const (Cint i) ->
let v = AbstractValue.Constants.get_int i in
let astate =
let+ astate =
PulseArithmetic.and_eq_int v i astate
|> AddressAttributes.invalidate
>>| AddressAttributes.invalidate
(v, [ValueHistory.Assignment location])
(ConstantDereference i) location
in
Ok (astate, (v, []))
(astate, (v, []))
| UnOp (unop, exp, _typ) ->
let+ astate, (addr, hist) = eval Read exp astate in
let* astate, (addr, hist) = eval Read exp astate in
let unop_addr = AbstractValue.mk_fresh () in
(PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist))
let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in
(astate, (unop_addr, hist))
| BinOp (bop, e_lhs, e_rhs) ->
let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in
(* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
let+ astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in
let* astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in
let binop_addr = AbstractValue.mk_fresh () in
( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
let+ astate =
PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
(AbstractValueOperand addr_rhs) astate
, (binop_addr, hist_lhs) )
in
(astate, (binop_addr, hist_lhs))
| Const _ | Sizeof _ | Exn _ ->
Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
in
@ -253,7 +250,7 @@ let prune location ~condition astate =
match (exp : Exp.t) with
| BinOp (bop, exp_lhs, exp_rhs) ->
let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in
let+ astate, rhs_op = eval_to_operand Read location exp_rhs astate in
let* astate, rhs_op = eval_to_operand Read location exp_rhs astate in
PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate
| UnOp (LNot, exp', _) ->
prune_aux ~negated:(not negated) exp' astate
@ -651,9 +648,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
map_call_result ~is_isl_error_prepost:false
(astate :> AbductiveDomain.t)
~f:(fun subst astate ->
let* (astate_summary : AbductiveDomain.summary) =
let* astate_summary_result =
AbductiveDomain.summary_of_post tenv caller_proc_desc astate
>>| AccessResult.of_abductive_result
in
match astate_summary_result with
| Error _ as error ->
Sat error
| Ok (astate_summary : AbductiveDomain.summary) -> (
match callee_exec_state with
| ContinueProgram _ | ISLLatentMemoryError _ ->
assert false
@ -673,13 +675,17 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
Sat
(Error
(ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}))
)
| `ISLDelay astate ->
Sat (Error (ISLError (astate :> AbductiveDomain.t))) )
| LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> (
match AbstractValue.Map.find_opt address_callee subst with
| None ->
(* the address became unreachable so the bug can never be reached; drop it *) Unsat
(* the address became unreachable so the bug can never be reached; drop it *)
Unsat
| Some (address, _history) -> (
let calling_context = (CallEvent.Call callee_pname, call_loc) :: calling_context in
let calling_context =
(CallEvent.Call callee_pname, call_loc) :: calling_context
in
match
AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t)
|> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs)
@ -700,13 +706,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
; invalidation
; invalidation_trace
; access_trace= must_be_valid }
; astate= (astate_summary :> AbductiveDomain.t) })) ) ) )
; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) )
| ISLLatentMemoryError astate ->
map_call_result ~is_isl_error_prepost:true
(astate :> AbductiveDomain.t)
~f:(fun _subst astate ->
let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
Ok (ISLLatentMemoryError astate_summary) )
AbductiveDomain.summary_of_post tenv caller_proc_desc astate
>>| AccessResult.of_abductive_result
>>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) )
let get_captured_actuals location ~captured_vars ~actual_closure astate =

@ -35,6 +35,9 @@ module Import : sig
| ISLLatentMemoryError of AbductiveDomain.summary
type 'astate base_error = 'astate AccessResult.error =
| PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
| PotentialInvalidAccessSummary of
{astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ISLError of 'astate

@ -16,10 +16,9 @@ let report ?(extra_trace = []) proc_desc err_log diagnostic =
Pulse (get_issue_type diagnostic) (get_message diagnostic)
let report_latent_issue proc_desc err_log latent_issue =
let report_latent_diagnostic proc_desc err_log diagnostic =
(* HACK: report latent issues with a prominent message to distinguish them from
non-latent. Useful for infer's own tests. *)
let diagnostic = LatentIssue.to_diagnostic latent_issue in
let extra_trace =
let depth = 0 in
let tags = [] in
@ -29,6 +28,10 @@ let report_latent_issue proc_desc err_log latent_issue =
report ~extra_trace proc_desc err_log diagnostic
let report_latent_issue proc_desc err_log latent_issue =
LatentIssue.to_diagnostic latent_issue |> report_latent_diagnostic proc_desc err_log
let is_nullsafe_error tenv diagnostic jn =
(not Config.pulse_nullsafe_report_npe)
&& IssueType.equal (Diagnostic.get_issue_type diagnostic) IssueType.nullptr_dereference
@ -46,8 +49,12 @@ let is_suppressed tenv proc_desc diagnostic astate =
let summary_of_error_post tenv proc_desc mk_error astate =
match AbductiveDomain.summary_of_post tenv proc_desc astate with
| Sat astate ->
| Sat (Ok astate) ->
Sat (mk_error astate)
| Sat (Error error) ->
(* ignore the error we wanted to report (with [mk_error]): the abstract state contained a
potential error already so report [error] instead *)
Sat (AccessResult.of_abductive_error error)
| Unsat ->
Unsat
@ -55,17 +62,33 @@ let summary_of_error_post tenv proc_desc mk_error astate =
let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) :
AbductiveDomain.summary AccessResult.error SatUnsat.t =
match error with
| PotentialInvalidAccessSummary {astate; address; must_be_valid} ->
Sat (PotentialInvalidAccessSummary {astate; address; must_be_valid})
| PotentialInvalidAccess {astate; address; must_be_valid} ->
summary_of_error_post tenv proc_desc
(fun astate -> PotentialInvalidAccess {astate; address; must_be_valid})
astate
| ReportableError {astate; diagnostic} ->
summary_of_error_post tenv proc_desc
(fun astate -> AccessResult.ReportableError {astate; diagnostic})
(fun astate -> ReportableError {astate; diagnostic})
astate
| ISLError astate ->
summary_of_error_post tenv proc_desc (fun astate -> AccessResult.ISLError astate) astate
summary_of_error_post tenv proc_desc (fun astate -> ISLError astate) astate
let report_summary_error tenv proc_desc err_log
(access_error : AbductiveDomain.summary AccessResult.error) : _ ExecutionDomain.base_t =
match access_error with
| PotentialInvalidAccess {astate; address; must_be_valid}
| PotentialInvalidAccessSummary {astate; address; must_be_valid} ->
if Config.pulse_report_latent_issues then
report_latent_diagnostic proc_desc err_log
(AccessToInvalidAddress
{ calling_context= []
; invalidation= ConstantDereference IntLit.zero
; invalidation_trace= Immediate {location= Procdesc.get_loc proc_desc; history= []}
; access_trace= must_be_valid }) ;
LatentInvalidAccess {astate; address; must_be_valid; calling_context= []}
| ISLError astate ->
ISLLatentMemoryError astate
| ReportableError {astate; diagnostic} -> (

@ -11,6 +11,13 @@ open PulseDomainInterface
val report_result :
Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list
val report_summary_error :
Tenv.t
-> Procdesc.t
-> Errlog.t
-> AbductiveDomain.summary AccessResult.error
-> _ ExecutionDomain.base_t
val report_results :
Tenv.t
-> Procdesc.t

@ -21,15 +21,33 @@ let pp fmt summary =
F.close_box ()
let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : ExecutionDomain.t) :
_ ExecutionDomain.base_t option =
let exec_summary_of_post_common tenv ~continue_program proc_desc err_log
(exec_astate : ExecutionDomain.t) : _ ExecutionDomain.base_t option =
match exec_astate with
| ContinueProgram astate -> (
match AbductiveDomain.summary_of_post tenv proc_desc astate with
| Unsat ->
None
| Sat astate ->
Some (continue_program astate) )
| Sat (Ok astate) ->
Some (continue_program astate)
| Sat (Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))) -> (
match
AbductiveDomain.find_post_cell_opt address (astate :> AbductiveDomain.t)
|> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs)
with
| None ->
Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context= []})
| Some (invalidation, invalidation_trace) ->
PulseReport.report_summary_error tenv proc_desc err_log
(ReportableError
{ diagnostic=
AccessToInvalidAddress
{ calling_context= []
; invalidation
; invalidation_trace
; access_trace= must_be_valid }
; astate })
|> Option.some ) )
(* already a summary but need to reconstruct the variants to make the type system happy :( *)
| AbortProgram astate ->
Some (AbortProgram astate)
@ -43,13 +61,13 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate :
Some (ISLLatentMemoryError astate)
let force_exit_program tenv proc_desc post =
exec_summary_of_post_common tenv proc_desc post ~continue_program:(fun astate ->
let force_exit_program tenv proc_desc err_log post =
exec_summary_of_post_common tenv proc_desc err_log post ~continue_program:(fun astate ->
ExitProgram astate )
let of_posts tenv proc_desc posts =
let of_posts tenv proc_desc err_log posts =
List.filter_mapi posts ~f:(fun i exec_state ->
L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ;
exec_summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate ->
exec_summary_of_post_common tenv proc_desc err_log exec_state ~continue_program:(fun astate ->
ContinueProgram astate ) )

@ -10,9 +10,9 @@ open PulseDomainInterface
type t = ExecutionDomain.summary list [@@deriving yojson_of]
val of_posts : Tenv.t -> Procdesc.t -> ExecutionDomain.t list -> t
val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t list -> t
val force_exit_program :
Tenv.t -> Procdesc.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option
Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option
val pp : Format.formatter -> t -> unit

@ -69,10 +69,11 @@ void stack_addresses_are_distinct_ok() {
}
}
void null_test_after_deref_ok(int* x) {
*x = 42;
// latent because of the condition "x==0" in the pre-condition
void null_test_after_deref_latent(int* x) {
*x = 42; // latent error given that x is tested for null below
if (x == nullptr) {
int* p = nullptr;
*p = 42;
*p = 42; // should be ignored as we can never get there
}
}

@ -43,6 +43,9 @@ struct X {
f = x.f + 10;
copy_from(x);
}
// should realise [this] cannot be null to avoid FP latent (that can never be
// manifested)
~X() {
std::cerr << "~X(" << f << ") " << name();
if (original_counter) {

@ -23,7 +23,9 @@ class UsingDelayedDestruction : folly::DelayedDestruction {
delete this;
}
void double_delete_ok() {
// should realise [this] cannot be null to avoid FP latent (that can never be
// manifested)
void FP_latent_double_delete_ok() {
destroy(); // should not delete this double delete
delete this;
}

@ -55,7 +55,9 @@ void delete_inner_then_write_bad(struct X& x) {
wraps_read(x);
}
void read_write_then_delete_good(struct X& x) {
// latent because delete(&x) creates a path where &x==0 but it was dereferences
// before, but that does not make sense as &x cannot be null
void FP_latent_read_write_then_delete_ok(struct X& x) {
wraps_write(x, 10);
wraps_read(x);
wraps_delete(&x);

@ -1,5 +1,6 @@
codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
codetoanalyze/cpp/pulse/aliasing.cpp, null_test_after_deref_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 null_test_after_deref_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
@ -24,6 +25,7 @@ codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DE
codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `update_inside_lambda_as_argument`,return from call to `update_inside_lambda_as_argument`,invalid access occurs here]
codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::FP_track_copy_operations_complex_ok, 16, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::FP_track_copy_operations_one_copy_ok, 17, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::X::__infer_inner_destructor_~X, 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 `this` of condtemp::X::__infer_inner_destructor_~X,when calling `condtemp::X::name` here,parameter `this` of condtemp::X::name,invalid access occurs here]
codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_latent, 5, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test5_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,invalid access occurs here]
@ -31,6 +33,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_delete_function<int>` here,parameter `a` of deduplication::templated_delete_function<int>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_access_function<int>` here,parameter `a` of deduplication::templated_access_function<int>,invalid access occurs here]
codetoanalyze/cpp/pulse/exit_test.cpp, store_exit_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `store_exit` here,parameter `x` of store_exit,invalid access occurs here]
codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::FP_latent_double_delete_ok, 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 `this` of UsingDelayedDestruction::FP_latent_double_delete_ok,invalid access occurs here]
codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::FP_init_single_field_struct_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor2_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
@ -39,6 +42,7 @@ codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_set_field_via_local_bad, 5,
codetoanalyze/cpp/pulse/frontend.cpp, frontend::conditional_expression_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `frontend::some::thing::bad_ptr` here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `frontend::some::thing::bad_ptr`,return from call to `frontend::some::thing::bad_ptr`,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::not_boolean_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, FP_latent_read_write_then_delete_ok, 2, 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 FP_latent_read_write_then_delete_ok,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
@ -51,11 +55,13 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4,
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference2_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `test_after_dereference2_latent` here,parameter `x` of test_after_dereference2_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `FN_test_after_dereference_latent` here,parameter `x` of FN_test_after_dereference_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,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, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, cannot_be_empty_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getOptionalValue` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `getOptionalValue`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `getOptionalValue`,invalid access occurs here]

@ -206,12 +206,12 @@ void call_test_after_dereference_bad() {
FN_test_after_dereference_latent(NULL);
}
void FN_test_after_dereference2_latent(int* x) {
void test_after_dereference2_latent(int* x) {
*x = 42;
if (x == 0)
;
}
void FN_call_test_after_dereference2_bad() {
FN_test_after_dereference2_latent(NULL);
void call_test_after_dereference2_bad() {
test_after_dereference2_latent(NULL);
}

Loading…
Cancel
Save