[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

@@ -16,6 +16,8 @@ end
 
 open! Types
 
+exception Stop_analysis
+
 module type S = sig
   type astate
 

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

infer/src/absint/AbstractInterpreter.ml

@@ -140,7 +140,10 @@ 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 ->
+          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 ;

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

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
 

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