[pulse] report errors only when the PRUNE nodes along the path are true

Summary:
Take another page from the Incorrectness Logic book and refrain from reporting issues on paths unless we know for sure that this path will be taken.

Previously, we would report on paths that are merely *not impossible*. This goes very far in the other direction, so it's possible we'll want to go back to some sort of middle ground. Or maybe not. See the changes in the tests to get a sense of what we're missing.

Reviewed By: ezgicicek

Differential Revision: D24014719

fbshipit-source-id: d451faf02
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 980f110156
commit 7fdb33b710

@ -1731,6 +1731,12 @@ INTERNAL OPTIONS
Maximum number of array elements and structure fields to keep Maximum number of array elements and structure fields to keep
track of for a given array address. track of for a given array address.
--pulse-report-latent-issues
Activates: Only use for testing, there should be no need to turn
this on for regular code analysis. Report latent issues instead of
waiting for them to become concrete. (Conversely:
--no-pulse-report-latent-issues)
--pulse-widen-threshold int --pulse-widen-threshold int
Under-approximate after int loop iterations Under-approximate after int loop iterations

@ -157,3 +157,5 @@ let min i1 i2 = if leq i1 i2 then i1 else i2
let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i
let to_string i = F.asprintf "%a" pp i let to_string i = F.asprintf "%a" pp i
let equal i1 i2 = eq i1 i2

@ -27,6 +27,9 @@ val div : t -> t -> t
val eq : t -> t -> bool val eq : t -> t -> bool
val equal : t -> t -> bool
(** an alias for {!eq}, for convenience *)
val of_int : int -> t val of_int : int -> t
val of_big_int : Z.t -> t [@@warning "-32"] val of_big_int : Z.t -> t [@@warning "-32"]

@ -332,6 +332,6 @@ module Set = PrettyPrintable.MakePPSet (struct
let pp = pp Pp.text let pp = pp Pp.text
end) end)
type capture_mode = ByReference | ByValue [@@deriving compare] type capture_mode = ByReference | ByValue [@@deriving compare, equal]
let string_of_capture_mode = function ByReference -> "by ref" | ByValue -> "by value" let string_of_capture_mode = function ByReference -> "by ref" | ByValue -> "by value"

@ -174,6 +174,6 @@ val rename : f:(string -> string) -> t -> t
(** Sets of pvars. *) (** Sets of pvars. *)
module Set : PrettyPrintable.PPSet with type elt = t module Set : PrettyPrintable.PPSet with type elt = t
type capture_mode = ByReference | ByValue [@@deriving compare] type capture_mode = ByReference | ByValue [@@deriving compare, equal]
val string_of_capture_mode : capture_mode -> string val string_of_capture_mode : capture_mode -> string

@ -23,7 +23,7 @@ type if_kind =
| Ik_land_lor (** obtained from translation of && or || *) | Ik_land_lor (** obtained from translation of && or || *)
| Ik_while | Ik_while
| Ik_switch | Ik_switch
[@@deriving compare] [@@deriving compare, equal]
type instr_metadata = type instr_metadata =
| Abstract of Location.t | Abstract of Location.t

@ -22,7 +22,7 @@ type if_kind =
| Ik_land_lor (** obtained from translation of && or || *) | Ik_land_lor (** obtained from translation of && or || *)
| Ik_while | Ik_while
| Ik_switch | Ik_switch
[@@deriving compare] [@@deriving compare, equal]
type instr_metadata = type instr_metadata =
| Abstract of Location.t | Abstract of Location.t

@ -1881,6 +1881,12 @@ and pulse_model_transfer_ownership =
are method or namespace::method" are method or namespace::method"
and pulse_report_latent_issues =
CLOpt.mk_bool ~long:"pulse-report-latent-issues"
"Only use for testing, there should be no need to turn this on for regular code analysis. \
Report latent issues instead of waiting for them to become concrete."
and pulse_widen_threshold = and pulse_widen_threshold =
CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3 CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3
"Under-approximate after $(i,int) loop iterations" "Under-approximate after $(i,int) loop iterations"
@ -3025,6 +3031,8 @@ and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
List.partition_map ~f:aux models List.partition_map ~f:aux models
and pulse_report_latent_issues = !pulse_report_latent_issues
and pulse_widen_threshold = !pulse_widen_threshold and pulse_widen_threshold = !pulse_widen_threshold
and pure_by_default = !pure_by_default and pure_by_default = !pure_by_default

@ -469,6 +469,8 @@ val pulse_model_transfer_ownership_namespace : (string * string) list
val pulse_model_transfer_ownership : string list val pulse_model_transfer_ownership : string list
val pulse_report_latent_issues : bool
val pulse_widen_threshold : int val pulse_widen_threshold : int
val pure_by_default : bool val pure_by_default : bool

@ -142,7 +142,7 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai
match exec_state with match exec_state with
| ExitProgram astate -> | ExitProgram astate ->
(astate, true) (astate, true)
| AbortProgram astate | ContinueProgram astate -> | AbortProgram astate | ContinueProgram astate | LatentAbortProgram {astate} ->
(astate, false) (astate, false)
in in
let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in

