[pulse] initial commit

Summary:
New analysis in foetal form to detect invalid use of C++ objects after their
lifetime has ended. For now it has:
- A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended)
- The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid.
- A simple transfer function reads and updates the stack and heap in a rudimentary way for now
- C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations
- Also, the domain has a really crappy join and widening for now (see comments in the code)

With this we already pass most of the "use after delete" tests from the
Ownership checker. The ones we don't pass are only because we are missing
models.

Reviewed By: mbouaziz

Differential Revision: D10383249

fbshipit-source-id: f414664cb

Makefile

@@ -46,9 +46,24 @@ BUILD_SYSTEMS_TESTS += \
   utf8_in_procname \
 
 DIRECT_TESTS += \
-  c_biabduction c_bufferoverrun c_errors c_frontend c_performance c_uninit \
+  c_biabduction \
-  cpp_bufferoverrun cpp_errors cpp_frontend  cpp_liveness cpp_ownership cpp_quandary cpp_quandaryBO \
+  c_bufferoverrun \
-  cpp_racerd cpp_siof cpp_uninit cpp_nullable cpp_conflicts cpp_linters-for-test-only \
+  c_errors \
+  c_frontend \
+  c_performance \
+  c_uninit \
+  cpp_bufferoverrun \
+  cpp_conflicts \
+  cpp_errors \
+  cpp_frontend \
+  cpp_linters-for-test-only \
+  cpp_liveness \
+  cpp_nullable \
+  cpp_ownership cpp_pulse \
+  cpp_quandary cpp_quandaryBO \
+  cpp_racerd \
+  cpp_siof \
+  cpp_uninit \
 
 ifneq ($(BUCK),no)
 BUILD_SYSTEMS_TESTS += buck_blacklist buck-clang-db buck_flavors buck_flavors_run buck_flavors_deterministic

infer/man/man1/infer-analyze.txt

@@ -219,6 +219,14 @@ OPTIONS
        --project-root,-C dir
            Specify the root directory of the project (default: .)
 
+       --pulse
+           Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely:
+           --no-pulse)
+
+       --pulse-only
+           Activates: Enable --pulse and disable all other checkers
+           (Conversely: --no-pulse-only)
+
        --purity
            Activates: [EXPERIMENTAL] Purity analysis (Conversely:
            --no-purity)

infer/man/man1/infer-full.txt

@@ -650,6 +650,14 @@ OPTIONS
     See also infer-analyze(1), infer-capture(1), infer-report(1), and
            infer-run(1).
 
+       --pulse
+           Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely:
+           --no-pulse)           See also infer-analyze(1).
+
+       --pulse-only
+           Activates: Enable --pulse and disable all other checkers
+           (Conversely: --no-pulse-only)           See also infer-analyze(1).
+
        --purity
            Activates: [EXPERIMENTAL] Purity analysis (Conversely:
            --no-purity)           See also infer-analyze(1).

infer/man/man1/infer.txt

@@ -650,6 +650,14 @@ OPTIONS
     See also infer-analyze(1), infer-capture(1), infer-report(1), and
            infer-run(1).
 
+       --pulse
+           Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely:
+           --no-pulse)           See also infer-analyze(1).
+
+       --pulse-only
+           Activates: Enable --pulse and disable all other checkers
+           (Conversely: --no-pulse-only)           See also infer-analyze(1).
+
        --purity
            Activates: [EXPERIMENTAL] Purity analysis (Conversely:
            --no-purity)           See also infer-analyze(1).

infer/src/absint/AbstractDomain.ml

@@ -30,6 +30,18 @@ module type S = sig
   val pp : F.formatter -> astate -> unit
 end
 
+module Empty : S with type astate = unit = struct
+  type astate = unit
+
+  let ( <= ) ~lhs:() ~rhs:() = true
+
+  let join () () = ()
+
+  let widen ~prev:() ~next:() ~num_iters:_ = ()
+
+  let pp f () = F.pp_print_string f "()"
+end
+
 module type WithBottom = sig
   include S
 

infer/src/absint/AbstractDomain.mli

@@ -31,6 +31,15 @@ module type S = sig
   val pp : F.formatter -> astate -> unit
 end
 
