[pulse] add tracing of arithmetic facts

Summary:
When reporting null dereference it is useful to know where the null came
from.

Reviewed By: skcho

Differential Revision: D18206459

fbshipit-source-id: 0c8e6781b

infer/src/pulse/Pulse.ml

@@ -168,9 +168,10 @@ module PulseTransferFunctions = struct
               Ok astate
         in
         [check_error summary result]
-    | Prune (condition, loc, _is_then_branch, _if_kind) ->
+    | Prune (condition, loc, is_then_branch, if_kind) ->
         let post, cond_satisfiable =
-          PulseOperations.assert_is_true loc ~condition astate |> check_error summary
+          PulseOperations.prune ~is_then_branch if_kind loc ~condition astate
+          |> check_error summary
         in
         if cond_satisfiable then
           (* [condition] is true or unknown value: go into the branch *)

infer/src/pulse/PulseAbductiveDomain.ml

@@ -440,25 +440,41 @@ module PrePost = struct
 
   (* {3 reading the pre from the current state} *)
 
-  let solve_arithmetic_constraints ~addr_pre ~attrs_pre ~addr_hist_caller call_state =
+  let add_call_to_trace proc_name call_location caller_history in_call =
+    Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
+
+
+  let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
+      ~addr_hist_caller call_state =
     match Attributes.get_arithmetic attrs_pre with
     | None ->
         call_state
-    | Some _ as arith_callee -> (
-        let addr_caller = fst addr_hist_caller in
+    | Some (arith_callee, arith_callee_hist) -> (
+        let addr_caller, hist_caller = addr_hist_caller in
         let astate = call_state.astate in
-        let arith_caller = Memory.get_arithmetic addr_caller astate in
+        let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in
         (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes
            for that address in the post since abstract values are immutable *)
-        match Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee with
+        match
+          Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee)
+        with
         | Unsatisfiable ->
             raise
               (CannotApplyPre
-                 (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee}))
+                 (Arithmetic
+                    { addr_caller
+                    ; addr_callee= addr_pre
+                    ; arith_caller= arith_caller_opt
+                    ; arith_callee= Some arith_callee }))
         | Satisfiable (abduce_caller, _abduce_callee) ->
             let new_astate =
               Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller ->
-                  let attribute = Attribute.Arithmetic abduce_caller in
+                  let attribute =
+                    Attribute.Arithmetic
+                      ( abduce_caller
+                      , add_call_to_trace callee_proc_name call_location hist_caller
+                          arith_callee_hist )
+                  in
                   Memory.abduce_attribute addr_caller attribute astate
                   |> Memory.add_attribute addr_caller attribute )
             in
@@ -479,7 +495,8 @@ module PrePost = struct
           Ok call_state
       | Some (edges_pre, attrs_pre) ->
           let call_state =
-            solve_arithmetic_constraints ~addr_pre ~attrs_pre ~addr_hist_caller call_state
+            solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
+              ~addr_hist_caller call_state
           in
           Container.fold_result
             ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
@@ -610,14 +627,13 @@ module PrePost = struct
 
   let add_call_to_attr proc_name call_location caller_history attr =
     match (attr : Attribute.t) with
-    | Invalid (invalidation, in_call) ->
+    | Invalid (invalidation, trace) ->
         Attribute.Invalid
-          ( invalidation
-          , ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
-          )
+          (invalidation, add_call_to_trace proc_name call_location caller_history trace)
+    | Arithmetic (arith, trace) ->
+        Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace)
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
-    | Arithmetic _
     | Closure _
     | MustBeValid _
     | StdVectorReserve

infer/src/pulse/PulseAbductiveDomain.mli

@@ -80,7 +80,7 @@ module Memory : sig
   (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
       returns what it points to or creates a fresh value if that edge didn't exist.  *)
 
-  val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option
+  val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 end
 
 val is_local : Var.t -> t -> bool

infer/src/pulse/PulseAttribute.ml

@@ -29,7 +29,7 @@ module Attribute = struct
   type t =
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
-    | Arithmetic of Arithmetic.t
+    | Arithmetic of Arithmetic.t * Trace.t
     | Closure of Typ.Procname.t
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
@@ -60,7 +60,7 @@ module Attribute = struct
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
-  let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero))
+  let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero, dummy_trace))
 
   let pp f attribute =
     let pp_string_if_debug string fmt =