@ -12,21 +12,40 @@ open IResult.Let_syntax
open PulseBasicInterface open PulseBasicInterface
open PulseDomainInterface open PulseDomainInterface
let report {InterproceduralAnalysis.proc_desc; err_log} diagnostic = let report ?(extra_trace = []) proc_desc err_log diagnostic =
let open Diagnostic in let open Diagnostic in
Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic) Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic)
~ltr:(extra_trace @ get_trace diagnostic)
Pulse (get_issue_type diagnostic) (get_message diagnostic) Pulse (get_issue_type diagnostic) (get_message diagnostic)
let check_error_transform analysis_data ~f = function let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = function
| Ok astate -> | Ok astate ->
f astate f astate
| Error (diagnostic, astate) -> | Error (diagnostic, astate) -> (
let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
if is_unsat then [] if is_unsat then []
else ( else
report analysis_data diagnostic ; let astate = AbductiveDomain.of_post proc_desc astate in
[ExecutionDomain.AbortProgram astate] ) if PulseArithmetic.is_unsat_cheap astate then []
else
match LatentIssue.should_report_diagnostic astate diagnostic with
| `ReportNow ->
report proc_desc err_log diagnostic ;
[ExecutionDomain.AbortProgram astate]
| `DelayReport latent_issue ->
( if Config.pulse_report_latent_issues then
(* 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
let location = Diagnostic.get_location diagnostic in
[Errlog.make_trace_element depth location "*** LATENT ***" tags]
in
report ~extra_trace proc_desc err_log diagnostic ) ;
[ExecutionDomain.LatentAbortProgram {astate; latent_issue}] )
let check_error_continue analysis_data result = let check_error_continue analysis_data result =
@ -83,14 +102,14 @@ module PulseTransferFunctions = struct
(** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
let exec_object_out_of_scope call_loc (pvar, typ) exec_state = let exec_object_out_of_scope call_loc (pvar, typ) exec_state =
match exec_state with match (exec_state : ExecutionDomain.t) with
| ExecutionDomain.ContinueProgram astate -> | ContinueProgram astate ->
let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in
(* invalidate [&x] *) (* invalidate [&x] *)
PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
>>| ExecutionDomain.continue >>| ExecutionDomain.continue
| ExecutionDomain.AbortProgram _ | ExecutionDomain.ExitProgram _ -> | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
Ok exec_state Ok exec_state
@ -183,7 +202,7 @@ module PulseTransferFunctions = struct
~f:(fun astates (astate : Domain.t) -> ~f:(fun astates (astate : Domain.t) ->
let astate = let astate =
match astate with match astate with
| AbortProgram _ | ExitProgram _ -> | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
[astate] [astate]
| ContinueProgram astate -> | ContinueProgram astate ->
dispatch_call analysis_data ret call_exp actuals location call_flags astate dispatch_call analysis_data ret call_exp actuals location call_flags astate
@ -207,7 +226,7 @@ module PulseTransferFunctions = struct
let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data) let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
_cfg_node (instr : Sil.instr) : Domain.t list = _cfg_node (instr : Sil.instr) : Domain.t list =
match astate with match astate with
| AbortProgram _ -> | AbortProgram _ | LatentAbortProgram _ ->
(* We can also continue the analysis with the error state here (* We can also continue the analysis with the error state here
but there might be a risk we would get nonsense. *) but there might be a risk we would get nonsense. *)
[astate] [astate]
@ -258,7 +277,7 @@ module PulseTransferFunctions = struct
List.fold List.fold
~f:(fun astates (astate : Domain.t) -> ~f:(fun astates (astate : Domain.t) ->
match astate with match astate with
| AbortProgram _ | ExitProgram _ -> | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
[astate] [astate]
| ContinueProgram astate -> | ContinueProgram astate ->
let astate = let astate =

@ -52,3 +52,7 @@ let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.
let is_unsat_expensive astate = let is_unsat_expensive astate =
let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in
(AbductiveDomain.set_path_condition phi' astate, is_unsat) (AbductiveDomain.set_path_condition phi' astate, is_unsat)
let has_no_assumptions astate =
PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition

@ -35,3 +35,5 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
val is_unsat_cheap : AbductiveDomain.t -> bool val is_unsat_cheap : AbductiveDomain.t -> bool
val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool
val has_no_assumptions : AbductiveDomain.t -> bool

@ -12,7 +12,7 @@ type t =
| Model of string | Model of string
| SkippedKnownCall of Procname.t | SkippedKnownCall of Procname.t
| SkippedUnknownCall of Exp.t | SkippedUnknownCall of Exp.t
[@@deriving compare] [@@deriving compare, equal]
let pp_config ~verbose fmt = let pp_config ~verbose fmt =
let pp_proc_name = if verbose then Procname.pp else Procname.describe in let pp_proc_name = if verbose then Procname.pp else Procname.describe in

@ -13,7 +13,7 @@ type t =
| Model of string (** hardcoded model *) | Model of string (** hardcoded model *)
| SkippedKnownCall of Procname.t (** known function without summary *) | SkippedKnownCall of Procname.t (** known function without summary *)
| SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *)
[@@deriving compare] [@@deriving compare, equal]
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit

@ -12,21 +12,30 @@ module Invalidation = PulseInvalidation
module Trace = PulseTrace module Trace = PulseTrace
module ValueHistory = PulseValueHistory module ValueHistory = PulseValueHistory
type access_to_invalid_address =
{ calling_context: (CallEvent.t * Location.t) list
; invalidation: Invalidation.t
; invalidation_trace: Trace.t
; access_trace: Trace.t }
[@@deriving equal]
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of access_to_invalid_address
{invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
| MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
| StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
[@@deriving equal]
let get_location = function let get_location = function
| AccessToInvalidAddress {access_trace} -> | AccessToInvalidAddress {calling_context= []; access_trace} ->
Trace.get_outer_location access_trace Trace.get_outer_location access_trace
| AccessToInvalidAddress {calling_context= (_, location) :: _} ->
(* report at the call site that triggers the bug *) location
| MemoryLeak {location} | StackVariableAddressEscape {location} -> | MemoryLeak {location} | StackVariableAddressEscape {location} ->
location location
let get_message = function let get_message = function
| AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} -> | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} ->
(* The goal is to get one of the following messages depending on the scenario: (* The goal is to get one of the following messages depending on the scenario:
42: delete x; return x->f 42: delete x; return x->f
@ -44,19 +53,27 @@ let get_message = function
Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
"`x->f` accesses `x`, which was invalidated at line 42 by `delete`" "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
*) *)
(* whether the [calling_context + trace] starts with a call or contains only an immediate event *)
let immediate_or_first_call calling_context (trace : Trace.t) =
match (calling_context, trace) with
| [], Immediate _ ->
`Immediate
| (f, _) :: _, _ | [], ViaCall {f; _} ->
`Call f
in
let pp_access_trace fmt (trace : Trace.t) = let pp_access_trace fmt (trace : Trace.t) =
match trace with match immediate_or_first_call calling_context trace with
| Immediate _ -> | `Immediate ->
F.fprintf fmt "accessing memory that " F.fprintf fmt "accessing memory that "
| ViaCall {f; _} -> | `Call f ->
F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f
in in
let pp_invalidation_trace line invalidation fmt (trace : Trace.t) = let pp_invalidation_trace line invalidation fmt (trace : Trace.t) =
let pp_line fmt line = F.fprintf fmt " on line %d" line in let pp_line fmt line = F.fprintf fmt " on line %d" line in
match trace with match immediate_or_first_call calling_context trace with
| Immediate _ -> | `Immediate ->
F.fprintf fmt "%a%a" Invalidation.describe invalidation pp_line line F.fprintf fmt "%a%a" Invalidation.describe invalidation pp_line line
| ViaCall {f; _} -> | `Call f ->
F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalidation F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalidation
pp_line line CallEvent.describe f pp_line line CallEvent.describe f
in in
@ -97,7 +114,21 @@ let add_errlog_header ~title location errlog =
let get_trace = function let get_trace = function
| AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} -> | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} ->
(fun errlog ->
match calling_context with
| [] ->
errlog
| (_, first_call_loc) :: _ ->
add_errlog_header ~title:"calling context starts here" first_call_loc
@@ ( List.fold calling_context ~init:(errlog, 0) ~f:(fun (errlog, depth) (call, loc) ->
( Errlog.make_trace_element depth loc
(F.asprintf "in call to %a" CallEvent.pp call)
[]
:: errlog
, depth + 1 ) )
|> fst ) )
@@
let start_location = Trace.get_start_location invalidation_trace in let start_location = Trace.get_start_location invalidation_trace in
add_errlog_header ~title:"invalidation part of the trace starts here" start_location add_errlog_header ~title:"invalidation part of the trace starts here" start_location
@@ Trace.add_to_errlog ~nesting:1 @@ Trace.add_to_errlog ~nesting:1

@ -6,16 +6,30 @@
*) *)
open! IStd open! IStd
module CallEvent = PulseCallEvent
module Invalidation = PulseInvalidation module Invalidation = PulseInvalidation
module Trace = PulseTrace module Trace = PulseTrace
module ValueHistory = PulseValueHistory module ValueHistory = PulseValueHistory
type access_to_invalid_address =
{ calling_context: (CallEvent.t * Location.t) list
(** the list of function calls leading to the issue being realised, which is an additional
common prefix to the traces in the record *)
; invalidation: Invalidation.t
; invalidation_trace: Trace.t
(** assuming we are in the calling context, the trace leads to [invalidation] without
further assumptions *)
; access_trace: Trace.t
(** assuming we are in the calling context, the trace leads to an access to the value
invalidated in [invalidation_trace] without further assumptions *) }
[@@deriving equal]
(** an error to report to the user *) (** an error to report to the user *)
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of access_to_invalid_address
{invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
| MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
| StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
[@@deriving equal]
val get_message : t -> string val get_message : t -> string

@ -21,6 +21,7 @@ module BaseDomain = PulseBaseDomain
module BaseStack = PulseBaseStack module BaseStack = PulseBaseStack
module BaseMemory = PulseBaseMemory module BaseMemory = PulseBaseMemory
module BaseAddressAttributes = PulseBaseAddressAttributes module BaseAddressAttributes = PulseBaseAddressAttributes
module LatentIssue = PulseLatentIssue
(** {2 Enforce short form usage} *) (** {2 Enforce short form usage} *)
@ -36,4 +37,5 @@ include struct
[@@deprecated "use the short form BaseAddressAttributes instead"] [@@deprecated "use the short form BaseAddressAttributes instead"]
module PulseExecutionDomain = PulseExecutionDomain module PulseExecutionDomain = PulseExecutionDomain
[@@deprecated "use the short form ExecutionDomain instead"] [@@deprecated "use the short form ExecutionDomain instead"]
module PulseLatentIssue = PulseLatentIssue [@@deprecated "use the short form LatentIssue instead"]
end end

@ -8,12 +8,15 @@
open! IStd open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain module AbductiveDomain = PulseAbductiveDomain
module LatentIssue = PulseLatentIssue
type t = type t =
| AbortProgram of AbductiveDomain.t | AbortProgram of AbductiveDomain.t
| ContinueProgram of AbductiveDomain.t | ContinueProgram of AbductiveDomain.t
| ExitProgram of AbductiveDomain.t | ExitProgram of AbductiveDomain.t
| LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
let continue astate = ContinueProgram astate let continue astate = ContinueProgram astate
@ -25,6 +28,9 @@ let leq ~lhs ~rhs =
| ContinueProgram astate1, ContinueProgram astate2 | ContinueProgram astate1, ContinueProgram astate2
| ExitProgram astate1, ExitProgram astate2 -> | ExitProgram astate1, ExitProgram astate2 ->
AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
| ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
, LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
LatentIssue.equal issue1 issue2 && AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
| _ -> | _ ->
false false
@ -36,6 +42,12 @@ let pp fmt = function
F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate
| AbortProgram astate -> | AbortProgram astate ->
F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate
| LatentAbortProgram {astate; latent_issue} ->
let diagnostic = LatentIssue.to_diagnostic latent_issue in
let message = Diagnostic.get_message diagnostic in
let location = Diagnostic.get_location diagnostic in
F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message
AbductiveDomain.pp astate
let map ~f exec_state = let map ~f exec_state =
@ -46,11 +58,18 @@ let map ~f exec_state =
ContinueProgram (f astate) ContinueProgram (f astate)
| ExitProgram astate -> | ExitProgram astate ->
ExitProgram (f astate) ExitProgram (f astate)
| LatentAbortProgram {astate; latent_issue} ->
LatentAbortProgram {astate= f astate; latent_issue}
let of_posts pdesc posts = let of_posts pdesc posts =
List.filter_mapi posts ~f:(fun i exec_state -> List.filter_mapi posts ~f:(fun i exec_state ->
let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in let ( AbortProgram astate
| ContinueProgram astate
| ExitProgram astate
| LatentAbortProgram {astate} ) =
exec_state
in
L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
if is_unsat then None if is_unsat then None

@ -4,18 +4,22 @@
* This source code is licensed under the MIT license found in the * This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree. * LICENSE file in the root directory of this source tree.
*) *)
open! IStd open! IStd
module AbductiveDomain = PulseAbductiveDomain
module LatentIssue = PulseLatentIssue
type t = type t =
| AbortProgram of PulseAbductiveDomain.t | AbortProgram of AbductiveDomain.t
(** represents the state at the program point that caused an error *) (** represents the state at the program point that caused an error *)
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) | ContinueProgram of AbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t | ExitProgram of AbductiveDomain.t (** represents the state originating at exit/divergence. *)
(** represents the state originating at exit/divergence. *) | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
(** this path leads to an error but we don't have conclusive enough data to report it yet *)
include AbstractDomain.NoJoin with type t := t include AbstractDomain.NoJoin with type t := t
val continue : PulseAbductiveDomain.t -> t val continue : AbductiveDomain.t -> t
val of_posts : Procdesc.t -> t list -> t list val of_posts : Procdesc.t -> t list -> t list

@ -925,9 +925,19 @@ module Atom = struct
Term.has_var_notin vars t1 || Term.has_var_notin vars t2 Term.has_var_notin vars t1 || Term.has_var_notin vars t2
module Set = Caml.Set.Make (struct module Set = struct
type nonrec t = t [@@deriving compare] include Caml.Set.Make (struct
end) type nonrec t = t [@@deriving compare]
end)
let pp_with_pp_var pp_var fmt atoms =
if is_empty atoms then F.pp_print_string fmt "true (no atoms)"
else
Pp.collection ~sep:""
~fold:(IContainer.fold_of_pervasives_set_fold fold)
~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (pp_with_pp_var pp_var) atom)
fmt atoms
end
end end
module SatUnsatMonad = struct module SatUnsatMonad = struct
@ -957,267 +967,293 @@ module VarUF =
end) end)
(Var.Set) (Var.Set)
type t = module Formula = struct
{ var_eqs: VarUF.t (** equality relation between variables *) type t =
; linear_eqs: LinArith.t Var.Map.t { var_eqs: VarUF.t (** equality relation between variables *)
(** equalities of the form [x = l] where [l] is from linear arithmetic *) ; linear_eqs: LinArith.t Var.Map.t
; atoms: Atom.Set.t (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) } (** equalities of the form [x = l] where [l] is from linear arithmetic *)
; atoms: Atom.Set.t (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) }
let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty} let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty}
let pp_with_pp_var pp_var fmt phi = let pp_with_pp_var pp_var fmt phi =
let pp_linear_eqs fmt m = let pp_linear_eqs fmt m =
if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)" if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)"
else else
Pp.collection ~sep:"" Pp.collection ~sep:""
~fold:(IContainer.fold_of_pervasives_map_fold Var.Map.fold) ~fold:(IContainer.fold_of_pervasives_map_fold Var.Map.fold)
~pp_item:(fun fmt (v, l) -> F.fprintf fmt "%a = %a" pp_var v (LinArith.pp pp_var) l) ~pp_item:(fun fmt (v, l) -> F.fprintf fmt "%a = %a" pp_var v (LinArith.pp pp_var) l)
fmt m fmt m
in in
let pp_atoms fmt atoms = F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
if Atom.Set.is_empty atoms then F.pp_print_string fmt "true (no atoms)" (VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
else phi.var_eqs pp_linear_eqs phi.linear_eqs (Atom.Set.pp_with_pp_var pp_var) phi.atoms
Pp.collection ~sep:""
~fold:(IContainer.fold_of_pervasives_set_fold Atom.Set.fold)
~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (Atom.pp_with_pp_var pp_var) atom)
fmt atoms
in
F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
(VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
phi.var_eqs pp_linear_eqs phi.linear_eqs pp_atoms phi.atoms
let pp = pp_with_pp_var Var.pp (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
module Normalizer : sig
val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized
(** module that breaks invariants more often that the rest, with an interface that is safer to use *) val and_var_var : Var.t -> Var.t -> t -> t normalized
module Normalizer : sig
val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized
val and_var_var : Var.t -> Var.t -> t -> t normalized val and_atom : Atom.t -> t -> t normalized
val and_atom : Atom.t -> t -> t normalized val normalize_atom : t -> Atom.t -> Atom.t option normalized
val normalize : t -> t normalized val normalize : t -> t normalized
end = struct
(* Use the monadic notations when normalizing formulas. *)
open SatUnsatMonad
(** OVERVIEW: the best way to think about this is as a half-assed Shostak technique.
The [var_eqs] and [linear_eqs] parts of a formula are kept in a normal form of sorts. We apply
some deduction every time a new equality is discovered. Where this is incomplete is that 1) we
don't insist on normalizing the linear part of the relation always, and 2) we stop discovering
new consequences of facts after some fixed number of steps (the [fuel] argument of some of the
functions of this module).
Normalizing more than 1) happens on [normalize], where we rebuild the linear equality relation
(the equalities between variables are always "normalized" thanks to the union-find data
structure).
For 2), there is no mitigation as saturating the consequences of what we know implies keeping
track of *all* the consequences (to avoid diverging by re-discovering the same facts over and
over), which would be expensive.
There is also an interaction between equality classes and linear equalities [x = l], as each
such key [x] in the [linear_eqs] map is (or was at some point) the representative of its
class. Unlike (non-diverging...) Shostak techniques, we do not try very hard to normalize the
[l] in the linear equalities.
Disclaimer: It could be that this half-assedness is premature optimisation and that we could
afford much more completeness. *)
(** the canonical representative of a given variable *)
let get_repr phi x = VarUF.find phi.var_eqs x
(** substitute vars in [l] *once* with their linear form to discover more simplification
opportunities *)
let apply phi l =
LinArith.subst_variables l ~f:(fun v ->
let repr = (get_repr phi v :> Var.t) in
match Var.Map.find_opt repr phi.linear_eqs with
| None ->
VarSubst repr
| Some l' ->
LinSubst l' )
val implies_atom : t -> Atom.t -> bool
end = struct
(* Use the monadic notations when normalizing formulas. *)
open SatUnsatMonad
let rec solve_normalized_eq ~fuel l1 l2 phi = (** OVERVIEW: the best way to think about this is as a half-assed Shostak technique.
LinArith.solve_eq l1 l2
>>= function
| None ->
Sat phi
| Some (v, l) -> (
match LinArith.get_as_var l with
| Some v' ->
merge_vars ~fuel (v :> Var.t) v' phi
| None -> (
match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
| None ->
(* this can break the (as a result non-)invariant that variables in the domain of
[linear_eqs] do not appear in the range of [linear_eqs] *)
Sat {phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}
| Some l' ->
(* This is the only step that consumes fuel: discovering an equality [l = l']: because we
do not record these anywhere (except when there consequence can be recorded as [y =
l''] or [y = y'], we could potentially discover the same equality over and over and
diverge otherwise. Or could we? *)
(* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
normalize it *)
if fuel > 0 then (
L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi )
else (
(* [fuel = 0]: give up simplifying further for fear of diverging *)
L.d_printfln "Ran out of fuel solving linear equality" ;
Sat phi ) ) )
and merge_vars ~fuel v1 v2 phi =
let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
let phi = {phi with var_eqs} in
match subst_opt with
| None ->
(* we already knew the equality *)
Sat phi
| Some (v_old, v_new) -> (
(* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
(* NOTE: we try to maintain the invariant that for all [x=l] in [phi.linear_eqs], [x ∉
vars(l)]. We also try to stay as close as possible (without going back and re-normalizing
every linear equality every time we learn new equalities) to the invariant that the
domain and the range of [phi.linear_eqs] mention distinct variables. This is to speed up
normalization steps: when the stronger invariant holds we can normalize in one step (in
[normalize_linear_eqs]). *)
let v_new = (v_new :> Var.t) in
let phi, l_new =
match Var.Map.find_opt v_new phi.linear_eqs with
| None ->
(phi, None)
| Some l ->
if LinArith.has_var v_old l then
let l_new = LinArith.subst v_old v_new l in
let linear_eqs = Var.Map.add v_new l_new phi.linear_eqs in
({phi with linear_eqs}, Some l_new)
else (phi, Some l)
in
let phi, l_old =
match Var.Map.find_opt v_old phi.linear_eqs with
| None ->
(phi, None)
| Some l_old ->
(* [l_old] has no [v_old] or [v_new] by invariant so no need to subst, unlike for
[l_new] above: variables in [l_old] are strictly greater than [v_old], and [v_new]
is smaller than [v_old] *)
({phi with linear_eqs= Var.Map.remove v_old phi.linear_eqs}, Some l_old)
in
match (l_old, l_new) with
| None, None | None, Some _ ->
Sat phi
| Some l, None ->
Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}
| Some l1, Some l2 ->
(* no need to consume fuel here as we can only go through this branch finitely many
times because there are finitely many variables in a given formula *)
(* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
solve_normalized_eq ~fuel l1 l2 phi )
The [var_eqs] and [linear_eqs] parts of a formula are kept in a normal form of sorts. We
apply some deduction every time a new equality is discovered. Where this is incomplete is
that 1) we don't insist on normalizing the linear part of the relation always, and 2) we
stop discovering new consequences of facts after some fixed number of steps (the [fuel]
argument of some of the functions of this module).
(** an arbitrary value *) Normalizing more than 1) happens on [normalize], where we rebuild the linear equality
let base_fuel = 5 relation (the equalities between variables are always "normalized" thanks to the union-find
data structure).
let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi For 2), there is no mitigation as saturating the consequences of what we know implies
keeping track of *all* the consequences (to avoid diverging by re-discovering the same facts
over and over), which would be expensive.
let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi There is also an interaction between equality classes and linear equalities [x = l], as each
such key [x] in the [linear_eqs] map is (or was at some point) the representative of its
class. Unlike (non-diverging...) Shostak techniques, we do not try very hard to normalize
the [l] in the linear equalities.
let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi Disclaimer: It could be that this half-assedness is premature optimisation and that we could
afford much more completeness. *)
let rec normalize_linear_eqs ~fuel phi0 = (** the canonical representative of a given variable *)
let* changed, phi' = let get_repr phi x = VarUF.find phi.var_eqs x
(* reconstruct the relation from scratch *)
Var.Map.fold (** substitute vars in [l] *once* with their linear form to discover more simplification
(fun v l acc -> opportunities *)
let* changed, phi = acc in let apply phi l =
let l' = apply phi0 l in LinArith.subst_variables l ~f:(fun v ->
let+ phi' = and_var_linarith v l' phi in let repr = (get_repr phi v :> Var.t) in
(changed || not (phys_equal l l'), phi') ) match Var.Map.find_opt repr phi.linear_eqs with
phi0.linear_eqs
(Sat (false, {phi0 with linear_eqs= Var.Map.empty}))
in
if changed then
if fuel > 0 then (
(* do another pass if we can afford it *)
L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
normalize_linear_eqs ~fuel:(fuel - 1) phi' )
else (
L.d_printfln "ran out of fuel normalizing linear equalities" ;
Sat phi' )
else Sat phi0
let normalize_atom phi (atom : Atom.t) =
let normalize_term phi t =
Term.subst_variables t ~f:(fun v ->
let v_canon = (VarUF.find phi.var_eqs v :> Var.t) in
match Var.Map.find_opt v_canon phi.linear_eqs with
| None -> | None ->
VarSubst v_canon VarSubst repr
| Some l -> ( | Some l' ->
match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) ) LinSubst l' )
in
let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in
Atom.eval atom' |> sat_of_eval_result
(** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if let rec solve_normalized_eq ~fuel l1 l2 phi =
[phi.linear_eqs] was changed as a result *) LinArith.solve_eq l1 l2
let and_atom atom phi = >>= function
normalize_atom phi atom | None ->
>>= function Sat phi
| None -> | Some (v, l) -> (
Sat (false, phi) match LinArith.get_as_var l with
| Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) -> | Some v' ->
(* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so merge_vars ~fuel (v :> Var.t) v' phi
they end up only on one side, hence only this match case is needed to detect linear | None -> (
equalities *) match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
let+ phi' = solve_eq l (LinArith.of_q c) phi in | None ->
(true, phi') (* this can break the (as a result non-)invariant that variables in the domain of
| Some atom' -> [linear_eqs] do not appear in the range of [linear_eqs] *)
Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms}) Sat {phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}
| Some l' ->
(* This is the only step that consumes fuel: discovering an equality [l = l']: because we
let normalize_atoms phi = do not record these anywhere (except when there consequence can be recorded as [y =
let atoms0 = phi.atoms in l''] or [y = y'], we could potentially discover the same equality over and over and
let init = Sat (false, {phi with atoms= Atom.Set.empty}) in diverge otherwise. Or could we? *)
IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom -> (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
let* changed, phi = acc in normalize it *)
let+ changed', phi = and_atom atom phi in if fuel > 0 then (
(changed || changed', phi) ) L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi )
else (
let normalize phi = (* [fuel = 0]: give up simplifying further for fear of diverging *)
(* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by L.d_printfln "Ran out of fuel solving linear equality" ;
[normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining Sat phi ) ) )
fuel). That's ok because there's not much fuel to begin with, and as long as we're making
progress it's probably worth it anyway. *)
let rec normalize_with_fuel ~fuel phi = and merge_vars ~fuel v1 v2 phi =
if fuel <= 0 then ( let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
L.d_printfln "ran out of fuel when normalizing" ; let phi = {phi with var_eqs} in
Sat phi ) match subst_opt with
else | None ->
let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in (* we already knew the equality *)
if new_linear_eqs then ( Sat phi
L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ; | Some (v_old, v_new) -> (
normalize_with_fuel ~fuel:(fuel - 1) phi ) (* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
else Sat phi l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
in (* NOTE: we try to maintain the invariant that for all [x=l] in [phi.linear_eqs], [x ∉
normalize_with_fuel ~fuel:base_fuel phi vars(l)]. We also try to stay as close as possible (without going back and re-normalizing
every linear equality every time we learn new equalities) to the invariant that the
domain and the range of [phi.linear_eqs] mention distinct variables. This is to speed up
normalization steps: when the stronger invariant holds we can normalize in one step (in
[normalize_linear_eqs]). *)
let v_new = (v_new :> Var.t) in
let phi, l_new =
match Var.Map.find_opt v_new phi.linear_eqs with
| None ->
(phi, None)
| Some l ->
if LinArith.has_var v_old l then
let l_new = LinArith.subst v_old v_new l in
let linear_eqs = Var.Map.add v_new l_new phi.linear_eqs in
({phi with linear_eqs}, Some l_new)
else (phi, Some l)
in
let phi, l_old =
match Var.Map.find_opt v_old phi.linear_eqs with
| None ->
(phi, None)
| Some l_old ->
(* [l_old] has no [v_old] or [v_new] by invariant so no need to subst, unlike for
[l_new] above: variables in [l_old] are strictly greater than [v_old], and [v_new]
is smaller than [v_old] *)
({phi with linear_eqs= Var.Map.remove v_old phi.linear_eqs}, Some l_old)
in
match (l_old, l_new) with
| None, None | None, Some _ ->
Sat phi
| Some l, None ->
Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}
| Some l1, Some l2 ->
(* no need to consume fuel here as we can only go through this branch finitely many
times because there are finitely many variables in a given formula *)
(* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
solve_normalized_eq ~fuel l1 l2 phi )
(** an arbitrary value *)
let base_fuel = 5
let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi
let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi
let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi
let rec normalize_linear_eqs ~fuel phi0 =
let* changed, phi' =
(* reconstruct the relation from scratch *)
Var.Map.fold
(fun v l acc ->
let* changed, phi = acc in
let l' = apply phi0 l in
let+ phi' = and_var_linarith v l' phi in
(changed || not (phys_equal l l'), phi') )
phi0.linear_eqs
(Sat (false, {phi0 with linear_eqs= Var.Map.empty}))
in
if changed then
if fuel > 0 then (
(* do another pass if we can afford it *)
L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
normalize_linear_eqs ~fuel:(fuel - 1) phi' )
else (
L.d_printfln "ran out of fuel normalizing linear equalities" ;
Sat phi' )
else Sat phi0
let normalize_atom phi (atom : Atom.t) =
let normalize_term phi t =
Term.subst_variables t ~f:(fun v ->
let v_canon = (VarUF.find phi.var_eqs v :> Var.t) in
match Var.Map.find_opt v_canon phi.linear_eqs with
| None ->
VarSubst v_canon
| Some l -> (
match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) )
in
let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in
Atom.eval atom' |> sat_of_eval_result
let and_atom atom phi = and_atom atom phi >>| snd (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
[phi.linear_eqs] was changed as a result *)
let and_atom atom phi =
normalize_atom phi atom
>>= function
| None ->
Sat (false, phi)
| Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) ->
(* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so
they end up only on one side, hence only this match case is needed to detect linear
equalities *)
let+ phi' = solve_eq l (LinArith.of_q c) phi in
(true, phi')
| Some atom' ->
Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms})
let normalize_atoms phi =
let atoms0 = phi.atoms in
let init = Sat (false, {phi with atoms= Atom.Set.empty}) in
IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom ->
let* changed, phi = acc in
let+ changed', phi = and_atom atom phi in
(changed || changed', phi) )
let normalize phi =
(* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by
[normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining
fuel). That's ok because there's not much fuel to begin with, and as long as we're making
progress it's probably worth it anyway. *)
let rec normalize_with_fuel ~fuel phi =
if fuel <= 0 then (
L.d_printfln "ran out of fuel when normalizing" ;
Sat phi )
else
let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in
if new_linear_eqs then (
L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
normalize_with_fuel ~fuel:(fuel - 1) phi )
else Sat phi
in
normalize_with_fuel ~fuel:base_fuel phi
let and_atom atom phi = and_atom atom phi >>| snd
let implies_atom phi atom =
(* [φ ⊢ a] iff [φ ∧ ¬a] is inconsistent *)
match and_atom (Atom.nnot atom) phi with Sat _ -> false | Unsat -> true
end
end end
(** Instead of a single formula, distinguish what we have observed to be true (coming from
assignments) from what we have assumed to be true (coming from conditionals). This lets us delay
reporting certain errors until no assumptions are needed (i.e. the issue is certain to arise
regardless of context). *)
type t =
{ known: Formula.t (** all the things we know to be true for sure *)
; pruned: Atom.Set.t (** collection of conditions that have to be true along the path *)
; both: Formula.t (** [both = known ∧ pruned], allows us to detect contradictions *) }
let ttrue = {known= Formula.ttrue; pruned= Atom.Set.empty; both= Formula.ttrue}
let pp_with_pp_var pp_var fmt {known; pruned; both} =
F.fprintf fmt "@[known=%a,@;pruned=%a,@;both=%a@]@." (Formula.pp_with_pp_var pp_var) known
(Atom.Set.pp_with_pp_var pp_var) pruned (Formula.pp_with_pp_var pp_var) both
let pp = pp_with_pp_var Var.pp
let and_known_atom atom phi =
let open SatUnsatMonad in
let* known = Formula.Normalizer.and_atom atom phi.known in
let+ both = Formula.Normalizer.and_atom atom phi.both in
{phi with known; both}
let and_mk_atom mk_atom op1 op2 phi = let and_mk_atom mk_atom op1 op2 phi =
Normalizer.and_atom (mk_atom (Term.of_operand op1) (Term.of_operand op2)) phi let atom = mk_atom (Term.of_operand op1) (Term.of_operand op2) in
and_known_atom atom phi
let and_equal = and_mk_atom Atom.equal let and_equal = and_mk_atom Atom.equal
@ -1227,22 +1263,49 @@ let and_less_equal = and_mk_atom Atom.less_equal
let and_less_than = and_mk_atom Atom.less_than let and_less_than = and_mk_atom Atom.less_than
let and_equal_unop v (op : Unop.t) x phi = let and_equal_unop v (op : Unop.t) x phi =
Normalizer.and_atom (Equal (Var v, Term.of_unop op (Term.of_operand x))) phi and_known_atom (Equal (Var v, Term.of_unop op (Term.of_operand x))) phi
let and_equal_binop v (bop : Binop.t) x y phi = let and_equal_binop v (bop : Binop.t) x y phi =
Normalizer.and_atom (Equal (Var v, Term.of_binop bop (Term.of_operand x) (Term.of_operand y))) phi and_known_atom (Equal (Var v, Term.of_binop bop (Term.of_operand x) (Term.of_operand y))) phi
let prune_binop ~negated (bop : Binop.t) x y phi = let prune_binop ~negated (bop : Binop.t) x y phi =
let open SatUnsatMonad in
let tx = Term.of_operand x in let tx = Term.of_operand x in
let ty = Term.of_operand y in let ty = Term.of_operand y in
let t = Term.of_binop bop tx ty in let t = Term.of_binop bop tx ty in
let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in
Normalizer.and_atom atom phi let* both = Formula.Normalizer.and_atom atom phi.both in
let+ pruned =
(* Use [both] to normalize [atom] here to take previous [prune]s into account. This shouldn't
change whether [known |- pruned] overall, which is what we'll want to ultimately check in
{!has_no_assumptions}. *)
Formula.Normalizer.normalize_atom phi.both atom
>>| Option.fold ~init:phi.pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
in
{phi with pruned; both}
let normalize phi = Normalizer.normalize phi let normalize phi =
let open SatUnsatMonad in
let* both = Formula.Normalizer.normalize phi.both in
let* known = Formula.Normalizer.normalize phi.known in
let+ pruned =
Atom.Set.fold
(fun atom pruned_sat ->
let* pruned = pruned_sat in
match Formula.Normalizer.normalize_atom known atom with
| Unsat ->
Unsat
| Sat None ->
(* normalized to [true] *) pruned_sat
| Sat (Some atom) ->
Sat (Atom.Set.add atom pruned) )
phi.pruned (Sat Atom.Set.empty)
in
{both; known; pruned}
(** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *) (** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *)
let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var = let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
@ -1255,32 +1318,56 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
let sat_value_exn (norm : 'a normalized) = let sat_value_exn (norm : 'a normalized) =
match norm with Unsat -> raise Contradiction | Sat x -> x match norm with Unsat -> raise Contradiction | Sat x -> x
in in
let and_var_eqs acc = let and_var_eqs var_eqs_foreign acc_phi =
VarUF.fold_congruences phi_foreign.var_eqs ~init:acc VarUF.fold_congruences var_eqs_foreign ~init:acc_phi
~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) -> ~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) ->
let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in
IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi) IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi)
~f:(fun (acc_f, phi) v_foreign -> ~f:(fun (acc_f, phi) v_foreign ->
let acc_f, v = f_var acc_f v_foreign in let acc_f, v = f_var acc_f v_foreign in
let phi = Normalizer.and_var_var repr v phi |> sat_value_exn in let phi = Formula.Normalizer.and_var_var repr v phi |> sat_value_exn in
(acc_f, phi) ) ) (acc_f, phi) ) )
in in
let and_linear_eqs acc = let and_linear_eqs linear_eqs_foreign acc_phi =
IContainer.fold_of_pervasives_map_fold Var.Map.fold phi_foreign.linear_eqs ~init:acc IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi
~f:(fun (acc_f, phi) (v_foreign, l_foreign) -> ~f:(fun (acc_f, phi) (v_foreign, l_foreign) ->
let acc_f, v = f_var acc_f v_foreign in let acc_f, v = f_var acc_f v_foreign in
let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in
let phi = Normalizer.and_var_linarith v l phi |> sat_value_exn in let phi = Formula.Normalizer.and_var_linarith v l phi |> sat_value_exn in
(acc_f, phi) ) (acc_f, phi) )
in in
let and_atoms acc = let and_atoms atoms_foreign acc_phi =
IContainer.fold_of_pervasives_set_fold Atom.Set.fold phi_foreign.atoms ~init:acc IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi
~f:(fun (acc_f, phi) atom_foreign -> ~f:(fun (acc_f, phi) atom_foreign ->
let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
let phi = Normalizer.and_atom atom phi |> sat_value_exn in let phi = Formula.Normalizer.and_atom atom phi |> sat_value_exn in
(acc_f, phi) ) (acc_f, phi) )
in in
try Sat (and_var_eqs (init, phi0) |> and_linear_eqs |> and_atoms) with Contradiction -> Unsat let and_ phi_foreign acc phi =
try
Sat
( and_var_eqs phi_foreign.Formula.var_eqs (acc, phi)
|> and_linear_eqs phi_foreign.Formula.linear_eqs
|> and_atoms phi_foreign.Formula.atoms )
with Contradiction -> Unsat
in
let open SatUnsatMonad in
let* acc, both = and_ phi_foreign.both init phi0.both in
let* acc, known = and_ phi_foreign.known acc phi0.known in
let and_pruned pruned_foreign acc_pruned =
IContainer.fold_of_pervasives_set_fold Atom.Set.fold pruned_foreign ~init:acc_pruned
~f:(fun (acc_f, pruned) atom_foreign ->
let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
let atom_opt = Formula.Normalizer.normalize_atom known atom |> sat_value_exn in
let pruned =
Option.fold atom_opt ~init:pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
in
(acc_f, pruned) )
in
let+ acc, pruned =
try Sat (and_pruned phi_foreign.pruned (acc, phi0.pruned)) with Contradiction -> Unsat
in
(acc, {known; pruned; both})
(** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge (** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge
@ -1310,14 +1397,14 @@ let build_var_graph phi =
in in
Var.Set.iter (fun v -> add_set graph v vs) vs Var.Set.iter (fun v -> add_set graph v vs) vs
in in
Container.iter ~fold:VarUF.fold_congruences phi.var_eqs ~f:(fun ((repr : VarUF.repr), vs) -> Container.iter ~fold:VarUF.fold_congruences phi.Formula.var_eqs
add_all (Var.Set.add (repr :> Var.t) vs) ) ; ~f:(fun ((repr : VarUF.repr), vs) -> add_all (Var.Set.add (repr :> Var.t) vs)) ;
Var.Map.iter Var.Map.iter
(fun v l -> (fun v l ->
LinArith.get_variables l LinArith.get_variables l
|> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v) |> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v)
|> add_all ) |> add_all )
phi.linear_eqs ; phi.Formula.linear_eqs ;
(* add edges between all pairs of variables appearing in [t1] or [t2] (yes this is quadratic in (* add edges between all pairs of variables appearing in [t1] or [t2] (yes this is quadratic in
the number of variables of these terms) *) the number of variables of these terms) *)
let add_from_terms t1 t2 = let add_from_terms t1 t2 =
@ -1331,7 +1418,7 @@ let build_var_graph phi =
(fun atom -> (fun atom ->
let t1, t2 = Atom.get_terms atom in let t1, t2 = Atom.get_terms atom in
add_from_terms t1 t2 ) add_from_terms t1 t2 )
phi.atoms ; phi.Formula.atoms ;
graph graph
@ -1364,31 +1451,50 @@ let get_reachable_from graph vs =
let simplify ~keep phi = let simplify ~keep phi =
let open SatUnsatMonad in let open SatUnsatMonad in
let+ phi = normalize phi in let+ phi = normalize phi in
L.d_printfln "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ; L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
(* Get rid of atoms when they contain only variables that do not appear in atoms mentioning (* Get rid of atoms when they contain only variables that do not appear in atoms mentioning
variables in [keep], or variables appearing in atoms together with variables in [keep], and variables in [keep], or variables appearing in atoms together with variables in [keep], and
so on. In other words, the variables to keep are all the ones transitively reachable from so on. In other words, the variables to keep are all the ones transitively reachable from
variables in [keep] in the graph connecting two variables whenever they appear together in variables in [keep] in the graph connecting two variables whenever they appear together in
a same atom of the formula. *) a same atom of the formula. *)
let var_graph = build_var_graph phi in (* We only consider [phi.both] when building the relation. Considering [phi.known] and
[phi.pruned] as well could lead to us keeping more variables around, but that's not necessarily
a good idea. Ignoring them means we err on the side of reporting potentially slightly more
issues than we would otherwise, as some atoms in [phi.pruned] may vanish unfairly as a
result. *)
let var_graph = build_var_graph phi.both in
let vars_to_keep = get_reachable_from var_graph keep in let vars_to_keep = get_reachable_from var_graph keep in
L.d_printfln "Reachable vars: {%a}" Var.Set.pp vars_to_keep ; L.d_printfln "Reachable vars: {%a}" Var.Set.pp vars_to_keep ;
(* discard atoms which have variables *not* in [vars_to_keep], which in particular is enough (* discard atoms which have variables *not* in [vars_to_keep], which in particular is enough
to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive
closure on the graph above *) closure on the graph above *)
let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.var_eqs in let filter_atom atom = not (Atom.has_var_notin vars_to_keep atom) in
let linear_eqs = Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.linear_eqs in let simplify_phi phi =
let atoms = Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep atom)) phi.atoms in let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.Formula.var_eqs in
{var_eqs; linear_eqs; atoms} let linear_eqs =
Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.Formula.linear_eqs
in
let atoms = Atom.Set.filter filter_atom phi.Formula.atoms in
{Formula.var_eqs; linear_eqs; atoms}
in
let known = simplify_phi phi.known in
let both = simplify_phi phi.both in
let pruned = Atom.Set.filter filter_atom phi.pruned in
{known; pruned; both}
let is_known_zero phi v = let is_known_zero phi v =
Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs Var.Map.find_opt (VarUF.find phi.both.var_eqs v :> Var.t) phi.both.linear_eqs
|> Option.exists ~f:LinArith.is_zero |> Option.exists ~f:LinArith.is_zero
let as_int phi v = let as_int phi v =
let maybe_int q = if Z.equal (Q.den q) Z.one then Q.to_int q else None in let maybe_int q = if Z.equal (Q.den q) Z.one then Q.to_int q else None in
let open Option.Monad_infix in let open Option.Monad_infix in
Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs Var.Map.find_opt (VarUF.find phi.both.var_eqs v :> Var.t) phi.both.linear_eqs
>>= LinArith.get_as_const >>= maybe_int >>= LinArith.get_as_const >>= maybe_int
(** test if [phi.known ⊢ phi.pruned] *)
let has_no_assumptions phi =
Atom.Set.for_all (fun atom -> Formula.Normalizer.implies_atom phi.known atom) phi.pruned

@ -58,6 +58,8 @@ val is_known_zero : t -> Var.t -> bool
val as_int : t -> Var.t -> int option val as_int : t -> Var.t -> int option
val has_no_assumptions : t -> bool
(** {3 Notations} *) (** {3 Notations} *)
include sig include sig

@ -516,7 +516,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
( Diagnostic.AccessToInvalidAddress ( Diagnostic.AccessToInvalidAddress
{invalidation; invalidation_trace; access_trace} {calling_context= []; invalidation; invalidation_trace; access_trace}
, astate ) ) ) ) , astate ) ) ) )
call_state.subst (Ok call_state.astate) call_state.subst (Ok call_state.astate)