+include
+  (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
+  sig
+    [@@@warning "-60"]
+
+    (** a trivial domain *)
+    module Empty : S with type astate = unit
+end
+
 (** A domain with an explicit bottom value *)
 module type WithBottom = sig
   include S

infer/src/base/Config.ml

@@ -598,6 +598,7 @@ and ( annotation_reachability
     , loop_hoisting
     , ownership
     , printf_args
+    , pulse
     , purity
     , quandary
     , quandaryBO
@@ -653,8 +654,9 @@ and ( annotation_reachability
       "the detection of mismatch between the Java printf format strings and the argument types \
        For, example, this checker will warn about the type error in `printf(\"Hello %d\", \
        \"world\")`"
-  and quandary = mk_checker ~long:"quandary" ~default:false "the quandary taint analysis"
+  and pulse = mk_checker ~long:"pulse" "[EXPERIMENTAL] C++ lifetime analysis"
   and purity = mk_checker ~long:"purity" ~default:false "[EXPERIMENTAL] Purity analysis"
+  and quandary = mk_checker ~long:"quandary" ~default:false "the quandary taint analysis"
   and quandaryBO =
     mk_checker ~long:"quandaryBO" ~default:false
       "[EXPERIMENTAL] The quandaryBO tainted buffer access analysis"
@@ -721,6 +723,7 @@ and ( annotation_reachability
   , loop_hoisting
   , ownership
   , printf_args
+  , pulse
   , purity
   , quandary
   , quandaryBO
@@ -2782,6 +2785,8 @@ and procs_csv = !procs_csv
 
 and project_root = !project_root
 
+and pulse = !pulse
+
 and purity = !purity
 
 and quandary = !quandary

infer/src/base/Config.mli

@@ -529,6 +529,8 @@ val project_root : string
 
 val progress_bar : [`MultiLine | `Plain | `Quiet]
 
+val pulse : bool
+
 val purity : bool
 
 val quandary : bool

infer/src/checkers/Pulse.ml

@@ -0,0 +1,72 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 F = Format
+open Result.Monad_infix
+
+let read astate access_expr =
+  PulseDomain.materialize_location astate access_expr
+  >>= fun (astate, loc) -> PulseDomain.check_loc_access loc astate
+
+
+let read_all access_exprs astate = List.fold_result access_exprs ~init:astate ~f:read
+
+let write access_expr astate =
+  PulseDomain.overwrite_location astate access_expr (PulseDomain.AbstractLocation.mk_fresh ())
+  >>| fun (astate, _) -> astate
+
+
+let check_error summary loc = function
+  | Ok astate ->
+      astate
+  | Error (astate, message) ->
+      Reporting.log_error summary ~loc IssueType.use_after_lifetime message ;
+      astate
+
+
+let invalidate access_expr astate =
+  PulseDomain.materialize_location astate access_expr
+  >>= fun (astate, loc) -> PulseDomain.check_loc_access loc astate >>| PulseDomain.mark_invalid loc
+
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = PulseDomain
+
+  type extras = Summary.t
+
+  let exec_instr (astate : Domain.astate) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
+      =
+    match instr with
+    | Assign (lhs_access, rhs_exp, loc) ->
+        (* we could be more precise and try and evaluate [rhs_exp] down to a location and use it to
+           record the value written instead of recording a fresh location *)
+        write lhs_access astate
+        >>= read_all (HilExp.get_access_exprs rhs_exp)
+        |> check_error summary loc
+    | Assume (condition, _, _, loc) ->
+        read_all (HilExp.get_access_exprs condition) astate |> check_error summary loc
+    | Call (_ret, HilInstr.Direct callee_pname, [AccessExpression deleted_access], _flags, loc)
+      when Typ.Procname.equal callee_pname BuiltinDecl.__delete ->
+        (* TODO: use {!ProcnameDispatcher.ProcName} instead of pattern matching name ourselves *)
+        invalidate deleted_access astate |> check_error summary loc
+    | Call (_ret, HilInstr.Direct _, actuals, _flags, loc)
+    | Call (_ret, HilInstr.Indirect _, actuals, _flags, loc) ->
+        (* TODO: function calls, right now we just register the reads of the arguments *)
+        read_all (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+        |> check_error summary loc
+
+
+  let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
+end
+
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
+
+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) ;
+  summary

infer/src/checkers/Pulse.mli

@@ -0,0 +1,9 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+val checker : Callbacks.proc_callback_args -> Summary.t

infer/src/checkers/PulseDomain.ml

@@ -0,0 +1,177 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 F = Format
+module L = Logging
+open Result.Monad_infix
+
+(** An abstract address in memory. *)
+module AbstractLocation : sig
+  type t = private int [@@deriving compare]
+
+  val equal : t -> t -> bool
+
+  val mk_fresh : unit -> t
+
+  val pp : F.formatter -> t -> unit
+end = struct
+  type t = int [@@deriving compare]
+
+  let equal = [%compare.equal: t]
+
+  let next_fresh = ref 0
+
+  let mk_fresh () =
+    let l = !next_fresh in
+    incr next_fresh ; l
+
+
+  let pp = F.pp_print_int
+end
+
+module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLocation.t = struct
+  type astate = AbstractLocation.t
+
+  let ( <= ) ~lhs ~rhs = AbstractLocation.equal lhs rhs
+
+  let join l1 l2 =
+    if AbstractLocation.equal l1 l2 then l1 else (* TODO: scary *) AbstractLocation.mk_fresh ()
+
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+
+  let pp = AbstractLocation.pp
+end
+
+module MemoryKey = struct
+  type t = AbstractLocation.t * AccessPath.access [@@deriving compare]
+
+  let pp f k = Pp.pair ~fst:AbstractLocation.pp ~snd:AccessPath.pp_access f k
+end
+
+module MemoryDomain = AbstractDomain.Map (MemoryKey) (AbstractLocationDomain)
+module AliasingDomain = AbstractDomain.Map (Var) (AbstractLocationDomain)
+module AbstractLocationsDomain = AbstractDomain.FiniteSet (AbstractLocation)
+module InvalidLocationsDomain = AbstractLocationsDomain
+
+type t =
+  {heap: MemoryDomain.astate; stack: AliasingDomain.astate; invalids: InvalidLocationsDomain.astate}
+
+module Domain : AbstractDomain.S with type astate = t = struct
+  type astate = t
+
+  (* This is very naive and should be improved. We can compare two memory graphs by trying to
+     establish that the graphs reachable from each root are the same up to some additional
+     unfolding, i.e. are not incompatible when we prune everything that is not reachable from the
+     roots. Here the roots are the known aliases in the stack since that's the only way to address
+     into the heap. *)
+  let ( <= ) ~lhs ~rhs =
+    phys_equal lhs rhs
+    || InvalidLocationsDomain.( <= ) ~lhs:lhs.invalids ~rhs:rhs.invalids
+       && AliasingDomain.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack
+       && MemoryDomain.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap
+
+
+  (* Like (<=) this is probably too naive *)
+  let join astate1 astate2 =
+    if phys_equal astate1 astate2 then astate1
+    else
+      { heap= MemoryDomain.join astate1.heap astate2.heap
+      ; stack= AliasingDomain.join astate1.stack astate2.stack
+      ; invalids= InvalidLocationsDomain.join astate1.invalids astate2.invalids }
+
+
+  let max_widening = 5
+
+  let widen ~prev ~next ~num_iters =
+    (* probably pretty obvious but that widening is just bad... We need to add a wildcard [*] to
+       access path elements in our graph representing repeated paths if we hope to converge (like
+       {!AccessPath.Abs.Abstracted}, we actually need something very similar). *)
+    if num_iters > max_widening then prev
+    else if phys_equal prev next then prev
+    else
+      { heap= MemoryDomain.widen ~num_iters ~prev:prev.heap ~next:next.heap
+      ; stack= AliasingDomain.widen ~num_iters ~prev:prev.stack ~next:next.stack
+      ; invalids= InvalidLocationsDomain.widen ~num_iters ~prev:prev.invalids ~next:next.invalids
+      }
+
+
+  let pp fmt {heap; stack; invalids} =
+    F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@;invalids=@[<hv>%a@];@]}"
+      MemoryDomain.pp heap AliasingDomain.pp stack InvalidLocationsDomain.pp invalids
+end
+
+include Domain
+
+let initial =
+  {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty}
+
+
+let check_loc_access loc astate =
+  if AbstractLocationsDomain.mem loc astate.invalids then
+    (* TODO: more structured error type so that we can actually report something informative about
+       the variables being accessed along with a trace *)
+    Error (astate, "invalid loc")
+  else Ok astate
+
+
+(** Walk the heap starting from [loc] and following [path]. Stop either at the element before last
+   and return [new_loc] if [overwrite_last] is [Some new_loc], or go until the end of the path if it
+   is [None]. Create more locations into the heap as needed to follow the [path]. Check that each
+   location reached is valid. *)
+let rec walk ~overwrite_last loc path astate =
+  match (path, overwrite_last) with
+  | [], None ->
+      Ok (astate, loc)
+  | [], Some _ ->
+      L.die InternalError "Cannot overwrite last location in empty path"
+  | [a], Some new_loc ->
+      check_loc_access loc astate
+      >>| fun astate ->
+      let heap = MemoryDomain.add (loc, a) new_loc astate.heap in
+      ({astate with heap}, new_loc)
+  | a :: path, _ -> (
+      check_loc_access loc astate
+      >>= fun astate ->
+      match MemoryDomain.find_opt (loc, a) astate.heap with
+      | None ->
+          let loc' = AbstractLocation.mk_fresh () in
+          let heap = MemoryDomain.add (loc, a) loc' astate.heap in
+          let astate = {astate with heap} in
+          walk ~overwrite_last loc' path astate
+      | Some loc' ->
+          walk ~overwrite_last loc' path astate )
+
+
+(** add locations to the state to give a location to the destination of the given access path *)
+let walk_access_expr ?overwrite_last astate access_expr =
+  let (access_var, _), access_list = AccessExpression.to_access_path access_expr in
+  match (overwrite_last, access_list) with
+  | Some new_loc, [] ->
+      let stack = AliasingDomain.add access_var new_loc astate.stack in
+      Ok ({astate with stack}, new_loc)
+  | None, _ | Some _, _ :: _ ->
+      let astate, base_loc =
+        match AliasingDomain.find_opt access_var astate.stack with
+        | Some loc ->
+            (astate, loc)
+        | None ->
+            let loc = AbstractLocation.mk_fresh () in
+            let stack = AliasingDomain.add access_var loc astate.stack in
+            ({astate with stack}, loc)
+      in
+      walk ~overwrite_last base_loc access_list astate
+
+
+let materialize_location astate access_expr = walk_access_expr astate access_expr
+
+let overwrite_location astate access_expr new_loc =
+  walk_access_expr ~overwrite_last:new_loc astate access_expr
+
+
+let mark_invalid loc astate =
+  {astate with invalids= AbstractLocationsDomain.add loc astate.invalids}

infer/src/checkers/PulseDomain.mli

@@ -0,0 +1,72 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 F = Format
+
+module AbstractLocation : sig
+  type t = private int [@@deriving compare]
+
+  val mk_fresh : unit -> t
+
+  val pp : F.formatter -> t -> unit
+end
+
+module MemoryKey : sig
+  type t = AbstractLocation.t * AccessPath.access [@@deriving compare]
+
+  val pp : F.formatter -> t -> unit
+end
+
+module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLocation.t
+
+module AbstractLocationsDomain : module type of AbstractDomain.FiniteSet (AbstractLocation)
+
+module MemoryDomain : module type of AbstractDomain.Map (MemoryKey) (AbstractLocationDomain)
+
+module AliasingDomain : module type of AbstractDomain.Map (Var) (AbstractLocationDomain)
+
+module InvalidLocationsDomain : module type of AbstractLocationsDomain
+
+type t =
+  { heap: MemoryDomain.astate
+        (** Symbolic representation of the heap: a graph where nodes are abstract locations and edges are
+            access path elements. *)
+  ; stack: AliasingDomain.astate
+        (** Symbolic representation of the stack: which memory location do variables point to. No other
+            values are being tracked. *)
+  ; invalids: InvalidLocationsDomain.astate
+        (** Set of locations known to be in an invalid state. *) }
+
+include AbstractDomain.S with type astate = t
+
+val initial : t
+
+val check_loc_access : AbstractLocation.t -> astate -> (astate, astate * string) result
+(** Check that the location is not known to be invalid *)
+
+val materialize_location :
+  astate -> AccessExpression.t -> (astate * AbstractLocation.t, astate * string) result
+(** Use the stack and heap to walk the access path represented by the given expression down to an
+    abstract location representing what the expression points to.
+
+    Return an error state if it traverses some known invalid location or if the end destination is
+    known to be invalid. *)
+
+val overwrite_location :
+     astate
+  -> AccessExpression.t
+  -> AbstractLocation.t
+  -> (astate * AbstractLocation.t, astate * string) result
+(** Use the stack and heap to walk the access path represented by the given expression down to an
+    abstract location representing what the expression points to, and replace that with the given
+    location.
+
+    Return an error state if it traverses some known invalid location. *)
+
+val mark_invalid : AbstractLocation.t -> astate -> astate
+(** Add the given location to the set of know invalid locations. *)

infer/src/checkers/registerCheckers.ml

@@ -77,6 +77,7 @@ let all_checkers =
   ; { name= "ownership"
     ; active= Config.ownership
     ; callbacks= [(Procedure Ownership.checker, Language.Clang)] }
+  ; {name= "pulse"; active= Config.pulse; callbacks= [(Procedure Pulse.checker, Language.Clang)]}
   ; { name= "quandary"
     ; active= Config.quandary || Config.quandaryBO
     ; callbacks=

infer/tests/codetoanalyze/cpp/pulse/Makefile

@@ -0,0 +1,17 @@
+# Copyright (c) 2018-present, Facebook, Inc.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+# see explanations in cpp/errors/Makefile for the custom isystem
+CLANG_OPTIONS = -x c++ -std=c++14 -Wc++1z-extensions -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard ../ownership/*.cpp)
+
+include $(TESTS_DIR)/clang.make
+
+infer-out/report.json: $(MAKEFILE_LIST)

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -0,0 +1,15 @@
+codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_throw_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_exit_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -0,0 +1,17 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <iostream>
+#include <vector>
+
+void FN_deref_vector_element_after_lifetime_bad() {
+  std::vector<int> x = {0, 0};
+  int* y = &x[1];
+  x.push_back(4);
+  std::cout << *y << "\n";
+}
+
+int main() { deref_vector_element_after_lifetime(); }