@@ -73,8 +73,8 @@ module Attribute = struct
         F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location
     | Closure pname ->
         Typ.Procname.pp f pname
-    | Arithmetic phi ->
-        Arithmetic.pp f phi
+    | Arithmetic (phi, trace) ->
+        F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> Arithmetic.pp fmt phi)) trace
     | Invalid (invalidation, trace) ->
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
@@ -137,8 +137,8 @@ module Attributes = struct
   let get_arithmetic attrs =
     Set.find_rank attrs Attribute.const_rank
     |> Option.map ~f:(fun attr ->
-           let[@warning "-8"] (Attribute.Arithmetic a) = attr in
-           a )
+           let[@warning "-8"] (Attribute.Arithmetic (a, trace)) = attr in
+           (a, trace) )
 
 
   include Set

infer/src/pulse/PulseAttribute.mli

@@ -14,7 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
-  | Arithmetic of Arithmetic.t
+  | Arithmetic of Arithmetic.t * Trace.t
   | Closure of Typ.Procname.t
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t
@@ -31,7 +31,7 @@ module Attributes : sig
 
   val get_closure_proc_name : t -> Typ.Procname.t option
 
-  val get_arithmetic : t -> Arithmetic.t option
+  val get_arithmetic : t -> (Arithmetic.t * Trace.t) option
 
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 

infer/src/pulse/PulseBaseMemory.mli

@@ -60,7 +60,7 @@ val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) resul
 
 val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
-val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option
+val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 

infer/src/pulse/PulseOperations.ml

@@ -134,7 +134,11 @@ let eval location exp0 astate =
     | Const (Cint i) ->
         (* TODO: make identical const the same address *)
         let addr = AbstractValue.mk_fresh () in
-        let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.equal_to i)) astate in
+        let astate =
+          Memory.add_attribute addr
+            (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
+            astate
+        in
         Ok (astate, (addr, []))
     | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
@@ -145,7 +149,12 @@ let eval location exp0 astate =
 let eval_arith location exp astate =
   match (exp : Exp.t) with
   | Const (Cint i) ->
-      Ok (astate, None, Some (Arithmetic.equal_to i))
+      Ok
+        ( astate
+        , None
+        , Some
+            ( Arithmetic.equal_to i
+            , Trace.Immediate {location; history= [ValueHistory.Assignment location]} ) )
   | exp -> (
       eval location exp astate
       >>| fun (astate, (addr, _)) ->
@@ -156,36 +165,51 @@ let eval_arith location exp astate =
           (astate, Some addr, None) )
 
 
-let record_abduced addr_opt arith_opt astate =
+let record_abduced ~is_then_branch if_kind location addr_opt orig_arith_hist_opt arith_opt astate =
   match Option.both addr_opt arith_opt with
   | None ->
       astate
   | Some (addr, arith) ->
-      let attribute = Attribute.Arithmetic arith in
+      let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
+      let trace =
+        match orig_arith_hist_opt with
+        | None ->
+            Trace.Immediate {location; history= [event]}
+        | Some (_, trace) ->
+            Trace.add_event event trace
+      in
+      let attribute = Attribute.Arithmetic (arith, trace) in
       Memory.abduce_attribute addr attribute astate |> Memory.add_attribute addr attribute
 
 
-let rec eval_cond ~negated location exp astate =
-  match (exp : Exp.t) with
-  | BinOp (bop, e1, e2) -> (
-      eval_arith location e1 astate
-      >>= fun (astate, addr1, eval1) ->
-      eval_arith location e2 astate
-      >>| fun (astate, addr2, eval2) ->
-      match Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 with
-      | Unsatisfiable ->
-          (astate, false)
-      | Satisfiable (abduced1, abduced2) ->
-          let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in
-          (astate, true) )
-  | UnOp (LNot, exp', _) ->
-      eval_cond ~negated:(not negated) location exp' astate
-  | exp ->
-      let zero = Exp.Const (Cint IntLit.zero) in
-      eval_cond ~negated location (Exp.BinOp (Ne, exp, zero)) astate
-
-
-let assert_is_true location ~condition astate = eval_cond ~negated:false location condition astate
+let prune ~is_then_branch if_kind location ~condition astate =
+  let rec prune_aux ~negated exp astate =
+    match (exp : Exp.t) with
+    | BinOp (bop, e1, e2) -> (
+        eval_arith location e1 astate
+        >>= fun (astate, addr1, eval1) ->
+        eval_arith location e2 astate
+        >>| fun (astate, addr2, eval2) ->
+        match
+          Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst eval1)
+            (Option.map ~f:fst eval2)
+        with
+        | Unsatisfiable ->
+            (astate, false)
+        | Satisfiable (abduced1, abduced2) ->
+            let astate =
+              record_abduced ~is_then_branch if_kind location addr1 eval1 abduced1 astate
+              |> record_abduced ~is_then_branch if_kind location addr2 eval2 abduced2
+            in
+            (astate, true) )
+    | UnOp (LNot, exp', _) ->
+        prune_aux ~negated:(not negated) exp' astate
+    | exp ->
+        let zero = Exp.Const (Cint IntLit.zero) in
+        prune_aux ~negated (Exp.BinOp (Ne, exp, zero)) astate
+  in
+  prune_aux ~negated:false condition astate
+
 
 let eval_deref location exp astate =
   eval location exp astate

infer/src/pulse/PulseOperations.mli

@@ -25,7 +25,13 @@ val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t))
     Return an error state if it traverses some known invalid address or if the end destination is
     known to be invalid. *)
 