@ -16,7 +16,7 @@ type std_vector_function =
| PushBack | PushBack
| Reserve | Reserve
| ShrinkToFit | ShrinkToFit
[@@deriving compare] [@@deriving compare, equal]
let pp_std_vector_function f = function let pp_std_vector_function f = function
| Assign -> | Assign ->
@ -37,7 +37,7 @@ let pp_std_vector_function f = function
F.fprintf f "std::vector::shrink_to_fit" F.fprintf f "std::vector::shrink_to_fit"
type java_iterator_function = Remove [@@deriving compare] type java_iterator_function = Remove [@@deriving compare, equal]
let pp_java_iterator_function f = function Remove -> F.pp_print_string f "Iterator.remove" let pp_java_iterator_function f = function Remove -> F.pp_print_string f "Iterator.remove"
@ -50,7 +50,7 @@ type t =
| OptionalEmpty | OptionalEmpty
| StdVector of std_vector_function | StdVector of std_vector_function
| JavaIterator of java_iterator_function | JavaIterator of java_iterator_function
[@@deriving compare] [@@deriving compare, equal]
let issue_type_of_cause = function let issue_type_of_cause = function
| CFree -> | CFree ->

@ -17,11 +17,10 @@ type std_vector_function =
| PushBack | PushBack
| Reserve | Reserve
| ShrinkToFit | ShrinkToFit
[@@deriving compare]
val pp_std_vector_function : F.formatter -> std_vector_function -> unit val pp_std_vector_function : F.formatter -> std_vector_function -> unit
type java_iterator_function = Remove [@@deriving compare] type java_iterator_function = Remove
type t = type t =
| CFree | CFree
@ -32,7 +31,7 @@ type t =
| OptionalEmpty | OptionalEmpty
| StdVector of std_vector_function | StdVector of std_vector_function
| JavaIterator of java_iterator_function | JavaIterator of java_iterator_function
[@@deriving compare] [@@deriving compare, equal]
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit

