From 7fdb33b710416eb29ab278c92dea828b94b60603 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 2 Oct 2020 07:26:03 -0700 Subject: [PATCH] [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 --- infer/man/man1/infer-full.txt | 6 + infer/src/IR/IntLit.ml | 2 + infer/src/IR/IntLit.mli | 3 + infer/src/IR/Pvar.ml | 2 +- infer/src/IR/Pvar.mli | 2 +- infer/src/IR/Sil.ml | 2 +- infer/src/IR/Sil.mli | 2 +- infer/src/base/Config.ml | 8 + infer/src/base/Config.mli | 2 + infer/src/checkers/impurity.ml | 2 +- infer/src/pulse/Pulse.ml | 45 +- infer/src/pulse/PulseArithmetic.ml | 4 + infer/src/pulse/PulseArithmetic.mli | 2 + infer/src/pulse/PulseCallEvent.ml | 2 +- infer/src/pulse/PulseCallEvent.mli | 2 +- infer/src/pulse/PulseDiagnostic.ml | 53 +- infer/src/pulse/PulseDiagnostic.mli | 18 +- infer/src/pulse/PulseDomainInterface.ml | 2 + infer/src/pulse/PulseExecutionDomain.ml | 21 +- infer/src/pulse/PulseExecutionDomain.mli | 14 +- infer/src/pulse/PulseFormula.ml | 650 ++++++++++-------- infer/src/pulse/PulseFormula.mli | 2 + infer/src/pulse/PulseInterproc.ml | 2 +- infer/src/pulse/PulseInvalidation.ml | 6 +- infer/src/pulse/PulseInvalidation.mli | 5 +- infer/src/pulse/PulseLatentIssue.ml | 32 + infer/src/pulse/PulseLatentIssue.mli | 24 + infer/src/pulse/PulseModels.ml | 2 +- infer/src/pulse/PulseOperations.ml | 25 +- infer/src/pulse/PulsePathCondition.ml | 3 + infer/src/pulse/PulsePathCondition.mli | 3 + infer/src/pulse/PulseTrace.ml | 2 +- infer/src/pulse/PulseTrace.mli | 2 +- infer/src/pulse/PulseValueHistory.ml | 2 +- infer/src/pulse/PulseValueHistory.mli | 2 +- infer/src/pulse/unit/PulseFormulaTest.ml | 114 ++- infer/tests/codetoanalyze/cpp/pulse/Makefile | 3 +- .../codetoanalyze/cpp/pulse/aliasing.cpp | 6 +- .../tests/codetoanalyze/cpp/pulse/basics.cpp | 4 +- .../codetoanalyze/cpp/pulse/conditionals.cpp | 4 +- .../codetoanalyze/cpp/pulse/exit_test.cpp | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 33 +- infer/tests/codetoanalyze/cpp/pulse/join.cpp | 6 +- infer/tests/codetoanalyze/cpp/pulse/path.cpp | 22 + .../cpp/pulse/use_after_delete.cpp | 4 +- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 11 +- .../cpp/pulse/vector_iterator.cpp | 4 +- .../java/pulse/DefaultInInterface.java | 2 +- infer/tests/codetoanalyze/java/pulse/Makefile | 2 +- .../tests/codetoanalyze/java/pulse/issues.exp | 2 +- 50 files changed, 783 insertions(+), 392 deletions(-) create mode 100644 infer/src/pulse/PulseLatentIssue.ml create mode 100644 infer/src/pulse/PulseLatentIssue.mli create mode 100644 infer/tests/codetoanalyze/cpp/pulse/path.cpp diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index de7e20f7d..0757dac31 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1731,6 +1731,12 @@ INTERNAL OPTIONS Maximum number of array elements and structure fields to keep 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 Under-approximate after int loop iterations diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index 6420009b9..6ab2a8e51 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -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 to_string i = F.asprintf "%a" pp i + +let equal i1 i2 = eq i1 i2 diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli index f5d277e0a..9468b4872 100644 --- a/infer/src/IR/IntLit.mli +++ b/infer/src/IR/IntLit.mli @@ -27,6 +27,9 @@ val div : t -> t -> t val eq : t -> t -> bool +val equal : t -> t -> bool +(** an alias for {!eq}, for convenience *) + val of_int : int -> t val of_big_int : Z.t -> t [@@warning "-32"] diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index 308097782..45d5913f5 100644 --- a/infer/src/IR/Pvar.ml +++ b/infer/src/IR/Pvar.ml @@ -332,6 +332,6 @@ module Set = PrettyPrintable.MakePPSet (struct let pp = pp Pp.text 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" diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index a214483c8..11674f5b3 100644 --- a/infer/src/IR/Pvar.mli +++ b/infer/src/IR/Pvar.mli @@ -174,6 +174,6 @@ val rename : f:(string -> string) -> t -> t (** Sets of pvars. *) 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 diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index f848a36ad..116fed58f 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -23,7 +23,7 @@ type if_kind = | Ik_land_lor (** obtained from translation of && or || *) | Ik_while | Ik_switch -[@@deriving compare] +[@@deriving compare, equal] type instr_metadata = | Abstract of Location.t diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index dcabb35b8..4221d5d27 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -22,7 +22,7 @@ type if_kind = | Ik_land_lor (** obtained from translation of && or || *) | Ik_while | Ik_switch -[@@deriving compare] +[@@deriving compare, equal] type instr_metadata = | Abstract of Location.t diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index efc6844a3..1764f8f79 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1881,6 +1881,12 @@ and pulse_model_transfer_ownership = 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 = CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3 "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 +and pulse_report_latent_issues = !pulse_report_latent_issues + and pulse_widen_threshold = !pulse_widen_threshold and pure_by_default = !pure_by_default diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4203bd309..6f83ab8f7 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -469,6 +469,8 @@ val pulse_model_transfer_ownership_namespace : (string * string) list val pulse_model_transfer_ownership : string list +val pulse_report_latent_issues : bool + val pulse_widen_threshold : int val pure_by_default : bool diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index aa2cff7ac..ffc3acbf4 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -142,7 +142,7 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai match exec_state with | ExitProgram astate -> (astate, true) - | AbortProgram astate | ContinueProgram astate -> + | AbortProgram astate | ContinueProgram astate | LatentAbortProgram {astate} -> (astate, false) in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 31b8f0ac4..be78f3962 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -12,21 +12,40 @@ open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface -let report {InterproceduralAnalysis.proc_desc; err_log} diagnostic = +let report ?(extra_trace = []) proc_desc err_log diagnostic = 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) -let check_error_transform analysis_data ~f = function +let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = function | Ok astate -> f astate - | Error (diagnostic, astate) -> + | Error (diagnostic, astate) -> ( let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in if is_unsat then [] - else ( - report analysis_data diagnostic ; - [ExecutionDomain.AbortProgram astate] ) + else + let astate = AbductiveDomain.of_post proc_desc astate in + 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 = @@ -83,14 +102,14 @@ module PulseTransferFunctions = struct (** [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 = - match exec_state with - | ExecutionDomain.ContinueProgram astate -> + match (exec_state : ExecutionDomain.t) with + | ContinueProgram astate -> 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 (* invalidate [&x] *) PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue - | ExecutionDomain.AbortProgram _ | ExecutionDomain.ExitProgram _ -> + | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> Ok exec_state @@ -183,7 +202,7 @@ module PulseTransferFunctions = struct ~f:(fun astates (astate : Domain.t) -> let astate = match astate with - | AbortProgram _ | ExitProgram _ -> + | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> [astate] | ContinueProgram 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) _cfg_node (instr : Sil.instr) : Domain.t list = match astate with - | AbortProgram _ -> + | AbortProgram _ | LatentAbortProgram _ -> (* We can also continue the analysis with the error state here but there might be a risk we would get nonsense. *) [astate] @@ -258,7 +277,7 @@ module PulseTransferFunctions = struct List.fold ~f:(fun astates (astate : Domain.t) -> match astate with - | AbortProgram _ | ExitProgram _ -> + | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> [astate] | ContinueProgram astate -> let astate = diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 2f6dc24a3..105a622bc 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -52,3 +52,7 @@ let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain. let is_unsat_expensive astate = let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in (AbductiveDomain.set_path_condition phi' astate, is_unsat) + + +let has_no_assumptions astate = + PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 0d5e440ac..1c986714f 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -35,3 +35,5 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool val is_unsat_cheap : AbductiveDomain.t -> bool val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool + +val has_no_assumptions : AbductiveDomain.t -> bool diff --git a/infer/src/pulse/PulseCallEvent.ml b/infer/src/pulse/PulseCallEvent.ml index cf423a756..8aad844b3 100644 --- a/infer/src/pulse/PulseCallEvent.ml +++ b/infer/src/pulse/PulseCallEvent.ml @@ -12,7 +12,7 @@ type t = | Model of string | SkippedKnownCall of Procname.t | SkippedUnknownCall of Exp.t -[@@deriving compare] +[@@deriving compare, equal] let pp_config ~verbose fmt = let pp_proc_name = if verbose then Procname.pp else Procname.describe in diff --git a/infer/src/pulse/PulseCallEvent.mli b/infer/src/pulse/PulseCallEvent.mli index ad6b37ab3..a3fc36be9 100644 --- a/infer/src/pulse/PulseCallEvent.mli +++ b/infer/src/pulse/PulseCallEvent.mli @@ -13,7 +13,7 @@ type t = | Model of string (** hardcoded model *) | SkippedKnownCall of Procname.t (** known function without summary *) | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) -[@@deriving compare] +[@@deriving compare, equal] val pp : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 538bd6181..05277d50e 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -12,21 +12,30 @@ module Invalidation = PulseInvalidation module Trace = PulseTrace 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 = - | AccessToInvalidAddress of - {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} + | AccessToInvalidAddress of access_to_invalid_address | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} +[@@deriving equal] let get_location = function - | AccessToInvalidAddress {access_trace} -> + | AccessToInvalidAddress {calling_context= []; 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} -> location 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: 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 "`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) = - match trace with - | Immediate _ -> + match immediate_or_first_call calling_context trace with + | `Immediate -> F.fprintf fmt "accessing memory that " - | ViaCall {f; _} -> + | `Call f -> F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f in let pp_invalidation_trace line invalidation fmt (trace : Trace.t) = let pp_line fmt line = F.fprintf fmt " on line %d" line in - match trace with - | Immediate _ -> + match immediate_or_first_call calling_context trace with + | `Immediate -> 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 pp_line line CallEvent.describe f in @@ -97,7 +114,21 @@ let add_errlog_header ~title location errlog = 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 add_errlog_header ~title:"invalidation part of the trace starts here" start_location @@ Trace.add_to_errlog ~nesting:1 diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index ef5952e7d..eda012f90 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -6,16 +6,30 @@ *) open! IStd +module CallEvent = PulseCallEvent module Invalidation = PulseInvalidation module Trace = PulseTrace 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 *) type t = - | AccessToInvalidAddress of - {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} + | AccessToInvalidAddress of access_to_invalid_address | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} +[@@deriving equal] val get_message : t -> string diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml index 97e5dde9f..d49e9c972 100644 --- a/infer/src/pulse/PulseDomainInterface.ml +++ b/infer/src/pulse/PulseDomainInterface.ml @@ -21,6 +21,7 @@ module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory module BaseAddressAttributes = PulseBaseAddressAttributes +module LatentIssue = PulseLatentIssue (** {2 Enforce short form usage} *) @@ -36,4 +37,5 @@ include struct [@@deprecated "use the short form BaseAddressAttributes instead"] module PulseExecutionDomain = PulseExecutionDomain [@@deprecated "use the short form ExecutionDomain instead"] + module PulseLatentIssue = PulseLatentIssue [@@deprecated "use the short form LatentIssue instead"] end diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 2b8428d7d..b09e6eb09 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -8,12 +8,15 @@ open! IStd module F = Format module L = Logging +open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain +module LatentIssue = PulseLatentIssue type t = | AbortProgram of AbductiveDomain.t | ContinueProgram of AbductiveDomain.t | ExitProgram of AbductiveDomain.t + | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t} let continue astate = ContinueProgram astate @@ -25,6 +28,9 @@ let leq ~lhs ~rhs = | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram 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 @@ -36,6 +42,12 @@ let pp fmt = function F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate | AbortProgram 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 = @@ -46,11 +58,18 @@ let map ~f exec_state = ContinueProgram (f astate) | ExitProgram astate -> ExitProgram (f astate) + | LatentAbortProgram {astate; latent_issue} -> + LatentAbortProgram {astate= f astate; latent_issue} let of_posts pdesc posts = 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 ; let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in if is_unsat then None diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 446a9210d..9d4791db8 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -4,18 +4,22 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd +module AbductiveDomain = PulseAbductiveDomain +module LatentIssue = PulseLatentIssue type t = - | AbortProgram of PulseAbductiveDomain.t + | AbortProgram of AbductiveDomain.t (** represents the state at the program point that caused an error *) - | ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) - | ExitProgram of PulseAbductiveDomain.t - (** represents the state originating at exit/divergence. *) + | ContinueProgram of AbductiveDomain.t (** represents the state at the program point *) + | ExitProgram of AbductiveDomain.t (** 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 -val continue : PulseAbductiveDomain.t -> t +val continue : AbductiveDomain.t -> t val of_posts : Procdesc.t -> t list -> t list diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index b3525cffa..4bac45ca4 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -925,9 +925,19 @@ module Atom = struct Term.has_var_notin vars t1 || Term.has_var_notin vars t2 - module Set = Caml.Set.Make (struct - type nonrec t = t [@@deriving compare] - end) + module Set = struct + include Caml.Set.Make (struct + 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 module SatUnsatMonad = struct @@ -957,267 +967,293 @@ module VarUF = end) (Var.Set) -type t = - { var_eqs: VarUF.t (** equality relation between variables *) - ; linear_eqs: LinArith.t Var.Map.t - (** 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] *) } +module Formula = struct + type t = + { var_eqs: VarUF.t (** equality relation between variables *) + ; linear_eqs: LinArith.t Var.Map.t + (** 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_linear_eqs fmt m = - if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)" - else - Pp.collection ~sep:" ∧ " - ~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) - fmt m - in - let pp_atoms fmt atoms = - if Atom.Set.is_empty atoms then F.pp_print_string fmt "true (no atoms)" - else - 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 "@[%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_with_pp_var pp_var fmt phi = + let pp_linear_eqs fmt m = + if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)" + else + Pp.collection ~sep:" ∧ " + ~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) + fmt m + in + F.fprintf fmt "@[%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 (Atom.Set.pp_with_pp_var pp_var) 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 *) -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_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 -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 normalize : t -> t normalized + 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 = - 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 ) + (** 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). - (** an arbitrary value *) - let base_fuel = 5 + 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). - 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 = - 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 + (** 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 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 + VarSubst repr + | Some l' -> + LinSubst l' ) - (** 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 rec solve_normalized_eq ~fuel l1 l2 phi = + 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 ) + + + (** 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 +(** 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 = - 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 @@ -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_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 = - 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 open SatUnsatMonad in let tx = Term.of_operand x in let ty = Term.of_operand y 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 - 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] *) 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) = match norm with Unsat -> raise Contradiction | Sat x -> x in - let and_var_eqs acc = - VarUF.fold_congruences phi_foreign.var_eqs ~init:acc + let and_var_eqs var_eqs_foreign acc_phi = + VarUF.fold_congruences var_eqs_foreign ~init:acc_phi ~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) -> 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) ~f:(fun (acc_f, phi) v_foreign -> 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) ) ) in - let and_linear_eqs acc = - IContainer.fold_of_pervasives_map_fold Var.Map.fold phi_foreign.linear_eqs ~init:acc + let and_linear_eqs linear_eqs_foreign acc_phi = + IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi ~f:(fun (acc_f, phi) (v_foreign, l_foreign) -> 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 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) ) in - let and_atoms acc = - IContainer.fold_of_pervasives_set_fold Atom.Set.fold phi_foreign.atoms ~init:acc + let and_atoms atoms_foreign acc_phi = + IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi ~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 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) ) 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 @@ -1310,14 +1397,14 @@ let build_var_graph phi = in Var.Set.iter (fun v -> add_set graph v vs) vs in - Container.iter ~fold:VarUF.fold_congruences phi.var_eqs ~f:(fun ((repr : VarUF.repr), vs) -> - add_all (Var.Set.add (repr :> Var.t) vs) ) ; + Container.iter ~fold:VarUF.fold_congruences phi.Formula.var_eqs + ~f:(fun ((repr : VarUF.repr), vs) -> add_all (Var.Set.add (repr :> Var.t) vs)) ; Var.Map.iter (fun v l -> LinArith.get_variables l |> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v) |> 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 the number of variables of these terms) *) let add_from_terms t1 t2 = @@ -1331,7 +1418,7 @@ let build_var_graph phi = (fun atom -> let t1, t2 = Atom.get_terms atom in add_from_terms t1 t2 ) - phi.atoms ; + phi.Formula.atoms ; graph @@ -1364,31 +1451,50 @@ let get_reachable_from graph vs = let simplify ~keep phi = let open SatUnsatMonad 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 - 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 - variables in [keep] in the graph connecting two variables whenever they appear together in - a same atom of the formula. *) - let var_graph = build_var_graph phi in + 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 + variables in [keep] in the graph connecting two variables whenever they appear together in + a same atom of the formula. *) + (* 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 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 - to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive - closure on the graph above *) - let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.var_eqs in - let linear_eqs = Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.linear_eqs in - let atoms = Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep atom)) phi.atoms in - {var_eqs; linear_eqs; atoms} + to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive + closure on the graph above *) + let filter_atom atom = not (Atom.has_var_notin vars_to_keep atom) in + let simplify_phi phi = + let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.Formula.var_eqs in + 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 = - 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 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 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 + + +(** 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 diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 47bc9e3f8..2e5d73c38 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -58,6 +58,8 @@ val is_known_zero : t -> Var.t -> bool val as_int : t -> Var.t -> int option +val has_no_assumptions : t -> bool + (** {3 Notations} *) include sig diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 26178cc62..3a3171856 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -516,7 +516,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; ( Diagnostic.AccessToInvalidAddress - {invalidation; invalidation_trace; access_trace} + {calling_context= []; invalidation; invalidation_trace; access_trace} , astate ) ) ) ) call_state.subst (Ok call_state.astate) diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 114d6e918..a794be9db 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -16,7 +16,7 @@ type std_vector_function = | PushBack | Reserve | ShrinkToFit -[@@deriving compare] +[@@deriving compare, equal] let pp_std_vector_function f = function | Assign -> @@ -37,7 +37,7 @@ let pp_std_vector_function f = function 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" @@ -50,7 +50,7 @@ type t = | OptionalEmpty | StdVector of std_vector_function | JavaIterator of java_iterator_function -[@@deriving compare] +[@@deriving compare, equal] let issue_type_of_cause = function | CFree -> diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index e21065bc2..8fcdfbb5e 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -17,11 +17,10 @@ type std_vector_function = | PushBack | Reserve | ShrinkToFit -[@@deriving compare] 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 = | CFree @@ -32,7 +31,7 @@ type t = | OptionalEmpty | StdVector of std_vector_function | JavaIterator of java_iterator_function -[@@deriving compare] +[@@deriving compare, equal] val pp : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml new file mode 100644 index 000000000..69f5d02da --- /dev/null +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -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) diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli new file mode 100644 index 000000000..ce9aa378b --- /dev/null +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index a2023e1c9..18ab3aa98 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -554,7 +554,7 @@ module GenericArrayBackedCollectionIterator = struct let access_trace = Trace.Immediate {location; history= snd pointer} in Error ( Diagnostic.AccessToInvalidAddress - {invalidation= EndIterator; invalidation_trace; access_trace} + {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace} , astate ) else Ok astate in diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 309a4deb4..685fdf379 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -20,7 +20,9 @@ let check_addr_access location (address, history) astate = let access_trace = Trace.Immediate {location; history} in AddressAttributes.check_valid access_trace address astate |> 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 @@ -440,9 +442,9 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit let apply callee_prepost ~f = PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals ~formals ~actuals astate - >>| function + >>= function | None -> - (* couldn't apply pre/post pair *) None + (* couldn't apply pre/post pair *) Ok None | Some (post, return_val_opt) -> let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in let post = @@ -452,17 +454,26 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit | None -> havoc_id (fst ret) [event] post in - Some (f post) + f post in let open ExecutionDomain in match callee_exec_state with | 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) | ContinueProgram astate -> - apply astate ~f:(fun astate -> ContinueProgram astate) + apply astate ~f:(fun astate -> Ok (Some (ContinueProgram 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 = diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 0a5b25303..6a2afb4cc 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -385,3 +385,6 @@ let as_int phi v = IList.force_until_first_some [ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int) ; lazy (Formula.as_int phi.formula v) ] + + +let has_no_assumptions phi = Formula.has_no_assumptions phi.formula diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 160c0a925..b201612ae 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -61,3 +61,6 @@ val is_unsat_expensive : t -> t * bool 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 [is_known_zero] *) + +val has_no_assumptions : t -> bool +(** whether the current path is independent of any calling context *) diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index 1ae4fe6cd..2800fdf96 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -12,7 +12,7 @@ module ValueHistory = PulseValueHistory type t = | Immediate of {location: Location.t; history: ValueHistory.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 diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 5795a530b..ed67b71e7 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -16,7 +16,7 @@ type t = ; location: Location.t (** location of the call event *) ; 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] *) } -[@@deriving compare] +[@@deriving compare, equal] val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 3d9c94ecf..3d7c33b70 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -19,7 +19,7 @@ type event = | VariableAccessed 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_pvar fmt pvar = diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 56db0dc5e..84c12af0a 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -19,7 +19,7 @@ type event = | VariableAccessed 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 diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index bcf3fb964..67753dd45 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -130,7 +130,10 @@ let%test_module "normalization" = ( module struct let%expect_test _ = 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 _ = normalize (x + i 1 - i 1 < x) ; @@ -160,7 +163,10 @@ let%test_module "normalization" = let%expect_test _ = 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 _ = 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) ; [%expect {| - true (no var=var) - && - x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0 - && - {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}] + known=true (no var=var) + && + x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0 + && + {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 *) let%expect_test _ = normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ; [%expect {| - true (no var=var) - && - x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 - && - true (no atoms)|}] + known=true (no var=var) + && + x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 + && + 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 *) let%expect_test _ = normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ; [%expect {| - 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)|}] + known=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), + 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 ) let%test_module "variable elimination" = ( module struct let%expect_test _ = 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 _ = 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 _ = 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] *) let%expect_test _ = 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 _ = simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ; [%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 _ = 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 ) let%test_module "non-linear simplifications" = ( module struct let%expect_test "zero propagation" = 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" = 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" = normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ; [%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 ) diff --git a/infer/tests/codetoanalyze/cpp/pulse/Makefile b/infer/tests/codetoanalyze/cpp/pulse/Makefile index a479a7f50..fce546ad8 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/Makefile +++ b/infer/tests/codetoanalyze/cpp/pulse/Makefile @@ -7,7 +7,8 @@ TESTS_DIR = ../../.. # see explanations in cpp/biabduction/Makefile for the custom isystem 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 SOURCES = $(wildcard *.cpp) diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp index fc28c52e3..1121a6d0f 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.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 // disjoint unless specified otherwise" but we detect the bug because // 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; *y = 52; if (x == y) { diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp index d911a2a07..c64321908 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp @@ -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) { delete ptr; } else { @@ -62,7 +62,7 @@ int multiple_invalidations_branch_bad(int n, int* 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++) { if (i == 7) { delete ptr; diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp index 95e288ff1..bac6520c2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp @@ -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); if (y > 2 && y + z > 5) { // sometimes true *x = 42; @@ -95,7 +95,7 @@ void add_test4_bad_FN(int* x) { *x = 42; } -void add_test5_bad(int* x, int n) { +void add_test5_latent(int* x, int n) { free(x); // the unknown bound is treated non-deterministically, good thing here for (int i = 0; i < n; i++) { diff --git a/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp index 9b588dd71..0c75bfd62 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp @@ -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); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 980d1fe01..df3d5f4f3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -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_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/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_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_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_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_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] +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_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_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] @@ -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_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/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_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_test3_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_latent,invalid access occurs here] +codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_latent, 5, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test5_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_latent,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::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] @@ -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_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/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, 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_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, 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, 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_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::operator->`,return from call to `folly::Optional::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_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] @@ -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/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/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, 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, 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_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 `()` (modelled),return from call to `()` (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/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/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, 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] @@ -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_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, 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, 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_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_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_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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/join.cpp b/infer/tests/codetoanalyze/cpp/pulse/join.cpp index b980a3e62..d23744073 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/join.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/join.cpp @@ -22,7 +22,7 @@ struct list { 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; struct list* x = head; if (cond) { @@ -37,6 +37,10 @@ int invalidate_node_alias_bad(struct list* head, int cond) { return *result; } +int invalidate_node_alias_bad(struct list* head) { + invalidate_node_alias_latent(head, true); +} + void list_delete_ok(struct list** l) { auto head = *l; *l = nullptr; diff --git a/infer/tests/codetoanalyze/cpp/pulse/path.cpp b/infer/tests/codetoanalyze/cpp/pulse/path.cpp new file mode 100644 index 000000000..a634b6c68 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/path.cpp @@ -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); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp index 6cf1d9314..40cd22b24 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp @@ -52,7 +52,7 @@ void double_delete_bad() { delete s; } -void delete_in_branch_bad(bool b) { +void delete_in_branch_latent(bool b) { auto s = new Simple{1}; if (b) { 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}; delete s; if (b) { diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index ce2a95785..3a9dee0a6 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -71,16 +71,17 @@ void reserve_then_push_back_loop_ok(std::vector& vec, std::cout << *elt << "\n"; } -void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { +void FP_init_fill_then_push_back_ok(std::vector& vec_other) { std::vector vec(vec_other.size()); int* elt = &vec[1]; - for (const auto& i : vec_other) { - vec.push_back(i); - } + vec.push_back(0); + vec.push_back(0); + vec.push_back(0); + vec.push_back(0); std::cout << *elt << "\n"; } -void push_back_loop_bad(std::vector& vec_other) { +void push_back_loop_latent(std::vector& vec_other) { std::vector vec(2); int* elt = &vec[1]; for (const auto& i : vec_other) { diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp index 4e7955c3a..acdca06d0 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp @@ -36,7 +36,7 @@ void read_iterator_loop_ok(std::vector& vec) { } } -void iterator_next_after_emplace_loop_bad(std::vector& vec) { +void iterator_next_after_emplace_loop_latent(std::vector& vec) { int sum = 0; for (auto iter = vec.begin(); iter != vec.end(); ++iter) { int elem = *iter; @@ -46,7 +46,7 @@ void iterator_next_after_emplace_loop_bad(std::vector& vec) { } } -void iterator_after_push_back_loop_bad(std::vector& vec_other) { +void iterator_after_push_back_loop_latent(std::vector& vec_other) { std::vector vec(2); auto iter_begin = vec.begin(); auto iter_end = vec.end(); diff --git a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java index dd4352bbc..aae3123ea 100644 --- a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java +++ b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java @@ -45,7 +45,7 @@ public class DefaultInInterface { } } - static void uncertainCallMethod1NPE(int i) { + static void uncertainCallMethod1NPE_latent(int i) { A aAorB = new A(); if (i > 0) { // feasible path aAorB = new B(); diff --git a/infer/tests/codetoanalyze/java/pulse/Makefile b/infer/tests/codetoanalyze/java/pulse/Makefile index 636a8e4ba..e146b8265 100644 --- a/infer/tests/codetoanalyze/java/pulse/Makefile +++ b/infer/tests/codetoanalyze/java/pulse/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../.. -INFER_OPTIONS = --pulse-only --debug-exceptions +INFER_OPTIONS = --pulse-only --debug-exceptions --pulse-report-latent-issues INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 7509df621..c12072be8 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -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$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.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]