-val assert_is_true : Location.t -> condition:Exp.t -> t -> (t * bool) access_result
+val prune :
+     is_then_branch:bool
+  -> Sil.if_kind
+  -> Location.t
+  -> condition:Exp.t
+  -> t
+  -> (t * bool) access_result
 
 val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Like [eval] but evaluates [*exp]. *)

infer/src/pulse/PulseTrace.ml

@@ -37,6 +37,13 @@ let rec pp ~pp_immediate fmt trace =
           in_call
 
 
+let add_event event = function
+  | Immediate {location; history} ->
+      Immediate {location; history= event :: history}
+  | ViaCall {f; in_call; location; history} ->
+      ViaCall {f; in_call; location; history= event :: history}
+
+
 let rec add_to_errlog ~nesting ~pp_immediate trace errlog =
   match trace with
   | Immediate {location; history} ->

infer/src/pulse/PulseTrace.mli

@@ -27,6 +27,8 @@ val get_outer_location : t -> Location.t
 val get_start_location : t -> Location.t
 (** initial step in the history if not empty, or else same as {!get_outer_location} *)
 
+val add_event : ValueHistory.event -> t -> t
+
 val add_to_errlog :
      nesting:int
   -> pp_immediate:(F.formatter -> unit)

infer/src/pulse/PulseValueHistory.ml

@@ -12,6 +12,7 @@ type event =
   | Assignment of Location.t
   | Call of {f: CallEvent.t; location: Location.t; in_call: t}
   | Capture of {captured_as: Pvar.t; location: Location.t}
+  | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t}
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t
   | VariableAccessed of Pvar.t * Location.t
@@ -31,6 +32,9 @@ let pp_event_no_location fmt event =
       F.fprintf fmt "passed as argument to %a" CallEvent.pp f
   | Capture {captured_as; location= _} ->
       F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as
+  | Conditional {is_then_branch; if_kind; location= _} ->
+      F.fprintf fmt "expression in %s condition is %b" (Sil.if_kind_to_string if_kind)
+        is_then_branch
   | CppTemporaryCreated _ ->
       F.pp_print_string fmt "C++ temporary created"
   | FormalDeclared (pvar, _) ->
@@ -49,6 +53,7 @@ let location_of_event = function
   | Assignment location
   | Call {location}
   | Capture {location}
+  | Conditional {location}
   | CppTemporaryCreated location
   | FormalDeclared (_, location)
   | VariableAccessed (_, location)

infer/src/pulse/PulseValueHistory.mli

@@ -12,6 +12,7 @@ type event =
   | Assignment of Location.t
   | Call of {f: CallEvent.t; location: Location.t; in_call: t}
   | Capture of {captured_as: Pvar.t; location: Location.t}
+  | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t}
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t
   | VariableAccessed of Pvar.t * Location.t