@ -0,0 +1,32 @@
(*
* 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
type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal]
let to_diagnostic = function
| AccessToInvalidAddress access_to_invalid_address ->
Diagnostic.AccessToInvalidAddress access_to_invalid_address
let add_call call_and_loc = function
| AccessToInvalidAddress access ->
AccessToInvalidAddress {access with calling_context= call_and_loc :: access.calling_context}
let should_report astate = PulseArithmetic.has_no_assumptions astate
let should_report_diagnostic astate (diagnostic : Diagnostic.t) =
match diagnostic with
| MemoryLeak _ | StackVariableAddressEscape _ ->
(* these issues are reported regardless of the calling context, not sure if that's the right
decision yet *)
`ReportNow
| AccessToInvalidAddress diag ->
if should_report astate then `ReportNow else `DelayReport (AccessToInvalidAddress diag)

@ -0,0 +1,24 @@
(*
* 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
(** A subset of [PulseDiagnostic] that can be "latent", i.e. there is a potential issue in the code
but we want to delay reporting until we see the conditions for the bug manifest themselves in
some calling context. *)
type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal]
val to_diagnostic : t -> Diagnostic.t
val should_report : PulseAbductiveDomain.t -> bool
val should_report_diagnostic :
PulseAbductiveDomain.t -> Diagnostic.t -> [`ReportNow | `DelayReport of t]
val add_call : CallEvent.t * Location.t -> t -> t

@ -554,7 +554,7 @@ module GenericArrayBackedCollectionIterator = struct
let access_trace = Trace.Immediate {location; history= snd pointer} in let access_trace = Trace.Immediate {location; history= snd pointer} in
Error Error
( Diagnostic.AccessToInvalidAddress ( Diagnostic.AccessToInvalidAddress
{invalidation= EndIterator; invalidation_trace; access_trace} {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace}
, astate ) , astate )
else Ok astate else Ok astate
in in

@ -20,7 +20,9 @@ let check_addr_access location (address, history) astate =
let access_trace = Trace.Immediate {location; history} in let access_trace = Trace.Immediate {location; history} in
AddressAttributes.check_valid access_trace address astate AddressAttributes.check_valid access_trace address astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
(Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) ) ( Diagnostic.AccessToInvalidAddress
{calling_context= []; invalidation; invalidation_trace; access_trace}
, astate ) )
module Closures = struct module Closures = struct
@ -440,9 +442,9 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit
let apply callee_prepost ~f = let apply callee_prepost ~f =
PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals
~formals ~actuals astate ~formals ~actuals astate
>>| function >>= function
| None -> | None ->
(* couldn't apply pre/post pair *) None (* couldn't apply pre/post pair *) Ok None
| Some (post, return_val_opt) -> | Some (post, return_val_opt) ->
let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
let post = let post =
@ -452,17 +454,26 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit
| None -> | None ->
havoc_id (fst ret) [event] post havoc_id (fst ret) [event] post
in in
Some (f post) f post
in in
let open ExecutionDomain in let open ExecutionDomain in
match callee_exec_state with match callee_exec_state with
| AbortProgram _ -> | AbortProgram _ ->
(* Callee has failed; don't propagate the failure *) (* Callee has failed; propagate the fact that a failure happened. TODO: should only do so if
we can apply the precondition? *)
Ok (Some callee_exec_state) Ok (Some callee_exec_state)
| ContinueProgram astate -> | ContinueProgram astate ->
apply astate ~f:(fun astate -> ContinueProgram astate) apply astate ~f:(fun astate -> Ok (Some (ContinueProgram astate)))
| ExitProgram astate -> | ExitProgram astate ->
apply astate ~f:(fun astate -> ExitProgram astate) apply astate ~f:(fun astate -> Ok (Some (ExitProgram astate)))
| LatentAbortProgram {astate; latent_issue} ->
apply astate ~f:(fun astate ->
let latent_issue =
LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
in
if LatentIssue.should_report astate then
Error (LatentIssue.to_diagnostic latent_issue, astate)
else Ok (Some (LatentAbortProgram {astate; latent_issue})) )
let get_captured_actuals location ~captured_vars ~actual_closure astate = let get_captured_actuals location ~captured_vars ~actual_closure astate =

@ -385,3 +385,6 @@ let as_int phi v =
IList.force_until_first_some IList.force_until_first_some
[ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int) [ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int)
; lazy (Formula.as_int phi.formula v) ] ; lazy (Formula.as_int phi.formula v) ]
let has_no_assumptions phi = Formula.has_no_assumptions phi.formula

@ -61,3 +61,6 @@ val is_unsat_expensive : t -> t * bool
val as_int : t -> AbstractValue.t -> int option val as_int : t -> AbstractValue.t -> int option
(** [as_int phi t] returns an integer x such that [phi |- t = x], if known for sure; see also (** [as_int phi t] returns an integer x such that [phi |- t = x], if known for sure; see also
[is_known_zero] *) [is_known_zero] *)
val has_no_assumptions : t -> bool
(** whether the current path is independent of any calling context *)

@ -12,7 +12,7 @@ module ValueHistory = PulseValueHistory
type t = type t =
| Immediate of {location: Location.t; history: ValueHistory.t} | Immediate of {location: Location.t; history: ValueHistory.t}
| ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t} | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t}
[@@deriving compare] [@@deriving compare, equal]
let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location

@ -16,7 +16,7 @@ type t =
; location: Location.t (** location of the call event *) ; location: Location.t (** location of the call event *)
; history: ValueHistory.t (** the call involves a value with this prior history *) ; history: ValueHistory.t (** the call involves a value with this prior history *)
; in_call: t (** last step of the trace is in a call to [f] made at [location] *) } ; in_call: t (** last step of the trace is in a call to [f] made at [location] *) }
[@@deriving compare] [@@deriving compare, equal]
val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit

@ -19,7 +19,7 @@ type event =
| VariableAccessed of Pvar.t * Location.t | VariableAccessed of Pvar.t * Location.t
| VariableDeclared of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t
and t = event list [@@deriving compare] and t = event list [@@deriving compare, equal]
let pp_event_no_location fmt event = let pp_event_no_location fmt event =
let pp_pvar fmt pvar = let pp_pvar fmt pvar =

@ -19,7 +19,7 @@ type event =
| VariableAccessed of Pvar.t * Location.t | VariableAccessed of Pvar.t * Location.t
| VariableDeclared of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t
and t = event list [@@deriving compare] and t = event list [@@deriving compare, equal]
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit

@ -130,7 +130,10 @@ let%test_module "normalization" =
( module struct ( module struct
let%expect_test _ = let%expect_test _ =
normalize (x < y) ; normalize (x < y) ;
[%expect {|true (no var=var) && true (no linear) && {[x + -y] < 0}|}] [%expect
{|
known=true (no var=var) && true (no linear) && {[x + -y] < 0}, pruned=true (no atoms),
both=true (no var=var) && true (no linear) && {[x + -y] < 0}|}]
let%expect_test _ = let%expect_test _ =
normalize (x + i 1 - i 1 < x) ; normalize (x + i 1 - i 1 < x) ;
@ -160,7 +163,10 @@ let%test_module "normalization" =
let%expect_test _ = let%expect_test _ =
normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ; normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
[%expect {|true (no var=var) && x = 0 y = 1 v6 = 0 && true (no atoms)|}] [%expect
{|
known=true (no var=var) && x = 0 y = 1 v6 = 0 && true (no atoms), pruned=true (no atoms),
both=true (no var=var) && x = 0 y = 1 v6 = 0 && true (no atoms)|}]
let%expect_test _ = let%expect_test _ =
normalize (x = i 0 && x < i 0) ; normalize (x = i 0 && x < i 0) ;
@ -174,77 +180,131 @@ let%test_module "normalization" =
normalize (z * (x + (v * y) + i 1) / w = i 0) ; normalize (z * (x + (v * y) + i 1) / w = i 0) ;
[%expect [%expect
{| {|
true (no var=var) known=true (no var=var)
&& &&
x = -v6 + v8 -1 v7 = v8 -1 v10 = 0 x = -v6 + v8 -1 v7 = v8 -1 v10 = 0
&& &&
{0 = [v9]÷[w]}{[v6] = [v]×[y]}{[v9] = [z]×[v8]} |}] {0 = [v9]÷[w]}{[v6] = [v]×[y]}{[v9] = [z]×[v8]},
pruned=true (no atoms),
both=true (no var=var)
&&
x = -v6 + v8 -1 v7 = v8 -1 v10 = 0
&&
{0 = [v9]÷[w]}{[v6] = [v]×[y]}{[v9] = [z]×[v8]} |}]
(* check that this becomes all linear equalities *) (* check that this becomes all linear equalities *)
let%expect_test _ = let%expect_test _ =
normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ; normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ;
[%expect [%expect
{| {|
true (no var=var) known=true (no var=var)
&& &&
x = -v6 -1 y = 1/3·v6 v7 = -1 v8 = 0 v9 = 0 v10 = 0 x = -v6 -1 y = 1/3·v6 v7 = -1 v8 = 0 v9 = 0 v10 = 0
&& &&
true (no atoms)|}] true (no atoms),
pruned=true (no atoms),
both=true (no var=var)
&&
x = -v6 -1 y = 1/3·v6 v7 = -1 v8 = 0 v9 = 0 v10 = 0
&&
true (no atoms)|}]
(* check that this becomes all linear equalities thanks to constant propagation *) (* check that this becomes all linear equalities thanks to constant propagation *)
let%expect_test _ = let%expect_test _ =
normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ; normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ;
[%expect [%expect
{| {|
true (no var=var) known=true (no var=var)
&& &&
x = -v6 -1 y = 1/3·v6 z = 12 w = 7 v = 3 v7 = -1 x = -v6 -1 y = 1/3·v6 z = 12 w = 7 v = 3 v7 = -1
v8 = 0 v9 = 0 v10 = 0 v8 = 0 v9 = 0 v10 = 0
&& &&
true (no atoms)|}] true (no atoms),
pruned=true (no atoms),
both=true (no var=var)
&&
x = -v6 -1 y = 1/3·v6 z = 12 w = 7 v = 3 v7 = -1
v8 = 0 v9 = 0 v10 = 0
&&
true (no atoms)|}]
end ) end )
let%test_module "variable elimination" = let%test_module "variable elimination" =
( module struct ( module struct
let%expect_test _ = let%expect_test _ =
simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ; simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
[%expect {|true (no var=var) && x = 0 && true (no atoms)|}] [%expect
{|
known=true (no var=var) && x = 0 && true (no atoms), pruned=true (no atoms),
both=true (no var=var) && x = 0 && true (no atoms)|}]
let%expect_test _ = let%expect_test _ =
simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ; simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
[%expect {|x=v6 && x = 0 && true (no atoms)|}] [%expect
{|
known=x=v6 && x = 0 && true (no atoms), pruned=true (no atoms),
both=x=v6 && x = 0 && true (no atoms)|}]
let%expect_test _ = let%expect_test _ =
simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ; simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
[%expect {|true (no var=var) && y = -1 && true (no atoms)|}] [%expect
{|
known=true (no var=var) && y = -1 && true (no atoms), pruned=true (no atoms),
both=true (no var=var) && y = -1 && true (no atoms)|}]
(* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *) (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *)
let%expect_test _ = let%expect_test _ =
simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ; simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ;
[%expect {|x=v6 z=w=v7 && x = y -1 z = -1 && true (no atoms)|}] [%expect
{|
known=x=v6 z=w=v7 && x = y -1 z = -1 && true (no atoms), pruned=true (no atoms),
both=x=v6 z=w=v7 && x = y -1 z = -1 && true (no atoms)|}]
let%expect_test _ = let%expect_test _ =
simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ; simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
[%expect [%expect
{|x=v6 v=v9 && x = -v + v7 +1 y = -v7 z = -v + 2·v7 +1 w = v -1 && true (no atoms)|}] {|
known=x=v6 v=v9
&&
x = -v + v7 +1 y = -v7 z = -v + 2·v7 +1 w = v -1
&&
true (no atoms),
pruned=true (no atoms),
both=x=v6 v=v9
&&
x = -v + v7 +1 y = -v7 z = -v + 2·v7 +1 w = v -1
&&
true (no atoms)|}]
let%expect_test _ = let%expect_test _ =
simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ; simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
[%expect {|x=w=v6 y=z && x = y +4 && true (no atoms)|}] [%expect
{|
known=x=w=v6 y=z && x = y +4 && true (no atoms), pruned=true (no atoms),
both=x=w=v6 y=z && x = y +4 && true (no atoms)|}]
end ) end )
let%test_module "non-linear simplifications" = let%test_module "non-linear simplifications" =
( module struct ( module struct
let%expect_test "zero propagation" = let%expect_test "zero propagation" =
simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ; simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ;
[%expect {|true (no var=var) && w = 0 && true (no atoms)|}] [%expect
{|
known=true (no var=var) && w = 0 && true (no atoms), pruned=true (no atoms),
both=true (no var=var) && w = 0 && true (no atoms)|}]
let%expect_test "constant propagation: bitshift" = let%expect_test "constant propagation: bitshift" =
simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ; simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ;
[%expect {|true (no var=var) && x = 4 && true (no atoms)|}] [%expect
{|
known=true (no var=var) && x = 4 && true (no atoms), pruned=true (no atoms),
both=true (no var=var) && x = 4 && true (no atoms)|}]
let%expect_test "non-linear becomes linear" = let%expect_test "non-linear becomes linear" =
normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ; normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ;
[%expect [%expect
{|z=v8 w=v7 && x = 1/4·v6 y = 2 z = 1/2·v6 w = v6 -3 && true (no atoms)|}] {|
known=z=v8 w=v7 && x = 1/4·v6 y = 2 z = 1/2·v6 w = v6 -3 && true (no atoms),
pruned=true (no atoms),
both=z=v8 w=v7 && x = 1/4·v6 y = 2 z = 1/2·v6 w = v6 -3 && true (no atoms)|}]
end ) end )

@ -7,7 +7,8 @@ TESTS_DIR = ../../..
# see explanations in cpp/biabduction/Makefile for the custom isystem # see explanations in cpp/biabduction/Makefile for the custom isystem
CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
--pulse-report-latent-issues
INFERPRINT_OPTIONS = --issues-tests INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.cpp) SOURCES = $(wildcard *.cpp)

@ -28,7 +28,11 @@ void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
// should be FN given the current "all allocated addresses are assumed // should be FN given the current "all allocated addresses are assumed
// disjoint unless specified otherwise" but we detect the bug because // disjoint unless specified otherwise" but we detect the bug because
// we don't propagate pure equalities that we discover to the heap part // we don't propagate pure equalities that we discover to the heap part
void alias_null_deref_bad(int* x, int* y) { //
// Well, at the moment it *is* FN but because we mark the issue
// "latent" because the "if" test is not conclusively true. This is
// also ok.
void alias_null_deref_latent(int* x, int* y) {
*x = 32; *x = 32;
*y = 52; *y = 52;
if (x == y) { if (x == y) {

@ -53,7 +53,7 @@ void aggregate_reassign3_ok() {
} }
} }
int multiple_invalidations_branch_bad(int n, int* ptr) { int multiple_invalidations_branch_latent(int n, int* ptr) {
if (n == 7) { if (n == 7) {
delete ptr; delete ptr;
} else { } else {
@ -62,7 +62,7 @@ int multiple_invalidations_branch_bad(int n, int* ptr) {
return *ptr; return *ptr;
} }
int multiple_invalidations_loop_bad(int n, int* ptr) { int multiple_invalidations_loop_latent(int n, int* ptr) {
for (int i = 0; i < n; i++) { for (int i = 0; i < n; i++) {
if (i == 7) { if (i == 7) {
delete ptr; delete ptr;

@ -79,7 +79,7 @@ void add_test2_ok(int* x, int y, int z) {
} }
} }
void add_test3_bad(int* x, int y, int z) { void add_test3_latent(int* x, int y, int z) {
free(x); free(x);
if (y > 2 && y + z > 5) { // sometimes true if (y > 2 && y + z > 5) { // sometimes true
*x = 42; *x = 42;
@ -95,7 +95,7 @@ void add_test4_bad_FN(int* x) {
*x = 42; *x = 42;
} }
void add_test5_bad(int* x, int n) { void add_test5_latent(int* x, int n) {
free(x); free(x);
// the unknown bound is treated non-deterministically, good thing here // the unknown bound is treated non-deterministically, good thing here
for (int i = 0; i < n; i++) { for (int i = 0; i < n; i++) {

@ -26,4 +26,4 @@ void store_exit(int* x, bool b) {
} }
} }
void store_exit_null_bad(bool b) { store_exit(NULL, b); } void store_exit_null_bad() { store_exit(NULL, true); }

@ -1,11 +1,11 @@
codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_latent, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime 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, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,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` declared 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` declared 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/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` declared 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` declared 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_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,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_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,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_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, 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,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 `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, 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,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 `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, 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,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 `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, 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,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 `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here]
codetoanalyze/cpp/pulse/closures.cpp, call_std_fun_constructor_bad, 5, 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,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 `call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator()` here,parameter `s` of call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator(),invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_std_fun_constructor_bad, 5, 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,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 `call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator()` here,parameter `s` of call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator(),invalid access occurs here]
@ -23,8 +23,8 @@ codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_ref_bad, 7, NULLPTR_DERE
codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,use-after-lifetime 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/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,use-after-lifetime 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/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,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_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,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] 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]
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] 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]
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<_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]
@ -39,8 +39,9 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_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, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_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, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_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, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_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, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` 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 `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` 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 `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,invalid access occurs here] 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_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,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, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime 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, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime 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, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime 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, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
@ -50,6 +51,8 @@ codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_b
codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, 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 folly::None,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::Optional(arg)` (modelled),return from call to `folly::Optional::Optional(arg)` (modelled),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, 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 folly::None,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::Optional(arg)` (modelled),return from call to `folly::Optional::Optional(arg)` (modelled),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, 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 folly::None,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::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, 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 folly::None,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::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, 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 folly::None,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),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional<State>::operator->`,return from call to `folly::Optional<State>::operator->`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, 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 folly::None,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),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional<State>::operator->`,return from call to `folly::Optional<State>::operator->`,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`,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,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 ***,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,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,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from 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,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,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,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from 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,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,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,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument 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,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,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument 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]
@ -71,12 +74,12 @@ codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_
codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here] codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here]
codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, 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,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts 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 `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 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,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 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,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,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 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,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 `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 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,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 `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 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,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 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,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,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 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,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 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,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,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, 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,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 `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_latent, 4, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts 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 `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, 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,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, 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,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,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, 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,passed as argument to `<placement new>()` (modelled),return from call to `<placement new>()` (modelled),assigned,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,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, 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,passed as argument to `<placement new>()` (modelled),return from call to `<placement new>()` (modelled),assigned,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,invalid access occurs here]
@ -94,7 +97,7 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AF
codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_ok, 7, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
@ -104,13 +107,13 @@ codetoanalyze/cpp/pulse/vector.cpp, deref_vector_pointer_element_after_push_back
codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_latent, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_latent, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_next_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_next_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_read_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_read_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_bad, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_latent, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_latent,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_prev_after_emplace_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_prev_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_prev_after_emplace_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_prev_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]

@ -22,7 +22,7 @@ struct list {
struct foo* foo; struct foo* foo;
}; };
int invalidate_node_alias_bad(struct list* head, int cond) { int invalidate_node_alias_latent(struct list* head, int cond) {
int* result = 0; int* result = 0;
struct list* x = head; struct list* x = head;
if (cond) { if (cond) {
@ -37,6 +37,10 @@ int invalidate_node_alias_bad(struct list* head, int cond) {
return *result; return *result;
} }
int invalidate_node_alias_bad(struct list* head) {
invalidate_node_alias_latent(head, true);
}
void list_delete_ok(struct list** l) { void list_delete_ok(struct list** l) {
auto head = *l; auto head = *l;
*l = nullptr; *l = nullptr;

@ -0,0 +1,22 @@
/*
* 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.
*/
int* may_return_null(int x) {
if (x == 42) {
return nullptr;
}
return new int();
}
void only_bad_on_42_latent(int x) {
int* p = may_return_null(x);
*p = 12;
}
void faulty_call_bad() { only_bad_on_42_latent(42); }
void call_not_with_42_ok() { only_bad_on_42_latent(41); }

@ -52,7 +52,7 @@ void double_delete_bad() {
delete s; delete s;
} }
void delete_in_branch_bad(bool b) { void delete_in_branch_latent(bool b) {
auto s = new Simple{1}; auto s = new Simple{1};
if (b) { if (b) {
delete s; delete s;
@ -69,7 +69,7 @@ void delete_in_branch_ok(bool b) {
} }
} }
void use_in_branch_bad(bool b) { void use_in_branch_latent(bool b) {
auto s = new Simple{1}; auto s = new Simple{1};
delete s; delete s;
if (b) { if (b) {

@ -71,16 +71,17 @@ void reserve_then_push_back_loop_ok(std::vector<int>& vec,
std::cout << *elt << "\n"; std::cout << *elt << "\n";
} }
void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) { void FP_init_fill_then_push_back_ok(std::vector<int>& vec_other) {
std::vector<int> vec(vec_other.size()); std::vector<int> vec(vec_other.size());
int* elt = &vec[1]; int* elt = &vec[1];
for (const auto& i : vec_other) { vec.push_back(0);
vec.push_back(i); vec.push_back(0);
} vec.push_back(0);
vec.push_back(0);
std::cout << *elt << "\n"; std::cout << *elt << "\n";
} }
void push_back_loop_bad(std::vector<int>& vec_other) { void push_back_loop_latent(std::vector<int>& vec_other) {
std::vector<int> vec(2); std::vector<int> vec(2);
int* elt = &vec[1]; int* elt = &vec[1];
for (const auto& i : vec_other) { for (const auto& i : vec_other) {

@ -36,7 +36,7 @@ void read_iterator_loop_ok(std::vector<int>& vec) {
} }
} }
void iterator_next_after_emplace_loop_bad(std::vector<int>& vec) { void iterator_next_after_emplace_loop_latent(std::vector<int>& vec) {
int sum = 0; int sum = 0;
for (auto iter = vec.begin(); iter != vec.end(); ++iter) { for (auto iter = vec.begin(); iter != vec.end(); ++iter) {
int elem = *iter; int elem = *iter;
@ -46,7 +46,7 @@ void iterator_next_after_emplace_loop_bad(std::vector<int>& vec) {
} }
} }
void iterator_after_push_back_loop_bad(std::vector<int>& vec_other) { void iterator_after_push_back_loop_latent(std::vector<int>& vec_other) {
std::vector<int> vec(2); std::vector<int> vec(2);
auto iter_begin = vec.begin(); auto iter_begin = vec.begin();
auto iter_end = vec.end(); auto iter_end = vec.end();

@ -45,7 +45,7 @@ public class DefaultInInterface {
} }
} }
static void uncertainCallMethod1NPE(int i) { static void uncertainCallMethod1NPE_latent(int i) {
A aAorB = new A(); A aAorB = new A();
if (i > 0) { // feasible path if (i > 0) { // feasible path
aAorB = new B(); aAorB = new B();

@ -5,7 +5,7 @@
TESTS_DIR = ../../.. TESTS_DIR = ../../..
INFER_OPTIONS = --pulse-only --debug-exceptions INFER_OPTIONS = --pulse-only --debug-exceptions --pulse-report-latent-issues
INFERPRINT_OPTIONS = --issues-tests INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java) SOURCES = $(wildcard *.java)

@ -1,6 +1,6 @@
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE_latent(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Supertype.bar()`,return from call to `Object DynamicDispatch$Supertype.bar()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Supertype.bar()`,return from call to `Object DynamicDispatch$Supertype.bar()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]

Loading…
Cancel
Save