From a295d26f694078a692ca752ec8100f212fb2857f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 22 Oct 2018 07:58:53 -0700 Subject: [PATCH] [pulse] do not propagate states with errors Summary: Instead of propagating a partial state give up the analysis of the function entirely on error. The state after an error is mostly non-sensical so until we know better just giving up makes sure the analysis remains sensible and produce fewer spurious warnings. Reviewed By: mbouaziz Differential Revision: D10483979 fbshipit-source-id: 171ec8469 --- infer/src/absint/AbstractDomain.ml | 2 ++ infer/src/absint/AbstractDomain.mli | 4 ++++ infer/src/absint/AbstractInterpreter.ml | 13 ++++++++----- infer/src/checkers/Pulse.ml | 10 +++++++--- infer/src/checkers/PulseDomain.ml | 5 ++--- infer/src/checkers/PulseDomain.mli | 2 +- 6 files changed, 24 insertions(+), 12 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 8f7426233..af4269cec 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -16,6 +16,8 @@ end open! Types +exception Stop_analysis + module type S = sig type astate diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index fdc317830..0c9021ac5 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -16,6 +16,10 @@ end open! Types +(** This exception can be raised by abstract interpreters to stop the analysis early without + triggering further errors. Clients who raise this exception should catch it eventually. *) +exception Stop_analysis + (** Abstract domains and domain combinators *) module type S = sig diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index a2949b285..c14fca8a7 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -140,11 +140,14 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s (* don't forget to reset this so we output messages for future errors too *) logged_error := false ; post - with exn -> - IExn.reraise_after exn ~f:(fun () -> - if not !logged_error then ( - L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ; - logged_error := true ) ) + with + | AbstractDomain.Stop_analysis as exn -> + raise_notrace exn + | exn -> + IExn.reraise_after exn ~f:(fun () -> + if not !logged_error then ( + L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ; + logged_error := true ) ) in Instrs.fold ~f:compute_post ~init:pre instrs in diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 5bb1f4454..30d02b0ed 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -17,8 +17,11 @@ let report summary diagnostic = let check_error summary = function | Ok astate -> astate - | Error (astate, diagnostic) -> - report summary diagnostic ; astate + | Error diagnostic -> + report summary diagnostic ; + (* We can also continue the analysis by returning {!PulseDomain.initial} here but there might + be a risk we would get nonsense. This seems safer for now but TODO. *) + raise_notrace AbstractDomain.Stop_analysis module TransferFunctions (CFG : ProcCfg.S) = struct @@ -70,5 +73,6 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (Transf let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in - ignore (Analyzer.compute_post proc_data ~initial:PulseDomain.initial) ; + ( try ignore (Analyzer.compute_post proc_data ~initial:PulseDomain.initial) + with AbstractDomain.Stop_analysis -> () ) ; summary diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index b3f23e84f..e38021bf4 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -188,14 +188,13 @@ module Diagnostic = struct let get_issue_type (AccessToInvalidAddress _) = IssueType.use_after_lifetime end -type 'a access_result = ('a, t * Diagnostic.t) result +type 'a access_result = ('a, Diagnostic.t) result (** Check that the address is not known to be invalid *) let check_addr_access actor address astate = match InvalidAddressesDomain.get_invalidation address astate.invalids with | Some invalidated_at -> - Error - (astate, Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address}) + Error (Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address}) | None -> Ok astate diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 06036b57c..81542e40e 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -58,7 +58,7 @@ module Diagnostic : sig val get_trace : t -> Errlog.loc_trace end -type 'a access_result = ('a, t * Diagnostic.t) result +type 'a access_result = ('a, Diagnostic.t) result val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) access_result